src/ZF/WF.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 22710 f44439cdce77
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
added Tools/lin_arith.ML;
paulson@13165
     1
(*  Title:      ZF/WF.thy
clasohm@0
     2
    ID:         $Id$
clasohm@1478
     3
    Author:     Tobias Nipkow and Lawrence C Paulson
lcp@435
     4
    Copyright   1994  University of Cambridge
clasohm@0
     5
paulson@13165
     6
Derived first for transitive relations, and finally for arbitrary WF relations
paulson@13165
     7
via wf_trancl and trans_trancl.
paulson@13165
     8
paulson@13165
     9
It is difficult to derive this general case directly, using r^+ instead of
paulson@13165
    10
r.  In is_recfun, the two occurrences of the relation must have the same
paulson@13165
    11
form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
paulson@13165
    12
r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
paulson@13165
    13
principle, but harder to use, especially to prove wfrec_eclose_eq in
paulson@13165
    14
epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
paulson@13165
    15
a mess.
clasohm@0
    16
*)
clasohm@0
    17
paulson@13356
    18
header{*Well-Founded Recursion*}
paulson@13356
    19
haftmann@16417
    20
theory WF imports Trancl begin
paulson@13165
    21
paulson@13165
    22
constdefs
paulson@13165
    23
  wf           :: "i=>o"
paulson@13165
    24
    (*r is a well-founded relation*)
paulson@13165
    25
    "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. <y,x>:r --> ~ y:Z)"
paulson@13165
    26
paulson@13165
    27
  wf_on        :: "[i,i]=>o"                      ("wf[_]'(_')")
paulson@13165
    28
    (*r is well-founded on A*)
paulson@13165
    29
    "wf_on(A,r) == wf(r Int A*A)"
paulson@13165
    30
paulson@13165
    31
  is_recfun    :: "[i, i, [i,i]=>i, i] =>o"
paulson@13165
    32
    "is_recfun(r,a,H,f) == (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))"
paulson@13165
    33
paulson@13165
    34
  the_recfun   :: "[i, i, [i,i]=>i] =>i"
paulson@13165
    35
    "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))"
paulson@13165
    36
paulson@13165
    37
  wftrec :: "[i, i, [i,i]=>i] =>i"
paulson@13165
    38
    "wftrec(r,a,H) == H(a, the_recfun(r,a,H))"
paulson@13165
    39
paulson@13165
    40
  wfrec :: "[i, i, [i,i]=>i] =>i"
paulson@13165
    41
    (*public version.  Does not require r to be transitive*)
paulson@13165
    42
    "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))"
paulson@13165
    43
paulson@13165
    44
  wfrec_on     :: "[i, i, i, [i,i]=>i] =>i"       ("wfrec[_]'(_,_,_')")
paulson@13165
    45
    "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)"
paulson@13165
    46
paulson@13165
    47
paulson@13356
    48
subsection{*Well-Founded Relations*}
paulson@13165
    49
paulson@13634
    50
subsubsection{*Equivalences between @{term wf} and @{term wf_on}*}
paulson@13165
    51
paulson@13165
    52
lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)"
paulson@13780
    53
by (unfold wf_def wf_on_def, force) 
paulson@13165
    54
paulson@13248
    55
lemma wf_on_imp_wf: "[|wf[A](r); r <= A*A|] ==> wf(r)";
paulson@13248
    56
by (simp add: wf_on_def subset_Int_iff)
paulson@13248
    57
paulson@13165
    58
lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)"
paulson@13165
    59
by (unfold wf_def wf_on_def, fast)
paulson@13165
    60
paulson@13165
    61
lemma wf_iff_wf_on_field: "wf(r) <-> wf[field(r)](r)"
paulson@13165
    62
by (blast intro: wf_imp_wf_on wf_on_field_imp_wf)
paulson@13165
    63
paulson@13165
    64
lemma wf_on_subset_A: "[| wf[A](r);  B<=A |] ==> wf[B](r)"
paulson@13165
    65
by (unfold wf_on_def wf_def, fast)
paulson@13165
    66
paulson@13165
    67
lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)"
paulson@13165
    68
by (unfold wf_on_def wf_def, fast)
paulson@13165
    69
paulson@13217
    70
lemma wf_subset: "[|wf(s); r<=s|] ==> wf(r)"
paulson@13217
    71
by (simp add: wf_def, fast)
paulson@13217
    72
paulson@13634
    73
subsubsection{*Introduction Rules for @{term wf_on}*}
paulson@13165
    74
paulson@13634
    75
text{*If every non-empty subset of @{term A} has an @{term r}-minimal element
paulson@13634
    76
   then we have @{term "wf[A](r)"}.*}
paulson@13165
    77
lemma wf_onI:
paulson@13165
    78
 assumes prem: "!!Z u. [| Z<=A;  u:Z;  ALL x:Z. EX y:Z. <y,x>:r |] ==> False"
paulson@13165
    79
 shows         "wf[A](r)"
paulson@13165
    80
apply (unfold wf_on_def wf_def)
paulson@13165
    81
apply (rule equals0I [THEN disjCI, THEN allI])
paulson@13784
    82
apply (rule_tac Z = Z in prem, blast+)
paulson@13165
    83
done
paulson@13165
    84
paulson@13634
    85
text{*If @{term r} allows well-founded induction over @{term A}
paulson@13634
    86
   then we have @{term "wf[A](r)"}.   Premise is equivalent to
wenzelm@22710
    87
  @{prop "!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B"} *}
paulson@13165
    88
lemma wf_onI2:
paulson@13165
    89
 assumes prem: "!!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;   y:A |]
paulson@13165
    90
                       ==> y:B"
paulson@13165
    91
 shows         "wf[A](r)"
paulson@13165
    92
apply (rule wf_onI)
paulson@13165
    93
apply (rule_tac c=u in prem [THEN DiffE])
paulson@13165
    94
  prefer 3 apply blast 
paulson@13165
    95
 apply fast+
paulson@13165
    96
done
paulson@13165
    97
paulson@13165
    98
paulson@13634
    99
subsubsection{*Well-founded Induction*}
paulson@13165
   100
paulson@13634
   101
text{*Consider the least @{term z} in @{term "domain(r)"} such that
paulson@13634
   102
  @{term "P(z)"} does not hold...*}
wenzelm@13534
   103
lemma wf_induct [induct set: wf]:
paulson@13165
   104
    "[| wf(r);
paulson@13634
   105
        !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) |]  
paulson@13634
   106
     ==> P(a)"
paulson@13165
   107
apply (unfold wf_def) 
paulson@13252
   108
apply (erule_tac x = "{z : domain(r). ~ P(z)}" in allE)
paulson@13165
   109
apply blast 
paulson@13165
   110
done
lcp@435
   111
wenzelm@13534
   112
lemmas wf_induct_rule = wf_induct [rule_format, induct set: wf]
paulson@13203
   113
paulson@13634
   114
text{*The form of this rule is designed to match @{text wfI}*}
paulson@13165
   115
lemma wf_induct2:
paulson@13165
   116
    "[| wf(r);  a:A;  field(r)<=A;
paulson@13165
   117
        !!x.[| x: A;  ALL y. <y,x>: r --> P(y) |] ==> P(x) |]
paulson@13165
   118
     ==>  P(a)"
paulson@13165
   119
apply (erule_tac P="a:A" in rev_mp)
paulson@13165
   120
apply (erule_tac a=a in wf_induct, blast) 
paulson@13165
   121
done
paulson@13165
   122
paulson@13165
   123
lemma field_Int_square: "field(r Int A*A) <= A"
paulson@13165
   124
by blast
paulson@13165
   125
wenzelm@13534
   126
lemma wf_on_induct [consumes 2, induct set: wf_on]:
paulson@13165
   127
    "[| wf[A](r);  a:A;
paulson@13165
   128
        !!x.[| x: A;  ALL y:A. <y,x>: r --> P(y) |] ==> P(x)
paulson@13165
   129
     |]  ==>  P(a)"
paulson@13165
   130
apply (unfold wf_on_def) 
paulson@13165
   131
apply (erule wf_induct2, assumption)
paulson@13165
   132
apply (rule field_Int_square, blast)
paulson@13165
   133
done
paulson@13165
   134
wenzelm@13534
   135
lemmas wf_on_induct_rule =
wenzelm@13534
   136
  wf_on_induct [rule_format, consumes 2, induct set: wf_on]
paulson@13203
   137
paulson@13203
   138
paulson@13634
   139
text{*If @{term r} allows well-founded induction 
paulson@13634
   140
   then we have @{term "wf(r)"}.*}
paulson@13165
   141
lemma wfI:
paulson@13165
   142
    "[| field(r)<=A;
paulson@13165
   143
        !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B;  y:A|]
paulson@13165
   144
               ==> y:B |]
paulson@13165
   145
     ==>  wf(r)"
paulson@13165
   146
apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf])
paulson@13165
   147
apply (rule wf_onI2)
paulson@13165
   148
 prefer 2 apply blast  
paulson@13165
   149
apply blast 
paulson@13165
   150
done
paulson@13165
   151
paulson@13165
   152
paulson@13356
   153
subsection{*Basic Properties of Well-Founded Relations*}
paulson@13165
   154
paulson@13165
   155
lemma wf_not_refl: "wf(r) ==> <a,a> ~: r"
paulson@13165
   156
by (erule_tac a=a in wf_induct, blast)
paulson@13165
   157
paulson@13165
   158
lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. <a,x>:r --> <x,a> ~: r"
paulson@13165
   159
by (erule_tac a=a in wf_induct, blast)
paulson@13165
   160
paulson@13165
   161
(* [| wf(r);  <a,x> : r;  ~P ==> <x,a> : r |] ==> P *)
paulson@13165
   162
lemmas wf_asym = wf_not_sym [THEN swap, standard]
paulson@13165
   163
paulson@13165
   164
lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> <a,a> ~: r"
paulson@13269
   165
by (erule_tac a=a in wf_on_induct, assumption, blast)
clasohm@0
   166
paulson@13165
   167
lemma wf_on_not_sym [rule_format]:
paulson@13165
   168
     "[| wf[A](r);  a:A |] ==> ALL b:A. <a,b>:r --> <b,a>~:r"
paulson@13269
   169
apply (erule_tac a=a in wf_on_induct, assumption, blast)
paulson@13165
   170
done
paulson@13165
   171
paulson@13165
   172
lemma wf_on_asym:
paulson@13165
   173
     "[| wf[A](r);  ~Z ==> <a,b> : r;
paulson@13165
   174
         <b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z"
paulson@13269
   175
by (blast dest: wf_on_not_sym) 
paulson@13165
   176
paulson@13165
   177
paulson@13165
   178
(*Needed to prove well_ordI.  Could also reason that wf[A](r) means
paulson@13165
   179
  wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)
paulson@13165
   180
lemma wf_on_chain3:
paulson@13165
   181
     "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P"
paulson@13165
   182
apply (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P",
paulson@13165
   183
       blast) 
paulson@13269
   184
apply (erule_tac a=a in wf_on_induct, assumption, blast)
paulson@13165
   185
done
paulson@13165
   186
paulson@13165
   187
paulson@13165
   188
paulson@13634
   189
text{*transitive closure of a WF relation is WF provided 
paulson@13634
   190
  @{term A} is downward closed*}
paulson@13165
   191
lemma wf_on_trancl:
paulson@13165
   192
    "[| wf[A](r);  r-``A <= A |] ==> wf[A](r^+)"
paulson@13165
   193
apply (rule wf_onI2)
paulson@13165
   194
apply (frule bspec [THEN mp], assumption+)
paulson@13784
   195
apply (erule_tac a = y in wf_on_induct, assumption)
paulson@13165
   196
apply (blast elim: tranclE, blast) 
paulson@13165
   197
done
paulson@13165
   198
paulson@13165
   199
lemma wf_trancl: "wf(r) ==> wf(r^+)"
paulson@13165
   200
apply (simp add: wf_iff_wf_on_field)
paulson@13165
   201
apply (rule wf_on_subset_A) 
paulson@13165
   202
 apply (erule wf_on_trancl)
paulson@13165
   203
 apply blast 
paulson@13165
   204
apply (rule trancl_type [THEN field_rel_subset])
paulson@13165
   205
done
paulson@13165
   206
paulson@13165
   207
paulson@13634
   208
text{*@{term "r-``{a}"} is the set of everything under @{term a} in @{term r}*}
paulson@13165
   209
paulson@13165
   210
lemmas underI = vimage_singleton_iff [THEN iffD2, standard]
paulson@13165
   211
lemmas underD = vimage_singleton_iff [THEN iffD1, standard]
paulson@13165
   212
paulson@13634
   213
paulson@13634
   214
subsection{*The Predicate @{term is_recfun}*}
clasohm@0
   215
paulson@13165
   216
lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)"
paulson@13165
   217
apply (unfold is_recfun_def)
paulson@13165
   218
apply (erule ssubst)
paulson@13165
   219
apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
paulson@13165
   220
done
paulson@13165
   221
paulson@13269
   222
lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function]
paulson@13269
   223
paulson@13165
   224
lemma apply_recfun:
paulson@13165
   225
    "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"
paulson@13165
   226
apply (unfold is_recfun_def) 
paulson@13175
   227
  txt{*replace f only on the left-hand side*}
paulson@13175
   228
apply (erule_tac P = "%x.?t(x) = ?u" in ssubst)
paulson@13269
   229
apply (simp add: underI) 
paulson@13165
   230
done
paulson@13165
   231
paulson@13165
   232
lemma is_recfun_equal [rule_format]:
paulson@13165
   233
     "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |]
paulson@13165
   234
      ==> <x,a>:r --> <x,b>:r --> f`x=g`x"
paulson@13784
   235
apply (frule_tac f = f in is_recfun_type)
paulson@13784
   236
apply (frule_tac f = g in is_recfun_type)
paulson@13165
   237
apply (simp add: is_recfun_def)
paulson@13165
   238
apply (erule_tac a=x in wf_induct)
paulson@13165
   239
apply (intro impI)
paulson@13165
   240
apply (elim ssubst)
paulson@13165
   241
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
paulson@13165
   242
apply (rule_tac t = "%z. H (?x,z) " in subst_context)
paulson@13165
   243
apply (subgoal_tac "ALL y : r-``{x}. ALL z. <y,z>:f <-> <y,z>:g")
paulson@13165
   244
 apply (blast dest: transD)
paulson@13165
   245
apply (simp add: apply_iff)
paulson@13165
   246
apply (blast dest: transD intro: sym)
paulson@13165
   247
done
paulson@13165
   248
paulson@13165
   249
lemma is_recfun_cut:
paulson@13165
   250
     "[| wf(r);  trans(r);
paulson@13165
   251
         is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  <b,a>:r |]
paulson@13165
   252
      ==> restrict(f, r-``{b}) = g"
paulson@13784
   253
apply (frule_tac f = f in is_recfun_type)
paulson@13165
   254
apply (rule fun_extension)
paulson@13165
   255
  apply (blast dest: transD intro: restrict_type2)
paulson@13165
   256
 apply (erule is_recfun_type, simp)
paulson@13165
   257
apply (blast dest: transD intro: is_recfun_equal)
paulson@13165
   258
done
paulson@13165
   259
paulson@13356
   260
subsection{*Recursion: Main Existence Lemma*}
lcp@435
   261
paulson@13165
   262
lemma is_recfun_functional:
paulson@13165
   263
     "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |]  ==>  f=g"
paulson@13165
   264
by (blast intro: fun_extension is_recfun_type is_recfun_equal)
paulson@13165
   265
paulson@13248
   266
lemma the_recfun_eq:
paulson@13248
   267
    "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |] ==> the_recfun(r,a,H) = f"
paulson@13248
   268
apply (unfold the_recfun_def)
paulson@13248
   269
apply (blast intro: is_recfun_functional)
paulson@13248
   270
done
paulson@13248
   271
paulson@13165
   272
(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
paulson@13165
   273
lemma is_the_recfun:
paulson@13165
   274
    "[| is_recfun(r,a,H,f);  wf(r);  trans(r) |]
paulson@13165
   275
     ==> is_recfun(r, a, H, the_recfun(r,a,H))"
paulson@13248
   276
by (simp add: the_recfun_eq)
paulson@13165
   277
paulson@13165
   278
lemma unfold_the_recfun:
paulson@13165
   279
     "[| wf(r);  trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"
paulson@13165
   280
apply (rule_tac a=a in wf_induct, assumption)
paulson@13165
   281
apply (rename_tac a1) 
paulson@13165
   282
apply (rule_tac f = "lam y: r-``{a1}. wftrec (r,y,H)" in is_the_recfun)
paulson@13165
   283
  apply typecheck
paulson@13165
   284
apply (unfold is_recfun_def wftrec_def)
paulson@13634
   285
  --{*Applying the substitution: must keep the quantified assumption!*}
paulson@13165
   286
apply (rule lam_cong [OF refl]) 
paulson@13165
   287
apply (drule underD) 
paulson@13165
   288
apply (fold is_recfun_def)
paulson@13165
   289
apply (rule_tac t = "%z. H(?x,z)" in subst_context)
paulson@13165
   290
apply (rule fun_extension)
paulson@13165
   291
  apply (blast intro: is_recfun_type)
paulson@13165
   292
 apply (rule lam_type [THEN restrict_type2])
paulson@13165
   293
  apply blast
paulson@13165
   294
 apply (blast dest: transD)
paulson@13165
   295
apply (frule spec [THEN mp], assumption)
paulson@13165
   296
apply (subgoal_tac "<xa,a1> : r")
paulson@13784
   297
 apply (drule_tac x1 = xa in spec [THEN mp], assumption)
paulson@13175
   298
apply (simp add: vimage_singleton_iff 
paulson@13165
   299
                 apply_recfun is_recfun_cut)
paulson@13165
   300
apply (blast dest: transD)
paulson@13165
   301
done
paulson@13165
   302
paulson@13165
   303
paulson@13356
   304
subsection{*Unfolding @{term "wftrec(r,a,H)"}*}
paulson@13165
   305
paulson@13165
   306
lemma the_recfun_cut:
paulson@13165
   307
     "[| wf(r);  trans(r);  <b,a>:r |]
paulson@13165
   308
      ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
paulson@13269
   309
by (blast intro: is_recfun_cut unfold_the_recfun)
clasohm@0
   310
paulson@13165
   311
(*NOT SUITABLE FOR REWRITING: it is recursive!*)
paulson@13165
   312
lemma wftrec:
paulson@13165
   313
    "[| wf(r);  trans(r) |] ==>
paulson@13165
   314
          wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))"
paulson@13165
   315
apply (unfold wftrec_def)
paulson@13165
   316
apply (subst unfold_the_recfun [unfolded is_recfun_def])
paulson@13165
   317
apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
paulson@13165
   318
done
paulson@13165
   319
paulson@13634
   320
paulson@13634
   321
subsubsection{*Removal of the Premise @{term "trans(r)"}*}
paulson@13165
   322
paulson@13165
   323
(*NOT SUITABLE FOR REWRITING: it is recursive!*)
paulson@13165
   324
lemma wfrec:
paulson@13165
   325
    "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))"
paulson@13165
   326
apply (unfold wfrec_def) 
paulson@13165
   327
apply (erule wf_trancl [THEN wftrec, THEN ssubst])
paulson@13165
   328
 apply (rule trans_trancl)
paulson@13165
   329
apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context])
paulson@13165
   330
 apply (erule r_into_trancl)
paulson@13165
   331
apply (rule subset_refl)
paulson@13165
   332
done
clasohm@0
   333
paulson@13165
   334
(*This form avoids giant explosions in proofs.  NOTE USE OF == *)
paulson@13165
   335
lemma def_wfrec:
paulson@13165
   336
    "[| !!x. h(x)==wfrec(r,x,H);  wf(r) |] ==>
paulson@13165
   337
     h(a) = H(a, lam x: r-``{a}. h(x))"
paulson@13165
   338
apply simp
paulson@13165
   339
apply (elim wfrec) 
paulson@13165
   340
done
paulson@13165
   341
paulson@13165
   342
lemma wfrec_type:
paulson@13165
   343
    "[| wf(r);  a:A;  field(r)<=A;
paulson@13165
   344
        !!x u. [| x: A;  u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x)
paulson@13165
   345
     |] ==> wfrec(r,a,H) : B(a)"
paulson@13784
   346
apply (rule_tac a = a in wf_induct2, assumption+)
paulson@13165
   347
apply (subst wfrec, assumption)
paulson@13165
   348
apply (simp add: lam_type underD)  
paulson@13165
   349
done
paulson@13165
   350
paulson@13165
   351
paulson@13165
   352
lemma wfrec_on:
paulson@13165
   353
 "[| wf[A](r);  a: A |] ==>
paulson@13165
   354
         wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))"
paulson@13165
   355
apply (unfold wf_on_def wfrec_on_def)
paulson@13165
   356
apply (erule wfrec [THEN trans])
paulson@13165
   357
apply (simp add: vimage_Int_square cons_subset_iff)
paulson@13165
   358
done
clasohm@0
   359
paulson@13634
   360
text{*Minimal-element characterization of well-foundedness*}
paulson@13165
   361
lemma wf_eq_minimal:
paulson@13165
   362
     "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q))"
paulson@13634
   363
by (unfold wf_def, blast)
paulson@13634
   364
paulson@13165
   365
paulson@13165
   366
ML
paulson@13165
   367
{*
paulson@13165
   368
val wf_def = thm "wf_def";
paulson@13165
   369
val wf_on_def = thm "wf_on_def";
clasohm@0
   370
paulson@13165
   371
val wf_imp_wf_on = thm "wf_imp_wf_on";
paulson@13165
   372
val wf_on_field_imp_wf = thm "wf_on_field_imp_wf";
paulson@13165
   373
val wf_iff_wf_on_field = thm "wf_iff_wf_on_field";
paulson@13165
   374
val wf_on_subset_A = thm "wf_on_subset_A";
paulson@13165
   375
val wf_on_subset_r = thm "wf_on_subset_r";
paulson@13165
   376
val wf_onI = thm "wf_onI";
paulson@13165
   377
val wf_onI2 = thm "wf_onI2";
paulson@13165
   378
val wf_induct = thm "wf_induct";
paulson@13165
   379
val wf_induct2 = thm "wf_induct2";
paulson@13165
   380
val field_Int_square = thm "field_Int_square";
paulson@13165
   381
val wf_on_induct = thm "wf_on_induct";
paulson@13165
   382
val wfI = thm "wfI";
paulson@13165
   383
val wf_not_refl = thm "wf_not_refl";
paulson@13165
   384
val wf_not_sym = thm "wf_not_sym";
paulson@13165
   385
val wf_asym = thm "wf_asym";
paulson@13165
   386
val wf_on_not_refl = thm "wf_on_not_refl";
paulson@13165
   387
val wf_on_not_sym = thm "wf_on_not_sym";
paulson@13165
   388
val wf_on_asym = thm "wf_on_asym";
paulson@13165
   389
val wf_on_chain3 = thm "wf_on_chain3";
paulson@13165
   390
val wf_on_trancl = thm "wf_on_trancl";
paulson@13165
   391
val wf_trancl = thm "wf_trancl";
paulson@13165
   392
val underI = thm "underI";
paulson@13165
   393
val underD = thm "underD";
paulson@13165
   394
val is_recfun_type = thm "is_recfun_type";
paulson@13165
   395
val apply_recfun = thm "apply_recfun";
paulson@13165
   396
val is_recfun_equal = thm "is_recfun_equal";
paulson@13165
   397
val is_recfun_cut = thm "is_recfun_cut";
paulson@13165
   398
val is_recfun_functional = thm "is_recfun_functional";
paulson@13165
   399
val is_the_recfun = thm "is_the_recfun";
paulson@13165
   400
val unfold_the_recfun = thm "unfold_the_recfun";
paulson@13165
   401
val the_recfun_cut = thm "the_recfun_cut";
paulson@13165
   402
val wftrec = thm "wftrec";
paulson@13165
   403
val wfrec = thm "wfrec";
paulson@13165
   404
val def_wfrec = thm "def_wfrec";
paulson@13165
   405
val wfrec_type = thm "wfrec_type";
paulson@13165
   406
val wfrec_on = thm "wfrec_on";
paulson@13165
   407
val wf_eq_minimal = thm "wf_eq_minimal";
paulson@13165
   408
*}
lcp@435
   409
clasohm@0
   410
end