# HG changeset patch
# User huffman
# Date 1293229570 28800
# Node ID b647212cee032ec0fda8c7d605ad71bd320f08f7
# Parent  e3ec82999306f8154d79200588c946cdee9213a8
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead

diff -r e3ec82999306 -r b647212cee03 src/HOL/HOLCF/Completion.thy
--- a/src/HOL/HOLCF/Completion.thy	Thu Dec 23 13:11:40 2010 -0800
+++ b/src/HOL/HOLCF/Completion.thy	Fri Dec 24 14:26:10 2010 -0800
@@ -271,16 +271,6 @@
 apply (simp add: admD [OF adm] P)
 done
 
-lemma principal_induct2:
-  "\<lbrakk>\<And>y. adm (\<lambda>x. P x y); \<And>x. adm (\<lambda>y. P x y);
-    \<And>a b. P (principal a) (principal b)\<rbrakk> \<Longrightarrow> P x y"
-apply (rule_tac x=y in spec)
-apply (rule_tac x=x in principal_induct, simp)
-apply (rule allI, rename_tac y)
-apply (rule_tac x=y in principal_induct, simp)
-apply simp
-done
-
 lemma compact_imp_principal: "compact x \<Longrightarrow> \<exists>a. x = principal a"
 apply (rule obtain_principal_chain [of x])
 apply (drule adm_compact_neq [OF _ cont_id])
diff -r e3ec82999306 -r b647212cee03 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Thu Dec 23 13:11:40 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Fri Dec 24 14:26:10 2010 -0800
@@ -201,12 +201,14 @@
 interpretation convex_add: semilattice convex_add proof
   fix xs ys zs :: "'a convex_pd"
   show "(xs \<union>\<natural> ys) \<union>\<natural> zs = xs \<union>\<natural> (ys \<union>\<natural> zs)"
-    apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
-    apply (rule_tac x=zs in convex_pd.principal_induct, simp)
+    apply (induct xs rule: convex_pd.principal_induct, simp)
+    apply (induct ys rule: convex_pd.principal_induct, simp)
+    apply (induct zs rule: convex_pd.principal_induct, simp)
     apply (simp add: PDPlus_assoc)
     done
   show "xs \<union>\<natural> ys = ys \<union>\<natural> xs"
-    apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
+    apply (induct xs rule: convex_pd.principal_induct, simp)
+    apply (induct ys rule: convex_pd.principal_induct, simp)
     apply (simp add: PDPlus_commute)
     done
   show "xs \<union>\<natural> xs = xs"
@@ -364,7 +366,8 @@
 
 lemma convex_bind_plus [simp]:
   "convex_bind\<cdot>(xs \<union>\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f \<union>\<natural> convex_bind\<cdot>ys\<cdot>f"
-by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
+by (induct xs rule: convex_pd.principal_induct, simp,
+    induct ys rule: convex_pd.principal_induct, simp, simp)
 
 lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
 unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit)
@@ -537,7 +540,8 @@
 
 lemma convex_to_upper_plus [simp]:
   "convex_to_upper\<cdot>(xs \<union>\<natural> ys) = convex_to_upper\<cdot>xs \<union>\<sharp> convex_to_upper\<cdot>ys"
-by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
+by (induct xs rule: convex_pd.principal_induct, simp,
+    induct ys rule: convex_pd.principal_induct, simp, simp)
 
 lemma convex_to_upper_bind [simp]:
   "convex_to_upper\<cdot>(convex_bind\<cdot>xs\<cdot>f) =
@@ -576,7 +580,8 @@
 
 lemma convex_to_lower_plus [simp]:
   "convex_to_lower\<cdot>(xs \<union>\<natural> ys) = convex_to_lower\<cdot>xs \<union>\<flat> convex_to_lower\<cdot>ys"
-by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
+by (induct xs rule: convex_pd.principal_induct, simp,
+    induct ys rule: convex_pd.principal_induct, simp, simp)
 
 lemma convex_to_lower_bind [simp]:
   "convex_to_lower\<cdot>(convex_bind\<cdot>xs\<cdot>f) =
diff -r e3ec82999306 -r b647212cee03 src/HOL/HOLCF/LowerPD.thy
--- 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)
diff -r e3ec82999306 -r b647212cee03 src/HOL/HOLCF/UpperPD.thy
--- a/src/HOL/HOLCF/UpperPD.thy	Thu Dec 23 13:11:40 2010 -0800
+++ b/src/HOL/HOLCF/UpperPD.thy	Fri Dec 24 14:26:10 2010 -0800
@@ -154,12 +154,14 @@
 interpretation upper_add: semilattice upper_add proof
   fix xs ys zs :: "'a upper_pd"
   show "(xs \<union>\<sharp> ys) \<union>\<sharp> zs = xs \<union>\<sharp> (ys \<union>\<sharp> zs)"
-    apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
-    apply (rule_tac x=zs in upper_pd.principal_induct, simp)
+    apply (induct xs rule: upper_pd.principal_induct, simp)
+    apply (induct ys rule: upper_pd.principal_induct, simp)
+    apply (induct zs rule: upper_pd.principal_induct, simp)
     apply (simp add: PDPlus_assoc)
     done
   show "xs \<union>\<sharp> ys = ys \<union>\<sharp> xs"
-    apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
+    apply (induct xs rule: upper_pd.principal_induct, simp)
+    apply (induct ys rule: upper_pd.principal_induct, simp)
     apply (simp add: PDPlus_commute)
     done
   show "xs \<union>\<sharp> xs = xs"
@@ -183,7 +185,8 @@
   upper_plus_ac upper_plus_absorb upper_plus_left_absorb
 
 lemma upper_plus_below1: "xs \<union>\<sharp> ys \<sqsubseteq> xs"
-apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
+apply (induct xs rule: upper_pd.principal_induct, simp)
+apply (induct ys rule: upper_pd.principal_induct, simp)
 apply (simp add: PDPlus_upper_le)
 done
 
@@ -240,12 +243,10 @@
 
 lemma upper_plus_bottom_iff [simp]:
   "xs \<union>\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
-apply (rule iffI)
-apply (erule rev_mp)
-apply (rule upper_pd.principal_induct2 [where x=xs and y=ys], simp, simp)
+apply (induct xs rule: upper_pd.principal_induct, simp)
+apply (induct ys rule: upper_pd.principal_induct, simp)
 apply (simp add: inst_upper_pd_pcpo upper_pd.principal_eq_iff
                  upper_le_PDPlus_PDUnit_iff)
-apply auto
 done
 
 lemma compact_upper_unit: "compact x \<Longrightarrow> compact {x}\<sharp>"
@@ -352,7 +353,8 @@
 
 lemma upper_bind_plus [simp]:
   "upper_bind\<cdot>(xs \<union>\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f \<union>\<sharp> upper_bind\<cdot>ys\<cdot>f"
-by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
+by (induct xs rule: upper_pd.principal_induct, simp,
+    induct ys rule: upper_pd.principal_induct, simp, simp)
 
 lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
 unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit)