src/HOL/Library/Old_SMT/old_z3_proof_methods.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 60752 b48830b670a1
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_z3_proof_methods.ML
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     3
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     4
Proof methods for Z3 proof reconstruction.
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     5
*)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     6
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_Z3_PROOF_METHODS =
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     8
sig
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     9
  val prove_injectivity: Proof.context -> cterm -> thm
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    10
  val prove_ite: Proof.context -> cterm -> thm
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    11
end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    12
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    13
structure Old_Z3_Proof_Methods: OLD_Z3_PROOF_METHODS =
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    14
struct
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    15
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    16
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    17
fun apply tac st =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    18
  (case Seq.pull (tac 1 st) of
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    19
    NONE => raise THM ("tactic failed", 1, [st])
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    20
  | SOME (st', _) => st')
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    21
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    22
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    23
45392
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    24
(* if-then-else *)
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    25
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    26
val pull_ite = mk_meta_eq
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    27
  @{lemma "f (if P then x else y) = (if P then f x else f y)" by simp}
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    28
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    29
fun pull_ites_conv ct =
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    30
  (Conv.rewr_conv pull_ite then_conv
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    31
   Conv.binop_conv (Conv.try_conv pull_ites_conv)) ct
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    32
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    33
fun prove_ite ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    34
  Old_Z3_Proof_Tools.by_tac ctxt (
45392
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    35
    CONVERSION (Conv.arg_conv (Conv.arg1_conv pull_ites_conv))
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 59621
diff changeset
    36
    THEN' resolve_tac ctxt @{thms refl})
45392
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    37
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    38
828e08541cee replace higher-order matching against schematic theorem with dedicated reconstruction method
boehmes
parents: 45263
diff changeset
    39
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    40
(* injectivity *)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    41
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    42
local
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    43
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    44
val B = @{typ bool}
45263
93ac73160d78 clarify types of terms: use proper set type
boehmes
parents: 41899
diff changeset
    45
fun mk_univ T = Const (@{const_name top}, HOLogic.mk_setT T)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    46
fun mk_inj_on T U =
45263
93ac73160d78 clarify types of terms: use proper set type
boehmes
parents: 41899
diff changeset
    47
  Const (@{const_name inj_on}, (T --> U) --> HOLogic.mk_setT T --> B)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    48
fun mk_inv_into T U =
45263
93ac73160d78 clarify types of terms: use proper set type
boehmes
parents: 41899
diff changeset
    49
  Const (@{const_name inv_into}, [HOLogic.mk_setT T, T --> U, U] ---> T)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    50
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    51
fun mk_inv_of ctxt ct =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    52
  let
59586
ddf6deaadfe8 clarified signature;
wenzelm
parents: 59498
diff changeset
    53
    val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct)
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59590
diff changeset
    54
    val inv = Thm.cterm_of ctxt (mk_inv_into dT rT)
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59590
diff changeset
    55
    val univ = Thm.cterm_of ctxt (mk_univ dT)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    56
  in Thm.mk_binop inv univ ct end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    57
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    58
fun mk_inj_prop ctxt ct =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    59
  let
59586
ddf6deaadfe8 clarified signature;
wenzelm
parents: 59498
diff changeset
    60
    val (dT, rT) = Term.dest_funT (Thm.typ_of_cterm ct)
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59590
diff changeset
    61
    val inj = Thm.cterm_of ctxt (mk_inj_on dT rT)
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59590
diff changeset
    62
    val univ = Thm.cterm_of ctxt (mk_univ dT)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    63
  in Old_SMT_Utils.mk_cprop (Thm.mk_binop inj ct univ) end
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    64
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    65
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    66
val disjE = @{lemma "~P | Q ==> P ==> Q" by fast}
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    67
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
    68
fun prove_inj_prop ctxt def lhs =
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    69
  let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    70
    val (ct, ctxt') = Old_SMT_Utils.dest_all_cabs (Thm.rhs_of def) ctxt
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    71
    val rule = disjE OF [Object_Logic.rulify ctxt' (Thm.assume lhs)]
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    72
  in
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    73
    Goal.init (mk_inj_prop ctxt' (Thm.dest_arg ct))
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 59621
diff changeset
    74
    |> apply (resolve_tac ctxt' @{thms injI})
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
    75
    |> apply (Tactic.solve_tac ctxt' [rule, rule RS @{thm sym}])
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
    76
    |> Goal.norm_result ctxt' o Goal.finish ctxt'
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    77
    |> singleton (Variable.export ctxt' ctxt)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    78
  end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    79
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
    80
fun prove_rhs ctxt def lhs =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    81
  Old_Z3_Proof_Tools.by_tac ctxt (
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
    82
    CONVERSION (Conv.top_sweep_conv (K (Conv.rewr_conv def)) ctxt)
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58058
diff changeset
    83
    THEN' REPEAT_ALL_NEW (match_tac ctxt @{thms allI})
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 59621
diff changeset
    84
    THEN' resolve_tac ctxt [@{thm inv_f_f} OF [prove_inj_prop ctxt def lhs]])
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    85
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    86
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    87
fun expand thm ct =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    88
  let
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    89
    val cpat = Thm.dest_arg (Thm.rhs_of thm)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    90
    val (cl, cr) = Thm.dest_binop (Thm.dest_arg (Thm.dest_arg1 ct))
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    91
    val thm1 = Thm.instantiate (Thm.match (cpat, cl)) thm
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    92
    val thm2 = Thm.instantiate (Thm.match (cpat, cr)) thm
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    93
  in Conv.arg_conv (Conv.binop_conv (Conv.rewrs_conv [thm1, thm2])) ct end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    94
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
    95
fun prove_lhs ctxt rhs =
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    96
  let
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52732
diff changeset
    97
    val eq = Thm.symmetric (mk_meta_eq (Object_Logic.rulify ctxt (Thm.assume rhs)))
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    98
    val conv = Old_SMT_Utils.binders_conv (K (expand eq)) ctxt
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    99
  in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   100
    Old_Z3_Proof_Tools.by_tac ctxt (
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   101
      CONVERSION (Old_SMT_Utils.prop_conv conv)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46497
diff changeset
   102
      THEN' Simplifier.simp_tac (put_simpset HOL_ss ctxt))
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   103
  end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   104
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   105
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   106
fun mk_inv_def ctxt rhs =
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   107
  let
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 40840
diff changeset
   108
    val (ct, ctxt') =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   109
      Old_SMT_Utils.dest_all_cbinders (Old_SMT_Utils.dest_cprop rhs) ctxt
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   110
    val (cl, cv) = Thm.dest_binop ct
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   111
    val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45392
diff changeset
   112
    val cu = fold_rev Thm.lambda cargs (mk_inv_of ctxt' (Thm.lambda cv cf))
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   113
  in Thm.assume (Old_SMT_Utils.mk_cequals cg cu) end
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   114
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   115
fun prove_inj_eq ctxt ct =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   116
  let
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 40840
diff changeset
   117
    val (lhs, rhs) =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58957
diff changeset
   118
      apply2 Old_SMT_Utils.mk_cprop (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct))
41899
83dd157ec9ab finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents: 41328
diff changeset
   119
    val lhs_thm = Thm.implies_intr rhs (prove_lhs ctxt rhs lhs)
83dd157ec9ab finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents: 41328
diff changeset
   120
    val rhs_thm =
83dd157ec9ab finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents: 41328
diff changeset
   121
      Thm.implies_intr lhs (prove_rhs ctxt (mk_inv_def ctxt rhs) lhs rhs)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   122
  in lhs_thm COMP (rhs_thm COMP @{thm iffI}) end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   123
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   124
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   125
val swap_eq_thm = mk_meta_eq @{thm eq_commute}
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   126
val swap_disj_thm = mk_meta_eq @{thm disj_commute}
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   127
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   128
fun swap_conv dest eq =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58957
diff changeset
   129
  Old_SMT_Utils.if_true_conv ((op <) o apply2 Term.size_of_term o dest)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   130
    (Conv.rewr_conv eq)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   131
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   132
val swap_eq_conv = swap_conv HOLogic.dest_eq swap_eq_thm
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   133
val swap_disj_conv = swap_conv Old_SMT_Utils.dest_disj swap_disj_thm
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   134
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   135
fun norm_conv ctxt =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   136
  swap_eq_conv then_conv
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   137
  Conv.arg1_conv (Old_SMT_Utils.binders_conv (K swap_disj_conv) ctxt) then_conv
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   138
  Conv.arg_conv (Old_SMT_Utils.binders_conv (K swap_eq_conv) ctxt)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   139
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   140
in
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   141
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   142
fun prove_injectivity ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   143
  Old_Z3_Proof_Tools.by_tac ctxt (
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   144
    CONVERSION (Old_SMT_Utils.prop_conv (norm_conv ctxt))
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 59621
diff changeset
   145
    THEN' CSUBGOAL (uncurry (resolve_tac ctxt o single o prove_inj_eq ctxt)))
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   146
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   147
end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   148
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   149
end