src/HOL/Tools/SMT/z3_proof_tools.ML
author boehmes
Mon, 20 Dec 2010 22:02:57 +0100
changeset 41328 6792a5c92a58
parent 41281 679118e35378
child 41899 83dd157ec9ab
permissions -rw-r--r--
avoid ML structure aliases (especially single-letter abbreviations)
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
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
    66
fun net_instance' f net ct =
40806
59d96f777da3 also support higher-order rules for Z3 proof reconstruction
boehmes
parents: 40681
diff changeset
    67
  let
59d96f777da3 also support higher-order rules for Z3 proof reconstruction
boehmes
parents: 40681
diff changeset
    68
    val xthms = Net.match_term net (Thm.term_of ct)
59d96f777da3 also support higher-order rules for Z3 proof reconstruction
boehmes
parents: 40681
diff changeset
    69
    fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms 
59d96f777da3 also support higher-order rules for Z3 proof reconstruction
boehmes
parents: 40681
diff changeset
    70
    fun first_of' f ct =
59d96f777da3 also support higher-order rules for Z3 proof reconstruction
boehmes
parents: 40681
diff changeset
    71
      let val thm = Thm.trivial ct
59d96f777da3 also support higher-order rules for Z3 proof reconstruction
boehmes
parents: 40681
diff changeset
    72
      in get_first (f (try (fn rule => rule COMP thm))) xthms end
59d96f777da3 also support higher-order rules for Z3 proof reconstruction
boehmes
parents: 40681
diff changeset
    73
  in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
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
    74
val net_instance = net_instance' I
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    75
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    76
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    77
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    78
(* proof combinators *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    80
fun under_assumption f ct =
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
    81
  let val ct' = SMT_Utils.mk_cprop ct
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
  in Thm.implies_intr ct' (f (Thm.assume ct')) end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    83
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    84
fun with_conv conv prove ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    85
  let val eq = Thm.symmetric (conv ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
  in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
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 discharge p pq = Thm.implies_elim pq p
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    89
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    90
fun varify vars = Drule.generalize ([], vars)
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 unfold_eqs _ [] = Conv.all_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    93
  | unfold_eqs ctxt eqs =
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
    94
      Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt
36898
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 match_instantiate f ct thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    97
  Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
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 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
   100
41123
boehmes
parents: 40806
diff changeset
   101
(*
boehmes
parents: 40806
diff changeset
   102
   |- c x == t x ==> P (c x)
boehmes
parents: 40806
diff changeset
   103
  ---------------------------
boehmes
parents: 40806
diff changeset
   104
      c == t |- P (c x)
boehmes
parents: 40806
diff changeset
   105
*) 
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   106
fun make_hyp_def thm ctxt =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   107
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
    val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   109
    val (cf, cvs) = Drule.strip_comb lhs
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
   110
    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
   111
    fun apply cv th =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
      Thm.combination th (Thm.reflexive cv)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
      |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   115
    yield_singleton Assumption.add_assumes eq ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
    |>> Thm.implies_elim thm o fold apply cvs
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   118
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   119
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   120
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   121
(* abstraction *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   122
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   123
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   124
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   125
fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   126
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   127
fun context_of (ctxt, _, _, _) = ctxt
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   128
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   129
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
   130
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   131
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
   132
  fold replace (Termtab.dest tab) #>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   133
  beta_norm ? Conv.fconv_rule (Thm.beta_conversion true)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   134
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   135
fun lambda_abstract cvs t =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   136
  let
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   137
    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
   138
    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
   139
    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
   140
  in (Term.list_abs_free (vs, t), cvs') end
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   141
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   142
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
   143
  let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   144
  in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   145
    (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
   146
      SOME (cv, _) => (Drule.list_comb (cv, cvs'), cx)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   147
    | NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   148
        let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   149
          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
   150
          val cv = SMT_Utils.certify ctxt'
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
   151
            (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
   152
          val cu = Drule.list_comb (cv, cvs')
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   153
          val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   154
          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
   155
        in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   156
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   157
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   158
fun abs_comb f g cvs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   159
  let val (cf, cu) = Thm.dest_comb ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   160
  in f cvs cf ##>> g cvs cu #>> uncurry Thm.capply end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   161
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   162
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
   163
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   164
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
   165
  (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
   166
    _ $ _ => 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
   167
  | _ => pair ct)
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   168
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   169
fun abs_list f g cvs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   170
  (case Thm.term_of ct of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   171
    Const (@{const_name Nil}, _) => pair ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   172
  | Const (@{const_name Cons}, _) $ _ $ _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   173
      abs_comb (abs_arg f) (abs_list f g) cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   174
  | _ => g cvs ct)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   176
fun abs_abs f cvs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   177
  let val (cv, cu) = Thm.dest_abs NONE ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   178
  in f (cv :: cvs) cu #>> Thm.cabs cv end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   179
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   180
val is_atomic = (fn _ $ _ => false | Abs _ => false | _ => true)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   181
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   182
fun abstract (ext_logic, with_theories) =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   183
  let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   184
    fun abstr1 cvs ct = abs_arg abstr cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   185
    and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   186
    and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   187
    and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   188
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   189
    and abstr cvs ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   190
      (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
   191
        @{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
   192
      | @{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
   193
      | @{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
   194
      | @{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
   195
      | @{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
   196
      | @{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
   197
      | @{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
   198
      | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct
38864
4abe644fcea5 formerly unnamed infix equality now named HOL.eq
haftmann
parents: 38795
diff changeset
   199
      | 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
   200
      | Const (@{const_name distinct}, _) $ _ =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   201
          if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   202
          else fresh_abstraction cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   203
      | Const (@{const_name If}, _) $ _ $ _ $ _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   204
          if ext_logic then abstr3 cvs ct else fresh_abstraction cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
      | Const (@{const_name All}, _) $ _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   206
          if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   207
      | Const (@{const_name Ex}, _) $ _ =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   208
          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
   209
      | t => (fn cx =>
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   210
          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
   211
          else if with_theories andalso
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41281
diff changeset
   212
            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
   213
          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
   214
          else fresh_abstraction cvs ct cx))
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   215
  in abstr [] end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   216
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
   217
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
   218
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   219
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
   220
  fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   221
  |> f
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   222
  |> fold (fn prem => fn th => Thm.implies_elim th prem) thms
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   223
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   224
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   225
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   226
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
   227
  let val (cu, cx) = abstract mode ct (abs_context ctxt)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   228
  in abs_instantiate cx (prove (context_of cx) cu) end)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   229
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   230
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   231
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   232
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   233
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   234
(* a faster COMP *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   235
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   236
type compose_data = cterm list * (cterm -> cterm list) * thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   237
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   238
fun list2 (x, y) = [x, y]
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   239
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   240
fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   241
fun precompose2 f rule = precompose (list2 o f) rule
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   242
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   243
fun compose (cvs, f, rule) thm =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   244
  discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   245
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   246
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   247
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
(* unfolding of 'distinct' *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   249
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   250
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   251
  val set1 = @{lemma "x ~: set [] == ~False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   252
  val set2 = @{lemma "x ~: set [x] == False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
  val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   254
  val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   255
  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
   256
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
  fun set_conv ct =
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
   258
    (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
    (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
40681
872b08416fb4 be more precise: only treat constant 'distinct' applied to an explicit list as built-in
boehmes
parents: 40663
diff changeset
   261
  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
   262
  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
   263
  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
   264
    by (simp add: distinct_def)}
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
  fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   267
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   268
fun unfold_distinct_conv ct =
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
   269
  (Conv.rewrs_conv [dist1, dist2] else_conv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   270
  (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
   271
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   272
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   273
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   274
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   275
(* simpset *)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   276
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   277
local
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   278
  val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   279
  val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   280
  val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   281
  val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   282
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   283
  fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   284
  fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   285
    | dest_binop t = raise TERM ("dest_binop", [t])
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   286
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   287
  fun prove_antisym_le ss t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   288
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   289
      val (le, r, s) = dest_binop t
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   290
      val less = Const (@{const_name less}, Term.fastype_of le)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   291
      val prems = Simplifier.prems_of_ss ss
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   292
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   293
      (case find_first (eq_prop (le $ s $ r)) prems of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   294
        NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   295
          find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   296
          |> Option.map (fn thm => thm RS antisym_less1)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   297
      | SOME thm => SOME (thm RS antisym_le1))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   298
    end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   299
    handle THM _ => NONE
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   300
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   301
  fun prove_antisym_less ss t =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   302
    let
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   303
      val (less, r, s) = dest_binop (HOLogic.dest_not t)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   304
      val le = Const (@{const_name less_eq}, Term.fastype_of less)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   305
      val prems = prems_of_ss ss
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   306
    in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   307
      (case find_first (eq_prop (le $ r $ s)) prems of
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   308
        NONE =>
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   309
          find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   310
          |> Option.map (fn thm => thm RS antisym_less2)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   311
      | SOME thm => SOME (thm RS antisym_le2))
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   312
  end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   313
  handle THM _ => NONE
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   314
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   315
  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
   316
    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
   317
    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
   318
    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
   319
    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
   320
    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
   321
    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
   322
    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
   323
    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
   324
    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
   325
    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
   326
      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
   327
        "(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
   328
      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
   329
        (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
   330
      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
   331
        (K prove_antisym_less)]
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   332
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   333
  structure Simpset = Generic_Data
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   334
  (
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   335
    type T = simpset
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   336
    val empty = basic_simpset
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   337
    val extend = I
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   338
    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
   339
  )
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   340
in
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   341
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   342
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
   343
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
   344
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
   345
  Simplifier.context ctxt (Simpset.get (Context.Proof ctxt)) addsimps rules
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   346
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   347
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   348
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   349
end