src/HOL/Library/old_recdef.ML
author wenzelm
Wed, 09 Dec 2015 16:36:26 +0100
changeset 61814 1ca1142e1711
parent 61466 9a468c3a1fa1
child 62058 1cfd5d604937
permissions -rw-r--r--
clarified type Token.src: plain token list, with usual implicit value assignment; clarified type Token.name_value, notably for head of Token.src; clarified Attrib/Method check_src vs. parser;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOL/Tools/old_recdef.ML
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
     2
    Author:     Konrad Slind, Cambridge University Computer Laboratory
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
     3
    Author:     Lucas Dixon, University of Edinburgh
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
     4
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
     5
Old TFL/recdef package.
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
     6
*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
     7
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
     8
signature CASE_SPLIT =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
     9
sig
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    10
  (* try to recursively split conjectured thm to given list of thms *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    11
  val splitto : Proof.context -> thm list -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    12
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    13
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    14
signature UTILS =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    15
sig
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    16
  exception ERR of {module: string, func: string, mesg: string}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    17
  val end_itlist: ('a -> 'a -> 'a) -> 'a list -> 'a
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    18
  val itlist2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    19
  val pluck: ('a -> bool) -> 'a list -> 'a * 'a list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    20
  val zip3: 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    21
  val take: ('a -> 'b) -> int * 'a list -> 'b list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    22
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    23
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    24
signature USYNTAX =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    25
sig
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    26
  datatype lambda = VAR   of {Name : string, Ty : typ}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    27
                  | CONST of {Name : string, Ty : typ}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    28
                  | COMB  of {Rator: term, Rand : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    29
                  | LAMB  of {Bvar : term, Body : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    30
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    31
  val alpha : typ
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    32
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    33
  (* Types *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    34
  val type_vars  : typ -> typ list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    35
  val type_varsl : typ list -> typ list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    36
  val mk_vartype : string -> typ
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    37
  val is_vartype : typ -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    38
  val strip_prod_type : typ -> typ list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    39
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    40
  (* Terms *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    41
  val free_vars_lr : term -> term list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    42
  val type_vars_in_term : term -> typ list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    43
  val dest_term  : term -> lambda
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    44
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    45
  (* Prelogic *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    46
  val inst      : (typ*typ) list -> term -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    47
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    48
  (* Construction routines *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    49
  val mk_abs    :{Bvar  : term, Body : term} -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    50
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    51
  val mk_imp    :{ant : term, conseq :  term} -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    52
  val mk_select :{Bvar : term, Body : term} -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    53
  val mk_forall :{Bvar : term, Body : term} -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    54
  val mk_exists :{Bvar : term, Body : term} -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    55
  val mk_conj   :{conj1 : term, conj2 : term} -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    56
  val mk_disj   :{disj1 : term, disj2 : term} -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    57
  val mk_pabs   :{varstruct : term, body : term} -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    58
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    59
  (* Destruction routines *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    60
  val dest_const: term -> {Name : string, Ty : typ}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    61
  val dest_comb : term -> {Rator : term, Rand : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    62
  val dest_abs  : string list -> term -> {Bvar : term, Body : term} * string list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    63
  val dest_eq     : term -> {lhs : term, rhs : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    64
  val dest_imp    : term -> {ant : term, conseq : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    65
  val dest_forall : term -> {Bvar : term, Body : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    66
  val dest_exists : term -> {Bvar : term, Body : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    67
  val dest_neg    : term -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    68
  val dest_conj   : term -> {conj1 : term, conj2 : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    69
  val dest_disj   : term -> {disj1 : term, disj2 : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    70
  val dest_pair   : term -> {fst : term, snd : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    71
  val dest_pabs   : string list -> term -> {varstruct : term, body : term, used : string list}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    72
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    73
  val lhs   : term -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    74
  val rhs   : term -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    75
  val rand  : term -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    76
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    77
  (* Query routines *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    78
  val is_imp    : term -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    79
  val is_forall : term -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    80
  val is_exists : term -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    81
  val is_neg    : term -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    82
  val is_conj   : term -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    83
  val is_disj   : term -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    84
  val is_pair   : term -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    85
  val is_pabs   : term -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    86
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    87
  (* Construction of a term from a list of Preterms *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    88
  val list_mk_abs    : (term list * term) -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    89
  val list_mk_imp    : (term list * term) -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    90
  val list_mk_forall : (term list * term) -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    91
  val list_mk_conj   : term list -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    92
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    93
  (* Destructing a term to a list of Preterms *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    94
  val strip_comb     : term -> (term * term list)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    95
  val strip_abs      : term -> (term list * term)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    96
  val strip_imp      : term -> (term list * term)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    97
  val strip_forall   : term -> (term list * term)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    98
  val strip_exists   : term -> (term list * term)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
    99
  val strip_disj     : term -> term list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   100
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   101
  (* Miscellaneous *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   102
  val mk_vstruct : typ -> term list -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   103
  val gen_all    : term -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   104
  val find_term  : (term -> bool) -> term -> term option
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   105
  val dest_relation : term -> term * term * term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   106
  val is_WFR : term -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   107
  val ARB : typ -> term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   108
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   109
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   110
signature DCTERM =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   111
sig
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   112
  val dest_comb: cterm -> cterm * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   113
  val dest_abs: string option -> cterm -> cterm * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   114
  val capply: cterm -> cterm -> cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   115
  val cabs: cterm -> cterm -> cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   116
  val mk_conj: cterm * cterm -> cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   117
  val mk_disj: cterm * cterm -> cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   118
  val mk_exists: cterm * cterm -> cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   119
  val dest_conj: cterm -> cterm * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   120
  val dest_const: cterm -> {Name: string, Ty: typ}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   121
  val dest_disj: cterm -> cterm * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   122
  val dest_eq: cterm -> cterm * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   123
  val dest_exists: cterm -> cterm * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   124
  val dest_forall: cterm -> cterm * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   125
  val dest_imp: cterm -> cterm * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   126
  val dest_neg: cterm -> cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   127
  val dest_pair: cterm -> cterm * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   128
  val dest_var: cterm -> {Name:string, Ty:typ}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   129
  val is_conj: cterm -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   130
  val is_disj: cterm -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   131
  val is_eq: cterm -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   132
  val is_exists: cterm -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   133
  val is_forall: cterm -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   134
  val is_imp: cterm -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   135
  val is_neg: cterm -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   136
  val is_pair: cterm -> bool
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   137
  val list_mk_disj: cterm list -> cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   138
  val strip_abs: cterm -> cterm list * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   139
  val strip_comb: cterm -> cterm * cterm list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   140
  val strip_disj: cterm -> cterm list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   141
  val strip_exists: cterm -> cterm list * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   142
  val strip_forall: cterm -> cterm list * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   143
  val strip_imp: cterm -> cterm list * cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   144
  val drop_prop: cterm -> cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   145
  val mk_prop: cterm -> cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   146
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   147
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   148
signature RULES =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   149
sig
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   150
  val dest_thm: thm -> term list * term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   151
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   152
  (* Inference rules *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   153
  val REFL: cterm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   154
  val ASSUME: cterm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   155
  val MP: thm -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   156
  val MATCH_MP: thm -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   157
  val CONJUNCT1: thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   158
  val CONJUNCT2: thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   159
  val CONJUNCTS: thm -> thm list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   160
  val DISCH: cterm -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   161
  val UNDISCH: thm  -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   162
  val SPEC: cterm -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   163
  val ISPEC: cterm -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   164
  val ISPECL: cterm list -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   165
  val GEN: Proof.context -> cterm -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   166
  val GENL: Proof.context -> cterm list -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   167
  val LIST_CONJ: thm list -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   168
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   169
  val SYM: thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   170
  val DISCH_ALL: thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   171
  val FILTER_DISCH_ALL: (term -> bool) -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   172
  val SPEC_ALL: thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   173
  val GEN_ALL: Proof.context -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   174
  val IMP_TRANS: thm -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   175
  val PROVE_HYP: thm -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   176
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   177
  val CHOOSE: Proof.context -> cterm * thm -> thm -> thm
60781
2da59cdf531c updated to infer_instantiate;
wenzelm
parents: 60774
diff changeset
   178
  val EXISTS: Proof.context -> cterm * cterm -> thm -> thm
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   179
  val IT_EXISTS: Proof.context -> (cterm * cterm) list -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   180
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   181
  val EVEN_ORS: thm list -> thm list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   182
  val DISJ_CASESL: thm -> thm list -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   183
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   184
  val list_beta_conv: cterm -> cterm list -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   185
  val SUBS: Proof.context -> thm list -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   186
  val simpl_conv: Proof.context -> thm list -> cterm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   187
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   188
  val rbeta: thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   189
  val tracing: bool Unsynchronized.ref
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   190
  val CONTEXT_REWRITE_RULE: Proof.context ->
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   191
    term * term list * thm * thm list -> thm -> thm * term list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   192
  val RIGHT_ASSOC: Proof.context -> thm -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   193
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   194
  val prove: Proof.context -> bool -> term * tactic -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   195
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   196
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   197
signature THRY =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   198
sig
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   199
  val match_term: theory -> term -> term -> (term * term) list * (typ * typ) list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   200
  val match_type: theory -> typ -> typ -> (typ * typ) list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   201
  val typecheck: theory -> term -> cterm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   202
  (*datatype facts of various flavours*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   203
  val match_info: theory -> string -> {constructors: term list, case_const: term} option
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   204
  val induct_info: theory -> string -> {constructors: term list, nchotomy: thm} option
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   205
  val extract_info: theory -> {case_congs: thm list, case_rewrites: thm list}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   206
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   207
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   208
signature PRIM =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   209
sig
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   210
  val trace: bool Unsynchronized.ref
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   211
  val trace_thms: Proof.context -> string -> thm list -> unit
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   212
  val trace_cterm: Proof.context -> string -> cterm -> unit
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   213
  type pattern
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   214
  val mk_functional: theory -> term list -> {functional: term, pats: pattern list}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   215
  val wfrec_definition0: string -> term -> term -> theory -> thm * theory
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   216
  val post_definition: Proof.context -> thm list -> thm * pattern list ->
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   217
   {rules: thm,
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   218
    rows: int list,
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   219
    TCs: term list list,
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   220
    full_pats_TCs: (term * term list) list}
60699
7bf560b196a3 clarified context;
wenzelm
parents: 60642
diff changeset
   221
  val mk_induction: Proof.context ->
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   222
    {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   223
  val postprocess: Proof.context -> bool ->
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   224
    {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} ->
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   225
    {rules: thm, induction: thm, TCs: term list list} ->
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   226
    {rules: thm, induction: thm, nested_tcs: thm list}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   227
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   228
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   229
signature TFL =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   230
sig
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   231
  val define_i: bool -> thm list -> thm list -> xstring -> term -> term list -> Proof.context ->
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   232
    {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   233
  val define: bool -> thm list -> thm list -> xstring -> string -> string list -> Proof.context ->
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   234
    {lhs: term, rules: (thm * int) list, induct: thm, tcs: term list} * Proof.context
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   235
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   236
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   237
signature OLD_RECDEF =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   238
sig
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   239
  val get_recdef: theory -> string
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   240
    -> {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list} option
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   241
  val get_hints: Proof.context -> {simps: thm list, congs: (string * thm) list, wfs: thm list}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   242
  val simp_add: attribute
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   243
  val simp_del: attribute
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   244
  val cong_add: attribute
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   245
  val cong_del: attribute
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   246
  val wf_add: attribute
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   247
  val wf_del: attribute
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   248
  val add_recdef: bool -> xstring -> string -> ((binding * string) * Token.src list) list ->
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   249
    Token.src option -> theory -> theory
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   250
      * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   251
  val add_recdef_i: bool -> xstring -> term -> ((binding * term) * attribute list) list ->
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   252
    theory -> theory * {lhs: term, simps: thm list, rules: thm list list, induct: thm, tcs: term list}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   253
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   254
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   255
structure Old_Recdef: OLD_RECDEF =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   256
struct
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   257
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   258
(*** extra case splitting for TFL ***)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   259
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   260
structure CaseSplit: CASE_SPLIT =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   261
struct
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   262
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   263
(* make a casethm from an induction thm *)
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60699
diff changeset
   264
fun cases_thm_of_induct_thm ctxt =
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60699
diff changeset
   265
  Seq.hd o (ALLGOALS (fn i => REPEAT (eresolve_tac ctxt [Drule.thin_rl] i)));
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   266
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   267
(* get the case_thm (my version) from a type *)
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60699
diff changeset
   268
fun case_thm_of_ty ctxt ty  =
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   269
    let
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60699
diff changeset
   270
      val thy = Proof_Context.theory_of ctxt
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   271
      val ty_str = case ty of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   272
                     Type(ty_str, _) => ty_str
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   273
                   | TFree(s,_)  => error ("Free type: " ^ s)
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   274
                   | TVar((s,_),_) => error ("Free variable: " ^ s)
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   275
      val {induct, ...} = BNF_LFP_Compat.the_info thy [BNF_LFP_Compat.Keep_Nesting] ty_str
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   276
    in
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60699
diff changeset
   277
      cases_thm_of_induct_thm ctxt induct
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   278
    end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   279
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   280
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   281
(* for use when there are no prems to the subgoal *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   282
(* does a case split on the given variable *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   283
fun mk_casesplit_goal_thm ctxt (vstr,ty) gt =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   284
    let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   285
      val thy = Proof_Context.theory_of ctxt;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   286
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   287
      val x = Free(vstr,ty);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   288
      val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   289
60752
b48830b670a1 prefer tactics with explicit context;
wenzelm
parents: 60699
diff changeset
   290
      val case_thm = case_thm_of_ty ctxt ty;
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   291
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   292
      val abs_ct = Thm.cterm_of ctxt abst;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   293
      val free_ct = Thm.cterm_of ctxt x;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   294
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   295
      val (Pv, Dv, type_insts) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   296
          case (Thm.concl_of case_thm) of
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   297
            (_ $ (Pv $ (Dv as Var(_, Dty)))) =>
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   298
            (Pv, Dv,
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   299
             Sign.typ_match thy (Dty, ty) Vartab.empty)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   300
          | _ => error "not a valid case 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: 60524
diff changeset
   301
      val type_cinsts = map (fn (ixn, (S, T)) => ((ixn, S), Thm.ctyp_of ctxt T))
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   302
        (Vartab.dest type_insts);
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: 60524
diff changeset
   303
      val Pv = dest_Var (Envir.subst_term_types type_insts Pv);
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: 60524
diff changeset
   304
      val Dv = dest_Var (Envir.subst_term_types type_insts Dv);
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   305
    in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   306
      Conv.fconv_rule Drule.beta_eta_conversion
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   307
         (case_thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   308
            |> Thm.instantiate (type_cinsts, [])
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: 60524
diff changeset
   309
            |> Thm.instantiate ([], [(Pv, abs_ct), (Dv, free_ct)]))
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   310
    end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   311
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   312
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   313
(* the find_XXX_split functions are simply doing a lightwieght (I
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   314
think) term matching equivalent to find where to do the next split *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   315
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   316
(* assuming two twems are identical except for a free in one at a
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   317
subterm, or constant in another, ie assume that one term is a plit of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   318
another, then gives back the free variable that has been split. *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   319
exception find_split_exp of string
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   320
fun find_term_split (Free v, _ $ _) = SOME v
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   321
  | find_term_split (Free v, Const _) = SOME v
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   322
  | find_term_split (Free v, Abs _) = SOME v (* do we really want this case? *)
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   323
  | find_term_split (Free _, Var _) = NONE (* keep searching *)
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   324
  | find_term_split (a $ b, a2 $ b2) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   325
    (case find_term_split (a, a2) of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   326
       NONE => find_term_split (b,b2)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   327
     | vopt => vopt)
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   328
  | find_term_split (Abs(_,_,t1), Abs(_,_,t2)) =
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   329
    find_term_split (t1, t2)
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   330
  | find_term_split (Const (x,_), Const(x2,_)) =
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   331
    if x = x2 then NONE else (* keep searching *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   332
    raise find_split_exp (* stop now *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   333
            "Terms are not identical upto a free varaible! (Consts)"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   334
  | find_term_split (Bound i, Bound j) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   335
    if i = j then NONE else (* keep searching *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   336
    raise find_split_exp (* stop now *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   337
            "Terms are not identical upto a free varaible! (Bound)"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   338
  | find_term_split _ =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   339
    raise find_split_exp (* stop now *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   340
            "Terms are not identical upto a free varaible! (Other)";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   341
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   342
(* assume that "splitth" is a case split form of subgoal i of "genth",
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   343
then look for a free variable to split, breaking the subgoal closer to
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   344
splitth. *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   345
fun find_thm_split splitth i genth =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   346
    find_term_split (Logic.get_goal (Thm.prop_of genth) i,
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   347
                     Thm.concl_of splitth) handle find_split_exp _ => NONE;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   348
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   349
(* as above but searches "splitths" for a theorem that suggest a case split *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   350
fun find_thms_split splitths i genth =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   351
    Library.get_first (fn sth => find_thm_split sth i genth) splitths;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   352
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   353
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   354
(* split the subgoal i of "genth" until we get to a member of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   355
splitths. Assumes that genth will be a general form of splitths, that
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   356
can be case-split, as needed. Otherwise fails. Note: We assume that
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   357
all of "splitths" are split to the same level, and thus it doesn't
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   358
matter which one we choose to look for the next split. Simply add
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   359
search on splitthms and split variable, to change this.  *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   360
(* Note: possible efficiency measure: when a case theorem is no longer
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   361
useful, drop it? *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   362
(* Note: This should not be a separate tactic but integrated into the
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   363
case split done during recdef's case analysis, this would avoid us
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   364
having to (re)search for variables to split. *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   365
fun splitto ctxt splitths genth =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   366
    let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   367
      val _ = not (null splitths) orelse error "splitto: no given splitths";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   368
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   369
      (* check if we are a member of splitths - FIXME: quicker and
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   370
      more flexible with discrim net. *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   371
      fun solve_by_splitth th split =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   372
        Thm.biresolution (SOME ctxt) false [(false,split)] 1 th;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   373
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   374
      fun split th =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   375
        (case find_thms_split splitths 1 th of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   376
          NONE =>
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   377
           (writeln (cat_lines
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 61125
diff changeset
   378
            (["th:", Thm.string_of_thm ctxt th, "split ths:"] @
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 61125
diff changeset
   379
              map (Thm.string_of_thm ctxt) splitths @ ["\n--"]));
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   380
            error "splitto: cannot find variable to split on")
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   381
        | SOME v =>
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   382
            let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   383
              val gt = HOLogic.dest_Trueprop (#1 (Logic.dest_implies (Thm.prop_of th)));
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   384
              val split_thm = mk_casesplit_goal_thm ctxt v gt;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   385
              val (subthms, expf) = IsaND.fixed_subgoal_thms ctxt split_thm;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   386
            in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   387
              expf (map recsplitf subthms)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   388
            end)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   389
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   390
      and recsplitf th =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   391
        (* note: multiple unifiers! we only take the first element,
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   392
           probably fine -- there is probably only one anyway. *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   393
        (case get_first (Seq.pull o solve_by_splitth th) splitths of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   394
          NONE => split th
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   395
        | SOME (solved_th, _) => solved_th);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   396
    in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   397
      recsplitf genth
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   398
    end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   399
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   400
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   401
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   402
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   403
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   404
(*** basic utilities ***)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   405
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   406
structure Utils: UTILS =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   407
struct
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   408
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   409
(*standard exception for TFL*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   410
exception ERR of {module: string, func: string, mesg: string};
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   411
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   412
fun UTILS_ERR func mesg = ERR {module = "Utils", func = func, mesg = mesg};
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   413
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   414
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   415
fun end_itlist _ [] = raise (UTILS_ERR "end_itlist" "list too short")
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   416
  | end_itlist _ [x] = x
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   417
  | end_itlist f (x :: xs) = f x (end_itlist f xs);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   418
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   419
fun itlist2 f L1 L2 base_value =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   420
 let fun it ([],[]) = base_value
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   421
       | it ((a::rst1),(b::rst2)) = f a b (it (rst1,rst2))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   422
       | it _ = raise UTILS_ERR "itlist2" "different length lists"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   423
 in  it (L1,L2)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   424
 end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   425
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   426
fun pluck p  =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   427
  let fun remv ([],_) = raise UTILS_ERR "pluck" "item not found"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   428
        | remv (h::t, A) = if p h then (h, rev A @ t) else remv (t,h::A)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   429
  in fn L => remv(L,[])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   430
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   431
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   432
fun take f =
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   433
  let fun grab(0, _) = []
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   434
        | grab(n, x::rst) = f x::grab(n-1,rst)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   435
  in grab
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   436
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   437
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   438
fun zip3 [][][] = []
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   439
  | zip3 (x::l1) (y::l2) (z::l3) = (x,y,z)::zip3 l1 l2 l3
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   440
  | zip3 _ _ _ = raise UTILS_ERR "zip3" "different lengths";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   441
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   442
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   443
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   444
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   445
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   446
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   447
(*** emulation of HOL's abstract syntax functions ***)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   448
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   449
structure USyntax: USYNTAX =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   450
struct
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   451
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   452
infix 4 ##;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   453
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   454
fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg};
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   455
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   456
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   457
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   458
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   459
 *                            Types
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   460
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   461
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   462
val mk_prim_vartype = TVar;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   463
fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type});
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   464
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   465
(* But internally, it's useful *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   466
fun dest_vtype (TVar x) = x
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   467
  | dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   468
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   469
val is_vartype = can dest_vtype;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   470
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   471
val type_vars  = map mk_prim_vartype o Misc_Legacy.typ_tvars
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   472
fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   473
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   474
val alpha  = mk_vartype "'a"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   475
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   476
val strip_prod_type = HOLogic.flatten_tupleT;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   477
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   478
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   479
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   480
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   481
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   482
 *                              Terms
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   483
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   484
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   485
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   486
(* Free variables, in order of occurrence, from left to right in the
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   487
 * syntax tree. *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   488
fun free_vars_lr tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   489
  let fun memb x = let fun m[] = false | m(y::rst) = (x=y)orelse m rst in m end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   490
      fun add (t, frees) = case t of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   491
            Free   _ => if (memb t frees) then frees else t::frees
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   492
          | Abs (_,_,body) => add(body,frees)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   493
          | f$t =>  add(t, add(f, frees))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   494
          | _ => frees
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   495
  in rev(add(tm,[]))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   496
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   497
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   498
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   499
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   500
val type_vars_in_term = map mk_prim_vartype o Misc_Legacy.term_tvars;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   501
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   502
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   503
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   504
(* Prelogic *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   505
fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   506
fun inst theta = subst_vars (map dest_tybinding theta,[])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   507
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   508
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   509
(* Construction routines *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   510
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   511
fun mk_abs{Bvar as Var((s,_),ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   512
  | mk_abs{Bvar as Free(s,ty),Body}  = Abs(s,ty,abstract_over(Bvar,Body))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   513
  | mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   514
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   515
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   516
fun mk_imp{ant,conseq} =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   517
   let val c = Const(@{const_name HOL.implies},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   518
   in list_comb(c,[ant,conseq])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   519
   end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   521
fun mk_select (r as {Bvar,Body}) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   522
  let val ty = type_of Bvar
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   523
      val c = Const(@{const_name Eps},(ty --> HOLogic.boolT) --> ty)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   524
  in list_comb(c,[mk_abs r])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   525
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   526
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   527
fun mk_forall (r as {Bvar,Body}) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   528
  let val ty = type_of Bvar
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   529
      val c = Const(@{const_name All},(ty --> HOLogic.boolT) --> HOLogic.boolT)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   530
  in list_comb(c,[mk_abs r])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   531
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   532
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   533
fun mk_exists (r as {Bvar,Body}) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   534
  let val ty = type_of Bvar
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   535
      val c = Const(@{const_name Ex},(ty --> HOLogic.boolT) --> HOLogic.boolT)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   536
  in list_comb(c,[mk_abs r])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   537
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   538
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   539
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   540
fun mk_conj{conj1,conj2} =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   541
   let val c = Const(@{const_name HOL.conj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   542
   in list_comb(c,[conj1,conj2])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   543
   end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   544
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   545
fun mk_disj{disj1,disj2} =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   546
   let val c = Const(@{const_name HOL.disj},HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   547
   in list_comb(c,[disj1,disj2])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   548
   end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   549
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   550
fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   551
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   552
local
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   553
fun mk_uncurry (xt, yt, zt) =
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61268
diff changeset
   554
    Const(@{const_name case_prod}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   555
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   556
  | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   557
fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   558
in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   559
fun mk_pabs{varstruct,body} =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   560
 let fun mpa (varstruct, body) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   561
       if is_var varstruct
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   562
       then mk_abs {Bvar = varstruct, Body = body}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   563
       else let val {fst, snd} = dest_pair varstruct
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   564
            in mk_uncurry (type_of fst, type_of snd, type_of body) $
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   565
               mpa (fst, mpa (snd, body))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   566
            end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   567
 in mpa (varstruct, body) end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   568
 handle TYPE _ => raise USYN_ERR "mk_pabs" "";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   569
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   570
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   571
(* Destruction routines *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   572
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   573
datatype lambda = VAR   of {Name : string, Ty : typ}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   574
                | CONST of {Name : string, Ty : typ}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   575
                | COMB  of {Rator: term, Rand : term}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   576
                | LAMB  of {Bvar : term, Body : term};
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   577
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   578
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   579
fun dest_term(Var((s,_),ty)) = VAR{Name = s, Ty = ty}
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   580
  | dest_term(Free(s,ty))    = VAR{Name = s, Ty = ty}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   581
  | dest_term(Const(s,ty))   = CONST{Name = s, Ty = ty}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   582
  | dest_term(M$N)           = COMB{Rator=M,Rand=N}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   583
  | dest_term(Abs(s,ty,M))   = let  val v = Free(s,ty)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   584
                               in LAMB{Bvar = v, Body = Term.betapply (M,v)}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   585
                               end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   586
  | dest_term(Bound _)       = raise USYN_ERR "dest_term" "Bound";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   587
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   588
fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   589
  | dest_const _ = raise USYN_ERR "dest_const" "not a constant";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   590
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   591
fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   592
  | dest_comb _ =  raise USYN_ERR "dest_comb" "not a comb";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   593
60524
ffc1ee11759c removed dead code;
wenzelm
parents: 60523
diff changeset
   594
fun dest_abs used (a as Abs(s, ty, _)) =
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   595
     let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   596
       val s' = singleton (Name.variant_list used) s;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   597
       val v = Free(s', ty);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   598
     in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   599
     end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   600
  | dest_abs _ _ =  raise USYN_ERR "dest_abs" "not an abstraction";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   601
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   602
fun dest_eq(Const(@{const_name HOL.eq},_) $ M $ N) = {lhs=M, rhs=N}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   603
  | dest_eq _ = raise USYN_ERR "dest_eq" "not an equality";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   604
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   605
fun dest_imp(Const(@{const_name HOL.implies},_) $ M $ N) = {ant=M, conseq=N}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   606
  | dest_imp _ = raise USYN_ERR "dest_imp" "not an implication";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   607
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   608
fun dest_forall(Const(@{const_name All},_) $ (a as Abs _)) = fst (dest_abs [] a)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   609
  | dest_forall _ = raise USYN_ERR "dest_forall" "not a forall";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   610
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   611
fun dest_exists(Const(@{const_name Ex},_) $ (a as Abs _)) = fst (dest_abs [] a)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   612
  | dest_exists _ = raise USYN_ERR "dest_exists" "not an existential";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   613
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   614
fun dest_neg(Const(@{const_name Not},_) $ M) = M
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   615
  | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   616
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   617
fun dest_conj(Const(@{const_name HOL.conj},_) $ M $ N) = {conj1=M, conj2=N}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   618
  | dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   619
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   620
fun dest_disj(Const(@{const_name HOL.disj},_) $ M $ N) = {disj1=M, disj2=N}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   621
  | dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   622
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   623
fun mk_pair{fst,snd} =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   624
   let val ty1 = type_of fst
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   625
       val ty2 = type_of snd
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   626
       val c = Const(@{const_name Pair},ty1 --> ty2 --> prod_ty ty1 ty2)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   627
   in list_comb(c,[fst,snd])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   628
   end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   629
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   630
fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   631
  | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   632
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   633
61424
c3658c18b7bc prod_case as canonical name for product type eliminator
haftmann
parents: 61268
diff changeset
   634
local  fun ucheck t = (if #Name (dest_const t) = @{const_name case_prod} then t
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   635
                       else raise Match)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   636
in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   637
fun dest_pabs used tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   638
   let val ({Bvar,Body}, used') = dest_abs used tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   639
   in {varstruct = Bvar, body = Body, used = used'}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   640
   end handle Utils.ERR _ =>
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   641
          let val {Rator,Rand} = dest_comb tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   642
              val _ = ucheck Rator
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   643
              val {varstruct = lv, body, used = used'} = dest_pabs used Rand
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   644
              val {varstruct = rv, body, used = used''} = dest_pabs used' body
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   645
          in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   646
          end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   647
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   648
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   649
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   650
val lhs   = #lhs o dest_eq
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   651
val rhs   = #rhs o dest_eq
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   652
val rand  = #Rand o dest_comb
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   653
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   654
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   655
(* Query routines *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   656
val is_imp    = can dest_imp
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   657
val is_forall = can dest_forall
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   658
val is_exists = can dest_exists
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   659
val is_neg    = can dest_neg
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   660
val is_conj   = can dest_conj
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   661
val is_disj   = can dest_disj
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   662
val is_pair   = can dest_pair
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   663
val is_pabs   = can (dest_pabs [])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   664
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   665
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   666
(* Construction of a cterm from a list of Terms *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   667
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   668
fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   669
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   670
(* These others are almost never used *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   671
fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   672
fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   673
val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   674
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   675
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   676
(* Need to reverse? *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   677
fun gen_all tm = list_mk_forall(Misc_Legacy.term_frees tm, tm);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   678
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   679
(* Destructing a cterm to a list of Terms *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   680
fun strip_comb tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   681
   let fun dest(M$N, A) = dest(M, N::A)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   682
         | dest x = x
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   683
   in dest(tm,[])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   684
   end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   685
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   686
fun strip_abs(tm as Abs _) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   687
       let val ({Bvar,Body}, _) = dest_abs [] tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   688
           val (bvs, core) = strip_abs Body
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   689
       in (Bvar::bvs, core)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   690
       end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   691
  | strip_abs M = ([],M);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   692
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   693
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   694
fun strip_imp fm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   695
   if (is_imp fm)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   696
   then let val {ant,conseq} = dest_imp fm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   697
            val (was,wb) = strip_imp conseq
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   698
        in ((ant::was), wb)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   699
        end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   700
   else ([],fm);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   701
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   702
fun strip_forall fm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   703
   if (is_forall fm)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   704
   then let val {Bvar,Body} = dest_forall fm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   705
            val (bvs,core) = strip_forall Body
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   706
        in ((Bvar::bvs), core)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   707
        end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   708
   else ([],fm);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   709
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   710
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   711
fun strip_exists fm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   712
   if (is_exists fm)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   713
   then let val {Bvar, Body} = dest_exists fm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   714
            val (bvs,core) = strip_exists Body
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   715
        in (Bvar::bvs, core)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   716
        end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   717
   else ([],fm);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   718
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   719
fun strip_disj w =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   720
   if (is_disj w)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   721
   then let val {disj1,disj2} = dest_disj w
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   722
        in (strip_disj disj1@strip_disj disj2)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   723
        end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   724
   else [w];
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   725
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   726
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   727
(* Miscellaneous *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   728
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   729
fun mk_vstruct ty V =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   730
  let fun follow_prod_type (Type(@{type_name Product_Type.prod},[ty1,ty2])) vs =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   731
              let val (ltm,vs1) = follow_prod_type ty1 vs
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   732
                  val (rtm,vs2) = follow_prod_type ty2 vs1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   733
              in (mk_pair{fst=ltm, snd=rtm}, vs2) end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   734
        | follow_prod_type _ (v::vs) = (v,vs)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   735
  in #1 (follow_prod_type ty V)  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   736
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   737
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   738
(* Search a term for a sub-term satisfying the predicate p. *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   739
fun find_term p =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   740
   let fun find tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   741
      if (p tm) then SOME tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   742
      else case tm of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   743
          Abs(_,_,body) => find body
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   744
        | (t$u)         => (case find t of NONE => find u | some => some)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   745
        | _             => NONE
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   746
   in find
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   747
   end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   748
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   749
fun dest_relation tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   750
   if (type_of tm = HOLogic.boolT)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   751
   then let val (Const(@{const_name Set.member},_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   752
        in (R,y,x)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   753
        end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   754
   else raise USYN_ERR "dest_relation" "not a boolean term";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   755
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   756
fun is_WFR (Const(@{const_name Wellfounded.wf},_)$_) = true
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   757
  | is_WFR _                 = false;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   758
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   759
fun ARB ty = mk_select{Bvar=Free("v",ty),
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   760
                       Body=Const(@{const_name True},HOLogic.boolT)};
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   761
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   762
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   763
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   764
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   765
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   766
(*** derived cterm destructors ***)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   767
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   768
structure Dcterm: DCTERM =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   769
struct
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   770
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   771
fun ERR func mesg = Utils.ERR {module = "Dcterm", func = func, mesg = mesg};
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   772
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   773
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   774
fun dest_comb t = Thm.dest_comb t
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   775
  handle CTERM (msg, _) => raise ERR "dest_comb" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   776
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   777
fun dest_abs a t = Thm.dest_abs a t
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   778
  handle CTERM (msg, _) => raise ERR "dest_abs" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   779
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   780
fun capply t u = Thm.apply t u
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   781
  handle CTERM (msg, _) => raise ERR "capply" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   782
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   783
fun cabs a t = Thm.lambda a t
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   784
  handle CTERM (msg, _) => raise ERR "cabs" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   785
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   786
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   787
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   788
 * Some simple constructor functions.
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   789
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   790
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   791
val mk_hol_const = Thm.cterm_of @{theory_context HOL} o Const;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   792
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   793
fun mk_exists (r as (Bvar, Body)) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   794
  let val ty = Thm.typ_of_cterm Bvar
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   795
      val c = mk_hol_const(@{const_name Ex}, (ty --> HOLogic.boolT) --> HOLogic.boolT)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   796
  in capply c (uncurry cabs r) end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   797
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   798
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   799
local val c = mk_hol_const(@{const_name HOL.conj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   800
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   801
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   802
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   803
local val c = mk_hol_const(@{const_name HOL.disj}, HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   804
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   805
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   806
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   807
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   808
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   809
 * The primitives.
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   810
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   811
fun dest_const ctm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   812
   (case Thm.term_of ctm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   813
      of Const(s,ty) => {Name = s, Ty = ty}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   814
       | _ => raise ERR "dest_const" "not a constant");
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   815
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   816
fun dest_var ctm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   817
   (case Thm.term_of ctm
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   818
      of Var((s,_),ty) => {Name=s, Ty=ty}
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   819
       | Free(s,ty)    => {Name=s, Ty=ty}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   820
       |             _ => raise ERR "dest_var" "not a variable");
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   821
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   822
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   823
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   824
 * Derived destructor operations.
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   825
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   826
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   827
fun dest_monop expected tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   828
 let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   829
   fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   830
   val (c, N) = dest_comb tm handle Utils.ERR _ => err ();
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   831
   val name = #Name (dest_const c handle Utils.ERR _ => err ());
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   832
 in if name = expected then N else err () end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   833
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   834
fun dest_binop expected tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   835
 let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   836
   fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   837
   val (M, N) = dest_comb tm handle Utils.ERR _ => err ()
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   838
 in (dest_monop expected M, N) handle Utils.ERR _ => err () end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   839
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   840
fun dest_binder expected tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   841
  dest_abs NONE (dest_monop expected tm)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   842
  handle Utils.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   843
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   844
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   845
val dest_neg    = dest_monop @{const_name Not}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   846
val dest_pair   = dest_binop @{const_name Pair}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   847
val dest_eq     = dest_binop @{const_name HOL.eq}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   848
val dest_imp    = dest_binop @{const_name HOL.implies}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   849
val dest_conj   = dest_binop @{const_name HOL.conj}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   850
val dest_disj   = dest_binop @{const_name HOL.disj}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   851
val dest_exists = dest_binder @{const_name Ex}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   852
val dest_forall = dest_binder @{const_name All}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   853
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   854
(* Query routines *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   855
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   856
val is_eq     = can dest_eq
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   857
val is_imp    = can dest_imp
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   858
val is_forall = can dest_forall
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   859
val is_exists = can dest_exists
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   860
val is_neg    = can dest_neg
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   861
val is_conj   = can dest_conj
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   862
val is_disj   = can dest_disj
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   863
val is_pair   = can dest_pair
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   864
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   865
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   866
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   867
 * Iterated creation.
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   868
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   869
val list_mk_disj = Utils.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   870
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   871
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   872
 * Iterated destruction. (To the "right" in a term.)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   873
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   874
fun strip break tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   875
  let fun dest (p as (ctm,accum)) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   876
        let val (M,N) = break ctm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   877
        in dest (N, M::accum)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   878
        end handle Utils.ERR _ => p
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   879
  in dest (tm,[])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   880
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   881
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   882
fun rev2swap (x,l) = (rev l, x);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   883
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   884
val strip_comb   = strip (Library.swap o dest_comb)  (* Goes to the "left" *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   885
val strip_imp    = rev2swap o strip dest_imp
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   886
val strip_abs    = rev2swap o strip (dest_abs NONE)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   887
val strip_forall = rev2swap o strip dest_forall
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   888
val strip_exists = rev2swap o strip dest_exists
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   889
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   890
val strip_disj   = rev o (op::) o strip dest_disj
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   891
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   892
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   893
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   894
 * Going into and out of prop
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   895
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   896
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   897
fun is_Trueprop ct =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   898
  (case Thm.term_of ct of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   899
    Const (@{const_name Trueprop}, _) $ _ => true
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   900
  | _ => false);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   901
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   902
fun mk_prop ct = if is_Trueprop ct then ct else Thm.apply @{cterm Trueprop} ct;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   903
fun drop_prop ct = if is_Trueprop ct then Thm.dest_arg ct else ct;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   904
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   905
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   906
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   907
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   908
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   909
(*** emulation of HOL inference rules for TFL ***)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   910
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   911
structure Rules: RULES =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   912
struct
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   913
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   914
fun RULES_ERR func mesg = Utils.ERR {module = "Rules", func = func, mesg = mesg};
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   915
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   916
60949
ccbf9379e355 added Thm.chyps_of;
wenzelm
parents: 60825
diff changeset
   917
fun cconcl thm = Dcterm.drop_prop (Thm.cprop_of thm);
ccbf9379e355 added Thm.chyps_of;
wenzelm
parents: 60825
diff changeset
   918
fun chyps thm = map Dcterm.drop_prop (Thm.chyps_of thm);
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   919
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   920
fun dest_thm thm =
61038
wenzelm
parents: 60949
diff changeset
   921
  (map HOLogic.dest_Trueprop (Thm.hyps_of thm), HOLogic.dest_Trueprop (Thm.prop_of thm))
wenzelm
parents: 60949
diff changeset
   922
    handle TERM _ => raise RULES_ERR "dest_thm" "missing Trueprop";
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   923
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   924
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   925
(* Inference rules *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   926
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   927
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   928
 *        Equality (one step)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   929
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   930
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   931
fun REFL tm = Thm.reflexive tm RS meta_eq_to_obj_eq
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   932
  handle THM (msg, _, _) => raise RULES_ERR "REFL" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   933
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   934
fun SYM thm = thm RS sym
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   935
  handle THM (msg, _, _) => raise RULES_ERR "SYM" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   936
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   937
fun ALPHA thm ctm1 =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   938
  let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   939
    val ctm2 = Thm.cprop_of thm;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   940
    val ctm2_eq = Thm.reflexive ctm2;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   941
    val ctm1_eq = Thm.reflexive ctm1;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   942
  in Thm.equal_elim (Thm.transitive ctm2_eq ctm1_eq) thm end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   943
  handle THM (msg, _, _) => raise RULES_ERR "ALPHA" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   944
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   945
fun rbeta th =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   946
  (case Dcterm.strip_comb (cconcl th) of
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
   947
    (_, [_, r]) => Thm.transitive th (Thm.beta_conversion false r)
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   948
  | _ => raise RULES_ERR "rbeta" "");
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   949
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   950
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   951
(*----------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   952
 *        Implication and the assumption list
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   953
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   954
 * Assumptions get stuck on the meta-language assumption list. Implications
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   955
 * are in the object language, so discharging an assumption "A" from theorem
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   956
 * "B" results in something that looks like "A --> B".
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   957
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   958
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   959
fun ASSUME ctm = Thm.assume (Dcterm.mk_prop ctm);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   960
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   961
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   962
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   963
 * Implication in TFL is -->. Meta-language implication (==>) is only used
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   964
 * in the implementation of some of the inference rules below.
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   965
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   966
fun MP th1 th2 = th2 RS (th1 RS mp)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   967
  handle THM (msg, _, _) => raise RULES_ERR "MP" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   968
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   969
(*forces the first argument to be a proposition if necessary*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   970
fun DISCH tm thm = Thm.implies_intr (Dcterm.mk_prop tm) thm COMP impI
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   971
  handle THM (msg, _, _) => raise RULES_ERR "DISCH" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   972
60949
ccbf9379e355 added Thm.chyps_of;
wenzelm
parents: 60825
diff changeset
   973
fun DISCH_ALL thm = fold_rev DISCH (Thm.chyps_of thm) thm;
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   974
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   975
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   976
fun FILTER_DISCH_ALL P thm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   977
 let fun check tm = P (Thm.term_of tm)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   978
 in  fold_rev (fn tm => fn th => if check tm then DISCH tm th else th) (chyps thm) thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   979
 end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   980
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   981
fun UNDISCH thm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   982
   let val tm = Dcterm.mk_prop (#1 (Dcterm.dest_imp (cconcl thm)))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   983
   in Thm.implies_elim (thm RS mp) (ASSUME tm) end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   984
   handle Utils.ERR _ => raise RULES_ERR "UNDISCH" ""
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   985
     | THM _ => raise RULES_ERR "UNDISCH" "";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   986
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   987
fun PROVE_HYP ath bth = MP (DISCH (cconcl ath) bth) ath;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   988
60522
wenzelm
parents: 60521
diff changeset
   989
fun IMP_TRANS th1 th2 = th2 RS (th1 RS @{thm tfl_imp_trans})
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   990
  handle THM (msg, _, _) => raise RULES_ERR "IMP_TRANS" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   991
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   992
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   993
(*----------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   994
 *        Conjunction
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   995
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   996
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   997
fun CONJUNCT1 thm = thm RS conjunct1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   998
  handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT1" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
   999
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1000
fun CONJUNCT2 thm = thm RS conjunct2
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1001
  handle THM (msg, _, _) => raise RULES_ERR "CONJUNCT2" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1002
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1003
fun CONJUNCTS th = CONJUNCTS (CONJUNCT1 th) @ CONJUNCTS (CONJUNCT2 th) handle Utils.ERR _ => [th];
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1004
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1005
fun LIST_CONJ [] = raise RULES_ERR "LIST_CONJ" "empty list"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1006
  | LIST_CONJ [th] = th
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1007
  | LIST_CONJ (th :: rst) = MP (MP (conjI COMP (impI RS impI)) th) (LIST_CONJ rst)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1008
      handle THM (msg, _, _) => raise RULES_ERR "LIST_CONJ" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1009
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1010
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1011
(*----------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1012
 *        Disjunction
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1013
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1014
local
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1015
  val prop = Thm.prop_of disjI1
60524
ffc1ee11759c removed dead code;
wenzelm
parents: 60523
diff changeset
  1016
  val [_,Q] = Misc_Legacy.term_vars prop
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1017
  val disj1 = Thm.forall_intr (Thm.cterm_of @{context} Q) disjI1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1018
in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1019
fun DISJ1 thm tm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj1)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1020
  handle THM (msg, _, _) => raise RULES_ERR "DISJ1" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1021
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1022
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1023
local
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1024
  val prop = Thm.prop_of disjI2
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
  1025
  val [P,_] = Misc_Legacy.term_vars prop
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1026
  val disj2 = Thm.forall_intr (Thm.cterm_of @{context} P) disjI2
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1027
in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1028
fun DISJ2 tm thm = thm RS (Thm.forall_elim (Dcterm.drop_prop tm) disj2)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1029
  handle THM (msg, _, _) => raise RULES_ERR "DISJ2" msg;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1030
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1031
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1032
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1033
(*----------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1034
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1035
 *                   A1 |- M1, ..., An |- Mn
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1036
 *     ---------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1037
 *     [A1 |- M1 \/ ... \/ Mn, ..., An |- M1 \/ ... \/ Mn]
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1038
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1039
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1040
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1041
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1042
fun EVEN_ORS thms =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1043
  let fun blue ldisjs [] _ = []
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1044
        | blue ldisjs (th::rst) rdisjs =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1045
            let val tail = tl rdisjs
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1046
                val rdisj_tl = Dcterm.list_mk_disj tail
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1047
            in fold_rev DISJ2 ldisjs (DISJ1 th rdisj_tl)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1048
               :: blue (ldisjs @ [cconcl th]) rst tail
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1049
            end handle Utils.ERR _ => [fold_rev DISJ2 ldisjs th]
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1050
   in blue [] thms (map cconcl thms) end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1051
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1052
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1053
(*----------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1054
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1055
 *         A |- P \/ Q   B,P |- R    C,Q |- R
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1056
 *     ---------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1057
 *                     A U B U C |- R
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1058
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1059
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1060
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1061
fun DISJ_CASES th1 th2 th3 =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1062
  let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1063
    val c = Dcterm.drop_prop (cconcl th1);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1064
    val (disj1, disj2) = Dcterm.dest_disj c;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1065
    val th2' = DISCH disj1 th2;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1066
    val th3' = DISCH disj2 th3;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1067
  in
60522
wenzelm
parents: 60521
diff changeset
  1068
    th3' RS (th2' RS (th1 RS @{thm tfl_disjE}))
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1069
      handle THM (msg, _, _) => raise RULES_ERR "DISJ_CASES" msg
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1070
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1071
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1072
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1073
(*-----------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1074
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1075
 *       |- A1 \/ ... \/ An     [A1 |- M, ..., An |- M]
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1076
 *     ---------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1077
 *                           |- M
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1078
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1079
 * Note. The list of theorems may be all jumbled up, so we have to
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1080
 * first organize it to align with the first argument (the disjunctive
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1081
 * theorem).
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1082
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1083
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1084
fun organize eq =    (* a bit slow - analogous to insertion sort *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1085
 let fun extract a alist =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1086
     let fun ex (_,[]) = raise RULES_ERR "organize" "not a permutation.1"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1087
           | ex(left,h::t) = if (eq h a) then (h,rev left@t) else ex(h::left,t)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1088
     in ex ([],alist)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1089
     end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1090
     fun place [] [] = []
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1091
       | place (a::rst) alist =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1092
           let val (item,next) = extract a alist
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1093
           in item::place rst next
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1094
           end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1095
       | place _ _ = raise RULES_ERR "organize" "not a permutation.2"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1096
 in place
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1097
 end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1098
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1099
fun DISJ_CASESL disjth thl =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1100
   let val c = cconcl disjth
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1101
       fun eq th atm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1102
        exists (fn t => HOLogic.dest_Trueprop t aconv Thm.term_of atm) (Thm.hyps_of th)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1103
       val tml = Dcterm.strip_disj c
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
  1104
       fun DL _ [] = raise RULES_ERR "DISJ_CASESL" "no cases"
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1105
         | DL th [th1] = PROVE_HYP th th1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1106
         | DL th [th1,th2] = DISJ_CASES th th1 th2
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1107
         | DL th (th1::rst) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1108
            let val tm = #2 (Dcterm.dest_disj (Dcterm.drop_prop(cconcl th)))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1109
             in DISJ_CASES th th1 (DL (ASSUME tm) rst) end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1110
   in DL disjth (organize eq tml thl)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1111
   end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1112
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1113
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1114
(*----------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1115
 *        Universals
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1116
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1117
local (* this is fragile *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1118
  val prop = Thm.prop_of spec
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1119
  val x = hd (tl (Misc_Legacy.term_vars prop))
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: 60524
diff changeset
  1120
  val TV = dest_TVar (type_of x)
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1121
  val gspec = Thm.forall_intr (Thm.cterm_of @{context} x) spec
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1122
in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1123
fun SPEC tm 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: 60524
diff changeset
  1124
   let val gspec' = Drule.instantiate_normalize ([(TV, Thm.ctyp_of_cterm tm)], []) gspec
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1125
   in thm RS (Thm.forall_elim tm gspec') end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1126
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1127
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1128
fun SPEC_ALL thm = fold SPEC (#1 (Dcterm.strip_forall(cconcl thm))) thm;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1129
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1130
val ISPEC = SPEC
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1131
val ISPECL = fold ISPEC;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1132
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1133
(* Not optimized! Too complicated. *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1134
local
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1135
  val prop = Thm.prop_of allI
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1136
  val [P] = Misc_Legacy.add_term_vars (prop, [])
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: 60524
diff changeset
  1137
  fun cty_theta ctxt = map (fn (i, (S, ty)) => ((i, S), Thm.ctyp_of ctxt ty))
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1138
  fun ctm_theta ctxt =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1139
    map (fn (i, (_, tm2)) =>
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1140
      let val ctm2 = Thm.cterm_of ctxt tm2
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: 60524
diff changeset
  1141
      in ((i, Thm.typ_of_cterm ctm2), ctm2) end)
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1142
  fun certify ctxt (ty_theta,tm_theta) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1143
    (cty_theta ctxt (Vartab.dest ty_theta),
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1144
     ctm_theta ctxt (Vartab.dest tm_theta))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1145
in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1146
fun GEN ctxt v th =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1147
   let val gth = Thm.forall_intr v th
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1148
       val thy = Proof_Context.theory_of ctxt
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1149
       val Const(@{const_name Pure.all},_)$Abs(x,ty,rst) = Thm.prop_of gth
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1150
       val P' = Abs(x,ty, HOLogic.dest_Trueprop rst)  (* get rid of trueprop *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1151
       val theta = Pattern.match thy (P,P') (Vartab.empty, Vartab.empty);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1152
       val allI2 = Drule.instantiate_normalize (certify ctxt theta) allI
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1153
       val thm = Thm.implies_elim allI2 gth
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1154
       val tp $ (A $ Abs(_,_,M)) = Thm.prop_of thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1155
       val prop' = tp $ (A $ Abs(x,ty,M))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1156
   in ALPHA thm (Thm.cterm_of ctxt prop') end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1157
end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1158
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1159
fun GENL ctxt = fold_rev (GEN ctxt);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1160
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1161
fun GEN_ALL ctxt thm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1162
  let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1163
    val prop = Thm.prop_of thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1164
    val vlist = map (Thm.cterm_of ctxt) (Misc_Legacy.add_term_vars (prop, []))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1165
  in GENL ctxt vlist thm end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1166
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1167
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1168
fun MATCH_MP th1 th2 =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1169
   if (Dcterm.is_forall (Dcterm.drop_prop(cconcl th1)))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1170
   then MATCH_MP (th1 RS spec) th2
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1171
   else MP th1 th2;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1172
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1173
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1174
(*----------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1175
 *        Existentials
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1176
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1177
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1178
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1179
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1180
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1181
 * Existential elimination
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1182
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1183
 *      A1 |- ?x.t[x]   ,   A2, "t[v]" |- t'
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1184
 *      ------------------------------------     (variable v occurs nowhere)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1185
 *                A1 u A2 |- t'
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1186
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1187
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1188
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1189
fun CHOOSE ctxt (fvar, exth) fact =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1190
  let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1191
    val lam = #2 (Dcterm.dest_comb (Dcterm.drop_prop (cconcl exth)))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1192
    val redex = Dcterm.capply lam fvar
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1193
    val t$u = Thm.term_of redex
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1194
    val residue = Thm.cterm_of ctxt (Term.betapply (t, u))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1195
  in
60522
wenzelm
parents: 60521
diff changeset
  1196
    GEN ctxt fvar (DISCH residue fact) RS (exth RS @{thm tfl_exE})
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1197
      handle THM (msg, _, _) => raise RULES_ERR "CHOOSE" msg
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1198
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1199
60781
2da59cdf531c updated to infer_instantiate;
wenzelm
parents: 60774
diff changeset
  1200
fun EXISTS ctxt (template,witness) thm =
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1201
  let val abstr = #2 (Dcterm.dest_comb template) in
60781
2da59cdf531c updated to infer_instantiate;
wenzelm
parents: 60774
diff changeset
  1202
    thm RS (infer_instantiate ctxt [(("P", 0), abstr), (("x", 0), witness)] exI)
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1203
      handle THM (msg, _, _) => raise RULES_ERR "EXISTS" msg
60781
2da59cdf531c updated to infer_instantiate;
wenzelm
parents: 60774
diff changeset
  1204
  end;
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1205
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1206
(*----------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1207
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1208
 *       A |- M[x_1,...,x_n]
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1209
 *   ----------------------------   [(x |-> y)_1,...,(x |-> y)_n]
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1210
 *       A |- ?y_1...y_n. M
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1211
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1212
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1213
(* Could be improved, but needs "subst_free" for certified terms *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1214
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1215
fun IT_EXISTS ctxt blist th =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1216
  let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1217
    val blist' = map (apply2 Thm.term_of) blist
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1218
    fun ex v M = Thm.cterm_of ctxt (USyntax.mk_exists{Bvar=v,Body = M})
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1219
  in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1220
    fold_rev (fn (b as (r1,r2)) => fn thm =>
60781
2da59cdf531c updated to infer_instantiate;
wenzelm
parents: 60774
diff changeset
  1221
        EXISTS ctxt (ex r2 (subst_free [b]
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1222
                   (HOLogic.dest_Trueprop(Thm.prop_of thm))), Thm.cterm_of ctxt r1)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1223
              thm)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1224
       blist' th
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1225
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1226
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1227
(*----------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1228
 *        Rewriting
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1229
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1230
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1231
fun SUBS ctxt thl =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1232
  rewrite_rule ctxt (map (fn th => th RS eq_reflection handle THM _ => th) thl);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1233
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1234
val rew_conv = Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE));
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1235
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1236
fun simpl_conv ctxt thl ctm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1237
 rew_conv (ctxt addsimps thl) ctm RS meta_eq_to_obj_eq;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1238
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1239
60522
wenzelm
parents: 60521
diff changeset
  1240
fun RIGHT_ASSOC ctxt = rewrite_rule ctxt @{thms tfl_disj_assoc};
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1241
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1242
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1243
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1244
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1245
 *                  TERMINATION CONDITION EXTRACTION
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1246
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1247
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1248
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1249
(* Object language quantifier, i.e., "!" *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1250
fun Forall v M = USyntax.mk_forall{Bvar=v, Body=M};
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1251
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1252
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1253
(* Fragile: it's a cong if it is not "R y x ==> cut f R x y = f y" *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1254
fun is_cong thm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1255
  case (Thm.prop_of thm) of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1256
    (Const(@{const_name Pure.imp},_)$(Const(@{const_name Trueprop},_)$ _) $
60524
ffc1ee11759c removed dead code;
wenzelm
parents: 60523
diff changeset
  1257
      (Const(@{const_name Pure.eq},_) $ (Const (@{const_name Wfrec.cut},_) $ _ $ _ $ _ $ _) $ _)) =>
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1258
        false
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1259
  | _ => true;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1260
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1261
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1262
fun dest_equal(Const (@{const_name Pure.eq},_) $
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1263
               (Const (@{const_name Trueprop},_) $ lhs)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1264
               $ (Const (@{const_name Trueprop},_) $ rhs)) = {lhs=lhs, rhs=rhs}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1265
  | dest_equal(Const (@{const_name Pure.eq},_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1266
  | dest_equal tm = USyntax.dest_eq tm;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1267
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1268
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1269
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1270
fun dest_all used (Const(@{const_name Pure.all},_) $ (a as Abs _)) = USyntax.dest_abs used a
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1271
  | dest_all _ _ = raise RULES_ERR "dest_all" "not a !!";
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1272
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1273
val is_all = can (dest_all []);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1274
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1275
fun strip_all used fm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1276
   if (is_all fm)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1277
   then let val ({Bvar, Body}, used') = dest_all used fm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1278
            val (bvs, core, used'') = strip_all used' Body
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1279
        in ((Bvar::bvs), core, used'')
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1280
        end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1281
   else ([], fm, used);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1282
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1283
fun list_break_all(Const(@{const_name Pure.all},_) $ Abs (s,ty,body)) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1284
     let val (L,core) = list_break_all body
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1285
     in ((s,ty)::L, core)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1286
     end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1287
  | list_break_all tm = ([],tm);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1288
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1289
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1290
 * Rename a term of the form
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1291
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1292
 *      !!x1 ...xn. x1=M1 ==> ... ==> xn=Mn
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1293
 *                  ==> ((%v1...vn. Q) x1 ... xn = g x1 ... xn.
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1294
 * to one of
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1295
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1296
 *      !!v1 ... vn. v1=M1 ==> ... ==> vn=Mn
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1297
 *      ==> ((%v1...vn. Q) v1 ... vn = g v1 ... vn.
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1298
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1299
 * This prevents name problems in extraction, and helps the result to read
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1300
 * better. There is a problem with varstructs, since they can introduce more
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1301
 * than n variables, and some extra reasoning needs to be done.
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1302
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1303
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1304
fun get ([],_,L) = rev L
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1305
  | get (ant::rst,n,L) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1306
      case (list_break_all ant)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1307
        of ([],_) => get (rst, n+1,L)
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
  1308
         | (_,body) =>
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1309
            let val eq = Logic.strip_imp_concl body
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
  1310
                val (f,_) = USyntax.strip_comb (get_lhs eq)
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1311
                val (vstrl,_) = USyntax.strip_abs f
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1312
                val names  =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1313
                  Name.variant_list (Misc_Legacy.add_term_names(body, [])) (map (#1 o dest_Free) vstrl)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1314
            in get (rst, n+1, (names,n)::L) end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1315
            handle TERM _ => get (rst, n+1, L)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1316
              | Utils.ERR _ => get (rst, n+1, L);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1317
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1318
(* Note: Thm.rename_params_rule counts from 1, not 0 *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1319
fun rename thm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1320
  let
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1321
    val ants = Logic.strip_imp_prems (Thm.prop_of thm)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1322
    val news = get (ants,1,[])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1323
  in fold Thm.rename_params_rule news thm end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1324
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1325
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1326
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1327
 * Beta-conversion to the rhs of an equation (taken from hol90/drule.sml)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1328
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1329
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1330
fun list_beta_conv tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1331
  let fun rbeta th = Thm.transitive th (Thm.beta_conversion false (#2(Dcterm.dest_eq(cconcl th))))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1332
      fun iter [] = Thm.reflexive tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1333
        | iter (v::rst) = rbeta (Thm.combination(iter rst) (Thm.reflexive v))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1334
  in iter  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1335
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1336
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1337
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1338
 * Trace information for the rewriter
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1339
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1340
val tracing = Unsynchronized.ref false;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1341
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1342
fun say s = if !tracing then writeln s else ();
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1343
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1344
fun print_thms ctxt s L =
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 61125
diff changeset
  1345
  say (cat_lines (s :: map (Thm.string_of_thm ctxt) L));
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1346
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1347
fun print_term ctxt s t =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1348
  say (cat_lines [s, Syntax.string_of_term ctxt t]);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1349
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1350
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1351
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1352
 * General abstraction handlers, should probably go in USyntax.
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1353
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1354
fun mk_aabs (vstr, body) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1355
  USyntax.mk_abs {Bvar = vstr, Body = body}
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1356
  handle Utils.ERR _ => USyntax.mk_pabs {varstruct = vstr, body = body};
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1357
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1358
fun list_mk_aabs (vstrl,tm) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1359
    fold_rev (fn vstr => fn tm => mk_aabs(vstr,tm)) vstrl tm;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1360
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1361
fun dest_aabs used tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1362
   let val ({Bvar,Body}, used') = USyntax.dest_abs used tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1363
   in (Bvar, Body, used') end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1364
   handle Utils.ERR _ =>
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1365
     let val {varstruct, body, used} = USyntax.dest_pabs used tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1366
     in (varstruct, body, used) end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1367
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1368
fun strip_aabs used tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1369
   let val (vstr, body, used') = dest_aabs used tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1370
       val (bvs, core, used'') = strip_aabs used' body
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1371
   in (vstr::bvs, core, used'') end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1372
   handle Utils.ERR _ => ([], tm, used);
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1373
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1374
fun dest_combn tm 0 = (tm,[])
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1375
  | dest_combn tm n =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1376
     let val {Rator,Rand} = USyntax.dest_comb tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1377
         val (f,rands) = dest_combn Rator (n-1)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1378
     in (f,Rand::rands)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1379
     end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1380
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1381
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1382
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1383
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1384
local fun dest_pair M = let val {fst,snd} = USyntax.dest_pair M in (fst,snd) end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1385
      fun mk_fst tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1386
          let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1387
          in  Const (@{const_name Product_Type.fst}, ty --> fty) $ tm  end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1388
      fun mk_snd tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1389
          let val ty as Type(@{type_name Product_Type.prod}, [fty,sty]) = type_of tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1390
          in  Const (@{const_name Product_Type.snd}, ty --> sty) $ tm  end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1391
in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1392
fun XFILL tych x vstruct =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1393
  let fun traverse p xocc L =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1394
        if (is_Free p)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1395
        then tych xocc::L
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1396
        else let val (p1,p2) = dest_pair p
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1397
             in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1398
             end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1399
  in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1400
  traverse vstruct x []
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1401
end end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1402
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1403
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1404
 * Replace a free tuple (vstr) by a universally quantified variable (a).
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1405
 * Note that the notion of "freeness" for a tuple is different than for a
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1406
 * variable: if variables in the tuple also occur in any other place than
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1407
 * an occurrences of the tuple, they aren't "free" (which is thus probably
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1408
 *  the wrong word to use).
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1409
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1410
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1411
fun VSTRUCT_ELIM ctxt tych a vstr th =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1412
  let val L = USyntax.free_vars_lr vstr
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1413
      val bind1 = tych (HOLogic.mk_Trueprop (HOLogic.mk_eq(a,vstr)))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1414
      val thm1 = Thm.implies_intr bind1 (SUBS ctxt [SYM(Thm.assume bind1)] th)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1415
      val thm2 = forall_intr_list (map tych L) thm1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1416
      val thm3 = forall_elim_list (XFILL tych a vstr) thm2
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1417
  in refl RS
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1418
     rewrite_rule ctxt [Thm.symmetric (@{thm surjective_pairing} RS eq_reflection)] thm3
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1419
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1420
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1421
fun PGEN ctxt tych a vstr th =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1422
  let val a1 = tych a
60781
2da59cdf531c updated to infer_instantiate;
wenzelm
parents: 60774
diff changeset
  1423
  in Thm.forall_intr a1 (VSTRUCT_ELIM ctxt tych a vstr th) end;
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1424
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1425
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1426
(*---------------------------------------------------------------------------
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1427
 * Takes apart a paired beta-redex, looking like "(\(x,y).N) vstr", into
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1428
 *
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1429
 *     (([x,y],N),vstr)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1430
 *---------------------------------------------------------------------------*)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1431
fun dest_pbeta_redex used M n =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1432
  let val (f,args) = dest_combn M n
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
  1433
      val _ = dest_aabs used f
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1434
  in (strip_aabs used f,args)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1435
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1436
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1437
fun pbeta_redex M n = can (fn t => dest_pbeta_redex [] t n) M;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1438
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1439
fun dest_impl tm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1440
  let val ants = Logic.strip_imp_prems tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1441
      val eq = Logic.strip_imp_concl tm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1442
  in (ants,get_lhs eq)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1443
  end;
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1444
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1445
fun restricted t = is_some (USyntax.find_term
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1446
                            (fn (Const(@{const_name Wfrec.cut},_)) =>true | _ => false)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1447
                            t)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1448
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1449
fun CONTEXT_REWRITE_RULE main_ctxt (func, G, cut_lemma, congs) th =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1450
 let val globals = func::G
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1451
     val ctxt0 = empty_simpset main_ctxt
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1452
     val pbeta_reduce = simpl_conv ctxt0 [@{thm split_conv} RS eq_reflection];
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1453
     val tc_list = Unsynchronized.ref []: term list Unsynchronized.ref
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1454
     val cut_lemma' = cut_lemma RS eq_reflection
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1455
     fun prover used ctxt thm =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1456
     let fun cong_prover ctxt thm =
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
  1457
         let val _ = say "cong_prover:"
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1458
             val cntxt = Simplifier.prems_of ctxt
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
  1459
             val _ = print_thms ctxt "cntxt:" cntxt
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
  1460
             val _ = say "cong rule:"
61268
abe08fb15a12 moved remaining display.ML to more_thm.ML;
wenzelm
parents: 61125
diff changeset
  1461
             val _ = say (Thm.string_of_thm ctxt thm)
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1462
             (* Unquantified eliminate *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1463
             fun uq_eliminate (thm,imp) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1464
                 let val tych = Thm.cterm_of ctxt
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1465
                     val _ = print_term ctxt "To eliminate:" imp
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1466
                     val ants = map tych (Logic.strip_imp_prems imp)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1467
                     val eq = Logic.strip_imp_concl imp
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1468
                     val lhs = tych(get_lhs eq)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1469
                     val ctxt' = Simplifier.add_prems (map ASSUME ants) ctxt
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1470
                     val lhs_eq_lhs1 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used) ctxt' lhs
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1471
                       handle Utils.ERR _ => Thm.reflexive lhs
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1472
                     val _ = print_thms ctxt' "proven:" [lhs_eq_lhs1]
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1473
                     val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1474
                     val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1475
                  in
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1476
                  lhs_eeq_lhs2 COMP thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1477
                  end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1478
             fun pq_eliminate (thm, vlist, imp_body, lhs_eq) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1479
              let val ((vstrl, _, used'), args) = dest_pbeta_redex used lhs_eq (length vlist)
60521
52e956416fbf removed dead code;
wenzelm
parents: 60520
diff changeset
  1480
                  val _ = forall (op aconv) (ListPair.zip (vlist, args))
60520
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1481
                    orelse error "assertion failed in CONTEXT_REWRITE_RULE"
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1482
                  val imp_body1 = subst_free (ListPair.zip (args, vstrl))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1483
                                             imp_body
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1484
                  val tych = Thm.cterm_of ctxt
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1485
                  val ants1 = map tych (Logic.strip_imp_prems imp_body1)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1486
                  val eq1 = Logic.strip_imp_concl imp_body1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1487
                  val Q = get_lhs eq1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1488
                  val QeqQ1 = pbeta_reduce (tych Q)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1489
                  val Q1 = #2(Dcterm.dest_eq(cconcl QeqQ1))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1490
                  val ctxt' = Simplifier.add_prems (map ASSUME ants1) ctxt
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1491
                  val Q1eeqQ2 = Raw_Simplifier.rewrite_cterm (false,true,false) (prover used') ctxt' Q1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1492
                                handle Utils.ERR _ => Thm.reflexive Q1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1493
                  val Q2 = #2 (Logic.dest_equals (Thm.prop_of Q1eeqQ2))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1494
                  val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1495
                  val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1496
                  val thA = Thm.transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1497
                  val QeeqQ3 = Thm.transitive thA Q2eeqQ3 handle THM _ =>
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1498
                               ((Q2eeqQ3 RS meta_eq_to_obj_eq)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1499
                                RS ((thA RS meta_eq_to_obj_eq) RS trans))
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1500
                                RS eq_reflection
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1501
                  val impth = implies_intr_list ants1 QeeqQ3
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1502
                  val impth1 = impth RS meta_eq_to_obj_eq
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1503
                  (* Need to abstract *)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1504
                  val ant_th = Utils.itlist2 (PGEN ctxt' tych) args vstrl impth1
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1505
              in ant_th COMP thm
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1506
              end
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1507
             fun q_eliminate (thm, imp) =
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1508
              let val (vlist, imp_body, used') = strip_all used imp
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1509
                  val (ants,Q) = dest_impl imp_body
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1510
              in if (pbeta_redex Q) (length vlist)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1511
                 then pq_eliminate (thm, vlist, imp_body, Q)
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1512
                 else
09fc5eaa21ce moved sources;
wenzelm
parents:
diff changeset
  1513
                 let val tych = Thm.cterm_of ctxt