src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
changeset 58058 1a0b18176548
parent 58057 883f3c4c928e
child 58957 c9e744ea8a38
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_methods.ML	Thu Aug 28 00:40:38 2014 +0200
     1.3 @@ -0,0 +1,149 @@
     1.4 +(*  Title:      HOL/Library/Old_SMT/old_z3_proof_methods.ML
     1.5 +    Author:     Sascha Boehme, TU Muenchen
     1.6 +
     1.7 +Proof methods for Z3 proof reconstruction.
     1.8 +*)
     1.9 +
    1.10 +signature OLD_Z3_PROOF_METHODS =
    1.11 +sig
    1.12 +  val prove_injectivity: Proof.context -> cterm -> thm
    1.13 +  val prove_ite: Proof.context -> cterm -> thm
    1.14 +end
    1.15 +
    1.16 +structure Old_Z3_Proof_Methods: OLD_Z3_PROOF_METHODS =
    1.17 +struct
    1.18 +
    1.19 +
    1.20 +fun apply tac st =
    1.21 +  (case Seq.pull (tac 1 st) of
    1.22 +    NONE => raise THM ("tactic failed", 1, [st])
    1.23 +  | SOME (st', _) => st')
    1.24 +
    1.25 +
    1.26 +
    1.27 +(* if-then-else *)
    1.28 +
    1.29 +val pull_ite = mk_meta_eq
    1.30 +  @{lemma "f (if P then x else y) = (if P then f x else f y)" by simp}
    1.31 +
    1.32 +fun pull_ites_conv ct =
    1.33 +  (Conv.rewr_conv pull_ite then_conv
    1.34 +   Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct
    1.35 +
    1.36 +fun prove_ite ctxt =
    1.37 +  Old_Z3_Proof_Tools.by_tac ctxt (
    1.38 +    CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
    1.39 +    THEN' rtac @{thm refl})
    1.40 +
    1.41 +
    1.42 +
    1.43 +(* injectivity *)
    1.44 +
    1.45 +local
    1.46 +
    1.47 +val B = @{typ bool}
    1.48 +fun mk_univ T = Const (@{const_name top}, HOLogic.mk_setT T)
    1.49 +fun mk_inj_on T U =
    1.50 +  Const (@{const_name inj_on}, (T --> U) --> HOLogic.mk_setT T --> B)
    1.51 +fun mk_inv_into T U =
    1.52 +  Const (@{const_name inv_into}, [HOLogic.mk_setT T, T --> U, U] ---> T)
    1.53 +
    1.54 +fun mk_inv_of ctxt ct =
    1.55 +  let
    1.56 +    val (dT, rT) = Term.dest_funT (Old_SMT_Utils.typ_of ct)
    1.57 +    val inv = Old_SMT_Utils.certify ctxt (mk_inv_into dT rT)
    1.58 +    val univ = Old_SMT_Utils.certify ctxt (mk_univ dT)
    1.59 +  in Thm.mk_binop inv univ ct end
    1.60 +
    1.61 +fun mk_inj_prop ctxt ct =
    1.62 +  let
    1.63 +    val (dT, rT) = Term.dest_funT (Old_SMT_Utils.typ_of ct)
    1.64 +    val inj = Old_SMT_Utils.certify ctxt (mk_inj_on dT rT)
    1.65 +    val univ = Old_SMT_Utils.certify ctxt (mk_univ dT)
    1.66 +  in Old_SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end
    1.67 +
    1.68 +
    1.69 +val disjE = @{lemma "~P | Q ==> P ==> Q" by fast}
    1.70 +
    1.71 +fun prove_inj_prop ctxt def lhs =
    1.72 +  let
    1.73 +    val (ct, ctxt') = Old_SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt
    1.74 +    val rule = disjE OF [Object_Logic.rulify ctxt' (Thm.assume lhs)]
    1.75 +  in
    1.76 +    Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
    1.77 +    |> apply (rtac @{thm injI})
    1.78 +    |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
    1.79 +    |> Goal.norm_result ctxt' o Goal.finish ctxt'
    1.80 +    |> singleton (Variable.export ctxt' ctxt)
    1.81 +  end
    1.82 +
    1.83 +fun prove_rhs ctxt def lhs =
    1.84 +  Old_Z3_Proof_Tools.by_tac ctxt (
    1.85 +    CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
    1.86 +    THEN' REPEAT_ALL_NEW (match_tac @{thms allI})
    1.87 +    THEN' rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
    1.88 +
    1.89 +
    1.90 +fun expand thm ct =
    1.91 +  let
    1.92 +    val cpat = Thm.dest_arg (Thm.rhs_of thm)
    1.93 +    val (cl, cr) = Thm.dest_binop (Thm.dest_arg (Thm.dest_arg1 ct))
    1.94 +    val thm1 = Thm.instantiate (Thm.match (cpat, cl)) thm
    1.95 +    val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm
    1.96 +  in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end
    1.97 +
    1.98 +fun prove_lhs ctxt rhs =
    1.99 +  let
   1.100 +    val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs)))
   1.101 +    val conv = Old_SMT_Utils.binders_conv (K (expand eq)) ctxt
   1.102 +  in
   1.103 +    Old_Z3_Proof_Tools.by_tac ctxt (
   1.104 +      CONVERSION (Old_SMT_Utils.prop_conv conv)
   1.105 +      THEN' Simplifier.simp_tac (put_simpset HOL_ss ctxt))
   1.106 +  end
   1.107 +
   1.108 +
   1.109 +fun mk_inv_def ctxt rhs =
   1.110 +  let
   1.111 +    val (ct, ctxt') =
   1.112 +      Old_SMT_Utils.dest_all_cbinders (Old_SMT_Utils.dest_cprop rhs) ctxt
   1.113 +    val (cl, cv) = Thm.dest_binop ct
   1.114 +    val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
   1.115 +    val cu = fold_rev Thm.lambda cargs (mk_inv_of ctxt' (Thm.lambda cv cf))
   1.116 +  in Thm.assume (Old_SMT_Utils.mk_cequals cg cu) end
   1.117 +
   1.118 +fun prove_inj_eq ctxt ct =
   1.119 +  let
   1.120 +    val (lhs, rhs) =
   1.121 +      pairself Old_SMT_Utils.mk_cprop (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct))
   1.122 +    val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs)
   1.123 +    val rhs_thm =
   1.124 +      Thm.implies_intr lhs (prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs)
   1.125 +  in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
   1.126 +
   1.127 +
   1.128 +val swap_eq_thm = mk_meta_eq @{thm eq_commute}
   1.129 +val swap_disj_thm = mk_meta_eq @{thm disj_commute}
   1.130 +
   1.131 +fun swap_conv dest eq =
   1.132 +  Old_SMT_Utils.if_true_conv ((op <) o pairself Term.size_of_term o dest)
   1.133 +    (Conv.rewr_conv eq)
   1.134 +
   1.135 +val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm
   1.136 +val swap_disj_conv = swap_conv Old_SMT_Utils.dest_disj swap_disj_thm
   1.137 +
   1.138 +fun norm_conv ctxt =
   1.139 +  swap_eq_conv then_conv
   1.140 +  Conv.arg1_conv (Old_SMT_Utils.binders_conv (K swap_disj_conv) ctxt) then_conv
   1.141 +  Conv.arg_conv (Old_SMT_Utils.binders_conv (K swap_eq_conv) ctxt)
   1.142 +
   1.143 +in
   1.144 +
   1.145 +fun prove_injectivity ctxt =
   1.146 +  Old_Z3_Proof_Tools.by_tac ctxt (
   1.147 +    CONVERSION (Old_SMT_Utils.prop_conv (norm_conv ctxt))
   1.148 +    THEN' CSUBGOAL (uncurry (rtac o prove_inj_eq ctxt)))
   1.149 +
   1.150 +end
   1.151 +
   1.152 +end