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