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