author wenzelm Wed, 17 May 2006 01:23:40 +0200 changeset 19669 95ac857276e1 parent 19668 6afaf300cb78 child 19670 2e4a143c73c5
tuned source/document;
```--- a/src/HOL/Accessible_Part.thy	Tue May 16 21:34:06 2006 +0200
+++ b/src/HOL/Accessible_Part.thy	Wed May 17 01:23:40 2006 +0200
@@ -76,48 +76,42 @@
done

-(* Smaller relations have bigger accessible parts: *)
+text {* Smaller relations have bigger accessible parts: *}
+
lemma acc_subset:
-  assumes sub:"R1 \<subseteq> R2"
+  assumes sub: "R1 \<subseteq> R2"
shows "acc R2 \<subseteq> acc R1"
proof
fix x assume "x \<in> acc R2"
-  thus "x \<in> acc R1"
-  proof (induct x) -- "acc-induction"
+  then show "x \<in> acc R1"
+  proof (induct x)
fix x
assume ih: "\<And>y. (y, x) \<in> R2 \<Longrightarrow> y \<in> acc R1"
-
with sub show "x \<in> acc R1"
by (blast intro:accI)
qed
qed

+text {* This is a generalized induction theorem that works on
+  subsets of the accessible part. *}

-(* This is a generalized induction theorem that works on
-    subsets of the accessible part. *)
lemma acc_subset_induct:
assumes subset: "D \<subseteq> acc R"
-  assumes dcl: "\<And>x z. \<lbrakk>x \<in> D; (z, x)\<in>R\<rbrakk> \<Longrightarrow> z \<in> D"
-
-  assumes "x \<in> D"
-  assumes istep: "\<And>x. \<lbrakk>x \<in> D; (\<And>z. (z, x)\<in>R \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
-shows "P x"
+    and dcl: "\<And>x z. \<lbrakk>x \<in> D; (z, x)\<in>R\<rbrakk> \<Longrightarrow> z \<in> D"
+    and "x \<in> D"
+    and istep: "\<And>x. \<lbrakk>x \<in> D; (\<And>z. (z, x)\<in>R \<Longrightarrow> P z)\<rbrakk> \<Longrightarrow> P x"
+  shows "P x"
proof -
from `x \<in> D` and subset
have "x \<in> acc R" ..
-
-  thus "P x" using `x \<in> D`
+  then show "P x" using `x \<in> D`
proof (induct x)
fix x
assume "x \<in> D"
and "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<in> D \<Longrightarrow> P y"
-
with dcl and istep show "P x" by blast
qed
qed

-
-
-
end```