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