# HG changeset patch
# User huffman
# Date 1120601254 -7200
# Node ID 24b494ff8f0fd83b21e089a07e15d221bc1aaf07
# Parent  53ba41c5fa7c05cd67c84dd0674becc6ce70098c
use new pcpodef package

diff -r 53ba41c5fa7c -r 24b494ff8f0f src/HOLCF/Cfun.ML
--- a/src/HOLCF/Cfun.ML	Wed Jul 06 00:06:34 2005 +0200
+++ b/src/HOLCF/Cfun.ML	Wed Jul 06 00:07:34 2005 +0200
@@ -1,7 +1,7 @@
 
 (* legacy ML bindings *)
 
-val less_cfun_def = thm "less_cfun_def";
+val less_cfun_def = thm "less_CFun_def";
 val cfun_cong = thm "cfun_cong";
 val cfun_fun_cong = thm "cfun_fun_cong";
 val cfun_arg_cong = thm "cfun_arg_cong";
diff -r 53ba41c5fa7c -r 24b494ff8f0f src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Wed Jul 06 00:06:34 2005 +0200
+++ b/src/HOLCF/Cfun.thy	Wed Jul 06 00:07:34 2005 +0200
@@ -8,7 +8,7 @@
 header {* The type of continuous functions *}
 
 theory Cfun
-imports TypedefPcpo
+imports Pcpodef
 uses ("cont_proc.ML")
 begin
 
@@ -16,8 +16,14 @@
 
 subsection {* Definition of continuous function type *}
 
-typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}"
-by (rule exI, fast intro: cont_const)
+lemma Ex_cont: "\<exists>f. cont f"
+by (rule exI, rule cont_const)
+
+lemma adm_cont: "adm cont"
+by (rule admI, rule cont_lub_fun)
+
+cpodef (CFun)  ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}"
+by (simp add: Ex_cont adm_cont)
 
 syntax
   Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("_$_" [999,1000] 999)
@@ -36,37 +42,17 @@
 
 subsection {* Class instances *}
 
-instance "->"  :: (cpo, cpo) sq_ord ..
-
-defs (overloaded)
-  less_cfun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. Rep_CFun f \<sqsubseteq> Rep_CFun g)"
-
-lemma adm_CFun: "adm (\<lambda>f. f \<in> CFun)"
-by (simp add: CFun_def, rule admI, rule cont_lub_fun)
-
 lemma UU_CFun: "\<bottom> \<in> CFun"
 by (simp add: CFun_def inst_fun_pcpo cont_const)
 
-instance "->" :: (cpo, cpo) po
-by (rule typedef_po [OF type_definition_CFun less_cfun_def])
-
-instance "->" :: (cpo, cpo) cpo
-by (rule typedef_cpo [OF type_definition_CFun less_cfun_def adm_CFun])
-
 instance "->" :: (cpo, pcpo) pcpo
-by (rule typedef_pcpo_UU [OF type_definition_CFun less_cfun_def UU_CFun])
-
-lemmas cont_Rep_CFun =
-  typedef_cont_Rep [OF type_definition_CFun less_cfun_def adm_CFun]
-
-lemmas cont_Abs_CFun = 
-  typedef_cont_Abs [OF type_definition_CFun less_cfun_def adm_CFun]
+by (rule typedef_pcpo_UU [OF type_definition_CFun less_CFun_def UU_CFun])
 
 lemmas Rep_CFun_strict =
-  typedef_Rep_strict [OF type_definition_CFun less_cfun_def UU_CFun]
+  typedef_Rep_strict [OF type_definition_CFun less_CFun_def UU_CFun]
 
 lemmas Abs_CFun_strict =
-  typedef_Abs_strict [OF type_definition_CFun less_cfun_def UU_CFun]
+  typedef_Abs_strict [OF type_definition_CFun less_CFun_def UU_CFun]
 
 text {* Additional lemma about the isomorphism between
         @{typ "'a -> 'b"} and @{term CFun} *}
@@ -136,12 +122,12 @@
 text {* Extensionality wrt. @{term "op <<"} in @{typ "'a -> 'b"} *}
 
 lemma less_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
-by (simp add: less_cfun_def less_fun_def)
+by (simp add: less_CFun_def less_fun_def)
 
 text {* monotonicity of application *}
 
 lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
-by (simp add: less_cfun_def less_fun_def)
+by (simp add: less_CFun_def less_fun_def)
 
 lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
 by (rule monofun_Rep_CFun2 [THEN monofunE])
@@ -204,9 +190,8 @@
 
 text {* a lemma about the exchange of lubs for type @{typ "'a -> 'b"} *}
 
-lemma ex_lub_cfun: "[| chain(F); chain(Y) |] ==> 
-                lub(range(%j. lub(range(%i. F(j)$(Y i))))) = 
-                lub(range(%i. lub(range(%j. F(j)$(Y i)))))"
+lemma ex_lub_cfun:
+  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>j. \<Squnion>i. F j\<cdot>(Y i)) = (\<Squnion>i. \<Squnion>j. F j\<cdot>(Y i))"
 by (simp add: diag_lub ch2ch_Rep_CFunL ch2ch_Rep_CFunR)
 
 text {* the lub of a chain of cont. functions is continuous *}
@@ -222,7 +207,7 @@
 lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (LAM x. LUB i. F i$x)"
 apply (subst thelub_fun [symmetric])
 apply (erule monofun_Rep_CFun [THEN ch2ch_monofun])
-apply (erule typedef_is_lub [OF type_definition_CFun less_cfun_def adm_CFun])
+apply (erule typedef_is_lub [OF type_definition_CFun less_CFun_def adm_CFun])
 done
 
 lemmas thelub_cfun = lub_cfun [THEN thelubI, standard]
@@ -232,8 +217,9 @@
 
 text {* Monotonicity of @{term Abs_CFun} *}
 
-lemma semi_monofun_Abs_CFun: "[| cont(f); cont(g); f<<g|] ==> Abs_CFun(f)<<Abs_CFun(g)"
-by (simp add: less_cfun_def Abs_CFun_inverse2)
+lemma semi_monofun_Abs_CFun:
+  "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_CFun f \<sqsubseteq> Abs_CFun g"
+by (simp add: less_CFun_def Abs_CFun_inverse2)
 
 text {* for compatibility with old HOLCF-Version *}
 lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)"
@@ -454,7 +440,8 @@
 lemma contlub_Istrictify2: "contlub (\<lambda>x. Istrictify f x)"
 apply (rule contlubI)
 apply (case_tac "lub (range Y) = \<bottom>")
-apply (simp add: Istrictify1 chain_UU_I thelub_const)
+apply (drule (1) chain_UU_I)
+apply (simp add: Istrictify1 thelub_const)
 apply (simp add: Istrictify2)
 apply (simp add: contlub_cfun_arg)
 apply (rule lub_equal2)
diff -r 53ba41c5fa7c -r 24b494ff8f0f src/HOLCF/Sprod.ML
--- a/src/HOLCF/Sprod.ML	Wed Jul 06 00:06:34 2005 +0200
+++ b/src/HOLCF/Sprod.ML	Wed Jul 06 00:07:34 2005 +0200
@@ -1,7 +1,7 @@
 
 (* legacy ML bindings *)
 
-val less_sprod_def = thm "less_sprod_def";
+val less_sprod_def = thm "less_Sprod_def";
 val spair_def = thm "spair_def";
 val sfst_def = thm "sfst_def";
 val ssnd_def = thm "ssnd_def";
diff -r 53ba41c5fa7c -r 24b494ff8f0f src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Wed Jul 06 00:06:34 2005 +0200
+++ b/src/HOLCF/Sprod.thy	Wed Jul 06 00:07:34 2005 +0200
@@ -8,55 +8,22 @@
 header {* The type of strict products *}
 
 theory Sprod
-imports Cprod TypedefPcpo
+imports Cprod
 begin
 
 defaultsort pcpo
 
 subsection {* Definition of strict product type *}
 
-typedef (Sprod)  ('a, 'b) "**" (infixr 20) =
+pcpodef (Sprod)  ('a, 'b) "**" (infixr 20) =
         "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
-by (auto simp add: inst_cprod_pcpo)
+by simp
 
 syntax (xsymbols)
   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
 syntax (HTML output)
   "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
 
-subsection {* Class instances *}
-
-instance "**" :: (pcpo, pcpo) sq_ord ..
-defs (overloaded)
-  less_sprod_def: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_Sprod x \<sqsubseteq> Rep_Sprod y"
-
-lemma adm_Sprod: "adm (\<lambda>x. x \<in> Sprod)"
-by (simp add: Sprod_def)
-
-lemma UU_Sprod: "\<bottom> \<in> Sprod"
-by (simp add: Sprod_def)
-
-instance "**" :: (pcpo, pcpo) po
-by (rule typedef_po [OF type_definition_Sprod less_sprod_def])
-
-instance "**" :: (pcpo, pcpo) cpo
-by (rule typedef_cpo [OF type_definition_Sprod less_sprod_def adm_Sprod])
-
-instance "**" :: (pcpo, pcpo) pcpo
-by (rule typedef_pcpo_UU [OF type_definition_Sprod less_sprod_def UU_Sprod])
-
-lemmas cont_Rep_Sprod =
-  typedef_cont_Rep [OF type_definition_Sprod less_sprod_def adm_Sprod]
-
-lemmas cont_Abs_Sprod = 
-  typedef_cont_Abs [OF type_definition_Sprod less_sprod_def adm_Sprod]
-
-lemmas Rep_Sprod_strict =
-  typedef_Rep_strict [OF type_definition_Sprod less_sprod_def UU_Sprod]
-
-lemmas Abs_Sprod_strict =
-  typedef_Abs_strict [OF type_definition_Sprod less_sprod_def UU_Sprod]
-
 lemma UU_Abs_Sprod: "\<bottom> = Abs_Sprod <\<bottom>, \<bottom>>"
 by (simp add: Abs_Sprod_strict inst_cprod_pcpo2 [symmetric])
 
@@ -178,7 +145,7 @@
 by (rule_tac p=p in sprodE, simp_all)
 
 lemma less_sprod: "p1 \<sqsubseteq> p2 = (sfst\<cdot>p1 \<sqsubseteq> sfst\<cdot>p2 \<and> ssnd\<cdot>p1 \<sqsubseteq> ssnd\<cdot>p2)"
-apply (simp add: less_sprod_def sfst_def ssnd_def cont_Rep_Sprod)
+apply (simp add: less_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
 apply (rule less_cprod)
 done
 
diff -r 53ba41c5fa7c -r 24b494ff8f0f src/HOLCF/Ssum.ML
--- a/src/HOLCF/Ssum.ML	Wed Jul 06 00:06:34 2005 +0200
+++ b/src/HOLCF/Ssum.ML	Wed Jul 06 00:07:34 2005 +0200
@@ -5,7 +5,7 @@
 val Iwhen1 = thm "Iwhen1";
 val Iwhen2 = thm "Iwhen2";
 val Iwhen3 = thm "Iwhen3";
-val less_ssum_def = thm "less_ssum_def";
+val less_ssum_def = thm "less_Ssum_def";
 val sinl_def = thm "sinl_def";
 val sinr_def = thm "sinr_def";
 val sscase_def = thm "sscase_def";
diff -r 53ba41c5fa7c -r 24b494ff8f0f src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Wed Jul 06 00:06:34 2005 +0200
+++ b/src/HOLCF/Ssum.thy	Wed Jul 06 00:07:34 2005 +0200
@@ -8,55 +8,22 @@
 header {* The type of strict sums *}
 
 theory Ssum
-imports Cprod TypedefPcpo
+imports Cprod
 begin
 
 defaultsort pcpo
 
 subsection {* Definition of strict sum type *}
 
-typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
+pcpodef (Ssum)  ('a, 'b) "++" (infixr 10) = 
         "{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}"
-by (rule_tac x="<\<bottom>,\<bottom>>" in exI, simp)
+by simp
 
 syntax (xsymbols)
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
 syntax (HTML output)
   "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
 
-subsection {* Class instances *}
-
-instance "++" :: (pcpo, pcpo) sq_ord ..
-defs (overloaded)
-  less_ssum_def: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_Ssum x \<sqsubseteq> Rep_Ssum y"
-
-lemma adm_Ssum: "adm (\<lambda>x. x \<in> Ssum)"
-by (simp add: Ssum_def cont_fst cont_snd)
-
-lemma UU_Ssum: "\<bottom> \<in> Ssum"
-by (simp add: Ssum_def inst_cprod_pcpo2)
-
-instance "++" :: (pcpo, pcpo) po
-by (rule typedef_po [OF type_definition_Ssum less_ssum_def])
-
-instance "++" :: (pcpo, pcpo) cpo
-by (rule typedef_cpo [OF type_definition_Ssum less_ssum_def adm_Ssum])
-
-instance "++" :: (pcpo, pcpo) pcpo
-by (rule typedef_pcpo_UU [OF type_definition_Ssum less_ssum_def UU_Ssum])
-
-lemmas cont_Rep_Ssum =
-  typedef_cont_Rep [OF type_definition_Ssum less_ssum_def adm_Ssum]
-
-lemmas cont_Abs_Ssum = 
-  typedef_cont_Abs [OF type_definition_Ssum less_ssum_def adm_Ssum]
-
-lemmas Rep_Ssum_strict =
-  typedef_Rep_strict [OF type_definition_Ssum less_ssum_def UU_Ssum]
-
-lemmas Abs_Ssum_strict =
-  typedef_Abs_strict [OF type_definition_Ssum less_ssum_def UU_Ssum]
-
 lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>"
 by (simp add: Abs_Ssum_strict inst_cprod_pcpo2 [symmetric])
 
@@ -146,16 +113,16 @@
 subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
 
 lemma sinl_less: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: less_ssum_def Rep_Ssum_sinl cpair_less)
+by (simp add: less_Ssum_def Rep_Ssum_sinl cpair_less)
 
 lemma sinr_less: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
-by (simp add: less_ssum_def Rep_Ssum_sinr cpair_less)
+by (simp add: less_Ssum_def Rep_Ssum_sinr cpair_less)
 
 lemma sinl_less_sinr: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
 
 lemma sinr_less_sinl: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
-by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
+by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
 
 subsection {* Chains of strict sums *}