src/HOLCF/CompactBasis.thy

 by (fast intro: compact_approx)
 
 lemma compact_Rep_compact_basis: "compact (Rep_compact_basis a)"
 by (rule Rep_compact_basis [unfolded mem_Collect_eq])
 
-instantiation compact_basis :: (profinite) sq_ord
+instantiation compact_basis :: (profinite) below
 begin
 
 definition
   compact_le_def:
     "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. Rep_compact_basis x \<sqsubseteq> Rep_compact_basis y)"

 by (simp add: Abs_compact_basis_inverse)
 
 lemmas approx_Rep_compact_basis = Rep_compact_take [symmetric]
 
 interpretation compact_basis:
-  basis_take sq_le compact_take
+  basis_take below compact_take
 proof
   fix n :: nat and a :: "'a compact_basis"
   show "compact_take n a \<sqsubseteq> a"
     unfolding compact_le_def
-    by (simp add: Rep_compact_take approx_less)
+    by (simp add: Rep_compact_take approx_below)
 next
   fix n :: nat and a :: "'a compact_basis"
   show "compact_take n (compact_take n a) = compact_take n a"
     by (simp add: Rep_compact_basis_inject [symmetric] Rep_compact_take)
 next

 definition
   approximants :: "'a \<Rightarrow> 'a compact_basis set" where
   "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
 
 interpretation compact_basis:
-  ideal_completion sq_le compact_take Rep_compact_basis approximants
+  ideal_completion below compact_take Rep_compact_basis approximants
 proof
   fix w :: 'a
-  show "preorder.ideal sq_le (approximants w)"
-  proof (rule sq_le.idealI)
+  show "preorder.ideal below (approximants w)"
+  proof (rule below.idealI)
     show "\<exists>x. x \<in> approximants w"
       unfolding approximants_def
       apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
-      apply (simp add: Abs_compact_basis_inverse approx_less)
+      apply (simp add: Abs_compact_basis_inverse approx_below)
       done
   next
     fix x y :: "'a compact_basis"
     assume "x \<in> approximants w" "y \<in> approximants w"
     thus "\<exists>z \<in> approximants w. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"

       apply (drule profinite_compact_eq_approx)
       apply (drule profinite_compact_eq_approx)
       apply (clarify, rename_tac i j)
       apply (rule_tac x="Abs_compact_basis (approx (max i j)\<cdot>w)" in exI)
       apply (simp add: compact_le_def)
-      apply (simp add: Abs_compact_basis_inverse approx_less)
+      apply (simp add: Abs_compact_basis_inverse approx_below)
       apply (erule subst, erule subst)
       apply (simp add: monofun_cfun chain_mono [OF chain_approx])
       done
   next
     fix x y :: "'a compact_basis"
     assume "x \<sqsubseteq> y" "y \<in> approximants w" thus "x \<in> approximants w"
       unfolding approximants_def
       apply simp
       apply (simp add: compact_le_def)
-      apply (erule (1) trans_less)
+      apply (erule (1) below_trans)
       done
   qed
 next
   fix Y :: "nat \<Rightarrow> 'a"
   assume Y: "chain Y"
   show "approximants (\<Squnion>i. Y i) = (\<Union>i. approximants (Y i))"
     unfolding approximants_def
     apply safe
     apply (simp add: compactD2 [OF compact_Rep_compact_basis Y])
-    apply (erule trans_less, rule is_ub_thelub [OF Y])
+    apply (erule below_trans, rule is_ub_thelub [OF Y])
     done
 next
   fix a :: "'a compact_basis"
   show "approximants (Rep_compact_basis a) = {b. b \<sqsubseteq> a}"
     unfolding approximants_def compact_le_def ..

   fix x y :: "'a"
   assume "approximants x \<subseteq> approximants y" thus "x \<sqsubseteq> y"
     apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> y", simp)
     apply (rule admD, simp, simp)
     apply (drule_tac c="Abs_compact_basis (approx i\<cdot>x)" in subsetD)
-    apply (simp add: approximants_def Abs_compact_basis_inverse approx_less)
+    apply (simp add: approximants_def Abs_compact_basis_inverse approx_below)
     apply (simp add: approximants_def Abs_compact_basis_inverse)
     done
 qed
 
 text {* minimal compact element *}

 apply (subgoal_tac "\<exists>n. \<forall>m\<ge>n. pd_take m t = t", fast)
 apply (induct t rule: pd_basis_induct)
 apply (cut_tac a=a in compact_basis.take_covers)
 apply (clarify, rule_tac x=n in exI)
 apply (clarify, simp)
-apply (rule antisym_less)
+apply (rule below_antisym)
 apply (rule compact_basis.take_less)
 apply (drule_tac a=a in compact_basis.take_chain_le)
 apply simp
 apply (clarify, rename_tac i j)
 apply (rule_tac x="max i j" in exI, simp)