# HG changeset patch
# User huffman
# Date 1213823250 -7200
# Node ID 1d8c6703c7b11a8a8d72b8943f76f6730dd20da4
# Parent  5ebfb7f25ebb40926402d23eb5f9e377714fd35a
replace preorder class with locale

diff -r 5ebfb7f25ebb -r 1d8c6703c7b1 src/HOLCF/CompactBasis.thy
--- a/src/HOLCF/CompactBasis.thy	Wed Jun 18 23:03:11 2008 +0200
+++ b/src/HOLCF/CompactBasis.thy	Wed Jun 18 23:07:30 2008 +0200
@@ -11,18 +11,21 @@
 
 subsection {* Ideals over a preorder *}
 
-context preorder
+locale preorder =
+  fixes r :: "'a::type \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<preceq>" 50)
+  assumes r_refl: "x \<preceq> x"
+  assumes r_trans: "\<lbrakk>x \<preceq> y; y \<preceq> z\<rbrakk> \<Longrightarrow> x \<preceq> z"
 begin
 
 definition
   ideal :: "'a set \<Rightarrow> bool" where
-  "ideal A = ((\<exists>x. x \<in> A) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<exists>z\<in>A. x \<sqsubseteq> z \<and> y \<sqsubseteq> z) \<and>
-    (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> y \<in> A \<longrightarrow> x \<in> A))"
+  "ideal A = ((\<exists>x. x \<in> A) \<and> (\<forall>x\<in>A. \<forall>y\<in>A. \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z) \<and>
+    (\<forall>x y. x \<preceq> y \<longrightarrow> y \<in> A \<longrightarrow> x \<in> A))"
 
 lemma idealI:
   assumes "\<exists>x. x \<in> A"
-  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
-  assumes "\<And>x y. \<lbrakk>x \<sqsubseteq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
+  assumes "\<And>x y. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z"
+  assumes "\<And>x y. \<lbrakk>x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
   shows "ideal A"
 unfolding ideal_def using prems by fast
 
@@ -31,36 +34,39 @@
 unfolding ideal_def by fast
 
 lemma idealD2:
-  "\<lbrakk>ideal A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
+  "\<lbrakk>ideal A; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. x \<preceq> z \<and> y \<preceq> z"
 unfolding ideal_def by fast
 
 lemma idealD3:
-  "\<lbrakk>ideal A; x \<sqsubseteq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
+  "\<lbrakk>ideal A; x \<preceq> y; y \<in> A\<rbrakk> \<Longrightarrow> x \<in> A"
 unfolding ideal_def by fast
 
 lemma ideal_directed_finite:
   assumes A: "ideal A"
-  shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. x \<sqsubseteq> z"
+  shows "\<lbrakk>finite U; U \<subseteq> A\<rbrakk> \<Longrightarrow> \<exists>z\<in>A. \<forall>x\<in>U. x \<preceq> z"
 apply (induct U set: finite)
 apply (simp add: idealD1 [OF A])
 apply (simp, clarify, rename_tac y)
 apply (drule (1) idealD2 [OF A])
 apply (clarify, erule_tac x=z in rev_bexI)
-apply (fast intro: trans_less)
+apply (fast intro: r_trans)
 done
 
-lemma ideal_principal: "ideal {x. x \<sqsubseteq> z}"
+lemma ideal_principal: "ideal {x. x \<preceq> z}"
 apply (rule idealI)
 apply (rule_tac x=z in exI)
-apply fast
+apply (fast intro: r_refl)
 apply (rule_tac x=z in bexI, fast)
-apply fast
-apply (fast intro: trans_less)
+apply (fast intro: r_refl)
+apply (fast intro: r_trans)
 done
 
+lemma ex_ideal: "\<exists>A. ideal A"
+by (rule exI, rule ideal_principal)
+
 lemma directed_image_ideal:
   assumes A: "ideal A"
-  assumes f: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+  assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   shows "directed (f ` A)"
 apply (rule directedI)
 apply (cut_tac idealD1 [OF A], fast)
@@ -76,18 +82,24 @@
 unfolding ideal_def by (intro adm_lemmas adm_set_lemmas)
 
 lemma lub_image_principal:
-  assumes f: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-  shows "(\<Squnion>x\<in>{x. x \<sqsubseteq> y}. f x) = f y"
+  assumes f: "\<And>x y. x \<preceq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+  shows "(\<Squnion>x\<in>{x. x \<preceq> y}. f x) = f y"
 apply (rule thelubI)
 apply (rule is_lub_maximal)
 apply (rule ub_imageI)
 apply (simp add: f)
 apply (rule imageI)
-apply simp
+apply (simp add: r_refl)
 done
 
 end
 
+interpretation sq_le: preorder ["sq_le :: 'a::po \<Rightarrow> 'a \<Rightarrow> bool"]
+apply unfold_locales
+apply (rule refl_less)
+apply (erule (1) trans_less)
+done
+
 subsection {* Defining functions in terms of basis elements *}
 
 lemma finite_directed_contains_lub:
@@ -116,21 +128,21 @@
 lemma is_lub_thelub0: "\<lbrakk>\<exists>u. S <<| u; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> x"
 by (erule exE, drule lubI, erule is_lub_lub)
 
-locale basis_take = preorder r +
+locale basis_take = preorder +
   fixes take :: "nat \<Rightarrow> 'a::type \<Rightarrow> 'a"
-  assumes take_less: "r (take n a) a"
+  assumes take_less: "take n a \<preceq> a"
   assumes take_take: "take n (take n a) = take n a"
-  assumes take_mono: "r a b \<Longrightarrow> r (take n a) (take n b)"
-  assumes take_chain: "r (take n a) (take (Suc n) a)"
+  assumes take_mono: "a \<preceq> b \<Longrightarrow> take n a \<preceq> take n b"
+  assumes take_chain: "take n a \<preceq> take (Suc n) a"
   assumes finite_range_take: "finite (range (take n))"
   assumes take_covers: "\<exists>n. take n a = a"
 
-locale ideal_completion = basis_take r +
+locale ideal_completion = basis_take +
   fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
   fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
   assumes ideal_rep: "\<And>x. preorder.ideal r (rep x)"
   assumes cont_rep: "cont rep"
-  assumes rep_principal: "\<And>a. rep (principal a) = {b. r b a}"
+  assumes rep_principal: "\<And>a. rep (principal a) = {b. b \<preceq> a}"
   assumes subset_repD: "\<And>x y. rep x \<subseteq> rep y \<Longrightarrow> x \<sqsubseteq> y"
 begin
 
@@ -139,7 +151,7 @@
 
 lemma basis_fun_lemma0:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
-  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
+  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "\<exists>u. f ` take i ` rep x <<| u"
 apply (rule finite_directed_has_lub)
 apply (rule finite_imageI)
@@ -153,7 +165,7 @@
 
 lemma basis_fun_lemma1:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
-  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
+  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "chain (\<lambda>i. lub (f ` take i ` rep x))"
  apply (rule chainI)
  apply (rule is_lub_thelub0)
@@ -167,7 +179,7 @@
 
 lemma basis_fun_lemma2:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
-  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
+  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "f ` rep x <<| (\<Squnion>i. lub (f ` take i ` rep x))"
  apply (rule is_lubI)
  apply (rule ub_imageI, rename_tac a)
@@ -190,7 +202,7 @@
 
 lemma basis_fun_lemma:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
-  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
+  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "\<exists>u. f ` rep x <<| u"
 by (rule exI, rule basis_fun_lemma2, erule f_mono)
 
@@ -210,7 +222,7 @@
 unfolding less_def rep_principal
 apply safe
 apply (erule (1) idealD3 [OF ideal_rep])
-apply (erule subsetD, simp add: refl)
+apply (erule subsetD, simp add: r_refl)
 done
 
 lemma mem_rep_iff_principal_less: "a \<in> rep x \<longleftrightarrow> principal a \<sqsubseteq> x"
@@ -219,16 +231,16 @@
 lemma principal_less_iff_mem_rep: "principal a \<sqsubseteq> x \<longleftrightarrow> a \<in> rep x"
 by (simp add: rep_eq)
 
-lemma principal_less_iff: "principal a \<sqsubseteq> principal b \<longleftrightarrow> r a b"
+lemma principal_less_iff: "principal a \<sqsubseteq> principal b \<longleftrightarrow> a \<preceq> b"
 by (simp add: principal_less_iff_mem_rep rep_principal)
 
-lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> r a b \<and> r b a"
+lemma principal_eq_iff: "principal a = principal b \<longleftrightarrow> a \<preceq> b \<and> b \<preceq> a"
 unfolding po_eq_conv [where 'a='b] principal_less_iff ..
 
 lemma repD: "a \<in> rep x \<Longrightarrow> principal a \<sqsubseteq> x"
 by (simp add: rep_eq)
 
-lemma principal_mono: "r a b \<Longrightarrow> principal a \<sqsubseteq> principal b"
+lemma principal_mono: "a \<preceq> b \<Longrightarrow> principal a \<sqsubseteq> principal b"
 by (simp add: principal_less_iff)
 
 lemma lessI: "(\<And>a. principal a \<sqsubseteq> x \<Longrightarrow> principal a \<sqsubseteq> u) \<Longrightarrow> x \<sqsubseteq> u"
@@ -251,7 +263,7 @@
 
 lemma basis_fun_beta:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
-  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
+  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "basis_fun f\<cdot>x = lub (f ` rep x)"
 unfolding basis_fun_def
 proof (rule beta_cfun)
@@ -272,7 +284,7 @@
 
 lemma basis_fun_principal:
   fixes f :: "'a::type \<Rightarrow> 'c::cpo"
-  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
+  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
   shows "basis_fun f\<cdot>(principal a) = f a"
 apply (subst basis_fun_beta, erule f_mono)
 apply (subst rep_principal)
@@ -280,8 +292,8 @@
 done
 
 lemma basis_fun_mono:
-  assumes f_mono: "\<And>a b. r a b \<Longrightarrow> f a \<sqsubseteq> f b"
-  assumes g_mono: "\<And>a b. r a b \<Longrightarrow> g a \<sqsubseteq> g b"
+  assumes f_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> f a \<sqsubseteq> f b"
+  assumes g_mono: "\<And>a b. a \<preceq> b \<Longrightarrow> g a \<sqsubseteq> g b"
   assumes less: "\<And>a. f a \<sqsubseteq> g a"
   shows "basis_fun f \<sqsubseteq> basis_fun g"
  apply (rule less_cfun_ext)
@@ -435,10 +447,9 @@
   compacts :: "'a \<Rightarrow> 'a compact_basis set" where
   "compacts = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
 
-lemma ideal_compacts: "preorder.ideal sq_le (compacts w)"
+lemma ideal_compacts: "sq_le.ideal (compacts w)"
 unfolding compacts_def
- apply (rule preorder.idealI)
-    apply (rule preorder_class.axioms)
+ apply (rule sq_le.idealI)
    apply (rule_tac x="Abs_compact_basis (approx 0\<cdot>w)" in exI)
    apply (simp add: approx_less)
   apply simp
diff -r 5ebfb7f25ebb -r 1d8c6703c7b1 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Jun 18 23:03:11 2008 +0200
+++ b/src/HOLCF/Porder.thy	Wed Jun 18 23:07:30 2008 +0200
@@ -20,11 +20,9 @@
 notation (xsymbols)
   sq_le (infixl "\<sqsubseteq>" 55)
 
-class preorder = sq_ord +
+class po = sq_ord +
   assumes refl_less [iff]: "x \<sqsubseteq> x"
   assumes trans_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
-
-class po = preorder +
   assumes antisym_less: "\<lbrakk>x \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
 
 text {* minimal fixes least element *}