src/HOL/Tools/SMT/z3_proof_tools.ML
author boehmes
Fri, 08 Apr 2011 19:04:08 +0200
changeset 42322 be1c32069daa
parent 41899 83dd157ec9ab
child 42992 4fc15e3217eb
permissions -rw-r--r--
use unification instead of matching to find proper assertions (which might not match original assumptions due to lambda-lifting and introduction of fresh variables)
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_tools.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
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
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     7
signature Z3_PROOF_TOOLS =
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
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
    14
  val net_instance': ((thm -> thm option) -> 'a -> 'a option) -> 'a Net.net ->
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
    15
    cterm -> 'a option
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    16
  val net_instance: thm Net.net -> cterm -> thm option
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
41123
boehmes
parents: 40806
diff changeset
    18
  (*proof combinators*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    19
  val under_assumption: (thm -> thm) -> cterm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
  val with_conv: conv -> (cterm -> thm) -> cterm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
  val discharge: thm -> thm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    22
  val varify: string list -> thm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    23
  val unfold_eqs: Proof.context -> thm list -> conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    24
  val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    25
  val by_tac: (int -> tactic) -> cterm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
  val make_hyp_def: thm -> Proof.context -> thm * Proof.context
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    27
  val by_abstraction: bool * bool -> Proof.context -> thm list ->
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    28
    (Proof.context -> cterm -> thm) -> cterm -> thm
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    29
41123
boehmes
parents: 40806
diff changeset
    30
  (*a faster COMP*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    31
  type compose_data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    32
  val precompose: (cterm -> cterm list) -> thm -> compose_data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    33
  val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    34
  val compose: compose_data -> thm -> thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    35
41123
boehmes
parents: 40806
diff changeset
    36
  (*unfolding of 'distinct'*)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    37
  val unfold_distinct_conv: conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    38
41123
boehmes
parents: 40806
diff changeset
    39
  (*simpset*)
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    40
  val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    41
  val make_simpset: Proof.context -> thm list -> simpset
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    42
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    43
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    44
structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    45
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    46
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    47
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    48
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
    49
(* modifying terms *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
    51
fun as_meta_eq ct =
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
    52
  uncurry SMT_Utils.mk_cequals (Thm.dest_binop (SMT_Utils.dest_cprop ct))
36898
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
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    56
(* theorem nets *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    57
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
    58
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
    59
  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
    60
  in fold insert xthms Net.empty end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    61
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    62
fun maybe_instantiate ct thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
  try Thm.first_order_match (Thm.cprop_of thm, ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    64
  |> Option.map (fn inst => Thm.instantiate inst thm)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
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
    66
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
    67
  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
    68
    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
    69
      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
    70
      val xthms = lookup net (Thm.term_of 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
    71
      fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms 
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
      fun first_of' f 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
    73
        let val thm = Thm.trivial 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
    74
        in get_first (f (try (fn rule => rule COMP thm))) xthms end
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 (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
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
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
    77
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
    78
fun net_instance' f = instances_from_net false f
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
    79
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
val net_instance = instances_from_net true I
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
    81
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
end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
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
(* proof combinators *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    87
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    88
fun under_assumption f ct =
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
    89
  let val ct' = SMT_Utils.mk_cprop ct
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
  in Thm.implies_intr ct' (f (Thm.assume ct')) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    91
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
fun with_conv conv prove ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
  let val eq = Thm.symmetric (conv ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    94
  in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    95
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    96
fun discharge p pq = Thm.implies_elim pq p
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
fun varify vars = Drule.generalize ([], vars)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    99
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   100
fun unfold_eqs _ [] = Conv.all_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   101
  | unfold_eqs ctxt eqs =
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
   102
      Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   103
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
fun match_instantiate f ct thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   105
  Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
41123
boehmes
parents: 40806
diff changeset
   109
(*
boehmes
parents: 40806
diff changeset
   110
   |- c x == t x ==> P (c x)
boehmes
parents: 40806
diff changeset
   111
  ---------------------------
boehmes
parents: 40806
diff changeset
   112
      c == t |- P (c x)
boehmes
parents: 40806
diff changeset
   113
*) 
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
fun make_hyp_def thm ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
    val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
    val (cf, cvs) = Drule.strip_comb lhs
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
   118
    val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
    fun apply cv th =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
      Thm.combination th (Thm.reflexive cv)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
      |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
    yield_singleton Assumption.add_assumes eq ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
    |>> Thm.implies_elim thm o fold apply cvs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
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
(* abstraction *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   130
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   132
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   135
fun context_of (ctxt, _, _, _) = ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   137
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
   138
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   139
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
   140
  fold replace (Termtab.dest tab) #>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
  beta_norm ? Conv.fconv_rule (Thm.beta_conversion true)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   143
fun lambda_abstract cvs t =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
  let
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   145
    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
   146
    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
   147
    val vs = map (Term.dest_Free o Thm.term_of) cvs'
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   148
  in (Term.list_abs_free (vs, t), cvs') end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   150
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
   151
  let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   152
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
    (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
   154
      SOME (cv, _) => (Drule.list_comb (cv, cvs'), cx)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   155
    | NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
        let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
          val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
   158
          val cv = SMT_Utils.certify ctxt'
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
   159
            (Free (n, map SMT_Utils.typ_of cvs' ---> SMT_Utils.typ_of ct))
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   160
          val cu = Drule.list_comb (cv, cvs')
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
          val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   162
          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
   163
        in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   164
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   165
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   166
fun abs_comb f g cvs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   167
  let val (cf, cu) = Thm.dest_comb ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   168
  in f cvs cf ##>> g cvs cu #>> uncurry Thm.capply end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   170
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
   171
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   172
fun abs_args f cvs ct =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   173
  (case Thm.term_of ct of
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   174
    _ $ _ => abs_comb (abs_args f) f cvs ct
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   175
  | _ => pair ct)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   176
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
fun abs_list f g cvs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
  (case Thm.term_of ct of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
    Const (@{const_name Nil}, _) => pair ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
  | Const (@{const_name Cons}, _) $ _ $ _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
      abs_comb (abs_arg f) (abs_list f g) cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
  | _ => g cvs ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
fun abs_abs f cvs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
  let val (cv, cu) = Thm.dest_abs NONE ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
  in f (cv :: cvs) cu #>> Thm.cabs cv end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
41899
83dd157ec9ab finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents: 41328
diff changeset
   188
val is_atomic =
83dd157ec9ab finished and tested Z3 proof reconstruction for injective functions;
boehmes
parents: 41328
diff changeset
   189
  (fn Free _ => true | Var _ => true | Bound _ => true | _ => false)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   191
fun abstract (ext_logic, with_theories) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   192
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   193
    fun abstr1 cvs ct = abs_arg abstr cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   194
    and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   195
    and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   196
    and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   197
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   198
    and abstr cvs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   199
      (case Thm.term_of ct 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: 40274
diff changeset
   200
        @{const Trueprop} $ _ => abstr1 cvs 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
   201
      | @{const "==>"} $ _ $ _ => abstr2 cvs 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
   202
      | @{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
   203
      | @{const False} => 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 Not} $ _ => abstr1 cvs 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
   205
      | @{const HOL.conj} $ _ $ _ => abstr2 cvs 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
   206
      | @{const HOL.disj} $ _ $ _ => abstr2 cvs 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
   207
      | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38795
diff changeset
   208
      | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
40681
872b08416fb4 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents: 40663
diff changeset
   209
      | Const (@{const_name distinct}, _) $ _ =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   210
          if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   211
          else fresh_abstraction cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   212
      | Const (@{const_name If}, _) $ _ $ _ $ _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   213
          if ext_logic then abstr3 cvs ct else fresh_abstraction cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   214
      | Const (@{const_name All}, _) $ _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
          if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
      | Const (@{const_name Ex}, _) $ _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   217
          if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   218
      | t => (fn cx =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   219
          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
   220
          else if with_theories andalso
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
   221
            Z3_Interface.is_builtin_theory_term (context_of cx) t
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   222
          then abs_args abstr cvs ct cx
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   223
          else fresh_abstraction cvs ct cx))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
  in abstr [] end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
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
   226
val cimp = Thm.cterm_of @{theory} @{const "==>"}
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
   227
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
fun with_prems 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
   229
  fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
  |> f
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
  |> fold (fn prem => fn th => Thm.implies_elim th prem) thms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   235
fun by_abstraction mode ctxt thms prove = with_prems thms (fn ct =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   236
  let val (cu, cx) = abstract mode ct (abs_context ctxt)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
  in abs_instantiate cx (prove (context_of cx) cu) end)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
(* a faster COMP *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
type compose_data = cterm list * (cterm -> cterm list) * thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
fun list2 (x, y) = [x, y]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
fun precompose2 f rule = precompose (list2 o f) rule
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
fun compose (cvs, f, rule) thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
  discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
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
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
(* unfolding of 'distinct' *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
  val set1 = @{lemma "x ~: set [] == ~False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   261
  val set2 = @{lemma "x ~: set [x] == False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   262
  val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   263
  val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   264
  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
   265
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   266
  fun set_conv ct =
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
   267
    (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
    (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   269
40681
872b08416fb4 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents: 40663
diff changeset
   270
  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
   271
  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
   272
  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
   273
    by (simp add: distinct_def)}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
  fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
fun unfold_distinct_conv ct =
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
   278
  (Conv.rewrs_conv [dist1, dist2] else_conv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
  (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
   280
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
(* simpset *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   286
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
  val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
  val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
  val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   290
  val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   291
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
  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
   293
  fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
    | dest_binop t = raise TERM ("dest_binop", [t])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   296
  fun prove_antisym_le ss t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   297
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
      val (le, r, s) = dest_binop t
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
      val less = Const (@{const_name less}, Term.fastype_of le)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
      val prems = Simplifier.prems_of_ss ss
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
      (case find_first (eq_prop (le $ s $ r)) prems of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
        NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
          find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
          |> Option.map (fn thm => thm RS antisym_less1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
      | SOME thm => SOME (thm RS antisym_le1))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
    handle THM _ => NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   309
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
  fun prove_antisym_less ss t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   311
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
      val (less, r, s) = dest_binop (HOLogic.dest_not t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   313
      val le = Const (@{const_name less_eq}, Term.fastype_of less)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   314
      val prems = prems_of_ss ss
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   315
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   316
      (case find_first (eq_prop (le $ r $ s)) prems of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   317
        NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   318
          find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   319
          |> Option.map (fn thm => thm RS antisym_less2)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   320
      | SOME thm => SOME (thm RS antisym_le2))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   321
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   322
  handle THM _ => NONE
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   323
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   324
  val basic_simpset = HOL_ss addsimps @{thms field_simps}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   325
    addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   326
    addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   327
    addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   328
    addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   329
    addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   330
    addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   331
    addsimps @{thms array_rules}
41281
679118e35378 removed odd decoration of built-in symbols as Vars (instead provide built-in desctructor functions along with their inverse functions);
boehmes
parents: 41172
diff changeset
   332
    addsimps @{thms term_true_def} addsimps @{thms term_false_def}
37151
3e9e8dfb3c98 use Z3's builtin support for div and mod
boehmes
parents: 36936
diff changeset
   333
    addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   334
    addsimprocs [
38715
6513ea67d95d renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents: 37151
diff changeset
   335
      Simplifier.simproc_global @{theory} "fast_int_arith" [
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   336
        "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
38715
6513ea67d95d renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents: 37151
diff changeset
   337
      Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"]
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   338
        (K prove_antisym_le),
38715
6513ea67d95d renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
wenzelm
parents: 37151
diff changeset
   339
      Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   340
        (K prove_antisym_less)]
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   341
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   342
  structure Simpset = Generic_Data
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   343
  (
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   344
    type T = simpset
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   345
    val empty = basic_simpset
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   346
    val extend = I
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   347
    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
   348
  )
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   349
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   350
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   351
fun add_simproc simproc = Simpset.map (fn ss => ss addsimprocs [simproc])
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   352
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   353
fun make_simpset ctxt rules =
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   354
  Simplifier.context ctxt (Simpset.get (Context.Proof ctxt)) addsimps rules
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   355
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   356
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   357
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   358
end