src/HOL/Library/Old_SMT/old_smt_normalize.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63950 cdc1e59aa513
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     1
(*  Title:      HOL/Library/Old_SMT/old_smt_normalize.ML
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     3
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
     4
Normalization steps on theorems required by SMT solvers.
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     5
*)
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     6
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
     7
signature OLD_SMT_NORMALIZE =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
     8
sig
54041
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 51717
diff changeset
     9
  val drop_fact_warning: Proof.context -> thm -> unit
36899
bcd6fce5bf06 layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
boehmes
parents: 36898
diff changeset
    10
  val atomize_conv: Proof.context -> conv
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    11
  type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    12
  val add_extra_norm: Old_SMT_Utils.class * extra_norm -> Context.generic ->
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    13
    Context.generic
41300
528f5d00b542 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
boehmes
parents: 41280
diff changeset
    14
  val normalize: (int * (int option * thm)) list -> Proof.context ->
528f5d00b542 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
boehmes
parents: 41280
diff changeset
    15
    (int * thm) list * Proof.context
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40686
diff changeset
    16
  val setup: theory -> theory
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    17
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    18
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    19
structure Old_SMT_Normalize: OLD_SMT_NORMALIZE =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    20
struct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    21
54041
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 51717
diff changeset
    22
fun drop_fact_warning ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    23
  Old_SMT_Config.verbose_msg ctxt (prefix "Warning: dropping assumption: " o
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 60642
diff changeset
    24
    Thm.string_of_thm ctxt)
54041
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 51717
diff changeset
    25
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    26
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    27
(* general theorem normalizations *)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    28
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    29
(** instantiate elimination rules **)
40685
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    30
 
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    31
local
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
    32
  val (cpfalse, cfalse) =
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
    33
    `Old_SMT_Utils.mk_cprop (Thm.cterm_of @{context} @{const False})
40685
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    34
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    35
  fun inst f ct thm =
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    36
    let val cv = f (Drule.strip_imp_concl (Thm.cprop_of thm))
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60352
diff changeset
    37
    in Thm.instantiate ([], [(dest_Var (Thm.term_of cv), ct)]) thm end
40685
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    38
in
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    39
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    40
fun instantiate_elim thm =
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    41
  (case Thm.concl_of thm of
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    42
    @{const Trueprop} $ Var (_, @{typ bool}) => inst Thm.dest_arg cfalse thm
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    43
  | Var _ => inst I cpfalse thm
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    44
  | _ => thm)
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    45
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    46
end
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    47
dcb27631cb45 instantiate elimination rules (reduces number of quantified variables, and makes such theorems better amenable for SMT solvers)
boehmes
parents: 40681
diff changeset
    48
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    49
(** normalize definitions **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    50
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    51
fun norm_def thm =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    52
  (case Thm.prop_of thm of
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    53
    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    54
      norm_def (thm RS @{thm fun_cong})
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55414
diff changeset
    55
  | Const (@{const_name Pure.eq}, _) $ _ $ Abs _ =>
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    56
      norm_def (thm RS @{thm meta_eq_to_obj_eq})
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    57
  | _ => thm)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    58
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    59
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    60
(** atomization **)
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 atomize_conv ctxt ct =
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    63
  (case Thm.term_of ct of
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55414
diff changeset
    64
    @{const Pure.imp} $ _ $ _ =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    65
      Conv.binop_conv (atomize_conv ctxt) then_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    66
      Conv.rewr_conv @{thm atomize_imp}
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55414
diff changeset
    67
  | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    68
      Conv.binop_conv (atomize_conv ctxt) then_conv
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    69
      Conv.rewr_conv @{thm atomize_eq}
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55414
diff changeset
    70
  | Const (@{const_name Pure.all}, _) $ Abs _ =>
36936
c52d1c130898 incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents: 36899
diff changeset
    71
      Conv.binder_conv (atomize_conv o snd) ctxt then_conv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    72
      Conv.rewr_conv @{thm atomize_all}
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    73
  | _ => Conv.all_conv) ct
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    74
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40686
diff changeset
    75
val setup_atomize =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    76
  fold Old_SMT_Builtin.add_builtin_fun_ext'' [@{const_name Pure.imp},
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 55414
diff changeset
    77
    @{const_name Pure.eq}, @{const_name Pure.all}, @{const_name Trueprop}]
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40686
diff changeset
    78
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    79
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    80
(** unfold special quantifiers **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    81
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    82
local
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    83
  val ex1_def = mk_meta_eq @{lemma
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    84
    "Ex1 = (%P. EX x. P x & (ALL y. P y --> y = x))"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    85
    by (rule ext) (simp only: Ex1_def)}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    86
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    87
  val ball_def = mk_meta_eq @{lemma "Ball = (%A P. ALL x. x : A --> P x)"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    88
    by (rule ext)+ (rule Ball_def)}
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    89
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    90
  val bex_def = mk_meta_eq @{lemma "Bex = (%A P. EX x. x : A & P x)"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    91
    by (rule ext)+ (rule Bex_def)}
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    92
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    93
  val special_quants = [(@{const_name Ex1}, ex1_def),
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    94
    (@{const_name Ball}, ball_def), (@{const_name Bex}, bex_def)]
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    95
  
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    96
  fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    97
    | special_quant _ = NONE
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
    98
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
    99
  fun special_quant_conv _ ct =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   100
    (case special_quant (Thm.term_of ct) of
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   101
      SOME thm => Conv.rewr_conv thm
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   102
    | NONE => Conv.all_conv) ct
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   103
in
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   104
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   105
fun unfold_special_quants_conv ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   106
  Old_SMT_Utils.if_exists_conv (is_some o special_quant)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   107
    (Conv.top_conv special_quant_conv ctxt)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   108
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   109
val setup_unfolded_quants =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   110
  fold (Old_SMT_Builtin.add_builtin_fun_ext'' o fst) special_quants
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   111
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   112
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   113
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   114
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   115
(** trigger inference **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   116
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   117
local
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   118
  (*** check trigger syntax ***)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   119
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   120
  fun dest_trigger (Const (@{const_name pat}, _) $ _) = SOME true
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   121
    | dest_trigger (Const (@{const_name nopat}, _) $ _) = SOME false
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   122
    | dest_trigger _ = NONE
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   123
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   124
  fun eq_list [] = false
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   125
    | eq_list (b :: bs) = forall (equal b) bs
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   127
  fun proper_trigger t =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   128
    t
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   129
    |> these o try HOLogic.dest_list
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   130
    |> map (map_filter dest_trigger o these o try HOLogic.dest_list)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   131
    |> (fn [] => false | bss => forall eq_list bss)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   132
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   133
  fun proper_quant inside f t =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   134
    (case t of
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   135
      Const (@{const_name All}, _) $ Abs (_, _, u) => proper_quant true f u
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   136
    | Const (@{const_name Ex}, _) $ Abs (_, _, u) => proper_quant true f u
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   137
    | @{const trigger} $ p $ u =>
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   138
        (if inside then f p else false) andalso proper_quant false f u
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   139
    | Abs (_, _, u) => proper_quant false f u
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   140
    | u1 $ u2 => proper_quant false f u1 andalso proper_quant false f u2
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   141
    | _ => true)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   142
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   143
  fun check_trigger_error ctxt t =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   144
    error ("SMT triggers must only occur under quantifier and multipatterns " ^
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   145
      "must have the same kind: " ^ Syntax.string_of_term ctxt t)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   146
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   147
  fun check_trigger_conv ctxt ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   148
    if proper_quant false proper_trigger (Old_SMT_Utils.term_of ct) then
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   149
      Conv.all_conv ct
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   150
    else check_trigger_error ctxt (Thm.term_of ct)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   151
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   152
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   153
  (*** infer simple triggers ***)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   154
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   155
  fun dest_cond_eq ct =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   156
    (case Thm.term_of ct of
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   157
      Const (@{const_name HOL.eq}, _) $ _ $ _ => Thm.dest_binop ct
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   158
    | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   159
    | _ => raise CTERM ("no equation", [ct]))
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   160
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 58058
diff changeset
   161
  fun get_constrs thy (Type (n, _)) = these (Old_Datatype_Data.get_constrs thy n)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   162
    | get_constrs _ _ = []
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   163
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   164
  fun is_constr thy (n, T) =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   165
    let fun match (m, U) = m = n andalso Sign.typ_instance thy (T, U)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   166
    in can (the o find_first match o get_constrs thy o Term.body_type) T end
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   167
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   168
  fun is_constr_pat thy t =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   169
    (case Term.strip_comb t of
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   170
      (Free _, []) => true
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   171
    | (Const c, ts) => is_constr thy c andalso forall (is_constr_pat thy) ts
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   172
    | _ => false)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   173
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   174
  fun is_simp_lhs ctxt t =
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   175
    (case Term.strip_comb t of
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   176
      (Const c, ts as _ :: _) =>
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   177
        not (Old_SMT_Builtin.is_builtin_fun_ext ctxt c ts) andalso
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42190
diff changeset
   178
        forall (is_constr_pat (Proof_Context.theory_of ctxt)) ts
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   179
    | _ => false)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   180
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   181
  fun has_all_vars vs t =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   182
    subset (op aconv) (vs, map Free (Term.add_frees t []))
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   183
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   184
  fun minimal_pats vs ct =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   185
    if has_all_vars vs (Thm.term_of ct) then
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   186
      (case Thm.term_of ct of
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   187
        _ $ _ =>
59058
a78612c67ec0 renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents: 58112
diff changeset
   188
          (case apply2 (minimal_pats vs) (Thm.dest_comb ct) of
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   189
            ([], []) => [[ct]]
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   190
          | (ctss, ctss') => union (eq_set (op aconvc)) ctss ctss')
41174
10eb369f8c01 fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents: 41173
diff changeset
   191
      | _ => [])
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   192
    else []
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   193
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   194
  fun proper_mpat _ _ _ [] = false
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   195
    | proper_mpat thy gen u cts =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   196
        let
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   197
          val tps = (op ~~) (`gen (map Thm.term_of cts))
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   198
          fun some_match u = tps |> exists (fn (t', t) =>
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   199
            Pattern.matches thy (t', u) andalso not (t aconv u))
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   200
        in not (Term.exists_subterm some_match u) end
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   201
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   202
  val pat =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   203
    Old_SMT_Utils.mk_const_pat @{theory} @{const_name pat} Old_SMT_Utils.destT1
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   204
  fun mk_pat ct = Thm.apply (Old_SMT_Utils.instT' ct pat) ct
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   205
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   206
  fun mk_clist T = apply2 (Thm.cterm_of @{context}) (HOLogic.cons_const T, HOLogic.nil_const T)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   207
  fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   208
  val mk_pat_list = mk_list (mk_clist @{typ pattern})
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   209
  val mk_mpat_list = mk_list (mk_clist @{typ "pattern list"})  
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   210
  fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   211
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   212
  val trigger_eq =
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   213
    mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)}
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   214
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   215
  fun insert_trigger_conv [] ct = Conv.all_conv ct
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   216
    | insert_trigger_conv ctss ct =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   217
        let val (ctr, cp) = Thm.dest_binop (Thm.rhs_of trigger_eq) ||> rpair ct
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60352
diff changeset
   218
        in Thm.instantiate ([], map (apfst (dest_Var o Thm.term_of)) [cp, (ctr, mk_trigger ctss)]) trigger_eq end
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   219
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   220
  fun infer_trigger_eq_conv outer_ctxt (ctxt, cvs) ct =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   221
    let
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   222
      val (lhs, rhs) = dest_cond_eq ct
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   223
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   224
      val vs = map Thm.term_of cvs
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 42190
diff changeset
   225
      val thy = Proof_Context.theory_of ctxt
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   226
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   227
      fun get_mpats ct =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   228
        if is_simp_lhs ctxt (Thm.term_of ct) then minimal_pats vs ct
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   229
        else []
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   230
      val gen = Variable.export_terms ctxt outer_ctxt
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   231
      val filter_mpats = filter (proper_mpat thy gen (Thm.term_of rhs))
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   232
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   233
    in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   234
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   235
  fun has_trigger (@{const trigger} $ _ $ _) = true
41174
10eb369f8c01 fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents: 41173
diff changeset
   236
    | has_trigger _ = false
10eb369f8c01 fixed trigger inference: testing if a theorem already has a trigger was too strict;
boehmes
parents: 41173
diff changeset
   237
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   238
  fun try_trigger_conv cv ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   239
    if Old_SMT_Utils.under_quant has_trigger (Old_SMT_Utils.term_of ct) then
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   240
      Conv.all_conv ct
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   241
    else Conv.try_conv cv ct
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   242
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   243
  fun infer_trigger_conv ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   244
    if Config.get ctxt Old_SMT_Config.infer_triggers then
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   245
      try_trigger_conv
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   246
        (Old_SMT_Utils.under_quant_conv (infer_trigger_eq_conv ctxt) ctxt)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   247
    else Conv.all_conv
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   248
in
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   249
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   250
fun trigger_conv ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   251
  Old_SMT_Utils.prop_conv
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   252
    (check_trigger_conv ctxt then_conv infer_trigger_conv ctxt)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   253
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   254
val setup_trigger =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   255
  fold Old_SMT_Builtin.add_builtin_fun_ext''
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   256
    [@{const_name pat}, @{const_name nopat}, @{const_name trigger}]
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   257
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   258
end
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   259
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   260
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   261
(** adding quantifier weights **)
39483
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   262
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   263
local
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   264
  (*** check weight syntax ***)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   265
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   266
  val has_no_weight =
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   267
    not o Term.exists_subterm (fn @{const weight} => true | _ => false)
39483
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   268
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   269
  fun is_weight (@{const weight} $ w $ t) =
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   270
        (case try HOLogic.dest_number w of
41173
7c6178d45cc8 fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents: 41126
diff changeset
   271
          SOME (_, i) => i >= 0 andalso has_no_weight t
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   272
        | _ => false)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   273
    | is_weight t = has_no_weight t
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   274
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   275
  fun proper_trigger (@{const trigger} $ _ $ t) = is_weight t
41173
7c6178d45cc8 fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents: 41126
diff changeset
   276
    | proper_trigger t = is_weight t 
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   277
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   278
  fun check_weight_error ctxt t =
41173
7c6178d45cc8 fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars)
boehmes
parents: 41126
diff changeset
   279
    error ("SMT weight must be a non-negative number and must only occur " ^
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   280
      "under the top-most quantifier and an optional trigger: " ^
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   281
      Syntax.string_of_term ctxt t)
39483
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   282
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   283
  fun check_weight_conv ctxt ct =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   284
    if Old_SMT_Utils.under_quant proper_trigger (Old_SMT_Utils.term_of ct) then
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   285
      Conv.all_conv ct
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   286
    else check_weight_error ctxt (Thm.term_of ct)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   287
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   288
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   289
  (*** insertion of weights ***)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   290
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   291
  fun under_trigger_conv cv ct =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   292
    (case Thm.term_of ct of
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   293
      @{const trigger} $ _ $ _ => Conv.arg_conv cv
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   294
    | _ => cv) ct
39483
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   295
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   296
  val weight_eq =
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   297
    mk_meta_eq @{lemma "p = weight i p" by (simp add: weight_def)}
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   298
  fun mk_weight_eq w =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   299
    let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   300
    in
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60352
diff changeset
   301
      Thm.instantiate ([], [(dest_Var (Thm.term_of cv), Numeral.mk_cnumber @{ctyp int} w)])
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 60352
diff changeset
   302
        weight_eq
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   303
    end
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   304
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   305
  fun add_weight_conv NONE _ = Conv.all_conv
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   306
    | add_weight_conv (SOME weight) ctxt =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   307
        let val cv = Conv.rewr_conv (mk_weight_eq weight)
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   308
        in Old_SMT_Utils.under_quant_conv (K (under_trigger_conv cv)) ctxt end
39483
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   309
in
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   310
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   311
fun weight_conv weight ctxt = 
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   312
  Old_SMT_Utils.prop_conv
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   313
    (check_weight_conv ctxt then_conv add_weight_conv weight ctxt)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   314
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   315
val setup_weight = Old_SMT_Builtin.add_builtin_fun_ext'' @{const_name weight}
39483
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   316
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   317
end
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   318
9f0e5684f04b add full support for datatypes to the SMT interface (only used by Z3 in oracle mode so far); added store to keep track of datatype selector functions
boehmes
parents: 38864
diff changeset
   319
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   320
(** combined general normalizations **)
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   321
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   322
fun gen_normalize1_conv ctxt weight =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   323
  atomize_conv ctxt then_conv
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   324
  unfold_special_quants_conv ctxt then_conv
41327
49feace87649 added an additional beta reduction: unfolding of special quantifiers might leave terms unnormalized wrt to beta reductions
boehmes
parents: 41300
diff changeset
   325
  Thm.beta_conversion true then_conv
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   326
  trigger_conv ctxt then_conv
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   327
  weight_conv weight ctxt
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   328
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   329
fun gen_normalize1 ctxt weight thm =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   330
  thm
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   331
  |> instantiate_elim
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   332
  |> norm_def
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   333
  |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   334
  |> Drule.forall_intr_vars
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   335
  |> Conv.fconv_rule (gen_normalize1_conv ctxt weight)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   336
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   337
fun gen_norm1_safe ctxt (i, (weight, thm)) =
54041
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 51717
diff changeset
   338
  (case try (gen_normalize1 ctxt weight) thm of
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 51717
diff changeset
   339
    SOME thm' => SOME (i, thm')
227908156cd2 make SMT integration slacker w.r.t. bad apples (facts)
blanchet
parents: 51717
diff changeset
   340
  | NONE => (drop_fact_warning ctxt thm; NONE))
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   341
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   342
fun gen_normalize ctxt iwthms = map_filter (gen_norm1_safe ctxt) iwthms
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   343
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40686
diff changeset
   344
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40686
diff changeset
   345
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   346
(* unfolding of definitions and theory-specific rewritings *)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   347
50601
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   348
fun expand_head_conv cv ct =
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   349
  (case Thm.term_of ct of
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   350
    _ $ _ =>
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   351
      Conv.fun_conv (expand_head_conv cv) then_conv
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   352
      Conv.try_conv (Thm.beta_conversion false)
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   353
  | _ => cv) ct
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   354
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   355
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   356
(** rewrite bool case expressions as if expressions **)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   357
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   358
local
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 54883
diff changeset
   359
  fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 54883
diff changeset
   360
    | is_case_bool _ = false
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   361
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   362
  val thm = mk_meta_eq @{lemma
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 54883
diff changeset
   363
    "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp}
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   364
50601
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   365
  fun unfold_conv _ =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   366
    Old_SMT_Utils.if_true_conv (is_case_bool o Term.head_of)
50601
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   367
      (expand_head_conv (Conv.rewr_conv thm))
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   368
in
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   369
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 54883
diff changeset
   370
fun rewrite_case_bool_conv ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   371
  Old_SMT_Utils.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   372
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 54883
diff changeset
   373
val setup_case_bool =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   374
  Old_SMT_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   375
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   376
end
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   377
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   378
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   379
(** unfold abs, min and max **)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   380
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   381
local
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   382
  val abs_def = mk_meta_eq @{lemma
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   383
    "abs = (%a::'a::abs_if. if a < 0 then - a else a)"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   384
    by (rule ext) (rule abs_if)}
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   385
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   386
  val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   387
    by (rule ext)+ (rule min_def)}
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   388
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   389
  val max_def = mk_meta_eq  @{lemma "max = (%a b. if a <= b then b else a)"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   390
    by (rule ext)+ (rule max_def)}
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   391
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   392
  val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def),
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   393
    (@{const_name abs}, abs_def)]
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   394
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   395
  fun is_builtinT ctxt T =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   396
    Old_SMT_Builtin.is_builtin_typ_ext ctxt (Term.domain_type T)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   397
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   398
  fun abs_min_max ctxt (Const (n, T)) =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   399
        (case AList.lookup (op =) defs n of
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   400
          NONE => NONE
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   401
        | SOME thm => if is_builtinT ctxt T then SOME thm else NONE)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   402
    | abs_min_max _ _ = NONE
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   403
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   404
  fun unfold_amm_conv ctxt ct =
50601
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   405
    (case abs_min_max ctxt (Term.head_of (Thm.term_of ct)) of
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   406
      SOME thm => expand_head_conv (Conv.rewr_conv thm)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   407
    | NONE => Conv.all_conv) ct
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   408
in
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   409
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   410
fun unfold_abs_min_max_conv ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   411
  Old_SMT_Utils.if_exists_conv (is_some o abs_min_max ctxt)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   412
    (Conv.top_conv unfold_amm_conv ctxt)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   413
  
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   414
val setup_abs_min_max = fold (Old_SMT_Builtin.add_builtin_fun_ext'' o fst) defs
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   415
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   416
end
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   417
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   418
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   419
(** embedding of standard natural number operations into integer operations **)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   420
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   421
local
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   422
  val nat_embedding = @{lemma
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   423
    "ALL n. nat (int n) = n"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   424
    "ALL i. i >= 0 --> int (nat i) = i"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   425
    "ALL i. i < 0 --> int (nat i) = 0"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   426
    by simp_all}
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   427
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   428
  val simple_nat_ops = [
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   429
    @{const less (nat)}, @{const less_eq (nat)},
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   430
    @{const Suc}, @{const plus (nat)}, @{const minus (nat)}]
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   431
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   432
  val mult_nat_ops =
63950
cdc1e59aa513 syntactic type class for operation mod named after mod;
haftmann
parents: 62348
diff changeset
   433
    [@{const times (nat)}, @{const divide (nat)}, @{const modulo (nat)}]
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   434
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   435
  val nat_ops = simple_nat_ops @ mult_nat_ops
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   436
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   437
  val nat_consts = nat_ops @ [@{const numeral (nat)},
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   438
    @{const zero_class.zero (nat)}, @{const one_class.one (nat)}]
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   439
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   440
  val nat_int_coercions = [@{const of_nat (int)}, @{const nat}]
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   441
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   442
  val builtin_nat_ops = nat_int_coercions @ simple_nat_ops
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   443
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   444
  val is_nat_const = member (op aconv) nat_consts
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   445
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   446
  fun is_nat_const' @{const of_nat (int)} = true
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   447
    | is_nat_const' t = is_nat_const t
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   448
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   449
  val expands = map mk_meta_eq @{lemma
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   450
    "0 = nat 0"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   451
    "1 = nat 1"
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   452
    "(numeral :: num => nat) = (%i. nat (numeral i))"
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   453
    "op < = (%a b. int a < int b)"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   454
    "op <= = (%a b. int a <= int b)"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   455
    "Suc = (%a. nat (int a + 1))"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   456
    "op + = (%a b. nat (int a + int b))"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   457
    "op - = (%a b. nat (int a - int b))"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   458
    "op * = (%a b. nat (int a * int b))"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   459
    "op div = (%a b. nat (int a div int b))"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   460
    "op mod = (%a b. nat (int a mod int b))"
44890
22f665a2e91c new fastforce replacing fastsimp - less confusing name
nipkow
parents: 44718
diff changeset
   461
    by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   462
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   463
  val ints = map mk_meta_eq @{lemma
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   464
    "int 0 = 0"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   465
    "int 1 = 1"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   466
    "int (Suc n) = int n + 1"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   467
    "int (n + m) = int n + int m"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   468
    "int (n - m) = int (nat (int n - int m))"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   469
    "int (n * m) = int n * int m"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   470
    "int (n div m) = int n div int m"
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   471
    "int (n mod m) = int n mod int m"
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 61268
diff changeset
   472
    by (auto simp add: of_nat_mult zdiv_int zmod_int)}
50601
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   473
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   474
  val int_if = mk_meta_eq @{lemma
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   475
    "int (if P then n else m) = (if P then int n else int m)"
50601
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   476
    by simp}
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   477
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   478
  fun mk_number_eq ctxt i lhs =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   479
    let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   480
      val eq = Old_SMT_Utils.mk_cequals lhs (Numeral.mk_cnumber @{ctyp int} i)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51575
diff changeset
   481
      val tac =
62348
9a5f43dac883 dropped various legacy fact bindings
haftmann
parents: 61268
diff changeset
   482
        Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm of_nat_numeral}]) 1
54883
dd04a8b654fc proper context for norm_hhf and derived operations;
wenzelm
parents: 54489
diff changeset
   483
    in Goal.norm_result ctxt (Goal.prove_internal ctxt [] eq (K tac)) end
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   484
50601
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   485
  fun ite_conv cv1 cv2 =
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   486
    Conv.combination_conv (Conv.combination_conv (Conv.arg_conv cv1) cv2) cv2
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   487
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   488
  fun int_conv ctxt ct =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   489
    (case Thm.term_of ct of
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46497
diff changeset
   490
      @{const of_nat (int)} $ (n as (@{const numeral (nat)} $ _)) =>
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   491
        Conv.rewr_conv (mk_number_eq ctxt (snd (HOLogic.dest_number n)) ct)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   492
    | @{const of_nat (int)} $ _ =>
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   493
        (Conv.rewrs_conv ints then_conv Conv.sub_conv ints_conv ctxt) else_conv
50601
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   494
        (Conv.rewr_conv int_if then_conv
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   495
          ite_conv (nat_conv ctxt) (int_conv ctxt)) else_conv
74da81de127f refined normalization of theorems before giving them to SMT solvers (due to recent changes in rewr_conv, the rewriting of natural-number constants might leave some of them untouched)
boehmes
parents: 47207
diff changeset
   496
        Conv.sub_conv (Conv.top_sweep_conv nat_conv) ctxt
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   497
    | _ => Conv.no_conv) ct
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   498
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   499
  and ints_conv ctxt = Conv.top_sweep_conv int_conv ctxt
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   500
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   501
  and expand_conv ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   502
    Old_SMT_Utils.if_conv (is_nat_const o Term.head_of)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   503
      (expand_head_conv (Conv.rewrs_conv expands) then_conv ints_conv ctxt)
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41224
diff changeset
   504
      (int_conv ctxt)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   505
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   506
  and nat_conv ctxt = Old_SMT_Utils.if_exists_conv is_nat_const'
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   507
    (Conv.top_sweep_conv expand_conv ctxt)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   508
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   509
  val uses_nat_int = Term.exists_subterm (member (op aconv) nat_int_coercions)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   510
in
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   511
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   512
val nat_as_int_conv = nat_conv
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   513
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   514
fun add_nat_embedding thms =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   515
  if exists (uses_nat_int o Thm.prop_of) thms then (thms, nat_embedding)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   516
  else (thms, [])
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   517
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   518
val setup_nat_as_int =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   519
  Old_SMT_Builtin.add_builtin_typ_ext (@{typ nat}, K true) #>
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   520
  fold (Old_SMT_Builtin.add_builtin_fun_ext' o Term.dest_Const) builtin_nat_ops
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   521
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   522
end
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   523
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   524
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   525
(** normalize numerals **)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   526
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   527
local
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   528
  (*
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   529
    rewrite Numeral1 into 1
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   530
    rewrite - 0 into 0
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   531
  *)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   532
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   533
  fun is_irregular_number (Const (@{const_name numeral}, _) $ Const (@{const_name num.One}, _)) =
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   534
        true
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   535
    | is_irregular_number (Const (@{const_name uminus}, _) $ Const (@{const_name Groups.zero}, _)) =
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   536
        true
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   537
    | is_irregular_number _ =
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   538
        false;
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   539
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   540
  fun is_strange_number ctxt t = is_irregular_number t andalso Old_SMT_Builtin.is_builtin_num ctxt t;
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   541
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   542
  val proper_num_ss =
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 51575
diff changeset
   543
    simpset_of (put_simpset HOL_ss @{context}
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   544
      addsimps @{thms Num.numeral_One minus_zero})
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   545
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   546
  fun norm_num_conv ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   547
    Old_SMT_Utils.if_conv (is_strange_number ctxt)
54489
03ff4d1e6784 eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents: 54293
diff changeset
   548
      (Simplifier.rewrite (put_simpset proper_num_ss ctxt)) Conv.no_conv
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   549
in
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   550
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   551
fun normalize_numerals_conv ctxt =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   552
  Old_SMT_Utils.if_exists_conv (is_strange_number ctxt)
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   553
    (Conv.top_sweep_conv norm_num_conv ctxt)
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   554
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   555
end
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   556
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   557
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   558
(** combined unfoldings and rewritings **)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   559
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   560
fun unfold_conv ctxt =
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 54883
diff changeset
   561
  rewrite_case_bool_conv ctxt then_conv
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   562
  unfold_abs_min_max_conv ctxt then_conv
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   563
  nat_as_int_conv ctxt then_conv
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   564
  Thm.beta_conversion true
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   565
41300
528f5d00b542 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
boehmes
parents: 41280
diff changeset
   566
fun unfold1 ctxt = map (apsnd (Conv.fconv_rule (unfold_conv ctxt)))
528f5d00b542 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
boehmes
parents: 41280
diff changeset
   567
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   568
fun burrow_ids f ithms =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   569
  let
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   570
    val (is, thms) = split_list ithms
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   571
    val (thms', extra_thms) = f thms
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   572
  in (is ~~ thms') @ map (pair ~1) extra_thms end
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   573
51575
907efc894051 new, simpler implementation of monomorphization;
boehmes
parents: 50601
diff changeset
   574
fun unfold2 ctxt ithms =
41300
528f5d00b542 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
boehmes
parents: 41280
diff changeset
   575
  ithms
528f5d00b542 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
boehmes
parents: 41280
diff changeset
   576
  |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt)))
528f5d00b542 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
boehmes
parents: 41280
diff changeset
   577
  |> burrow_ids add_nat_embedding
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   578
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   579
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   580
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   581
(* overall normalization *)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   582
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   583
type extra_norm = Proof.context -> thm list * thm list -> thm list * thm list
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   584
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   585
structure Extra_Norms = Generic_Data
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   586
(
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   587
  type T = extra_norm Old_SMT_Utils.dict
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   588
  val empty = []
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   589
  val extend = I
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   590
  fun merge data = Old_SMT_Utils.dict_merge fst data
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   591
)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   592
41328
6792a5c92a58 avoid ML structure aliases (especially single-letter abbreviations)
boehmes
parents: 41327
diff changeset
   593
fun add_extra_norm (cs, norm) =
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   594
  Extra_Norms.map (Old_SMT_Utils.dict_update (cs, norm))
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   595
51575
907efc894051 new, simpler implementation of monomorphization;
boehmes
parents: 50601
diff changeset
   596
fun apply_extra_norms ctxt ithms =
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   597
  let
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   598
    val cs = Old_SMT_Config.solver_class_of ctxt
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
   599
    val es = Old_SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs
51575
907efc894051 new, simpler implementation of monomorphization;
boehmes
parents: 50601
diff changeset
   600
  in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   601
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   602
local
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   603
  val ignored = member (op =) [@{const_name All}, @{const_name Ex},
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   604
    @{const_name Let}, @{const_name If}, @{const_name HOL.eq}]
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   605
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   606
  val schematic_consts_of =
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   607
    let
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   608
      fun collect (@{const trigger} $ p $ t) =
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   609
            collect_trigger p #> collect t
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   610
        | collect (t $ u) = collect t #> collect u
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   611
        | collect (Abs (_, _, t)) = collect t
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   612
        | collect (t as Const (n, _)) = 
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   613
            if not (ignored n) then Monomorph.add_schematic_consts_of t else I
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   614
        | collect _ = I
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   615
      and collect_trigger t =
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   616
        let val dest = these o try HOLogic.dest_list 
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   617
        in fold (fold collect_pat o dest) (dest t) end
58057
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   618
      and collect_pat (Const (@{const_name pat}, _) $ t) = collect t
883f3c4c928e renaming theory 'Old_SMT'
blanchet
parents: 58055
diff changeset
   619
        | collect_pat (Const (@{const_name nopat}, _) $ t) = collect t
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   620
        | collect_pat _ = I
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   621
    in (fn t => collect t Symtab.empty) end
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   622
in
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   623
51575
907efc894051 new, simpler implementation of monomorphization;
boehmes
parents: 50601
diff changeset
   624
fun monomorph ctxt xthms =
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   625
  let val (xs, thms) = split_list xthms
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   626
  in
51575
907efc894051 new, simpler implementation of monomorphization;
boehmes
parents: 50601
diff changeset
   627
    map (pair 1) thms
907efc894051 new, simpler implementation of monomorphization;
boehmes
parents: 50601
diff changeset
   628
    |> Monomorph.monomorph schematic_consts_of ctxt
907efc894051 new, simpler implementation of monomorphization;
boehmes
parents: 50601
diff changeset
   629
    |> maps (uncurry (map o pair)) o map2 pair xs o map (map snd)
43116
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   630
  end
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   631
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   632
end
e0add071fa10 use new monomorphizer for SMT;
boehmes
parents: 42361
diff changeset
   633
41300
528f5d00b542 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
boehmes
parents: 41280
diff changeset
   634
fun normalize iwthms ctxt =
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   635
  iwthms
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   636
  |> gen_normalize ctxt
41300
528f5d00b542 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
boehmes
parents: 41280
diff changeset
   637
  |> unfold1 ctxt
51575
907efc894051 new, simpler implementation of monomorphization;
boehmes
parents: 50601
diff changeset
   638
  |> monomorph ctxt
907efc894051 new, simpler implementation of monomorphization;
boehmes
parents: 50601
diff changeset
   639
  |> unfold2 ctxt
907efc894051 new, simpler implementation of monomorphization;
boehmes
parents: 50601
diff changeset
   640
  |> apply_extra_norms ctxt
41300
528f5d00b542 perform monomorphization during normalization: schematic numerals might be monomorphized into built-in numerals and then numeral normalization is required
boehmes
parents: 41280
diff changeset
   641
  |> rpair ctxt
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40686
diff changeset
   642
41072
9f9bc1bdacef be more flexible: store SMT built-in symbols in generic contexts (not in theory contexts)
boehmes
parents: 41059
diff changeset
   643
val setup = Context.theory_map (
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   644
  setup_atomize #>
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   645
  setup_unfolded_quants #>
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   646
  setup_trigger #>
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   647
  setup_weight #>
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 54883
diff changeset
   648
  setup_case_bool #>
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   649
  setup_abs_min_max #>
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41072
diff changeset
   650
  setup_nat_as_int)
41059
d2b1fc1b8e19 centralized handling of built-in types and constants;
boehmes
parents: 40686
diff changeset
   651
36898
8e55aa1306c5 integrated SMT into the HOL image
boehmes
parents:
diff changeset
   652
end