src/HOL/Tools/SMT/z3_proof_reconstruction.ML
author boehmes
Wed, 15 Dec 2010 10:12:48 +0100
changeset 41130 130771a48c70
parent 41127 2ea84c8535c6
child 41131 fc9d503c3d67
permissions -rw-r--r--
adapted the Z3 proof parser to recent changes in Z3's proof format; keep the proof steps in an ordered list instead of in an Inttab (simplifies proof reconstruction code)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     1
(*  Title:      HOL/Tools/SMT/z3_proof_reconstruction.ML
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
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     7
signature Z3_PROOF_RECONSTRUCTION =
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
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
    10
  val reconstruct: Proof.context -> SMT_Translate.recon -> string list ->
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
    11
    int list * thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    12
  val setup: theory -> theory
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    13
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    14
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
structure P = Z3_Proof_Parser
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
structure T = Z3_Proof_Tools
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
structure L = Z3_Proof_Literals
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents: 40579
diff changeset
    21
structure M = Z3_Proof_Methods
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40274
diff changeset
    23
fun z3_exn msg = raise SMT_Failure.SMT (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
    24
  ("Z3 proof reconstruction: " ^ msg))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    27
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
    28
(* net of schematic rules *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    30
val z3_ruleN = "z3_rule"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
  val description = "declaration of Z3 proof rules"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
  val eq = Thm.eq_thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
  structure Z3_Rules = Generic_Data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
  (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    39
    type T = thm Net.net
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
    val empty = Net.empty
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
    val extend = I
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
    val merge = Net.merge eq
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
  )
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
  val prep = `Thm.prop_of o Simplifier.rewrite_rule [L.rewrite_true]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
  fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
  fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
  val add = Thm.declaration_attribute (Z3_Rules.map o ins)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    51
  val del = Thm.declaration_attribute (Z3_Rules.map o del)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    54
val add_z3_rule = Z3_Rules.map o ins
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
fun by_schematic_rule ctxt ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
  the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
val z3_rules_setup =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
  Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
39557
fe5722fce758 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents: 39020
diff changeset
    61
  Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
    67
(* proof tools *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
fun named ctxt name prover ct =
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40274
diff changeset
    70
  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    71
  in prover ct end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
fun NAMED ctxt name tac i st =
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40274
diff changeset
    74
  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
  in tac i st end
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 pretty_goal ctxt thms t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
  [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
  |> not (null thms) ? cons (Pretty.big_list "assumptions:"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
       (map (Display.pretty_thm ctxt) thms))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
fun try_apply ctxt thms =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
    fun try_apply_err ct = Pretty.string_of (Pretty.chunks [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
      Pretty.big_list ("Z3 found a proof," ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
        " but proof reconstruction failed at the following subgoal:")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
        (pretty_goal ctxt thms (Thm.term_of ct)),
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
      Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
        " might solve this problem.")])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
    fun apply [] ct = error (try_apply_err ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
      | apply (prover :: provers) ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
          (case try prover ct of
40424
7550b2cba1cb better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
boehmes
parents: 40274
diff changeset
    94
            SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
          | NONE => apply provers ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
  in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    99
local
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   100
  val rewr_if =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   101
    @{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
   102
in
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   103
val simp_fast_tac =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   104
  Simplifier.simp_tac (HOL_ss addsimps [rewr_if])
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   105
  THEN_ALL_NEW Classical.fast_tac HOL_cs
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   106
end
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   107
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   110
(* theorems and proofs *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   111
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   112
(** theorem incarnations **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
datatype theorem =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
  Thm of thm | (* theorem without special features *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
  MetaEq of thm | (* meta equality "t == s" *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
  Literals of thm * L.littab
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
    (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
fun thm_of (Thm thm) = thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
  | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
  | thm_of (Literals (thm, _)) = thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
fun meta_eq_of (MetaEq thm) = thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
  | meta_eq_of p = mk_meta_eq (thm_of p)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
fun literals_of (Literals (_, lits)) = lits
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
  | literals_of p = L.make_littab [thm_of p]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
(** core proof rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
(* assumption *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
  val remove_trigger = @{lemma "trigger t p == p"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
    by (rule eq_reflection, rule trigger_def)}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   138
40664
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   139
  val remove_weight = @{lemma "weight w p == p"
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   140
    by (rule eq_reflection, rule weight_def)}
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   141
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   142
  val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
e023788a91a1 added support for quantifier weight annotations
boehmes
parents: 40663
diff changeset
   143
    L.rewrite_true]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
  fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   146
    (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
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
   148
  fun rewrites f ctxt eqs = map (f (Conv.fconv_rule (rewrite_conv ctxt eqs)))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
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
   150
  fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   151
  fun lookup_assm ctxt assms ct =
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
   152
    (case T.net_instance' burrow_snd_option assms ct 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
   153
      SOME ithm => ithm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
    | _ => z3_exn ("not asserted: " ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
        quote (Syntax.string_of_term ctxt (Thm.term_of ct))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
in
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
   157
fun prepare_assms ctxt rewrite_rules assms =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
  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
   159
    val eqs = rewrites I ctxt [L.rewrite_true] rewrite_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
   160
    val assms' =
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
   161
      assms
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   162
      |> rewrites apsnd ctxt (union Thm.eq_thm eqs prep_rules)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   163
      |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   164
  in (eqs, T.thm_net_of snd assms') end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
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
   166
fun asserted ctxt (eqs, assms) ct =
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
  let val revert_conv = rewrite_conv ctxt eqs then_conv Thm.eta_conversion
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
   168
  in Thm (T.with_conv revert_conv (snd o lookup_assm ctxt assms) ct) end
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
   169
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
   170
fun find_assm ctxt (unfolds, assms) ct =
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
   171
  fst (lookup_assm ctxt assms (Thm.rhs_of (rewrite_conv ctxt unfolds ct)))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
(* P = Q ==> P ==> Q   or   P --> Q ==> P ==> Q *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
  val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
  val meta_iffD1_c = T.precompose2 Thm.dest_binop meta_iffD1
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
  val iffD1_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
  val mp_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm mp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (T.compose meta_iffD1_c thm) p)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
  | mp p_q p = 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
      let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
        val pq = thm_of p_q
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
        val thm = T.compose iffD1_c pq handle THM _ => T.compose mp_c pq
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
      in Thm (Thm.implies_elim thm p) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
(* and_elim:     P1 & ... & Pn ==> Pi *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
(* not_or_elim:  ~(P1 | ... | Pn) ==> ~Pi *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
  fun is_sublit conj t = L.exists_lit conj (fn u => u aconv t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
  fun derive conj t lits idx ptab =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
      val lit = the (L.get_first_lit (is_sublit conj t) lits)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
      val ls = L.explode conj false false [t] lit
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
      val lits' = fold L.insert_lit ls (L.delete_lit lit lits)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   203
      fun upd thm = Literals (thm_of thm, lits')
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
    in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
  fun lit_elim conj (p, idx) ct ptab =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
    let val lits = literals_of p
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   209
      (case L.lookup_lit lits (T.term_of ct) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
        SOME lit => (Thm lit, ptab)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   211
      | NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
val and_elim = lit_elim true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
val not_or_elim = lit_elim false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   218
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
(* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   220
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   221
  fun step lit thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   222
    Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   223
  val explode_disj = L.explode false false false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
  fun intro hyps thm th = fold step (explode_disj hyps th) thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   226
  fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   227
  val ccontr = T.precompose dest_ccontr @{thm ccontr}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
fun lemma thm ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
  let
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
   231
    val cu = L.negate (Thm.dest_arg ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
    val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
  in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
  val explode_disj = L.explode false true false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
  val join_disj = L.join false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
  fun unit thm thms th =
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
   242
    let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
    in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
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 dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
  fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
  val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
fun unit_resolution thm thms 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
   250
  L.negate (Thm.dest_arg ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
  |> T.under_assumption (unit thm thms)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
  |> Thm o T.discharge thm o T.compose contrapos
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
(* P ==> P == True   or   P ==> P == False *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
  val iff1 = @{lemma "P ==> P == (~ False)" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
  val iff2 = @{lemma "~P ==> P == False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   261
fun iff_true thm = MetaEq (thm COMP iff1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
fun iff_false thm = MetaEq (thm COMP iff2)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
(* distributivity of | over & *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
fun distributivity ctxt = Thm o try_apply ctxt [] [
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   268
  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
    (* FIXME: not very well tested *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
(* Tseitin-like axioms *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
  val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
  val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
  val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
  val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
  fun prove' conj1 conj2 ct2 thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
    let val lits = L.true_thm :: L.explode conj1 true (conj1 <> conj2) [] thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
    in L.join conj2 (L.make_littab lits) (Thm.term_of ct2) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
  fun prove rule (ct1, conj1) (ct2, conj2) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
    T.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   286
  fun prove_def_axiom ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
    let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
      (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
   290
        @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   291
          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
   292
      | @{const HOL.conj} $ _ $ _ =>
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
   293
          prove disjI3 (L.negate ct2, false) (ct1, true)
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
   294
      | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
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
   295
          prove disjI3 (L.negate ct2, false) (ct1, false)
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
   296
      | @{const HOL.disj} $ _ $ _ =>
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
   297
          prove disjI2 (L.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
   298
      | Const (@{const_name distinct}, _) $ _ =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
          let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
            fun prv cu =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
              let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
              in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
          in T.with_conv (dis_conv T.unfold_distinct_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
   305
      | @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
          let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
            fun prv cu =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   309
              let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
              in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   311
          in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
      | _ => raise CTERM ("prove_def_axiom", [ct]))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   313
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   314
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   315
fun def_axiom ctxt = Thm o try_apply ctxt [] [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   316
  named ctxt "conj/disj/distinct" prove_def_axiom,
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   317
  T.by_abstraction (true, false) ctxt [] (fn ctxt' =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   318
    named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   319
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   320
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   321
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   322
(* local definitions *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   323
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   324
  val intro_rules = [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   325
    @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   326
    @{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
   327
      by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   328
    @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   329
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   330
  val apply_rules = [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   331
    @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   332
    @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   333
      by (atomize(full)) fastsimp} ]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   334
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   335
  val inst_rule = T.match_instantiate Thm.dest_arg
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   336
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   337
  fun apply_rule ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   338
    (case get_first (try (inst_rule ct)) intro_rules of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   339
      SOME thm => thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   340
    | NONE => raise CTERM ("intro_def", [ct]))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   341
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   342
fun intro_def ct = T.make_hyp_def (apply_rule ct) #>> Thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   343
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   344
fun apply_def thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   345
  get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   346
  |> the_default (Thm thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   347
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   348
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   349
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   350
(* negation normal form *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   351
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   352
  val quant_rules1 = ([
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   353
    @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   354
    @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   355
    @{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
   356
    @{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
   357
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   358
  val quant_rules2 = ([
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   359
    @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp},
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   360
    @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   361
    @{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
   362
    @{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
   363
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   364
  fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   365
    Tactic.rtac thm ORELSE'
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   366
    (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   367
    (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   368
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   369
  fun nnf_quant vars qs p ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   370
    T.as_meta_eq ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   371
    |> T.by_tac (nnf_quant_tac (T.varify vars (meta_eq_of p)) qs)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   372
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   373
  fun prove_nnf ctxt = try_apply ctxt [] [
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   374
    named ctxt "conj/disj" L.prove_conj_disj_eq,
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   375
    T.by_abstraction (true, false) ctxt [] (fn ctxt' =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   376
      named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   377
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   378
fun nnf ctxt vars ps ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   379
  (case T.term_of ct of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   380
    _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   381
      if l aconv r
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   382
      then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   383
      else MetaEq (nnf_quant 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
   384
  | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   385
      MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   386
  | _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   387
      let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   388
        val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   389
          (T.unfold_eqs ctxt (map (Thm.symmetric o meta_eq_of) ps)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   390
      in Thm (T.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   391
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   392
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   393
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   394
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   395
(** equality proof rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   396
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   397
(* |- t = t *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   398
fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
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
(* s = t ==> t = s *)
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 symm_rule = @{lemma "s = t ==> t == s" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   404
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   405
fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   406
  | symm p = MetaEq (thm_of p COMP symm_rule)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   407
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   408
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   409
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   410
(* s = t ==> t = u ==> s = u *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   411
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   412
  val trans1 = @{lemma "s == t ==> t =  u ==> s == u" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   413
  val trans2 = @{lemma "s =  t ==> t == u ==> s == u" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   414
  val trans3 = @{lemma "s =  t ==> t =  u ==> s == u" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   415
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   416
fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   417
  | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   418
  | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   419
  | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   420
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   421
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   422
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   423
(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   424
   (reflexive antecendents are droppped) *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   425
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   426
  exception MONO
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   427
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   428
  fun prove_refl (ct, _) = Thm.reflexive ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   429
  fun prove_comb f g cp =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   430
    let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   431
    in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   432
  fun prove_arg f = prove_comb prove_refl f
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   433
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   434
  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
   435
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   436
  fun prove_nary is_comb f =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   437
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   438
      fun prove (cp as (ct, _)) = f cp handle MONO =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   439
        if is_comb (Thm.term_of ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   440
        then prove_comb (prove_arg prove) prove cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   441
        else prove_refl cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   442
    in prove end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   443
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   444
  fun prove_list f n cp =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   445
    if n = 0 then prove_refl cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   446
    else prove_comb (prove_arg f) (prove_list f (n-1)) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   447
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   448
  fun with_length f (cp as (cl, _)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   449
    f (length (HOLogic.dest_list (Thm.term_of cl))) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   450
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   451
  fun prove_distinct f = prove_arg (with_length (prove_list f))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   452
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   453
  fun prove_eq exn lookup cp =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   454
    (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   455
      SOME eq => eq
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   456
    | NONE => if exn then raise MONO else prove_refl cp)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   457
  
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   458
  val prove_eq_exn = prove_eq true
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   459
  and prove_eq_safe = prove_eq false
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   460
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   461
  fun mono f (cp as (cl, _)) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   462
    (case Term.head_of (Thm.term_of cl) 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
   463
      @{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
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
   464
    | @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
40681
872b08416fb4 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents: 40680
diff changeset
   465
    | Const (@{const_name distinct}, _) => prove_distinct (prove_eq_safe f)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   466
    | _ => prove (prove_eq_safe f)) cp
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   467
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   468
fun monotonicity eqs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   469
  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
   470
    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
   471
    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
   472
    val lookup = AList.lookup (op aconv) teqs
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   473
    val cp = Thm.dest_binop (Thm.dest_arg ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   474
  in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end
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
(* |- f a b = f b a (where f is equality) *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   479
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   480
  val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   481
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   482
fun commutativity ct = MetaEq (T.match_instantiate I (T.as_meta_eq ct) rule)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   483
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   484
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   485
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   486
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   487
(** quantifier proof rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   488
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   489
(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   490
   P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x)    *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   491
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   492
  val rules = [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   493
    @{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
   494
    @{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
   495
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   496
fun quant_intro vars p ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   497
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   498
    val thm = meta_eq_of p
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   499
    val rules' = T.varify vars thm :: rules
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   500
    val cu = T.as_meta_eq ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   501
  in MetaEq (T.by_tac (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   502
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   503
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   504
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   505
(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   506
fun pull_quant ctxt = Thm o try_apply ctxt [] [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   507
  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   508
    (* FIXME: not very well tested *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   509
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   510
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   511
(* |- (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
   512
fun push_quant ctxt = Thm o try_apply ctxt [] [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   513
  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   514
    (* FIXME: not very well tested *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   515
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   516
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   517
(* |- (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
   518
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   519
  val elim_all = @{lemma "(ALL x. P) == P" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   520
  val elim_ex = @{lemma "(EX x. P) == P" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   521
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   522
  fun elim_unused_conv ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   523
    Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
   524
      (Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   525
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   526
  fun elim_unused_tac ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   527
    REPEAT_ALL_NEW (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   528
      Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   529
      ORELSE' CONVERSION (elim_unused_conv ctxt))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   530
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   531
fun elim_unused_vars ctxt = Thm o T.by_tac (elim_unused_tac ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   532
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   533
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   534
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   535
(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   536
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   537
  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   538
    (* FIXME: not very well tested *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   539
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   540
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   541
(* |- ~(ALL x1...xn. P x1...xn) | P a1...an *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   542
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   543
  val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   544
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   545
val quant_inst = Thm o T.by_tac (
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   546
  REPEAT_ALL_NEW (Tactic.match_tac [rule])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   547
  THEN' Tactic.rtac @{thm excluded_middle})
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   548
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   549
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   550
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   551
(* c = SOME x. P x |- (EX x. P x) = P c
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   552
   c = SOME x. ~ P x |- ~(ALL x. P x) = ~ P c *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   553
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   554
  val elim_ex = @{lemma "EX x. P == P" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   555
  val elim_all = @{lemma "~ (ALL x. P) == ~P" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   556
  val sk_ex = @{lemma "c == SOME x. P x ==> EX x. P x == P c"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   557
    by simp (intro eq_reflection some_eq_ex[symmetric])}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   558
  val sk_all = @{lemma "c == SOME x. ~ P x ==> ~(ALL x. P x) == ~ P c"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   559
    by (simp only: not_all) (intro eq_reflection some_eq_ex[symmetric])}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   560
  val sk_ex_rule = ((sk_ex, I), elim_ex)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   561
  and sk_all_rule = ((sk_all, Thm.dest_arg), elim_all)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   562
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   563
  fun dest f sk_rule = 
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   564
    Thm.dest_comb (f (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of sk_rule))))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   565
  fun type_of f sk_rule = Thm.ctyp_of_term (snd (dest f sk_rule))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   566
  fun pair2 (a, b) (c, d) = [(a, c), (b, d)]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   567
  fun inst_sk (sk_rule, f) p c =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   568
    Thm.instantiate ([(type_of f sk_rule, Thm.ctyp_of_term c)], []) sk_rule
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   569
    |> (fn sk' => Thm.instantiate ([], (pair2 (dest f sk') (p, c))) sk')
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   570
    |> Conv.fconv_rule (Thm.beta_conversion true)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   571
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   572
  fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
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
   573
    | kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) =
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
   574
        (sk_all_rule, Thm.dest_arg, L.negate)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   575
    | kind t = raise TERM ("skolemize", [t])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   576
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   577
  fun dest_abs_type (Abs (_, T, _)) = T
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   578
    | dest_abs_type t = raise TERM ("dest_abs_type", [t])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   579
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   580
  fun bodies_of thy lhs rhs =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   581
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   582
      val (rule, dest, make) = kind (Thm.term_of lhs)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   583
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   584
      fun dest_body idx cbs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   585
        let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   586
          val cb = Thm.dest_arg (dest ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   587
          val T = dest_abs_type (Thm.term_of cb)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   588
          val cv = Thm.cterm_of thy (Var (("x", idx), T))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   589
          val cu = make (Drule.beta_conv cb cv)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   590
          val cbs' = (cv, cb) :: cbs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   591
        in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   592
          (snd (Thm.first_order_match (cu, rhs)), rev cbs')
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   593
          handle Pattern.MATCH => dest_body (idx+1) cbs' cu
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   594
        end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   595
    in (rule, dest_body 1 [] lhs) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   596
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   597
  fun transitive f thm = Thm.transitive thm (f (Thm.rhs_of thm))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   598
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   599
  fun sk_step (rule, elim) (cv, mct, cb) ((is, thm), ctxt) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   600
    (case mct of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   601
      SOME ct =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   602
        ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   603
        |> T.make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   604
        |>> pair ((cv, ct) :: is) o Thm.transitive thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   605
    | NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   606
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   607
fun skolemize ct ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   608
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   609
    val (lhs, rhs) = Thm.dest_binop (Thm.dest_arg ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   610
    val (rule, (ctab, cbs)) = bodies_of (ProofContext.theory_of ctxt) lhs rhs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   611
    fun lookup_var (cv, cb) = (cv, AList.lookup (op aconvc) ctab cv, cb)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   612
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   613
    (([], Thm.reflexive lhs), ctxt)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   614
    |> fold (sk_step rule) (map lookup_var cbs)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   615
    |>> MetaEq o snd
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   616
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   617
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   618
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   619
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   620
(** theory proof rules **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   621
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   622
(* theory lemmas: linear arithmetic, arrays *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   623
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   624
  T.by_abstraction (false, true) ctxt thms (fn ctxt' => T.by_tac (
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   625
    NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   626
    ORELSE' NAMED ctxt' "simp+arith" (Simplifier.simp_tac simpset THEN_ALL_NEW
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   627
      Arith_Data.arith_tac ctxt')))]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   628
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   629
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   630
(* rewriting: prove equalities:
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   631
     * ACI of conjunction/disjunction
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   632
     * contradiction, excluded middle
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   633
     * logical rewriting rules (for negation, implication, equivalence,
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   634
         distinct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   635
     * normal forms for polynoms (integer/real arithmetic)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   636
     * quantifier elimination over linear arithmetic
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   637
     * ... ? **)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   638
structure Z3_Simps = Named_Thms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   639
(
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   640
  val name = "z3_simp"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   641
  val description = "simplification rules for Z3 proof reconstruction"
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   642
)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   643
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   644
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   645
  fun spec_meta_eq_of thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   646
    (case try (fn th => th RS @{thm spec}) thm of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   647
      SOME thm' => spec_meta_eq_of thm'
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   648
    | NONE => mk_meta_eq thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   649
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   650
  fun prep (Thm thm) = spec_meta_eq_of thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   651
    | prep (MetaEq thm) = thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   652
    | prep (Literals (thm, _)) = spec_meta_eq_of thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   653
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   654
  fun unfold_conv ctxt ths =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   655
    Conv.arg_conv (Conv.binop_conv (T.unfold_eqs ctxt (map prep ths)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   656
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   657
  fun with_conv _ [] prv = prv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   658
    | with_conv ctxt ths prv = T.with_conv (unfold_conv ctxt ths) prv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   659
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   660
  val unfold_conv =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   661
    Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   662
  val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   664
  fun assume_prems ctxt thm =
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   665
    Assumption.add_assumes (Drule.cprems_of thm) ctxt
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   666
    |>> (fn thms => fold Thm.elim_implies thms thm)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   667
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   668
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   669
fun rewrite simpset ths ct ctxt =
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   670
  apfst Thm (assume_prems ctxt (with_conv ctxt ths (try_apply ctxt [] [
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   671
    named ctxt "conj/disj/distinct" prove_conj_disj_eq,
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   672
    T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   673
      NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   674
      THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   675
    T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   676
      NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   677
      THEN_ALL_NEW (
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   678
        NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   679
        ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   680
    T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   681
      NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   682
      THEN_ALL_NEW (
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   683
        NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   684
        ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   685
    named ctxt "injectivity" (M.prove_injectivity ctxt)]) ct))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   686
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   687
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   688
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   689
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   690
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   691
(* proof reconstruction *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   692
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   693
(** tracing and checking **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   694
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   695
fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r =>
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   696
  "Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   697
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   698
fun check_after idx r ps ct (p, (ctxt, _)) =
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   699
  if not (Config.get ctxt SMT_Config.trace) then ()
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   700
  else
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   701
    let val thm = thm_of p |> tap (Thm.join_proofs o single)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   702
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   703
      if (Thm.cprop_of thm) aconvc ct then ()
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   704
      else z3_exn (Pretty.string_of (Pretty.big_list ("proof step failed: " ^
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   705
        quote (P.string_of_rule r) ^ " (#" ^ string_of_int idx ^ ")")
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   706
          (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   707
           [Pretty.block [Pretty.str "expected: ",
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   708
            Syntax.pretty_term ctxt (Thm.term_of ct)]])))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   709
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   710
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   711
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   712
(** overall reconstruction procedure **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   713
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
   714
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
   715
  fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
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
   716
    quote (P.string_of_rule r))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   717
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   718
  fun prove_step assms 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
   719
    (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
   720
      (* core rules *)
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   721
      (P.True_Axiom, _) => (Thm L.true_thm, 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
   722
    | (P.Asserted, _) => (asserted cx assms ct, cxp)
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
   723
    | (P.Goal, _) => (asserted cx assms ct, cxp)
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   724
    | (P.Modus_Ponens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   725
    | (P.Modus_Ponens_Oeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   726
    | (P.And_Elim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   727
    | (P.Not_Or_Elim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx
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
   728
    | (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
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
   729
    | (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   730
    | (P.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
   731
        (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   732
    | (P.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   733
    | (P.Iff_False, [(p, _)]) => (iff_false (thm_of p), 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
   734
    | (P.Distributivity, _) => (distributivity cx ct, cxp)
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   735
    | (P.Def_Axiom, _) => (def_axiom cx ct, cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   736
    | (P.Intro_Def, _) => intro_def ct cx ||> rpair ptab
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   737
    | (P.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   738
    | (P.Iff_Oeq, [(p, _)]) => (p, cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   739
    | (P.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   740
    | (P.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   741
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
   742
      (* equality rules *)
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
   743
    | (P.Reflexivity, _) => (refl ct, cxp)
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
   744
    | (P.Symmetry, [(p, _)]) => (symm p, cxp)
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
   745
    | (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
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
   746
    | (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
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
   747
    | (P.Commutativity, _) => (commutativity ct, cxp)
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
   748
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
   749
      (* quantifier rules *)
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   750
    | (P.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   751
    | (P.Pull_Quant, _) => (pull_quant cx ct, cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   752
    | (P.Push_Quant, _) => (push_quant cx ct, cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   753
    | (P.Elim_Unused_Vars, _) => (elim_unused_vars cx ct, cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   754
    | (P.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   755
    | (P.Quant_Inst, _) => (quant_inst 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
   756
    | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
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
   757
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
   758
      (* theory rules *)
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   759
    | (P.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
   760
        (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents: 40579
diff changeset
   761
    | (P.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   762
    | (P.Rewrite_Star, ps) => rewrite simpset (map fst ps) ct cx ||> rpair ptab
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   763
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   764
    | (P.Nnf_Star, _) => not_supported r
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   765
    | (P.Cnf_Star, _) => not_supported r
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   766
    | (P.Transitivity_Star, _) => not_supported r
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   767
    | (P.Pull_Quant_Star, _) => not_supported r
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   768
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
   769
    | _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^
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
   770
       " has an unexpected number of arguments."))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   771
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   772
  fun lookup_proof ptab idx =
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   773
    (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
   774
      SOME p => (p, idx)
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   775
    | 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
   776
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   777
  fun prove assms 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
   778
    let
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   779
      val P.Proof_Step {rule=r, prems, prop, ...} = step
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   780
      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
   781
      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
   782
      val (thm, (ctxt', ptab')) =
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   783
        cxp
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   784
        |> prove_step assms simpset vars r ps prop
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   785
        |> 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
   786
    in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   787
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
   788
  val disch_rules = map (pair false)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   789
    [@{thm allI}, @{thm refl}, @{thm reflexive}]
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   790
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   791
  fun disch_assm 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
   792
    if Thm.nprems_of thm = 0 then Drule.flexflex_unique 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
   793
    else
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   794
      (case Seq.pull (Thm.biresolution false disch_rules 1 thm) of
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   795
        SOME (thm', _) => disch_assm 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
   796
      | 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
   797
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   798
  fun discharge outer_ctxt (p, (inner_ctxt, _)) =
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   799
    thm_of p
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
   800
    |> singleton (ProofContext.export inner_ctxt outer_ctxt)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   801
    |> disch_assm    
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   802
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   803
  fun filter_assms ctxt assms =
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
    let
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   805
      fun add_assm r ct =
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
   806
        (case r 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
   807
          P.Asserted => insert (op =) (find_assm ctxt assms ct)
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
   808
        | P.Goal => insert (op =) (find_assm ctxt assms ct)
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
   809
        | _ => I)
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   810
    in fold (fn (_, P.Proof_Step {rule, prop, ...}) => add_assm rule prop) 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
   811
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
   812
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
   813
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
   814
  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
   815
    val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   816
    val (steps, vars, ctxt') = P.parse ctxt typs terms output
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
   817
    val assms' = prepare_assms ctxt' rewrite_rules assms
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   818
    val simpset = T.make_simpset ctxt' (Z3_Simps.get ctxt')
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   819
  in
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
   820
    if Config.get ctxt' SMT_Config.filter_only_facts then
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   821
      (filter_assms ctxt' assms' steps [], @{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
   822
    else
41130
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   823
      (Thm @{thm TrueI}, (ctxt', Inttab.empty))
130771a48c70 adapted the Z3 proof parser to recent changes in Z3's proof format;
boehmes
parents: 41127
diff changeset
   824
      |> fold (prove assms' simpset vars) steps 
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
   825
      |> discharge outer_ctxt
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 40681
diff changeset
   826
      |> pair []
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   827
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   828
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
   829
end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   830
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
   831
val setup = z3_rules_setup #> Z3_Simps.setup
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   832
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   833
end