src/HOL/Library/Old_SMT/old_smt_utils.ML
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 60642 48dd1cefb4ae
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_utils.ML
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     3
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     4
General utility functions.
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     5
*)
798aad2229c0 added prove reconstruction for injective functions;
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_UTILS =
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
     8
sig
41123
boehmes
parents: 40840
diff changeset
     9
  (*basic combinators*)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    10
  val repeat: ('a -> 'a option) -> 'a -> 'a
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    11
  val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    12
41124
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    13
  (*class dictionaries*)
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    14
  type class = string list
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    15
  val basicC: class
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
    16
  val string_of_class: class -> string
41124
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    17
  type 'a dict = (class * 'a) Ord_List.T
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    18
  val dict_map_default: class * 'a -> ('a -> 'a) -> 'a dict -> 'a dict
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    19
  val dict_update: class * 'a -> 'a dict -> 'a dict
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    20
  val dict_merge: ('a * 'a -> 'a) -> 'a dict * 'a dict -> 'a dict
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    21
  val dict_lookup: 'a dict -> class -> 'a list
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
    22
  val dict_get: 'a dict -> class -> 'a option
41124
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    23
41123
boehmes
parents: 40840
diff changeset
    24
  (*types*)
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
    25
  val dest_funT: int -> typ -> typ list * typ
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
    26
41123
boehmes
parents: 40840
diff changeset
    27
  (*terms*)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    28
  val dest_conj: term -> term * term
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    29
  val dest_disj: term -> term * term
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
    30
  val under_quant: (term -> 'a) -> term -> 'a
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
    31
  val is_number: term -> bool
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    32
41123
boehmes
parents: 40840
diff changeset
    33
  (*patterns and instantiations*)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    34
  val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    35
  val destT1: ctyp -> ctyp
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    36
  val destT2: ctyp -> ctyp
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    37
  val instTs: ctyp list -> ctyp list * cterm -> cterm
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    38
  val instT: ctyp -> ctyp * cterm -> cterm
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    39
  val instT': cterm -> ctyp * cterm -> cterm
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    40
41123
boehmes
parents: 40840
diff changeset
    41
  (*certified terms*)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    42
  val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    43
  val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    44
  val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    45
  val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    46
  val mk_cprop: cterm -> cterm
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    47
  val dest_cprop: cterm -> cterm
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    48
  val mk_cequals: cterm -> cterm -> cterm
41172
a17c2d669c40 the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents: 41127
diff changeset
    49
  val term_of: cterm -> term
a17c2d669c40 the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents: 41127
diff changeset
    50
  val prop_of: thm -> term
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    51
41123
boehmes
parents: 40840
diff changeset
    52
  (*conversions*)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    53
  val if_conv: (term -> bool) -> conv -> conv -> conv
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    54
  val if_true_conv: (term -> bool) -> conv -> 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: 41124
diff changeset
    55
  val if_exists_conv: (term -> bool) -> conv -> conv
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    56
  val binders_conv: (Proof.context -> 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: 41124
diff changeset
    57
  val under_quant_conv: (Proof.context * cterm list -> conv) ->
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
    58
    Proof.context -> conv
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    59
  val prop_conv: conv -> conv
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    60
end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    61
58058
1a0b18176548 add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents: 58057
diff changeset
    62
structure Old_SMT_Utils: OLD_SMT_UTILS =
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    63
struct
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    64
41123
boehmes
parents: 40840
diff changeset
    65
(* basic combinators *)
boehmes
parents: 40840
diff changeset
    66
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    67
fun repeat f =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    68
  let fun rep x = (case f x of SOME y => rep y | NONE => x)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    69
  in rep end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    70
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    71
fun repeat_yield f =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    72
  let fun rep x y = (case f x y of SOME (x', y') => rep x' y' | NONE => (x, y))
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    73
  in rep end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    74
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
    75
41124
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    76
(* class dictionaries *)
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    77
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    78
type class = string list
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    79
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    80
val basicC = []
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    81
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
    82
fun string_of_class [] = "basic"
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
    83
  | string_of_class cs = "basic." ^ space_implode "." cs
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
    84
41124
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    85
type 'a dict = (class * 'a) Ord_List.T
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    86
41301
0a00fd2f5351 derived SMT solver classes override inherited properties (properties of derived classes have a higher priority than properties of base classes)
boehmes
parents: 41280
diff changeset
    87
fun class_ord ((cs1, _), (cs2, _)) =
0a00fd2f5351 derived SMT solver classes override inherited properties (properties of derived classes have a higher priority than properties of base classes)
boehmes
parents: 41280
diff changeset
    88
  rev_order (list_ord fast_string_ord (cs1, cs2))
41124
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    89
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    90
fun dict_insert (cs, x) d =
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    91
  if AList.defined (op =) d cs then d
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    92
  else Ord_List.insert class_ord (cs, x) d
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    93
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    94
fun dict_map_default (cs, x) f =
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    95
  dict_insert (cs, x) #> AList.map_entry (op =) cs f
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    96
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    97
fun dict_update (e as (_, x)) = dict_map_default e (K x)
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    98
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
    99
fun dict_merge val_merge = sort class_ord o AList.join (op =) (K val_merge)
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
   100
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
   101
fun dict_lookup d cs =
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
   102
  let fun match (cs', x) = if is_prefix (op =) cs' cs then SOME x else NONE
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
   103
  in map_filter match d end
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
   104
41127
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   105
fun dict_get d cs =
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   106
  (case AList.lookup (op =) d cs of
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   107
    NONE => (case cs of [] => NONE | _ => dict_get d (take (length cs - 1) cs))
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   108
  | SOME x => SOME x)
2ea84c8535c6 re-implemented eta-expansion, lambda-lifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents: 41126
diff changeset
   109
41124
1de17a2de5ad moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents: 41123
diff changeset
   110
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   111
(* types *)
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   112
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   113
val dest_funT =
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   114
  let
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   115
    fun dest Ts 0 T = (rev Ts, T)
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   116
      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   117
      | dest _ _ T = raise TYPE ("not a function type", [T], [])
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   118
  in dest [] end
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   119
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   120
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   121
(* terms *)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   122
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   123
fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   124
  | dest_conj t = raise TERM ("not a conjunction", [t])
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   125
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   126
fun dest_disj (@{const HOL.disj} $ t $ u) = (t, u)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   127
  | dest_disj t = raise TERM ("not a disjunction", [t])
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   128
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   129
fun under_quant 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: 41124
diff changeset
   130
  (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: 41124
diff changeset
   131
    Const (@{const_name All}, _) $ Abs (_, _, u) => under_quant 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: 41124
diff changeset
   132
  | Const (@{const_name Ex}, _) $ Abs (_, _, u) => under_quant 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: 41124
diff changeset
   133
  | _ => 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: 41124
diff changeset
   134
41280
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
   135
val is_number =
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
   136
  let
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
   137
    fun is_num env (Const (@{const_name If}, _) $ _ $ t $ u) =
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
   138
          is_num env t andalso is_num env u
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
   139
      | is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) =
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
   140
          is_num (t :: env) u
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
   141
      | is_num env (Bound i) = i < length env andalso is_num env (nth env i)
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
   142
      | is_num _ t = can HOLogic.dest_number t
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
   143
  in is_num [] end
a7de9d36f4f2 only linear occurrences of multiplication are treated as built-in (SMT solvers only support linear arithmetic in general);
boehmes
parents: 41172
diff changeset
   144
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   145
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   146
(* patterns and instantiations *)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   147
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   148
fun mk_const_pat thy name destT =
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59590
diff changeset
   149
  let val cpat = Thm.global_cterm_of thy (Const (name, Sign.the_const_type thy name))
59586
ddf6deaadfe8 clarified signature;
wenzelm
parents: 59580
diff changeset
   150
  in (destT (Thm.ctyp_of_cterm cpat), cpat) end
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   151
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   152
val destT1 = hd o Thm.dest_ctyp
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   153
val destT2 = hd o tl o Thm.dest_ctyp
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   154
60642
48dd1cefb4ae simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
wenzelm
parents: 59634
diff changeset
   155
fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   156
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
59586
ddf6deaadfe8 clarified signature;
wenzelm
parents: 59580
diff changeset
   157
fun instT' ct = instT (Thm.ctyp_of_cterm ct)
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   158
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   159
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   160
(* certified terms *)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   161
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   162
fun dest_cabs ct ctxt =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   163
  (case Thm.term_of ct of
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   164
    Abs _ =>
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   165
      let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   166
      in (snd (Thm.dest_abs (SOME n) ct), ctxt') end
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   167
  | _ => raise CTERM ("no abstraction", [ct]))
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   168
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   169
val dest_all_cabs = repeat_yield (try o dest_cabs) 
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   170
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   171
fun dest_cbinder ct ctxt =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   172
  (case Thm.term_of ct of
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   173
    Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   174
  | _ => raise CTERM ("not a binder", [ct]))
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   175
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   176
val dest_all_cbinders = repeat_yield (try o dest_cbinder)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   177
59634
4b94cc030ba0 clarified context;
wenzelm
parents: 59621
diff changeset
   178
val mk_cprop = Thm.apply (Thm.cterm_of @{context} @{const Trueprop})
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   179
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   180
fun dest_cprop ct =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   181
  (case Thm.term_of ct of
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   182
    @{const Trueprop} $ _ => Thm.dest_arg ct
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   183
  | _ => raise CTERM ("not a property", [ct]))
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   184
56245
84fc7dfa3cd4 more qualified names;
wenzelm
parents: 54489
diff changeset
   185
val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   186
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   187
41172
a17c2d669c40 the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents: 41127
diff changeset
   188
val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
a17c2d669c40 the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents: 41127
diff changeset
   189
fun term_of ct = dest_prop (Thm.term_of ct)
a17c2d669c40 the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents: 41127
diff changeset
   190
fun prop_of thm = dest_prop (Thm.prop_of thm)
a17c2d669c40 the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents: 41127
diff changeset
   191
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   192
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   193
(* conversions *)
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   194
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   195
fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   196
40663
e080c9e68752 share and use more utility functions;
boehmes
parents: 40662
diff changeset
   197
fun if_true_conv pred cv = if_conv pred cv Conv.all_conv
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   198
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   199
fun if_exists_conv pred = if_true_conv (Term.exists_subterm pred)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   200
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   201
fun binders_conv cv ctxt =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   202
  Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   203
41126
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   204
fun under_quant_conv cv ctxt =
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   205
  let
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   206
    fun quant_conv inside 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: 41124
diff changeset
   207
      (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: 41124
diff changeset
   208
        Const (@{const_name All}, _) $ Abs _ =>
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   209
          Conv.binder_conv (under_conv cvs) ctxt
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   210
      | Const (@{const_name Ex}, _) $ Abs _ =>
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   211
          Conv.binder_conv (under_conv cvs) ctxt
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   212
      | _ => if inside then cv (ctxt, cvs) else 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: 41124
diff changeset
   213
    and under_conv cvs (cv, ctxt) = quant_conv true ctxt (cv :: cvs)
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   214
  in quant_conv false ctxt [] end
e0bd443c0fdd re-ordered SMT normalization code (eta-normalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents: 41124
diff changeset
   215
40662
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   216
fun prop_conv cv ct =
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   217
  (case Thm.term_of ct of
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   218
    @{const Trueprop} $ _ => Conv.arg_conv cv ct
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   219
  | _ => raise CTERM ("not a property", [ct]))
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   220
798aad2229c0 added prove reconstruction for injective functions;
boehmes
parents:
diff changeset
   221
end