Bugs in TIP-to-Isabelle translation #7
Description
Omar Montano Rivas has tested the TIP-to-Isabelle translation and found a number of bugs:
He also wishes to have a pass which translates properties to Isabelle with Frees instead of Vars (i.e. x not ?x).
-- Variable names are not translated properly to Isabelle/HOL as they sometimes clash with the ASCII representation of HOL constants. e.g. 'EX'
, 'o', etc. For example, the following definition is not accepted by the Isabelle outer syntax parser. The culprit is the name of the variable 'o' in the last equation of the definition. A potential solution would be to just rename the variable 'o' to some new fresh variable.
fun minus :: "Nat => Nat => Integer" where
"minus (Z) (Z) = P Z"
| "minus (Z) (S n) = N n"
| "minus (S m) (Z) = P (S m)"
| "minus (S m) (S o) = minus m o"
-- Identifiers in SMT files such as '1' are not properly translated into Isabelle/HOL. e.g.
fun 1 :: "Nat" where
"1 = S Z"
A potential solution would be to use the definition command using a proper identifier. e.g.
definition id1 :: "Nat" ("1") where
[simp]: "id1 = S Z"
Here we use the fresh identifier 'id1' and add it to Isabelle/HOL's simpset to simulate the fun command. An alternative would be to use a syntax translation.
-- Constants with non-functional type are not properly translated to Isabelle/HOL as fun does not support the definition of functions with atomic type (Probably a syntax translation or the definition command would be more suitable). e.g.
fun one :: "Nat" where
"one = S Z"
I think the previous suggested solution would work here.
-- A harder problem to fix is that some definition translations, can not be proved to terminate automatically by fun such as:
fun interleave :: "'a list => 'a list => 'a list" where
"interleave (nil2) y = y"
| "interleave (cons2 z xs) y = cons2 z (interleave y xs)"
Here it occurs to me to make a call to 'isabelle_process' to see if fun can handle the definition. If not, the definition can be phrased with the 'function' command to give it a try to the size_change automatic method, which in this case solves the pending goals.
function (sequential) interleave :: "'a list => 'a list => 'a list" where
"interleave (nil2) y = y"
| "interleave (cons2 z xs) y = cons2 z (interleave y xs)"
by pat_completeness auto
termination by size_change
Of course this will not work in all cases such as:
function (sequential) weirdconcat :: "('a list) list => 'a list" where
"weirdconcat (nil2) = nil2"
| "weirdconcat (cons2 (nil2) xss) = weirdconcat xss"
| "weirdconcat (cons2 (cons2 z xs) xss) =
cons2 z (weirdconcat (cons2 xs xss))"
by pat_completeness auto
termination by size_change
The 'relation' method can be used for such cases but I think it would be more difficult to come up with the decreasing measure automatically. One last think that can be done and will work on most cases is to use partiality. For example, if lexicographic order and size_change fail, instead making the translation like this:
fun m :: "int => int" where
"m x = (if x > 100 then x - 10 else m (m (x + 11)))"
theorem x0 :
"!! (n :: int) . ((n <= 100) ==> ((m n) = 91))"
by induct_auto_astar
We can do it with the equivalent (where m is partial and terminates under n ("m_dom n" holds)):
function m :: "int => int" where
"m x = (if x > 100 then x - 10 else m (m (x + 11)))"
by pat_completeness auto
theorem x0 :
"!! (n :: int) . m_dom n ⟹ ((n <= 100) ==> ((m n) = 91))"
-- Other problem is not produced by the translator itself but by the smt2 file. e.g. the file tip2015/list_z_elem.smt2 only contains "(check-sat)". This can be just me not downloading an updated version of the repository.
-- Another one is not the fault of the translator because Isabelle does not support non-linear datatypes. e.g polyrec_seq_index.smt2 file produces.
datatype 'a list = nil2 | cons2 "'a" "'a list"
datatype ('a, 'b) Pair = Pair2 "'a" "'b"
datatype 'a Maybe = Nothing | Just "'a"
datatype 'a Seq = Nil2 | Cons2 "'a" "(('a, ('a Maybe)) Pair) Seq"
-- I can see the translator uses partiality to some extend with the file propositional_AndCommutative.smt2 but some errors are produced. My first guess is that non-constructor patterns are used in definitions:
e.g.
models ( p q) y = models2 q (models p y)"