src/HOL/Wellfounded_Recursion.thy
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 22390 378f34b1e380
child 22766 116c1d6b4026
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
paulson@15341
     1
(*  ID:         $Id$
nipkow@10213
     2
    Author:     Tobias Nipkow
nipkow@10213
     3
    Copyright   1992  University of Cambridge
nipkow@10213
     4
*)
nipkow@10213
     5
paulson@15341
     6
header {*Well-founded Recursion*}
paulson@15341
     7
paulson@15341
     8
theory Wellfounded_Recursion
paulson@15341
     9
imports Transitive_Closure
paulson@15341
    10
begin
nipkow@10213
    11
berghofe@22263
    12
inductive2
berghofe@22263
    13
  wfrec_rel :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b => bool"
berghofe@22263
    14
  for R :: "('a * 'a) set"
berghofe@22263
    15
  and F :: "('a => 'b) => 'a => 'b"
berghofe@22263
    16
where
berghofe@22263
    17
  wfrecI: "ALL z. (z, x) : R --> wfrec_rel R F z (g z) ==>
berghofe@22263
    18
            wfrec_rel R F x (F g x)"
berghofe@11328
    19
nipkow@10213
    20
constdefs
nipkow@10213
    21
  wf         :: "('a * 'a)set => bool"
nipkow@10213
    22
  "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
nipkow@10213
    23
berghofe@22263
    24
  wfP :: "('a => 'a => bool) => bool"
berghofe@22263
    25
  "wfP r == wf (Collect2 r)"
berghofe@22263
    26
nipkow@10213
    27
  acyclic :: "('a*'a)set => bool"
nipkow@10213
    28
  "acyclic r == !x. (x,x) ~: r^+"
nipkow@10213
    29
nipkow@10213
    30
  cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
nipkow@10213
    31
  "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
nipkow@10213
    32
berghofe@11328
    33
  adm_wf :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => bool"
berghofe@11328
    34
  "adm_wf R F == ALL f g x.
berghofe@11328
    35
     (ALL z. (z, x) : R --> f z = g z) --> F f x = F g x"
nipkow@10213
    36
berghofe@11328
    37
  wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b"
berghofe@22263
    38
  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
berghofe@22263
    39
berghofe@22263
    40
abbreviation acyclicP :: "('a => 'a => bool) => bool" where
berghofe@22263
    41
  "acyclicP r == acyclic (Collect2 r)"
nipkow@10213
    42
haftmann@22390
    43
class wellorder = linorder +
haftmann@22390
    44
  assumes wf: "wf {(x, y). x \<sqsubset> y}"
paulson@15341
    45
paulson@15341
    46
berghofe@22263
    47
lemma wfP_wf_eq [pred_set_conv]: "wfP (member2 r) = wf r"
berghofe@22263
    48
  by (simp add: wfP_def)
berghofe@22263
    49
berghofe@22263
    50
lemma wf_implies_wfP: "wf r \<Longrightarrow> wfP (member2 r)"
berghofe@22263
    51
  by (simp add: wfP_def)
berghofe@22263
    52
berghofe@22263
    53
lemma wfP_implies_wf: "wfP r \<Longrightarrow> wf (Collect2 r)"
berghofe@22263
    54
  by (simp add: wfP_def)
berghofe@22263
    55
paulson@15341
    56
lemma wfUNIVI: 
paulson@15341
    57
   "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"
paulson@15341
    58
by (unfold wf_def, blast)
paulson@15341
    59
berghofe@22263
    60
lemmas wfPUNIVI = wfUNIVI [to_pred]
berghofe@22263
    61
paulson@19766
    62
text{*Restriction to domain @{term A} and range @{term B}.  If @{term r} is
paulson@19766
    63
    well-founded over their intersection, then @{term "wf r"}*}
paulson@15341
    64
lemma wfI: 
paulson@19766
    65
 "[| r \<subseteq> A <*> B; 
paulson@19766
    66
     !!x P. [|\<forall>x. (\<forall>y. (y,x) : r --> P y) --> P x;  x : A; x : B |] ==> P x |]
paulson@15341
    67
  ==>  wf r"
paulson@15341
    68
by (unfold wf_def, blast)
paulson@15341
    69
paulson@15341
    70
lemma wf_induct: 
paulson@15341
    71
    "[| wf(r);           
paulson@15341
    72
        !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x)  
paulson@15341
    73
     |]  ==>  P(a)"
paulson@15341
    74
by (unfold wf_def, blast)
paulson@15341
    75
berghofe@22263
    76
lemmas wfP_induct = wf_induct [to_pred]
berghofe@22263
    77
wenzelm@18458
    78
lemmas wf_induct_rule = wf_induct [rule_format, consumes 1, case_names less, induct set: wf]
nipkow@17042
    79
berghofe@22263
    80
lemmas wfP_induct_rule =
berghofe@22263
    81
  wf_induct_rule [to_pred, consumes 1, case_names less, induct set: wfP]
berghofe@22263
    82
paulson@15341
    83
lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r"
paulson@15341
    84
by (erule_tac a=a in wf_induct, blast)
paulson@15341
    85
paulson@15341
    86
(* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)
paulson@15341
    87
lemmas wf_asym = wf_not_sym [elim_format]
paulson@15341
    88
paulson@15341
    89
lemma wf_not_refl [simp]: "wf(r) ==> (a,a) ~: r"
paulson@15341
    90
by (blast elim: wf_asym)
paulson@15341
    91
paulson@15341
    92
(* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
paulson@15341
    93
lemmas wf_irrefl = wf_not_refl [elim_format]
paulson@15341
    94
paulson@15341
    95
text{*transitive closure of a well-founded relation is well-founded! *}
paulson@15341
    96
lemma wf_trancl: "wf(r) ==> wf(r^+)"
paulson@15341
    97
apply (subst wf_def, clarify)
paulson@15341
    98
apply (rule allE, assumption)
paulson@15341
    99
  --{*Retains the universal formula for later use!*}
paulson@15341
   100
apply (erule mp)
paulson@15341
   101
apply (erule_tac a = x in wf_induct)
paulson@15341
   102
apply (blast elim: tranclE)
paulson@15341
   103
done
paulson@15341
   104
berghofe@22263
   105
lemmas wfP_trancl = wf_trancl [to_pred]
berghofe@22263
   106
paulson@15341
   107
lemma wf_converse_trancl: "wf (r^-1) ==> wf ((r^+)^-1)"
paulson@15341
   108
apply (subst trancl_converse [symmetric])
paulson@15341
   109
apply (erule wf_trancl)
paulson@15341
   110
done
paulson@15341
   111
paulson@15341
   112
paulson@15341
   113
subsubsection{*Other simple well-foundedness results*}
paulson@15341
   114
paulson@15341
   115
paulson@19870
   116
text{*Minimal-element characterization of well-foundedness*}
paulson@19870
   117
lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
paulson@19870
   118
proof (intro iffI strip)
paulson@19870
   119
  fix Q::"'a set" and x
paulson@19870
   120
  assume "wf r" and "x \<in> Q"
paulson@19870
   121
  thus "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
paulson@19870
   122
    by (unfold wf_def, 
paulson@19870
   123
        blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"]) 
paulson@19870
   124
next
paulson@19870
   125
  assume "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
paulson@19870
   126
  thus "wf r" by (unfold wf_def, force)
paulson@19870
   127
qed
paulson@19870
   128
berghofe@22263
   129
lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
berghofe@22263
   130
paulson@15341
   131
text{*Well-foundedness of subsets*}
paulson@15341
   132
lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
paulson@15341
   133
apply (simp (no_asm_use) add: wf_eq_minimal)
paulson@15341
   134
apply fast
paulson@15341
   135
done
paulson@15341
   136
berghofe@22263
   137
lemmas wfP_subset = wf_subset [to_pred]
berghofe@22263
   138
paulson@15341
   139
text{*Well-foundedness of the empty relation*}
paulson@15341
   140
lemma wf_empty [iff]: "wf({})"
paulson@15341
   141
by (simp add: wf_def)
paulson@15341
   142
berghofe@22263
   143
lemmas wfP_empty [iff] = wf_empty [to_pred]
berghofe@22263
   144
paulson@19870
   145
lemma wf_Int1: "wf r ==> wf (r Int r')"
paulson@19870
   146
by (erule wf_subset, rule Int_lower1)
paulson@19870
   147
paulson@19870
   148
lemma wf_Int2: "wf r ==> wf (r' Int r)"
paulson@19870
   149
by (erule wf_subset, rule Int_lower2)
paulson@19870
   150
paulson@15341
   151
text{*Well-foundedness of insert*}
paulson@15341
   152
lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
paulson@15341
   153
apply (rule iffI)
paulson@15341
   154
 apply (blast elim: wf_trancl [THEN wf_irrefl]
paulson@15341
   155
              intro: rtrancl_into_trancl1 wf_subset 
paulson@15341
   156
                     rtrancl_mono [THEN [2] rev_subsetD])
paulson@15341
   157
apply (simp add: wf_eq_minimal, safe)
paulson@15341
   158
apply (rule allE, assumption, erule impE, blast) 
paulson@15341
   159
apply (erule bexE)
paulson@15341
   160
apply (rename_tac "a", case_tac "a = x")
paulson@15341
   161
 prefer 2
paulson@15341
   162
apply blast 
paulson@15341
   163
apply (case_tac "y:Q")
paulson@15341
   164
 prefer 2 apply blast
paulson@15341
   165
apply (rule_tac x = "{z. z:Q & (z,y) : r^*}" in allE)
paulson@15341
   166
 apply assumption
paulson@15341
   167
apply (erule_tac V = "ALL Q. (EX x. x : Q) --> ?P Q" in thin_rl) 
paulson@15341
   168
  --{*essential for speed*}
kleing@15343
   169
txt{*Blast with new substOccur fails*}
paulson@15341
   170
apply (fast intro: converse_rtrancl_into_rtrancl)
paulson@15341
   171
done
paulson@15341
   172
paulson@15341
   173
text{*Well-foundedness of image*}
paulson@15341
   174
lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
paulson@15341
   175
apply (simp only: wf_eq_minimal, clarify)
paulson@15341
   176
apply (case_tac "EX p. f p : Q")
paulson@15341
   177
apply (erule_tac x = "{p. f p : Q}" in allE)
paulson@15341
   178
apply (fast dest: inj_onD, blast)
paulson@15341
   179
done
paulson@15341
   180
paulson@15341
   181
paulson@15341
   182
subsubsection{*Well-Foundedness Results for Unions*}
paulson@15341
   183
paulson@15341
   184
text{*Well-foundedness of indexed union with disjoint domains and ranges*}
paulson@15341
   185
paulson@15341
   186
lemma wf_UN: "[| ALL i:I. wf(r i);  
paulson@15341
   187
         ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {}  
paulson@15341
   188
      |] ==> wf(UN i:I. r i)"
paulson@15341
   189
apply (simp only: wf_eq_minimal, clarify)
paulson@15341
   190
apply (rename_tac A a, case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i")
paulson@15341
   191
 prefer 2
paulson@15341
   192
 apply force 
paulson@15341
   193
apply clarify
paulson@15341
   194
apply (drule bspec, assumption)  
paulson@15341
   195
apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r i) }" in allE)
paulson@15341
   196
apply (blast elim!: allE)  
paulson@15341
   197
done
paulson@15341
   198
berghofe@22263
   199
lemmas wfP_SUP = wf_UN [where I=UNIV and r="\<lambda>i. Collect2 (r i)",
berghofe@22263
   200
  to_pred member2_SUP, simplified, standard]
berghofe@22263
   201
paulson@15341
   202
lemma wf_Union: 
paulson@15341
   203
 "[| ALL r:R. wf r;  
paulson@15341
   204
     ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
paulson@15341
   205
  |] ==> wf(Union R)"
paulson@15341
   206
apply (simp add: Union_def)
paulson@15341
   207
apply (blast intro: wf_UN)
paulson@15341
   208
done
paulson@15341
   209
paulson@15341
   210
(*Intuition: we find an (R u S)-min element of a nonempty subset A
paulson@15341
   211
             by case distinction.
paulson@15341
   212
  1. There is a step a -R-> b with a,b : A.
paulson@15341
   213
     Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.
paulson@15341
   214
     By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the
paulson@15341
   215
     subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot
paulson@15341
   216
     have an S-successor and is thus S-min in A as well.
paulson@15341
   217
  2. There is no such step.
paulson@15341
   218
     Pick an S-min element of A. In this case it must be an R-min
paulson@15341
   219
     element of A as well.
paulson@15341
   220
paulson@15341
   221
*)
paulson@15341
   222
lemma wf_Un:
paulson@15341
   223
     "[| wf r; wf s; Domain r Int Range s = {} |] ==> wf(r Un s)"
paulson@15341
   224
apply (simp only: wf_eq_minimal, clarify) 
paulson@15341
   225
apply (rename_tac A a)
paulson@15341
   226
apply (case_tac "EX a:A. EX b:A. (b,a) : r") 
paulson@15341
   227
 prefer 2
paulson@15341
   228
 apply simp
paulson@15341
   229
 apply (drule_tac x=A in spec)+
paulson@15341
   230
 apply blast 
paulson@15341
   231
apply (erule_tac x="{a. a:A & (EX b:A. (b,a) : r) }" in allE)+
paulson@15341
   232
apply (blast elim!: allE)  
paulson@15341
   233
done
paulson@15341
   234
paulson@15341
   235
subsubsection {*acyclic*}
paulson@15341
   236
paulson@15341
   237
lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
paulson@15341
   238
by (simp add: acyclic_def)
paulson@15341
   239
paulson@15341
   240
lemma wf_acyclic: "wf r ==> acyclic r"
paulson@15341
   241
apply (simp add: acyclic_def)
paulson@15341
   242
apply (blast elim: wf_trancl [THEN wf_irrefl])
paulson@15341
   243
done
paulson@15341
   244
berghofe@22263
   245
lemmas wfP_acyclicP = wf_acyclic [to_pred]
berghofe@22263
   246
paulson@15341
   247
lemma acyclic_insert [iff]:
paulson@15341
   248
     "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"
paulson@15341
   249
apply (simp add: acyclic_def trancl_insert)
paulson@15341
   250
apply (blast intro: rtrancl_trans)
paulson@15341
   251
done
paulson@15341
   252
paulson@15341
   253
lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"
paulson@15341
   254
by (simp add: acyclic_def trancl_converse)
paulson@15341
   255
berghofe@22263
   256
lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]
berghofe@22263
   257
paulson@15341
   258
lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"
paulson@15341
   259
apply (simp add: acyclic_def antisym_def)
paulson@15341
   260
apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)
paulson@15341
   261
done
paulson@15341
   262
paulson@15341
   263
(* Other direction:
paulson@15341
   264
acyclic = no loops
paulson@15341
   265
antisym = only self loops
paulson@15341
   266
Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)
paulson@15341
   267
==> antisym( r^* ) = acyclic(r - Id)";
paulson@15341
   268
*)
paulson@15341
   269
paulson@15341
   270
lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"
paulson@15341
   271
apply (simp add: acyclic_def)
paulson@15341
   272
apply (blast intro: trancl_mono)
paulson@15341
   273
done
paulson@15341
   274
paulson@15341
   275
paulson@15341
   276
subsection{*Well-Founded Recursion*}
paulson@15341
   277
paulson@15341
   278
text{*cut*}
paulson@15341
   279
paulson@15341
   280
lemma cuts_eq: "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"
paulson@15341
   281
by (simp add: expand_fun_eq cut_def)
paulson@15341
   282
paulson@15341
   283
lemma cut_apply: "(x,a):r ==> (cut f r a)(x) = f(x)"
paulson@15341
   284
by (simp add: cut_def)
paulson@15341
   285
paulson@15341
   286
text{*Inductive characterization of wfrec combinator; for details see:  
paulson@15341
   287
John Harrison, "Inductive definitions: automation and application"*}
paulson@15341
   288
berghofe@22263
   289
lemma wfrec_unique: "[| adm_wf R F; wf R |] ==> EX! y. wfrec_rel R F x y"
paulson@15341
   290
apply (simp add: adm_wf_def)
paulson@15341
   291
apply (erule_tac a=x in wf_induct) 
paulson@15341
   292
apply (rule ex1I)
berghofe@22263
   293
apply (rule_tac g = "%x. THE y. wfrec_rel R F x y" in wfrec_rel.wfrecI)
paulson@15341
   294
apply (fast dest!: theI')
paulson@15341
   295
apply (erule wfrec_rel.cases, simp)
paulson@15341
   296
apply (erule allE, erule allE, erule allE, erule mp)
paulson@15341
   297
apply (fast intro: the_equality [symmetric])
paulson@15341
   298
done
paulson@15341
   299
paulson@15341
   300
lemma adm_lemma: "adm_wf R (%f x. F (cut f R x) x)"
paulson@15341
   301
apply (simp add: adm_wf_def)
paulson@15341
   302
apply (intro strip)
paulson@15341
   303
apply (rule cuts_eq [THEN iffD2, THEN subst], assumption)
paulson@15341
   304
apply (rule refl)
paulson@15341
   305
done
paulson@15341
   306
paulson@15341
   307
lemma wfrec: "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"
paulson@15341
   308
apply (simp add: wfrec_def)
paulson@15341
   309
apply (rule adm_lemma [THEN wfrec_unique, THEN the1_equality], assumption)
paulson@15341
   310
apply (rule wfrec_rel.wfrecI)
paulson@15341
   311
apply (intro strip)
paulson@15341
   312
apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
paulson@15341
   313
done
paulson@15341
   314
paulson@15341
   315
paulson@15341
   316
text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
paulson@15341
   317
lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
paulson@15341
   318
apply auto
paulson@15341
   319
apply (blast intro: wfrec)
paulson@15341
   320
done
paulson@15341
   321
paulson@15341
   322
wenzelm@17459
   323
subsection {* Code generator setup *}
wenzelm@17459
   324
wenzelm@17459
   325
consts_code
berghofe@17654
   326
  "wfrec"   ("\<module>wfrec?")
wenzelm@17459
   327
attach {*
berghofe@17654
   328
fun wfrec f x = f (wfrec f) x;
wenzelm@17459
   329
*}
wenzelm@17459
   330
wenzelm@17459
   331
paulson@15341
   332
subsection{*Variants for TFL: the Recdef Package*}
paulson@15341
   333
paulson@15341
   334
lemma tfl_wf_induct: "ALL R. wf R -->  
paulson@15341
   335
       (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"
paulson@15341
   336
apply clarify
paulson@15341
   337
apply (rule_tac r = R and P = P and a = x in wf_induct, assumption, blast)
paulson@15341
   338
done
paulson@15341
   339
paulson@15341
   340
lemma tfl_cut_apply: "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"
paulson@15341
   341
apply clarify
paulson@15341
   342
apply (rule cut_apply, assumption)
paulson@15341
   343
done
paulson@15341
   344
paulson@15341
   345
lemma tfl_wfrec:
paulson@15341
   346
     "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"
paulson@15341
   347
apply clarify
paulson@15341
   348
apply (erule wfrec)
paulson@15341
   349
done
paulson@15341
   350
paulson@15341
   351
subsection {*LEAST and wellorderings*}
paulson@15341
   352
paulson@15341
   353
text{* See also @{text wf_linord_ex_has_least} and its consequences in
paulson@15341
   354
 @{text Wellfounded_Relations.ML}*}
paulson@15341
   355
paulson@15341
   356
lemma wellorder_Least_lemma [rule_format]:
paulson@15341
   357
     "P (k::'a::wellorder) --> P (LEAST x. P(x)) & (LEAST x. P(x)) <= k"
paulson@15341
   358
apply (rule_tac a = k in wf [THEN wf_induct])
paulson@15341
   359
apply (rule impI)
paulson@15341
   360
apply (rule classical)
paulson@15341
   361
apply (rule_tac s = x in Least_equality [THEN ssubst], auto)
paulson@15341
   362
apply (auto simp add: linorder_not_less [symmetric])
paulson@15341
   363
done
paulson@15341
   364
paulson@15341
   365
lemmas LeastI   = wellorder_Least_lemma [THEN conjunct1, standard]
paulson@15341
   366
lemmas Least_le = wellorder_Least_lemma [THEN conjunct2, standard]
paulson@15341
   367
nipkow@15950
   368
-- "The following 3 lemmas are due to Brian Huffman"
nipkow@15950
   369
lemma LeastI_ex: "EX x::'a::wellorder. P x ==> P (Least P)"
nipkow@15950
   370
apply (erule exE)
nipkow@15950
   371
apply (erule LeastI)
nipkow@15950
   372
done
nipkow@15950
   373
nipkow@15950
   374
lemma LeastI2:
nipkow@15950
   375
  "[| P (a::'a::wellorder); !!x. P x ==> Q x |] ==> Q (Least P)"
nipkow@15950
   376
by (blast intro: LeastI)
nipkow@15950
   377
nipkow@15950
   378
lemma LeastI2_ex:
nipkow@15950
   379
  "[| EX a::'a::wellorder. P a; !!x. P x ==> Q x |] ==> Q (Least P)"
nipkow@15950
   380
by (blast intro: LeastI_ex)
nipkow@15950
   381
paulson@15341
   382
lemma not_less_Least: "[| k < (LEAST x. P x) |] ==> ~P (k::'a::wellorder)"
paulson@15341
   383
apply (simp (no_asm_use) add: linorder_not_le [symmetric])
paulson@15341
   384
apply (erule contrapos_nn)
paulson@15341
   385
apply (erule Least_le)
paulson@15341
   386
done
paulson@15341
   387
paulson@15341
   388
ML
paulson@15341
   389
{*
paulson@15341
   390
val wf_def = thm "wf_def";
paulson@15341
   391
val wfUNIVI = thm "wfUNIVI";
paulson@15341
   392
val wfI = thm "wfI";
paulson@15341
   393
val wf_induct = thm "wf_induct";
paulson@15341
   394
val wf_not_sym = thm "wf_not_sym";
paulson@15341
   395
val wf_asym = thm "wf_asym";
paulson@15341
   396
val wf_not_refl = thm "wf_not_refl";
paulson@15341
   397
val wf_irrefl = thm "wf_irrefl";
paulson@15341
   398
val wf_trancl = thm "wf_trancl";
paulson@15341
   399
val wf_converse_trancl = thm "wf_converse_trancl";
paulson@15341
   400
val wf_eq_minimal = thm "wf_eq_minimal";
paulson@15341
   401
val wf_subset = thm "wf_subset";
paulson@15341
   402
val wf_empty = thm "wf_empty";
paulson@15341
   403
val wf_insert = thm "wf_insert";
paulson@15341
   404
val wf_UN = thm "wf_UN";
paulson@15341
   405
val wf_Union = thm "wf_Union";
paulson@15341
   406
val wf_Un = thm "wf_Un";
paulson@15341
   407
val wf_prod_fun_image = thm "wf_prod_fun_image";
paulson@15341
   408
val acyclicI = thm "acyclicI";
paulson@15341
   409
val wf_acyclic = thm "wf_acyclic";
paulson@15341
   410
val acyclic_insert = thm "acyclic_insert";
paulson@15341
   411
val acyclic_converse = thm "acyclic_converse";
paulson@15341
   412
val acyclic_impl_antisym_rtrancl = thm "acyclic_impl_antisym_rtrancl";
paulson@15341
   413
val acyclic_subset = thm "acyclic_subset";
paulson@15341
   414
val cuts_eq = thm "cuts_eq";
paulson@15341
   415
val cut_apply = thm "cut_apply";
paulson@15341
   416
val wfrec_unique = thm "wfrec_unique";
paulson@15341
   417
val wfrec = thm "wfrec";
paulson@15341
   418
val def_wfrec = thm "def_wfrec";
paulson@15341
   419
val tfl_wf_induct = thm "tfl_wf_induct";
paulson@15341
   420
val tfl_cut_apply = thm "tfl_cut_apply";
paulson@15341
   421
val tfl_wfrec = thm "tfl_wfrec";
paulson@15341
   422
val LeastI = thm "LeastI";
paulson@15341
   423
val Least_le = thm "Least_le";
paulson@15341
   424
val not_less_Least = thm "not_less_Least";
paulson@15341
   425
*}
oheimb@11137
   426
nipkow@10213
   427
end