1.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Apr 01 11:54:51 2011 +0200
1.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Fri Apr 01 12:16:41 2011 +0200
1.3 @@ -599,71 +599,42 @@
1.4 (* c = SOME x. P x |- (EX x. P x) = P c
1.5 c = SOME x. ~ P x |- ~(ALL x. P x) = ~ P c *)
1.6 local
1.7 - val elim_ex = @{lemma "EX x. P == P" by simp}
1.8 - val elim_all = @{lemma "~ (ALL x. P) == ~P" by simp}
1.9 - val sk_ex = @{lemma "c == SOME x. P x ==> EX x. P x == P c"
1.10 - by simp (intro eq_reflection some_eq_ex[symmetric])}
1.11 - val sk_all = @{lemma "c == SOME x. ~ P x ==> ~(ALL x. P x) == ~ P c"
1.12 - by (simp only: not_all) (intro eq_reflection some_eq_ex[symmetric])}
1.13 - val sk_ex_rule = ((sk_ex, I), elim_ex)
1.14 - and sk_all_rule = ((sk_all, Thm.dest_arg), elim_all)
1.15 + val forall =
1.16 + SMT_Utils.mk_const_pat @{theory} @{const_name all}
1.17 + (SMT_Utils.destT1 o SMT_Utils.destT1)
1.18 + fun mk_forall cv ct =
1.19 + Thm.capply (SMT_Utils.instT' cv forall) (Thm.cabs cv ct)
1.20
1.21 - fun dest f sk_rule =
1.22 - Thm.dest_comb (f (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of sk_rule))))
1.23 - fun type_of f sk_rule = Thm.ctyp_of_term (snd (dest f sk_rule))
1.24 - fun pair2 (a, b) (c, d) = [(a, c), (b, d)]
1.25 - fun inst_sk (sk_rule, f) p c =
1.26 - Thm.instantiate ([(type_of f sk_rule, Thm.ctyp_of_term c)], []) sk_rule
1.27 - |> (fn sk' => Thm.instantiate ([], (pair2 (dest f sk') (p, c))) sk')
1.28 - |> Conv.fconv_rule (Thm.beta_conversion true)
1.29 + fun get_vars f mk pred ctxt t =
1.30 + Term.fold_aterms f t []
1.31 + |> map_filter (fn v =>
1.32 + if pred v then SOME (SMT_Utils.certify ctxt (mk v)) else NONE)
1.33
1.34 - fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
1.35 - | kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) =
1.36 - (sk_all_rule, Thm.dest_arg, Z3_Proof_Literals.negate)
1.37 - | kind t = raise TERM ("skolemize", [t])
1.38 + fun close vars f ct ctxt =
1.39 + let
1.40 + val frees_of = get_vars Term.add_frees Free (member (op =) vars o fst)
1.41 + val vs = frees_of ctxt (Thm.term_of ct)
1.42 + val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt
1.43 + val vars_of = get_vars Term.add_vars Var (K true) ctxt'
1.44 + in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
1.45
1.46 - fun dest_abs_type (Abs (_, T, _)) = T
1.47 - | dest_abs_type t = raise TERM ("dest_abs_type", [t])
1.48 + val sk_rules = @{lemma
1.49 + "a = (SOME x. P x) ==> (EX x. P x) = P a"
1.50 + "a = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P a)"
1.51 + by (metis someI_ex)+}
1.52 +in
1.53
1.54 - fun bodies_of thy lhs rhs =
1.55 - let
1.56 - val (rule, dest, make) = kind (Thm.term_of lhs)
1.57 +fun skolemize vars =
1.58 + apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
1.59
1.60 - fun dest_body idx cbs ct =
1.61 - let
1.62 - val cb = Thm.dest_arg (dest ct)
1.63 - val T = dest_abs_type (Thm.term_of cb)
1.64 - val cv = Thm.cterm_of thy (Var (("x", idx), T))
1.65 - val cu = make (Drule.beta_conv cb cv)
1.66 - val cbs' = (cv, cb) :: cbs
1.67 - in
1.68 - (snd (Thm.first_order_match (cu, rhs)), rev cbs')
1.69 - handle Pattern.MATCH => dest_body (idx+1) cbs' cu
1.70 - end
1.71 - in (rule, dest_body 1 [] lhs) end
1.72 +fun discharge_sk_tac i st = (
1.73 + Tactic.rtac @{thm trans} i
1.74 + THEN Tactic.resolve_tac sk_rules i
1.75 + THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
1.76 + THEN Tactic.rtac @{thm refl} i) st
1.77
1.78 - fun transitive f thm = Thm.transitive thm (f (Thm.rhs_of thm))
1.79 +end
1.80
1.81 - fun sk_step (rule, elim) (cv, mct, cb) ((is, thm), ctxt) =
1.82 - (case mct of
1.83 - SOME ct =>
1.84 - ctxt
1.85 - |> Z3_Proof_Tools.make_hyp_def
1.86 - (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
1.87 - |>> pair ((cv, ct) :: is) o Thm.transitive thm
1.88 - | NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt))
1.89 -in
1.90 -fun skolemize ct ctxt =
1.91 - let
1.92 - val (lhs, rhs) = Thm.dest_binop (Thm.dest_arg ct)
1.93 - val (rule, (ctab, cbs)) = bodies_of (ProofContext.theory_of ctxt) lhs rhs
1.94 - fun lookup_var (cv, cb) = (cv, AList.lookup (op aconvc) ctab cv, cb)
1.95 - in
1.96 - (([], Thm.reflexive lhs), ctxt)
1.97 - |> fold (sk_step rule) (map lookup_var cbs)
1.98 - |>> MetaEq o snd
1.99 - end
1.100 -end
1.101
1.102
1.103 (** theory proof rules **)
1.104 @@ -816,7 +787,7 @@
1.105 | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
1.106 | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
1.107 | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
1.108 - | (Z3_Proof_Parser.Skolemize, _) => skolemize ct cx ||> rpair ptab
1.109 + | (Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab
1.110
1.111 (* theory rules *)
1.112 | (Z3_Proof_Parser.Th_Lemma _, _) => (* FIXME: use arguments *)
1.113 @@ -850,21 +821,23 @@
1.114 |> tap (check_after idx r ps prop)
1.115 in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end
1.116
1.117 - val disch_rules = [@{thm allI}, @{thm refl}, @{thm reflexive},
1.118 - Z3_Proof_Literals.true_thm]
1.119 - fun all_disch_rules rules = map (pair false) (disch_rules @ rules)
1.120 + fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
1.121 + @{thm reflexive}, Z3_Proof_Literals.true_thm]
1.122
1.123 - fun disch_assm rules thm =
1.124 - if Thm.nprems_of thm = 0 then Drule.flexflex_unique thm
1.125 + fun discharge_tac rules =
1.126 + Tactic.resolve_tac rules ORELSE' SOLVED' discharge_sk_tac
1.127 +
1.128 + fun discharge_assms rules thm =
1.129 + if Thm.nprems_of thm = 0 then Goal.norm_result thm
1.130 else
1.131 - (case Seq.pull (Thm.biresolution false rules 1 thm) of
1.132 - SOME (thm', _) => disch_assm rules thm'
1.133 + (case Seq.pull (discharge_tac rules 1 thm) of
1.134 + SOME (thm', _) => discharge_assms rules thm'
1.135 | NONE => raise THM ("failed to discharge premise", 1, [thm]))
1.136
1.137 fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =
1.138 thm_of p
1.139 |> singleton (ProofContext.export inner_ctxt outer_ctxt)
1.140 - |> disch_assm rules
1.141 + |> discharge_assms (make_discharge_rules rules)
1.142 in
1.143
1.144 fun reconstruct outer_ctxt recon output =
1.145 @@ -882,7 +855,7 @@
1.146 else
1.147 (Thm @{thm TrueI}, cxp)
1.148 |> fold (prove simpset vars) steps
1.149 - |> discharge (all_disch_rules rules) outer_ctxt
1.150 + |> discharge rules outer_ctxt
1.151 |> pair []
1.152 end
1.153