blanchet@58058: (*  Title:      HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
boehmes@36898:     Author:     Sascha Boehme, TU Muenchen
boehmes@36898: 
boehmes@36898: Proof reconstruction for proofs found by Z3.
boehmes@36898: *)
boehmes@36898: 
blanchet@58058: signature OLD_Z3_PROOF_RECONSTRUCTION =
boehmes@36898: sig
boehmes@36899:   val add_z3_rule: thm -> Context.generic -> Context.generic
blanchet@58058:   val reconstruct: Proof.context -> Old_SMT_Translate.recon -> string list -> int list * thm
boehmes@36898: end
boehmes@36898: 
blanchet@58058: structure Old_Z3_Proof_Reconstruction: OLD_Z3_PROOF_RECONSTRUCTION =
boehmes@36898: struct
boehmes@36898: 
boehmes@36898: 
blanchet@58058: fun z3_exn msg = raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure
boehmes@40162:   ("Z3 proof reconstruction: " ^ msg))
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
boehmes@41130: (* net of schematic rules *)
boehmes@36898: 
boehmes@36898: local
boehmes@36898:   val description = "declaration of Z3 proof rules"
boehmes@36898: 
boehmes@36898:   val eq = Thm.eq_thm
boehmes@36898: 
blanchet@58058:   structure Old_Z3_Rules = Generic_Data
boehmes@36898:   (
boehmes@36898:     type T = thm Net.net
boehmes@36898:     val empty = Net.empty
boehmes@36898:     val extend = I
boehmes@36898:     val merge = Net.merge eq
boehmes@36898:   )
boehmes@36898: 
wenzelm@54742:   fun prep context =
blanchet@58058:     `Thm.prop_of o rewrite_rule (Context.proof_of context) [Old_Z3_Proof_Literals.rewrite_true]
boehmes@36898: 
wenzelm@54742:   fun ins thm context =
blanchet@58058:     context |> Old_Z3_Rules.map (fn net => Net.insert_term eq (prep context thm) net handle Net.INSERT => net)
wenzelm@54742:   fun rem thm context =
blanchet@58058:     context |> Old_Z3_Rules.map (fn net => Net.delete_term eq (prep context thm) net handle Net.DELETE => net)
boehmes@36898: 
wenzelm@54742:   val add = Thm.declaration_attribute ins
wenzelm@54742:   val del = Thm.declaration_attribute rem
boehmes@36898: in
boehmes@36898: 
wenzelm@54742: val add_z3_rule = ins
boehmes@36898: 
boehmes@36898: fun by_schematic_rule ctxt ct =
blanchet@58058:   the (Old_Z3_Proof_Tools.net_instance (Old_Z3_Rules.get (Context.Proof ctxt)) ct)
boehmes@36898: 
wenzelm@57957: val _ = Theory.setup
blanchet@58059:  (Attrib.setup @{binding old_z3_rule} (Attrib.add_del add del) description #>
blanchet@58059:   Global_Theory.add_thms_dynamic (@{binding old_z3_rule}, Net.content o Old_Z3_Rules.get))
boehmes@36898: 
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
boehmes@41130: (* proof tools *)
boehmes@36898: 
boehmes@36898: fun named ctxt name prover ct =
blanchet@58058:   let val _ = Old_SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
boehmes@36898:   in prover ct end
boehmes@36898: 
boehmes@36898: fun NAMED ctxt name tac i st =
blanchet@58058:   let val _ = Old_SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
boehmes@36898:   in tac i st end
boehmes@36898: 
boehmes@36898: fun pretty_goal ctxt thms t =
boehmes@36898:   [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
boehmes@36898:   |> not (null thms) ? cons (Pretty.big_list "assumptions:"
boehmes@36898:        (map (Display.pretty_thm ctxt) thms))
boehmes@36898: 
boehmes@36898: fun try_apply ctxt thms =
boehmes@36898:   let
boehmes@36898:     fun try_apply_err ct = Pretty.string_of (Pretty.chunks [
boehmes@36898:       Pretty.big_list ("Z3 found a proof," ^
boehmes@36898:         " but proof reconstruction failed at the following subgoal:")
boehmes@36898:         (pretty_goal ctxt thms (Thm.term_of ct)),
blanchet@58059:       Pretty.str ("Declaring a rule as [old_z3_rule] might solve this problem.")])
boehmes@36898: 
boehmes@36898:     fun apply [] ct = error (try_apply_err ct)
boehmes@36898:       | apply (prover :: provers) ct =
boehmes@36898:           (case try prover ct of
blanchet@58058:             SOME thm => (Old_SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
boehmes@36898:           | NONE => apply provers ct)
boehmes@36898: 
boehmes@43893:     fun schematic_label full = "schematic rules" |> full ? suffix " (full)"
boehmes@43893:     fun schematic ctxt full ct =
boehmes@43893:       ct
boehmes@43893:       |> full ? fold_rev (curry Drule.mk_implies o Thm.cprop_of) thms
boehmes@43893:       |> named ctxt (schematic_label full) (by_schematic_rule ctxt)
boehmes@43893:       |> fold Thm.elim_implies thms
boehmes@43893: 
boehmes@43893:   in apply o cons (schematic ctxt false) o cons (schematic ctxt true) end
boehmes@36898: 
boehmes@36899: local
boehmes@36899:   val rewr_if =
boehmes@36899:     @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
boehmes@36899: in
wenzelm@42793: 
wenzelm@42793: fun HOL_fast_tac ctxt =
wenzelm@42793:   Classical.fast_tac (put_claset HOL_cs ctxt)
wenzelm@42793: 
wenzelm@42793: fun simp_fast_tac ctxt =
wenzelm@51717:   Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [rewr_if])
wenzelm@42793:   THEN_ALL_NEW HOL_fast_tac ctxt
wenzelm@42793: 
boehmes@36899: end
boehmes@36899: 
boehmes@36898: 
boehmes@36898: 
boehmes@41130: (* theorems and proofs *)
boehmes@36898: 
boehmes@41130: (** theorem incarnations **)
boehmes@36898: 
boehmes@36898: datatype theorem =
boehmes@36898:   Thm of thm | (* theorem without special features *)
boehmes@36898:   MetaEq of thm | (* meta equality "t == s" *)
blanchet@58058:   Literals of thm * Old_Z3_Proof_Literals.littab
boehmes@36898:     (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *)
boehmes@36898: 
boehmes@36898: fun thm_of (Thm thm) = thm
boehmes@36898:   | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq}
boehmes@36898:   | thm_of (Literals (thm, _)) = thm
boehmes@36898: 
boehmes@36898: fun meta_eq_of (MetaEq thm) = thm
boehmes@36898:   | meta_eq_of p = mk_meta_eq (thm_of p)
boehmes@36898: 
boehmes@36898: fun literals_of (Literals (_, lits)) = lits
blanchet@58058:   | literals_of p = Old_Z3_Proof_Literals.make_littab [thm_of p]
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (** core proof rules **)
boehmes@36898: 
boehmes@36898: (* assumption *)
boehmes@41131: 
boehmes@36898: local
blanchet@58057:   val remove_trigger = mk_meta_eq @{thm trigger_def}
blanchet@58057:   val remove_weight = mk_meta_eq @{thm weight_def}
blanchet@58057:   val remove_fun_app = mk_meta_eq @{thm fun_app_def}
boehmes@36898: 
boehmes@44488:   fun rewrite_conv _ [] = Conv.all_conv
wenzelm@51717:     | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
boehmes@36898: 
boehmes@41131:   val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
blanchet@58058:     remove_fun_app, Old_Z3_Proof_Literals.rewrite_true]
boehmes@41131: 
boehmes@44488:   fun rewrite _ [] = I
boehmes@44488:     | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
boehmes@36898: 
boehmes@41131:   fun lookup_assm assms_net ct =
blanchet@58058:     Old_Z3_Proof_Tools.net_instances assms_net ct
boehmes@45393:     |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
boehmes@36898: in
boehmes@41131: 
boehmes@41131: fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt =
boehmes@36898:   let
blanchet@58058:     val eqs = map (rewrite ctxt [Old_Z3_Proof_Literals.rewrite_true]) rewrite_rules
boehmes@41131:     val eqs' = union Thm.eq_thm eqs prep_rules
boehmes@41131: 
boehmes@41131:     val assms_net =
boehmes@41127:       assms
boehmes@41131:       |> map (apsnd (rewrite ctxt eqs'))
boehmes@41127:       |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
blanchet@58058:       |> Old_Z3_Proof_Tools.thm_net_of snd 
boehmes@41131: 
boehmes@41131:     fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
boehmes@41131: 
boehmes@41131:     fun assume thm ctxt =
boehmes@41131:       let
boehmes@41131:         val ct = Thm.cprem_of thm 1
boehmes@41131:         val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt
boehmes@41131:       in (Thm.implies_elim thm thm', ctxt') end
boehmes@36898: 
boehmes@45393:     fun add1 idx thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) =
boehmes@45393:       let
boehmes@45393:         val (thm, ctxt') =
boehmes@45393:           if exact then (Thm.implies_elim thm1 th, ctxt)
boehmes@45393:           else assume thm1 ctxt
boehmes@45393:         val thms' = if exact then thms else th :: thms
boehmes@45393:       in 
boehmes@45393:         ((insert (op =) i is, thms'),
boehmes@45393:           (ctxt', Inttab.update (idx, Thm thm) ptab))
boehmes@45393:       end
boehmes@45393: 
boehmes@45393:     fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) =
boehmes@41131:       let
boehmes@41131:         val thm1 = 
boehmes@41131:           Thm.trivial ct
boehmes@41131:           |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
boehmes@41131:         val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
boehmes@41131:       in
boehmes@41131:         (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
boehmes@45393:           [] =>
boehmes@41131:             let val (thm, ctxt') = assume thm1 ctxt
boehmes@41131:             in ((is, thms), (ctxt', Inttab.update (idx, Thm thm) ptab)) end
boehmes@45393:         | ithms => fold (add1 idx thm1) ithms cx)
boehmes@41131:       end
boehmes@41131:   in fold add asserted (([], []), (ctxt, Inttab.empty)) end
boehmes@40164: 
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* P = Q ==> P ==> Q   or   P --> Q ==> P ==> Q *)
boehmes@36898: local
blanchet@58058:   val precomp = Old_Z3_Proof_Tools.precompose2
blanchet@58058:   val comp = Old_Z3_Proof_Tools.compose
boehmes@36898: 
boehmes@41328:   val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
boehmes@41328:   val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1
boehmes@41328: 
boehmes@41328:   val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
boehmes@41328:   val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
boehmes@36898: in
boehmes@41328: fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
boehmes@36898:   | mp p_q p = 
boehmes@36898:       let
boehmes@36898:         val pq = thm_of p_q
boehmes@41328:         val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
boehmes@36898:       in Thm (Thm.implies_elim thm p) end
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* and_elim:     P1 & ... & Pn ==> Pi *)
boehmes@36898: (* not_or_elim:  ~(P1 | ... | Pn) ==> ~Pi *)
boehmes@36898: local
blanchet@58058:   fun is_sublit conj t = Old_Z3_Proof_Literals.exists_lit conj (fn u => u aconv t)
boehmes@36898: 
boehmes@36898:   fun derive conj t lits idx ptab =
boehmes@36898:     let
blanchet@58058:       val lit = the (Old_Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits)
blanchet@58058:       val ls = Old_Z3_Proof_Literals.explode conj false false [t] lit
blanchet@58058:       val lits' = fold Old_Z3_Proof_Literals.insert_lit ls
blanchet@58058:         (Old_Z3_Proof_Literals.delete_lit lit lits)
boehmes@36898: 
boehmes@41130:       fun upd thm = Literals (thm_of thm, lits')
boehmes@41328:       val ptab' = Inttab.map_entry idx upd ptab
blanchet@58058:     in (the (Old_Z3_Proof_Literals.lookup_lit lits' t), ptab') end
boehmes@36898: 
boehmes@36898:   fun lit_elim conj (p, idx) ct ptab =
boehmes@36898:     let val lits = literals_of p
boehmes@36898:     in
blanchet@58058:       (case Old_Z3_Proof_Literals.lookup_lit lits (Old_SMT_Utils.term_of ct) of
boehmes@36898:         SOME lit => (Thm lit, ptab)
blanchet@58058:       | NONE => apfst Thm (derive conj (Old_SMT_Utils.term_of ct) lits idx ptab))
boehmes@36898:     end
boehmes@36898: in
boehmes@36898: val and_elim = lit_elim true
boehmes@36898: val not_or_elim = lit_elim false
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *)
boehmes@36898: local
boehmes@36898:   fun step lit thm =
boehmes@36898:     Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
blanchet@58058:   val explode_disj = Old_Z3_Proof_Literals.explode false false false
boehmes@36898:   fun intro hyps thm th = fold step (explode_disj hyps th) thm
boehmes@36898: 
boehmes@36898:   fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
blanchet@58058:   val ccontr = Old_Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr}
boehmes@36898: in
boehmes@36898: fun lemma thm ct =
boehmes@36898:   let
blanchet@58058:     val cu = Old_Z3_Proof_Literals.negate (Thm.dest_arg ct)
wenzelm@44058:     val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm)
blanchet@58058:     val th = Old_Z3_Proof_Tools.under_assumption (intro hyps thm) cu
blanchet@58058:   in Thm (Old_Z3_Proof_Tools.compose ccontr th) end
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
boehmes@36898: local
blanchet@58058:   val explode_disj = Old_Z3_Proof_Literals.explode false true false
blanchet@58058:   val join_disj = Old_Z3_Proof_Literals.join false
boehmes@36898:   fun unit thm thms th =
boehmes@41328:     let
blanchet@58058:       val t = @{const Not} $ Old_SMT_Utils.prop_of thm
blanchet@58058:       val ts = map Old_SMT_Utils.prop_of thms
boehmes@41328:     in
blanchet@58058:       join_disj (Old_Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t
boehmes@41328:     end
boehmes@36898: 
boehmes@36898:   fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
boehmes@36898:   fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
boehmes@41328:   val contrapos =
blanchet@58058:     Old_Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
boehmes@36898: in
boehmes@36898: fun unit_resolution thm thms ct =
blanchet@58058:   Old_Z3_Proof_Literals.negate (Thm.dest_arg ct)
blanchet@58058:   |> Old_Z3_Proof_Tools.under_assumption (unit thm thms)
blanchet@58058:   |> Thm o Old_Z3_Proof_Tools.discharge thm o Old_Z3_Proof_Tools.compose contrapos
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* P ==> P == True   or   P ==> P == False *)
boehmes@36898: local
boehmes@36898:   val iff1 = @{lemma "P ==> P == (~ False)" by simp}
boehmes@36898:   val iff2 = @{lemma "~P ==> P == False" by simp}
boehmes@36898: in
boehmes@36898: fun iff_true thm = MetaEq (thm COMP iff1)
boehmes@36898: fun iff_false thm = MetaEq (thm COMP iff2)
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* distributivity of | over & *)
boehmes@36898: fun distributivity ctxt = Thm o try_apply ctxt [] [
blanchet@58058:   named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
boehmes@36898:     (* FIXME: not very well tested *)
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* Tseitin-like axioms *)
boehmes@36898: local
boehmes@36898:   val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
boehmes@36898:   val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
boehmes@36898:   val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast}
boehmes@36898:   val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
boehmes@36898: 
boehmes@36898:   fun prove' conj1 conj2 ct2 thm =
boehmes@41328:     let
boehmes@41328:       val littab =
blanchet@58058:         Old_Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm
blanchet@58058:         |> cons Old_Z3_Proof_Literals.true_thm
blanchet@58058:         |> Old_Z3_Proof_Literals.make_littab
blanchet@58058:     in Old_Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end
boehmes@36898: 
boehmes@36898:   fun prove rule (ct1, conj1) (ct2, conj2) =
blanchet@58058:     Old_Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
boehmes@36898: 
boehmes@36898:   fun prove_def_axiom ct =
boehmes@36898:     let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
boehmes@36898:     in
boehmes@36898:       (case Thm.term_of ct1 of
boehmes@40579:         @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
boehmes@36898:           prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
boehmes@40579:       | @{const HOL.conj} $ _ $ _ =>
blanchet@58058:           prove disjI3 (Old_Z3_Proof_Literals.negate ct2, false) (ct1, true)
boehmes@40579:       | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
blanchet@58058:           prove disjI3 (Old_Z3_Proof_Literals.negate ct2, false) (ct1, false)
boehmes@40579:       | @{const HOL.disj} $ _ $ _ =>
blanchet@58058:           prove disjI2 (Old_Z3_Proof_Literals.negate ct1, false) (ct2, true)
boehmes@40681:       | Const (@{const_name distinct}, _) $ _ =>
boehmes@36898:           let
boehmes@36898:             fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
blanchet@58058:             val unfold_dis_conv = dis_conv Old_Z3_Proof_Tools.unfold_distinct_conv
boehmes@36898:             fun prv cu =
boehmes@36898:               let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
boehmes@36898:               in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
blanchet@58058:           in Old_Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
boehmes@40681:       | @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
boehmes@36898:           let
boehmes@36898:             fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
blanchet@58058:             val unfold_dis_conv = dis_conv Old_Z3_Proof_Tools.unfold_distinct_conv
boehmes@36898:             fun prv cu =
boehmes@36898:               let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
boehmes@36898:               in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
blanchet@58058:           in Old_Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
boehmes@36898:       | _ => raise CTERM ("prove_def_axiom", [ct]))
boehmes@36898:     end
boehmes@36898: in
boehmes@36898: fun def_axiom ctxt = Thm o try_apply ctxt [] [
boehmes@36898:   named ctxt "conj/disj/distinct" prove_def_axiom,
blanchet@58058:   Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
blanchet@58058:     named ctxt' "simp+fast" (Old_Z3_Proof_Tools.by_tac ctxt (simp_fast_tac ctxt')))]
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* local definitions *)
boehmes@36898: local
boehmes@36898:   val intro_rules = [
boehmes@36898:     @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp},
boehmes@36898:     @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)"
boehmes@36898:       by simp},
boehmes@36898:     @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ]
boehmes@36898: 
boehmes@36898:   val apply_rules = [
boehmes@36898:     @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast},
boehmes@36898:     @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
nipkow@44890:       by (atomize(full)) fastforce} ]
boehmes@36898: 
blanchet@58058:   val inst_rule = Old_Z3_Proof_Tools.match_instantiate Thm.dest_arg
boehmes@36898: 
boehmes@36898:   fun apply_rule ct =
boehmes@36898:     (case get_first (try (inst_rule ct)) intro_rules of
boehmes@36898:       SOME thm => thm
boehmes@36898:     | NONE => raise CTERM ("intro_def", [ct]))
boehmes@36898: in
blanchet@58058: fun intro_def ct = Old_Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm
boehmes@36898: 
boehmes@36898: fun apply_def thm =
boehmes@36898:   get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
boehmes@36898:   |> the_default (Thm thm)
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* negation normal form *)
boehmes@36898: local
boehmes@36898:   val quant_rules1 = ([
boehmes@36898:     @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp},
boehmes@36898:     @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [
boehmes@36898:     @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp},
boehmes@36898:     @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}])
boehmes@36898: 
boehmes@36898:   val quant_rules2 = ([
boehmes@36898:     @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp},
boehmes@36898:     @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [
boehmes@36898:     @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
boehmes@36898:     @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
boehmes@36898: 
boehmes@36898:   fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
wenzelm@52732:     rtac thm ORELSE'
wenzelm@52732:     (match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
wenzelm@52732:     (match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
boehmes@36898: 
boehmes@41328:   fun nnf_quant_tac_varified vars eq =
blanchet@58058:     nnf_quant_tac (Old_Z3_Proof_Tools.varify vars eq)
boehmes@41328: 
wenzelm@54883:   fun nnf_quant ctxt vars qs p ct =
blanchet@58058:     Old_Z3_Proof_Tools.as_meta_eq ct
blanchet@58058:     |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified vars (meta_eq_of p) qs)
boehmes@36898: 
boehmes@36898:   fun prove_nnf ctxt = try_apply ctxt [] [
blanchet@58058:     named ctxt "conj/disj" Old_Z3_Proof_Literals.prove_conj_disj_eq,
blanchet@58058:     Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
blanchet@58058:       named ctxt' "simp+fast" (Old_Z3_Proof_Tools.by_tac ctxt' (simp_fast_tac ctxt')))]
boehmes@36898: in
boehmes@36898: fun nnf ctxt vars ps ct =
blanchet@58058:   (case Old_SMT_Utils.term_of ct of
boehmes@36898:     _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
boehmes@36898:       if l aconv r
boehmes@36898:       then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
wenzelm@54883:       else MetaEq (nnf_quant ctxt vars quant_rules1 (hd ps) ct)
boehmes@40579:   | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
wenzelm@54883:       MetaEq (nnf_quant ctxt vars quant_rules2 (hd ps) ct)
boehmes@36898:   | _ =>
boehmes@36898:       let
boehmes@36898:         val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
blanchet@58058:           (Old_Z3_Proof_Tools.unfold_eqs ctxt
boehmes@41328:             (map (Thm.symmetric o meta_eq_of) ps)))
blanchet@58058:       in Thm (Old_Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (** equality proof rules **)
boehmes@36898: 
boehmes@36898: (* |- t = t *)
boehmes@36898: fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* s = t ==> t = s *)
boehmes@36898: local
boehmes@36898:   val symm_rule = @{lemma "s = t ==> t == s" by simp}
boehmes@36898: in
boehmes@36898: fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm)
boehmes@36898:   | symm p = MetaEq (thm_of p COMP symm_rule)
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* s = t ==> t = u ==> s = u *)
boehmes@36898: local
boehmes@36898:   val trans1 = @{lemma "s == t ==> t =  u ==> s == u" by simp}
boehmes@36898:   val trans2 = @{lemma "s =  t ==> t == u ==> s == u" by simp}
boehmes@36898:   val trans3 = @{lemma "s =  t ==> t =  u ==> s == u" by simp}
boehmes@36898: in
boehmes@36898: fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2)
boehmes@36898:   | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1))
boehmes@36898:   | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2))
boehmes@36898:   | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3))
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn
boehmes@36898:    (reflexive antecendents are droppped) *)
boehmes@36898: local
boehmes@36898:   exception MONO
boehmes@36898: 
boehmes@36898:   fun prove_refl (ct, _) = Thm.reflexive ct
boehmes@36898:   fun prove_comb f g cp =
boehmes@36898:     let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp
boehmes@36898:     in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
boehmes@36898:   fun prove_arg f = prove_comb prove_refl f
boehmes@36898: 
boehmes@36898:   fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp
boehmes@36898: 
boehmes@36898:   fun prove_nary is_comb f =
boehmes@36898:     let
boehmes@36898:       fun prove (cp as (ct, _)) = f cp handle MONO =>
boehmes@36898:         if is_comb (Thm.term_of ct)
boehmes@36898:         then prove_comb (prove_arg prove) prove cp
boehmes@36898:         else prove_refl cp
boehmes@36898:     in prove end
boehmes@36898: 
boehmes@36898:   fun prove_list f n cp =
boehmes@36898:     if n = 0 then prove_refl cp
boehmes@36898:     else prove_comb (prove_arg f) (prove_list f (n-1)) cp
boehmes@36898: 
boehmes@36898:   fun with_length f (cp as (cl, _)) =
boehmes@36898:     f (length (HOLogic.dest_list (Thm.term_of cl))) cp
boehmes@36898: 
boehmes@36898:   fun prove_distinct f = prove_arg (with_length (prove_list f))
boehmes@36898: 
boehmes@36898:   fun prove_eq exn lookup cp =
boehmes@36898:     (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of
boehmes@36898:       SOME eq => eq
boehmes@36898:     | NONE => if exn then raise MONO else prove_refl cp)
boehmes@36898:   
boehmes@41328:   val prove_exn = prove_eq true
boehmes@41328:   and prove_safe = prove_eq false
boehmes@36898: 
boehmes@36898:   fun mono f (cp as (cl, _)) =
boehmes@36898:     (case Term.head_of (Thm.term_of cl) of
blanchet@58058:       @{const HOL.conj} => prove_nary Old_Z3_Proof_Literals.is_conj (prove_exn f)
blanchet@58058:     | @{const HOL.disj} => prove_nary Old_Z3_Proof_Literals.is_disj (prove_exn f)
boehmes@41328:     | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f)
boehmes@41328:     | _ => prove (prove_safe f)) cp
boehmes@36898: in
boehmes@36898: fun monotonicity eqs ct =
boehmes@36898:   let
boehmes@40680:     fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)]
boehmes@40680:     val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs
boehmes@40680:     val lookup = AList.lookup (op aconv) teqs
boehmes@36898:     val cp = Thm.dest_binop (Thm.dest_arg ct)
boehmes@41328:   in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* |- f a b = f b a (where f is equality) *)
boehmes@36898: local
boehmes@36898:   val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
boehmes@36898: in
boehmes@41328: fun commutativity ct =
blanchet@58058:   MetaEq (Old_Z3_Proof_Tools.match_instantiate I
blanchet@58058:     (Old_Z3_Proof_Tools.as_meta_eq ct) rule)
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (** quantifier proof rules **)
boehmes@36898: 
boehmes@36898: (* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x)
boehmes@36898:    P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x)    *)
boehmes@36898: local
boehmes@36898:   val rules = [
boehmes@36898:     @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp},
boehmes@36898:     @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}]
boehmes@36898: in
wenzelm@54883: fun quant_intro ctxt vars p ct =
boehmes@36898:   let
boehmes@36898:     val thm = meta_eq_of p
blanchet@58058:     val rules' = Old_Z3_Proof_Tools.varify vars thm :: rules
blanchet@58058:     val cu = Old_Z3_Proof_Tools.as_meta_eq ct
wenzelm@52732:     val tac = REPEAT_ALL_NEW (match_tac rules')
blanchet@58058:   in MetaEq (Old_Z3_Proof_Tools.by_tac ctxt tac cu) end
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
boehmes@36898: fun pull_quant ctxt = Thm o try_apply ctxt [] [
blanchet@58058:   named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
boehmes@36898:     (* FIXME: not very well tested *)
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
boehmes@36898: fun push_quant ctxt = Thm o try_apply ctxt [] [
blanchet@58058:   named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
boehmes@36898:     (* FIXME: not very well tested *)
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *)
boehmes@36898: local
boehmes@42318:   val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
boehmes@42318:   val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
boehmes@36898: 
boehmes@42318:   fun elim_unused_tac i st = (
wenzelm@52732:     match_tac [@{thm refl}]
wenzelm@52732:     ORELSE' (match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
boehmes@42318:     ORELSE' (
wenzelm@52732:       match_tac [@{thm iff_allI}, @{thm iff_exI}]
boehmes@42318:       THEN' elim_unused_tac)) i st
boehmes@36898: in
boehmes@42318: 
blanchet@58058: fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt elim_unused_tac
boehmes@42318: 
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
boehmes@36898: fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
blanchet@58058:   named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
boehmes@36898:     (* FIXME: not very well tested *)
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* |- ~(ALL x1...xn. P x1...xn) | P a1...an *)
boehmes@36898: local
boehmes@36898:   val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
boehmes@36898: in
blanchet@58058: fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (
wenzelm@52732:   REPEAT_ALL_NEW (match_tac [rule])
wenzelm@52732:   THEN' rtac @{thm excluded_middle})
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@42196: (* |- (EX x. P x) = P c     |- ~(ALL x. P x) = ~ P c *)
boehmes@36898: local
boehmes@42191:   val forall =
blanchet@58058:     Old_SMT_Utils.mk_const_pat @{theory} @{const_name Pure.all}
blanchet@58058:       (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1)
boehmes@42191:   fun mk_forall cv ct =
blanchet@58058:     Thm.apply (Old_SMT_Utils.instT' cv forall) (Thm.lambda cv ct)
boehmes@36898: 
boehmes@42191:   fun get_vars f mk pred ctxt t =
boehmes@42191:     Term.fold_aterms f t []
boehmes@42191:     |> map_filter (fn v =>
blanchet@58058:          if pred v then SOME (Old_SMT_Utils.certify ctxt (mk v)) else NONE)
boehmes@36898: 
boehmes@42191:   fun close vars f ct ctxt =
boehmes@42191:     let
boehmes@42191:       val frees_of = get_vars Term.add_frees Free (member (op =) vars o fst)
boehmes@42191:       val vs = frees_of ctxt (Thm.term_of ct)
boehmes@42191:       val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt
boehmes@42191:       val vars_of = get_vars Term.add_vars Var (K true) ctxt'
boehmes@42191:     in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
boehmes@36898: 
boehmes@42191:   val sk_rules = @{lemma
boehmes@44488:     "c = (SOME x. P x) ==> (EX x. P x) = P c"
boehmes@44488:     "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)"
boehmes@42191:     by (metis someI_ex)+}
boehmes@36898: in
boehmes@42191: 
boehmes@42191: fun skolemize vars =
boehmes@42191:   apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
boehmes@42191: 
boehmes@42191: fun discharge_sk_tac i st = (
wenzelm@52732:   rtac @{thm trans} i
wenzelm@52732:   THEN resolve_tac sk_rules i
wenzelm@52732:   THEN (rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
wenzelm@52732:   THEN rtac @{thm refl} i) st
boehmes@42191: 
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@42191: 
boehmes@36898: (** theory proof rules **)
boehmes@36898: 
boehmes@36898: (* theory lemmas: linear arithmetic, arrays *)
boehmes@36898: fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
blanchet@58058:   Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' =>
blanchet@58058:     Old_Z3_Proof_Tools.by_tac ctxt' (
boehmes@41328:       NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
boehmes@41328:       ORELSE' NAMED ctxt' "simp+arith" (
wenzelm@51717:         Simplifier.asm_full_simp_tac (put_simpset simpset ctxt')
boehmes@41328:         THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
boehmes@36898: 
boehmes@36898: 
boehmes@36898: (* rewriting: prove equalities:
boehmes@36898:      * ACI of conjunction/disjunction
boehmes@36898:      * contradiction, excluded middle
boehmes@36898:      * logical rewriting rules (for negation, implication, equivalence,
boehmes@36898:          distinct)
boehmes@36898:      * normal forms for polynoms (integer/real arithmetic)
boehmes@36898:      * quantifier elimination over linear arithmetic
boehmes@36898:      * ... ? **)
boehmes@36898: local
boehmes@36898:   fun spec_meta_eq_of thm =
boehmes@36898:     (case try (fn th => th RS @{thm spec}) thm of
boehmes@36898:       SOME thm' => spec_meta_eq_of thm'
boehmes@36898:     | NONE => mk_meta_eq thm)
boehmes@36898: 
boehmes@36898:   fun prep (Thm thm) = spec_meta_eq_of thm
boehmes@36898:     | prep (MetaEq thm) = thm
boehmes@36898:     | prep (Literals (thm, _)) = spec_meta_eq_of thm
boehmes@36898: 
boehmes@36898:   fun unfold_conv ctxt ths =
blanchet@58058:     Conv.arg_conv (Conv.binop_conv (Old_Z3_Proof_Tools.unfold_eqs ctxt
boehmes@41328:       (map prep ths)))
boehmes@36898: 
boehmes@36898:   fun with_conv _ [] prv = prv
boehmes@41328:     | with_conv ctxt ths prv =
blanchet@58058:         Old_Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv
boehmes@36898: 
boehmes@36898:   val unfold_conv =
boehmes@41328:     Conv.arg_conv (Conv.binop_conv
blanchet@58058:       (Conv.try_conv Old_Z3_Proof_Tools.unfold_distinct_conv))
boehmes@41328:   val prove_conj_disj_eq =
blanchet@58058:     Old_Z3_Proof_Tools.with_conv unfold_conv Old_Z3_Proof_Literals.prove_conj_disj_eq
boehmes@40663: 
boehmes@41899:   fun declare_hyps ctxt thm =
boehmes@41899:     (thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt))
boehmes@36898: in
boehmes@36898: 
boehmes@42992: val abstraction_depth = 3
boehmes@42992:   (*
boehmes@42992:     This value was chosen large enough to potentially catch exceptions,
boehmes@42992:     yet small enough to not cause too much harm.  The value might be
boehmes@42992:     increased in the future, if reconstructing 'rewrite' fails on problems
boehmes@42992:     that get too much abstracted to be reconstructable.
boehmes@42992:   *)
boehmes@42992: 
boehmes@40663: fun rewrite simpset ths ct ctxt =
boehmes@41899:   apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [
boehmes@40663:     named ctxt "conj/disj/distinct" prove_conj_disj_eq,
blanchet@58058:     named ctxt "pull-ite" Old_Z3_Proof_Methods.prove_ite ctxt,
blanchet@58058:     Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
blanchet@58058:       Old_Z3_Proof_Tools.by_tac ctxt' (
wenzelm@51717:         NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
wenzelm@42793:         THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
blanchet@58058:     Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
blanchet@58058:       Old_Z3_Proof_Tools.by_tac ctxt' (
wenzelm@52732:         (rtac @{thm iff_allI} ORELSE' K all_tac)
wenzelm@51717:         THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
boehmes@41328:         THEN_ALL_NEW (
wenzelm@42793:           NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
boehmes@41328:           ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
blanchet@58058:     Old_Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
blanchet@58058:       Old_Z3_Proof_Tools.by_tac ctxt' (
wenzelm@52732:         (rtac @{thm iff_allI} ORELSE' K all_tac)
wenzelm@51717:         THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
boehmes@41328:         THEN_ALL_NEW (
wenzelm@42793:           NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
boehmes@41328:           ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
blanchet@58058:     named ctxt "injectivity" (Old_Z3_Proof_Methods.prove_injectivity ctxt),
blanchet@58058:     Old_Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
boehmes@42992:       (fn ctxt' =>
blanchet@58058:         Old_Z3_Proof_Tools.by_tac ctxt' (
wenzelm@52732:           (rtac @{thm iff_allI} ORELSE' K all_tac)
wenzelm@51717:           THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
boehmes@42992:           THEN_ALL_NEW (
boehmes@42992:             NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
boehmes@42992:             ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac
boehmes@42992:               ctxt'))))]) ct))
boehmes@36898: 
boehmes@36898: end
boehmes@36898: 
boehmes@36898: 
boehmes@36898: 
boehmes@41130: (* proof reconstruction *)
boehmes@36898: 
boehmes@41130: (** tracing and checking **)
boehmes@36898: 
blanchet@58058: fun trace_before ctxt idx = Old_SMT_Config.trace_msg ctxt (fn r =>
blanchet@58058:   "Z3: #" ^ string_of_int idx ^ ": " ^ Old_Z3_Proof_Parser.string_of_rule r)
boehmes@36898: 
boehmes@41130: fun check_after idx r ps ct (p, (ctxt, _)) =
blanchet@58058:   if not (Config.get ctxt Old_SMT_Config.trace) then ()
boehmes@41130:   else
boehmes@36898:     let val thm = thm_of p |> tap (Thm.join_proofs o single)
boehmes@36898:     in
boehmes@36898:       if (Thm.cprop_of thm) aconvc ct then ()
boehmes@41328:       else
boehmes@41328:         z3_exn (Pretty.string_of (Pretty.big_list
blanchet@58058:           ("proof step failed: " ^ quote (Old_Z3_Proof_Parser.string_of_rule r) ^
boehmes@41328:             " (#" ^ string_of_int idx ^ ")")
boehmes@36898:           (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
boehmes@41328:             [Pretty.block [Pretty.str "expected: ",
boehmes@41328:               Syntax.pretty_term ctxt (Thm.term_of ct)]])))
boehmes@36898:     end
boehmes@36898: 
boehmes@36898: 
boehmes@41130: (** overall reconstruction procedure **)
boehmes@36898: 
boehmes@40164: local
boehmes@40164:   fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
blanchet@58058:     quote (Old_Z3_Proof_Parser.string_of_rule r))
boehmes@36898: 
boehmes@41131:   fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) =
boehmes@40164:     (case (r, ps) of
boehmes@40164:       (* core rules *)
blanchet@58058:       (Old_Z3_Proof_Parser.True_Axiom, _) => (Thm Old_Z3_Proof_Literals.true_thm, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion"
blanchet@58058:     | (Old_Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion"
blanchet@58058:     | (Old_Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) =>
boehmes@41328:         (mp q (thm_of p), cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) =>
boehmes@41328:         (mp q (thm_of p), cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.And_Elim, [(p, i)]) =>
boehmes@41328:         and_elim (p, i) ct ptab ||> pair cx
blanchet@58058:     | (Old_Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) =>
boehmes@41328:         not_or_elim (p, i) ct ptab ||> pair cx
blanchet@58058:     | (Old_Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) =>
boehmes@40164:         (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab
blanchet@58058:     | (Old_Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
boehmes@36898: 
boehmes@40164:       (* equality rules *)
blanchet@58058:     | (Old_Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp)
boehmes@40164: 
boehmes@40164:       (* quantifier rules *)
blanchet@58058:     | (Old_Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro cx vars p ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Quant_Inst, _) => (quant_inst cx ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab
boehmes@40164: 
boehmes@40164:       (* theory rules *)
blanchet@58058:     | (Old_Z3_Proof_Parser.Th_Lemma _, _) =>  (* FIXME: use arguments *)
boehmes@40164:         (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
blanchet@58058:     | (Old_Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
blanchet@58058:     | (Old_Z3_Proof_Parser.Rewrite_Star, ps) =>
boehmes@41328:         rewrite simpset (map fst ps) ct cx ||> rpair ptab
boehmes@36898: 
blanchet@58058:     | (Old_Z3_Proof_Parser.Nnf_Star, _) => not_supported r
blanchet@58058:     | (Old_Z3_Proof_Parser.Cnf_Star, _) => not_supported r
blanchet@58058:     | (Old_Z3_Proof_Parser.Transitivity_Star, _) => not_supported r
blanchet@58058:     | (Old_Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r
boehmes@36898: 
boehmes@41328:     | _ => raise Fail ("Z3: proof rule " ^
blanchet@58058:         quote (Old_Z3_Proof_Parser.string_of_rule r) ^
boehmes@41328:         " has an unexpected number of arguments."))
boehmes@36898: 
boehmes@41130:   fun lookup_proof ptab idx =
boehmes@41130:     (case Inttab.lookup ptab idx of
boehmes@41130:       SOME p => (p, idx)
boehmes@41130:     | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
boehmes@41130: 
boehmes@41131:   fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) =
boehmes@40164:     let
blanchet@58058:       val Old_Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step
boehmes@41130:       val ps = map (lookup_proof ptab) prems
boehmes@41130:       val _ = trace_before ctxt idx r
boehmes@41130:       val (thm, (ctxt', ptab')) =
boehmes@41130:         cxp
boehmes@41131:         |> prove_step simpset vars r ps prop
boehmes@41130:         |> tap (check_after idx r ps prop)
boehmes@41130:     in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end
boehmes@36898: 
boehmes@42191:   fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
blanchet@58058:     @{thm reflexive}, Old_Z3_Proof_Literals.true_thm]
boehmes@42191: 
boehmes@45393:   fun discharge_assms_tac rules =
wenzelm@52732:     REPEAT (HEADGOAL (resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
boehmes@45393:     
wenzelm@54883:   fun discharge_assms ctxt rules thm =
wenzelm@54883:     if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm
boehmes@41127:     else
boehmes@45393:       (case Seq.pull (discharge_assms_tac rules thm) of
wenzelm@54883:         SOME (thm', _) => Goal.norm_result ctxt thm'
boehmes@41127:       | NONE => raise THM ("failed to discharge premise", 1, [thm]))
boehmes@41127: 
boehmes@41131:   fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =
boehmes@41130:     thm_of p
wenzelm@42361:     |> singleton (Proof_Context.export inner_ctxt outer_ctxt)
wenzelm@54883:     |> discharge_assms outer_ctxt (make_discharge_rules rules)
boehmes@40164: in
boehmes@40164: 
boehmes@41127: fun reconstruct outer_ctxt recon output =
boehmes@40164:   let
boehmes@41127:     val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
boehmes@41328:     val (asserted, steps, vars, ctxt1) =
blanchet@58058:       Old_Z3_Proof_Parser.parse ctxt typs terms output
boehmes@41131: 
wenzelm@57957:     val simpset =
blanchet@58059:       Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems old_z3_simp})
boehmes@41131: 
boehmes@41131:     val ((is, rules), cxp as (ctxt2, _)) =
boehmes@41131:       add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
boehmes@36898:   in
blanchet@58058:     if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI})
boehmes@41127:     else
boehmes@41131:       (Thm @{thm TrueI}, cxp)
boehmes@41131:       |> fold (prove simpset vars) steps 
boehmes@42191:       |> discharge rules outer_ctxt
boehmes@41127:       |> pair []
boehmes@36898:   end
boehmes@36898: 
boehmes@40164: end
boehmes@36898: 
boehmes@36898: end