src/HOL/Tools/SMT/z3_proof_methods.ML
author boehmes
Wed Nov 24 15:33:35 2010 +0100 (2010-11-24)
changeset 40686 4725ed462387
parent 40663 e080c9e68752
child 40840 2f97215e79bf
permissions -rw-r--r--
swap names for built-in tester functions (to better reflect the intuition of what they do);
eta-expand all built-in functions (even those which are only partially supported)
     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 end
    11 
    12 structure Z3_Proof_Methods: Z3_PROOF_METHODS =
    13 struct
    14 
    15 structure U = SMT_Utils
    16 structure T = Z3_Proof_Tools
    17 
    18 
    19 fun apply tac st =
    20   (case Seq.pull (tac 1 st) of
    21     NONE => raise THM ("tactic failed", 1, [st])
    22   | SOME (st', _) => st')
    23 
    24 
    25 
    26 (* injectivity *)
    27 
    28 local
    29 
    30 val B = @{typ bool}
    31 fun mk_univ T = Const (@{const_name top}, T --> B)
    32 fun mk_inj_on T U =
    33   Const (@{const_name inj_on}, (T --> U) --> (T --> B) --> B)
    34 fun mk_inv_into T U =
    35   Const (@{const_name inv_into}, [T --> B, T --> U, U] ---> T)
    36 
    37 fun mk_inv_of ctxt ct =
    38   let
    39     val (dT, rT) = U.split_type (U.typ_of ct)
    40     val inv = U.certify ctxt (mk_inv_into dT rT)
    41     val univ = U.certify ctxt (mk_univ dT)
    42   in Thm.mk_binop inv univ ct end
    43 
    44 fun mk_inj_prop ctxt ct =
    45   let
    46     val (dT, rT) = U.split_type (U.typ_of ct)
    47     val inj = U.certify ctxt (mk_inj_on dT rT)
    48     val univ = U.certify ctxt (mk_univ dT)
    49   in U.mk_cprop (Thm.mk_binop inj ct univ) end
    50 
    51 
    52 val disjE = @{lemma "~P | Q ==> P ==> Q" by fast}
    53 
    54 fun prove_inj_prop ctxt def lhs =
    55   let
    56     val (ct, ctxt') = U.dest_all_cabs (Thm.rhs_of def) ctxt
    57     val rule = disjE OF [Object_Logic.rulify (Thm.assume lhs)]
    58   in
    59     Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
    60     |> apply (Tactic.rtac @{thm injI})
    61     |> apply (Tactic.solve_tac [rule, rule RS @{thm sym}])
    62     |> Goal.norm_result o Goal.finish ctxt'
    63     |> singleton (Variable.export ctxt' ctxt)
    64   end
    65 
    66 fun prove_rhs ctxt def lhs =
    67   T.by_tac (
    68     CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
    69     THEN' REPEAT_ALL_NEW (Tactic.match_tac @{thms allI})
    70     THEN' Tactic.rtac (@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs])) #>
    71   Thm.elim_implies def
    72 
    73 
    74 fun expand thm ct =
    75   let
    76     val cpat = Thm.dest_arg (Thm.rhs_of thm)
    77     val (cl, cr) = Thm.dest_binop (Thm.dest_arg (Thm.dest_arg1 ct))
    78     val thm1 = Thm.instantiate (Thm.match (cpat, cl)) thm
    79     val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm
    80   in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end
    81 
    82 fun prove_lhs ctxt rhs =
    83   let
    84     val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify (Thm.assume rhs)))
    85   in
    86     T.by_tac (
    87       CONVERSION (U.prop_conv (U.binders_conv (K (expand eq)) ctxt))
    88       THEN' Simplifier.simp_tac HOL_ss)
    89   end
    90 
    91 
    92 fun mk_inv_def ctxt rhs =
    93   let
    94     val (ct, ctxt') = U.dest_all_cbinders (U.dest_cprop rhs) ctxt
    95     val (cl, cv) = Thm.dest_binop ct
    96     val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
    97     val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf))
    98   in Thm.assume (U.mk_cequals cg cu) end
    99 
   100 fun prove_inj_eq ctxt ct =
   101   let
   102     val (lhs, rhs) = pairself U.mk_cprop (Thm.dest_binop (U.dest_cprop ct))
   103     val lhs_thm = prove_lhs ctxt rhs lhs
   104     val rhs_thm = prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs
   105   in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
   106 
   107 
   108 val swap_eq_thm = mk_meta_eq @{thm eq_commute}
   109 val swap_disj_thm = mk_meta_eq @{thm disj_commute}
   110 
   111 fun swap_conv dest eq =
   112   U.if_true_conv ((op <) o pairself Term.size_of_term o dest)
   113     (Conv.rewr_conv eq)
   114 
   115 val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm
   116 val swap_disj_conv = swap_conv U.dest_disj swap_disj_thm
   117 
   118 fun norm_conv ctxt =
   119   swap_eq_conv then_conv
   120   Conv.arg1_conv (U.binders_conv (K swap_disj_conv) ctxt) then_conv
   121   Conv.arg_conv (U.binders_conv (K swap_eq_conv) ctxt)
   122 
   123 in
   124 
   125 fun prove_injectivity ctxt =
   126   T.by_tac (
   127     CONVERSION (U.prop_conv (norm_conv ctxt))
   128     THEN' CSUBGOAL (uncurry (Tactic.rtac o prove_inj_eq ctxt)))
   129 
   130 end
   131 
   132 end