--- 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";
--- 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)
--- 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";
--- 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
--- 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";
--- 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 *}