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.4  
     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.25  
    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.40      
    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