1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Fri Nov 12 15:56:10 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Fri Nov 12 15:56:11 2010 +0100
     1.3 @@ -78,7 +78,8 @@
     1.4  local
     1.5    structure I = Z3_Interface
     1.6  
     1.7 -  fun z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real}
     1.8 +  fun z3_mk_builtin_typ (I.Sym ("Real", _)) = SOME @{typ real}
     1.9 +    | z3_mk_builtin_typ (I.Sym ("real", _)) = SOME @{typ real} (*FIXME: delete*)
    1.10      | z3_mk_builtin_typ _ = NONE
    1.11  
    1.12    fun z3_mk_builtin_num _ i T =

     2.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Fri Nov 12 15:56:10 2010 +0100
     2.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Fri Nov 12 15:56:11 2010 +0100
     2.3 @@ -155,7 +155,8 @@
     2.4  (* basic and additional constructors *)
     2.5  
     2.6  fun mk_builtin_typ _ (Sym ("bool", _)) = SOME @{typ bool}
     2.7 -  | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int}
     2.8 +  | mk_builtin_typ _ (Sym ("Int", _)) = SOME @{typ int}
     2.9 +  | mk_builtin_typ _ (Sym ("int", _)) = SOME @{typ int}  (*FIXME: delete*)
    2.10    | mk_builtin_typ ctxt sym = chained_mk_builtin_typ (get_mk_builtins ctxt) sym
    2.11  
    2.12  fun mk_builtin_num _ i @{typ int} = SOME (Numeral.mk_cnumber @{ctyp int} i)

     3.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Fri Nov 12 15:56:10 2010 +0100
     3.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Fri Nov 12 15:56:11 2010 +0100
     3.3 @@ -13,7 +13,7 @@
     3.4      PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
     3.5      Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
     3.6      DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
     3.7 -    CnfStar | Skolemize | ModusPonensOeq | ThLemma
     3.8 +    CnfStar | Skolemize | ModusPonensOeq | ThLemma of string list
     3.9    val string_of_rule: rule -> string
    3.10  
    3.11    (* proof parser *)
    3.12 @@ -41,7 +41,7 @@
    3.13    PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
    3.14    Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
    3.15    DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
    3.16 -  CnfStar | Skolemize | ModusPonensOeq | ThLemma
    3.17 +  CnfStar | Skolemize | ModusPonensOeq | ThLemma of string list
    3.18  
    3.19  val rule_names = Symtab.make [
    3.20    ("true-axiom", TrueAxiom),
    3.21 @@ -81,11 +81,12 @@
    3.22    ("cnf*", CnfStar),
    3.23    ("sk", Skolemize),
    3.24    ("mp~", ModusPonensOeq),
    3.25 -  ("th-lemma", ThLemma)]
    3.26 +  ("th-lemma", ThLemma [])]
    3.27  
    3.28 -fun string_of_rule r =
    3.29 -  let fun eq_rule (s, r') = if r = r' then SOME s else NONE 
    3.30 -  in the (Symtab.get_first eq_rule rule_names) end
    3.31 +fun string_of_rule (ThLemma args) = space_implode " " ("th-lemma" :: args)
    3.32 +  | string_of_rule r =
    3.33 +      let fun eq_rule (s, r') = if r = r' then SOME s else NONE 
    3.34 +      in the (Symtab.get_first eq_rule rule_names) end
    3.35  
    3.36  
    3.37  
    3.38 @@ -271,14 +272,17 @@
    3.39  
    3.40  fun $$ s = Scan.lift (Scan.$$ s)
    3.41  fun this s = Scan.lift (Scan.this_string s)
    3.42 -fun blank st = Scan.lift (Scan.many1 Symbol.is_ascii_blank) st
    3.43 +val is_blank = Symbol.is_ascii_blank
    3.44 +fun blank st = Scan.lift (Scan.many1 is_blank) st
    3.45  fun sep scan = blank |-- scan
    3.46  fun seps scan = Scan.repeat (sep scan)
    3.47  fun seps1 scan = Scan.repeat1 (sep scan)
    3.48  fun seps_by scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan)
    3.49  
    3.50 -fun par scan = $$ "(" |-- scan --| $$ ")"
    3.51 -fun bra scan = $$ "[" |-- scan --| $$ "]"
    3.52 +val lpar = "(" and rpar = ")"
    3.53 +val lbra = "[" and rbra = "]"
    3.54 +fun par scan = $$ lpar |-- scan --| $$ rpar
    3.55 +fun bra scan = $$ lbra |-- scan --| $$ rbra
    3.56  
    3.57  val digit = (fn
    3.58    "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
    3.59 @@ -368,8 +372,14 @@
    3.60    Scan.first [bound, quantifier, pattern, application, number, constant] :|--
    3.61    with_context (pair NONE oo add_expr k)
    3.62  
    3.63 +fun th_lemma_arg st =
    3.64 +  Scan.lift (Scan.many1 (not o (is_blank orf equal rbra)) >> implode) st
    3.65 +
    3.66  fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn 
    3.67 -    (SOME r, _) => Scan.succeed r
    3.68 +    (SOME (ThLemma _), _) =>
    3.69 +      let fun stop st = (sep id >> K "" || $$ rbra) st
    3.70 +      in Scan.repeat (Scan.unless stop (sep th_lemma_arg)) >> ThLemma end
    3.71 +  | (SOME r, _) => Scan.succeed r
    3.72    | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st
    3.73  
    3.74  fun rule f k =

     4.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Nov 12 15:56:10 2010 +0100
     4.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Fri Nov 12 15:56:11 2010 +0100
     4.3 @@ -787,7 +787,7 @@
     4.4      | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
     4.5  
     4.6        (* theory rules *)
     4.7 -    | (P.ThLemma, _) =>
     4.8 +    | (P.ThLemma _, _) =>  (* FIXME: use arguments *)
     4.9          (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
    4.10      | (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp)
    4.11      | (P.RewriteStar, ps) =>