remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
authorhuffman
Fri Dec 24 14:26:10 2010 -0800 (2010-12-24)
changeset 41402b647212cee03
parent 41401 e3ec82999306
child 41403 7eba049f7310
remove lemma ideal_completion.principal_induct2, use principal_induct twice instead
src/HOL/HOLCF/Completion.thy
src/HOL/HOLCF/ConvexPD.thy
src/HOL/HOLCF/LowerPD.thy
src/HOL/HOLCF/UpperPD.thy
     1.1 --- a/src/HOL/HOLCF/Completion.thy	Thu Dec 23 13:11:40 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Completion.thy	Fri Dec 24 14:26:10 2010 -0800
     1.3 @@ -271,16 +271,6 @@
     1.4  apply (simp add: admD [OF adm] P)
     1.5  done
     1.6  
     1.7 -lemma principal_induct2:
     1.8 -  "\<lbrakk>\<And>y. adm (\<lambda>x. P x y); \<And>x. adm (\<lambda>y. P x y);
     1.9 -    \<And>a b. P (principal a) (principal b)\<rbrakk> \<Longrightarrow> P x y"
    1.10 -apply (rule_tac x=y in spec)
    1.11 -apply (rule_tac x=x in principal_induct, simp)
    1.12 -apply (rule allI, rename_tac y)
    1.13 -apply (rule_tac x=y in principal_induct, simp)
    1.14 -apply simp
    1.15 -done
    1.16 -
    1.17  lemma compact_imp_principal: "compact x \<Longrightarrow> \<exists>a. x = principal a"
    1.18  apply (rule obtain_principal_chain [of x])
    1.19  apply (drule adm_compact_neq [OF _ cont_id])
     2.1 --- a/src/HOL/HOLCF/ConvexPD.thy	Thu Dec 23 13:11:40 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/ConvexPD.thy	Fri Dec 24 14:26:10 2010 -0800
     2.3 @@ -201,12 +201,14 @@
     2.4  interpretation convex_add: semilattice convex_add proof
     2.5    fix xs ys zs :: "'a convex_pd"
     2.6    show "(xs \<union>\<natural> ys) \<union>\<natural> zs = xs \<union>\<natural> (ys \<union>\<natural> zs)"
     2.7 -    apply (induct xs ys arbitrary: zs rule: convex_pd.principal_induct2, simp, simp)
     2.8 -    apply (rule_tac x=zs in convex_pd.principal_induct, simp)
     2.9 +    apply (induct xs rule: convex_pd.principal_induct, simp)
    2.10 +    apply (induct ys rule: convex_pd.principal_induct, simp)
    2.11 +    apply (induct zs rule: convex_pd.principal_induct, simp)
    2.12      apply (simp add: PDPlus_assoc)
    2.13      done
    2.14    show "xs \<union>\<natural> ys = ys \<union>\<natural> xs"
    2.15 -    apply (induct xs ys rule: convex_pd.principal_induct2, simp, simp)
    2.16 +    apply (induct xs rule: convex_pd.principal_induct, simp)
    2.17 +    apply (induct ys rule: convex_pd.principal_induct, simp)
    2.18      apply (simp add: PDPlus_commute)
    2.19      done
    2.20    show "xs \<union>\<natural> xs = xs"
    2.21 @@ -364,7 +366,8 @@
    2.22  
    2.23  lemma convex_bind_plus [simp]:
    2.24    "convex_bind\<cdot>(xs \<union>\<natural> ys)\<cdot>f = convex_bind\<cdot>xs\<cdot>f \<union>\<natural> convex_bind\<cdot>ys\<cdot>f"
    2.25 -by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
    2.26 +by (induct xs rule: convex_pd.principal_induct, simp,
    2.27 +    induct ys rule: convex_pd.principal_induct, simp, simp)
    2.28  
    2.29  lemma convex_bind_strict [simp]: "convex_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
    2.30  unfolding convex_unit_strict [symmetric] by (rule convex_bind_unit)
    2.31 @@ -537,7 +540,8 @@
    2.32  
    2.33  lemma convex_to_upper_plus [simp]:
    2.34    "convex_to_upper\<cdot>(xs \<union>\<natural> ys) = convex_to_upper\<cdot>xs \<union>\<sharp> convex_to_upper\<cdot>ys"
    2.35 -by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
    2.36 +by (induct xs rule: convex_pd.principal_induct, simp,
    2.37 +    induct ys rule: convex_pd.principal_induct, simp, simp)
    2.38  
    2.39  lemma convex_to_upper_bind [simp]:
    2.40    "convex_to_upper\<cdot>(convex_bind\<cdot>xs\<cdot>f) =
    2.41 @@ -576,7 +580,8 @@
    2.42  
    2.43  lemma convex_to_lower_plus [simp]:
    2.44    "convex_to_lower\<cdot>(xs \<union>\<natural> ys) = convex_to_lower\<cdot>xs \<union>\<flat> convex_to_lower\<cdot>ys"
    2.45 -by (induct xs ys rule: convex_pd.principal_induct2, simp, simp, simp)
    2.46 +by (induct xs rule: convex_pd.principal_induct, simp,
    2.47 +    induct ys rule: convex_pd.principal_induct, simp, simp)
    2.48  
    2.49  lemma convex_to_lower_bind [simp]:
    2.50    "convex_to_lower\<cdot>(convex_bind\<cdot>xs\<cdot>f) =
     3.1 --- a/src/HOL/HOLCF/LowerPD.thy	Thu Dec 23 13:11:40 2010 -0800
     3.2 +++ b/src/HOL/HOLCF/LowerPD.thy	Fri Dec 24 14:26:10 2010 -0800
     3.3 @@ -156,12 +156,14 @@
     3.4  interpretation lower_add: semilattice lower_add proof
     3.5    fix xs ys zs :: "'a lower_pd"
     3.6    show "(xs \<union>\<flat> ys) \<union>\<flat> zs = xs \<union>\<flat> (ys \<union>\<flat> zs)"
     3.7 -    apply (induct xs ys arbitrary: zs rule: lower_pd.principal_induct2, simp, simp)
     3.8 -    apply (rule_tac x=zs in lower_pd.principal_induct, simp)
     3.9 +    apply (induct xs rule: lower_pd.principal_induct, simp)
    3.10 +    apply (induct ys rule: lower_pd.principal_induct, simp)
    3.11 +    apply (induct zs rule: lower_pd.principal_induct, simp)
    3.12      apply (simp add: PDPlus_assoc)
    3.13      done
    3.14    show "xs \<union>\<flat> ys = ys \<union>\<flat> xs"
    3.15 -    apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
    3.16 +    apply (induct xs rule: lower_pd.principal_induct, simp)
    3.17 +    apply (induct ys rule: lower_pd.principal_induct, simp)
    3.18      apply (simp add: PDPlus_commute)
    3.19      done
    3.20    show "xs \<union>\<flat> xs = xs"
    3.21 @@ -185,7 +187,8 @@
    3.22    lower_plus_ac lower_plus_absorb lower_plus_left_absorb
    3.23  
    3.24  lemma lower_plus_below1: "xs \<sqsubseteq> xs \<union>\<flat> ys"
    3.25 -apply (induct xs ys rule: lower_pd.principal_induct2, simp, simp)
    3.26 +apply (induct xs rule: lower_pd.principal_induct, simp)
    3.27 +apply (induct ys rule: lower_pd.principal_induct, simp)
    3.28  apply (simp add: PDPlus_lower_le)
    3.29  done
    3.30  
    3.31 @@ -357,7 +360,8 @@
    3.32  
    3.33  lemma lower_bind_plus [simp]:
    3.34    "lower_bind\<cdot>(xs \<union>\<flat> ys)\<cdot>f = lower_bind\<cdot>xs\<cdot>f \<union>\<flat> lower_bind\<cdot>ys\<cdot>f"
    3.35 -by (induct xs ys rule: lower_pd.principal_induct2, simp, simp, simp)
    3.36 +by (induct xs rule: lower_pd.principal_induct, simp,
    3.37 +    induct ys rule: lower_pd.principal_induct, simp, simp)
    3.38  
    3.39  lemma lower_bind_strict [simp]: "lower_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
    3.40  unfolding lower_unit_strict [symmetric] by (rule lower_bind_unit)
     4.1 --- a/src/HOL/HOLCF/UpperPD.thy	Thu Dec 23 13:11:40 2010 -0800
     4.2 +++ b/src/HOL/HOLCF/UpperPD.thy	Fri Dec 24 14:26:10 2010 -0800
     4.3 @@ -154,12 +154,14 @@
     4.4  interpretation upper_add: semilattice upper_add proof
     4.5    fix xs ys zs :: "'a upper_pd"
     4.6    show "(xs \<union>\<sharp> ys) \<union>\<sharp> zs = xs \<union>\<sharp> (ys \<union>\<sharp> zs)"
     4.7 -    apply (induct xs ys arbitrary: zs rule: upper_pd.principal_induct2, simp, simp)
     4.8 -    apply (rule_tac x=zs in upper_pd.principal_induct, simp)
     4.9 +    apply (induct xs rule: upper_pd.principal_induct, simp)
    4.10 +    apply (induct ys rule: upper_pd.principal_induct, simp)
    4.11 +    apply (induct zs rule: upper_pd.principal_induct, simp)
    4.12      apply (simp add: PDPlus_assoc)
    4.13      done
    4.14    show "xs \<union>\<sharp> ys = ys \<union>\<sharp> xs"
    4.15 -    apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
    4.16 +    apply (induct xs rule: upper_pd.principal_induct, simp)
    4.17 +    apply (induct ys rule: upper_pd.principal_induct, simp)
    4.18      apply (simp add: PDPlus_commute)
    4.19      done
    4.20    show "xs \<union>\<sharp> xs = xs"
    4.21 @@ -183,7 +185,8 @@
    4.22    upper_plus_ac upper_plus_absorb upper_plus_left_absorb
    4.23  
    4.24  lemma upper_plus_below1: "xs \<union>\<sharp> ys \<sqsubseteq> xs"
    4.25 -apply (induct xs ys rule: upper_pd.principal_induct2, simp, simp)
    4.26 +apply (induct xs rule: upper_pd.principal_induct, simp)
    4.27 +apply (induct ys rule: upper_pd.principal_induct, simp)
    4.28  apply (simp add: PDPlus_upper_le)
    4.29  done
    4.30  
    4.31 @@ -240,12 +243,10 @@
    4.32  
    4.33  lemma upper_plus_bottom_iff [simp]:
    4.34    "xs \<union>\<sharp> ys = \<bottom> \<longleftrightarrow> xs = \<bottom> \<or> ys = \<bottom>"
    4.35 -apply (rule iffI)
    4.36 -apply (erule rev_mp)
    4.37 -apply (rule upper_pd.principal_induct2 [where x=xs and y=ys], simp, simp)
    4.38 +apply (induct xs rule: upper_pd.principal_induct, simp)
    4.39 +apply (induct ys rule: upper_pd.principal_induct, simp)
    4.40  apply (simp add: inst_upper_pd_pcpo upper_pd.principal_eq_iff
    4.41                   upper_le_PDPlus_PDUnit_iff)
    4.42 -apply auto
    4.43  done
    4.44  
    4.45  lemma compact_upper_unit: "compact x \<Longrightarrow> compact {x}\<sharp>"
    4.46 @@ -352,7 +353,8 @@
    4.47  
    4.48  lemma upper_bind_plus [simp]:
    4.49    "upper_bind\<cdot>(xs \<union>\<sharp> ys)\<cdot>f = upper_bind\<cdot>xs\<cdot>f \<union>\<sharp> upper_bind\<cdot>ys\<cdot>f"
    4.50 -by (induct xs ys rule: upper_pd.principal_induct2, simp, simp, simp)
    4.51 +by (induct xs rule: upper_pd.principal_induct, simp,
    4.52 +    induct ys rule: upper_pd.principal_induct, simp, simp)
    4.53  
    4.54  lemma upper_bind_strict [simp]: "upper_bind\<cdot>\<bottom>\<cdot>f = f\<cdot>\<bottom>"
    4.55  unfolding upper_unit_strict [symmetric] by (rule upper_bind_unit)