# HG changeset patch # User huffman # Date 1200341720 -3600 # Node ID 6b96b93928738d9598cf344c83fa1d45f401e334 # Parent d8ce142f7e6e02926f669875251eb1c13ba3a87d add class bifinite_cpo for possibly-unpointed bifinite domains diff -r d8ce142f7e6e -r 6b96b9392873 src/HOLCF/Bifinite.thy --- a/src/HOLCF/Bifinite.thy Mon Jan 14 20:45:10 2008 +0100 +++ b/src/HOLCF/Bifinite.thy Mon Jan 14 21:15:20 2008 +0100 @@ -11,16 +11,18 @@ subsection {* Bifinite domains *} -axclass approx < pcpo +axclass approx < cpo consts approx :: "nat \ 'a::approx \ 'a" -axclass bifinite < approx +axclass bifinite_cpo < approx chain_approx_app: "chain (\i. approx i\x)" lub_approx_app [simp]: "(\i. approx i\x) = x" approx_idem: "approx i\(approx i\x) = approx i\x" finite_fixes_approx: "finite {x. approx i\x = x}" +axclass bifinite < bifinite_cpo, pcpo + lemma finite_range_imp_finite_fixes: "finite {x. \y. x = f y} \ finite {x. f x = x}" apply (subgoal_tac "{x. f x = x} \ {x. \y. x = f y}") @@ -29,17 +31,17 @@ done lemma chain_approx [simp]: - "chain (approx :: nat \ 'a::bifinite \ 'a)" + "chain (approx :: nat \ 'a::bifinite_cpo \ 'a)" apply (rule chainI) apply (rule less_cfun_ext) apply (rule chainE) apply (rule chain_approx_app) done -lemma lub_approx [simp]: "(\i. approx i) = (\(x::'a::bifinite). x)" +lemma lub_approx [simp]: "(\i. approx i) = (\(x::'a::bifinite_cpo). x)" by (rule ext_cfun, simp add: contlub_cfun_fun) -lemma approx_less: "approx i\x \ (x::'a::bifinite)" +lemma approx_less: "approx i\x \ (x::'a::bifinite_cpo)" apply (subgoal_tac "approx i\x \ (\i. approx i\x)", simp) apply (rule is_ub_thelub, simp) done @@ -48,7 +50,7 @@ by (rule UU_I, rule approx_less) lemma approx_approx1: - "i \ j \ approx i\(approx j\x) = approx i\(x::'a::bifinite)" + "i \ j \ approx i\(approx j\x) = approx i\(x::'a::bifinite_cpo)" apply (rule antisym_less) apply (rule monofun_cfun_arg [OF approx_less]) apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]]) @@ -58,7 +60,7 @@ done lemma approx_approx2: - "j \ i \ approx i\(approx j\x) = approx j\(x::'a::bifinite)" + "j \ i \ approx i\(approx j\x) = approx j\(x::'a::bifinite_cpo)" apply (rule antisym_less) apply (rule approx_less) apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]]) @@ -67,7 +69,7 @@ done lemma approx_approx [simp]: - "approx i\(approx j\x) = approx (min i j)\(x::'a::bifinite)" + "approx i\(approx j\x) = approx (min i j)\(x::'a::bifinite_cpo)" apply (rule_tac x=i and y=j in linorder_le_cases) apply (simp add: approx_approx1 min_def) apply (simp add: approx_approx2 min_def) @@ -77,15 +79,15 @@ "\x. f (f x) = f x \ {x. f x = x} = {y. \x. y = f x}" by (auto simp add: eq_sym_conv) -lemma finite_approx: "finite {y::'a::bifinite. \x. y = approx n\x}" +lemma finite_approx: "finite {y::'a::bifinite_cpo. \x. y = approx n\x}" using finite_fixes_approx by (simp add: idem_fixes_eq_range) lemma finite_range_approx: - "finite (range (\x::'a::bifinite. approx n\x))" + "finite (range (\x::'a::bifinite_cpo. approx n\x))" by (simp add: image_def finite_approx) lemma compact_approx [simp]: - fixes x :: "'a::bifinite" + fixes x :: "'a::bifinite_cpo" shows "compact (approx n\x)" proof (rule compactI2) fix Y::"nat \ 'a" @@ -116,7 +118,7 @@ qed lemma bifinite_compact_eq_approx: - fixes x :: "'a::bifinite" + fixes x :: "'a::bifinite_cpo" assumes x: "compact x" shows "\i. approx i\x = x" proof - @@ -130,7 +132,7 @@ qed lemma bifinite_compact_iff: - "compact (x::'a::bifinite) = (\n. approx n\x = x)" + "compact (x::'a::bifinite_cpo) = (\n. approx n\x = x)" apply (rule iffI) apply (erule bifinite_compact_eq_approx) apply (erule exE) @@ -148,7 +150,7 @@ qed lemma bifinite_less_ext: - fixes x y :: "'a::bifinite" + fixes x y :: "'a::bifinite_cpo" shows "(\i. approx i\x \ approx i\y) \ x \ y" apply (subgoal_tac "(\i. approx i\x) \ (\i. approx i\y)", simp) apply (rule lub_mono [rule_format], simp, simp, simp) @@ -176,13 +178,13 @@ apply clarsimp done -instance "->" :: (bifinite, bifinite) approx .. +instance "->" :: (bifinite_cpo, bifinite_cpo) approx .. defs (overloaded) approx_cfun_def: "approx \ \n. \ f x. approx n\(f\(approx n\x))" -instance "->" :: (bifinite, bifinite) bifinite +instance "->" :: (bifinite_cpo, bifinite_cpo) bifinite_cpo apply (intro_classes, unfold approx_cfun_def) apply simp apply (simp add: lub_distribs eta_cfun) @@ -192,6 +194,8 @@ apply (intro finite_range_lemma finite_approx) done +instance "->" :: (bifinite_cpo, bifinite) bifinite .. + lemma approx_cfun: "approx n\f\x = approx n\(f\(approx n\x))" by (simp add: approx_cfun_def)