Is function declaration a term of type Constant and how to cast such function declaration to Const class?

Question

I am trying to use https://github.com/dominique-unruh/scala-isabelle for parsing and decomposing the Isabelle terms and I am trying to decompose term - function declaration - from the formalization of quicksort https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html - this Isabelle code:

function quicksort :: "'a::{heap,linorder} array ⇒ nat ⇒ nat ⇒ unit Heap"
where
  "quicksort arr left right =
     (if (right > left)  then
        do {
          pivotNewIndex ← partition arr left right;
          pivotNewIndex ← assert (λx. left ≤ x ∧ x ≤ right) pivotNewIndex;
          quicksort arr left (pivotNewIndex - 1);
          quicksort arr (pivotNewIndex + 1) right
        }
     else return ())"
by pat_completeness auto

I am trying to use in Scala/Isabelle:

println("Before qs term")
val qs_term = Term(ctxt, "quicksort arr left right =" +
  "    (if (right > left)  then" +
  "        do {" +
  "          pivotNewIndex ← partition arr left right;" +
  "          pivotNewIndex ← assert (λx. left ≤ x ∧ x ≤ right) pivotNewIndex;" +
  "          quicksort arr left (pivotNewIndex - 1);" +
  "          quicksort arr (pivotNewIndex + 1) right" +
  "        }" +
  "     else return ())")
println("After qs term")

I am checking the documentation for the Term class: https://javadoc.io/doc/de.unruh/scala-isabelle_2.13/latest/de/unruh/isabelle/pure/Term.html and I see that there is Const constructor for this Term:

sealed abstract class Term
final case class Const(name: String, typ: Typ)            // Corresponds to ML constructor 'Const'
...

My question is: is the Isabelle function declaration an instance of Term with class constructor Const? And how can I cast my qs_term to class Const with the aim to access fields that are specific to Const? My aim is to do tree-search (DFS, BFS) over the class (taking Const class as the root object) and in such way to construct AST for this function declaration.

Answer 1

What you have constructed is not a definition of quicksort (at least not in the sense that it would define anything in Isabelle), but a simply a term that expresses the property that you want that quicksort should satisfy.

The function command in Isar (and also the definition command) takes the specification (e.g., the term you wrote) and transforms it internally into two parts: a name of the constant you define (here TheoryName.quicksort), and a term that says what quicksort should be defined as (here λarr left right. (if ...)).

If you want to create a definition programmatically in Isabelle (no matter whether Isabelle/ML), you need to:

1. Get a context (e.g., Context("TheoryName")) (or a theory).
2. Apply a suitable command for creating a definition. There is no predefined command for that in scala-isabelle, so you have to use the ML-code that does this and wrap it using MLValue.compileFunction (ScalaDoc). This function then takes your context (or theory) as well as the constant name and the term and further information, and returns a new theory or context that has the value defined. (E.g., Local_Defs.define in local_defs.ML is such a function, I think.)

The class Const has nothing to do with what you are asking. A term in Isabelle is a tree with different kinds of leafs. Some of the leafs are variables, and some of the leafs are constants. For example, if you traverse your quicksort-term, you will find, e.g., that partition and assert are constants and thus represented using class Const.