# HG changeset patch
# User boehmes
# Date 1289573771 -3600
# Node ID 516a367eb38cf311b281ad0e8224a0f185b6fe31
# Parent  25f2661442062748abfd189449dde7f8fcec2769
preliminary support for newer versions of Z3

diff -r 25f266144206 -r 516a367eb38c src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Fri Nov 12 15:56:10 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_real.ML	Fri Nov 12 15:56:11 2010 +0100
@@ -78,7 +78,8 @@
 local
   structure I = Z3_Interface
 
-  fun z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real}
+  fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
+    | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
     | z3_mk_builtin_typ _ = NONE
 
   fun z3_mk_builtin_num _ i T =
diff -r 25f266144206 -r 516a367eb38c src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Nov 12 15:56:10 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Nov 12 15:56:11 2010 +0100
@@ -155,7 +155,8 @@
 (* basic and additional constructors *)
 
 fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}
-  | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int}
+  | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
+  | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int}  (*FIXME: delete*)
   | mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym
 
 fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i)
diff -r 25f266144206 -r 516a367eb38c src/HOL/Tools/SMT/z3_proof_parser.ML
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Fri Nov 12 15:56:10 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Fri Nov 12 15:56:11 2010 +0100
@@ -13,7 +13,7 @@
     PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
     Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
     DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
-    CnfStar | Skolemize | ModusPonensOeq | ThLemma
+    CnfStar | Skolemize | ModusPonensOeq | ThLemma of string list
   val string_of_rule: rule -> string
 
   (* proof parser *)
@@ -41,7 +41,7 @@
   PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
   Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
   DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
-  CnfStar | Skolemize | ModusPonensOeq | ThLemma
+  CnfStar | Skolemize | ModusPonensOeq | ThLemma of string list
 
 val rule_names = Symtab.make [
   ("true-axiom", TrueAxiom),
@@ -81,11 +81,12 @@
   ("cnf*", CnfStar),
   ("sk", Skolemize),
   ("mp~", ModusPonensOeq),
-  ("th-lemma", ThLemma)]
+  ("th-lemma", ThLemma [])]
 
-fun string_of_rule r =
-  let fun eq_rule (s, r') = if r = r' then SOME s else NONE 
-  in the (Symtab.get_first eq_rule rule_names) end
+fun string_of_rule (ThLemma args) = space_implode " " ("th-lemma" :: args)
+  | string_of_rule r =
+      let fun eq_rule (s, r') = if r = r' then SOME s else NONE 
+      in the (Symtab.get_first eq_rule rule_names) end
 
 
 
@@ -271,14 +272,17 @@
 
 fun $$ s = Scan.lift (Scan.$$ s)
 fun this s = Scan.lift (Scan.this_string s)
-fun blank st = Scan.lift (Scan.many1 Symbol.is_ascii_blank) st
+val is_blank = Symbol.is_ascii_blank
+fun blank st = Scan.lift (Scan.many1 is_blank) st
 fun sep scan = blank |-- scan
 fun seps scan = Scan.repeat (sep scan)
 fun seps1 scan = Scan.repeat1 (sep scan)
 fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan)
 
-fun par scan = $$ "(" |-- scan --| $$ ")"
-fun bra scan = $$ "[" |-- scan --| $$ "]"
+val lpar = "(" and rpar = ")"
+val lbra = "[" and rbra = "]"
+fun par scan = $$ lpar |-- scan --| $$ rpar
+fun bra scan = $$ lbra |-- scan --| $$ rbra
 
 val digit = (fn
   "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
@@ -368,8 +372,14 @@
   Scan.first [bound, quantifier, pattern, application, number, constant] :|--
   with_context (pair NONE oo add_expr k)
 
+fun th_lemma_arg st =
+  Scan.lift (Scan.many1 (not o (is_blank orf equal rbra)) >> implode) st
+
 fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn 
-    (SOME r, _) => Scan.succeed r
+    (SOME (ThLemma _), _) =>
+      let fun stop st = (sep id >> K "" || $$ rbra) st
+      in Scan.repeat (Scan.unless stop (sep th_lemma_arg)) >> ThLemma end
+  | (SOME r, _) => Scan.succeed r
   | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st
 
 fun rule f k =
diff -r 25f266144206 -r 516a367eb38c src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Nov 12 15:56:10 2010 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Nov 12 15:56:11 2010 +0100
@@ -787,7 +787,7 @@
     | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
 
       (* theory rules *)
-    | (P.ThLemma, _) =>
+    | (P.ThLemma _, _) =>  (* FIXME: use arguments *)
         (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
     | (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp)
     | (P.RewriteStar, ps) =>