src/HOL/Tools/SMT/z3_proof_methods.ML
 author wenzelm Wed Feb 15 23:19:30 2012 +0100 (2012-02-15) changeset 46497 89ccf66aa73d parent 45392 828e08541cee child 51717 9e7d1c139569 permissions -rw-r--r--
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
```     1 (*  Title:      HOL/Tools/SMT/z3_proof_methods.ML
```
```     2     Author:     Sascha Boehme, TU Muenchen
```
```     3
```
```     4 Proof methods for Z3 proof reconstruction.
```
```     5 *)
```
```     6
```
```     7 signature Z3_PROOF_METHODS =
```
```     8 sig
```
```     9   val prove_injectivity: Proof.context -> cterm -> thm
```
```    10   val prove_ite: cterm -> thm
```
```    11 end
```
```    12
```
```    13 structure Z3_Proof_Methods: Z3_PROOF_METHODS =
```
```    14 struct
```
```    15
```
```    16
```
```    17 fun apply tac st =
```
```    18   (case Seq.pull (tac 1 st) of
```
```    19     NONE => raise THM ("tactic failed", 1, [st])
```
```    20   | SOME (st', _) => st')
```
```    21
```
```    22
```
```    23
```
```    24 (* if-then-else *)
```
```    25
```
```    26 val pull_ite = mk_meta_eq
```
```    27   @{lemma "f (if P then x else y) = (if P then f x else f y)" by simp}
```
```    28
```
```    29 fun pull_ites_conv ct =
```
```    30   (Conv.rewr_conv pull_ite then_conv
```
```    31    Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct
```
```    32
```
```    33 val prove_ite =
```
```    34   Z3_Proof_Tools.by_tac (
```
```    35     CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
```
```    36     THEN' Tactic.rtac @{thm refl})
```
```    37
```
```    38
```
```    39
```
```    40 (* injectivity *)
```
```    41
```
```    42 local
```
```    43
```
```    44 val B = @{typ bool}
```
```    45 fun mk_univ T = Const (@{const_name top}, HOLogic.mk_setT T)
```
```    46 fun mk_inj_on T U =
```
```    47   Const (@{const_name inj_on}, (T --> U) --> HOLogic.mk_setT T --> B)
```
```    48 fun mk_inv_into T U =
```
```    49   Const (@{const_name inv_into}, [HOLogic.mk_setT T, T --> U, U] ---> T)
```
```    50
```
```    51 fun mk_inv_of ctxt ct =
```
```    52   let
```
```    53     val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct)
```
```    54     val inv = SMT_Utils.certify ctxt (mk_inv_into dT rT)
```
```    55     val univ = SMT_Utils.certify ctxt (mk_univ dT)
```
```    56   in Thm.mk_binop inv univ ct end
```
```    57
```
```    58 fun mk_inj_prop ctxt ct =
```
```    59   let
```
```    60     val (dT, rT) = Term.dest_funT (SMT_Utils.typ_of ct)
```
```    61     val inj = SMT_Utils.certify ctxt (mk_inj_on dT rT)
```
```    62     val univ = SMT_Utils.certify ctxt (mk_univ dT)
```
```    63   in SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end
```
```    64
```
```    65
```
```    66 val disjE = @{lemma "~P | Q ==> P ==> Q" by fast}
```
```    67
```
```    68 fun prove_inj_prop ctxt def lhs =
```
```    69   let
```
```    70     val (ct, ctxt') = SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt
```
```    71     val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
```
```    72   in
```
```    73     Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
```
```    74     |> apply (Tactic.rtac @{thm injI})
```
```    75     |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
```
```    76     |> Goal.norm_result o Goal.finish ctxt'
```
```    77     |> singleton (Variable.export ctxt' ctxt)
```
```    78   end
```
```    79
```
```    80 fun prove_rhs ctxt def lhs =
```
```    81   Z3_Proof_Tools.by_tac (
```
```    82     CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
```
```    83     THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
```
```    84     THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]))
```
```    85
```
```    86
```
```    87 fun expand thm ct =
```
```    88   let
```
```    89     val cpat = Thm.dest_arg (Thm.rhs_of thm)
```
```    90     val (cl, cr) = Thm.dest_binop (Thm.dest_arg (Thm.dest_arg1 ct))
```
```    91     val thm1 = Thm.instantiate (Thm.match (cpat, cl)) thm
```
```    92     val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm
```
```    93   in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end
```
```    94
```
```    95 fun prove_lhs ctxt rhs =
```
```    96   let
```
```    97     val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
```
```    98     val conv = SMT_Utils.binders_conv (K (expand eq)) ctxt
```
```    99   in
```
```   100     Z3_Proof_Tools.by_tac (
```
```   101       CONVERSION (SMT_Utils.prop_conv conv)
```
```   102       THEN' Simplifier.simp_tac HOL_ss)
```
```   103   end
```
```   104
```
```   105
```
```   106 fun mk_inv_def ctxt rhs =
```
```   107   let
```
```   108     val (ct, ctxt') =
```
```   109       SMT_Utils.dest_all_cbinders (SMT_Utils.dest_cprop rhs) ctxt
```
```   110     val (cl, cv) = Thm.dest_binop ct
```
```   111     val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
```
```   112     val cu = fold_rev Thm.lambda cargs (mk_inv_of ctxt' (Thm.lambda cv cf))
```
```   113   in Thm.assume (SMT_Utils.mk_cequals cg cu) end
```
```   114
```
```   115 fun prove_inj_eq ctxt ct =
```
```   116   let
```
```   117     val (lhs, rhs) =
```
```   118       pairself SMT_Utils.mk_cprop (Thm.dest_binop (SMT_Utils.dest_cprop ct))
```
```   119     val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs)
```
```   120     val rhs_thm =
```
```   121       Thm.implies_intr lhs (prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs)
```
```   122   in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
```
```   123
```
```   124
```
```   125 val swap_eq_thm = mk_meta_eq @{thm eq_commute}
```
```   126 val swap_disj_thm = mk_meta_eq @{thm disj_commute}
```
```   127
```
```   128 fun swap_conv dest eq =
```
```   129   SMT_Utils.if_true_conv ((op <) o pairself Term.size_of_term o dest)
```
```   130     (Conv.rewr_conv eq)
```
```   131
```
```   132 val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm
```
```   133 val swap_disj_conv = swap_conv SMT_Utils.dest_disj swap_disj_thm
```
```   134
```
```   135 fun norm_conv ctxt =
```
```   136   swap_eq_conv then_conv
```
```   137   Conv.arg1_conv (SMT_Utils.binders_conv (K swap_disj_conv) ctxt) then_conv
```
```   138   Conv.arg_conv (SMT_Utils.binders_conv (K swap_eq_conv) ctxt)
```
```   139
```
```   140 in
```
```   141
```
```   142 fun prove_injectivity ctxt =
```
```   143   Z3_Proof_Tools.by_tac (
```
```   144     CONVERSION (SMT_Utils.prop_conv (norm_conv ctxt))
```
```   145     THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
```
```   146
```
```   147 end
```
```   148
```
```   149 end
```