src/HOLCF/Sum_Cpo.thy

 imports Bifinite
 begin
 
 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 Inr_less_iff [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
-unfolding less_sum_def by simp
-
-lemma Inl_less_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
-unfolding less_sum_def by simp
-
-lemma Inr_less_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl 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_below_Inr [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
+unfolding below_sum_def by simp
+
+lemma Inl_below_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
+unfolding below_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
 
 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
-
-lemma sum_less_cases:
+lemmas sum_below_elims = Inl_belowE Inr_belowE
+
+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 *}
 
 instance "+" :: (po, po) po
 proof

   show "x \<sqsubseteq> x"
     by (induct x, simp_all)
 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"
   assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R"
   assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R"

  apply (cases "Y 0")
   apply (rule A)
    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"
  apply (rule is_lubI)
   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)
 done
 
 lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
  apply (rule is_lubI)
   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)
 done
 

 done
 
 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 *}
 
 instantiation "+" :: (profinite, profinite) profinite
 begin