src/HOLCF/Sum_Cpo.thy

--- a/src/HOLCF/Sum_Cpo.thy	Fri May 08 19:28:11 2009 +0100
+++ b/src/HOLCF/Sum_Cpo.thy	Fri May 08 16:19:51 2009 -0700
@@ -10,28 +10,28 @@
 
 subsection {* Ordering on type @{typ "'a + 'b"} *}
 
-instantiation "+" :: (sq_ord, sq_ord) sq_ord
+instantiation "+" :: (below, below) below
 begin
 
-definition
-  less_sum_def: "x \<sqsubseteq> y \<equiv> case x of
+definition below_sum_def:
+  "x \<sqsubseteq> y \<equiv> case x of
          Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
          Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
 
 instance ..
 end
 
-lemma Inl_less_iff [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
-unfolding less_sum_def by simp
+lemma Inl_below_Inl [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
+unfolding below_sum_def by simp
 
-lemma Inr_less_iff [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
-unfolding less_sum_def by simp
+lemma Inr_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
+unfolding below_sum_def by simp
 
-lemma Inl_less_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
-unfolding less_sum_def by simp
+lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
+unfolding below_sum_def by simp
 
-lemma Inr_less_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
-unfolding less_sum_def by simp
+lemma Inr_below_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
+unfolding below_sum_def by simp
 
 lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
 by simp
@@ -39,20 +39,20 @@
 lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
 by simp
 
-lemma Inl_lessE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+lemma Inl_belowE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
 by (cases x, simp_all)
 
-lemma Inr_lessE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+lemma Inr_belowE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
 by (cases x, simp_all)
 
-lemmas sum_less_elims = Inl_lessE Inr_lessE
+lemmas sum_below_elims = Inl_belowE Inr_belowE
 
-lemma sum_less_cases:
+lemma sum_below_cases:
   "\<lbrakk>x \<sqsubseteq> y;
     \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
     \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
       \<Longrightarrow> R"
-by (cases x, safe elim!: sum_less_elims, auto)
+by (cases x, safe elim!: sum_below_elims, auto)
 
 subsection {* Sum type is a complete partial order *}
 
@@ -64,18 +64,18 @@
 next
   fix x y :: "'a + 'b"
   assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
-    by (induct x, auto elim!: sum_less_elims intro: antisym_less)
+    by (induct x, auto elim!: sum_below_elims intro: below_antisym)
 next
   fix x y z :: "'a + 'b"
   assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
-    by (induct x, auto elim!: sum_less_elims intro: trans_less)
+    by (induct x, auto elim!: sum_below_elims intro: below_trans)
 qed
 
 lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
-by (rule monofunI, erule sum_less_cases, simp_all)
+by (rule monofunI, erule sum_below_cases, simp_all)
 
 lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
-by (rule monofunI, erule sum_less_cases, simp_all)
+by (rule monofunI, erule sum_below_cases, simp_all)
 
 lemma sum_chain_cases:
   assumes Y: "chain Y"
@@ -87,12 +87,12 @@
    apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
   apply (rule ext)
   apply (cut_tac j=i in chain_mono [OF Y le0], simp)
-  apply (erule Inl_lessE, simp)
+  apply (erule Inl_belowE, simp)
  apply (rule B)
   apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
  apply (rule ext)
  apply (cut_tac j=i in chain_mono [OF Y le0], simp)
- apply (erule Inr_lessE, simp)
+ apply (erule Inr_belowE, simp)
 done
 
 lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
@@ -100,7 +100,7 @@
   apply (rule ub_rangeI)
   apply (simp add: is_ub_lub)
  apply (frule ub_rangeD [where i=arbitrary])
- apply (erule Inl_lessE, simp)
+ apply (erule Inl_belowE, simp)
  apply (erule is_lub_lub)
  apply (rule ub_rangeI)
  apply (drule ub_rangeD, simp)
@@ -111,7 +111,7 @@
   apply (rule ub_rangeI)
   apply (simp add: is_ub_lub)
  apply (frule ub_rangeD [where i=arbitrary])
- apply (erule Inr_lessE, simp)
+ apply (erule Inr_belowE, simp)
  apply (erule is_lub_lub)
  apply (rule ub_rangeI)
  apply (drule ub_rangeD, simp)
@@ -226,7 +226,7 @@
 instance "+" :: (finite_po, finite_po) finite_po ..
 
 instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
-by intro_classes (simp add: less_sum_def split: sum.split)
+by intro_classes (simp add: below_sum_def split: sum.split)
 
 subsection {* Sum type is a bifinite domain *}