--- a/src/HOL/HOLCF/LowerPD.thy Thu Dec 23 13:11:40 2010 -0800
+++ b/src/HOL/HOLCF/LowerPD.thy Fri Dec 24 14:26:10 2010 -0800
@@ -156,12 +156,14 @@
interpretation lower_add: semilattice lower_add proof
fix xs ys zs :: "'a lower_pd"
show "(xs \<union>\<flat> ys) \<union>\<flat> zs = xs \<union>\<flat> (ys \<union>\<flat> zs)"
- apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
- apply (rule_tac x=zs in lower_pd.principal_induct, simp)
+ apply (induct xs rule: lower_pd.principal_induct, simp)
+ apply (induct ys rule: lower_pd.principal_induct, simp)
+ apply (induct zs rule: lower_pd.principal_induct, simp)
apply (simp add: PDPlus_assoc)
done
show "xs \<union>\<flat> ys = ys \<union>\<flat> xs"
- apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
+ apply (induct xs rule: lower_pd.principal_induct, simp)
+ apply (induct ys rule: lower_pd.principal_induct, simp)
apply (simp add: PDPlus_commute)
done
show "xs \<union>\<flat> xs = xs"
@@ -185,7 +187,8 @@
lower_plus_ac lower_plus_absorb lower_plus_left_absorb
lemma lower_plus_below1: "xs \<sqsubseteq> xs \<union>\<flat> ys"
-apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
+apply (induct xs rule: lower_pd.principal_induct, simp)
+apply (induct ys rule: lower_pd.principal_induct, simp)
apply (simp add: PDPlus_lower_le)
done
@@ -357,7 +360,8 @@
lemma lower_bind_plus [simp]:
"lower_bind\<cdot>(xs \<union>\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f \<union>\<flat> lower_bind\<cdot>ys\<cdot>f"
-by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
+by (induct xs rule: lower_pd.principal_induct, simp,
+ induct ys rule: lower_pd.principal_induct, simp, simp)
lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit)