Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.

Relation.ML Trancl.ML: more thms

WF.ML WF.thy: added `acyclic'
WF_Rel.ML: moved some thms back into WF and added some new ones.

--- a/src/HOL/Finite.ML	Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/Finite.ML	Thu Jun 05 14:39:22 1997 +0200
@@ -8,8 +8,9 @@
 
 open Finite;
 
-section "The finite powerset operator -- Fin";
+section "finite";
 
+(*
 goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
 by (rtac lfp_mono 1);
 by (REPEAT (ares_tac basic_monos 1));
@@ -21,124 +22,99 @@
 
 (* A : Fin(B) ==> A <= B *)
 val FinD = Fin_subset_Pow RS subsetD RS PowD;
+*)
 
 (*Discharging ~ x:y entails extra work*)
 val major::prems = goal Finite.thy 
-    "[| F:Fin(A);  P({}); \
-\       !!F x. [| x:A;  F:Fin(A);  x~:F;  P(F) |] ==> P(insert x F) \
+    "[| finite F;  P({}); \
+\       !!F x. [| finite F;  x ~: F;  P(F) |] ==> P(insert x F) \
 \    |] ==> P(F)";
-by (rtac (major RS Fin.induct) 1);
-by (excluded_middle_tac "a:b" 2);
+by (rtac (major RS Finites.induct) 1);
+by (excluded_middle_tac "a:A" 2);
 by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3);   (*backtracking!*)
 by (REPEAT (ares_tac prems 1));
-qed "Fin_induct";
+qed "finite_induct";
+
+val major::prems = goal Finite.thy 
+    "[| finite F; \
+\       P({}); \
+\       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
+\    |] ==> F <= A --> P(F)";
+by (rtac (major RS finite_induct) 1);
+by(ALLGOALS (blast_tac (!claset addIs prems)));
+val lemma = result();
 
-Addsimps Fin.intrs;
+val prems = goal Finite.thy 
+    "[| finite F;  F <= A; \
+\       P({}); \
+\       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
+\    |] ==> P(F)";
+by(blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
+qed "finite_subset_induct";
+
+Addsimps Finites.intrs;
+AddSIs Finites.intrs;
 
 (*The union of two finite sets is finite*)
 val major::prems = goal Finite.thy
-    "[| F: Fin(A);  G: Fin(A) |] ==> F Un G : Fin(A)";
-by (rtac (major RS Fin_induct) 1);
+    "[| finite F;  finite G |] ==> finite(F Un G)";
+by (rtac (major RS finite_induct) 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
-qed "Fin_UnI";
+qed "finite_UnI";
 
 (*Every subset of a finite set is finite*)
-val [subs,fin] = goal Finite.thy "[| A<=B;  B: Fin(M) |] ==> A: Fin(M)";
-by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)",
+val [subs,fin] = goal Finite.thy "[| A<=B;  finite B |] ==> finite A";
+by (EVERY1 [subgoal_tac "ALL C. C<=B --> finite C",
             rtac mp, etac spec,
             rtac subs]);
-by (rtac (fin RS Fin_induct) 1);
+by (rtac (fin RS finite_induct) 1);
 by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
 by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1]));
 by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
 by (ALLGOALS Asm_simp_tac);
-qed "Fin_subset";
+qed "finite_subset";
 
-goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
-by (blast_tac (!claset addIs [Fin_UnI] addDs
-                [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
-qed "subset_Fin";
-Addsimps[subset_Fin];
+goal Finite.thy "finite(F Un G) = (finite F & finite G)";
+by (blast_tac (!claset addIs [finite_UnI] addDs
+                [Un_upper1 RS finite_subset, Un_upper2 RS finite_subset]) 1);
+qed "finite_Un";
+AddIffs[finite_Un];
 
-goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
+goal Finite.thy "finite(insert a A) = finite A";
 by (stac insert_is_Un 1);
-by (simp_tac (HOL_ss addsimps [subset_Fin]) 1);
-by (blast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
-qed "insert_Fin";
-Addsimps[insert_Fin];
+by (simp_tac (HOL_ss addsimps [finite_Un]) 1);
+by (blast_tac (!claset addSIs Finites.intrs) 1);
+qed "finite_insert";
+Addsimps[finite_insert];
 
-(*The image of a finite set is finite*)
-val major::_ = goal Finite.thy
-    "F: Fin(A) ==> h``F : Fin(h``A)";
-by (rtac (major RS Fin_induct) 1);
+(*The image of a finite set is finite *)
+goal Finite.thy  "!!F. finite F ==> finite(h``F)";
+by (etac finite_induct 1);
 by (Simp_tac 1);
-by (asm_simp_tac
-    (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]
-              delsimps [insert_Fin]) 1);
-qed "Fin_imageI";
+by (Asm_simp_tac 1);
+qed "finite_imageI";
 
 val major::prems = goal Finite.thy 
-    "[| c: Fin(A);  b: Fin(A);                                  \
+    "[| finite c;  finite b;                                  \
 \       P(b);                                                   \
-\       !!(x::'a) y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
+\       !!x y. [| finite y;  x:y;  P(y) |] ==> P(y-{x}) \
 \    |] ==> c<=b --> P(b-c)";
-by (rtac (major RS Fin_induct) 1);
+by (rtac (major RS finite_induct) 1);
 by (stac Diff_insert 2);
 by (ALLGOALS (asm_simp_tac
-                (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
+                (!simpset addsimps (prems@[Diff_subset RS finite_subset]))));
 val lemma = result();
 
 val prems = goal Finite.thy 
-    "[| b: Fin(A);                                              \
-\       P(b);                                                   \
-\       !!x y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
+    "[| finite A;                                       \
+\       P(A);                                           \
+\       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
 \    |] ==> P({})";
 by (rtac (Diff_cancel RS subst) 1);
 by (rtac (lemma RS mp) 1);
 by (REPEAT (ares_tac (subset_refl::prems) 1));
-qed "Fin_empty_induct";
-
-
-section "The predicate 'finite'";
-
-val major::prems = goalw Finite.thy [finite_def]
-    "[| finite F;  P({}); \
-\       !!F x. [| finite F;  x~:F;  P(F) |] ==> P(insert x F) \
-\    |] ==> P(F)";
-by (rtac (major RS Fin_induct) 1);
-by (REPEAT (ares_tac prems 1));
-qed "finite_induct";
-
-
-goalw Finite.thy [finite_def] "finite {}";
-by (Simp_tac 1);
-qed "finite_emptyI";
-Addsimps [finite_emptyI];
+qed "finite_empty_induct";
 
-goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)";
-by (Asm_simp_tac 1);
-qed "finite_insertI";
-
-(*The union of two finite sets is finite*)
-goalw Finite.thy [finite_def]
-    "!!F. [| finite F;  finite G |] ==> finite(F Un G)";
-by (Asm_simp_tac 1);
-qed "finite_UnI";
-
-goalw Finite.thy [finite_def] "!!A. [| A<=B;  finite B |] ==> finite A";
-by (etac Fin_subset 1);
-by (assume_tac 1);
-qed "finite_subset";
-
-goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
-by (Simp_tac 1);
-qed "finite_Un_eq";
-Addsimps[finite_Un_eq];
-
-goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
-by (Simp_tac 1);
-qed "finite_insert";
-Addsimps[finite_insert];
 
 (* finite B ==> finite (B - Ba) *)
 bind_thm ("finite_Diff", Diff_subset RS finite_subset);
@@ -152,25 +128,22 @@
 qed "finite_Diff_singleton";
 AddIffs [finite_Diff_singleton];
 
-(*The image of a finite set is finite*)
-goal Finite.thy "!!F. finite F ==> finite(h``F)";
+(*** FIXME -> equalities.ML ***)
+goal Set.thy "(f``A = {}) = (A = {})";
+by (blast_tac (!claset addSEs [equalityE]) 1);
+qed "image_is_empty";
+Addsimps [image_is_empty];
+
+goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
 by (etac finite_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "finite_imageI";
-
-goal Finite.thy "!!A. finite B ==> !A. B = f``A --> inj_onto f A --> finite A";
-by (etac finite_induct 1);
-by (ALLGOALS Asm_simp_tac);
+ by (ALLGOALS Asm_simp_tac);
 by (Step_tac 1);
-by (subgoal_tac "A={}" 1);
-by (blast_tac (!claset addSEs [equalityE]) 2);
-by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 2);
-by (Step_tac 1);
-bw inj_onto_def;
-by (Blast_tac 2);
-by (ALLGOALS Asm_simp_tac);
+by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
+ by (Step_tac 1);
+ bw inj_onto_def;
+ by (Blast_tac 1);
 by (thin_tac "ALL A. ?PP(A)" 1);
-by (forward_tac [[equalityD1, insertI1] MRS subsetD] 1);
+by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
 by (Step_tac 1);
 by (res_inst_tac [("x","xa")] bexI 1);
 by (ALLGOALS Asm_simp_tac);
@@ -207,15 +180,6 @@
 qed "finite_Pow_iff";
 AddIffs [finite_Pow_iff];
 
-val major::prems = goalw Finite.thy [finite_def]
-    "[| finite A;                                       \
-\       P(A);                                           \
-\       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
-\    |] ==> P({})";
-by (rtac (major RS Fin_empty_induct) 1);
-by (REPEAT (ares_tac (subset_refl::prems) 1));
-qed "finite_empty_induct";
-
 
 section "Finite cardinality -- 'card'";
 
@@ -346,7 +310,7 @@
 by (Simp_tac 1);
 by (strip_tac 1);
 by (case_tac "x:B" 1);
- by (dtac mk_disjoint_insert 1);
+ by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
  by (SELECT_GOAL(safe_tac (!claset))1);
  by (rotate_tac ~1 1);
  by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
@@ -439,7 +403,7 @@
 by (etac conjE 1);
 by (case_tac "x:A" 1);
 (*1*)
-by (dtac mk_disjoint_insert 1);
+by (dres_inst_tac [("A","A")]mk_disjoint_insert 1);
 by (etac exE 1);
 by (etac conjE 1);
 by (hyp_subst_tac 1);

--- a/src/HOL/Finite.thy	Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/Finite.thy	Thu Jun 05 14:39:22 1997 +0200
@@ -8,18 +8,17 @@
 
 Finite = Divides + Power + 
 
-consts Fin :: 'a set => 'a set set
+consts Finites :: 'a set set
 
-inductive "Fin(A)"
+inductive "Finites"
   intrs
-    emptyI  "{} : Fin(A)"
-    insertI "[| a: A;  b: Fin(A) |] ==> insert a b : Fin(A)"
+    emptyI  "{} : Finites"
+    insertI "A : Finites ==> insert a A : Finites"
+
+syntax finite :: 'a set => bool
+translations  "finite A"  ==  "A : Finites"
 
 constdefs
-
-  finite :: 'a set => bool
-  "finite A == A : Fin(UNIV)"
-
   card :: 'a set => nat
   "card A == LEAST n. ? f. A = {f i |i. i<n}"
 

--- a/src/HOL/Relation.ML	Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/Relation.ML	Thu Jun 05 14:39:22 1997 +0200
@@ -106,6 +106,11 @@
 goalw Relation.thy [converse_def] "converse(converse R) = R";
 by (Blast_tac 1);
 qed "converse_converse";
+Addsimps [converse_converse];
+
+goal Relation.thy "converse(r O s) = converse s O converse r";
+by(Blast_tac 1);
+qed "converse_comp";
 
 (** Domain **)
 

--- a/src/HOL/Trancl.ML	Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/Trancl.ML	Thu Jun 05 14:39:22 1997 +0200
@@ -182,9 +182,31 @@
 by (REPEAT(ares_tac prems 1));
 qed "converse_rtrancl_induct2";
 
+val major::prems = goal Trancl.thy
+ "[| (x,z):r^*; \
+\    x=z ==> P; \
+\    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
+\ |] ==> P";
+by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
+by (rtac (major RS converse_rtrancl_induct) 2);
+by (blast_tac (!claset addIs prems) 2);
+by (blast_tac (!claset addIs prems) 2);
+by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
+qed "rtranclE2";
+
+goal Trancl.thy "r O r^* = r^* O r";
+by(Step_tac 1);
+ by(blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
+by(blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
+qed "r_comp_rtrancl_eq";
+
 
 (**** The relation trancl ****)
 
+goalw Trancl.thy [trancl_def] "!!p.[| p:r^+; r <= s |] ==> p:s^+";
+by(blast_tac (!claset addIs [rtrancl_mono RS subsetD]) 1);
+qed "trancl_mono";
+
 (** Conversions between trancl and rtrancl **)
 
 val [major] = goalw Trancl.thy [trancl_def]
@@ -255,6 +277,11 @@
 
 bind_thm ("trancl_trans", trans_trancl RS transD);
 
+goalw Trancl.thy [trancl_def]
+  "!!r. [| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
+by(blast_tac (!claset addIs [rtrancl_trans,r_into_rtrancl]) 1);
+qed "rtrancl_trancl_trancl";
+
 val prems = goal Trancl.thy
     "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+";
 by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
@@ -262,6 +289,26 @@
 by (resolve_tac prems 1);
 qed "trancl_into_trancl2";
 
+(* primitive recursion for trancl over finite relations: *)
+goal Trancl.thy "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
+br equalityI 1;
+ br subsetI 1;
+ by(split_all_tac 1);
+ be trancl_induct 1;
+  by(blast_tac (!claset addIs [r_into_trancl]) 1);
+ by(blast_tac (!claset addIs
+     [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
+br subsetI 1;
+by(blast_tac (!claset addIs
+     [rtrancl_into_trancl2, rtrancl_trancl_trancl,
+      impOfSubs rtrancl_mono, trancl_mono]) 1);
+qed "trancl_insert";
+
+goalw Trancl.thy [trancl_def] "(converse r)^+ = converse(r^+)";
+by(simp_tac (!simpset addsimps [rtrancl_converse,converse_comp]) 1);
+by(simp_tac (!simpset addsimps [rtrancl_converse RS sym,r_comp_rtrancl_eq]) 1);
+qed "trancl_converse";
+
 
 val major::prems = goal Trancl.thy
     "[| (a,b) : r^*;  r <= A Times A |] ==> a=b | a:A";

--- a/src/HOL/WF.ML	Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/WF.ML	Thu Jun 05 14:39:22 1997 +0200
@@ -84,6 +84,66 @@
 by (blast_tac (!claset addSIs [lemma1, lemma2]) 1);
 qed "wf_eq_minimal";
 
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of subsets
+ *---------------------------------------------------------------------------*)
+
+goal thy "!!r. [| wf(r);  p<=r |] ==> wf(p)";
+by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
+by (Fast_tac 1);
+qed "wf_subset";
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of the empty relation.
+ *---------------------------------------------------------------------------*)
+
+goal thy "wf({})";
+by (simp_tac (!simpset addsimps [wf_def]) 1);
+qed "wf_empty";
+AddSIs [wf_empty];
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of `insert'
+ *---------------------------------------------------------------------------*)
+
+goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
+br iffI 1;
+ by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs
+      [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
+by(asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
+by(safe_tac (!claset));
+by(EVERY1[rtac allE, atac, etac impE, Blast_tac]);
+be bexE 1;
+by(rename_tac "a" 1);
+by(case_tac "a = x" 1);
+ by(res_inst_tac [("x","a")]bexI 2);
+  ba 3;
+ by(Blast_tac 2);
+by(case_tac "y:Q" 1);
+ by(Blast_tac 2);
+by(res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
+ ba 1;
+by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
+qed "wf_insert";
+AddIffs [wf_insert];
+
+(*** acyclic ***)
+
+goalw WF.thy [acyclic_def]
+ "!!r. wf r ==> acyclic r";
+by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1);
+qed "wf_acyclic";
+
+goalw WF.thy [acyclic_def]
+  "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
+by(simp_tac (!simpset addsimps [trancl_insert]) 1);
+by(blast_tac (!claset addEs [make_elim rtrancl_trans]) 1);
+qed "acyclic_insert";
+AddIffs [acyclic_insert];
+
+goalw WF.thy [acyclic_def] "acyclic(converse r) = acyclic r";
+by(simp_tac (!simpset addsimps [trancl_converse]) 1);
+qed "acyclic_converse";
 
 (** cut **)
 
@@ -272,4 +332,3 @@
 by (assume_tac 1);
 by (assume_tac 1);
 qed "tfl_wfrec";
-

--- a/src/HOL/WF.thy	Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/WF.thy	Thu Jun 05 14:39:22 1997 +0200
@@ -12,6 +12,9 @@
   wf         :: "('a * 'a)set => bool"
   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
 
+  acyclic :: "('a*'a)set => bool"
+  "acyclic r == !x. (x,x) ~: r^+"
+
   cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
   "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
 

--- a/src/HOL/WF_Rel.ML	Thu Jun 05 14:06:23 1997 +0200
+++ b/src/HOL/WF_Rel.ML	Thu Jun 05 14:39:22 1997 +0200
@@ -63,15 +63,10 @@
  * Wellfoundedness of lexicographic combinations
  *---------------------------------------------------------------------------*)
 
-goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)";
-by (rtac allI 1);
-by (rtac (surjective_pairing RS ssubst) 1);
-by (Blast_tac 1);
-qed "split_all_pair";
-
 val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
  "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
-by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
+by (EVERY1 [rtac allI,rtac impI]);
+by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
 by (rtac (wfa RS spec RS mp) 1);
 by (EVERY1 [rtac allI,rtac impI]);
 by (rtac (wfb RS spec RS mp) 1);
@@ -80,25 +75,6 @@
 AddSIs [wf_lex_prod];
 
 (*---------------------------------------------------------------------------
- * Wellfoundedness of subsets
- *---------------------------------------------------------------------------*)
-
-goal thy "!!r. [| wf(r);  p<=r |] ==> wf(p)";
-by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
-by (Fast_tac 1);
-qed "wf_subset";
-
-(*---------------------------------------------------------------------------
- * Wellfoundedness of the empty relation.
- *---------------------------------------------------------------------------*)
-
-goal thy "wf({})";
-by (simp_tac (!simpset addsimps [wf_def]) 1);
-qed "wf_empty";
-AddSIs [wf_empty];
-
-
-(*---------------------------------------------------------------------------
  * Transitivity of WF combinators.
  *---------------------------------------------------------------------------*)
 goalw thy [trans_def, lex_prod_def]
@@ -124,3 +100,58 @@
 by (Blast_tac 1);
 qed "trans_finite_psubset";
 
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of finite acyclic relations
+ * Cannot go into WF because it needs Finite
+ *---------------------------------------------------------------------------*)
+
+goal thy "!!r. finite r ==> acyclic r --> wf r";
+be finite_induct 1;
+ by(Blast_tac 1);
+by(split_all_tac 1);
+by(Asm_full_simp_tac 1);
+qed_spec_mp "finite_acyclic_wf";
+
+goal thy "!!r. finite r ==> wf r = acyclic r";
+by(blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
+qed "wf_iff_acyclic_if_finite";
+
+
+(*---------------------------------------------------------------------------
+ * A relation is wellfounded iff it has no infinite descending chain
+ *---------------------------------------------------------------------------*)
+
+goalw thy [wf_eq_minimal RS eq_reflection]
+  "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
+br iffI 1;
+ br notI 1;
+ be exE 1;
+ by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
+ by(Blast_tac 1);
+be swap 1;
+by(Asm_full_simp_tac 1);
+be exE 1;
+be swap 1;
+br impI 1;
+be swap 1;
+be exE 1;
+by(rename_tac "x" 1);
+by(subgoal_tac
+ "!i. nat_rec x (%i y. @z. z:Q & (z,y):r) (Suc i) : Q & \
+\     (nat_rec x (%i y. @z. z:Q & (z,y):r) (Suc i),\
+\      nat_rec x (%i y. @z. z:Q & (z,y):r) i): r" 1);
+ by(Blast_tac 1);
+br allI 1;
+by(induct_tac "i" 1);
+ by(Asm_simp_tac 1);
+ by(subgoal_tac "? y. y : Q & (y,x):r" 1);
+  by(Blast_tac 2);
+ be exE 1;
+ be selectI 1;
+by(subgoal_tac "? y.y:Q & (y,nat_rec x (%i y. @z. z:Q & (z,y):r)(Suc i)):r" 1);
+ by(Blast_tac 2);
+by(Asm_full_simp_tac 1);
+be exE 1;
+(* `be selectI 1' takes a long time; hence the instantiation: *)
+by (eres_inst_tac[("P","%u.u:Q & (u,?v):r")]selectI 1);
+qed "wf_iff_no_infinite_down_chain";