src/HOL/Wellfounded.thy
 changeset 32235 8f9b8d14fc9f parent 32205 49db434c157f child 32244 a99723d77ae0
1.1 --- a/src/HOL/Wellfounded.thy	Mon Jul 27 17:36:30 2009 +0200
1.2 +++ b/src/HOL/Wellfounded.thy	Mon Jul 27 21:47:41 2009 +0200
1.3 @@ -239,7 +239,7 @@
1.5  lemma wf_union_compatible:
1.6    assumes "wf R" "wf S"
1.7 -  assumes "S O R \<subseteq> R"
1.8 +  assumes "R O S \<subseteq> R"
1.9    shows "wf (R \<union> S)"
1.10  proof (rule wfI_min)
1.11    fix x :: 'a and Q
1.12 @@ -258,8 +258,8 @@
1.13        assume "y \<in> Q"
1.14        with `y \<notin> ?Q'`
1.15        obtain w where "(w, y) \<in> R" and "w \<in> Q" by auto
1.16 -      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> S O R" by (rule rel_compI)
1.17 -      with `S O R \<subseteq> R` have "(w, z) \<in> R" ..
1.18 +      from `(w, y) \<in> R` `(y, z) \<in> S` have "(w, z) \<in> R O S" by (rule rel_compI)
1.19 +      with `R O S \<subseteq> R` have "(w, z) \<in> R" ..
1.20        with `z \<in> ?Q'` have "w \<notin> Q" by blast
1.21        with `w \<in> Q` show False by contradiction
1.22      qed
1.23 @@ -312,7 +312,7 @@
1.24    by (auto simp: Un_ac)
1.26  lemma wf_union_merge:
1.27 -  "wf (R \<union> S) = wf (R O R \<union> R O S \<union> S)" (is "wf ?A = wf ?B")
1.28 +  "wf (R \<union> S) = wf (R O R \<union> S O R \<union> S)" (is "wf ?A = wf ?B")
1.29  proof
1.30    assume "wf ?A"
1.31    with wf_trancl have wfT: "wf (?A^+)" .
1.32 @@ -331,7 +331,7 @@
1.33      obtain z where "z \<in> Q" and "\<And>y. (y, z) \<in> ?B \<Longrightarrow> y \<notin> Q"
1.34        by (erule wfE_min)
1.35      then have A1: "\<And>y. (y, z) \<in> R O R \<Longrightarrow> y \<notin> Q"
1.36 -      and A2: "\<And>y. (y, z) \<in> R O S \<Longrightarrow> y \<notin> Q"
1.37 +      and A2: "\<And>y. (y, z) \<in> S O R \<Longrightarrow> y \<notin> Q"
1.38        and A3: "\<And>y. (y, z) \<in> S \<Longrightarrow> y \<notin> Q"
1.39        by auto
1.41 @@ -353,7 +353,7 @@
1.42            with A1 show "y \<notin> Q" .
1.43          next
1.44            assume "(y, z') \<in> S"
1.45 -          then have "(y, z) \<in> R O S" using  `(z', z) \<in> R` ..
1.46 +          then have "(y, z) \<in> S O R" using  `(z', z) \<in> R` ..
1.47            with A2 show "y \<notin> Q" .
1.48          qed
1.49        qed