split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)
--- a/src/HOL/IsaMakefile Wed May 12 23:53:58 2010 +0200
+++ b/src/HOL/IsaMakefile Wed May 12 23:53:59 2010 +0200
@@ -1247,9 +1247,10 @@
SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML \
SMT/Tools/z3_interface.ML SMT/Tools/smt_additional_facts.ML \
SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML \
- SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML \
- SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML \
- SMT/Tools/z3_model.ML SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML
+ SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_parser.ML \
+ SMT/Tools/z3_proof_tools.ML SMT/Tools/z3_proof_literals.ML \
+ SMT/Tools/z3_proof_reconstruction.ML SMT/Tools/z3_model.ML \
+ SMT/Tools/z3_solver.ML $(SRC)/Tools/cache_io.ML
@cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT
--- a/src/HOL/SMT/Tools/z3_proof.ML Wed May 12 23:53:58 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,251 +0,0 @@
-(* Title: HOL/SMT/Tools/z3_proof.ML
- Author: Sascha Boehme, TU Muenchen
-
-Proof reconstruction for proofs found by Z3.
-*)
-
-signature Z3_PROOF =
-sig
- val reconstruct: Proof.context -> SMT_Translate.recon -> string list -> thm
-end
-
-structure Z3_Proof: Z3_PROOF =
-struct
-
-structure T = Z3_Proof_Terms
-structure R = Z3_Proof_Rules
-
-fun z3_exn msg = raise SMT_Solver.SMT ("Z3 proof reconstruction: " ^ msg)
-
-
-fun lift f (x, y) = apsnd (pair x) (f y)
-fun lift' f v (x, y) = apsnd (rpair y) (f v x)
-
-fun $$ s = lift (Scan.$$ s)
-fun this s = lift (Scan.this_string s)
-
-fun blank s = lift (Scan.many1 Symbol.is_ascii_blank) s
-
-fun par scan = $$ "(" |-- scan --| $$ ")"
-fun bra scan = $$ "[" |-- scan --| $$ "]"
-
-val digit = (fn
- "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
- "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
- "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
-
-val nat_num = Scan.repeat1 (Scan.some digit) >>
- (fn ds => fold (fn d => fn i => i * 10 + d) ds 0)
-val int_num = Scan.optional (Scan.$$ "-" >> K (fn i => ~i)) I :|--
- (fn sign => nat_num >> sign)
-
-val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
- member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
-val name = Scan.many1 is_char >> implode
-
-datatype sym = Sym of string * sym list
-
-datatype context = Context of {
- Ttab: typ Symtab.table,
- ttab: cterm Symtab.table,
- etab: T.preterm Inttab.table,
- ptab: R.proof Inttab.table,
- nctxt: Name.context }
-
-fun make_context (Ttab, ttab, etab, ptab, nctxt) =
- Context {Ttab=Ttab, ttab=ttab, etab=etab, ptab=ptab, nctxt=nctxt}
-
-fun empty_context thy ({typs, terms, ...} : SMT_Translate.recon) =
- let
- val ttab = Symtab.map (fn @{term True} => @{term "~False"} | t => t) terms
- val ns = Symtab.fold (Term.add_free_names o snd) ttab []
- val nctxt = Name.make_context ns
- val ttab' = Symtab.map (Thm.cterm_of thy) ttab
- in make_context (typs, ttab', Inttab.empty, Inttab.empty, nctxt) end
-
-fun map_context f (Context {Ttab, ttab, etab, ptab, nctxt}) =
- make_context (f (Ttab, ttab, etab, ptab, nctxt))
-
-fun map_type_tab f = map_context (fn (Ttab, ttab, etab, ptab, nctxt) =>
- (f Ttab, ttab, etab, ptab, nctxt))
-
-fun map_term_tab f = map_context (fn (Ttab, ttab, etab, ptab, nctxt) =>
- (Ttab, f ttab, etab, ptab, nctxt))
-
-fun map_expr_tab f = map_context (fn (Ttab, ttab, etab, ptab, nctxt) =>
- (Ttab, ttab, f etab, ptab, nctxt))
-
-fun map_proof_tab f = map_context (fn (Ttab, ttab, etab, ptab, nctxt) =>
- (Ttab, ttab, etab, f ptab, nctxt))
-
-val free_prefix = "f"
-
-fun fresh_name (cx as Context {nctxt, ...}) =
- let val (n, nctxt') = yield_singleton Name.variants free_prefix nctxt
- in
- (n, map_context (fn (Ttab, ttab, etab, ptab, _) =>
- (Ttab, ttab, etab, ptab, nctxt')) cx)
- end
-
-fun typ_of_sort name (cx as Context {Ttab, ...}) =
- (case Symtab.lookup Ttab name of
- SOME T => (T, cx)
- | _ => cx |> fresh_name |-> (fn n =>
- let val T = TFree ("'" ^ n, @{sort type})
- in pair T o map_type_tab (Symtab.update (name, T)) end))
-
-fun lookup_expr id (cx as Context {etab, ...}) =
- (case Inttab.lookup etab id of
- SOME e => (e, cx)
- | _ => z3_exn ("unknown term id: " ^ quote (string_of_int id)))
-
-fun add_expr k t = map_expr_tab (Inttab.update (k, t))
-
-fun add_proof thy k ((r, ps), t) (cx as Context {nctxt, ...}) =
- let val p = R.make_proof r ps (T.compile thy nctxt t)
- in (k, map_proof_tab (Inttab.update (k, p)) cx) end
-
-fun mk_app app (cx as Context {ttab, ...}) =
- let
- val mk =
- (fn
- (Sym ("true", _), _) => T.mk_true
- | (Sym ("false", _), _) => T.mk_false
- | (Sym ("=", _), [t, u]) => T.mk_eq t u
- | (Sym ("distinct", _), ts) => T.mk_distinct ts
- | (Sym ("ite", _), [s, t, u]) => T.mk_if s t u
- | (Sym ("and", _), ts) => T.mk_and ts
- | (Sym ("or", _), ts) => T.mk_or ts
- | (Sym ("iff", _), [t, u]) => T.mk_iff t u
- | (Sym ("xor", _), [t, u]) => T.mk_not (T.mk_iff t u)
- | (Sym ("not", _), [t]) => T.mk_not t
- | (Sym ("implies", _), [t, u]) => T.mk_implies t u
- | (Sym ("~", _), [t, u]) => T.mk_eq t u
- | (Sym ("<", _), [t, u]) => T.mk_lt t u
- | (Sym ("<=", _), [t, u]) => T.mk_le t u
- | (Sym (">", _), [t, u]) => T.mk_lt u t
- | (Sym (">=", _), [t, u]) => T.mk_le u t
- | (Sym ("+", _), [t, u]) => T.mk_add t u
- | (Sym ("-", _), [t, u]) => T.mk_sub t u
- | (Sym ("-", _), [t]) => T.mk_uminus t
- | (Sym ("*", _), [t, u]) => T.mk_mul t u
- | (Sym ("/", _), [t, u]) => T.mk_real_div t u
- | (Sym ("div", _), [t, u]) => T.mk_int_div t u
- | (Sym ("mod", _), [t, u]) => T.mk_mod t u
- | (Sym ("rem", _), [t, u]) => T.mk_rem t u
- | (Sym ("select", _), [m, k]) => T.mk_access m k
- | (Sym ("store", _), [m, k, v]) => T.mk_update m k v
- | (Sym ("array-ext", _), [m1, m2]) => T.mk_array_ext m1 m2
- | (Sym ("pattern", _), _) => T.mk_true
- | (Sym (n, _), ts) =>
- (case Symtab.lookup ttab n of
- SOME ct => T.mk_fun ct ts
- | NONE => z3_exn ("unknown function: " ^ quote n)))
- in (mk app, cx) end
-
-fun add_decl thy (n, T) (cx as Context {ttab, ...}) =
- (case Symtab.lookup ttab n of
- SOME _ => cx
- | _ => cx |> fresh_name |-> (fn n' =>
- map_term_tab (Symtab.update (n, Thm.cterm_of thy (Free (n', T))))))
-
-
-fun sep scan_sep scan = scan ::: Scan.repeat (scan_sep |-- scan)
-fun bsep scan = Scan.repeat (blank |-- scan)
-fun bsep1 scan = Scan.repeat1 (blank |-- scan)
-
-val id = Scan.$$ "#" |-- int_num
-
-fun sym s =
- (lift name -- Scan.optional (bra (sep ($$ ":") sym)) [] >> Sym) s
-
-fun sort st = Scan.first [
- this "bool" >> K @{typ bool},
- this "int" >> K @{typ int},
- this "real" >> K @{typ real},
- this "bv" |-- bra (lift int_num) >> T.wordT,
- this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
- par (this "->" |-- bsep1 sort) >> ((op --->) o split_last),
- lift name #-> lift' typ_of_sort] st
-
-fun bound thy =
- par (this ":var" -- blank |-- lift int_num --| blank -- sort) >>
- uncurry (T.mk_bound thy)
-
-val number =
- int_num -- Scan.option (Scan.$$ "/" |-- int_num) --|
- Scan.this_string "::" :|-- (fn num as (n, _) =>
- Scan.this_string "int" >> K (T.mk_int_num n) ||
- Scan.this_string "real" >> K (T.mk_real_frac_num num))
-
-fun bv_number thy =
- this "bv" |-- bra (lift (int_num --| Scan.$$ ":" -- int_num)) >>
- uncurry (T.mk_bv_num thy)
-
-val constant = sym #-> lift' (mk_app o rpair [])
-
-fun arg thy = Scan.first [lift id #-> lift' lookup_expr,
- lift number, bv_number thy, constant]
-
-fun application thy =
- par (sym -- bsep1 (arg thy)) #-> lift' mk_app
-
-val variables =
- par (this "vars" |-- bsep1 (par ((lift name >> K "x") --| blank -- sort)))
-fun patterns st =
- bsep (par ((this ":pat" || this ":nopat") |-- bsep1 (lift id))) st
-fun quant_kind st =
- (this "forall" >> K T.mk_forall ||
- this "exists" >> K T.mk_exists) st
-fun quantifier thy = par (quant_kind --| blank --
- variables --| patterns --| blank -- arg thy) >>
- (fn ((q, vs), body) => fold_rev (q thy) vs body)
-
-fun expr thy k = Scan.first [bound thy, quantifier thy, application thy,
- lift number, bv_number thy, constant] #-> apfst o add_expr k
-
-fun rule_name name =
- (case R.rule_of_string name of
- SOME r => r
- | NONE => z3_exn ("unknown proof rule: " ^ quote name))
-
-fun rule thy k =
- bra (lift (name >> rule_name) -- bsep (lift id)) --|
- ($$ ":" -- blank) -- arg thy #-> lift' (add_proof thy k)
-
-fun decl thy = ((this "decl" -- blank) |-- lift name --|
- (blank -- this "::" -- blank) -- sort) #-> apfst o add_decl thy
-
-fun def st = (lift id --| (blank -- this ":=" -- blank)) st
-
-fun node thy =
- decl thy #> pair NONE ||
- def :|-- (fn k => expr thy k #> pair NONE || rule thy k #>> K NONE) ||
- rule thy ~1 #>> SOME
-
-fun handle_errors line_no scan (st as (_, xs)) =
- (case try scan st of
- SOME y => y
- | NONE => z3_exn ("parse error at line " ^ string_of_int line_no ^ ": " ^
- quote (implode xs)))
-
-fun parse_line thy l (st as (stop, line_no, cx)) =
- if is_some stop then st
- else
- (cx, explode l)
- |> handle_errors line_no (Scan.finite' Symbol.stopper (node thy))
- |> (fn (stop', (cx', _)) => (stop', line_no + 1, cx'))
-
-fun reconstruct ctxt recon output =
- let
- val _ = T.var_prefix <> free_prefix orelse error "Same prefixes"
-
- val thy = ProofContext.theory_of ctxt
- val {unfolds, assms, ...} = recon
- in
- (case fold (parse_line thy) output (NONE, 1, empty_context thy recon) of
- (SOME p, _, Context {ptab, ...}) => R.prove ctxt unfolds assms ptab p
- | _ => z3_exn "bad proof")
- end
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/z3_proof_literals.ML Wed May 12 23:53:59 2010 +0200
@@ -0,0 +1,346 @@
+(* Title: HOL/SMT/Tools/z3_proof_literals.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Proof tools related to conjunctions and disjunctions.
+*)
+
+signature Z3_PROOF_LITERALS =
+sig
+ (* literal table *)
+ type littab = thm Termtab.table
+ val make_littab: thm list -> littab
+ val insert_lit: thm -> littab -> littab
+ val delete_lit: thm -> littab -> littab
+ val lookup_lit: littab -> term -> thm option
+ val get_first_lit: (term -> bool) -> littab -> thm option
+
+ (* rules *)
+ val true_thm: thm
+ val rewrite_true: thm
+
+ (* properties *)
+ val is_conj: term -> bool
+ val is_disj: term -> bool
+ val exists_lit: bool -> (term -> bool) -> term -> bool
+
+ (* proof tools *)
+ val explode: bool -> bool -> bool -> term list -> thm -> thm list
+ val join: bool -> littab -> term -> thm
+ val prove_conj_disj_eq: cterm -> thm
+end
+
+structure Z3_Proof_Literals: Z3_PROOF_LITERALS =
+struct
+
+structure T = Z3_Proof_Tools
+
+
+
+(** literal table **)
+
+type littab = thm Termtab.table
+
+fun make_littab thms = fold (Termtab.update o `T.prop_of) thms Termtab.empty
+
+fun insert_lit thm = Termtab.update (`T.prop_of thm)
+fun delete_lit thm = Termtab.delete (T.prop_of thm)
+fun lookup_lit lits = Termtab.lookup lits
+fun get_first_lit f =
+ Termtab.get_first (fn (t, thm) => if f t then SOME thm else NONE)
+
+
+
+(** rules **)
+
+val true_thm = @{lemma "~False" by simp}
+val rewrite_true = @{lemma "True == ~ False" by simp}
+
+
+
+(** properties and term operations **)
+
+val is_neg = (fn @{term Not} $ _ => true | _ => false)
+fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
+val is_dneg = is_neg' is_neg
+val is_conj = (fn @{term "op &"} $ _ $ _ => true | _ => false)
+val is_disj = (fn @{term "op |"} $ _ $ _ => true | _ => false)
+
+fun dest_disj_term' f = (fn
+ @{term Not} $ (@{term "op |"} $ t $ u) => SOME (f t, f u)
+ | _ => NONE)
+
+val dest_conj_term = (fn @{term "op &"} $ t $ u => SOME (t, u) | _ => NONE)
+val dest_disj_term =
+ dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
+
+fun exists_lit is_conj P =
+ let
+ val dest = if is_conj then dest_conj_term else dest_disj_term
+ fun exists t = P t orelse
+ (case dest t of
+ SOME (t1, t2) => exists t1 orelse exists t2
+ | NONE => false)
+ in exists end
+
+
+
+(** proof tools **)
+
+(* explosion of conjunctions and disjunctions *)
+
+local
+ fun destc ct = Thm.dest_binop (Thm.dest_arg ct)
+ val dest_conj1 = T.precompose2 destc @{thm conjunct1}
+ val dest_conj2 = T.precompose2 destc @{thm conjunct2}
+ fun dest_conj_rules t =
+ dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2))
+
+ fun destd f ct = f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct)))
+ val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg
+ val dest_disj1 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
+ val dest_disj2 = T.precompose2 (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
+ val dest_disj3 = T.precompose2 (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
+ val dest_disj4 = T.precompose2 (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
+
+ fun dest_disj_rules t =
+ (case dest_disj_term' is_neg t of
+ SOME (true, true) => SOME (dest_disj2, dest_disj4)
+ | SOME (true, false) => SOME (dest_disj2, dest_disj3)
+ | SOME (false, true) => SOME (dest_disj1, dest_disj4)
+ | SOME (false, false) => SOME (dest_disj1, dest_disj3)
+ | NONE => NONE)
+
+ fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
+ val dneg_rule = T.precompose destn @{thm notnotD}
+in
+
+(* explode a term into literals and collect all rules to be able to deduce
+ particular literals afterwards *)
+fun explode_term is_conj =
+ let
+ val dest = if is_conj then dest_conj_term else dest_disj_term
+ val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
+
+ fun add (t, rs) = Termtab.map_default (t, rs)
+ (fn rs' => if length rs' < length rs then rs' else rs)
+
+ fun explode1 rules t =
+ (case dest t of
+ SOME (t1, t2) =>
+ let val (rule1, rule2) = the (dest_rules t)
+ in
+ explode1 (rule1 :: rules) t1 #>
+ explode1 (rule2 :: rules) t2 #>
+ add (t, rev rules)
+ end
+ | NONE => add (t, rev rules))
+
+ fun explode0 (@{term Not} $ (@{term Not} $ t)) =
+ Termtab.make [(t, [dneg_rule])]
+ | explode0 t = explode1 [] t Termtab.empty
+
+ in explode0 end
+
+(* extract a literal by applying previously collected rules *)
+fun extract_lit thm rules = fold T.compose rules thm
+
+
+(* explode a theorem into its literals *)
+fun explode is_conj full keep_intermediate stop_lits =
+ let
+ val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
+ val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
+
+ fun explode1 thm =
+ if Termtab.defined tab (T.prop_of thm) then cons thm
+ else
+ (case dest_rules (T.prop_of thm) of
+ SOME (rule1, rule2) =>
+ explode2 rule1 thm #>
+ explode2 rule2 thm #>
+ keep_intermediate ? cons thm
+ | NONE => cons thm)
+
+ and explode2 dest_rule thm =
+ if full orelse exists_lit is_conj (Termtab.defined tab) (T.prop_of thm)
+ then explode1 (T.compose dest_rule thm)
+ else cons (T.compose dest_rule thm)
+
+ fun explode0 thm =
+ if not is_conj andalso is_dneg (T.prop_of thm)
+ then [T.compose dneg_rule thm]
+ else explode1 thm []
+
+ in explode0 end
+
+end
+
+
+
+(* joining of literals to conjunctions or disjunctions *)
+
+local
+ fun on_cprem i f thm = f (Thm.cprem_of thm i)
+ fun on_cprop f thm = f (Thm.cprop_of thm)
+ fun precomp2 f g thm = (on_cprem 1 f thm, on_cprem 2 g thm, f, g, thm)
+ fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
+ Thm.instantiate ([], [(cv1, on_cprop f thm1), (cv2, on_cprop g thm2)]) rule
+ |> T.discharge thm1 |> T.discharge thm2
+
+ fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
+
+ val conj_rule = precomp2 d1 d1 @{thm conjI}
+ fun comp_conj ((_, thm1), (_, thm2)) = comp2 conj_rule thm1 thm2
+
+ val disj1 = precomp2 d2 d2 @{lemma "~P ==> ~Q ==> ~(P | Q)" by fast}
+ val disj2 = precomp2 d2 d1 @{lemma "~P ==> Q ==> ~(P | ~Q)" by fast}
+ val disj3 = precomp2 d1 d2 @{lemma "P ==> ~Q ==> ~(~P | Q)" by fast}
+ val disj4 = precomp2 d1 d1 @{lemma "P ==> Q ==> ~(~P | ~Q)" by fast}
+
+ fun comp_disj ((false, thm1), (false, thm2)) = comp2 disj1 thm1 thm2
+ | comp_disj ((false, thm1), (true, thm2)) = comp2 disj2 thm1 thm2
+ | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
+ | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
+
+ fun dest_conj (@{term "op &"} $ t $ u) = ((false, t), (false, u))
+ | dest_conj t = raise TERM ("dest_conj", [t])
+
+ val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
+ fun dest_disj (@{term Not} $ (@{term "op |"} $ t $ u)) = (neg t, neg u)
+ | dest_disj t = raise TERM ("dest_disj", [t])
+
+ val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
+ val dnegI = T.precompose (single o d1) @{lemma "P ==> ~~P" by fast}
+ fun as_dneg f t = f (@{term Not} $ (@{term Not} $ t))
+
+ fun dni f = apsnd f o Thm.dest_binop o f o d1
+ val negIffE = T.precompose2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
+ val negIffI = T.precompose2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
+ val iff_const = @{term "op = :: bool => _"}
+ fun as_negIff f (@{term "op = :: bool => _"} $ t $ u) =
+ f (@{term Not} $ (iff_const $ u $ (@{term Not} $ t)))
+ | as_negIff _ _ = NONE
+in
+
+fun join is_conj littab t =
+ let
+ val comp = if is_conj then comp_conj else comp_disj
+ val dest = if is_conj then dest_conj else dest_disj
+
+ val lookup = lookup_lit littab
+
+ fun lookup_rule t =
+ (case t of
+ @{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
+ | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
+ (T.compose negIffI, lookup (iff_const $ u $ t))
+ | @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
+ let fun rewr lit = lit COMP @{thm not_sym}
+ in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
+ | _ =>
+ (case as_dneg lookup t of
+ NONE => (T.compose negIffE, as_negIff lookup t)
+ | x => (T.compose dnegE, x)))
+
+ fun join1 (s, t) =
+ (case lookup t of
+ SOME lit => (s, lit)
+ | NONE =>
+ (case lookup_rule t of
+ (rewrite, SOME lit) => (s, rewrite lit)
+ | (_, NONE) => (s, comp (pairself join1 (dest t)))))
+
+ in snd (join1 (if is_conj then (false, t) else (true, t))) end
+
+end
+
+
+
+(* proving equality of conjunctions or disjunctions *)
+
+fun iff_intro thm1 thm2 = thm2 COMP (thm1 COMP @{thm iffI})
+
+local
+ val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
+ val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastsimp}
+ val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
+ val neg = Thm.capply @{cterm Not}
+in
+fun contrapos1 prove (ct, cu) = prove (neg ct, neg cu) COMP cp1
+fun contrapos2 prove (ct, cu) = prove (neg ct, Thm.dest_arg cu) COMP cp2
+fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, neg cu) COMP cp3
+end
+
+
+local
+ val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
+ fun contra_left conj thm =
+ let
+ val rules = explode_term conj (T.prop_of thm)
+ fun contra_lits (t, rs) =
+ (case t of
+ @{term Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
+ | _ => NONE)
+ in
+ (case Termtab.lookup rules @{term False} of
+ SOME rs => extract_lit thm rs
+ | NONE =>
+ the (Termtab.get_first contra_lits rules)
+ |> pairself (extract_lit thm)
+ |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
+ end
+
+ val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
+ fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
+in
+fun contradict conj ct =
+ iff_intro (T.under_assumption (contra_left conj) ct) (contra_right ct)
+end
+
+
+local
+ fun prove_eq l r (cl, cr) =
+ let
+ fun explode' is_conj = explode is_conj true (l <> r) []
+ fun make_tab is_conj thm = make_littab (true_thm :: explode' is_conj thm)
+ fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct)
+
+ val thm1 = T.under_assumption (prove r cr o make_tab l) cl
+ val thm2 = T.under_assumption (prove l cl o make_tab r) cr
+ in iff_intro thm1 thm2 end
+
+ datatype conj_disj = CONJ | DISJ | NCON | NDIS
+ fun kind_of t =
+ if is_conj t then SOME CONJ
+ else if is_disj t then SOME DISJ
+ else if is_neg' is_conj t then SOME NCON
+ else if is_neg' is_disj t then SOME NDIS
+ else NONE
+in
+
+fun prove_conj_disj_eq ct =
+ let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
+ in
+ (case (kind_of (Thm.term_of cl), Thm.term_of cr) of
+ (SOME CONJ, @{term False}) => contradict true cl
+ | (SOME DISJ, @{term "~False"}) => contrapos2 (contradict false o fst) cp
+ | (kl, _) =>
+ (case (kl, kind_of (Thm.term_of cr)) of
+ (SOME CONJ, SOME CONJ) => prove_eq true true cp
+ | (SOME CONJ, SOME NDIS) => prove_eq true false cp
+ | (SOME CONJ, _) => prove_eq true true cp
+ | (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp
+ | (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp
+ | (SOME DISJ, _) => contrapos1 (prove_eq false false) cp
+ | (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp
+ | (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp
+ | (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp
+ | (SOME NDIS, SOME NDIS) => prove_eq false false cp
+ | (SOME NDIS, SOME CONJ) => prove_eq false true cp
+ | (SOME NDIS, NONE) => prove_eq false true cp
+ | _ => raise CTERM ("prove_conj_disj_eq", [ct])))
+ end
+
+end
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/z3_proof_parser.ML Wed May 12 23:53:59 2010 +0200
@@ -0,0 +1,499 @@
+(* Title: HOL/SMT/Tools/z3_proof_parser.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Parser for Z3 proofs.
+*)
+
+signature Z3_PROOF_PARSER =
+sig
+ (* proof rules *)
+ datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
+ Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro |
+ Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant |
+ PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
+ Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
+ DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
+ CnfStar | Skolemize | ModusPonensOeq | ThLemma
+ val string_of_rule: rule -> string
+
+ (* proof parser *)
+ datatype proof_step = Proof_Step of {
+ rule: rule,
+ prems: int list,
+ prop: cterm }
+ val parse: Proof.context -> typ Symtab.table -> term Symtab.table ->
+ string list ->
+ int * (proof_step Inttab.table * string list * Proof.context)
+end
+
+structure Z3_Proof_Parser: Z3_PROOF_PARSER =
+struct
+
+(** proof rules **)
+
+datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
+ Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro |
+ Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant |
+ PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
+ Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
+ DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
+ CnfStar | Skolemize | ModusPonensOeq | ThLemma
+
+val rule_names = Symtab.make [
+ ("true-axiom", TrueAxiom),
+ ("asserted", Asserted),
+ ("goal", Goal),
+ ("mp", ModusPonens),
+ ("refl", Reflexivity),
+ ("symm", Symmetry),
+ ("trans", Transitivity),
+ ("trans*", TransitivityStar),
+ ("monotonicity", Monotonicity),
+ ("quant-intro", QuantIntro),
+ ("distributivity", Distributivity),
+ ("and-elim", AndElim),
+ ("not-or-elim", NotOrElim),
+ ("rewrite", Rewrite),
+ ("rewrite*", RewriteStar),
+ ("pull-quant", PullQuant),
+ ("pull-quant*", PullQuantStar),
+ ("push-quant", PushQuant),
+ ("elim-unused", ElimUnusedVars),
+ ("der", DestEqRes),
+ ("quant-inst", QuantInst),
+ ("hypothesis", Hypothesis),
+ ("lemma", Lemma),
+ ("unit-resolution", UnitResolution),
+ ("iff-true", IffTrue),
+ ("iff-false", IffFalse),
+ ("commutativity", Commutativity),
+ ("def-axiom", DefAxiom),
+ ("intro-def", IntroDef),
+ ("apply-def", ApplyDef),
+ ("iff~", IffOeq),
+ ("nnf-pos", NnfPos),
+ ("nnf-neg", NnfNeg),
+ ("nnf*", NnfStar),
+ ("cnf*", CnfStar),
+ ("sk", Skolemize),
+ ("mp~", ModusPonensOeq),
+ ("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
+
+
+
+(** certified terms and variables **)
+
+val (var_prefix, decl_prefix) = ("v", "sk") (* must be distinct *)
+
+fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
+fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
+fun mk_inst_pair destT cpat = (destT (Thm.ctyp_of_term cpat), cpat)
+val destT1 = hd o Thm.dest_ctyp
+val destT2 = hd o tl o Thm.dest_ctyp
+
+fun ctyp_of (ct, _) = Thm.ctyp_of_term ct
+fun instT' t = instT (ctyp_of t)
+
+fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
+
+val maxidx_of = #maxidx o Thm.rep_cterm
+
+fun mk_inst ctxt vars =
+ let
+ val max = fold (Integer.max o fst) vars 0
+ val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
+ fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
+ in map mk vars end
+
+fun close ctxt (ct, vars) =
+ let
+ val inst = mk_inst ctxt vars
+ val mk_prop = Thm.capply @{cterm Trueprop}
+ val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
+ in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
+
+
+fun mk_bound thy (i, T) =
+ let val ct = Thm.cterm_of thy (Var ((Name.uu, 0), T))
+ in (ct, [(i, ct)]) end
+
+local
+ fun mk_quant thy q T (ct, vars) =
+ let
+ val cv =
+ (case AList.lookup (op =) vars 0 of
+ SOME cv => cv
+ | _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T)))
+ val cq = instT (Thm.ctyp_of_term cv) q
+ fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
+ in (Thm.capply cq (Thm.cabs cv ct), map_filter dec vars) end
+
+ val forall = mk_inst_pair (destT1 o destT1) @{cpat All}
+ val exists = mk_inst_pair (destT1 o destT1) @{cpat Ex}
+in
+fun mk_forall thy = fold_rev (mk_quant thy forall)
+fun mk_exists thy = fold_rev (mk_quant thy exists)
+end
+
+
+local
+ fun equal_var cv (_, cu) = (cv aconvc cu)
+
+ fun apply (ct2, vars2) (ct1, vars1) =
+ let
+ val incr = Thm.incr_indexes_cterm (maxidx_of ct1 + maxidx_of ct2 + 2)
+
+ fun part (v as (i, cv)) =
+ (case AList.lookup (op =) vars1 i of
+ SOME cu => apfst (if cu aconvc cv then I else cons (cv, cu))
+ | NONE =>
+ if not (exists (equal_var cv) vars1) then apsnd (cons v)
+ else
+ let val cv' = incr cv
+ in apfst (cons (cv, cv')) #> apsnd (cons (i, cv')) end)
+
+ val (ct2', vars2') =
+ if null vars1 then (ct2, vars2)
+ else fold part vars2 ([], [])
+ |>> (fn inst => Thm.instantiate_cterm ([], inst) ct2)
+
+ in (Thm.capply ct1 ct2', vars1 @ vars2') end
+in
+fun mk_fun ct ts = fold apply ts (ct, [])
+fun mk_binop f t u = mk_fun f [t, u]
+fun mk_nary _ e [] = e
+ | mk_nary ct _ es = uncurry (fold_rev (mk_binop ct)) (split_last es)
+end
+
+
+val mk_true = mk_fun @{cterm "~False"} []
+val mk_false = mk_fun @{cterm "False"} []
+fun mk_not t = mk_fun @{cterm Not} [t]
+val mk_imp = mk_binop @{cterm "op -->"}
+val mk_iff = mk_binop @{cterm "op = :: bool => _"}
+
+val eq = mk_inst_pair destT1 @{cpat "op ="}
+fun mk_eq t u = mk_binop (instT' t eq) t u
+
+val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
+fun mk_if c t u = mk_fun (instT' t if_term) [c, t, u]
+
+val nil_term = mk_inst_pair destT1 @{cpat Nil}
+val cons_term = mk_inst_pair destT1 @{cpat Cons}
+fun mk_list cT es =
+ fold_rev (mk_binop (instT cT cons_term)) es (mk_fun (instT cT nil_term) [])
+
+val distinct = mk_inst_pair (destT1 o destT1) @{cpat distinct}
+fun mk_distinct [] = mk_true
+ | mk_distinct (es as (e :: _)) =
+ mk_fun (instT' e distinct) [mk_list (ctyp_of e) es]
+
+
+(* arithmetic *)
+
+fun mk_int_num i = mk_fun (Numeral.mk_cnumber @{ctyp int} i) []
+fun mk_real_num i = mk_fun (Numeral.mk_cnumber @{ctyp real} i) []
+fun mk_real_frac_num (e, NONE) = mk_real_num e
+ | mk_real_frac_num (e, SOME d) =
+ mk_binop @{cterm "op / :: real => _"} (mk_real_num e) (mk_real_num d)
+
+fun has_int_type e = (Thm.typ_of (ctyp_of e) = @{typ int})
+fun choose e i r = if has_int_type e then i else r
+
+val uminus_i = @{cterm "uminus :: int => _"}
+val uminus_r = @{cterm "uminus :: real => _"}
+fun mk_uminus e = mk_fun (choose e uminus_i uminus_r) [e]
+
+fun arith_op int_op real_op t u = mk_binop (choose t int_op real_op) t u
+
+val mk_add = arith_op @{cterm "op + :: int => _"} @{cterm "op + :: real => _"}
+val mk_sub = arith_op @{cterm "op - :: int => _"} @{cterm "op - :: real => _"}
+val mk_mul = arith_op @{cterm "op * :: int => _"} @{cterm "op * :: real => _"}
+val mk_int_div = mk_binop @{cterm "op div :: int => _"}
+val mk_real_div = mk_binop @{cterm "op / :: real => _"}
+val mk_mod = mk_binop @{cterm "op mod :: int => _"}
+val mk_lt = arith_op @{cterm "op < :: int => _"} @{cterm "op < :: real => _"}
+val mk_le = arith_op @{cterm "op <= :: int => _"} @{cterm "op <= :: real => _"}
+
+
+(* arrays *)
+
+val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat apply}
+fun mk_access array index =
+ let val cTs = Thm.dest_ctyp (ctyp_of array)
+ in mk_fun (instTs cTs access) [array, index] end
+
+val update = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_upd}
+fun mk_update array index value =
+ let val cTs = Thm.dest_ctyp (ctyp_of array)
+ in mk_fun (instTs cTs update) [array, index, value] end
+
+
+(* bitvectors *)
+
+fun mk_binT size =
+ let
+ fun bitT i T =
+ if i = 0
+ then Type (@{type_name "Numeral_Type.bit0"}, [T])
+ else Type (@{type_name "Numeral_Type.bit1"}, [T])
+
+ fun binT i =
+ if i = 0 then @{typ "Numeral_Type.num0"}
+ else if i = 1 then @{typ "Numeral_Type.num1"}
+ else let val (q, r) = Integer.div_mod i 2 in bitT r (binT q) end
+ in
+ if size >= 0 then binT size
+ else raise TYPE ("mk_binT: " ^ string_of_int size, [], [])
+ end
+
+fun mk_wordT size = Type (@{type_name "word"}, [mk_binT size])
+
+fun mk_bv_num thy (num, size) =
+ mk_fun (Numeral.mk_cnumber (Thm.ctyp_of thy (mk_wordT size)) num) []
+
+
+
+(** proof parser **)
+
+datatype proof_step = Proof_Step of {
+ rule: rule,
+ prems: int list,
+ prop: cterm }
+
+
+(* parser context *)
+
+fun make_context ctxt typs terms =
+ let
+ val ctxt' =
+ ctxt
+ |> Symtab.fold (Variable.declare_typ o snd) typs
+ |> Symtab.fold (Variable.declare_term o snd) terms
+
+ fun cert @{term True} = @{cterm "~False"}
+ | cert t = certify ctxt' t
+ in (typs, Symtab.map cert terms, Inttab.empty, Inttab.empty, [], ctxt') end
+
+fun fresh_name n (typs, terms, exprs, steps, vars, ctxt) =
+ let val (n', ctxt') = yield_singleton Variable.variant_fixes n ctxt
+ in (n', (typs, terms, exprs, steps, vars, ctxt')) end
+
+fun theory_of (_, _, _, _, _, ctxt) = ProofContext.theory_of ctxt
+
+fun typ_of_sort n (cx as (typs, _, _, _, _, _)) =
+ (case Symtab.lookup typs n of
+ SOME T => (T, cx)
+ | NONE => cx
+ |> fresh_name ("'" ^ n) |>> TFree o rpair @{sort type}
+ |> (fn (T, (typs, terms, exprs, steps, vars, ctxt)) =>
+ (T, (Symtab.update (n, T) typs, terms, exprs, steps, vars, ctxt))))
+
+fun add_decl (n, T) (cx as (_, terms, _, _, _, _)) =
+ (case Symtab.lookup terms n of
+ SOME _ => cx
+ | NONE => cx |> fresh_name (decl_prefix ^ n)
+ |> (fn (m, (typs, terms, exprs, steps, vars, ctxt)) =>
+ let val upd = Symtab.update (n, certify ctxt (Free (m, T)))
+ in (typs, upd terms, exprs, steps, vars, ctxt) end))
+
+datatype sym = Sym of string * sym list
+
+fun mk_app _ (Sym ("true", _), _) = SOME mk_true
+ | mk_app _ (Sym ("false", _), _) = SOME mk_false
+ | mk_app _ (Sym ("=", _), [t, u]) = SOME (mk_eq t u)
+ | mk_app _ (Sym ("distinct", _), ts) = SOME (mk_distinct ts)
+ | mk_app _ (Sym ("ite", _), [s, t, u]) = SOME (mk_if s t u)
+ | mk_app _ (Sym ("and", _), ts) = SOME (mk_nary @{cterm "op &"} mk_true ts)
+ | mk_app _ (Sym ("or", _), ts) = SOME (mk_nary @{cterm "op |"} mk_false ts)
+ | mk_app _ (Sym ("iff", _), [t, u]) = SOME (mk_iff t u)
+ | mk_app _ (Sym ("xor", _), [t, u]) = SOME (mk_not (mk_iff t u))
+ | mk_app _ (Sym ("not", _), [t]) = SOME (mk_not t)
+ | mk_app _ (Sym ("implies", _), [t, u]) = SOME (mk_imp t u)
+ | mk_app _ (Sym ("~", _), [t, u]) = SOME (mk_iff t u)
+ | mk_app _ (Sym ("<", _), [t, u]) = SOME (mk_lt t u)
+ | mk_app _ (Sym ("<=", _), [t, u]) = SOME (mk_le t u)
+ | mk_app _ (Sym (">", _), [t, u]) = SOME (mk_lt u t)
+ | mk_app _ (Sym (">=", _), [t, u]) = SOME (mk_le u t)
+ | mk_app _ (Sym ("+", _), [t, u]) = SOME (mk_add t u)
+ | mk_app _ (Sym ("-", _), [t, u]) = SOME (mk_sub t u)
+ | mk_app _ (Sym ("-", _), [t]) = SOME (mk_uminus t)
+ | mk_app _ (Sym ("*", _), [t, u]) = SOME (mk_mul t u)
+ | mk_app _ (Sym ("/", _), [t, u]) = SOME (mk_real_div t u)
+ | mk_app _ (Sym ("div", _), [t, u]) = SOME (mk_int_div t u)
+ | mk_app _ (Sym ("mod", _), [t, u]) = SOME (mk_mod t u)
+ | mk_app _ (Sym ("select", _), [m, k]) = SOME (mk_access m k)
+ | mk_app _ (Sym ("store", _), [m, k, v]) = SOME (mk_update m k v)
+ | mk_app _ (Sym ("pattern", _), _) = SOME mk_true
+ | mk_app (_, terms, _, _, _, _) (Sym (n, _), ts) =
+ Symtab.lookup terms n |> Option.map (fn ct => mk_fun ct ts)
+
+fun add_expr k t (typs, terms, exprs, steps, vars, ctxt) =
+ (typs, terms, Inttab.update (k, t) exprs, steps, vars, ctxt)
+
+fun lookup_expr (_, _, exprs, _, _, _) = Inttab.lookup exprs
+
+fun add_proof_step k ((r, prems), prop) cx =
+ let
+ val (typs, terms, exprs, steps, vars, ctxt) = cx
+ val (ct, vs) = close ctxt prop
+ val step = Proof_Step {rule=r, prems=prems, prop=ct}
+ val vars' = union (op =) vs vars
+ in (typs, terms, exprs, Inttab.update (k, step) steps, vars', ctxt) end
+
+fun finish (_, _, _, steps, vars, ctxt) = (steps, vars, ctxt)
+
+
+(* core parser *)
+
+fun parse_exn line_no msg = raise SMT_Solver.SMT ("Z3 proof parser (line " ^
+ string_of_int line_no ^ "): " ^ msg)
+
+fun scan_exn msg ((line_no, _), _) = parse_exn line_no msg
+
+fun with_info f cx =
+ (case f ((NONE, 1), cx) of
+ ((SOME root, _), cx') => (root, cx')
+ | ((_, line_no), _) => parse_exn line_no "bad proof")
+
+fun parse_line _ _ (st as ((SOME _, _), _)) = st
+ | parse_line scan line ((_, line_no), cx) =
+ let val st = ((line_no, cx), explode line)
+ in
+ (case Scan.catch (Scan.finite' Symbol.stopper (Scan.option scan)) st of
+ (SOME r, ((_, cx'), _)) => ((r, line_no+1), cx')
+ | (NONE, _) => parse_exn line_no ("bad proof line: " ^ quote line))
+ end
+
+fun with_context f x ((line_no, cx), st) =
+ let val (y, cx') = f x cx
+ in (y, ((line_no, cx'), st)) end
+
+
+fun lookup_context f x (st as ((_, cx), _)) = (f cx x, st)
+
+
+(* parser combinators and parsers for basic entities *)
+
+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
+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 digit = (fn
+ "0" => SOME 0 | "1" => SOME 1 | "2" => SOME 2 | "3" => SOME 3 |
+ "4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
+ "8" => SOME 8 | "9" => SOME 9 | _ => NONE)
+
+fun mk_num ds = fold (fn d => fn i => i * 10 + d) ds 0
+val nat_num = Scan.lift (Scan.repeat1 (Scan.some digit)) >> mk_num
+val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
+ (fn sign => nat_num >> sign)
+
+val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
+ member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
+val name = Scan.lift (Scan.many1 is_char) >> implode
+
+fun sym st = (name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> Sym) st
+
+fun id st = ($$ "#" |-- nat_num) st
+
+
+(* parsers for various parts of Z3 proofs *)
+
+fun sort st = Scan.first [
+ this "bool" >> K @{typ bool},
+ this "int" >> K @{typ int},
+ this "real" >> K @{typ real},
+ this "bv" |-- bra nat_num >> mk_wordT,
+ this "array" |-- bra (sort --| $$ ":" -- sort) >> (op -->),
+ par (this "->" |-- seps1 sort) >> ((op --->) o split_last),
+ name :|-- with_context typ_of_sort] st
+
+fun bound st = (par (this ":var" |-- sep nat_num -- sep sort) :|--
+ lookup_context (mk_bound o theory_of)) st
+
+fun number st = st |> (
+ int_num -- Scan.option ($$ "/" |-- int_num) --| this "::" :|--
+ (fn num as (n, _) =>
+ this "int" >> K (mk_int_num n) ||
+ this "real" >> K (mk_real_frac_num num)))
+
+fun bv_number st = (this "bv" |-- bra (nat_num --| $$ ":" -- nat_num) :|--
+ lookup_context (mk_bv_num o theory_of)) st
+
+fun appl (app as (Sym (n, _), _)) = lookup_context mk_app app :|-- (fn
+ SOME app' => Scan.succeed app'
+ | NONE => scan_exn ("unknown function: " ^ quote n))
+
+fun constant st = ((sym >> rpair []) :|-- appl) st
+
+fun expr_id st = (id :|-- (fn i => lookup_context lookup_expr i :|-- (fn
+ SOME e => Scan.succeed e
+ | NONE => scan_exn ("unknown term id: " ^ quote (string_of_int i))))) st
+
+fun arg st = Scan.first [expr_id, number, bv_number, constant] st
+
+fun application st = par ((sym -- Scan.repeat1 (sep arg)) :|-- appl) st
+
+fun variables st = par (this "vars" |-- seps1 (par (name |-- sep sort))) st
+
+fun patterns st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
+
+fun quant_kind st = st |> (
+ this "forall" >> K (mk_forall o theory_of) ||
+ this "exists" >> K (mk_exists o theory_of))
+
+fun quantifier st =
+ (par (quant_kind -- sep variables --| patterns -- sep arg) :|--
+ lookup_context (fn cx => fn ((mk_q, Ts), body) => mk_q cx Ts body)) st
+
+fun expr k =
+ Scan.first [bound, quantifier, application, number, bv_number, constant] :|--
+ with_context (pair NONE oo add_expr k)
+
+fun rule_name st = ((name >> `(Symtab.lookup rule_names)) :|-- (fn
+ (SOME r, _) => Scan.succeed r
+ | (NONE, n) => scan_exn ("unknown proof rule: " ^ quote n))) st
+
+fun rule f k =
+ bra (rule_name -- seps id) --| $$ ":" -- sep arg #->
+ with_context (pair (f k) oo add_proof_step k)
+
+fun decl st = (this "decl" |-- sep name --| sep (this "::") -- sep sort :|--
+ with_context (pair NONE oo add_decl)) st
+
+fun def st = (id --| sep (this ":=")) st
+
+fun node st = st |> (
+ decl ||
+ def :|-- (fn k => sep (expr k) || sep (rule (K NONE) k)) ||
+ rule SOME ~1)
+
+
+(* overall parser *)
+
+(* Currently, terms are parsed bottom-up (i.e., along with parsing the proof
+ text line by line), but proofs are reconstructed top-down (i.e. by an
+ in-order top-down traversal of the proof tree/graph). The latter approach
+ was taken because some proof texts comprise irrelevant proof steps which
+ will thus not be reconstructed. This approach might also be beneficial
+ for constructing terms, but it would also increase the complexity of the
+ (otherwise rather modular) code. *)
+
+fun parse ctxt typs terms proof_text =
+ make_context ctxt typs terms
+ |> with_info (fold (parse_line node) proof_text)
+ ||> finish
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/z3_proof_reconstruction.ML Wed May 12 23:53:59 2010 +0200
@@ -0,0 +1,831 @@
+(* Title: HOL/SMT/Tools/z3_proof_reconstruction.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Proof reconstruction for proofs found by Z3.
+*)
+
+signature Z3_PROOF_RECONSTRUCTION =
+sig
+ val trace_assms: bool Config.T
+ val reconstruct: Proof.context -> SMT_Translate.recon -> string list -> thm
+ val setup: theory -> theory
+end
+
+structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
+struct
+
+structure P = Z3_Proof_Parser
+structure T = Z3_Proof_Tools
+structure L = Z3_Proof_Literals
+
+fun z3_exn msg = raise SMT_Solver.SMT ("Z3 proof reconstruction: " ^ msg)
+
+
+
+(** net of schematic rules **)
+
+val z3_ruleN = "z3_rule"
+
+local
+ val description = "declaration of Z3 proof rules"
+
+ val eq = Thm.eq_thm
+
+ structure Z3_Rules = Generic_Data
+ (
+ type T = thm Net.net
+ val empty = Net.empty
+ val extend = I
+ val merge = Net.merge eq
+ )
+
+ val prep = `Thm.prop_of o Simplifier.rewrite_rule [L.rewrite_true]
+
+ fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
+ fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
+
+ val add = Thm.declaration_attribute (Z3_Rules.map o ins)
+ val del = Thm.declaration_attribute (Z3_Rules.map o del)
+in
+
+fun get_schematic_rules ctxt = Net.content (Z3_Rules.get (Context.Proof ctxt))
+
+fun by_schematic_rule ctxt ct =
+ the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
+
+val z3_rules_setup =
+ Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
+ PureThy.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
+
+end
+
+
+
+(** proof tools **)
+
+fun named ctxt name prover ct =
+ let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
+ in prover ct end
+
+fun NAMED ctxt name tac i st =
+ let val _ = SMT_Solver.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
+ in tac i st end
+
+fun pretty_goal ctxt thms t =
+ [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
+ |> not (null thms) ? cons (Pretty.big_list "assumptions:"
+ (map (Display.pretty_thm ctxt) thms))
+
+fun try_apply ctxt thms =
+ let
+ fun try_apply_err ct = Pretty.string_of (Pretty.chunks [
+ Pretty.big_list ("Z3 found a proof," ^
+ " but proof reconstruction failed at the following subgoal:")
+ (pretty_goal ctxt thms (Thm.term_of ct)),
+ Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^
+ " might solve this problem.")])
+
+ fun apply [] ct = error (try_apply_err ct)
+ | apply (prover :: provers) ct =
+ (case try prover ct of
+ SOME thm => (SMT_Solver.trace_msg ctxt I "Z3: succeeded"; thm)
+ | NONE => apply provers ct)
+
+ in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end
+
+
+
+(** theorems and proofs **)
+
+(* theorem incarnations *)
+
+datatype theorem =
+ Thm of thm | (* theorem without special features *)
+ MetaEq of thm | (* meta equality "t == s" *)
+ Literals of thm * L.littab
+ (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *)
+
+fun thm_of (Thm thm) = thm
+ | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq}
+ | thm_of (Literals (thm, _)) = thm
+
+fun meta_eq_of (MetaEq thm) = thm
+ | meta_eq_of p = mk_meta_eq (thm_of p)
+
+fun literals_of (Literals (_, lits)) = lits
+ | literals_of p = L.make_littab [thm_of p]
+
+
+(* proof representation *)
+
+datatype proof =
+ Unproved of P.proof_step |
+ Sequent of { hyps: cterm list, thm: theorem }
+
+
+
+(** core proof rules **)
+
+(* assumption *)
+
+val (trace_assms, trace_assms_setup) =
+ Attrib.config_bool "z3_trace_assms" (K false)
+
+local
+ val remove_trigger = @{lemma "trigger t p == p"
+ by (rule eq_reflection, rule trigger_def)}
+
+ val prep_rules = [@{thm Let_def}, remove_trigger, L.rewrite_true]
+
+ fun rewrite_conv ctxt eqs =
+ More_Conv.top_conv (K (Conv.try_conv (More_Conv.rewrs_conv eqs))) ctxt
+
+ fun rewrite_rules eqs = map (Simplifier.rewrite_rule eqs)
+
+ fun trace ctxt thm =
+ if Config.get ctxt trace_assms
+ then tracing (Display.string_of_thm ctxt thm)
+ else ()
+
+ fun lookup_assm ctxt assms ct =
+ (case T.net_instance assms ct of
+ SOME thm => (trace ctxt thm; thm)
+ | _ => z3_exn ("not asserted: " ^
+ quote (Syntax.string_of_term ctxt (Thm.term_of ct))))
+in
+fun prepare_assms unfolds assms =
+ let
+ val unfolds' = rewrite_rules [L.rewrite_true] unfolds
+ val assms' = rewrite_rules (unfolds' @ prep_rules) assms
+ in (unfolds', T.thm_net_of assms') end
+
+fun asserted _ NONE ct = Thm (Thm.assume ct)
+ | asserted ctxt (SOME (unfolds, assms)) ct =
+ let val revert_conv = rewrite_conv ctxt unfolds
+ in Thm (T.with_conv revert_conv (lookup_assm ctxt assms) ct) end
+end
+
+
+
+(* P = Q ==> P ==> Q or P --> Q ==> P ==> Q *)
+local
+ val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
+ val meta_iffD1_c = T.precompose2 Thm.dest_binop meta_iffD1
+
+ val iffD1_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
+ val mp_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm mp}
+in
+fun mp (MetaEq thm) p = Thm (Thm.implies_elim (T.compose meta_iffD1_c thm) p)
+ | mp p_q p =
+ let
+ val pq = thm_of p_q
+ val thm = T.compose iffD1_c pq handle THM _ => T.compose mp_c pq
+ in Thm (Thm.implies_elim thm p) end
+end
+
+
+
+(* and_elim: P1 & ... & Pn ==> Pi *)
+(* not_or_elim: ~(P1 | ... | Pn) ==> ~Pi *)
+local
+ fun is_sublit conj t = L.exists_lit conj (fn u => u aconv t)
+
+ fun derive conj t lits idx ptab =
+ let
+ val lit = the (L.get_first_lit (is_sublit conj t) lits)
+ val ls = L.explode conj false false [t] lit
+ val lits' = fold L.insert_lit ls (L.delete_lit lit lits)
+
+ fun upd (Sequent {hyps, thm}) =
+ Sequent {hyps = hyps, thm = Literals (thm_of thm, lits')}
+ | upd p = p
+ in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end
+
+ fun lit_elim conj (p, idx) ct ptab =
+ let val lits = literals_of p
+ in
+ (case L.lookup_lit lits (T.term_of ct) of
+ SOME lit => (Thm lit, ptab)
+ | NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab))
+ end
+in
+val and_elim = lit_elim true
+val not_or_elim = lit_elim false
+end
+
+
+
+(* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *)
+local
+ fun step lit thm =
+ Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
+ val explode_disj = L.explode false false false
+ fun intro hyps thm th = fold step (explode_disj hyps th) thm
+
+ fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
+ val ccontr = T.precompose dest_ccontr @{thm ccontr}
+in
+fun lemma thm ct =
+ let
+ val cu = Thm.capply @{cterm Not} (Thm.dest_arg ct)
+ val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
+ in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end
+end
+
+
+
+(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
+local
+ val explode_disj = L.explode false true false
+ val join_disj = L.join false
+ fun unit thm thms th =
+ let val t = @{term Not} $ T.prop_of thm and ts = map T.prop_of thms
+ in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
+
+ fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
+ fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
+ val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
+in
+fun unit_resolution thm thms ct =
+ Thm.capply @{cterm Not} (Thm.dest_arg ct)
+ |> T.under_assumption (unit thm thms)
+ |> Thm o T.discharge thm o T.compose contrapos
+end
+
+
+
+(* P ==> P == True or P ==> P == False *)
+local
+ val iff1 = @{lemma "P ==> P == (~ False)" by simp}
+ val iff2 = @{lemma "~P ==> P == False" by simp}
+in
+fun iff_true thm = MetaEq (thm COMP iff1)
+fun iff_false thm = MetaEq (thm COMP iff2)
+end
+
+
+
+(* distributivity of | over & *)
+fun distributivity ctxt = Thm o try_apply ctxt [] [
+ named ctxt "fast" (T.by_tac (Classical.best_tac HOL_cs))]
+ (* FIXME: not very well tested *)
+
+
+
+(* Tseitin-like axioms *)
+
+local
+ val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
+ val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
+ val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast}
+ val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
+
+ fun prove' conj1 conj2 ct2 thm =
+ let val lits = L.true_thm :: L.explode conj1 true (conj1 <> conj2) [] thm
+ in L.join conj2 (L.make_littab lits) (Thm.term_of ct2) end
+
+ fun prove rule (ct1, conj1) (ct2, conj2) =
+ T.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
+
+ fun prove_def_axiom ct =
+ let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
+ in
+ (case Thm.term_of ct1 of
+ @{term Not} $ (@{term "op &"} $ _ $ _) =>
+ prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
+ | @{term "op &"} $ _ $ _ =>
+ prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
+ | @{term Not} $ (@{term "op |"} $ _ $ _) =>
+ prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
+ | @{term "op |"} $ _ $ _ =>
+ prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
+ | Const (@{const_name distinct}, _) $ _ =>
+ let
+ fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
+ fun prv cu =
+ let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
+ in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
+ in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
+ | @{term Not} $ (Const (@{const_name distinct}, _) $ _) =>
+ let
+ fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
+ fun prv cu =
+ let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
+ in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
+ in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
+ | _ => raise CTERM ("prove_def_axiom", [ct]))
+ end
+
+ val rewr_if =
+ @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
+in
+fun def_axiom ctxt = Thm o try_apply ctxt [] [
+ named ctxt "conj/disj/distinct" prove_def_axiom,
+ T.by_abstraction ctxt [] (fn ctxt' =>
+ named ctxt' "simp+fast" (T.by_tac (
+ Simplifier.simp_tac (HOL_ss addsimps [rewr_if])
+ THEN_ALL_NEW Classical.best_tac HOL_cs)))]
+end
+
+
+
+(* local definitions *)
+local
+ val intro_rules = [
+ @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp},
+ @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)"
+ by simp},
+ @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ]
+
+ val apply_rules = [
+ @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast},
+ @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
+ by (atomize(full)) fastsimp} ]
+
+ val inst_rule = T.match_instantiate Thm.dest_arg
+
+ fun apply_rule ct =
+ (case get_first (try (inst_rule ct)) intro_rules of
+ SOME thm => thm
+ | NONE => raise CTERM ("intro_def", [ct]))
+in
+fun intro_def ct = apsnd Thm (T.make_hyp_def (apply_rule ct))
+
+fun apply_def thm =
+ get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
+ |> the_default (Thm thm)
+end
+
+
+
+(* negation normal form *)
+
+local
+ val quant_rules1 = ([
+ @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp},
+ @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [
+ @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp},
+ @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}])
+
+ val quant_rules2 = ([
+ @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp},
+ @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [
+ @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
+ @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
+
+ fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
+ Tactic.rtac thm ORELSE'
+ (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
+ (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
+
+ fun nnf_quant vars qs p ct =
+ T.as_meta_eq ct
+ |> T.by_tac (nnf_quant_tac (T.varify vars (meta_eq_of p)) qs)
+
+ fun prove_nnf ctxt = try_apply ctxt [] [
+ named ctxt "conj/disj" L.prove_conj_disj_eq]
+in
+fun nnf ctxt vars ps ct =
+ (case T.term_of ct of
+ _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
+ if l aconv r
+ then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
+ else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
+ | _ $ (@{term Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
+ MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
+ | _ =>
+ let
+ val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
+ (T.unfold_eqs ctxt (map (Thm.symmetric o meta_eq_of) ps)))
+ in Thm (T.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
+end
+
+
+
+(** equality proof rules **)
+
+(* |- t = t *)
+fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
+
+
+
+(* s = t ==> t = s *)
+local
+ val symm_rule = @{lemma "s = t ==> t == s" by simp}
+in
+fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm)
+ | symm p = MetaEq (thm_of p COMP symm_rule)
+end
+
+
+
+(* s = t ==> t = u ==> s = u *)
+local
+ val trans1 = @{lemma "s == t ==> t = u ==> s == u" by simp}
+ val trans2 = @{lemma "s = t ==> t == u ==> s == u" by simp}
+ val trans3 = @{lemma "s = t ==> t = u ==> s == u" by simp}
+in
+fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2)
+ | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1))
+ | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2))
+ | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3))
+end
+
+
+
+(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn
+ (reflexive antecendents are droppped) *)
+local
+ exception MONO
+
+ fun prove_refl (ct, _) = Thm.reflexive ct
+ fun prove_comb f g cp =
+ let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp
+ in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
+ fun prove_arg f = prove_comb prove_refl f
+
+ fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp
+
+ fun prove_nary is_comb f =
+ let
+ fun prove (cp as (ct, _)) = f cp handle MONO =>
+ if is_comb (Thm.term_of ct)
+ then prove_comb (prove_arg prove) prove cp
+ else prove_refl cp
+ in prove end
+
+ fun prove_list f n cp =
+ if n = 0 then prove_refl cp
+ else prove_comb (prove_arg f) (prove_list f (n-1)) cp
+
+ fun with_length f (cp as (cl, _)) =
+ f (length (HOLogic.dest_list (Thm.term_of cl))) cp
+
+ fun prove_distinct f = prove_arg (with_length (prove_list f))
+
+ fun prove_eq exn lookup cp =
+ (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of
+ SOME eq => eq
+ | NONE => if exn then raise MONO else prove_refl cp)
+
+ val prove_eq_exn = prove_eq true
+ and prove_eq_safe = prove_eq false
+
+ fun mono f (cp as (cl, _)) =
+ (case Term.head_of (Thm.term_of cl) of
+ @{term "op &"} => prove_nary L.is_conj (prove_eq_exn f)
+ | @{term "op |"} => prove_nary L.is_disj (prove_eq_exn f)
+ | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
+ | _ => prove (prove_eq_safe f)) cp
+in
+fun monotonicity eqs ct =
+ let
+ val lookup = AList.lookup (op aconv) (map (`Thm.prop_of o meta_eq_of) eqs)
+ val cp = Thm.dest_binop (Thm.dest_arg ct)
+ in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end
+end
+
+
+
+(* |- f a b = f b a (where f is equality) *)
+local
+ val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
+in
+fun commutativity ct = MetaEq (T.match_instantiate I (T.as_meta_eq ct) rule)
+end
+
+
+
+(** quantifier proof rules **)
+
+(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x)
+ P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x) *)
+local
+ val rules = [
+ @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp},
+ @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}]
+in
+fun quant_intro vars p ct =
+ let
+ val thm = meta_eq_of p
+ val rules' = T.varify vars thm :: rules
+ val cu = T.as_meta_eq ct
+ in MetaEq (T.by_tac (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end
+end
+
+
+
+(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
+fun pull_quant ctxt = Thm o try_apply ctxt [] [
+ named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
+ (* FIXME: not very well tested *)
+
+
+
+(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
+fun push_quant ctxt = Thm o try_apply ctxt [] [
+ named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
+ (* FIXME: not very well tested *)
+
+
+
+(* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *)
+local
+ val elim_all = @{lemma "(ALL x. P) == P" by simp}
+ val elim_ex = @{lemma "(EX x. P) == P" by simp}
+
+ fun elim_unused_conv ctxt =
+ Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv
+ (More_Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
+
+ fun elim_unused_tac ctxt =
+ REPEAT_ALL_NEW (
+ Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}]
+ ORELSE' CONVERSION (elim_unused_conv ctxt))
+in
+fun elim_unused_vars ctxt = Thm o T.by_tac (elim_unused_tac ctxt)
+end
+
+
+
+(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
+fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
+ named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
+ (* FIXME: not very well tested *)
+
+
+
+(* |- ~(ALL x1...xn. P x1...xn) | P a1...an *)
+local
+ val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
+in
+val quant_inst = Thm o T.by_tac (
+ REPEAT_ALL_NEW (Tactic.match_tac [rule])
+ THEN' Tactic.rtac @{thm excluded_middle})
+end
+
+
+
+(* c = SOME x. P x |- (EX x. P x) = P c
+ c = SOME x. ~ P x |- ~(ALL x. P x) = ~ P c *)
+local
+ val elim_ex = @{lemma "EX x. P == P" by simp}
+ val elim_all = @{lemma "~ (ALL x. P) == ~P" by simp}
+ val sk_ex = @{lemma "c == SOME x. P x ==> EX x. P x == P c"
+ by simp (intro eq_reflection some_eq_ex[symmetric])}
+ val sk_all = @{lemma "c == SOME x. ~ P x ==> ~(ALL x. P x) == ~ P c"
+ by (simp only: not_all) (intro eq_reflection some_eq_ex[symmetric])}
+ val sk_ex_rule = ((sk_ex, I), elim_ex)
+ and sk_all_rule = ((sk_all, Thm.dest_arg), elim_all)
+
+ fun dest f sk_rule =
+ Thm.dest_comb (f (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of sk_rule))))
+ fun type_of f sk_rule = Thm.ctyp_of_term (snd (dest f sk_rule))
+ fun pair2 (a, b) (c, d) = [(a, c), (b, d)]
+ fun inst_sk (sk_rule, f) p c =
+ Thm.instantiate ([(type_of f sk_rule, Thm.ctyp_of_term c)], []) sk_rule
+ |> (fn sk' => Thm.instantiate ([], (pair2 (dest f sk') (p, c))) sk')
+ |> Conv.fconv_rule (Thm.beta_conversion true)
+
+ fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
+ | kind (@{term Not} $ (Const (@{const_name All}, _) $ _)) =
+ (sk_all_rule, Thm.dest_arg, Thm.capply @{cterm Not})
+ | kind _ = z3_exn "skolemize: no quantifier"
+
+ fun dest_abs_type (Abs (_, T, _)) = T
+ | dest_abs_type t = raise TERM ("dest_abs_type", [t])
+
+ fun bodies_of thy lhs rhs =
+ let
+ val (rule, dest, make) = kind (Thm.term_of lhs)
+
+ fun dest_body idx cbs ct =
+ let
+ val cb = Thm.dest_arg (dest ct)
+ val T = dest_abs_type (Thm.term_of cb)
+ val cv = Thm.cterm_of thy (Var (("x", idx), T))
+ val cu = make (Drule.beta_conv cb cv)
+ val cbs' = (cv, cb) :: cbs
+ in
+ (snd (Thm.first_order_match (cu, rhs)), rev cbs')
+ handle Pattern.MATCH => dest_body (idx+1) cbs' cu
+ end
+ in (rule, dest_body 1 [] lhs) end
+
+ fun transitive f thm = Thm.transitive thm (f (Thm.rhs_of thm))
+
+ fun sk_step (rule, elim) (cv, mct, cb) (is, thm) =
+ (case mct of
+ SOME ct =>
+ T.make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
+ |> apsnd (pair ((cv, ct) :: is) o Thm.transitive thm)
+ | NONE => ([], (is, transitive (Conv.rewr_conv elim) thm)))
+in
+fun skolemize ctxt ct =
+ let
+ val (lhs, rhs) = Thm.dest_binop (Thm.dest_arg ct)
+ val (rule, (ctab, cbs)) = bodies_of (ProofContext.theory_of ctxt) lhs rhs
+ fun lookup_var (cv, cb) = (cv, AList.lookup (op aconvc) ctab cv, cb)
+ in
+ ([], Thm.reflexive lhs)
+ |> fold_map (sk_step rule) (map lookup_var cbs)
+ |> apfst (rev o flat) o apsnd (MetaEq o snd)
+ end
+end
+
+
+
+(** theory proof rules **)
+
+(* theory lemmas: linear arithmetic, arrays *)
+
+fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
+ T.by_abstraction ctxt thms (fn ctxt' => T.by_tac (
+ NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
+ ORELSE' NAMED ctxt' "simp+arith" (Simplifier.simp_tac simpset THEN_ALL_NEW
+ Arith_Data.arith_tac ctxt')))]
+
+
+
+(* rewriting: prove equalities:
+ * ACI of conjunction/disjunction
+ * contradiction, excluded middle
+ * logical rewriting rules (for negation, implication, equivalence,
+ distinct)
+ * normal forms for polynoms (integer/real arithmetic)
+ * quantifier elimination over linear arithmetic
+ * ... ? **)
+structure Z3_Simps = Named_Thms
+(
+ val name = "z3_simp"
+ val description = "simplification rules for Z3 proof reconstruction"
+)
+
+local
+ fun spec_meta_eq_of thm =
+ (case try (fn th => th RS @{thm spec}) thm of
+ SOME thm' => spec_meta_eq_of thm'
+ | NONE => mk_meta_eq thm)
+
+ fun prep (Thm thm) = spec_meta_eq_of thm
+ | prep (MetaEq thm) = thm
+ | prep (Literals (thm, _)) = spec_meta_eq_of thm
+
+ fun unfold_conv ctxt ths =
+ Conv.arg_conv (Conv.binop_conv (T.unfold_eqs ctxt (map prep ths)))
+
+ fun with_conv _ [] prv = prv
+ | with_conv ctxt ths prv = T.with_conv (unfold_conv ctxt ths) prv
+
+ val unfold_conv =
+ Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv))
+ val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq
+in
+
+fun rewrite ctxt simpset ths = Thm o with_conv ctxt ths (try_apply ctxt [] [
+ named ctxt "conj/disj/distinct" prove_conj_disj_eq,
+ T.by_abstraction ctxt [] (fn ctxt' => T.by_tac (
+ NAMED ctxt' "simp" (Simplifier.simp_tac simpset)
+ THEN_ALL_NEW (
+ NAMED ctxt' "fast" (Classical.fast_tac HOL_cs)
+ ORELSE' NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt'))))])
+
+end
+
+
+
+(** proof reconstruction **)
+
+(* tracing and checking *)
+
+local
+ fun count_rules ptab =
+ let
+ fun count (_, Unproved _) (solved, total) = (solved, total + 1)
+ | count (_, Sequent _) (solved, total) = (solved + 1, total + 1)
+ in Inttab.fold count ptab (0, 0) end
+
+ fun header idx r (solved, total) =
+ "Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r ^ " (goal " ^
+ string_of_int (solved + 1) ^ " of " ^ string_of_int total ^ ")"
+
+ fun check ctxt idx r ps ct ((_, p), _) =
+ let val thm = thm_of p |> tap (Thm.join_proofs o single)
+ in
+ if (Thm.cprop_of thm) aconvc ct then ()
+ else z3_exn (Pretty.string_of (Pretty.big_list ("proof step failed: " ^
+ quote (P.string_of_rule r) ^ " (#" ^ string_of_int idx ^ ")")
+ (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
+ [Pretty.block [Pretty.str "expected: ",
+ Syntax.pretty_term ctxt (Thm.term_of ct)]])))
+ end
+in
+fun trace_rule ctxt idx prove r ps ct ptab =
+ let
+ val _ = SMT_Solver.trace_msg ctxt (header idx r o count_rules) ptab
+ val result = prove r ps ct ptab
+ val _ = if not (Config.get ctxt SMT_Solver.trace) then ()
+ else check ctxt idx r ps ct result
+ in result end
+end
+
+
+(* overall reconstruction procedure *)
+
+fun not_supported r =
+ z3_exn ("proof rule not implemented: " ^ quote (P.string_of_rule r))
+
+fun prove ctxt unfolds assms vars =
+ let
+ val assms' = Option.map (prepare_assms unfolds) assms
+ val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt)
+
+ fun step r ps ct ptab =
+ (case (r, ps) of
+ (* core rules *)
+ (P.TrueAxiom, _) => (([], Thm L.true_thm), ptab)
+ | (P.Asserted, _) => (([], asserted ctxt assms' ct), ptab)
+ | (P.Goal, _) => (([], asserted ctxt assms' ct), ptab)
+ | (P.ModusPonens, [(p, _), (q, _)]) => (([], mp q (thm_of p)), ptab)
+ | (P.ModusPonensOeq, [(p, _), (q, _)]) => (([], mp q (thm_of p)), ptab)
+ | (P.AndElim, [(p, i)]) => apfst (pair []) (and_elim (p, i) ct ptab)
+ | (P.NotOrElim, [(p, i)]) => apfst (pair []) (not_or_elim (p, i) ct ptab)
+ | (P.Hypothesis, _) => (([], Thm (Thm.assume ct)), ptab)
+ | (P.Lemma, [(p, _)]) => (([], lemma (thm_of p) ct), ptab)
+ | (P.UnitResolution, (p, _) :: ps) =>
+ (([], unit_resolution (thm_of p) (map (thm_of o fst) ps) ct), ptab)
+ | (P.IffTrue, [(p, _)]) => (([], iff_true (thm_of p)), ptab)
+ | (P.IffFalse, [(p, _)]) => (([], iff_false (thm_of p)), ptab)
+ | (P.Distributivity, _) => (([], distributivity ctxt ct), ptab)
+ | (P.DefAxiom, _) => (([], def_axiom ctxt ct), ptab)
+ | (P.IntroDef, _) => (intro_def ct, ptab)
+ | (P.ApplyDef, [(p, _)]) => (([], apply_def (thm_of p)), ptab)
+ | (P.IffOeq, [(p, _)]) => (([], p), ptab)
+ | (P.NnfPos, _) => (([], nnf ctxt vars (map fst ps) ct), ptab)
+ | (P.NnfNeg, _) => (([], nnf ctxt vars (map fst ps) ct), ptab)
+
+ (* equality rules *)
+ | (P.Reflexivity, _) => (([], refl ct), ptab)
+ | (P.Symmetry, [(p, _)]) => (([], symm p), ptab)
+ | (P.Transitivity, [(p, _), (q, _)]) => (([], trans p q), ptab)
+ | (P.Monotonicity, _) => (([], monotonicity (map fst ps) ct), ptab)
+ | (P.Commutativity, _) => (([], commutativity ct), ptab)
+
+ (* quantifier rules *)
+ | (P.QuantIntro, [(p, _)]) => (([], quant_intro vars p ct), ptab)
+ | (P.PullQuant, _) => (([], pull_quant ctxt ct), ptab)
+ | (P.PushQuant, _) => (([], push_quant ctxt ct), ptab)
+ | (P.ElimUnusedVars, _) => (([], elim_unused_vars ctxt ct), ptab)
+ | (P.DestEqRes, _) => (([], dest_eq_res ctxt ct), ptab)
+ | (P.QuantInst, _) => (([], quant_inst ct), ptab)
+ | (P.Skolemize, _) => (skolemize ctxt ct, ptab)
+
+ (* theory rules *)
+ | (P.ThLemma, _) =>
+ (([], th_lemma ctxt simpset (map (thm_of o fst) ps) ct), ptab)
+ | (P.Rewrite, _) => (([], rewrite ctxt simpset [] ct), ptab)
+ | (P.RewriteStar, ps) =>
+ (([], rewrite ctxt simpset (map fst ps) ct), ptab)
+
+ | (P.NnfStar, _) => not_supported r
+ | (P.CnfStar, _) => not_supported r
+ | (P.TransitivityStar, _) => not_supported r
+ | (P.PullQuantStar, _) => not_supported r
+
+ | _ => z3_exn ("Proof rule " ^ quote (P.string_of_rule r) ^
+ " has an unexpected number of arguments."))
+
+ fun eq_hyp_def (ct, cu) = Thm.dest_arg1 ct aconvc Thm.dest_arg1 cu
+ (* compare only the defined Frees, not the whole definitions *)
+
+ fun conclude idx rule prop ((hypss, ps), ptab) =
+ trace_rule ctxt idx step rule ps prop ptab
+ |>> apfst (distinct eq_hyp_def o fold append hypss)
+
+ fun add_sequent idx (hyps, thm) ptab =
+ ((hyps, thm), Inttab.update (idx, Sequent {hyps=hyps, thm=thm}) ptab)
+
+ fun lookup idx ptab =
+ (case Inttab.lookup ptab idx of
+ SOME (Unproved (P.Proof_Step {rule, prems, prop})) =>
+ fold_map lookup prems ptab
+ |>> split_list
+ |>> apsnd (fn ps => ps ~~ prems)
+ |> conclude idx rule prop
+ |-> add_sequent idx
+ | SOME (Sequent {hyps, thm}) => ((hyps, thm), ptab)
+ | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
+
+ fun result (hyps, thm) =
+ fold SMT_Normalize.discharge_definition hyps (thm_of thm)
+ in
+ (fn (idx, ptab) => result (fst (lookup idx (Inttab.map Unproved ptab))))
+ end
+
+fun reconstruct ctxt {typs, terms, unfolds, assms} output =
+ P.parse ctxt typs terms output
+ |> (fn (idx, (ptab, vars, cx)) => prove cx unfolds assms vars (idx, ptab))
+
+val setup = trace_assms_setup #> z3_rules_setup #> Z3_Simps.setup
+
+end
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML Wed May 12 23:53:58 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1415 +0,0 @@
-(* Title: HOL/SMT/Tools/z3_proof_rules.ML
- Author: Sascha Boehme, TU Muenchen
-
-Z3 proof rules and their reconstruction.
-*)
-
-signature Z3_PROOF_RULES =
-sig
- (*proof rule names*)
- type rule
- val rule_of_string: string -> rule option
- val string_of_rule: rule -> string
-
- (*proof reconstruction*)
- type proof
- val make_proof: rule -> int list -> cterm * cterm list -> proof
- val prove: Proof.context -> thm list -> thm list option ->
- proof Inttab.table -> int -> thm
-
- (*setup*)
- val trace_assms: bool Config.T
- val setup: theory -> theory
-end
-
-structure Z3_Proof_Rules: Z3_PROOF_RULES =
-struct
-
-structure T = Z3_Proof_Terms
-
-fun z3_exn msg = raise SMT_Solver.SMT ("Z3 proof reconstruction: " ^ msg)
-
-
-(* proof rule names *)
-
-datatype rule = TrueAxiom | Asserted | Goal | ModusPonens | Reflexivity |
- Symmetry | Transitivity | TransitivityStar | Monotonicity | QuantIntro |
- Distributivity | AndElim | NotOrElim | Rewrite | RewriteStar | PullQuant |
- PullQuantStar | PushQuant | ElimUnusedVars | DestEqRes | QuantInst |
- Hypothesis | Lemma | UnitResolution | IffTrue | IffFalse | Commutativity |
- DefAxiom | IntroDef | ApplyDef | IffOeq | NnfPos | NnfNeg | NnfStar |
- CnfStar | Skolemize | ModusPonensOeq | ThLemma
-
-val rule_names = Symtab.make [
- ("true-axiom", TrueAxiom),
- ("asserted", Asserted),
- ("goal", Goal),
- ("mp", ModusPonens),
- ("refl", Reflexivity),
- ("symm", Symmetry),
- ("trans", Transitivity),
- ("trans*", TransitivityStar),
- ("monotonicity", Monotonicity),
- ("quant-intro", QuantIntro),
- ("distributivity", Distributivity),
- ("and-elim", AndElim),
- ("not-or-elim", NotOrElim),
- ("rewrite", Rewrite),
- ("rewrite*", RewriteStar),
- ("pull-quant", PullQuant),
- ("pull-quant*", PullQuantStar),
- ("push-quant", PushQuant),
- ("elim-unused", ElimUnusedVars),
- ("der", DestEqRes),
- ("quant-inst", QuantInst),
- ("hypothesis", Hypothesis),
- ("lemma", Lemma),
- ("unit-resolution", UnitResolution),
- ("iff-true", IffTrue),
- ("iff-false", IffFalse),
- ("commutativity", Commutativity),
- ("def-axiom", DefAxiom),
- ("intro-def", IntroDef),
- ("apply-def", ApplyDef),
- ("iff~", IffOeq),
- ("nnf-pos", NnfPos),
- ("nnf-neg", NnfNeg),
- ("nnf*", NnfStar),
- ("cnf*", CnfStar),
- ("sk", Skolemize),
- ("mp~", ModusPonensOeq),
- ("th-lemma", ThLemma)]
-
-val rule_of_string = Symtab.lookup rule_names
-fun string_of_rule r =
- let fun fit (s, r') = if r = r' then SOME s else NONE
- in the (Symtab.get_first fit rule_names) end
-
-
-(* proof representation *)
-
-datatype theorem =
- Thm of thm |
- MetaEq of thm |
- Literals of thm * thm Termtab.table
-
-fun thm_of (Thm thm) = thm
- | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq}
- | thm_of (Literals (thm, _)) = thm
-
-fun meta_eq_of (MetaEq thm) = thm
- | meta_eq_of p = mk_meta_eq (thm_of p)
-
-datatype proof =
- Unproved of {
- rule: rule,
- subs: int list,
- prop: cterm,
- vars: cterm list } |
- Sequent of {
- hyps: cterm list,
- vars: cterm list,
- thm: theorem }
-
-fun make_proof r ps (ct, cvs) = Unproved {rule=r, subs=ps, prop=ct, vars=cvs}
-
-
-(* proof reconstruction utilities *)
-
-fun try_apply ctxt name nfs ct =
- let
- val trace = SMT_Solver.trace_msg ctxt I
-
- fun first [] = z3_exn (name ^ " failed")
- | first ((n, f) :: nfs) =
- (case try f ct of
- SOME thm => (trace (n ^ " succeeded"); thm)
- | NONE => (trace (n ^ " failed"); first nfs))
- in first nfs end
-
-fun prop_of thm = (case Thm.prop_of thm of @{term Trueprop} $ t => t | t => t)
-
-fun as_meta_eq ct = uncurry T.mk_meta_eq (Thm.dest_binop ct)
-
-fun by_tac' tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
-fun by_tac tac ct = by_tac' tac (T.mk_prop ct)
-
-fun match_instantiate' f ct thm =
- Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
-val match_instantiate = match_instantiate' I
-
-local
- fun maybe_instantiate ct thm =
- try Thm.first_order_match (Thm.cprop_of thm, ct)
- |> Option.map (fn inst => Thm.instantiate inst thm)
-in
-fun thm_net_of thms =
- let fun insert thm = Net.insert_term (K false) (Thm.prop_of thm, thm)
- in fold insert thms Net.empty end
-
-fun first_of thms ct = get_first (maybe_instantiate ct) thms
-fun net_instance net ct = first_of (Net.match_term net (Thm.term_of ct)) ct
-end
-
-fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
-fun certify_var ctxt idx T = certify ctxt (Var (("x", idx), T))
-fun certify_free ctxt idx T = certify ctxt (Free ("x" ^ string_of_int idx, T))
-
-fun varify ctxt =
- let
- fun varify1 cv thm =
- let
- val T = Thm.typ_of (Thm.ctyp_of_term cv)
- val v = certify_var ctxt (Thm.maxidx_of thm + 1) T
- in SMT_Normalize.instantiate_free (cv, v) thm end
- in fold varify1 end
-
-fun under_assumption f ct =
- let val ct' = T.mk_prop ct
- in Thm.implies_intr ct' (f (Thm.assume ct')) end
-
-fun with_conv conv prove ct =
- let val eq = Thm.symmetric (conv ct)
- in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
-
-fun list2 (x, y) = [x, y]
-
-fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
-
-fun discharge p pq = Thm.implies_elim pq p
-
-fun compose (cvs, f, rule) thm =
- let fun inst thm = Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm))
- in discharge thm (inst thm rule) end
-
-fun make_hyp_def thm = (* |- c x == t x ==> P (c x) ~~> c == t |- P (c x) *)
- let
- val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
- val (cf, cvs) = Drule.strip_comb lhs
- val eq = T.mk_meta_eq cf (fold_rev Thm.cabs cvs rhs)
- fun apply cv th =
- Thm.combination th (Thm.reflexive cv)
- |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
- in ([eq], Thm.implies_elim thm (fold apply cvs (Thm.assume eq))) end
-
-val true_thm = @{lemma "~False" by simp}
-
-val is_neg = (fn @{term Not} $ _ => true | _ => false)
-fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
-val is_conj = (fn @{term "op &"} $ _ $ _ => true | _ => false)
-val is_disj = (fn @{term "op |"} $ _ $ _ => true | _ => false)
-
-(** explosion of conjunctions and disjunctions **)
-
-local
- val dest_conj_term = (fn @{term "op &"} $ t $ u => SOME (t, u) | _ => NONE)
-
- val negate_term = (fn @{term Not} $ t => t | t => @{term Not} $ t)
- fun dest_disj_term' f = (fn
- @{term Not} $ (@{term "op |"} $ t $ u) => SOME (f t, f u)
- | _ => NONE)
- val dest_disj_term = dest_disj_term' negate_term
-
- fun destc ct = list2 (Thm.dest_binop (Thm.dest_arg ct))
- val dest_conj1 = precompose destc @{thm conjunct1}
- val dest_conj2 = precompose destc @{thm conjunct2}
- fun dest_conj_rules t =
- dest_conj_term t |> Option.map (K (dest_conj1, dest_conj2))
-
- fun destd f ct = list2 (f (Thm.dest_binop (Thm.dest_arg (Thm.dest_arg ct))))
- val dn1 = apfst Thm.dest_arg and dn2 = apsnd Thm.dest_arg
- val dest_disj1 = precompose (destd I) @{lemma "~(P | Q) ==> ~P" by fast}
- and dest_disj2 = precompose (destd dn1) @{lemma "~(~P | Q) ==> P" by fast}
- and dest_disj3 = precompose (destd I) @{lemma "~(P | Q) ==> ~Q" by fast}
- and dest_disj4 = precompose (destd dn2) @{lemma "~(P | ~Q) ==> Q" by fast}
-
- fun dest_disj_rules t =
- (case dest_disj_term' is_neg t of
- SOME (true, true) => SOME (dest_disj2, dest_disj4)
- | SOME (true, false) => SOME (dest_disj2, dest_disj3)
- | SOME (false, true) => SOME (dest_disj1, dest_disj4)
- | SOME (false, false) => SOME (dest_disj1, dest_disj3)
- | NONE => NONE)
-
- val is_dneg = is_neg' is_neg
- fun destn ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg ct))]
- val dneg_rule = precompose destn @{thm notnotD}
-in
-fun exists_lit is_conj P =
- let
- val dest = if is_conj then dest_conj_term else dest_disj_term
- fun exists t = P t orelse
- (case dest t of
- SOME (t1, t2) => exists t1 orelse exists t2
- | NONE => false)
- in exists end
-
-fun explode_term is_conj keep_intermediate =
- let
- val dest = if is_conj then dest_conj_term else dest_disj_term
- val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
- fun explode1 rules t =
- (case dest t of
- SOME (t1, t2) =>
- let val (rule1, rule2) = the (dest_rules t)
- in
- explode1 (rule1 :: rules) t1 #>
- explode1 (rule2 :: rules) t2 #>
- keep_intermediate ? cons (t, rev rules)
- end
- | NONE => cons (t, rev rules))
- fun explode0 (@{term Not} $ (@{term Not} $ t)) = [(t, [dneg_rule])]
- | explode0 t = explode1 [] t []
- in explode0 end
-
-fun extract_lit thm rules = fold compose rules thm
-
-fun explode_thm is_conj full keep_intermediate stop_lits =
- let
- val dest_rules = if is_conj then dest_conj_rules else dest_disj_rules
- val tab = fold (Termtab.update o rpair ()) stop_lits Termtab.empty
-
- fun explode1 thm =
- if Termtab.defined tab (prop_of thm) then cons thm
- else
- (case dest_rules (prop_of thm) of
- SOME (rule1, rule2) => explode2 rule1 thm #> explode2 rule2 thm #>
- keep_intermediate ? cons thm
- | NONE => cons thm)
- and explode2 dest_rule thm =
- if full orelse exists_lit is_conj (Termtab.defined tab) (prop_of thm)
- then explode1 (compose dest_rule thm)
- else cons (compose dest_rule thm)
- fun explode0 thm =
- if not is_conj andalso is_dneg (prop_of thm) then [compose dneg_rule thm]
- else explode1 thm []
- in explode0 end
-end
-
-(** joining of literals to conjunctions or disjunctions **)
-
-local
- fun precomp2 f g thm =
- (f (Thm.cprem_of thm 1), g (Thm.cprem_of thm 2), f, g, thm)
- fun comp2 (cv1, cv2, f, g, rule) thm1 thm2 =
- let val inst = [(cv1, f (Thm.cprop_of thm1)), (cv2, g (Thm.cprop_of thm2))]
- in Thm.instantiate ([], inst) rule |> discharge thm1 |> discharge thm2 end
-
- fun d1 ct = Thm.dest_arg ct and d2 ct = Thm.dest_arg (Thm.dest_arg ct)
-
- val conj_rule = precomp2 d1 d1 @{thm conjI}
- fun comp_conj ((_, thm1), (_, thm2)) = comp2 conj_rule thm1 thm2
-
- val disj1 = precomp2 d2 d2 @{lemma "~P ==> ~Q ==> ~(P | Q)" by fast}
- val disj2 = precomp2 d2 d1 @{lemma "~P ==> Q ==> ~(P | ~Q)" by fast}
- val disj3 = precomp2 d1 d2 @{lemma "P ==> ~Q ==> ~(~P | Q)" by fast}
- val disj4 = precomp2 d1 d1 @{lemma "P ==> Q ==> ~(~P | ~Q)" by fast}
-
- fun comp_disj ((false, thm1), (false, thm2)) = comp2 disj1 thm1 thm2
- | comp_disj ((false, thm1), (true, thm2)) = comp2 disj2 thm1 thm2
- | comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
- | comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
-
- fun dest_conj (@{term "op &"} $ t $ u) = ((false, t), (false, u))
- | dest_conj t = raise TERM ("dest_conj", [t])
-
- val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
- fun dest_disj (@{term Not} $ (@{term "op |"} $ t $ u)) = (neg t, neg u)
- | dest_disj t = raise TERM ("dest_disj", [t])
-
- val dnegE = precompose (single o d2 o d1) @{thm notnotD}
- val dnegI = precompose (single o d1) @{lemma "P ==> ~~P" by fast}
- fun as_dneg f t = f (@{term Not} $ (@{term Not} $ t))
-
- fun dni f = list2 o apsnd f o Thm.dest_binop o f o d1
- val negIffE = precompose (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
- val negIffI = precompose (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
- val iff_const = @{term "op = :: bool => _"}
- fun as_negIff f (@{term "op = :: bool => _"} $ t $ u) =
- f (@{term Not} $ (iff_const $ u $ (@{term Not} $ t)))
- | as_negIff _ _ = NONE
-in
-fun make_lit_tab thms = fold (Termtab.update o ` prop_of) thms Termtab.empty
-
-fun join is_conj tab t =
- let
- val comp = if is_conj then comp_conj else comp_disj
- val dest = if is_conj then dest_conj else dest_disj
-
- val lookup_lit = Termtab.lookup tab
- fun lookup_lit' t =
- (case t of
- @{term Not} $ (@{term Not} $ t) => (compose dnegI, lookup_lit t)
- | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
- (compose negIffI, lookup_lit (iff_const $ u $ t))
- | @{term Not} $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u) =>
- let fun rewr lit = lit COMP @{thm not_sym}
- in (rewr, lookup_lit (@{term Not} $ (eq $ u $ t))) end
- | _ =>
- (case as_dneg lookup_lit t of
- NONE => (compose negIffE, as_negIff lookup_lit t)
- | x => (compose dnegE, x)))
- fun join1 (s, t) =
- (case lookup_lit t of
- SOME lit => (s, lit)
- | NONE =>
- (case lookup_lit' t of
- (rewrite, SOME lit) => (s, rewrite lit)
- | (_, NONE) => (s, comp (pairself join1 (dest t)))))
- in snd (join1 (if is_conj then (false, t) else (true, t))) end
-end
-
-(** proving equality of conjunctions or disjunctions **)
-
-fun iff_intro thm1 thm2 = thm2 COMP (thm1 COMP @{thm iffI})
-
-local
- val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
- val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastsimp}
- val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
- val neg = Thm.capply @{cterm Not}
-in
-fun contrapos1 prove (ct, cu) = prove (neg ct, neg cu) COMP cp1
-fun contrapos2 prove (ct, cu) = prove (neg ct, Thm.dest_arg cu) COMP cp2
-fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, neg cu) COMP cp3
-end
-
-local
- fun prove_eq l r (cl, cr) =
- let
- fun explode is_conj = explode_thm is_conj true (l <> r) []
- fun make_tab is_conj thm = make_lit_tab (true_thm :: explode is_conj thm)
- fun prove is_conj ct tab = join is_conj tab (Thm.term_of ct)
-
- val thm1 = under_assumption (prove r cr o make_tab l) cl
- val thm2 = under_assumption (prove l cl o make_tab r) cr
- in iff_intro thm1 thm2 end
-
- datatype conj_disj = CONJ | DISJ | NCON | NDIS
- fun kind_of t =
- if is_conj t then SOME CONJ
- else if is_disj t then SOME DISJ
- else if is_neg' is_conj t then SOME NCON
- else if is_neg' is_disj t then SOME NDIS
- else NONE
-in
-fun prove_conj_disj_eq ct =
- let val cp = Thm.dest_binop ct
- in
- (case pairself (kind_of o Thm.term_of) cp of
- (SOME CONJ, SOME CONJ) => prove_eq true true cp
- | (SOME CONJ, SOME NDIS) => prove_eq true false cp
- | (SOME CONJ, NONE) => prove_eq true true cp
- | (SOME DISJ, SOME DISJ) => contrapos1 (prove_eq false false) cp
- | (SOME DISJ, SOME NCON) => contrapos2 (prove_eq false true) cp
- | (SOME DISJ, NONE) => contrapos1 (prove_eq false false) cp
- | (SOME NCON, SOME NCON) => contrapos1 (prove_eq true true) cp
- | (SOME NCON, SOME DISJ) => contrapos3 (prove_eq true false) cp
- | (SOME NCON, NONE) => contrapos3 (prove_eq true false) cp
- | (SOME NDIS, SOME NDIS) => prove_eq false false cp
- | (SOME NDIS, SOME CONJ) => prove_eq false true cp
- | (SOME NDIS, NONE) => prove_eq false true cp
- | _ => raise CTERM ("prove_conj_disj_eq", [ct]))
- end
-end
-
-(** unfolding of distinct **)
-
-local
- val set1 = @{lemma "x ~: set [] == ~False" by simp}
- val set2 = @{lemma "x ~: set [x] == False" by simp}
- val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
- val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
- val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
-
- fun set_conv ct =
- (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
- (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
-
- val dist1 = @{lemma "distinct [] == ~False" by simp}
- val dist2 = @{lemma "distinct [x] == ~False" by simp}
- val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
- by simp}
-
- fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
-in
-fun unfold_distinct_conv ct =
- (More_Conv.rewrs_conv [dist1, dist2] else_conv
- (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
-end
-
-(** proving abstractions **)
-
-fun fold_map_op f ct =
- let val (cf, cu) = Thm.dest_comb ct
- in f cu #>> Thm.capply cf end
-
-fun fold_map_binop f1 f2 ct =
- let val ((cf, cu1), cu2) = apfst Thm.dest_comb (Thm.dest_comb ct)
- in f1 cu1 ##>> f2 cu2 #>> uncurry (Thm.mk_binop cf) end
-
-fun abstraction_context ctxt = (ctxt, certify_var, 1, false, Ctermtab.empty)
-fun abstraction_context' ctxt = (ctxt, certify_free, 1, true, Ctermtab.empty)
-
-fun fresh_abstraction ct (cx as (ctxt, mk_var, idx, gen, tab)) =
- (case Ctermtab.lookup tab ct of
- SOME cv => (cv, cx)
- | NONE =>
- let val cv = mk_var ctxt idx (#T (Thm.rep_cterm ct))
- in (cv, (ctxt, mk_var, idx + 1, gen, Ctermtab.update (ct, cv) tab)) end)
-
-fun prove_abstraction tac ct (_, _, _, gen, tab) =
- let
- val insts = map swap (Ctermtab.dest tab)
- val thm = Goal.prove_internal [] ct (fn _ => tac 1)
- in
- if gen
- then fold SMT_Normalize.instantiate_free insts thm
- else Thm.instantiate ([], insts) thm
- end
-
-
-(* core proof rules *)
-
-datatype assms = Some of thm list | Many of thm Net.net
-
-val true_false = @{lemma "True == ~ False" by simp}
-
-val (trace_assms, trace_assms_setup) =
- Attrib.config_bool "z3_trace_assms" (K false)
-
-local
- val remove_trigger = @{lemma "trigger t p == p"
- by (rule eq_reflection, rule trigger_def)}
-
- fun with_context simpset ctxt = Simplifier.context ctxt simpset
-
- val prep_ss = with_context (Simplifier.empty_ss addsimps
- [@{thm Let_def}, remove_trigger, true_false])
-
- fun norm_conv ctxt unfolds = More_Conv.top_conv
- (K (Conv.try_conv (More_Conv.rewrs_conv unfolds))) ctxt
-
- val threshold = 10
-
- fun trace ctxt thm =
- if Config.get ctxt trace_assms
- then tracing (Display.string_of_thm ctxt thm)
- else ()
-
- val lookup = (fn Some thms => first_of thms | Many net => net_instance net)
- fun lookup_assm ctxt assms ct =
- (case lookup assms ct of
- SOME thm => (trace ctxt thm; thm)
- | _ => z3_exn ("not asserted: " ^
- quote (Syntax.string_of_term ctxt (Thm.term_of ct))))
-in
-fun prepare_assms ctxt assms =
- let
- val rewrite = Conv.fconv_rule (Simplifier.rewrite (prep_ss ctxt))
- val thms = map rewrite assms
- in if length assms < threshold then Some thms else Many (thm_net_of thms) end
-
-fun asserted _ _ NONE ct = Thm (Thm.assume (T.mk_prop ct))
- | asserted ctxt unfolds (SOME assms) ct =
- Thm (with_conv (norm_conv ctxt unfolds) (lookup_assm ctxt assms)
- (T.mk_prop ct))
-end
-
-
-(** P ==> P = Q ==> Q or P ==> P --> Q ==> Q **)
-local
- val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
- val meta_iffD1_c = precompose (list2 o Thm.dest_binop) meta_iffD1
-
- val iffD1_c = precompose (list2 o Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
- val mp_c = precompose (list2 o Thm.dest_binop o Thm.dest_arg) @{thm mp}
-in
-fun mp (MetaEq thm) p = Thm (Thm.implies_elim (compose meta_iffD1_c thm) p)
- | mp p_q p =
- let
- val pq = thm_of p_q
- val thm = compose iffD1_c pq handle THM _ => compose mp_c pq
- in Thm (Thm.implies_elim thm p) end
-end
-
-
-(** and_elim: P1 & ... & Pn ==> Pi **)
-(** not_or_elim: ~(P1 | ... | Pn) ==> ~Pi **)
-local
- fun get_lit conj t (l, thm) =
- let val is_sublit_of = exists_lit conj (fn u => u aconv t)
- in if is_sublit_of (prop_of thm) then SOME (l, thm) else NONE end
-
- fun derive conj t lits idx ptab =
- let
- val (l, lit) = the (Termtab.get_first (get_lit conj t) lits)
- val ls = explode_thm conj false false [t] lit
- val lits' = fold (Termtab.update o ` prop_of) ls (Termtab.delete l lits)
- fun upd (Sequent {hyps, vars, thm}) =
- Sequent {hyps=hyps, vars=vars, thm = Literals (thm_of thm, lits')}
- | upd p = p
- in (the (Termtab.lookup lits' t), Inttab.map_entry idx upd ptab) end
-
- val mk_tab = make_lit_tab o single
- val literals_of = (fn Literals (_, lits) => lits | p => mk_tab (thm_of p))
- fun lit_elim conj (p, idx) ct ptab =
- let val lits = literals_of p
- in
- (case Termtab.lookup lits (Thm.term_of ct) of
- SOME lit => (Thm lit, ptab)
- | NONE => apfst Thm (derive conj (Thm.term_of ct) lits idx ptab))
- end
-in
-val and_elim = lit_elim true
-val not_or_elim = lit_elim false
-end
-
-
-(** P1 ... Pn |- False ==> |- ~P1 | ... | ~Pn **)
-local
- fun step lit thm =
- Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
- val explode_disj = explode_thm false false false
- fun intro hyps thm th = fold step (explode_disj hyps th) thm
-
- fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
- val ccontr = precompose dest_ccontr @{thm ccontr}
-in
-fun lemma thm ct =
- let
- val cu = Thm.capply @{cterm Not} ct
- val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
- in Thm (compose ccontr (under_assumption (intro hyps thm) cu)) end
-end
-
-
-(** \/{P1, ..., Pn, Q1, ..., Qn} & ~P1 & ... & ~Pn ==> \/{Q1, ..., Qn} **)
-local
- val explode_disj = explode_thm false true false and join_disj = join false
- fun unit thm thms th =
- let val t = @{term Not} $ prop_of thm and ts = map prop_of thms
- in join_disj (make_lit_tab (thms @ explode_disj ts th)) t end
-
- fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
- fun dest ct = list2 (pairself dest_arg2 (Thm.dest_binop ct))
- val contrapos = precompose dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
-in
-fun unit_resolution thm thms ct =
- under_assumption (unit thm thms) (Thm.capply @{cterm Not} ct)
- |> Thm o discharge thm o compose contrapos
-end
-
-
-local
- val iff1 = @{lemma "P ==> P == (~ False)" by simp}
- val iff2 = @{lemma "~P ==> P == False" by simp}
-in
-fun iff_true thm = MetaEq (thm COMP iff1)
-fun iff_false thm = MetaEq (thm COMP iff2)
-end
-
-
-(** distributivity of | over & **)
-val distributivity = Thm o by_tac (Classical.fast_tac HOL_cs)
-
-
-(** Tseitin-like axioms **)
-local
- val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
- val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
- val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast}
- val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
-
- fun prove' conj1 conj2 ct2 thm =
- let val tab =
- make_lit_tab (true_thm :: explode_thm conj1 true (conj1 <> conj2) [] thm)
- in join conj2 tab (Thm.term_of ct2) end
-
- fun prove rule (ct1, conj1) (ct2, conj2) =
- under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
-
- fun prove_def_axiom ct =
- let val (ct1, ct2) = Thm.dest_binop ct
- in
- (case Thm.term_of ct1 of
- @{term Not} $ (@{term "op &"} $ _ $ _) =>
- prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
- | @{term "op &"} $ _ $ _ =>
- prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
- | @{term Not} $ (@{term "op |"} $ _ $ _) =>
- prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
- | @{term "op |"} $ _ $ _ =>
- prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
- | Const (@{const_name distinct}, _) $ _ =>
- let
- fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
- fun prv cu =
- let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
- in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
- in with_conv (dis_conv unfold_distinct_conv) prv (T.mk_prop ct) end
- | @{term Not} $ (Const (@{const_name distinct}, _) $ _) =>
- let
- fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
- fun prv cu =
- let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
- in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
- in with_conv (dis_conv unfold_distinct_conv) prv (T.mk_prop ct) end
- | _ => raise CTERM ("prove_def_axiom", [ct]))
- end
-
- val ifI = @{lemma "(P ==> Q1) ==> (~P ==> Q2) ==> if P then Q1 else Q2"
- by simp}
- val ifE = @{lemma
- "(if P then Q1 else Q2) ==> (P --> Q1 ==> ~P --> Q2 ==> R) ==> R" by simp}
- val claset = HOL_cs addIs [ifI] addEs [ifE]
-in
-fun def_axiom ctxt ct =
- Thm (try_apply ctxt "def_axiom" [
- ("conj/disj", prove_def_axiom),
- ("simp", by_tac (Simplifier.simp_tac HOL_ss)),
- ("fast", by_tac (Classical.fast_tac claset)),
- ("simp+fast", by_tac (Simplifier.simp_tac HOL_ss THEN_ALL_NEW
- Classical.fast_tac claset))] ct)
-end
-
-
-(** local definitions **)
-local
- val intro_rules = [
- @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp},
- @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)"
- by simp},
- @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ]
-
- val apply_rules = [
- @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast},
- @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
- by (atomize(full)) fastsimp} ]
-
- val inst_rule = match_instantiate' Thm.dest_arg
-
- fun apply_rule ct =
- (case get_first (try (inst_rule (T.mk_prop ct))) intro_rules of
- SOME thm => thm
- | NONE => raise CTERM ("intro_def", [ct]))
-in
-fun intro_def ct = apsnd Thm (make_hyp_def (apply_rule ct))
-
-fun apply_def thm =
- get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
- |> the_default (Thm thm)
-end
-
-
-local
- val quant_rules1 = ([
- @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp},
- @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [
- @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp},
- @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}])
-
- val quant_rules2 = ([
- @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp},
- @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [
- @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
- @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
-
- fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
- Tactic.rtac thm ORELSE'
- (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
- (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
-
- fun nnf_quant ctxt qs (p, (vars, _)) ct =
- as_meta_eq ct
- |> by_tac' (nnf_quant_tac (varify ctxt vars (meta_eq_of p)) qs)
-
- val nnf_rules = thm_net_of [@{thm not_not}]
-
- fun abstract ct =
- (case Thm.term_of ct of
- @{term False} => pair
- | @{term Not} $ _ => fold_map_op abstract
- | @{term "op &"} $ _ $ _ => fold_map_binop abstract abstract
- | @{term "op |"} $ _ $ _ => fold_map_binop abstract abstract
- | @{term "op -->"} $ _ $ _ => fold_map_binop abstract abstract
- | @{term "op = :: bool => _"} $ _ $ _ => fold_map_binop abstract abstract
- | _ => fresh_abstraction) ct
-
- fun abstracted ctxt ct =
- abstraction_context' ctxt
- |> abstract (Thm.dest_arg ct)
- |>> T.mk_prop
- |-> prove_abstraction (Classical.best_tac HOL_cs)
-
- fun prove_nnf ctxt =
- try_apply ctxt "nnf" [
- ("conj/disj", prove_conj_disj_eq o Thm.dest_arg),
- ("rule", the o net_instance nnf_rules),
- ("abstract", abstracted ctxt),
- ("tactic", by_tac' (Classical.best_tac HOL_cs))]
-in
-fun nnf ctxt ps ct =
- (case Thm.term_of ct of
- _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
- if l aconv r then MetaEq (Thm.reflexive (Thm.dest_arg ct))
- else MetaEq (nnf_quant ctxt quant_rules1 (hd ps) ct)
- | _ $ (@{term Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
- MetaEq (nnf_quant ctxt quant_rules2 (hd ps) ct)
- | _ =>
- let
- val eqs = map (Thm.symmetric o meta_eq_of o fst) ps
- val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
- (More_Conv.top_sweep_conv (K (More_Conv.rewrs_conv eqs)) ctxt))
- in Thm (with_conv nnf_rewr_conv (prove_nnf ctxt) (T.mk_prop ct)) end)
-end
-
-
-(* equality proof rules *)
-
-(** t = t **)
-fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg ct))
-
-
-(** s = t ==> t = s **)
-local
- val symm_rule = @{lemma "s = t ==> t == s" by simp}
-in
-fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm)
- | symm p = MetaEq (thm_of p COMP symm_rule)
-end
-
-
-(** s = t ==> t = u ==> s = u **)
-local
- val trans_rule = @{lemma "s = t ==> t = u ==> s == u" by simp}
-in
-fun trans (MetaEq thm) q = MetaEq (Thm.transitive thm (meta_eq_of q))
- | trans p (MetaEq thm) = MetaEq (Thm.transitive (meta_eq_of p) thm)
- | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans_rule))
-end
-
-
-(** t1 = s1 & ... & tn = sn ==> f t1 ... tn = f s1 .. sn
- (reflexive antecendents are droppped) **)
-local
- exception MONO
-
- fun prove_refl (ct, _) = Thm.reflexive ct
- fun prove_comb f g cp =
- let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp
- in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
- fun prove_arg f = prove_comb prove_refl f
-
- fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp
-
- fun prove_nary is_comb f =
- let
- fun prove (cp as (ct, _)) = f cp handle MONO =>
- if is_comb (Thm.term_of ct)
- then prove_comb (prove_arg prove) prove cp
- else prove_refl cp
- in prove end
-
- fun prove_list f n cp =
- if n = 0 then prove_refl cp
- else prove_comb (prove_arg f) (prove_list f (n-1)) cp
-
- fun with_length f (cp as (cl, _)) =
- f (length (HOLogic.dest_list (Thm.term_of cl))) cp
-
- fun prove_distinct f = prove_arg (with_length (prove_list f))
-
- fun prove_eq exn lookup cp =
- (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of
- SOME eq => eq
- | NONE => if exn then raise MONO else prove_refl cp)
- val prove_eq_exn = prove_eq true and prove_eq_safe = prove_eq false
-
- fun mono f (cp as (cl, _)) =
- (case Term.head_of (Thm.term_of cl) of
- @{term "op &"} => prove_nary is_conj (prove_eq_exn f)
- | @{term "op |"} => prove_nary is_disj (prove_eq_exn f)
- | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
- | _ => prove (prove_eq_safe f)) cp
-in
-fun monotonicity eqs ct =
- let
- val tab = map (` Thm.prop_of o meta_eq_of) eqs
- val lookup = AList.lookup (op aconv) tab
- val cp = Thm.dest_binop ct
- in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end
-end
-
-
-(** f a b = f b a **)
-local
- val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
-in
-fun commutativity ct = MetaEq (match_instantiate (as_meta_eq ct) rule)
-end
-
-
-(* quantifier proof rules *)
-
-(** P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x)
- P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x) **)
-local
- val rules = [
- @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp},
- @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp}]
-in
-fun quant_intro ctxt (p, (vars, _)) ct =
- let
- val rules' = varify ctxt vars (meta_eq_of p) :: rules
- val cu = as_meta_eq ct
- in MetaEq (by_tac' (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end
-end
-
-
-(** |- ((ALL x. P x) | Q) = (ALL x. P x | Q) **)
-val pull_quant =
- Thm o by_tac (Tactic.rtac @{thm refl} ORELSE' Classical.best_tac HOL_cs)
-
-
-(** |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) **)
-val push_quant =
- Thm o by_tac (Tactic.rtac @{thm refl} ORELSE' Classical.best_tac HOL_cs)
-
-
-(**
- |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn)
-**)
-local
- val elim_all = @{lemma "ALL x. P == P" by simp}
- val elim_ex = @{lemma "EX x. P == P" by simp}
-
- val rule = (fn @{const_name All} => elim_all | _ => elim_ex)
-
- fun collect xs tp =
- if (op aconv) tp then rev xs
- else
- (case tp of
- (Const (q, _) $ Abs (_, _, l), r' as Const _ $ Abs (_, _, r)) =>
- if l aconv r then rev xs
- else if Term.loose_bvar1 (l, 0) then collect (NONE :: xs) (l, r)
- else collect (SOME (rule q) :: xs) (Term.incr_bv (~1, 0, l), r')
- | (Const (q, _) $ Abs (_, _, l), r) =>
- collect (SOME (rule q) :: xs) (Term.incr_bv (~1, 0, l), r)
- | (l, r) => raise TERM ("elim_unused", [l, r]))
-
- fun elim _ [] ct = Conv.all_conv ct
- | elim ctxt (x::xs) ct =
- (case x of
- SOME rule => Conv.rewr_conv rule then_conv elim ctxt xs
- | _ => Conv.arg_conv (Conv.abs_conv (fn (_,cx) => elim cx xs) ctxt)) ct
-in
-fun elim_unused_vars ctxt ct =
- let val (lhs, rhs) = Thm.dest_binop ct
- in MetaEq (elim ctxt (collect [] (Thm.term_of lhs, Thm.term_of rhs)) lhs) end
-end
-
-
-(**
- |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn
-**)
-val dest_eq_res = Thm o by_tac (Simplifier.simp_tac HOL_ss)
-
-
-(** |- ~(ALL x1...xn. P x1...xn) | P a1...an **)
-local
- val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
-in
-val quant_inst = Thm o by_tac (
- REPEAT_ALL_NEW (Tactic.match_tac [rule])
- THEN' Tactic.rtac @{thm excluded_middle})
-end
-
-
-(** c = SOME x. P x |- (EX x. P x) = P c
- c = SOME x. ~ P x |- ~(ALL x. P x) = ~ P c **)
-local
- val elim_ex = @{lemma "EX x. P == P" by simp}
- val elim_all = @{lemma "~ (ALL x. P) == ~P" by simp}
- val sk_ex = @{lemma "c == SOME x. P x ==> EX x. P x == P c"
- by simp (intro eq_reflection some_eq_ex[symmetric])}
- val sk_all = @{lemma "c == SOME x. ~ P x ==> ~(ALL x. P x) == ~ P c"
- by (simp only: not_all) (intro eq_reflection some_eq_ex[symmetric])}
- val sk_ex_rule = ((sk_ex, I), elim_ex)
- and sk_all_rule = ((sk_all, Thm.dest_arg), elim_all)
-
- fun dest f sk_rule =
- Thm.dest_comb (f (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of sk_rule))))
- fun type_of f sk_rule = Thm.ctyp_of_term (snd (dest f sk_rule))
- fun inst_sk (sk_rule, f) p c =
- Thm.instantiate ([(type_of f sk_rule, Thm.ctyp_of_term c)], []) sk_rule
- |> (fn sk' => Thm.instantiate ([], (list2 (dest f sk') ~~ [p, c])) sk')
- |> Conv.fconv_rule (Thm.beta_conversion true)
-
- fun kind (Const (q as @{const_name Ex}, _) $ _) = (sk_ex_rule, q, I, I)
- | kind (@{term Not} $ (Const (q as @{const_name All}, _) $ _)) =
- (sk_all_rule, q, Thm.dest_arg, Thm.capply @{cterm Not})
- | kind _ = z3_exn "skolemize: no quantifier"
-
- fun bodies_of ctxt ct =
- let
- val (rule, q, dest, make) = kind (Thm.term_of ct)
-
- fun inst_abs idx T cbs ct =
- let
- val cv = certify_var ctxt idx T
- val cu = Drule.beta_conv (Thm.dest_arg ct) cv
- in dest_body (idx + 1) ((cv, Thm.dest_arg ct) :: cbs) cu end
- and dest_body idx cbs ct =
- (case Thm.term_of ct of
- Const (qname, _) $ Abs (_, T, _) =>
- if q = qname then inst_abs idx T cbs ct else (make ct, rev cbs)
- | _ => (make ct, rev cbs))
- in (rule, dest_body (#maxidx (Thm.rep_cterm ct) + 1) [] (dest ct)) end
-
- fun transitive f thm = Thm.transitive thm (f (Thm.rhs_of thm))
-
- fun sk_step (rule, elim) (cv, mct, cb) (is, thm) =
- (case mct of
- SOME ct =>
- make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
- |> apsnd (pair ((cv, ct) :: is) o Thm.transitive thm)
- | NONE => ([], (is, transitive (Conv.rewr_conv elim) thm)))
-in
-fun skolemize ctxt ct =
- let
- val (lhs, rhs) = Thm.dest_binop ct
- val (rule, (cu, cbs)) = bodies_of ctxt lhs
- val ctab = snd (Thm.first_order_match (cu, rhs))
- fun lookup_var (cv, cb) = (cv, AList.lookup (op aconvc) ctab cv, cb)
- in
- ([], Thm.reflexive lhs)
- |> fold_map (sk_step rule) (map lookup_var cbs)
- |> apfst (rev o flat) o apsnd (MetaEq o snd)
- end
-end
-
-
-(* theory proof rules *)
-
-(** prove linear arithmetic problems via generalization **)
-local
- val is_numeral = can HOLogic.dest_number
- fun is_number (Const (@{const_name uminus}, _) $ t) = is_numeral t
- | is_number t = is_numeral t
-
- local
- val int_distrib = @{lemma "n * (x + y) == n * x + n * (y::int)"
- by (simp add: int_distrib)}
- val real_distrib = @{lemma "n * (x + y) == n * x + n * (y::real)"
- by (simp add: mult.add_right)}
- val int_assoc = @{lemma "n * (m * x) == (n * m) * (x::int)" by linarith}
- val real_assoc = @{lemma "n * (m * x) == (n * m) * (x::real)" by linarith}
-
- val number_of_cong = @{lemma
- "number_of x * number_of y == (number_of (x * y) :: int)"
- "number_of x * number_of y == (number_of (x * y) :: real)"
- by simp_all}
- val reduce_ss = HOL_ss addsimps @{thms mult_bin_simps}
- addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
- addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
- addsimps number_of_cong
- val reduce_conv = Simplifier.rewrite reduce_ss
-
- fun apply_conv distrib assoc u ct =
- ((case u of
- Const (@{const_name times}, _) $ n $ _ =>
- if is_number n
- then Conv.rewr_conv assoc then_conv Conv.arg1_conv reduce_conv
- else Conv.rewr_conv distrib
- | _ => Conv.rewr_conv distrib)
- then_conv Conv.binop_conv (Conv.try_conv distrib_conv)) ct
-
- and distrib_conv ct =
- (case Thm.term_of ct of
- @{term "op * :: int => _"} $ n $ u =>
- if is_number n then apply_conv int_distrib int_assoc u
- else Conv.no_conv
- | @{term "op * :: real => _"} $ n $ u =>
- if is_number n then apply_conv real_distrib real_assoc u
- else Conv.no_conv
- | _ => Conv.no_conv) ct
- in
- val all_distrib_conv = More_Conv.top_sweep_conv (K distrib_conv)
- end
-
- local
- fun fresh ct = fresh_abstraction ct
-
- fun mult f1 f2 ct t u =
- if is_number t
- then if is_number u then pair ct else fold_map_binop f1 f2 ct
- else fresh ct
-
- fun poly ct =
- (case Thm.term_of ct of
- Const (@{const_name plus}, _) $ _ $ _ => fold_map_binop poly poly ct
- | Const (@{const_name minus}, _) $ _ $ _ => fold_map_binop poly poly ct
- | Const (@{const_name times}, _) $ t $ u => mult pair fresh ct t u
- | Const (@{const_name div}, _) $ t $ u => mult fresh pair ct t u
- | Const (@{const_name mod}, _) $ t $ u => mult fresh pair ct t u
- | t => if is_number t then pair ct else fresh ct)
-
- val ineq_ops = [@{term "op = :: int => _"}, @{term "op < :: int => _"},
- @{term "op <= :: int => _"}, @{term "op = :: real => _"},
- @{term "op < :: real => _"}, @{term "op <= :: real => _"}]
- fun ineq ct =
- (case Thm.term_of ct of
- t $ _ $ _ =>
- if member (op =) ineq_ops t then fold_map_binop poly poly ct
- else raise CTERM ("arith_lemma", [ct])
- | @{term Not} $ (t $ _ $ _) =>
- if member (op =) ineq_ops t
- then fold_map_op (fold_map_binop poly poly) ct
- else raise CTERM ("arith_lemma", [ct])
- | _ => raise CTERM ("arith_lemma", [ct]))
-
- fun conj ct =
- (case Thm.term_of ct of
- @{term "op &"} $ _ $ _ => fold_map_binop conj conj ct
- | @{term "~False"} => pair ct
- | _ => ineq ct)
-
- fun disj ct =
- (case Thm.term_of ct of
- @{term "op |"} $ _ $ _ => fold_map_binop disj disj ct
- | @{term False} => pair ct
- | _ => conj ct)
- in
- fun prove_arith ctxt thms ct =
- abstraction_context ctxt
- |> fold_map (fold_map_op ineq o Thm.cprop_of) thms
- ||>> fold_map_op disj ct
- |>> uncurry (fold_rev (Thm.mk_binop @{cterm "op ==>"}))
- |-> prove_abstraction (Arith_Data.arith_tac ctxt)
- |> fold (fn th1 => fn th2 => Thm.implies_elim th2 th1) thms
- end
-in
-fun arith_lemma ctxt thms ct =
- let val thms' = map (Conv.fconv_rule (all_distrib_conv ctxt)) thms
- in with_conv (all_distrib_conv ctxt) (prove_arith ctxt thms') ct end
-end
-
-(** theory simpset **)
-local
- val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
- val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
- val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
- val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
-
- fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
- fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
- | dest_binop t = raise TERM ("dest_binop", [t])
-
- fun prove_antisym_le ss t =
- let
- val (le, r, s) = dest_binop t
- val less = Const (@{const_name less}, Term.fastype_of le)
- val prems = Simplifier.prems_of_ss ss
- in
- (case find_first (eq_prop (le $ s $ r)) prems of
- NONE =>
- find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
- |> Option.map (fn thm => thm RS antisym_less1)
- | SOME thm => SOME (thm RS antisym_le1))
- end
- handle THM _ => NONE
-
- fun prove_antisym_less ss t =
- let
- val (less, r, s) = dest_binop (HOLogic.dest_not t)
- val le = Const (@{const_name less_eq}, Term.fastype_of less)
- val prems = prems_of_ss ss
- in
- (case find_first (eq_prop (le $ r $ s)) prems of
- NONE =>
- find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
- |> Option.map (fn thm => thm RS antisym_less2)
- | SOME thm => SOME (thm RS antisym_le2))
- end
- handle THM _ => NONE
-in
-val z3_simpset = HOL_ss addsimps @{thms array_rules}
- addsimps @{thms ring_distribs} addsimps @{thms field_simps}
- addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
- addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
- addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}
- addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
- addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
- addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
- addsimps [@{thm mult_1_left}]
- addsimprocs [
- Simplifier.simproc @{theory} "fast_int_arith" [
- "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
- Simplifier.simproc @{theory} "fast_real_arith" [
- "(m::real) < n", "(m::real) <= n", "(m::real) = n"]
- (K Lin_Arith.simproc),
- Simplifier.simproc @{theory} "antisym le" ["(x::'a::order) <= y"]
- (K prove_antisym_le),
- Simplifier.simproc @{theory} "antisym less" ["~ (x::'a::linorder) < y"]
- (K prove_antisym_less)]
-end
-
-(** theory lemmas: linear arithmetic, arrays **)
-local
- val array_ss = HOL_ss addsimps @{thms array_rules}
- val array_pre_ss = HOL_ss addsimps @{thms apply_def array_ext_def}
- fun array_tac thms =
- Tactic.cut_facts_tac thms
- THEN' (Simplifier.asm_full_simp_tac array_pre_ss)
- THEN' (SOLVED' (Simplifier.asm_full_simp_tac array_ss) ORELSE'
- Tactic.rtac @{thm someI2_ex}
- THEN_ALL_NEW (SOLVED' (Simplifier.asm_full_simp_tac array_ss) ORELSE'
- Classical.fast_tac HOL_cs))
-
- fun full_arith_tac ctxt thms =
- Tactic.cut_facts_tac thms
- THEN' Arith_Data.arith_tac ctxt
-
- fun simp_arith_tac ctxt thms =
- Tactic.cut_facts_tac thms
- THEN' Simplifier.asm_full_simp_tac z3_simpset
- THEN' Arith_Data.arith_tac ctxt
-in
-fun th_lemma ctxt thms ct =
- Thm (try_apply ctxt "th-lemma" [
- ("abstract arith", arith_lemma ctxt thms),
- ("array", by_tac' (array_tac thms)),
- ("full arith", by_tac' (full_arith_tac ctxt thms)),
- ("simp arith", by_tac' (simp_arith_tac ctxt thms))] (T.mk_prop ct))
-end
-
-(** rewriting: prove equalities:
- * ACI of conjunction/disjunction
- * contradiction, excluded middle
- * logical rewriting rules (for negation, implication, equivalence,
- distinct)
- * normal forms for polynoms (integer/real arithmetic)
- * quantifier elimination over linear arithmetic
- * ... ? **)
-structure Z3_Rewrite_Rules =
-struct
- val name = "z3_rewrite"
- val descr = "Z3 rewrite rules used in proof reconstruction"
-
- structure Data = Generic_Data
- (
- type T = thm Net.net
- val empty = Net.empty
- val extend = I
- val merge = Net.merge Thm.eq_thm_prop
- )
- val get = Data.get o Context.Proof
-
- val entry = ` Thm.prop_of o Simplifier.rewrite_rule [true_false]
- val eq = Thm.eq_thm_prop
- val ins = Net.insert_term eq o entry and del = Net.delete_term eq o entry
- fun insert thm net = ins thm net handle Net.INSERT => net
- fun delete thm net = del thm net handle Net.DELETE => net
-
- val add = Thm.declaration_attribute (Data.map o insert)
- val del = Thm.declaration_attribute (Data.map o delete)
- val setup = Attrib.setup (Binding.name name) (Attrib.add_del add del) descr
-end
-
-local
- val contra_rule = @{lemma "P ==> ~P ==> False" by (rule notE)}
- fun contra_left conj thm =
- let
- fun make_tab xs = fold Termtab.update xs Termtab.empty
- val tab = make_tab (explode_term conj true (prop_of thm))
- fun pnlits (t, nrs) =
- (case t of
- @{term Not} $ u => Termtab.lookup tab u |> Option.map (pair nrs)
- | _ => NONE)
- in
- (case Termtab.lookup tab @{term False} of
- SOME rs => extract_lit thm rs
- | NONE =>
- pairself (extract_lit thm) (the (Termtab.get_first pnlits tab))
- |> (fn (nlit, plit) => nlit COMP (plit COMP contra_rule)))
- end
- val falseE_v = Thm.dest_arg (Thm.dest_arg (Thm.cprop_of @{thm FalseE}))
- fun contra_right ct = Thm.instantiate ([], [(falseE_v, ct)]) @{thm FalseE}
- fun contradiction conj ct =
- iff_intro (under_assumption (contra_left conj) ct) (contra_right ct)
-
- fun conj_disj ct =
- let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
- in
- (case Thm.term_of cr of
- @{term False} => contradiction true cl
- | @{term "~False"} => contrapos2 (contradiction false o fst) cp
- | _ => prove_conj_disj_eq (Thm.dest_arg ct))
- end
-
- val distinct =
- let val try_unfold = Conv.try_conv unfold_distinct_conv
- in with_conv (Conv.arg_conv (Conv.binop_conv try_unfold)) conj_disj end
-
- val nnf_neg_rule = @{lemma "~~P == P" by fastsimp}
- val nnf_cd_rules = @{lemma "~(P | Q) == ~P & ~Q" "~(P & Q) == ~P | ~Q"
- by fastsimp+}
-
- fun nnf_conv ct = Conv.try_conv (
- (Conv.rewr_conv nnf_neg_rule then_conv nnf_conv) else_conv
- (More_Conv.rewrs_conv nnf_cd_rules then_conv Conv.binop_conv nnf_conv)) ct
- val iffI_rule = @{lemma "~P | Q ==> ~Q | P ==> P = Q" by fast}
- fun arith_tac ctxt = CSUBGOAL (fn (goal, i) =>
- let val prep_then = with_conv (Conv.arg_conv (Conv.binop_conv nnf_conv))
- in Tactic.rtac (prep_then (arith_lemma ctxt []) goal) i end)
- fun arith_eq_tac ctxt =
- Tactic.rtac iffI_rule THEN_ALL_NEW arith_tac ctxt
- ORELSE' arith_tac ctxt
-
- fun simp_tac thms = CHANGED o Simplifier.simp_tac (z3_simpset addsimps thms)
- ORELSE' Classical.best_tac HOL_cs
- fun simp_arith_tac ctxt thms = Simplifier.simp_tac (z3_simpset addsimps thms)
- THEN_ALL_NEW Arith_Data.arith_tac ctxt
-in
-fun rewrite ctxt thms ct =
- let val rules_net = Z3_Rewrite_Rules.get ctxt
- in
- Thm (try_apply ctxt "rewrite" [
- ("schematic rule", the o net_instance rules_net),
- ("conj/disj", conj_disj),
- ("distinct", distinct),
- ("arith", by_tac' (arith_eq_tac ctxt)),
- ("classical", by_tac' (Classical.best_tac HOL_cs)),
- ("simp", by_tac' (simp_tac thms)),
- ("simp+arith", by_tac' (simp_arith_tac ctxt thms)),
- ("full arith", by_tac' (Arith_Data.arith_tac ctxt))] (T.mk_prop ct))
- end
-end
-
-
-(* tracing and debugging *)
-
-fun check idx r ct ((_, p), _) =
- let val thm = thm_of p |> tap (Thm.join_proofs o single)
- in
- if (Thm.cprop_of thm) aconvc (T.mk_prop ct) then ()
- else z3_exn ("proof step failed: " ^ quote (string_of_rule r) ^
- " (#" ^ string_of_int idx ^ ")")
- end
-
-local
- fun trace_before ctxt idx (r, ps, ct) =
- Pretty.string_of (
- Pretty.big_list ("#" ^ string_of_int idx ^ ": " ^ string_of_rule r) [
- Pretty.big_list "assumptions:"
- (map (Display.pretty_thm ctxt o thm_of o fst) ps),
- Pretty.block [Pretty.str "goal: ",
- Syntax.pretty_term ctxt (Thm.term_of ct)]])
-
- fun trace_after ctxt ((_, p), _) = Pretty.string_of (Pretty.block
- [Pretty.str "result: ", Display.pretty_thm ctxt (thm_of p)])
-in
-fun trace_rule ctxt idx prove r ps ct ptab =
- let
- val _ = SMT_Solver.trace_msg ctxt (trace_before ctxt idx) (r, ps, ct)
- val result = prove r ps ct ptab
- val _ = SMT_Solver.trace_msg ctxt (trace_after ctxt) result
- in result end
-end
-
-
-(* overall reconstruction procedure *)
-
-fun not_supported r =
- z3_exn ("proof rule not implemented: " ^ quote (string_of_rule r))
-
-fun prove ctxt unfolds assms =
- let
- val prems = Option.map (prepare_assms ctxt) assms
-
- fun step r ps ct ptab =
- (case (r, ps) of
- (* core rules *)
- (TrueAxiom, _) => (([], Thm true_thm), ptab)
- | (Asserted, _) => (([], asserted ctxt unfolds prems ct), ptab)
- | (Goal, _) => (([], asserted ctxt unfolds prems ct), ptab)
- | (ModusPonens, [(p, _), (q, _)]) => (([], mp q (thm_of p)), ptab)
- | (ModusPonensOeq, [(p, _), (q, _)]) => (([], mp q (thm_of p)), ptab)
- | (AndElim, [(p, (_, i))]) => apfst (pair []) (and_elim (p, i) ct ptab)
- | (NotOrElim, [(p, (_, i))]) =>
- apfst (pair []) (not_or_elim (p, i) ct ptab)
- | (Hypothesis, _) => (([], Thm (Thm.assume (T.mk_prop ct))), ptab)
- | (Lemma, [(p, _)]) => (([], lemma (thm_of p) ct), ptab)
- | (UnitResolution, (p, _) :: ps) =>
- (([], unit_resolution (thm_of p) (map (thm_of o fst) ps) ct), ptab)
- | (IffTrue, [(p, _)]) => (([], iff_true (thm_of p)), ptab)
- | (IffFalse, [(p, _)]) => (([], iff_false (thm_of p)), ptab)
- | (Distributivity, _) => (([], distributivity ct), ptab)
- | (DefAxiom, _) => (([], def_axiom ctxt ct), ptab)
- | (IntroDef, _) => (intro_def ct, ptab)
- | (ApplyDef, [(p, _)]) => (([], apply_def (thm_of p)), ptab)
- | (IffOeq, [(p, _)]) => (([], p), ptab)
- | (NnfPos, _) => (([], nnf ctxt ps ct), ptab)
- | (NnfNeg, _) => (([], nnf ctxt ps ct), ptab)
-
- (* equality rules *)
- | (Reflexivity, _) => (([], refl ct), ptab)
- | (Symmetry, [(p, _)]) => (([], symm p), ptab)
- | (Transitivity, [(p, _), (q, _)]) => (([], trans p q), ptab)
- | (Monotonicity, _) => (([], monotonicity (map fst ps) ct), ptab)
- | (Commutativity, _) => (([], commutativity ct), ptab)
-
- (* quantifier rules *)
- | (QuantIntro, [p]) => (([], quant_intro ctxt p ct), ptab)
- | (PullQuant, _) => (([], pull_quant ct), ptab)
- | (PushQuant, _) => (([], push_quant ct), ptab)
- | (ElimUnusedVars, _) => (([], elim_unused_vars ctxt ct), ptab)
- | (DestEqRes, _) => (([], dest_eq_res ct), ptab)
- | (QuantInst, _) => (([], quant_inst ct), ptab)
- | (Skolemize, _) => (skolemize ctxt ct, ptab)
-
- (* theory rules *)
- | (ThLemma, _) => (([], th_lemma ctxt (map (thm_of o fst) ps) ct), ptab)
- | (Rewrite, _) => (([], rewrite ctxt [] ct), ptab)
- | (RewriteStar, ps) =>
- (([], rewrite ctxt (map (thm_of o fst) ps) ct), ptab)
-
- | (NnfStar, _) => not_supported r
- | (CnfStar, _) => not_supported r
- | (TransitivityStar, _) => not_supported r
- | (PullQuantStar, _) => not_supported r
-
- | _ => z3_exn ("Proof rule " ^ quote (string_of_rule r) ^
- " has an unexpected number of arguments."))
-
- fun eq_hyp (ct, cu) = Thm.dest_arg1 ct aconvc Thm.dest_arg1 cu
-
- fun conclude idx rule prop ((hypss, ps), ptab) =
- trace_rule ctxt idx step rule ps prop ptab
- |> Config.get ctxt SMT_Solver.trace ? tap (check idx rule prop)
- |>> apfst (distinct eq_hyp o fold append hypss)
-
- fun add_sequent idx vars (hyps, thm) ptab =
- let val s = Sequent {hyps=hyps, vars=vars, thm=thm}
- in ((hyps, (thm, vars)), Inttab.update (idx, s) ptab) end
-
- fun lookup idx ptab =
- (case Inttab.lookup ptab idx of
- SOME (Unproved {rule, subs, vars, prop}) =>
- fold_map lookup subs ptab
- |>> split_list
- |>> apsnd (map2 (fn idx => fn (p, vs) => (p, (vs, idx))) subs)
- |> conclude idx rule prop
- |-> add_sequent idx vars
- | SOME (Sequent {hyps, vars, thm}) => ((hyps, (thm, vars)), ptab)
- | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
-
- fun result (hyps, (thm, _)) =
- fold SMT_Normalize.discharge_definition hyps (thm_of thm)
-
- in (fn ptab => fn idx => result (fst (lookup idx ptab))) end
-
-val setup = trace_assms_setup #> Z3_Rewrite_Rules.setup
-
-end
--- a/src/HOL/SMT/Tools/z3_proof_terms.ML Wed May 12 23:53:58 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,252 +0,0 @@
-(* Title: HOL/SMT/Tools/z3_proof_terms.ML
- Author: Sascha Boehme, TU Muenchen
-
-Reconstruction functions for terms occurring in Z3 proofs.
-*)
-
-signature Z3_PROOF_TERMS =
-sig
- val mk_prop: cterm -> cterm
- val mk_meta_eq: cterm -> cterm -> cterm
-
- type preterm
-
- val compile: theory -> Name.context -> preterm -> cterm * cterm list
-
- val mk_bound: theory -> int -> typ -> preterm
- val mk_fun: cterm -> preterm list -> preterm
- val mk_forall: theory -> string * typ -> preterm -> preterm
- val mk_exists: theory -> string * typ -> preterm -> preterm
-
- val mk_true: preterm
- val mk_false: preterm
- val mk_not: preterm -> preterm
- val mk_and: preterm list -> preterm
- val mk_or: preterm list -> preterm
- val mk_implies: preterm -> preterm -> preterm
- val mk_iff: preterm -> preterm -> preterm
-
- val mk_eq: preterm -> preterm -> preterm
- val mk_if: preterm -> preterm -> preterm -> preterm
- val mk_distinct: preterm list -> preterm
-
- val mk_pat: preterm list -> preterm
- val mk_nopat: preterm list -> preterm
- val mk_trigger: preterm list -> preterm -> preterm
-
- val mk_access: preterm -> preterm -> preterm
- val mk_update: preterm -> preterm -> preterm -> preterm
- val mk_array_ext: preterm -> preterm -> preterm
-
- val mk_int_num: int -> preterm
- val mk_real_frac_num: int * int option -> preterm
- val mk_uminus: preterm -> preterm
- val mk_add: preterm -> preterm -> preterm
- val mk_sub: preterm -> preterm -> preterm
- val mk_mul: preterm -> preterm -> preterm
- val mk_int_div: preterm -> preterm -> preterm
- val mk_real_div: preterm -> preterm -> preterm
- val mk_rem: preterm -> preterm -> preterm
- val mk_mod: preterm -> preterm -> preterm
- val mk_lt: preterm -> preterm -> preterm
- val mk_le: preterm -> preterm -> preterm
-
- val wordT : int -> typ
- val mk_bv_num : theory -> int -> int -> preterm
-
- val var_prefix: string
-end
-
-structure Z3_Proof_Terms: Z3_PROOF_TERMS =
-struct
-
-fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
-fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
-fun mk_inst_pair destT cpat = (destT (Thm.ctyp_of_term cpat), cpat)
-val destT1 = hd o Thm.dest_ctyp
-val destT2 = hd o tl o Thm.dest_ctyp
-
-
-val mk_prop = Thm.capply @{cterm Trueprop}
-
-val meta_eq = mk_inst_pair destT1 @{cpat "op =="}
-fun mk_meta_eq ct = Thm.mk_binop (instT (Thm.ctyp_of_term ct) meta_eq) ct
-
-
-datatype preterm = Preterm of {
- cterm: cterm,
- vars: (int * cterm) list }
-
-fun mk_preterm (ct, vs) = Preterm {cterm=ct, vars=vs}
-fun dest_preterm (Preterm {cterm, vars}) = (cterm, vars)
-fun ctyp_of_preterm (Preterm {cterm, ...}) = Thm.ctyp_of_term cterm
-
-fun instT' e = instT (ctyp_of_preterm e)
-
-val maxidx_of = #maxidx o Thm.rep_cterm
-
-val var_prefix = "v"
-
-local
-fun mk_inst nctxt cert vs =
- let
- val max = fold (Integer.max o fst) vs 0
- val names = fst (Name.variants (replicate (max + 1) var_prefix) nctxt)
- fun mk (i, v) = (v, cert (Free (nth names i, #T (Thm.rep_cterm v))))
- in map mk vs end
-
-fun fix_vars _ _ ct [] = (ct, [])
- | fix_vars thy nctxt ct vs =
- let
- val cert = Thm.cterm_of thy
- val inst = mk_inst nctxt cert vs
- in (Thm.instantiate_cterm ([], inst) ct, map snd inst) end
-in
-fun compile thy nctxt (Preterm {cterm, vars}) = fix_vars thy nctxt cterm vars
-end
-
-local
-fun app e (ct1, vs1) =
- let
- fun part (var as (i, v)) (inst, vs) =
- (case AList.lookup (op =) vs1 i of
- NONE => (inst, var :: vs)
- | SOME v' => ((v, v') :: inst, vs))
-
- val (ct2, vs2) = dest_preterm e
- val incr =
- if maxidx_of ct1 < 0 orelse maxidx_of ct2 < 0 then I
- else Thm.incr_indexes_cterm (maxidx_of ct1 + 1)
-
- val (inst, vs) = fold (part o apsnd incr) vs2 ([], vs1)
- val ct2' = Thm.instantiate_cterm ([], inst) (incr ct2)
- in (Thm.capply ct1 ct2', vs) end
-in
-fun mk_fun ct es = mk_preterm (fold app es (ct, []))
-fun mk_binop f t u = mk_fun f [t, u]
-fun mk_nary _ e [] = e
- | mk_nary ct _ es = uncurry (fold_rev (mk_binop ct)) (split_last es)
-end
-
-fun mk_bound thy i T =
- let val ct = Thm.cterm_of thy (Var ((Name.uu, 0), T))
- in mk_preterm (ct, [(i, ct)]) end
-
-local
-fun mk_quant q thy (_, T) e =
- let
- val (ct, vs) = dest_preterm e
- val cv =
- (case AList.lookup (op =) vs 0 of
- SOME cv => cv
- | _ => Thm.cterm_of thy (Var ((Name.uu, maxidx_of ct + 1), T)))
- val cq = instT (Thm.ctyp_of_term cv) q
- fun dec (i, v) = if i = 0 then NONE else SOME (i - 1, v)
- in mk_preterm (Thm.capply cq (Thm.cabs cv ct), map_filter dec vs) end
-in
-fun mk_forall thy = mk_quant (mk_inst_pair (destT1 o destT1) @{cpat All}) thy
-fun mk_exists thy = mk_quant (mk_inst_pair (destT1 o destT1) @{cpat Ex}) thy
-end
-
-
-val mk_false = mk_fun @{cterm False} []
-val mk_not = mk_fun @{cterm Not} o single
-val mk_true = mk_not mk_false
-val mk_and = mk_nary @{cterm "op &"} mk_true
-val mk_or = mk_nary @{cterm "op |"} mk_false
-val mk_implies = mk_binop @{cterm "op -->"}
-val mk_iff = mk_binop @{cterm "op = :: bool => _"}
-
-val eq = mk_inst_pair destT1 @{cpat "op ="}
-fun mk_eq t u = mk_binop (instT' t eq) t u
-
-val if_term = mk_inst_pair (destT1 o destT2) @{cpat If}
-fun mk_if c t u = mk_fun (instT' t if_term) [c, t, u]
-
-val nil_term = mk_inst_pair destT1 @{cpat Nil}
-val cons_term = mk_inst_pair destT1 @{cpat Cons}
-fun mk_list cT es =
- fold_rev (mk_binop (instT cT cons_term)) es (mk_fun (instT cT nil_term) [])
-
-val distinct = mk_inst_pair (destT1 o destT1) @{cpat distinct}
-fun mk_distinct [] = mk_true
- | mk_distinct (es as (e :: _)) =
- mk_fun (instT' e distinct) [mk_list (ctyp_of_preterm e) es]
-
-val pat = mk_inst_pair destT1 @{cpat pat}
-val nopat = mk_inst_pair destT1 @{cpat nopat}
-val andpat = mk_inst_pair (destT1 o destT2) @{cpat "op andpat"}
-fun mk_gen_pat _ [] = raise TERM ("mk_gen_pat: empty pattern", [])
- | mk_gen_pat pat (e :: es) =
- let fun mk t p = mk_fun (instT' t andpat) [p, t]
- in fold mk es (mk_fun (instT' e pat) [e]) end
-val mk_pat = mk_gen_pat pat
-val mk_nopat = mk_gen_pat nopat
-
-fun mk_trigger es e = mk_fun @{cterm trigger} [mk_list @{ctyp pattern} es, e]
-
-
-val access = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat apply}
-fun mk_access array index =
- let val cTs = Thm.dest_ctyp (ctyp_of_preterm array)
- in mk_fun (instTs cTs access) [array, index] end
-
-val update = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat fun_upd}
-fun mk_update array index value =
- let val cTs = Thm.dest_ctyp (ctyp_of_preterm array)
- in mk_fun (instTs cTs update) [array, index, value] end
-
-val array_ext = mk_inst_pair (Thm.dest_ctyp o destT1) @{cpat array_ext}
-fun mk_array_ext a1 a2 =
- let val cTs = Thm.dest_ctyp (ctyp_of_preterm a1)
- in mk_fun (instTs cTs array_ext) [a1, a2] end
-
-
-fun mk_int_num i = mk_fun (Numeral.mk_cnumber @{ctyp int} i) []
-fun mk_real_num i = mk_fun (Numeral.mk_cnumber @{ctyp real} i) []
-
-fun mk_real_frac_num (e, NONE) = mk_real_num e
- | mk_real_frac_num (e, SOME d) =
- mk_binop @{cterm "op / :: real => _"} (mk_real_num e) (mk_real_num d)
-
-fun has_int_type e = (Thm.typ_of (ctyp_of_preterm e) = @{typ int})
-fun choose e i r = if has_int_type e then i else r
-
-val uminus_i = @{cterm "uminus :: int => _"}
-val uminus_r = @{cterm "uminus :: real => _"}
-fun mk_uminus e = mk_fun (choose e uminus_i uminus_r) [e]
-
-fun arith_op int_op real_op t u = mk_binop (choose t int_op real_op) t u
-
-val mk_add = arith_op @{cterm "op + :: int => _"} @{cterm "op + :: real => _"}
-val mk_sub = arith_op @{cterm "op - :: int => _"} @{cterm "op - :: real => _"}
-val mk_mul = arith_op @{cterm "op * :: int => _"} @{cterm "op * :: real => _"}
-val mk_int_div = mk_binop @{cterm "op div :: int => _"}
-val mk_real_div = mk_binop @{cterm "op / :: real => _"}
-val mk_rem = mk_binop @{cterm "op rem :: int => _"}
-val mk_mod = mk_binop @{cterm "op mod :: int => _"}
-val mk_lt = arith_op @{cterm "op < :: int => _"} @{cterm "op < :: real => _"}
-val mk_le = arith_op @{cterm "op <= :: int => _"} @{cterm "op <= :: real => _"}
-
-fun binT size =
- let
- fun bitT i T =
- if i = 0
- then Type (@{type_name "Numeral_Type.bit0"}, [T])
- else Type (@{type_name "Numeral_Type.bit1"}, [T])
-
- fun binT i =
- if i = 0 then @{typ "Numeral_Type.num0"}
- else if i = 1 then @{typ "Numeral_Type.num1"}
- else let val (q, r) = Integer.div_mod i 2 in bitT r (binT q) end
- in
- if size >= 0 then binT size
- else raise TYPE ("mk_binT: " ^ string_of_int size, [], [])
- end
-
-fun wordT size = Type (@{type_name "word"}, [binT size])
-
-fun mk_bv_num thy num size =
- mk_fun (Numeral.mk_cnumber (Thm.ctyp_of thy (wordT size)) num) []
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/Tools/z3_proof_tools.ML Wed May 12 23:53:59 2010 +0200
@@ -0,0 +1,361 @@
+(* Title: HOL/SMT/Tools/z3_proof_tools.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Helper functions required for Z3 proof reconstruction.
+*)
+
+signature Z3_PROOF_TOOLS =
+sig
+ (* accessing and modifying terms *)
+ val term_of: cterm -> term
+ val prop_of: thm -> term
+ val mk_prop: cterm -> cterm
+ val as_meta_eq: cterm -> cterm
+
+ (* theorem nets *)
+ val thm_net_of: thm list -> thm Net.net
+ val net_instance: thm Net.net -> cterm -> thm option
+
+ (* proof combinators *)
+ val under_assumption: (thm -> thm) -> cterm -> thm
+ val with_conv: conv -> (cterm -> thm) -> cterm -> thm
+ val discharge: thm -> thm -> thm
+ val varify: string list -> thm -> thm
+ val unfold_eqs: Proof.context -> thm list -> conv
+ val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
+ val by_tac: (int -> tactic) -> cterm -> thm
+ val make_hyp_def: thm -> cterm list * thm
+ val by_abstraction: Proof.context -> thm list -> (Proof.context -> cterm ->
+ thm) -> cterm -> thm
+
+ (* a faster COMP *)
+ type compose_data
+ val precompose: (cterm -> cterm list) -> thm -> compose_data
+ val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
+ val compose: compose_data -> thm -> thm
+
+ (* unfolding of 'distinct' *)
+ val unfold_distinct_conv: conv
+
+ (* simpset *)
+ val make_simpset: Proof.context -> thm list -> simpset
+end
+
+structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
+struct
+
+
+
+(* accessing terms *)
+
+val dest_prop = (fn @{term Trueprop} $ t => t | t => t)
+
+fun term_of ct = dest_prop (Thm.term_of ct)
+fun prop_of thm = dest_prop (Thm.prop_of thm)
+
+val mk_prop = Thm.capply @{cterm Trueprop}
+
+val (eqT, eq) = `(hd o Thm.dest_ctyp o Thm.ctyp_of_term) @{cpat "op =="}
+fun mk_meta_eq_cterm ct cu =
+ let val inst = ([(eqT, Thm.ctyp_of_term ct)], [])
+ in Thm.mk_binop (Thm.instantiate_cterm inst eq) ct cu end
+
+fun as_meta_eq ct = uncurry mk_meta_eq_cterm (Thm.dest_binop (Thm.dest_arg ct))
+
+
+
+(* theorem nets *)
+
+fun thm_net_of thms =
+ let fun insert thm = Net.insert_term (K false) (Thm.prop_of thm, thm)
+ in fold insert thms Net.empty end
+
+fun maybe_instantiate ct thm =
+ try Thm.first_order_match (Thm.cprop_of thm, ct)
+ |> Option.map (fn inst => Thm.instantiate inst thm)
+
+fun first_of thms ct = get_first (maybe_instantiate ct) thms
+fun net_instance net ct = first_of (Net.match_term net (Thm.term_of ct)) ct
+
+
+
+(* proof combinators *)
+
+fun under_assumption f ct =
+ let val ct' = mk_prop ct
+ in Thm.implies_intr ct' (f (Thm.assume ct')) end
+
+fun with_conv conv prove ct =
+ let val eq = Thm.symmetric (conv ct)
+ in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
+
+fun discharge p pq = Thm.implies_elim pq p
+
+fun varify vars = Drule.generalize ([], vars)
+
+fun unfold_eqs _ [] = Conv.all_conv
+ | unfold_eqs ctxt eqs =
+ More_Conv.top_sweep_conv (K (More_Conv.rewrs_conv eqs)) ctxt
+
+fun match_instantiate f ct thm =
+ Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
+
+fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
+
+(* |- c x == t x ==> P (c x) ~~> c == t |- P (c x) *)
+fun make_hyp_def thm =
+ let
+ val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
+ val (cf, cvs) = Drule.strip_comb lhs
+ val eq = mk_meta_eq_cterm cf (fold_rev Thm.cabs cvs rhs)
+ fun apply cv th =
+ Thm.combination th (Thm.reflexive cv)
+ |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
+ in ([eq], Thm.implies_elim thm (fold apply cvs (Thm.assume eq))) end
+
+
+
+(* abstraction *)
+
+local
+
+fun typ_of ct = #T (Thm.rep_cterm ct)
+fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
+
+fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
+
+fun context_of (ctxt, _, _, _) = ctxt
+
+fun replace (cv, ct) = Thm.forall_elim ct o Thm.forall_intr cv
+
+fun abs_instantiate (_, tab, _, beta_norm) =
+ fold replace (map snd (Termtab.dest tab)) #>
+ beta_norm ? Conv.fconv_rule (Thm.beta_conversion true)
+
+fun generalize cvs =
+ let
+ val no_name = ""
+
+ fun dest (Free (n, _)) = n
+ | dest _ = no_name
+
+ fun gen vs (t as Free (n, _)) =
+ let val i = find_index (equal n) vs
+ in
+ if i >= 0 then insert (op aconvc) (nth cvs i) #> pair (Bound i)
+ else pair t
+ end
+ | gen vs (t $ u) = gen vs t ##>> gen vs u #>> (op $)
+ | gen vs (Abs (n, T, t)) =
+ gen (no_name :: vs) t #>> (fn u => Abs (n, T, u))
+ | gen _ t = pair t
+
+ in (fn ct => gen (map (dest o Thm.term_of) cvs) (Thm.term_of ct) []) end
+
+fun fresh_abstraction cvs ct (cx as (ctxt, tab, idx, beta_norm)) =
+ let val (t, cvs') = generalize cvs ct
+ in
+ (case Termtab.lookup tab t of
+ SOME (cv, _) => (cv, cx)
+ | NONE =>
+ let
+ val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
+ val cv = certify ctxt (Free (n, map typ_of cvs' ---> typ_of ct))
+ val cv' = Drule.list_comb (cv, cvs')
+ val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
+ val beta_norm' = beta_norm orelse not (null cvs')
+ in (cv', (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
+ end
+
+fun abs_arg f cvs ct =
+ let val (cf, cu) = Thm.dest_comb ct
+ in f cvs cu #>> Thm.capply cf end
+
+fun abs_comb f g cvs ct =
+ let val (cf, cu) = Thm.dest_comb ct
+ in f cvs cf ##>> g cvs cu #>> uncurry Thm.capply end
+
+fun abs_list f g cvs ct =
+ (case Thm.term_of ct of
+ Const (@{const_name Nil}, _) => pair ct
+ | Const (@{const_name Cons}, _) $ _ $ _ =>
+ abs_comb (abs_arg f) (abs_list f g) cvs ct
+ | _ => g cvs ct)
+
+fun abs_abs f cvs ct =
+ let val (cv, cu) = Thm.dest_abs NONE ct
+ in f (cv :: cvs) cu #>> Thm.cabs cv end
+
+val is_atomic = (fn _ $ _ => false | Abs _ => false | _ => true)
+val is_arithT = (fn @{typ int} => true | @{typ real} => true | _ => false)
+fun is_number t =
+ (case try HOLogic.dest_number t of
+ SOME (T, _) => is_arithT T
+ | NONE => false)
+
+val abstract =
+ let (* FIXME: provide an option to avoid abstraction of If/distinct/All/Ex *)
+ fun abstr1 cvs ct = abs_arg abstr cvs ct
+ and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
+ and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
+ and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct
+
+ and abstr cvs ct =
+ (case Thm.term_of ct of
+ @{term Trueprop} $ _ => abstr1 cvs ct
+ | @{term "op ==>"} $ _ $ _ => abstr2 cvs ct
+ | @{term True} => pair ct
+ | @{term False} => pair ct
+ | @{term Not} $ _ => abstr1 cvs ct
+ | @{term "op &"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op |"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op -->"} $ _ $ _ => abstr2 cvs ct
+ | Const (@{const_name "op ="}, _) $ _ $ _ => abstr2 cvs ct
+ | Const (@{const_name distinct}, _) $ _ =>
+ abs_arg (abs_list abstr fresh_abstraction) cvs ct
+ | Const (@{const_name If}, _) $ _ $ _ $ _ => abstr3 cvs ct
+ | Const (@{const_name All}, _) $ _ => abstr_abs cvs ct
+ | Const (@{const_name Ex}, _) $ _ => abstr_abs cvs ct
+ | @{term "uminus :: int => _"} $ _ => abstr1 cvs ct
+ | @{term "uminus :: real => _"} $ _ => abstr1 cvs ct
+ | @{term "op + :: int => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op + :: real => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op - :: int => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op - :: real => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op * :: int => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op * :: real => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op div :: int => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op mod :: int => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op / :: real => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op < :: int => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op < :: real => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op <= :: int => _"} $ _ $ _ => abstr2 cvs ct
+ | @{term "op <= :: real => _"} $ _ $ _ => abstr2 cvs ct
+ | Const (@{const_name apply}, _) $ _ $ _ => abstr2 cvs ct
+ | Const (@{const_name fun_upd}, _) $ _ $ _ $ _ => abstr3 cvs ct
+ | t =>
+ if is_atomic t orelse is_number t then pair ct
+ else fresh_abstraction cvs ct)
+ in abstr [] end
+
+fun with_prems thms f ct =
+ fold_rev (Thm.mk_binop @{cterm "op ==>"} o Thm.cprop_of) thms ct
+ |> f
+ |> fold (fn prem => fn th => Thm.implies_elim th prem) thms
+
+in
+
+fun by_abstraction ctxt thms prove = with_prems thms (fn ct =>
+ let val (cu, cx) = abstract ct (abs_context ctxt)
+ in abs_instantiate cx (prove (context_of cx) cu) end)
+
+end
+
+
+
+(* a faster COMP *)
+
+type compose_data = cterm list * (cterm -> cterm list) * thm
+
+fun list2 (x, y) = [x, y]
+
+fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
+fun precompose2 f rule = precompose (list2 o f) rule
+
+fun compose (cvs, f, rule) thm =
+ discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
+
+
+
+(* unfolding of 'distinct' *)
+
+local
+ val set1 = @{lemma "x ~: set [] == ~False" by simp}
+ val set2 = @{lemma "x ~: set [x] == False" by simp}
+ val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
+ val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
+ val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
+
+ fun set_conv ct =
+ (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
+ (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
+
+ val dist1 = @{lemma "distinct [] == ~False" by simp}
+ val dist2 = @{lemma "distinct [x] == ~False" by simp}
+ val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
+ by simp}
+
+ fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
+in
+fun unfold_distinct_conv ct =
+ (More_Conv.rewrs_conv [dist1, dist2] else_conv
+ (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
+end
+
+
+
+(* simpset *)
+
+local
+ val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
+ val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
+ val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
+ val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
+
+ fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
+ fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
+ | dest_binop t = raise TERM ("dest_binop", [t])
+
+ fun prove_antisym_le ss t =
+ let
+ val (le, r, s) = dest_binop t
+ val less = Const (@{const_name less}, Term.fastype_of le)
+ val prems = Simplifier.prems_of_ss ss
+ in
+ (case find_first (eq_prop (le $ s $ r)) prems of
+ NONE =>
+ find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
+ |> Option.map (fn thm => thm RS antisym_less1)
+ | SOME thm => SOME (thm RS antisym_le1))
+ end
+ handle THM _ => NONE
+
+ fun prove_antisym_less ss t =
+ let
+ val (less, r, s) = dest_binop (HOLogic.dest_not t)
+ val le = Const (@{const_name less_eq}, Term.fastype_of less)
+ val prems = prems_of_ss ss
+ in
+ (case find_first (eq_prop (le $ r $ s)) prems of
+ NONE =>
+ find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
+ |> Option.map (fn thm => thm RS antisym_less2)
+ | SOME thm => SOME (thm RS antisym_le2))
+ end
+ handle THM _ => NONE
+in
+
+fun make_simpset ctxt rules = Simplifier.context ctxt (HOL_ss
+ addsimps @{thms ring_distribs} addsimps @{thms field_simps}
+ addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
+ addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
+ addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}
+ addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
+ addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
+ addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
+ addsimps @{thms array_rules}
+ addsimprocs [
+ Simplifier.simproc @{theory} "fast_int_arith" [
+ "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
+ Simplifier.simproc @{theory} "fast_real_arith" [
+ "(m::real) < n", "(m::real) <= n", "(m::real) = n"]
+ (K Lin_Arith.simproc),
+ Simplifier.simproc @{theory} "antisym_le" ["(x::'a::order) <= y"]
+ (K prove_antisym_le),
+ Simplifier.simproc @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
+ (K prove_antisym_less)]
+ addsimps rules)
+
+end
+
+end
--- a/src/HOL/SMT/Tools/z3_solver.ML Wed May 12 23:53:58 2010 +0200
+++ b/src/HOL/SMT/Tools/z3_solver.ML Wed May 12 23:53:59 2010 +0200
@@ -63,7 +63,7 @@
fun prover ({context, output, recon} : SMT_Solver.proof_data) =
check_unsat recon output
- |> Z3_Proof.reconstruct context recon
+ |> Z3_Proof_Reconstruction.reconstruct context recon
fun solver oracle ctxt =
let val with_proof = Config.get ctxt proofs
--- a/src/HOL/SMT/Z3.thy Wed May 12 23:53:58 2010 +0200
+++ b/src/HOL/SMT/Z3.thy Wed May 12 23:53:59 2010 +0200
@@ -7,35 +7,70 @@
theory Z3
imports SMT_Base "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
uses
- "Tools/z3_proof_terms.ML"
- "Tools/z3_proof_rules.ML"
- "Tools/z3_proof.ML"
+ "Tools/z3_proof_parser.ML"
+ "Tools/z3_proof_tools.ML"
+ "Tools/z3_proof_literals.ML"
+ "Tools/z3_proof_reconstruction.ML"
"Tools/z3_model.ML"
"Tools/z3_interface.ML"
"Tools/z3_solver.ML"
begin
setup {*
- Z3_Proof_Rules.setup #>
+ Z3_Proof_Reconstruction.setup #>
Z3_Solver.setup #>
Arith_Data.add_tactic "Ferrante-Rackoff" (K FerranteRackoff.dlo_tac)
*}
-lemmas [z3_rewrite] =
+lemmas [z3_rule] =
refl eq_commute conj_commute disj_commute simp_thms nnf_simps
- ring_distribs field_simps times_divide_eq_right times_divide_eq_left if_True if_False
+ ring_distribs field_simps times_divide_eq_right times_divide_eq_left
+ if_True if_False not_not
+
+lemma [z3_rule]:
+ "(P \<longrightarrow> Q) = (Q \<or> \<not>P)"
+ "(\<not>P \<longrightarrow> Q) = (P \<or> Q)"
+ "(\<not>P \<longrightarrow> Q) = (Q \<or> P)"
+ by auto
-lemma [z3_rewrite]: "(P \<noteq> Q) = (Q = (\<not>P))" by fast
+lemma [z3_rule]:
+ "((P = Q) \<longrightarrow> R) = (R | (Q = (\<not>P)))"
+ by auto
+
+lemma [z3_rule]:
+ "((\<not>P) = P) = False"
+ "(P = (\<not>P)) = False"
+ "(P \<noteq> Q) = (Q = (\<not>P))"
+ "(P = Q) = ((\<not>P \<or> Q) \<and> (P \<or> \<not>Q))"
+ "(P \<noteq> Q) = ((\<not>P \<or> \<not>Q) \<and> (P \<or> Q))"
+ by auto
-lemma [z3_rewrite]: "(\<not>False \<longrightarrow> P) = P" by fast
-lemma [z3_rewrite]: "(P \<longrightarrow> Q) = (Q \<or> \<not>P)" by fast
-lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (P \<or> Q)" by fast
-lemma [z3_rewrite]: "(\<not>P \<longrightarrow> Q) = (Q \<or> P)" by fast
+lemma [z3_rule]:
+ "(if P then P else \<not>P) = True"
+ "(if \<not>P then \<not>P else P) = True"
+ "(if P then True else False) = P"
+ "(if P then False else True) = (\<not>P)"
+ "(if \<not>P then x else y) = (if P then y else x)"
+ by auto
-lemma [z3_rewrite]: "(if P then True else False) = P" by simp
-lemma [z3_rewrite]: "(if P then False else True) = (\<not>P)" by simp
+lemma [z3_rule]:
+ "P = Q \<or> P \<or> Q"
+ "P = Q \<or> \<not>P \<or> \<not>Q"
+ "(\<not>P) = Q \<or> \<not>P \<or> Q"
+ "(\<not>P) = Q \<or> P \<or> \<not>Q"
+ "P = (\<not>Q) \<or> \<not>P \<or> Q"
+ "P = (\<not>Q) \<or> P \<or> \<not>Q"
+ "P \<noteq> Q \<or> P \<or> \<not>Q"
+ "P \<noteq> Q \<or> \<not>P \<or> Q"
+ "P \<noteq> (\<not>Q) \<or> P \<or> Q"
+ "(\<not>P) \<noteq> Q \<or> P \<or> Q"
+ "P \<or> Q \<or> P \<noteq> (\<not>Q)"
+ "P \<or> Q \<or> (\<not>P) \<noteq> Q"
+ "P \<or> \<not>Q \<or> P \<noteq> Q"
+ "\<not>P \<or> Q \<or> P \<noteq> Q"
+ by auto
-lemma [z3_rewrite]:
+lemma [z3_rule]:
"0 + (x::int) = x"
"x + 0 = x"
"0 * x = 0"
@@ -43,7 +78,7 @@
"x + y = y + x"
by auto
-lemma [z3_rewrite]:
+lemma [z3_rule]:
"0 + (x::real) = x"
"x + 0 = x"
"0 * x = 0"