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