src/HOL/Library/Old_SMT/old_z3_proof_tools.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 62913 13252110a6fe
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_z3_proof_tools.ML
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     4
Helper functions required for Z3 proof reconstruction.
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_Z3_PROOF_TOOLS =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
41172
a17c2d669c40 the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents: 41123
diff changeset
     9
  (*modifying terms*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    10
  val as_meta_eq: cterm -> cterm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    11
41123
boehmes
parents: 40806
diff changeset
    12
  (*theorem nets*)
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 38864
diff changeset
    13
  val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
45393
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 44241
diff changeset
    14
  val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    15
  val net_instance: thm Net.net -> cterm -> thm option
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
41123
boehmes
parents: 40806
diff changeset
    17
  (*proof combinators*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
  val under_assumption: (thm -> thm) -> cterm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
  val with_conv: conv -> (cterm -> thm) -> cterm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
  val discharge: thm -> thm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
  val varify: string list -> thm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
  val unfold_eqs: Proof.context -> thm list -> conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
  val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 51717
diff changeset
    24
  val by_tac: Proof.context -> (int -> tactic) -> cterm -> thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
  val make_hyp_def: thm -> Proof.context -> thm * Proof.context
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
    26
  val by_abstraction: int -> bool * bool -> Proof.context -> thm list ->
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    27
    (Proof.context -> cterm -> thm) -> cterm -> thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
41123
boehmes
parents: 40806
diff changeset
    29
  (*a faster COMP*)
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59634
diff changeset
    30
  type compose_data = cterm list * (cterm -> cterm list) * thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
  val precompose: (cterm -> cterm list) -> thm -> compose_data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
  val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
  val compose: compose_data -> thm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
41123
boehmes
parents: 40806
diff changeset
    35
  (*unfolding of 'distinct'*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    36
  val unfold_distinct_conv: conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
41123
boehmes
parents: 40806
diff changeset
    38
  (*simpset*)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    39
  val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    40
  val make_simpset: Proof.context -> thm list -> simpset
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    43
structure Old_Z3_Proof_Tools: OLD_Z3_PROOF_TOOLS =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
41172
a17c2d669c40 the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents: 41123
diff changeset
    48
(* modifying terms *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    49
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
    50
fun as_meta_eq ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    51
  uncurry Old_SMT_Utils.mk_cequals (Thm.dest_binop (Old_SMT_Utils.dest_cprop ct))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    52
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    53
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    54
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    55
(* theorem nets *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
40164
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 38864
diff changeset
    57
fun thm_net_of f xthms =
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 38864
diff changeset
    58
  let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
57f5db2a48a3 added a mode to only filter assumptions used in a Z3 proof (in which no proof reconstruction is performed)
boehmes
parents: 38864
diff changeset
    59
  in fold insert xthms Net.empty end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    60
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
fun maybe_instantiate ct thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
  try Thm.first_order_match (Thm.cprop_of thm, ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
  |> Option.map (fn inst => Thm.instantiate inst thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
42322
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    65
local
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    66
  fun instances_from_net match f net ct =
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    67
    let
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    68
      val lookup = if match then Net.match_term else Net.unify_term
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    69
      val xthms = lookup net (Thm.term_of ct)
45393
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 44241
diff changeset
    70
      fun select ct = map_filter (f (maybe_instantiate ct)) xthms 
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 44241
diff changeset
    71
      fun select' ct =
42322
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    72
        let val thm = Thm.trivial ct
45393
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 44241
diff changeset
    73
        in map_filter (f (try (fn rule => rule COMP thm))) xthms end
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 44241
diff changeset
    74
    in (case select ct of [] => select' ct | xthms' => xthms') end
42322
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    75
in
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    76
45410
d58c25559dc0 made SML/NJ happy
boehmes
parents: 45393
diff changeset
    77
fun net_instances net =
45393
13ab80eafd71 try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
boehmes
parents: 44241
diff changeset
    78
  instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
45410
d58c25559dc0 made SML/NJ happy
boehmes
parents: 45393
diff changeset
    79
    net
42322
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    80
45410
d58c25559dc0 made SML/NJ happy
boehmes
parents: 45393
diff changeset
    81
fun net_instance net = try hd o instances_from_net true I net
42322
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    82
be1c32069daa use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
boehmes
parents: 41899
diff changeset
    83
end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
(* proof combinators *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
fun under_assumption f ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    90
  let val ct' = Old_SMT_Utils.mk_cprop ct
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
  in Thm.implies_intr ct' (f (Thm.assume ct')) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
fun with_conv conv prove ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
  let val eq = Thm.symmetric (conv ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
  in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
fun discharge p pq = Thm.implies_elim pq p
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
fun varify vars = Drule.generalize ([], vars)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
fun unfold_eqs _ [] = Conv.all_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   102
  | unfold_eqs ctxt eqs =
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
   103
      Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
fun match_instantiate f ct thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
  Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 51717
diff changeset
   108
fun by_tac ctxt tac ct = Goal.norm_result ctxt (Goal.prove_internal ctxt [] ct (K (tac 1)))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
41123
boehmes
parents: 40806
diff changeset
   110
(*
boehmes
parents: 40806
diff changeset
   111
   |- c x == t x ==> P (c x)
boehmes
parents: 40806
diff changeset
   112
  ---------------------------
boehmes
parents: 40806
diff changeset
   113
      c == t |- P (c x)
boehmes
parents: 40806
diff changeset
   114
*) 
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
fun make_hyp_def thm ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
    val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
    val (cf, cvs) = Drule.strip_comb lhs
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   119
    val eq = Old_SMT_Utils.mk_cequals cf (fold_rev Thm.lambda cvs rhs)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
    fun apply cv th =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
      Thm.combination th (Thm.reflexive cv)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
      |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
    yield_singleton Assumption.add_assumes eq ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
    |>> Thm.implies_elim thm o fold apply cvs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   129
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
(* abstraction *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
fun context_of (ctxt, _, _, _) = ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   137
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   138
fun replace (_, (cv, ct)) = Thm.forall_elim ct o Thm.forall_intr cv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   140
fun abs_instantiate (_, tab, _, beta_norm) =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   141
  fold replace (Termtab.dest tab) #>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
  beta_norm ? Conv.fconv_rule (Thm.beta_conversion true)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   143
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   144
fun lambda_abstract cvs t =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
  let
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   146
    val frees = map Free (Term.add_frees t [])
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   147
    val cvs' = filter (fn cv => member (op aconv) frees (Thm.term_of cv)) cvs
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   148
    val vs = map (Term.dest_Free o Thm.term_of) cvs'
44241
7943b69f0188 modernized signature of Term.absfree/absdummy;
wenzelm
parents: 43597
diff changeset
   149
  in (fold_rev absfree vs t, cvs') end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   151
fun fresh_abstraction (_, cvs) ct (cx as (ctxt, tab, idx, beta_norm)) =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   152
  let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
    (case Termtab.lookup tab t of
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   155
      SOME (cv, _) => (Drule.list_comb (cv, cvs'), cx)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
    | NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
        let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
          val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59590
diff changeset
   159
          val cv = Thm.cterm_of ctxt'
59586
ddf6deaadfe8 clarified signature;
wenzelm
parents: 58058
diff changeset
   160
            (Free (n, map Thm.typ_of_cterm cvs' ---> Thm.typ_of_cterm ct))
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   161
          val cu = Drule.list_comb (cv, cvs')
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45410
diff changeset
   162
          val e = (t, (cv, fold_rev Thm.lambda cvs' ct))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   163
          val beta_norm' = beta_norm orelse not (null cvs')
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   164
        in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   166
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   167
fun abs_comb f g dcvs ct =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
  let val (cf, cu) = Thm.dest_comb ct
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45410
diff changeset
   169
  in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.apply end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   171
fun abs_arg f = abs_comb (K pair) f
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   172
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   173
fun abs_args f dcvs ct =
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   174
  (case Thm.term_of ct of
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   175
    _ $ _ => abs_comb (abs_args f) f dcvs ct
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   176
  | _ => pair ct)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   177
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   178
fun abs_list f g dcvs ct =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
  (case Thm.term_of ct of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
    Const (@{const_name Nil}, _) => pair ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
  | Const (@{const_name Cons}, _) $ _ $ _ =>
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   182
      abs_comb (abs_arg f) (abs_list f g) dcvs ct
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   183
  | _ => g dcvs ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   185
fun abs_abs f (depth, cvs) ct =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
  let val (cv, cu) = Thm.dest_abs NONE ct
46497
89ccf66aa73d renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents: 45410
diff changeset
   187
  in f (depth, cv :: cvs) cu #>> Thm.lambda cv end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
41899
83dd157ec9ab finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents: 41328
diff changeset
   189
val is_atomic =
83dd157ec9ab finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents: 41328
diff changeset
   190
  (fn Free _ => true | Var _ => true | Bound _ => true | _ => false)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   192
fun abstract depth (ext_logic, with_theories) =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
    fun abstr1 cvs ct = abs_arg abstr cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
    and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
    and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
    and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   199
    and abstr (dcvs as (d, cvs)) ct =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   200
      (case Thm.term_of ct of
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   201
        @{const Trueprop} $ _ => abstr1 dcvs ct
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 54883
diff changeset
   202
      | @{const Pure.imp} $ _ $ _ => abstr2 dcvs 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: 40274
diff changeset
   203
      | @{const True} => pair ct
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: 40274
diff changeset
   204
      | @{const False} => pair ct
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   205
      | @{const Not} $ _ => abstr1 dcvs ct
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   206
      | @{const HOL.conj} $ _ $ _ => abstr2 dcvs ct
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   207
      | @{const HOL.disj} $ _ $ _ => abstr2 dcvs ct
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   208
      | @{const HOL.implies} $ _ $ _ => abstr2 dcvs ct
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   209
      | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 dcvs ct
40681
872b08416fb4 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents: 40663
diff changeset
   210
      | Const (@{const_name distinct}, _) $ _ =>
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   211
          if ext_logic then abs_arg (abs_list abstr fresh_abstraction) dcvs ct
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   212
          else fresh_abstraction dcvs ct
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
      | Const (@{const_name If}, _) $ _ $ _ $ _ =>
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   214
          if ext_logic then abstr3 dcvs ct else fresh_abstraction dcvs ct
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
      | Const (@{const_name All}, _) $ _ =>
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   216
          if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
      | Const (@{const_name Ex}, _) $ _ =>
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   218
          if ext_logic then abstr_abs dcvs ct else fresh_abstraction dcvs ct
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   219
      | t => (fn cx =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   220
          if is_atomic t orelse can HOLogic.dest_number t then (ct, cx)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   221
          else if with_theories andalso
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   222
            Old_Z3_Interface.is_builtin_theory_term (context_of cx) t
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   223
          then abs_args abstr dcvs ct cx
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   224
          else if d = 0 then fresh_abstraction dcvs ct cx
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   225
          else
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   226
            (case Term.strip_comb t of
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   227
              (Const _, _) => abs_args abstr (d-1, cvs) ct cx
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   228
            | (Free _, _) => abs_args abstr (d-1, cvs) ct cx
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   229
            | _ => fresh_abstraction dcvs ct cx)))
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   230
  in abstr (depth, []) end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   232
val cimp = Thm.cterm_of @{context} @{const Pure.imp}
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: 40274
diff changeset
   233
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   234
fun deepen depth f x =
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   235
  if depth = 0 then f depth x
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   236
  else (case try (f depth) x of SOME y => y | NONE => deepen (depth - 1) f x)
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   237
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   238
fun with_prems depth thms f 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: 40274
diff changeset
   239
  fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   240
  |> deepen depth f
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
  |> fold (fn prem => fn th => Thm.implies_elim th prem) thms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
42992
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   245
fun by_abstraction depth mode ctxt thms prove =
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   246
  with_prems depth thms (fn d => fn ct =>
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   247
    let val (cu, cx) = abstract d mode ct (abs_context ctxt)
4fc15e3217eb iteratively deepen abstractions to avoid rare Z3 proof reconstruction failures, e.g. when pulling if-then-else from below uninterpreted constants (suggested by Jasmin Christian Blanchette)
boehmes
parents: 42322
diff changeset
   248
    in abs_instantiate cx (prove (context_of cx) cu) end)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
(* a faster COMP *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   256
type compose_data = cterm list * (cterm -> cterm list) * thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
fun list2 (x, y) = [x, y]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59634
diff changeset
   260
fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule)
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59634
diff changeset
   261
fun precompose2 f rule : compose_data = precompose (list2 o f) rule
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
fun compose (cvs, f, rule) thm =
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59634
diff changeset
   264
  discharge thm (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   265
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
(* unfolding of 'distinct' *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   271
  val set1 = @{lemma "x ~: set [] == ~False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
  val set2 = @{lemma "x ~: set [x] == False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
  val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
  val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
  val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
  fun set_conv ct =
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
   278
    (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
    (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
40681
872b08416fb4 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents: 40663
diff changeset
   281
  val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)}
872b08416fb4 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents: 40663
diff changeset
   282
  val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)}
872b08416fb4 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents: 40663
diff changeset
   283
  val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
40274
6486c610a549 introduced SMT.distinct as a representation of the solvers' built-in predicate; check that SMT.distinct is always applied to an explicit list
boehmes
parents: 40164
diff changeset
   284
    by (simp add: distinct_def)}
36898
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 binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
fun unfold_distinct_conv ct =
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
   289
  (Conv.rewrs_conv [dist1, dist2] else_conv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   290
  (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   291
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
(* simpset *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   296
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   297
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
  val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
  val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
  val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
  val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
  fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
  fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
    | dest_binop t = raise TERM ("dest_binop", [t])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
61144
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 60868
diff changeset
   307
  fun prove_antisym_le ctxt ct =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
    let
61144
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 60868
diff changeset
   309
      val (le, r, s) = dest_binop (Thm.term_of ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
      val less = Const (@{const_name less}, Term.fastype_of le)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   311
      val prems = Simplifier.prems_of ctxt
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   313
      (case find_first (eq_prop (le $ s $ r)) prems of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   314
        NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   315
          find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   316
          |> Option.map (fn thm => thm RS antisym_less1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   317
      | SOME thm => SOME (thm RS antisym_le1))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   318
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   319
    handle THM _ => NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   320
61144
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 60868
diff changeset
   321
  fun prove_antisym_less ctxt ct =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   322
    let
61144
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 60868
diff changeset
   323
      val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   324
      val le = Const (@{const_name less_eq}, Term.fastype_of less)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   325
      val prems = Simplifier.prems_of ctxt
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   326
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   327
      (case find_first (eq_prop (le $ r $ s)) prems of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   328
        NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   329
          find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   330
          |> Option.map (fn thm => thm RS antisym_less2)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   331
      | SOME thm => SOME (thm RS antisym_le2))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   332
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   333
  handle THM _ => NONE
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   334
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   335
  val basic_simpset =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   336
    simpset_of (put_simpset HOL_ss @{context}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   337
      addsimps @{thms field_simps}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   338
      addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   339
      addsimps @{thms arith_special} addsimps @{thms arith_simps}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   340
      addsimps @{thms rel_simps}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   341
      addsimps @{thms array_rules}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   342
      addsimps @{thms term_true_def} addsimps @{thms term_false_def}
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   343
      addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
60868
dd18c33c001e direct bootstrap of integer division from natural division
haftmann
parents: 60642
diff changeset
   344
      addsimprocs [@{simproc numeral_divmod}]
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   345
      addsimprocs [
61144
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 60868
diff changeset
   346
        Simplifier.make_simproc @{context} "fast_int_arith"
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 60868
diff changeset
   347
         {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
62913
13252110a6fe eliminated unused simproc identifier;
wenzelm
parents: 61144
diff changeset
   348
          proc = K Lin_Arith.simproc},
61144
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 60868
diff changeset
   349
        Simplifier.make_simproc @{context} "antisym_le"
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 60868
diff changeset
   350
         {lhss = [@{term "(x::'a::order) \<le> y"}],
62913
13252110a6fe eliminated unused simproc identifier;
wenzelm
parents: 61144
diff changeset
   351
          proc = K prove_antisym_le},
61144
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 60868
diff changeset
   352
        Simplifier.make_simproc @{context} "antisym_less"
5e94dfead1c2 simplified simproc programming interfaces;
wenzelm
parents: 60868
diff changeset
   353
         {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
62913
13252110a6fe eliminated unused simproc identifier;
wenzelm
parents: 61144
diff changeset
   354
          proc = K prove_antisym_less}])
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   355
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   356
  structure Simpset = Generic_Data
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   357
  (
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   358
    type T = simpset
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   359
    val empty = basic_simpset
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   360
    val extend = I
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   361
    val merge = Simplifier.merge_ss
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   362
  )
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   363
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   364
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   365
fun add_simproc simproc context =
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   366
  Simpset.map (simpset_map (Context.proof_of context)
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   367
    (fn ctxt => ctxt addsimprocs [simproc])) context
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   368
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   369
fun make_simpset ctxt rules =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 47108
diff changeset
   370
  simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   371
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   372
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   373
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   374
end