# HG changeset patch
# User Brian Huffman <brianh@cs.pdx.edu>
# Date 1286323677 25200
# Node ID 9023b897e67a6599531a9f0f8775dc569538a720
# Parent  0b8e19f588a472701183a1322b95286ecb55874a
simplify proofs of powerdomain inequalities

diff -r 0b8e19f588a4 -r 9023b897e67a src/HOLCF/ConvexPD.thy
--- a/src/HOLCF/ConvexPD.thy	Mon Oct 04 06:58:37 2010 -0700
+++ b/src/HOLCF/ConvexPD.thy	Tue Oct 05 17:07:57 2010 -0700
@@ -312,48 +312,24 @@
 
 lemma convex_unit_below_plus_iff [simp]:
   "{x}\<natural> \<sqsubseteq> ys +\<natural> zs \<longleftrightarrow> {x}\<natural> \<sqsubseteq> ys \<and> {x}\<natural> \<sqsubseteq> zs"
- apply (rule iffI)
-  apply (subgoal_tac
-    "adm (\<lambda>f. f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>ys \<and> f\<cdot>{x}\<natural> \<sqsubseteq> f\<cdot>zs)")
-   apply (drule admD, rule chain_approx)
-    apply (drule_tac f="approx i" in monofun_cfun_arg)
-    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
-    apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
-    apply (cut_tac x="approx i\<cdot>zs" in convex_pd.compact_imp_principal, simp)
-    apply (clarify, simp)
-   apply simp
-  apply simp
- apply (erule conjE)
- apply (subst convex_plus_absorb [of "{x}\<natural>", symmetric])
- apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
+apply (induct x rule: compact_basis.principal_induct, simp)
+apply (induct ys rule: convex_pd.principal_induct, simp)
+apply (induct zs rule: convex_pd.principal_induct, simp)
+apply simp
 done
 
 lemma convex_plus_below_unit_iff [simp]:
   "xs +\<natural> ys \<sqsubseteq> {z}\<natural> \<longleftrightarrow> xs \<sqsubseteq> {z}\<natural> \<and> ys \<sqsubseteq> {z}\<natural>"
- apply (rule iffI)
-  apply (subgoal_tac
-    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<natural> \<and> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<natural>)")
-   apply (drule admD, rule chain_approx)
-    apply (drule_tac f="approx i" in monofun_cfun_arg)
-    apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
-    apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
-    apply (cut_tac x="approx i\<cdot>z" in compact_basis.compact_imp_principal, simp)
-    apply (clarify, simp)
-   apply simp
-  apply simp
- apply (erule conjE)
- apply (subst convex_plus_absorb [of "{z}\<natural>", symmetric])
- apply (erule (1) monofun_cfun [OF monofun_cfun_arg])
+apply (induct xs rule: convex_pd.principal_induct, simp)
+apply (induct ys rule: convex_pd.principal_induct, simp)
+apply (induct z rule: compact_basis.principal_induct, simp)
+apply simp
 done
 
 lemma convex_unit_below_iff [simp]: "{x}\<natural> \<sqsubseteq> {y}\<natural> \<longleftrightarrow> x \<sqsubseteq> y"
- apply (rule iffI)
-  apply (rule profinite_below_ext)
-  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
-  apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
-  apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
-  apply clarsimp
- apply (erule monofun_cfun_arg)
+apply (induct x rule: compact_basis.principal_induct, simp)
+apply (induct y rule: compact_basis.principal_induct, simp)
+apply simp
 done
 
 lemma convex_unit_eq_iff [simp]: "{x}\<natural> = {y}\<natural> \<longleftrightarrow> x = y"
@@ -627,14 +603,9 @@
   "(xs \<sqsubseteq> ys) =
     (convex_to_upper\<cdot>xs \<sqsubseteq> convex_to_upper\<cdot>ys \<and>
      convex_to_lower\<cdot>xs \<sqsubseteq> convex_to_lower\<cdot>ys)"
- apply (safe elim!: monofun_cfun_arg)
- apply (rule profinite_below_ext)
- apply (drule_tac f="approx i" in monofun_cfun_arg)
- apply (drule_tac f="approx i" in monofun_cfun_arg)
- apply (cut_tac x="approx i\<cdot>xs" in convex_pd.compact_imp_principal, simp)
- apply (cut_tac x="approx i\<cdot>ys" in convex_pd.compact_imp_principal, simp)
- apply clarify
- apply (simp add: approx_convex_to_upper approx_convex_to_lower convex_le_def)
+apply (induct xs rule: convex_pd.principal_induct, simp)
+apply (induct ys rule: convex_pd.principal_induct, simp)
+apply (simp add: convex_le_def)
 done
 
 lemmas convex_plus_below_plus_iff =
diff -r 0b8e19f588a4 -r 9023b897e67a src/HOLCF/LowerPD.thy
--- a/src/HOLCF/LowerPD.thy	Mon Oct 04 06:58:37 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Tue Oct 05 17:07:57 2010 -0700
@@ -288,30 +288,16 @@
 
 lemma lower_unit_below_plus_iff:
   "{x}\<flat> \<sqsubseteq> ys +\<flat> zs \<longleftrightarrow> {x}\<flat> \<sqsubseteq> ys \<or> {x}\<flat> \<sqsubseteq> zs"
- apply (rule iffI)
-  apply (subgoal_tac
-    "adm (\<lambda>f. f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>ys \<or> f\<cdot>{x}\<flat> \<sqsubseteq> f\<cdot>zs)")
-   apply (drule admD, rule chain_approx)
-    apply (drule_tac f="approx i" in monofun_cfun_arg)
-    apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
-    apply (cut_tac x="approx i\<cdot>ys" in lower_pd.compact_imp_principal, simp)
-    apply (cut_tac x="approx i\<cdot>zs" in lower_pd.compact_imp_principal, simp)
-    apply (clarify, simp add: lower_le_PDUnit_PDPlus_iff)
-   apply simp
-  apply simp
- apply (erule disjE)
-  apply (erule below_trans [OF _ lower_plus_below1])
- apply (erule below_trans [OF _ lower_plus_below2])
+apply (induct x rule: compact_basis.principal_induct, simp)
+apply (induct ys rule: lower_pd.principal_induct, simp)
+apply (induct zs rule: lower_pd.principal_induct, simp)
+apply (simp add: lower_le_PDUnit_PDPlus_iff)
 done
 
 lemma lower_unit_below_iff [simp]: "{x}\<flat> \<sqsubseteq> {y}\<flat> \<longleftrightarrow> x \<sqsubseteq> y"
- apply (rule iffI)
-  apply (rule profinite_below_ext)
-  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
-  apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
-  apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
-  apply clarsimp
- apply (erule monofun_cfun_arg)
+apply (induct x rule: compact_basis.principal_induct, simp)
+apply (induct y rule: compact_basis.principal_induct, simp)
+apply simp
 done
 
 lemmas lower_pd_below_simps =
diff -r 0b8e19f588a4 -r 9023b897e67a src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Mon Oct 04 06:58:37 2010 -0700
+++ b/src/HOLCF/UpperPD.thy	Tue Oct 05 17:07:57 2010 -0700
@@ -286,30 +286,16 @@
 
 lemma upper_plus_below_unit_iff:
   "xs +\<sharp> ys \<sqsubseteq> {z}\<sharp> \<longleftrightarrow> xs \<sqsubseteq> {z}\<sharp> \<or> ys \<sqsubseteq> {z}\<sharp>"
- apply (rule iffI)
-  apply (subgoal_tac
-    "adm (\<lambda>f. f\<cdot>xs \<sqsubseteq> f\<cdot>{z}\<sharp> \<or> f\<cdot>ys \<sqsubseteq> f\<cdot>{z}\<sharp>)")
-   apply (drule admD, rule chain_approx)
-    apply (drule_tac f="approx i" in monofun_cfun_arg)
-    apply (cut_tac x="approx i\<cdot>xs" in upper_pd.compact_imp_principal, simp)
-    apply (cut_tac x="approx i\<cdot>ys" in upper_pd.compact_imp_principal, simp)
-    apply (cut_tac x="approx i\<cdot>z" in compact_basis.compact_imp_principal, simp)
-    apply (clarify, simp add: upper_le_PDPlus_PDUnit_iff)
-   apply simp
-  apply simp
- apply (erule disjE)
-  apply (erule below_trans [OF upper_plus_below1])
- apply (erule below_trans [OF upper_plus_below2])
+apply (induct xs rule: upper_pd.principal_induct, simp)
+apply (induct ys rule: upper_pd.principal_induct, simp)
+apply (induct z rule: compact_basis.principal_induct, simp)
+apply (simp add: upper_le_PDPlus_PDUnit_iff)
 done
 
 lemma upper_unit_below_iff [simp]: "{x}\<sharp> \<sqsubseteq> {y}\<sharp> \<longleftrightarrow> x \<sqsubseteq> y"
- apply (rule iffI)
-  apply (rule profinite_below_ext)
-  apply (drule_tac f="approx i" in monofun_cfun_arg, simp)
-  apply (cut_tac x="approx i\<cdot>x" in compact_basis.compact_imp_principal, simp)
-  apply (cut_tac x="approx i\<cdot>y" in compact_basis.compact_imp_principal, simp)
-  apply clarsimp
- apply (erule monofun_cfun_arg)
+apply (induct x rule: compact_basis.principal_induct, simp)
+apply (induct y rule: compact_basis.principal_induct, simp)
+apply simp
 done
 
 lemmas upper_pd_below_simps =