src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 64574 1134e4d5e5b7
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_reconstruction.ML
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
Proof reconstruction for proofs found by Z3.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
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_RECONSTRUCTION =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
     9
  val add_z3_rule: thm -> Context.generic -> Context.generic
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    10
  val reconstruct: Proof.context -> Old_SMT_Translate.recon -> string list -> int list * thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
end
8e55aa1306c5 integrated SMT into the HOL image
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_Reconstruction: OLD_Z3_PROOF_RECONSTRUCTION =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    17
fun z3_exn msg = raise Old_SMT_Failure.SMT (Old_SMT_Failure.Other_Failure
40162
7f58a9a843c2 joined setup of SMT solvers in one place; turned Z3-specific options into SMT options (renamed configuration options from z3_* to smt_*); more detailed SMT exception; improved SMT filter interface
boehmes
parents: 40161
diff changeset
    18
  ("Z3 proof reconstruction: " ^ msg))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
    22
(* net of schematic rules *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
  val description = "declaration of Z3 proof rules"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
  val eq = Thm.eq_thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    29
  structure Old_Z3_Rules = Generic_Data
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
  (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
    type T = thm Net.net
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
    val empty = Net.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
    val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
    val merge = Net.merge eq
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
  )
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52732
diff changeset
    37
  fun prep context =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    38
    `Thm.prop_of o rewrite_rule (Context.proof_of context) [Old_Z3_Proof_Literals.rewrite_true]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52732
diff changeset
    40
  fun ins thm context =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    41
    context |> Old_Z3_Rules.map (fn net => Net.insert_term eq (prep context thm) net handle Net.INSERT => net)
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52732
diff changeset
    42
  fun rem thm context =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    43
    context |> Old_Z3_Rules.map (fn net => Net.delete_term eq (prep context thm) net handle Net.DELETE => net)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52732
diff changeset
    45
  val add = Thm.declaration_attribute ins
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52732
diff changeset
    46
  val del = Thm.declaration_attribute rem
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
54742
7a86358a3c0b proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents: 52732
diff changeset
    49
val add_z3_rule = ins
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
fun by_schematic_rule ctxt ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    52
  the (Old_Z3_Proof_Tools.net_instance (Old_Z3_Rules.get (Context.Proof ctxt)) ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
57957
e6ee35b8f4b5 updated to named_theorems;
wenzelm
parents: 56245
diff changeset
    54
val _ = Theory.setup
58059
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
    55
 (Attrib.setup @{binding old_z3_rule} (Attrib.add_del add del) description #>
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
    56
  Global_Theory.add_thms_dynamic (@{binding old_z3_rule}, Net.content o Old_Z3_Rules.get))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
    62
(* proof tools *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
fun named ctxt name prover ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    65
  let val _ = Old_SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
  in prover ct end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    67
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
fun NAMED ctxt name tac i st =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    69
  let val _ = Old_SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    70
  in tac i st end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
fun pretty_goal ctxt thms t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
  [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
  |> not (null thms) ? cons (Pretty.big_list "assumptions:"
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 60949
diff changeset
    75
       (map (Thm.pretty_thm ctxt) thms))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
fun try_apply ctxt thms =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
    fun try_apply_err ct = Pretty.string_of (Pretty.chunks [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
      Pretty.big_list ("Z3 found a proof," ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
        " but proof reconstruction failed at the following subgoal:")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
        (pretty_goal ctxt thms (Thm.term_of ct)),
58059
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
    83
      Pretty.str ("Declaring a rule as [old_z3_rule] might solve this problem.")])
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
    fun apply [] ct = error (try_apply_err ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
      | apply (prover :: provers) ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
          (case try prover ct of
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    88
            SOME thm => (Old_SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
          | NONE => apply provers ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
43893
f3e75541cb78 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents: 42992
diff changeset
    91
    fun schematic_label full = "schematic rules" |> full ? suffix " (full)"
f3e75541cb78 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents: 42992
diff changeset
    92
    fun schematic ctxt full ct =
f3e75541cb78 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents: 42992
diff changeset
    93
      ct
f3e75541cb78 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents: 42992
diff changeset
    94
      |> full ? fold_rev (curry Drule.mk_implies o Thm.cprop_of) thms
f3e75541cb78 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents: 42992
diff changeset
    95
      |> named ctxt (schematic_label full) (by_schematic_rule ctxt)
f3e75541cb78 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents: 42992
diff changeset
    96
      |> fold Thm.elim_implies thms
f3e75541cb78 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents: 42992
diff changeset
    97
f3e75541cb78 allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
boehmes
parents: 42992
diff changeset
    98
  in apply o cons (schematic ctxt false) o cons (schematic ctxt true) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   100
local
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   101
  val rewr_if =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   102
    @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   103
in
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   104
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   105
fun HOL_fast_tac ctxt =
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   106
  Classical.fast_tac (put_claset HOL_cs ctxt)
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   107
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   108
fun simp_fast_tac ctxt =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49980
diff changeset
   109
  Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [rewr_if])
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   110
  THEN_ALL_NEW HOL_fast_tac ctxt
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   111
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   112
end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   113
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   116
(* theorems and proofs *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   118
(** theorem incarnations **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
datatype theorem =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
  Thm of thm | (* theorem without special features *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
  MetaEq of thm | (* meta equality "t == s" *)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   123
  Literals of thm * Old_Z3_Proof_Literals.littab
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
    (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
fun thm_of (Thm thm) = thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
  | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
  | thm_of (Literals (thm, _)) = thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
fun meta_eq_of (MetaEq thm) = thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
  | meta_eq_of p = mk_meta_eq (thm_of p)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
fun literals_of (Literals (_, lits)) = lits
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   134
  | literals_of p = Old_Z3_Proof_Literals.make_littab [thm_of p]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
(** core proof rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
(* assumption *)
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   141
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
local
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   143
  val remove_trigger = mk_meta_eq @{thm trigger_def}
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   144
  val remove_weight = mk_meta_eq @{thm weight_def}
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   145
  val remove_fun_app = mk_meta_eq @{thm fun_app_def}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
44488
587bf61a00a1 improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents: 44058
diff changeset
   147
  fun rewrite_conv _ [] = Conv.all_conv
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49980
diff changeset
   148
    | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   150
  val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   151
    remove_fun_app, Old_Z3_Proof_Literals.rewrite_true]
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   152
44488
587bf61a00a1 improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents: 44058
diff changeset
   153
  fun rewrite _ [] = I
587bf61a00a1 improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents: 44058
diff changeset
   154
    | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   156
  fun lookup_assm assms_net ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   157
    Old_Z3_Proof_Tools.net_instances assms_net ct
45393
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   158
    |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
in
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   160
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   161
fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
  let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   163
    val eqs = map (rewrite ctxt [Old_Z3_Proof_Literals.rewrite_true]) rewrite_rules
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   164
    val eqs' = union Thm.eq_thm eqs prep_rules
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   165
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   166
    val assms_net =
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   167
      assms
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   168
      |> map (apsnd (rewrite ctxt eqs'))
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   169
      |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
64574
1134e4d5e5b7 consolidate nested thms with persistent result, for improved performance;
wenzelm
parents: 61268
diff changeset
   170
      |> Old_Z3_Proof_Tools.thm_net_of snd
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   171
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   172
    fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   173
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   174
    fun assume thm ctxt =
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   175
      let
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   176
        val ct = Thm.cprem_of thm 1
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   177
        val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   178
      in (Thm.implies_elim thm thm', ctxt') end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
45393
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   180
    fun add1 idx thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) =
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   181
      let
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   182
        val (thm, ctxt') =
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   183
          if exact then (Thm.implies_elim thm1 th, ctxt)
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   184
          else assume thm1 ctxt
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   185
        val thms' = if exact then thms else th :: thms
64574
1134e4d5e5b7 consolidate nested thms with persistent result, for improved performance;
wenzelm
parents: 61268
diff changeset
   186
      in
45393
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   187
        ((insert (op =) i is, thms'),
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   188
          (ctxt', Inttab.update (idx, Thm thm) ptab))
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   189
      end
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   190
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   191
    fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) =
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   192
      let
64574
1134e4d5e5b7 consolidate nested thms with persistent result, for improved performance;
wenzelm
parents: 61268
diff changeset
   193
        val thm1 =
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   194
          Thm.trivial ct
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   195
          |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   196
        val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   197
      in
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   198
        (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
45393
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   199
          [] =>
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   200
            let val (thm, ctxt') = assume thm1 ctxt
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   201
            in ((is, thms), (ctxt', Inttab.update (idx, Thm thm) ptab)) end
45393
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 45392
diff changeset
   202
        | ithms => fold (add1 idx thm1) ithms cx)
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   203
      end
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   204
  in fold add asserted (([], []), (ctxt, Inttab.empty)) end
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   205
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
(* P = Q ==> P ==> Q   or   P --> Q ==> P ==> Q *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
local
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   211
  val precomp = Old_Z3_Proof_Tools.precompose2
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   212
  val comp = Old_Z3_Proof_Tools.compose
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   214
  val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   215
  val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   216
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   217
  val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   218
  val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
in
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   220
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
64574
1134e4d5e5b7 consolidate nested thms with persistent result, for improved performance;
wenzelm
parents: 61268
diff changeset
   221
  | mp p_q p =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   222
      let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   223
        val pq = thm_of p_q
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   224
        val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
      in Thm (Thm.implies_elim thm p) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   226
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   227
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
(* and_elim:     P1 & ... & Pn ==> Pi *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
(* not_or_elim:  ~(P1 | ... | Pn) ==> ~Pi *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
local
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   232
  fun is_sublit conj t = Old_Z3_Proof_Literals.exists_lit conj (fn u => u aconv t)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
  fun derive conj t lits idx ptab =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
    let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   236
      val lit = the (Old_Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   237
      val ls = Old_Z3_Proof_Literals.explode conj false false [t] lit
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   238
      val lits' = fold Old_Z3_Proof_Literals.insert_lit ls
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   239
        (Old_Z3_Proof_Literals.delete_lit lit lits)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   241
      fun upd thm = Literals (thm_of thm, lits')
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   242
      val ptab' = Inttab.map_entry idx upd ptab
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   243
    in (the (Old_Z3_Proof_Literals.lookup_lit lits' t), ptab') end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
  fun lit_elim conj (p, idx) ct ptab =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
    let val lits = literals_of p
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
    in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   248
      (case Old_Z3_Proof_Literals.lookup_lit lits (Old_SMT_Utils.term_of ct) of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
        SOME lit => (Thm lit, ptab)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   250
      | NONE => apfst Thm (derive conj (Old_SMT_Utils.term_of ct) lits idx ptab))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
val and_elim = lit_elim true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
val not_or_elim = lit_elim false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
(* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
  fun step lit thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   261
    Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   262
  val explode_disj = Old_Z3_Proof_Literals.explode false false false
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
  fun intro hyps thm th = fold step (explode_disj hyps th) thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
  fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   266
  val ccontr = Old_Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
fun lemma thm ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
  let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   270
    val cu = Old_Z3_Proof_Literals.negate (Thm.dest_arg ct)
44058
ae85c5d64913 misc tuning -- eliminated old-fashioned rep_thm;
wenzelm
parents: 43893
diff changeset
   271
    val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   272
    val th = Old_Z3_Proof_Tools.under_assumption (intro hyps thm) cu
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   273
  in Thm (Old_Z3_Proof_Tools.compose ccontr th) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
local
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   279
  val explode_disj = Old_Z3_Proof_Literals.explode false true false
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   280
  val join_disj = Old_Z3_Proof_Literals.join false
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
  fun unit thm thms th =
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   282
    let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   283
      val t = @{const Not} $ Old_SMT_Utils.prop_of thm
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   284
      val ts = map Old_SMT_Utils.prop_of thms
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   285
    in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   286
      join_disj (Old_Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   287
    end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
  fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58957
diff changeset
   290
  fun dest ct = apply2 dest_arg2 (Thm.dest_binop ct)
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   291
  val contrapos =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   292
    Old_Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
fun unit_resolution thm thms ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   295
  Old_Z3_Proof_Literals.negate (Thm.dest_arg ct)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   296
  |> Old_Z3_Proof_Tools.under_assumption (unit thm thms)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   297
  |> Thm o Old_Z3_Proof_Tools.discharge thm o Old_Z3_Proof_Tools.compose contrapos
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
(* P ==> P == True   or   P ==> P == False *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
  val iff1 = @{lemma "P ==> P == (~ False)" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
  val iff2 = @{lemma "~P ==> P == False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
fun iff_true thm = MetaEq (thm COMP iff1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
fun iff_false thm = MetaEq (thm COMP iff2)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   309
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   311
(* distributivity of | over & *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
fun distributivity ctxt = Thm o try_apply ctxt [] [
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   313
  named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   314
    (* FIXME: not very well tested *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   315
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   316
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   317
(* Tseitin-like axioms *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   318
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   319
  val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   320
  val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   321
  val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   322
  val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   323
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   324
  fun prove' conj1 conj2 ct2 thm =
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   325
    let
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   326
      val littab =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   327
        Old_Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   328
        |> cons Old_Z3_Proof_Literals.true_thm
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   329
        |> Old_Z3_Proof_Literals.make_littab
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   330
    in Old_Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   331
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   332
  fun prove rule (ct1, conj1) (ct2, conj2) =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   333
    Old_Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   334
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   335
  fun prove_def_axiom ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   336
    let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   337
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   338
      (case Thm.term_of ct1 of
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
   339
        @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   340
          prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
   341
      | @{const HOL.conj} $ _ $ _ =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   342
          prove disjI3 (Old_Z3_Proof_Literals.negate ct2, false) (ct1, true)
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
   343
      | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   344
          prove disjI3 (Old_Z3_Proof_Literals.negate ct2, false) (ct1, false)
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
   345
      | @{const HOL.disj} $ _ $ _ =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   346
          prove disjI2 (Old_Z3_Proof_Literals.negate ct1, false) (ct2, true)
40681
872b08416fb4 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents: 40680
diff changeset
   347
      | Const (@{const_name distinct}, _) $ _ =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   348
          let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   349
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   350
            val unfold_dis_conv = dis_conv Old_Z3_Proof_Tools.unfold_distinct_conv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   351
            fun prv cu =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   352
              let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   353
              in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   354
          in Old_Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
40681
872b08416fb4 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents: 40680
diff changeset
   355
      | @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   356
          let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   357
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   358
            val unfold_dis_conv = dis_conv Old_Z3_Proof_Tools.unfold_distinct_conv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   359
            fun prv cu =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   360
              let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   361
              in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   362
          in Old_Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   363
      | _ => raise CTERM ("prove_def_axiom", [ct]))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   364
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   365
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   366
fun def_axiom ctxt = Thm o try_apply ctxt [] [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   367
  named ctxt "conj/disj/distinct" prove_def_axiom,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   368
  Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   369
    named ctxt' "simp+fast" (Old_Z3_Proof_Tools.by_tac ctxt (simp_fast_tac ctxt')))]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   370
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   371
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   372
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   373
(* local definitions *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   374
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   375
  val intro_rules = [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   376
    @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   377
    @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   378
      by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   379
    @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   380
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   381
  val apply_rules = [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   382
    @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   383
    @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44488
diff changeset
   384
      by (atomize(full)) fastforce} ]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   385
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   386
  val inst_rule = Old_Z3_Proof_Tools.match_instantiate Thm.dest_arg
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   387
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   388
  fun apply_rule ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   389
    (case get_first (try (inst_rule ct)) intro_rules of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   390
      SOME thm => thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   391
    | NONE => raise CTERM ("intro_def", [ct]))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   392
in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   393
fun intro_def ct = Old_Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   394
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   395
fun apply_def thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   396
  get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   397
  |> the_default (Thm thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   398
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   399
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   400
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   401
(* negation normal form *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   402
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   403
  val quant_rules1 = ([
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   404
    @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   405
    @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   406
    @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   407
    @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   408
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   409
  val quant_rules2 = ([
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   410
    @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   411
    @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   412
    @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   413
    @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   414
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   415
  fun nnf_quant_tac ctxt thm (qs as (qs1, qs2)) i st = (
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60642
diff changeset
   416
    resolve_tac ctxt [thm] ORELSE'
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   417
    (match_tac ctxt qs1 THEN' nnf_quant_tac ctxt thm qs) ORELSE'
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   418
    (match_tac ctxt qs2 THEN' nnf_quant_tac ctxt thm qs)) i st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   419
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   420
  fun nnf_quant_tac_varified ctxt vars eq =
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   421
    nnf_quant_tac ctxt (Old_Z3_Proof_Tools.varify vars eq)
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   422
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   423
  fun nnf_quant ctxt vars qs p ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   424
    Old_Z3_Proof_Tools.as_meta_eq ct
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   425
    |> Old_Z3_Proof_Tools.by_tac ctxt (nnf_quant_tac_varified ctxt vars (meta_eq_of p) qs)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   426
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   427
  fun prove_nnf ctxt = try_apply ctxt [] [
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   428
    named ctxt "conj/disj" Old_Z3_Proof_Literals.prove_conj_disj_eq,
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   429
    Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   430
      named ctxt' "simp+fast" (Old_Z3_Proof_Tools.by_tac ctxt' (simp_fast_tac ctxt')))]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   431
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   432
fun nnf ctxt vars ps ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   433
  (case Old_SMT_Utils.term_of ct of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   434
    _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   435
      if l aconv r
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   436
      then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   437
      else MetaEq (nnf_quant ctxt vars quant_rules1 (hd ps) ct)
40579
98ebd2300823 use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)
boehmes
parents: 40516
diff changeset
   438
  | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   439
      MetaEq (nnf_quant ctxt vars quant_rules2 (hd ps) ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   440
  | _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   441
      let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   442
        val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   443
          (Old_Z3_Proof_Tools.unfold_eqs ctxt
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   444
            (map (Thm.symmetric o meta_eq_of) ps)))
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   445
      in Thm (Old_Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   446
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   447
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   448
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   449
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   450
(** equality proof rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   451
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   452
(* |- t = t *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   453
fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   454
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   455
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   456
(* s = t ==> t = s *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   457
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   458
  val symm_rule = @{lemma "s = t ==> t == s" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   459
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   460
fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   461
  | symm p = MetaEq (thm_of p COMP symm_rule)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   462
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   463
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   464
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   465
(* s = t ==> t = u ==> s = u *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   466
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   467
  val trans1 = @{lemma "s == t ==> t =  u ==> s == u" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   468
  val trans2 = @{lemma "s =  t ==> t == u ==> s == u" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   469
  val trans3 = @{lemma "s =  t ==> t =  u ==> s == u" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   470
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   471
fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   472
  | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   473
  | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   474
  | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   475
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   476
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   477
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   478
(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   479
   (reflexive antecendents are droppped) *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   480
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   481
  exception MONO
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   482
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   483
  fun prove_refl (ct, _) = Thm.reflexive ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   484
  fun prove_comb f g cp =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58957
diff changeset
   485
    let val ((ct1, ct2), (cu1, cu2)) = apply2 Thm.dest_comb cp
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   486
    in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   487
  fun prove_arg f = prove_comb prove_refl f
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   488
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   489
  fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   490
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   491
  fun prove_nary is_comb f =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   492
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   493
      fun prove (cp as (ct, _)) = f cp handle MONO =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   494
        if is_comb (Thm.term_of ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   495
        then prove_comb (prove_arg prove) prove cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   496
        else prove_refl cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   497
    in prove end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   498
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   499
  fun prove_list f n cp =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   500
    if n = 0 then prove_refl cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   501
    else prove_comb (prove_arg f) (prove_list f (n-1)) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   502
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   503
  fun with_length f (cp as (cl, _)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   504
    f (length (HOLogic.dest_list (Thm.term_of cl))) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   505
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   506
  fun prove_distinct f = prove_arg (with_length (prove_list f))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   507
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   508
  fun prove_eq exn lookup cp =
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58957
diff changeset
   509
    (case lookup (Logic.mk_equals (apply2 Thm.term_of cp)) of
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   510
      SOME eq => eq
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   511
    | NONE => if exn then raise MONO else prove_refl cp)
64574
1134e4d5e5b7 consolidate nested thms with persistent result, for improved performance;
wenzelm
parents: 61268
diff changeset
   512
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   513
  val prove_exn = prove_eq true
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   514
  and prove_safe = prove_eq false
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   515
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   516
  fun mono f (cp as (cl, _)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   517
    (case Term.head_of (Thm.term_of cl) of
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   518
      @{const HOL.conj} => prove_nary Old_Z3_Proof_Literals.is_conj (prove_exn f)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   519
    | @{const HOL.disj} => prove_nary Old_Z3_Proof_Literals.is_disj (prove_exn f)
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   520
    | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f)
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   521
    | _ => prove (prove_safe f)) cp
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   522
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   523
fun monotonicity eqs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   524
  let
40680
02caa72cb950 be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents: 40664
diff changeset
   525
    fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)]
02caa72cb950 be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents: 40664
diff changeset
   526
    val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs
02caa72cb950 be more liberal in reconstructing congruences from Z3 (sometimes the symmetric version of a premise is needed)
boehmes
parents: 40664
diff changeset
   527
    val lookup = AList.lookup (op aconv) teqs
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   528
    val cp = Thm.dest_binop (Thm.dest_arg ct)
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   529
  in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   530
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   531
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   532
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   533
(* |- f a b = f b a (where f is equality) *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   534
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   535
  val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   536
in
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   537
fun commutativity ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   538
  MetaEq (Old_Z3_Proof_Tools.match_instantiate I
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   539
    (Old_Z3_Proof_Tools.as_meta_eq ct) rule)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   540
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   541
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   542
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   543
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   544
(** quantifier proof rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   545
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   546
(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   547
   P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x)    *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   548
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   549
  val rules = [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   550
    @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   551
    @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   552
in
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   553
fun quant_intro ctxt vars p ct =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   554
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   555
    val thm = meta_eq_of p
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   556
    val rules' = Old_Z3_Proof_Tools.varify vars thm :: rules
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   557
    val cu = Old_Z3_Proof_Tools.as_meta_eq ct
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   558
    val tac = REPEAT_ALL_NEW (match_tac ctxt rules')
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   559
  in MetaEq (Old_Z3_Proof_Tools.by_tac ctxt tac cu) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   560
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   561
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   562
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   563
(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   564
fun pull_quant ctxt = Thm o try_apply ctxt [] [
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   565
  named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   566
    (* FIXME: not very well tested *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   567
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   568
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   569
(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   570
fun push_quant ctxt = Thm o try_apply ctxt [] [
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   571
  named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   572
    (* FIXME: not very well tested *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   573
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   574
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   575
(* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   576
local
42318
0fd33b6b22cf corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents: 42196
diff changeset
   577
  val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
0fd33b6b22cf corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents: 42196
diff changeset
   578
  val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   579
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   580
  fun elim_unused_tac ctxt i st = (
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   581
    match_tac ctxt [@{thm refl}]
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   582
    ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt)
42318
0fd33b6b22cf corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents: 42196
diff changeset
   583
    ORELSE' (
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   584
      match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}]
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   585
      THEN' elim_unused_tac ctxt)) i st
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   586
in
42318
0fd33b6b22cf corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents: 42196
diff changeset
   587
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   588
fun elim_unused_vars ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (elim_unused_tac ctxt)
42318
0fd33b6b22cf corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
boehmes
parents: 42196
diff changeset
   589
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   590
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   591
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   592
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   593
(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   594
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   595
  named ctxt "fast" (Old_Z3_Proof_Tools.by_tac ctxt (HOL_fast_tac ctxt))]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   596
    (* FIXME: not very well tested *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   597
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   598
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   599
(* |- ~(ALL x1...xn. P x1...xn) | P a1...an *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   600
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   601
  val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   602
in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   603
fun quant_inst ctxt = Thm o Old_Z3_Proof_Tools.by_tac ctxt (
58957
c9e744ea8a38 proper context for match_tac etc.;
wenzelm
parents: 58059
diff changeset
   604
  REPEAT_ALL_NEW (match_tac ctxt [rule])
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60642
diff changeset
   605
  THEN' resolve_tac ctxt @{thms excluded_middle})
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   606
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   607
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   608
42196
9893b2913a44 save reflexivity steps in discharging Z3 Skolemization hypotheses
boehmes
parents: 42191
diff changeset
   609
(* |- (EX x. P x) = P c     |- ~(ALL x. P x) = ~ P c *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   610
local
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   611
  val forall =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   612
    Old_SMT_Utils.mk_const_pat @{theory} @{const_name Pure.all}
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   613
      (Old_SMT_Utils.destT1 o Old_SMT_Utils.destT1)
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   614
  fun mk_forall cv ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   615
    Thm.apply (Old_SMT_Utils.instT' cv forall) (Thm.lambda cv ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   616
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   617
  fun get_vars f mk pred ctxt t =
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   618
    Term.fold_aterms f t []
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   619
    |> map_filter (fn v =>
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59590
diff changeset
   620
         if pred v then SOME (Thm.cterm_of ctxt (mk v)) else NONE)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   621
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   622
  fun close vars f ct ctxt =
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   623
    let
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   624
      val frees_of = get_vars Term.add_frees Free (member (op =) vars o fst)
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   625
      val vs = frees_of ctxt (Thm.term_of ct)
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   626
      val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   627
      val vars_of = get_vars Term.add_vars Var (K true) ctxt'
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59621
diff changeset
   628
    in
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59621
diff changeset
   629
      (Thm.instantiate ([], map (dest_Var o Thm.term_of) (vars_of (Thm.prop_of thm)) ~~ vs) thm,
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59621
diff changeset
   630
        ctxt')
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59621
diff changeset
   631
    end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   632
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   633
  val sk_rules = @{lemma
44488
587bf61a00a1 improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents: 44058
diff changeset
   634
    "c = (SOME x. P x) ==> (EX x. P x) = P c"
587bf61a00a1 improved completeness and efficiency of Z3 proof reconstruction, especially by an improved handling of Skolemization
boehmes
parents: 44058
diff changeset
   635
    "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)"
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   636
    by (metis someI_ex)+}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   637
in
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   638
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   639
fun skolemize vars =
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   640
  apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   641
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   642
fun discharge_sk_tac ctxt i st = (
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60642
diff changeset
   643
  resolve_tac ctxt @{thms trans} i
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   644
  THEN resolve_tac ctxt sk_rules i
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60642
diff changeset
   645
  THEN (resolve_tac ctxt @{thms refl} ORELSE' discharge_sk_tac ctxt) (i+1)
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60642
diff changeset
   646
  THEN resolve_tac ctxt @{thms refl} i) st
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   647
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   648
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   649
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   650
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   651
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   652
(** theory proof rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   653
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   654
(* theory lemmas: linear arithmetic, arrays *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   655
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   656
  Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' =>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   657
    Old_Z3_Proof_Tools.by_tac ctxt' (
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   658
      NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   659
      ORELSE' NAMED ctxt' "simp+arith" (
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49980
diff changeset
   660
        Simplifier.asm_full_simp_tac (put_simpset simpset ctxt')
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   661
        THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   662
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   663
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   664
(* rewriting: prove equalities:
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   665
     * ACI of conjunction/disjunction
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   666
     * contradiction, excluded middle
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   667
     * logical rewriting rules (for negation, implication, equivalence,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   668
         distinct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   669
     * normal forms for polynoms (integer/real arithmetic)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   670
     * quantifier elimination over linear arithmetic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   671
     * ... ? **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   672
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   673
  fun spec_meta_eq_of thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   674
    (case try (fn th => th RS @{thm spec}) thm of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   675
      SOME thm' => spec_meta_eq_of thm'
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   676
    | NONE => mk_meta_eq thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   677
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   678
  fun prep (Thm thm) = spec_meta_eq_of thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   679
    | prep (MetaEq thm) = thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   680
    | prep (Literals (thm, _)) = spec_meta_eq_of thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   681
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   682
  fun unfold_conv ctxt ths =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   683
    Conv.arg_conv (Conv.binop_conv (Old_Z3_Proof_Tools.unfold_eqs ctxt
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   684
      (map prep ths)))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   685
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   686
  fun with_conv _ [] prv = prv
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   687
    | with_conv ctxt ths prv =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   688
        Old_Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   689
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   690
  val unfold_conv =
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   691
    Conv.arg_conv (Conv.binop_conv
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   692
      (Conv.try_conv Old_Z3_Proof_Tools.unfold_distinct_conv))
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   693
  val prove_conj_disj_eq =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   694
    Old_Z3_Proof_Tools.with_conv unfold_conv Old_Z3_Proof_Literals.prove_conj_disj_eq
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   695
41899
83dd157ec9ab finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents: 41426
diff changeset
   696
  fun declare_hyps ctxt thm =
60949
ccbf9379e355 added Thm.chyps_of;
wenzelm
parents: 60752
diff changeset
   697
    (thm, snd (Assumption.add_assumes (Thm.chyps_of thm) ctxt))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   698
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   699
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   700
val abstraction_depth = 3
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   701
  (*
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   702
    This value was chosen large enough to potentially catch exceptions,
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   703
    yet small enough to not cause too much harm.  The value might be
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   704
    increased in the future, if reconstructing 'rewrite' fails on problems
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   705
    that get too much abstracted to be reconstructable.
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   706
  *)
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   707
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   708
fun rewrite simpset ths ct ctxt =
41899
83dd157ec9ab finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents: 41426
diff changeset
   709
  apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   710
    named ctxt "conj/disj/distinct" prove_conj_disj_eq,
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   711
    named ctxt "pull-ite" Old_Z3_Proof_Methods.prove_ite ctxt,
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   712
    Old_Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   713
      Old_Z3_Proof_Tools.by_tac ctxt' (
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49980
diff changeset
   714
        NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   715
        THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   716
    Old_Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   717
      Old_Z3_Proof_Tools.by_tac ctxt' (
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60642
diff changeset
   718
        (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49980
diff changeset
   719
        THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   720
        THEN_ALL_NEW (
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   721
          NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   722
          ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   723
    Old_Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   724
      Old_Z3_Proof_Tools.by_tac ctxt' (
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60642
diff changeset
   725
        (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49980
diff changeset
   726
        THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   727
        THEN_ALL_NEW (
42793
88bee9f6eec7 proper Proof.context for classical tactics;
wenzelm
parents: 42361
diff changeset
   728
          NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   729
          ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   730
    named ctxt "injectivity" (Old_Z3_Proof_Methods.prove_injectivity ctxt),
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   731
    Old_Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   732
      (fn ctxt' =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   733
        Old_Z3_Proof_Tools.by_tac ctxt' (
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60642
diff changeset
   734
          (resolve_tac ctxt' @{thms iff_allI} ORELSE' K all_tac)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 49980
diff changeset
   735
          THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   736
          THEN_ALL_NEW (
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   737
            NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   738
            ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42793
diff changeset
   739
              ctxt'))))]) ct))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   740
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   741
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   742
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   743
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   744
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   745
(* proof reconstruction *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   746
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   747
(** tracing and checking **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   748
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   749
fun trace_before ctxt idx = Old_SMT_Config.trace_msg ctxt (fn r =>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   750
  "Z3: #" ^ string_of_int idx ^ ": " ^ Old_Z3_Proof_Parser.string_of_rule r)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   751
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   752
fun check_after idx r ps ct (p, (ctxt, _)) =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   753
  if not (Config.get ctxt Old_SMT_Config.trace) then ()
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   754
  else
64574
1134e4d5e5b7 consolidate nested thms with persistent result, for improved performance;
wenzelm
parents: 61268
diff changeset
   755
    let
1134e4d5e5b7 consolidate nested thms with persistent result, for improved performance;
wenzelm
parents: 61268
diff changeset
   756
      val thm = thm_of p
1134e4d5e5b7 consolidate nested thms with persistent result, for improved performance;
wenzelm
parents: 61268
diff changeset
   757
      val _ = Thm.consolidate thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   758
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   759
      if (Thm.cprop_of thm) aconvc ct then ()
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   760
      else
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   761
        z3_exn (Pretty.string_of (Pretty.big_list
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   762
          ("proof step failed: " ^ quote (Old_Z3_Proof_Parser.string_of_rule r) ^
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   763
            " (#" ^ string_of_int idx ^ ")")
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   764
          (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   765
            [Pretty.block [Pretty.str "expected: ",
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   766
              Syntax.pretty_term ctxt (Thm.term_of ct)]])))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   767
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   768
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   769
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   770
(** overall reconstruction procedure **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   771
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   772
local
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   773
  fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   774
    quote (Old_Z3_Proof_Parser.string_of_rule r))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   775
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   776
  fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) =
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   777
    (case (r, ps) of
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   778
      (* core rules *)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   779
      (Old_Z3_Proof_Parser.True_Axiom, _) => (Thm Old_Z3_Proof_Literals.true_thm, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   780
    | (Old_Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion"
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   781
    | (Old_Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion"
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   782
    | (Old_Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) =>
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   783
        (mp q (thm_of p), cxp)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   784
    | (Old_Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) =>
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   785
        (mp q (thm_of p), cxp)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   786
    | (Old_Z3_Proof_Parser.And_Elim, [(p, i)]) =>
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   787
        and_elim (p, i) ct ptab ||> pair cx
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   788
    | (Old_Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) =>
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   789
        not_or_elim (p, i) ct ptab ||> pair cx
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   790
    | (Old_Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   791
    | (Old_Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   792
    | (Old_Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) =>
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   793
        (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   794
    | (Old_Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   795
    | (Old_Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   796
    | (Old_Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   797
    | (Old_Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   798
    | (Old_Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   799
    | (Old_Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   800
    | (Old_Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   801
    | (Old_Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   802
    | (Old_Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   803
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   804
      (* equality rules *)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   805
    | (Old_Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   806
    | (Old_Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   807
    | (Old_Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   808
    | (Old_Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   809
    | (Old_Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp)
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   810
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   811
      (* quantifier rules *)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   812
    | (Old_Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro cx vars p ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   813
    | (Old_Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   814
    | (Old_Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   815
    | (Old_Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   816
    | (Old_Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   817
    | (Old_Z3_Proof_Parser.Quant_Inst, _) => (quant_inst cx ct, cxp)
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   818
    | (Old_Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   819
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   820
      (* theory rules *)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   821
    | (Old_Z3_Proof_Parser.Th_Lemma _, _) =>  (* FIXME: use arguments *)
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   822
        (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   823
    | (Old_Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   824
    | (Old_Z3_Proof_Parser.Rewrite_Star, ps) =>
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   825
        rewrite simpset (map fst ps) ct cx ||> rpair ptab
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   826
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   827
    | (Old_Z3_Proof_Parser.Nnf_Star, _) => not_supported r
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   828
    | (Old_Z3_Proof_Parser.Cnf_Star, _) => not_supported r
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   829
    | (Old_Z3_Proof_Parser.Transitivity_Star, _) => not_supported r
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   830
    | (Old_Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   831
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   832
    | _ => raise Fail ("Z3: proof rule " ^
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   833
        quote (Old_Z3_Proof_Parser.string_of_rule r) ^
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   834
        " has an unexpected number of arguments."))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   835
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   836
  fun lookup_proof ptab idx =
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   837
    (case Inttab.lookup ptab idx of
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   838
      SOME p => (p, idx)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   839
    | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   840
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   841
  fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) =
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   842
    let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   843
      val Old_Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   844
      val ps = map (lookup_proof ptab) prems
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   845
      val _ = trace_before ctxt idx r
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   846
      val (thm, (ctxt', ptab')) =
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   847
        cxp
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   848
        |> prove_step simpset vars r ps prop
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   849
        |> tap (check_after idx r ps prop)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   850
    in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   851
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   852
  fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   853
    @{thm reflexive}, Old_Z3_Proof_Literals.true_thm]
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   854
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   855
  fun discharge_assms_tac ctxt rules =
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   856
    REPEAT (HEADGOAL (resolve_tac ctxt rules ORELSE' SOLVED' (discharge_sk_tac ctxt)))
64574
1134e4d5e5b7 consolidate nested thms with persistent result, for improved performance;
wenzelm
parents: 61268
diff changeset
   857
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   858
  fun discharge_assms ctxt rules thm =
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   859
    if Thm.nprems_of thm = 0 then Goal.norm_result ctxt thm
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   860
    else
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 59058
diff changeset
   861
      (case Seq.pull (discharge_assms_tac ctxt rules thm) of
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   862
        SOME (thm', _) => Goal.norm_result ctxt thm'
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   863
      | NONE => raise THM ("failed to discharge premise", 1, [thm]))
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   864
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   865
  fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   866
    thm_of p
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42318
diff changeset
   867
    |> singleton (Proof_Context.export inner_ctxt outer_ctxt)
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54742
diff changeset
   868
    |> discharge_assms outer_ctxt (make_discharge_rules rules)
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   869
in
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   870
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   871
fun reconstruct outer_ctxt recon output =
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   872
  let
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   873
    val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41172
diff changeset
   874
    val (asserted, steps, vars, ctxt1) =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   875
      Old_Z3_Proof_Parser.parse ctxt typs terms output
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   876
57957
e6ee35b8f4b5 updated to named_theorems;
wenzelm
parents: 56245
diff changeset
   877
    val simpset =
58059
4e477dcd050a prefixed all old SMT commands, attributes, etc., with 'old_'
blanchet
parents: 58058
diff changeset
   878
      Old_Z3_Proof_Tools.make_simpset ctxt1 (Named_Theorems.get ctxt1 @{named_theorems old_z3_simp})
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   879
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   880
    val ((is, rules), cxp as (ctxt2, _)) =
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   881
      add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   882
  in
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   883
    if Config.get ctxt2 Old_SMT_Config.filter_only_facts then (is, @{thm TrueI})
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   884
    else
41131
fc9d503c3d67 fixed proof reconstruction for lambda-lifted problems (which broke when the lambda-lifting code was changed to operate on terms instead of on theorems)
boehmes
parents: 41130
diff changeset
   885
      (Thm @{thm TrueI}, cxp)
64574
1134e4d5e5b7 consolidate nested thms with persistent result, for improved performance;
wenzelm
parents: 61268
diff changeset
   886
      |> fold (prove simpset vars) steps
42191
09377c05c561 re-implemented proof reconstruction for Z3 skolemization: do not explicitly construct definitions for Skolem constants, and let higher-order resolution do most of the work in the end
boehmes
parents: 41899
diff changeset
   887
      |> discharge rules outer_ctxt
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   888
      |> pair []
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   889
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   890
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 40162
diff changeset
   891
end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   892
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   893
end