Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
authornipkow
Thu Jun 05 14:39:22 1997 +0200 (1997-06-05)
changeset 3413c1f63cc3a768
parent 3412 5b658dadf560
child 3414 804c8a178a7f
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.
src/HOL/Finite.ML
src/HOL/Finite.thy
src/HOL/Relation.ML
src/HOL/Trancl.ML
src/HOL/WF.ML
src/HOL/WF.thy
src/HOL/WF_Rel.ML
     1.1 --- a/src/HOL/Finite.ML	Thu Jun 05 14:06:23 1997 +0200
     1.2 +++ b/src/HOL/Finite.ML	Thu Jun 05 14:39:22 1997 +0200
     1.3 @@ -8,8 +8,9 @@
     1.4  
     1.5  open Finite;
     1.6  
     1.7 -section "The finite powerset operator -- Fin";
     1.8 +section "finite";
     1.9  
    1.10 +(*
    1.11  goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)";
    1.12  by (rtac lfp_mono 1);
    1.13  by (REPEAT (ares_tac basic_monos 1));
    1.14 @@ -21,124 +22,99 @@
    1.15  
    1.16  (* A : Fin(B) ==> A <= B *)
    1.17  val FinD = Fin_subset_Pow RS subsetD RS PowD;
    1.18 +*)
    1.19  
    1.20  (*Discharging ~ x:y entails extra work*)
    1.21  val major::prems = goal Finite.thy 
    1.22 -    "[| F:Fin(A);  P({}); \
    1.23 -\       !!F x. [| x:A;  F:Fin(A);  x~:F;  P(F) |] ==> P(insert x F) \
    1.24 +    "[| finite F;  P({}); \
    1.25 +\       !!F x. [| finite F;  x ~: F;  P(F) |] ==> P(insert x F) \
    1.26  \    |] ==> P(F)";
    1.27 -by (rtac (major RS Fin.induct) 1);
    1.28 -by (excluded_middle_tac "a:b" 2);
    1.29 +by (rtac (major RS Finites.induct) 1);
    1.30 +by (excluded_middle_tac "a:A" 2);
    1.31  by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3);   (*backtracking!*)
    1.32  by (REPEAT (ares_tac prems 1));
    1.33 -qed "Fin_induct";
    1.34 +qed "finite_induct";
    1.35 +
    1.36 +val major::prems = goal Finite.thy 
    1.37 +    "[| finite F; \
    1.38 +\       P({}); \
    1.39 +\       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
    1.40 +\    |] ==> F <= A --> P(F)";
    1.41 +by (rtac (major RS finite_induct) 1);
    1.42 +by(ALLGOALS (blast_tac (!claset addIs prems)));
    1.43 +val lemma = result();
    1.44  
    1.45 -Addsimps Fin.intrs;
    1.46 +val prems = goal Finite.thy 
    1.47 +    "[| finite F;  F <= A; \
    1.48 +\       P({}); \
    1.49 +\       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
    1.50 +\    |] ==> P(F)";
    1.51 +by(blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
    1.52 +qed "finite_subset_induct";
    1.53 +
    1.54 +Addsimps Finites.intrs;
    1.55 +AddSIs Finites.intrs;
    1.56  
    1.57  (*The union of two finite sets is finite*)
    1.58  val major::prems = goal Finite.thy
    1.59 -    "[| F: Fin(A);  G: Fin(A) |] ==> F Un G : Fin(A)";
    1.60 -by (rtac (major RS Fin_induct) 1);
    1.61 +    "[| finite F;  finite G |] ==> finite(F Un G)";
    1.62 +by (rtac (major RS finite_induct) 1);
    1.63  by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
    1.64 -qed "Fin_UnI";
    1.65 +qed "finite_UnI";
    1.66  
    1.67  (*Every subset of a finite set is finite*)
    1.68 -val [subs,fin] = goal Finite.thy "[| A<=B;  B: Fin(M) |] ==> A: Fin(M)";
    1.69 -by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)",
    1.70 +val [subs,fin] = goal Finite.thy "[| A<=B;  finite B |] ==> finite A";
    1.71 +by (EVERY1 [subgoal_tac "ALL C. C<=B --> finite C",
    1.72              rtac mp, etac spec,
    1.73              rtac subs]);
    1.74 -by (rtac (fin RS Fin_induct) 1);
    1.75 +by (rtac (fin RS finite_induct) 1);
    1.76  by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
    1.77  by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1]));
    1.78  by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
    1.79  by (ALLGOALS Asm_simp_tac);
    1.80 -qed "Fin_subset";
    1.81 +qed "finite_subset";
    1.82  
    1.83 -goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))";
    1.84 -by (blast_tac (!claset addIs [Fin_UnI] addDs
    1.85 -                [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1);
    1.86 -qed "subset_Fin";
    1.87 -Addsimps[subset_Fin];
    1.88 +goal Finite.thy "finite(F Un G) = (finite F & finite G)";
    1.89 +by (blast_tac (!claset addIs [finite_UnI] addDs
    1.90 +                [Un_upper1 RS finite_subset, Un_upper2 RS finite_subset]) 1);
    1.91 +qed "finite_Un";
    1.92 +AddIffs[finite_Un];
    1.93  
    1.94 -goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)";
    1.95 +goal Finite.thy "finite(insert a A) = finite A";
    1.96  by (stac insert_is_Un 1);
    1.97 -by (simp_tac (HOL_ss addsimps [subset_Fin]) 1);
    1.98 -by (blast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1);
    1.99 -qed "insert_Fin";
   1.100 -Addsimps[insert_Fin];
   1.101 +by (simp_tac (HOL_ss addsimps [finite_Un]) 1);
   1.102 +by (blast_tac (!claset addSIs Finites.intrs) 1);
   1.103 +qed "finite_insert";
   1.104 +Addsimps[finite_insert];
   1.105  
   1.106 -(*The image of a finite set is finite*)
   1.107 -val major::_ = goal Finite.thy
   1.108 -    "F: Fin(A) ==> h``F : Fin(h``A)";
   1.109 -by (rtac (major RS Fin_induct) 1);
   1.110 +(*The image of a finite set is finite *)
   1.111 +goal Finite.thy  "!!F. finite F ==> finite(h``F)";
   1.112 +by (etac finite_induct 1);
   1.113  by (Simp_tac 1);
   1.114 -by (asm_simp_tac
   1.115 -    (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]
   1.116 -              delsimps [insert_Fin]) 1);
   1.117 -qed "Fin_imageI";
   1.118 +by (Asm_simp_tac 1);
   1.119 +qed "finite_imageI";
   1.120  
   1.121  val major::prems = goal Finite.thy 
   1.122 -    "[| c: Fin(A);  b: Fin(A);                                  \
   1.123 +    "[| finite c;  finite b;                                  \
   1.124  \       P(b);                                                   \
   1.125 -\       !!(x::'a) y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
   1.126 +\       !!x y. [| finite y;  x:y;  P(y) |] ==> P(y-{x}) \
   1.127  \    |] ==> c<=b --> P(b-c)";
   1.128 -by (rtac (major RS Fin_induct) 1);
   1.129 +by (rtac (major RS finite_induct) 1);
   1.130  by (stac Diff_insert 2);
   1.131  by (ALLGOALS (asm_simp_tac
   1.132 -                (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
   1.133 +                (!simpset addsimps (prems@[Diff_subset RS finite_subset]))));
   1.134  val lemma = result();
   1.135  
   1.136  val prems = goal Finite.thy 
   1.137 -    "[| b: Fin(A);                                              \
   1.138 -\       P(b);                                                   \
   1.139 -\       !!x y. [| x:A; y: Fin(A);  x:y;  P(y) |] ==> P(y-{x}) \
   1.140 +    "[| finite A;                                       \
   1.141 +\       P(A);                                           \
   1.142 +\       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
   1.143  \    |] ==> P({})";
   1.144  by (rtac (Diff_cancel RS subst) 1);
   1.145  by (rtac (lemma RS mp) 1);
   1.146  by (REPEAT (ares_tac (subset_refl::prems) 1));
   1.147 -qed "Fin_empty_induct";
   1.148 -
   1.149 -
   1.150 -section "The predicate 'finite'";
   1.151 -
   1.152 -val major::prems = goalw Finite.thy [finite_def]
   1.153 -    "[| finite F;  P({}); \
   1.154 -\       !!F x. [| finite F;  x~:F;  P(F) |] ==> P(insert x F) \
   1.155 -\    |] ==> P(F)";
   1.156 -by (rtac (major RS Fin_induct) 1);
   1.157 -by (REPEAT (ares_tac prems 1));
   1.158 -qed "finite_induct";
   1.159 -
   1.160 -
   1.161 -goalw Finite.thy [finite_def] "finite {}";
   1.162 -by (Simp_tac 1);
   1.163 -qed "finite_emptyI";
   1.164 -Addsimps [finite_emptyI];
   1.165 +qed "finite_empty_induct";
   1.166  
   1.167 -goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)";
   1.168 -by (Asm_simp_tac 1);
   1.169 -qed "finite_insertI";
   1.170 -
   1.171 -(*The union of two finite sets is finite*)
   1.172 -goalw Finite.thy [finite_def]
   1.173 -    "!!F. [| finite F;  finite G |] ==> finite(F Un G)";
   1.174 -by (Asm_simp_tac 1);
   1.175 -qed "finite_UnI";
   1.176 -
   1.177 -goalw Finite.thy [finite_def] "!!A. [| A<=B;  finite B |] ==> finite A";
   1.178 -by (etac Fin_subset 1);
   1.179 -by (assume_tac 1);
   1.180 -qed "finite_subset";
   1.181 -
   1.182 -goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)";
   1.183 -by (Simp_tac 1);
   1.184 -qed "finite_Un_eq";
   1.185 -Addsimps[finite_Un_eq];
   1.186 -
   1.187 -goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)";
   1.188 -by (Simp_tac 1);
   1.189 -qed "finite_insert";
   1.190 -Addsimps[finite_insert];
   1.191  
   1.192  (* finite B ==> finite (B - Ba) *)
   1.193  bind_thm ("finite_Diff", Diff_subset RS finite_subset);
   1.194 @@ -152,25 +128,22 @@
   1.195  qed "finite_Diff_singleton";
   1.196  AddIffs [finite_Diff_singleton];
   1.197  
   1.198 -(*The image of a finite set is finite*)
   1.199 -goal Finite.thy "!!F. finite F ==> finite(h``F)";
   1.200 +(*** FIXME -> equalities.ML ***)
   1.201 +goal Set.thy "(f``A = {}) = (A = {})";
   1.202 +by (blast_tac (!claset addSEs [equalityE]) 1);
   1.203 +qed "image_is_empty";
   1.204 +Addsimps [image_is_empty];
   1.205 +
   1.206 +goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
   1.207  by (etac finite_induct 1);
   1.208 -by (ALLGOALS Asm_simp_tac);
   1.209 -qed "finite_imageI";
   1.210 -
   1.211 -goal Finite.thy "!!A. finite B ==> !A. B = f``A --> inj_onto f A --> finite A";
   1.212 -by (etac finite_induct 1);
   1.213 -by (ALLGOALS Asm_simp_tac);
   1.214 + by (ALLGOALS Asm_simp_tac);
   1.215  by (Step_tac 1);
   1.216 -by (subgoal_tac "A={}" 1);
   1.217 -by (blast_tac (!claset addSEs [equalityE]) 2);
   1.218 -by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 2);
   1.219 -by (Step_tac 1);
   1.220 -bw inj_onto_def;
   1.221 -by (Blast_tac 2);
   1.222 -by (ALLGOALS Asm_simp_tac);
   1.223 +by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
   1.224 + by (Step_tac 1);
   1.225 + bw inj_onto_def;
   1.226 + by (Blast_tac 1);
   1.227  by (thin_tac "ALL A. ?PP(A)" 1);
   1.228 -by (forward_tac [[equalityD1, insertI1] MRS subsetD] 1);
   1.229 +by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
   1.230  by (Step_tac 1);
   1.231  by (res_inst_tac [("x","xa")] bexI 1);
   1.232  by (ALLGOALS Asm_simp_tac);
   1.233 @@ -207,15 +180,6 @@
   1.234  qed "finite_Pow_iff";
   1.235  AddIffs [finite_Pow_iff];
   1.236  
   1.237 -val major::prems = goalw Finite.thy [finite_def]
   1.238 -    "[| finite A;                                       \
   1.239 -\       P(A);                                           \
   1.240 -\       !!a A. [| finite A;  a:A;  P(A) |] ==> P(A-{a}) \
   1.241 -\    |] ==> P({})";
   1.242 -by (rtac (major RS Fin_empty_induct) 1);
   1.243 -by (REPEAT (ares_tac (subset_refl::prems) 1));
   1.244 -qed "finite_empty_induct";
   1.245 -
   1.246  
   1.247  section "Finite cardinality -- 'card'";
   1.248  
   1.249 @@ -346,7 +310,7 @@
   1.250  by (Simp_tac 1);
   1.251  by (strip_tac 1);
   1.252  by (case_tac "x:B" 1);
   1.253 - by (dtac mk_disjoint_insert 1);
   1.254 + by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
   1.255   by (SELECT_GOAL(safe_tac (!claset))1);
   1.256   by (rotate_tac ~1 1);
   1.257   by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1);
   1.258 @@ -439,7 +403,7 @@
   1.259  by (etac conjE 1);
   1.260  by (case_tac "x:A" 1);
   1.261  (*1*)
   1.262 -by (dtac mk_disjoint_insert 1);
   1.263 +by (dres_inst_tac [("A","A")]mk_disjoint_insert 1);
   1.264  by (etac exE 1);
   1.265  by (etac conjE 1);
   1.266  by (hyp_subst_tac 1);
     2.1 --- a/src/HOL/Finite.thy	Thu Jun 05 14:06:23 1997 +0200
     2.2 +++ b/src/HOL/Finite.thy	Thu Jun 05 14:39:22 1997 +0200
     2.3 @@ -8,18 +8,17 @@
     2.4  
     2.5  Finite = Divides + Power + 
     2.6  
     2.7 -consts Fin :: 'a set => 'a set set
     2.8 +consts Finites :: 'a set set
     2.9  
    2.10 -inductive "Fin(A)"
    2.11 +inductive "Finites"
    2.12    intrs
    2.13 -    emptyI  "{} : Fin(A)"
    2.14 -    insertI "[| a: A;  b: Fin(A) |] ==> insert a b : Fin(A)"
    2.15 +    emptyI  "{} : Finites"
    2.16 +    insertI "A : Finites ==> insert a A : Finites"
    2.17 +
    2.18 +syntax finite :: 'a set => bool
    2.19 +translations  "finite A"  ==  "A : Finites"
    2.20  
    2.21  constdefs
    2.22 -
    2.23 -  finite :: 'a set => bool
    2.24 -  "finite A == A : Fin(UNIV)"
    2.25 -
    2.26    card :: 'a set => nat
    2.27    "card A == LEAST n. ? f. A = {f i |i. i<n}"
    2.28  
     3.1 --- a/src/HOL/Relation.ML	Thu Jun 05 14:06:23 1997 +0200
     3.2 +++ b/src/HOL/Relation.ML	Thu Jun 05 14:39:22 1997 +0200
     3.3 @@ -106,6 +106,11 @@
     3.4  goalw Relation.thy [converse_def] "converse(converse R) = R";
     3.5  by (Blast_tac 1);
     3.6  qed "converse_converse";
     3.7 +Addsimps [converse_converse];
     3.8 +
     3.9 +goal Relation.thy "converse(r O s) = converse s O converse r";
    3.10 +by(Blast_tac 1);
    3.11 +qed "converse_comp";
    3.12  
    3.13  (** Domain **)
    3.14  
     4.1 --- a/src/HOL/Trancl.ML	Thu Jun 05 14:06:23 1997 +0200
     4.2 +++ b/src/HOL/Trancl.ML	Thu Jun 05 14:39:22 1997 +0200
     4.3 @@ -182,9 +182,31 @@
     4.4  by (REPEAT(ares_tac prems 1));
     4.5  qed "converse_rtrancl_induct2";
     4.6  
     4.7 +val major::prems = goal Trancl.thy
     4.8 + "[| (x,z):r^*; \
     4.9 +\    x=z ==> P; \
    4.10 +\    !!y. [| (x,y):r; (y,z):r^* |] ==> P \
    4.11 +\ |] ==> P";
    4.12 +by (subgoal_tac "x = z  | (? y. (x,y) : r & (y,z) : r^*)" 1);
    4.13 +by (rtac (major RS converse_rtrancl_induct) 2);
    4.14 +by (blast_tac (!claset addIs prems) 2);
    4.15 +by (blast_tac (!claset addIs prems) 2);
    4.16 +by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1));
    4.17 +qed "rtranclE2";
    4.18 +
    4.19 +goal Trancl.thy "r O r^* = r^* O r";
    4.20 +by(Step_tac 1);
    4.21 + by(blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
    4.22 +by(blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
    4.23 +qed "r_comp_rtrancl_eq";
    4.24 +
    4.25  
    4.26  (**** The relation trancl ****)
    4.27  
    4.28 +goalw Trancl.thy [trancl_def] "!!p.[| p:r^+; r <= s |] ==> p:s^+";
    4.29 +by(blast_tac (!claset addIs [rtrancl_mono RS subsetD]) 1);
    4.30 +qed "trancl_mono";
    4.31 +
    4.32  (** Conversions between trancl and rtrancl **)
    4.33  
    4.34  val [major] = goalw Trancl.thy [trancl_def]
    4.35 @@ -255,6 +277,11 @@
    4.36  
    4.37  bind_thm ("trancl_trans", trans_trancl RS transD);
    4.38  
    4.39 +goalw Trancl.thy [trancl_def]
    4.40 +  "!!r. [| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
    4.41 +by(blast_tac (!claset addIs [rtrancl_trans,r_into_rtrancl]) 1);
    4.42 +qed "rtrancl_trancl_trancl";
    4.43 +
    4.44  val prems = goal Trancl.thy
    4.45      "[| (a,b) : r;  (b,c) : r^+ |]   ==>  (a,c) : r^+";
    4.46  by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1);
    4.47 @@ -262,6 +289,26 @@
    4.48  by (resolve_tac prems 1);
    4.49  qed "trancl_into_trancl2";
    4.50  
    4.51 +(* primitive recursion for trancl over finite relations: *)
    4.52 +goal Trancl.thy "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
    4.53 +br equalityI 1;
    4.54 + br subsetI 1;
    4.55 + by(split_all_tac 1);
    4.56 + be trancl_induct 1;
    4.57 +  by(blast_tac (!claset addIs [r_into_trancl]) 1);
    4.58 + by(blast_tac (!claset addIs
    4.59 +     [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
    4.60 +br subsetI 1;
    4.61 +by(blast_tac (!claset addIs
    4.62 +     [rtrancl_into_trancl2, rtrancl_trancl_trancl,
    4.63 +      impOfSubs rtrancl_mono, trancl_mono]) 1);
    4.64 +qed "trancl_insert";
    4.65 +
    4.66 +goalw Trancl.thy [trancl_def] "(converse r)^+ = converse(r^+)";
    4.67 +by(simp_tac (!simpset addsimps [rtrancl_converse,converse_comp]) 1);
    4.68 +by(simp_tac (!simpset addsimps [rtrancl_converse RS sym,r_comp_rtrancl_eq]) 1);
    4.69 +qed "trancl_converse";
    4.70 +
    4.71  
    4.72  val major::prems = goal Trancl.thy
    4.73      "[| (a,b) : r^*;  r <= A Times A |] ==> a=b | a:A";
     5.1 --- a/src/HOL/WF.ML	Thu Jun 05 14:06:23 1997 +0200
     5.2 +++ b/src/HOL/WF.ML	Thu Jun 05 14:39:22 1997 +0200
     5.3 @@ -84,6 +84,66 @@
     5.4  by (blast_tac (!claset addSIs [lemma1, lemma2]) 1);
     5.5  qed "wf_eq_minimal";
     5.6  
     5.7 +(*---------------------------------------------------------------------------
     5.8 + * Wellfoundedness of subsets
     5.9 + *---------------------------------------------------------------------------*)
    5.10 +
    5.11 +goal thy "!!r. [| wf(r);  p<=r |] ==> wf(p)";
    5.12 +by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
    5.13 +by (Fast_tac 1);
    5.14 +qed "wf_subset";
    5.15 +
    5.16 +(*---------------------------------------------------------------------------
    5.17 + * Wellfoundedness of the empty relation.
    5.18 + *---------------------------------------------------------------------------*)
    5.19 +
    5.20 +goal thy "wf({})";
    5.21 +by (simp_tac (!simpset addsimps [wf_def]) 1);
    5.22 +qed "wf_empty";
    5.23 +AddSIs [wf_empty];
    5.24 +
    5.25 +(*---------------------------------------------------------------------------
    5.26 + * Wellfoundedness of `insert'
    5.27 + *---------------------------------------------------------------------------*)
    5.28 +
    5.29 +goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
    5.30 +br iffI 1;
    5.31 + by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs
    5.32 +      [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
    5.33 +by(asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
    5.34 +by(safe_tac (!claset));
    5.35 +by(EVERY1[rtac allE, atac, etac impE, Blast_tac]);
    5.36 +be bexE 1;
    5.37 +by(rename_tac "a" 1);
    5.38 +by(case_tac "a = x" 1);
    5.39 + by(res_inst_tac [("x","a")]bexI 2);
    5.40 +  ba 3;
    5.41 + by(Blast_tac 2);
    5.42 +by(case_tac "y:Q" 1);
    5.43 + by(Blast_tac 2);
    5.44 +by(res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
    5.45 + ba 1;
    5.46 +by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
    5.47 +qed "wf_insert";
    5.48 +AddIffs [wf_insert];
    5.49 +
    5.50 +(*** acyclic ***)
    5.51 +
    5.52 +goalw WF.thy [acyclic_def]
    5.53 + "!!r. wf r ==> acyclic r";
    5.54 +by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1);
    5.55 +qed "wf_acyclic";
    5.56 +
    5.57 +goalw WF.thy [acyclic_def]
    5.58 +  "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
    5.59 +by(simp_tac (!simpset addsimps [trancl_insert]) 1);
    5.60 +by(blast_tac (!claset addEs [make_elim rtrancl_trans]) 1);
    5.61 +qed "acyclic_insert";
    5.62 +AddIffs [acyclic_insert];
    5.63 +
    5.64 +goalw WF.thy [acyclic_def] "acyclic(converse r) = acyclic r";
    5.65 +by(simp_tac (!simpset addsimps [trancl_converse]) 1);
    5.66 +qed "acyclic_converse";
    5.67  
    5.68  (** cut **)
    5.69  
    5.70 @@ -272,4 +332,3 @@
    5.71  by (assume_tac 1);
    5.72  by (assume_tac 1);
    5.73  qed "tfl_wfrec";
    5.74 -
     6.1 --- a/src/HOL/WF.thy	Thu Jun 05 14:06:23 1997 +0200
     6.2 +++ b/src/HOL/WF.thy	Thu Jun 05 14:39:22 1997 +0200
     6.3 @@ -12,6 +12,9 @@
     6.4    wf         :: "('a * 'a)set => bool"
     6.5    "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))"
     6.6  
     6.7 +  acyclic :: "('a*'a)set => bool"
     6.8 +  "acyclic r == !x. (x,x) ~: r^+"
     6.9 +
    6.10    cut        :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b"
    6.11    "cut f r x == (%y. if (y,x):r then f y else arbitrary)"
    6.12  
     7.1 --- a/src/HOL/WF_Rel.ML	Thu Jun 05 14:06:23 1997 +0200
     7.2 +++ b/src/HOL/WF_Rel.ML	Thu Jun 05 14:39:22 1997 +0200
     7.3 @@ -63,15 +63,10 @@
     7.4   * Wellfoundedness of lexicographic combinations
     7.5   *---------------------------------------------------------------------------*)
     7.6  
     7.7 -goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)";
     7.8 -by (rtac allI 1);
     7.9 -by (rtac (surjective_pairing RS ssubst) 1);
    7.10 -by (Blast_tac 1);
    7.11 -qed "split_all_pair";
    7.12 -
    7.13  val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
    7.14   "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
    7.15 -by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
    7.16 +by (EVERY1 [rtac allI,rtac impI]);
    7.17 +by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1);
    7.18  by (rtac (wfa RS spec RS mp) 1);
    7.19  by (EVERY1 [rtac allI,rtac impI]);
    7.20  by (rtac (wfb RS spec RS mp) 1);
    7.21 @@ -80,25 +75,6 @@
    7.22  AddSIs [wf_lex_prod];
    7.23  
    7.24  (*---------------------------------------------------------------------------
    7.25 - * Wellfoundedness of subsets
    7.26 - *---------------------------------------------------------------------------*)
    7.27 -
    7.28 -goal thy "!!r. [| wf(r);  p<=r |] ==> wf(p)";
    7.29 -by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
    7.30 -by (Fast_tac 1);
    7.31 -qed "wf_subset";
    7.32 -
    7.33 -(*---------------------------------------------------------------------------
    7.34 - * Wellfoundedness of the empty relation.
    7.35 - *---------------------------------------------------------------------------*)
    7.36 -
    7.37 -goal thy "wf({})";
    7.38 -by (simp_tac (!simpset addsimps [wf_def]) 1);
    7.39 -qed "wf_empty";
    7.40 -AddSIs [wf_empty];
    7.41 -
    7.42 -
    7.43 -(*---------------------------------------------------------------------------
    7.44   * Transitivity of WF combinators.
    7.45   *---------------------------------------------------------------------------*)
    7.46  goalw thy [trans_def, lex_prod_def]
    7.47 @@ -124,3 +100,58 @@
    7.48  by (Blast_tac 1);
    7.49  qed "trans_finite_psubset";
    7.50  
    7.51 +(*---------------------------------------------------------------------------
    7.52 + * Wellfoundedness of finite acyclic relations
    7.53 + * Cannot go into WF because it needs Finite
    7.54 + *---------------------------------------------------------------------------*)
    7.55 +
    7.56 +goal thy "!!r. finite r ==> acyclic r --> wf r";
    7.57 +be finite_induct 1;
    7.58 + by(Blast_tac 1);
    7.59 +by(split_all_tac 1);
    7.60 +by(Asm_full_simp_tac 1);
    7.61 +qed_spec_mp "finite_acyclic_wf";
    7.62 +
    7.63 +goal thy "!!r. finite r ==> wf r = acyclic r";
    7.64 +by(blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
    7.65 +qed "wf_iff_acyclic_if_finite";
    7.66 +
    7.67 +
    7.68 +(*---------------------------------------------------------------------------
    7.69 + * A relation is wellfounded iff it has no infinite descending chain
    7.70 + *---------------------------------------------------------------------------*)
    7.71 +
    7.72 +goalw thy [wf_eq_minimal RS eq_reflection]
    7.73 +  "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
    7.74 +br iffI 1;
    7.75 + br notI 1;
    7.76 + be exE 1;
    7.77 + by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
    7.78 + by(Blast_tac 1);
    7.79 +be swap 1;
    7.80 +by(Asm_full_simp_tac 1);
    7.81 +be exE 1;
    7.82 +be swap 1;
    7.83 +br impI 1;
    7.84 +be swap 1;
    7.85 +be exE 1;
    7.86 +by(rename_tac "x" 1);
    7.87 +by(subgoal_tac
    7.88 + "!i. nat_rec x (%i y. @z. z:Q & (z,y):r) (Suc i) : Q & \
    7.89 +\     (nat_rec x (%i y. @z. z:Q & (z,y):r) (Suc i),\
    7.90 +\      nat_rec x (%i y. @z. z:Q & (z,y):r) i): r" 1);
    7.91 + by(Blast_tac 1);
    7.92 +br allI 1;
    7.93 +by(induct_tac "i" 1);
    7.94 + by(Asm_simp_tac 1);
    7.95 + by(subgoal_tac "? y. y : Q & (y,x):r" 1);
    7.96 +  by(Blast_tac 2);
    7.97 + be exE 1;
    7.98 + be selectI 1;
    7.99 +by(subgoal_tac "? y.y:Q & (y,nat_rec x (%i y. @z. z:Q & (z,y):r)(Suc i)):r" 1);
   7.100 + by(Blast_tac 2);
   7.101 +by(Asm_full_simp_tac 1);
   7.102 +be exE 1;
   7.103 +(* `be selectI 1' takes a long time; hence the instantiation: *)
   7.104 +by (eres_inst_tac[("P","%u.u:Q & (u,?v):r")]selectI 1);
   7.105 +qed "wf_iff_no_infinite_down_chain";