use new pcpodef package
authorhuffman
Wed Jul 06 00:07:34 2005 +0200 (2005-07-06)
changeset 1669924b494ff8f0f
parent 16698 53ba41c5fa7c
child 16700 92925e30ff59
use new pcpodef package
src/HOLCF/Cfun.ML
src/HOLCF/Cfun.thy
src/HOLCF/Sprod.ML
src/HOLCF/Sprod.thy
src/HOLCF/Ssum.ML
src/HOLCF/Ssum.thy
     1.1 --- a/src/HOLCF/Cfun.ML	Wed Jul 06 00:06:34 2005 +0200
     1.2 +++ b/src/HOLCF/Cfun.ML	Wed Jul 06 00:07:34 2005 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  
     1.5  (* legacy ML bindings *)
     1.6  
     1.7 -val less_cfun_def = thm "less_cfun_def";
     1.8 +val less_cfun_def = thm "less_CFun_def";
     1.9  val cfun_cong = thm "cfun_cong";
    1.10  val cfun_fun_cong = thm "cfun_fun_cong";
    1.11  val cfun_arg_cong = thm "cfun_arg_cong";
     2.1 --- a/src/HOLCF/Cfun.thy	Wed Jul 06 00:06:34 2005 +0200
     2.2 +++ b/src/HOLCF/Cfun.thy	Wed Jul 06 00:07:34 2005 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* The type of continuous functions *}
     2.5  
     2.6  theory Cfun
     2.7 -imports TypedefPcpo
     2.8 +imports Pcpodef
     2.9  uses ("cont_proc.ML")
    2.10  begin
    2.11  
    2.12 @@ -16,8 +16,14 @@
    2.13  
    2.14  subsection {* Definition of continuous function type *}
    2.15  
    2.16 -typedef (CFun)  ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}"
    2.17 -by (rule exI, fast intro: cont_const)
    2.18 +lemma Ex_cont: "\<exists>f. cont f"
    2.19 +by (rule exI, rule cont_const)
    2.20 +
    2.21 +lemma adm_cont: "adm cont"
    2.22 +by (rule admI, rule cont_lub_fun)
    2.23 +
    2.24 +cpodef (CFun)  ('a, 'b) "->" (infixr 0) = "{f::'a => 'b. cont f}"
    2.25 +by (simp add: Ex_cont adm_cont)
    2.26  
    2.27  syntax
    2.28    Rep_CFun :: "('a -> 'b) => ('a => 'b)" ("_$_" [999,1000] 999)
    2.29 @@ -36,37 +42,17 @@
    2.30  
    2.31  subsection {* Class instances *}
    2.32  
    2.33 -instance "->"  :: (cpo, cpo) sq_ord ..
    2.34 -
    2.35 -defs (overloaded)
    2.36 -  less_cfun_def: "(op \<sqsubseteq>) \<equiv> (\<lambda>f g. Rep_CFun f \<sqsubseteq> Rep_CFun g)"
    2.37 -
    2.38 -lemma adm_CFun: "adm (\<lambda>f. f \<in> CFun)"
    2.39 -by (simp add: CFun_def, rule admI, rule cont_lub_fun)
    2.40 -
    2.41  lemma UU_CFun: "\<bottom> \<in> CFun"
    2.42  by (simp add: CFun_def inst_fun_pcpo cont_const)
    2.43  
    2.44 -instance "->" :: (cpo, cpo) po
    2.45 -by (rule typedef_po [OF type_definition_CFun less_cfun_def])
    2.46 -
    2.47 -instance "->" :: (cpo, cpo) cpo
    2.48 -by (rule typedef_cpo [OF type_definition_CFun less_cfun_def adm_CFun])
    2.49 -
    2.50  instance "->" :: (cpo, pcpo) pcpo
    2.51 -by (rule typedef_pcpo_UU [OF type_definition_CFun less_cfun_def UU_CFun])
    2.52 -
    2.53 -lemmas cont_Rep_CFun =
    2.54 -  typedef_cont_Rep [OF type_definition_CFun less_cfun_def adm_CFun]
    2.55 -
    2.56 -lemmas cont_Abs_CFun = 
    2.57 -  typedef_cont_Abs [OF type_definition_CFun less_cfun_def adm_CFun]
    2.58 +by (rule typedef_pcpo_UU [OF type_definition_CFun less_CFun_def UU_CFun])
    2.59  
    2.60  lemmas Rep_CFun_strict =
    2.61 -  typedef_Rep_strict [OF type_definition_CFun less_cfun_def UU_CFun]
    2.62 +  typedef_Rep_strict [OF type_definition_CFun less_CFun_def UU_CFun]
    2.63  
    2.64  lemmas Abs_CFun_strict =
    2.65 -  typedef_Abs_strict [OF type_definition_CFun less_cfun_def UU_CFun]
    2.66 +  typedef_Abs_strict [OF type_definition_CFun less_CFun_def UU_CFun]
    2.67  
    2.68  text {* Additional lemma about the isomorphism between
    2.69          @{typ "'a -> 'b"} and @{term CFun} *}
    2.70 @@ -136,12 +122,12 @@
    2.71  text {* Extensionality wrt. @{term "op <<"} in @{typ "'a -> 'b"} *}
    2.72  
    2.73  lemma less_cfun_ext: "(\<And>x. f\<cdot>x \<sqsubseteq> g\<cdot>x) \<Longrightarrow> f \<sqsubseteq> g"
    2.74 -by (simp add: less_cfun_def less_fun_def)
    2.75 +by (simp add: less_CFun_def less_fun_def)
    2.76  
    2.77  text {* monotonicity of application *}
    2.78  
    2.79  lemma monofun_cfun_fun: "f \<sqsubseteq> g \<Longrightarrow> f\<cdot>x \<sqsubseteq> g\<cdot>x"
    2.80 -by (simp add: less_cfun_def less_fun_def)
    2.81 +by (simp add: less_CFun_def less_fun_def)
    2.82  
    2.83  lemma monofun_cfun_arg: "x \<sqsubseteq> y \<Longrightarrow> f\<cdot>x \<sqsubseteq> f\<cdot>y"
    2.84  by (rule monofun_Rep_CFun2 [THEN monofunE])
    2.85 @@ -204,9 +190,8 @@
    2.86  
    2.87  text {* a lemma about the exchange of lubs for type @{typ "'a -> 'b"} *}
    2.88  
    2.89 -lemma ex_lub_cfun: "[| chain(F); chain(Y) |] ==> 
    2.90 -                lub(range(%j. lub(range(%i. F(j)$(Y i))))) = 
    2.91 -                lub(range(%i. lub(range(%j. F(j)$(Y i)))))"
    2.92 +lemma ex_lub_cfun:
    2.93 +  "\<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))"
    2.94  by (simp add: diag_lub ch2ch_Rep_CFunL ch2ch_Rep_CFunR)
    2.95  
    2.96  text {* the lub of a chain of cont. functions is continuous *}
    2.97 @@ -222,7 +207,7 @@
    2.98  lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (LAM x. LUB i. F i$x)"
    2.99  apply (subst thelub_fun [symmetric])
   2.100  apply (erule monofun_Rep_CFun [THEN ch2ch_monofun])
   2.101 -apply (erule typedef_is_lub [OF type_definition_CFun less_cfun_def adm_CFun])
   2.102 +apply (erule typedef_is_lub [OF type_definition_CFun less_CFun_def adm_CFun])
   2.103  done
   2.104  
   2.105  lemmas thelub_cfun = lub_cfun [THEN thelubI, standard]
   2.106 @@ -232,8 +217,9 @@
   2.107  
   2.108  text {* Monotonicity of @{term Abs_CFun} *}
   2.109  
   2.110 -lemma semi_monofun_Abs_CFun: "[| cont(f); cont(g); f<<g|] ==> Abs_CFun(f)<<Abs_CFun(g)"
   2.111 -by (simp add: less_cfun_def Abs_CFun_inverse2)
   2.112 +lemma semi_monofun_Abs_CFun:
   2.113 +  "\<lbrakk>cont f; cont g; f \<sqsubseteq> g\<rbrakk> \<Longrightarrow> Abs_CFun f \<sqsubseteq> Abs_CFun g"
   2.114 +by (simp add: less_CFun_def Abs_CFun_inverse2)
   2.115  
   2.116  text {* for compatibility with old HOLCF-Version *}
   2.117  lemma inst_cfun_pcpo: "\<bottom> = (\<Lambda> x. \<bottom>)"
   2.118 @@ -454,7 +440,8 @@
   2.119  lemma contlub_Istrictify2: "contlub (\<lambda>x. Istrictify f x)"
   2.120  apply (rule contlubI)
   2.121  apply (case_tac "lub (range Y) = \<bottom>")
   2.122 -apply (simp add: Istrictify1 chain_UU_I thelub_const)
   2.123 +apply (drule (1) chain_UU_I)
   2.124 +apply (simp add: Istrictify1 thelub_const)
   2.125  apply (simp add: Istrictify2)
   2.126  apply (simp add: contlub_cfun_arg)
   2.127  apply (rule lub_equal2)
     3.1 --- a/src/HOLCF/Sprod.ML	Wed Jul 06 00:06:34 2005 +0200
     3.2 +++ b/src/HOLCF/Sprod.ML	Wed Jul 06 00:07:34 2005 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  
     3.5  (* legacy ML bindings *)
     3.6  
     3.7 -val less_sprod_def = thm "less_sprod_def";
     3.8 +val less_sprod_def = thm "less_Sprod_def";
     3.9  val spair_def = thm "spair_def";
    3.10  val sfst_def = thm "sfst_def";
    3.11  val ssnd_def = thm "ssnd_def";
     4.1 --- a/src/HOLCF/Sprod.thy	Wed Jul 06 00:06:34 2005 +0200
     4.2 +++ b/src/HOLCF/Sprod.thy	Wed Jul 06 00:07:34 2005 +0200
     4.3 @@ -8,55 +8,22 @@
     4.4  header {* The type of strict products *}
     4.5  
     4.6  theory Sprod
     4.7 -imports Cprod TypedefPcpo
     4.8 +imports Cprod
     4.9  begin
    4.10  
    4.11  defaultsort pcpo
    4.12  
    4.13  subsection {* Definition of strict product type *}
    4.14  
    4.15 -typedef (Sprod)  ('a, 'b) "**" (infixr 20) =
    4.16 +pcpodef (Sprod)  ('a, 'b) "**" (infixr 20) =
    4.17          "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
    4.18 -by (auto simp add: inst_cprod_pcpo)
    4.19 +by simp
    4.20  
    4.21  syntax (xsymbols)
    4.22    "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
    4.23  syntax (HTML output)
    4.24    "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
    4.25  
    4.26 -subsection {* Class instances *}
    4.27 -
    4.28 -instance "**" :: (pcpo, pcpo) sq_ord ..
    4.29 -defs (overloaded)
    4.30 -  less_sprod_def: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_Sprod x \<sqsubseteq> Rep_Sprod y"
    4.31 -
    4.32 -lemma adm_Sprod: "adm (\<lambda>x. x \<in> Sprod)"
    4.33 -by (simp add: Sprod_def)
    4.34 -
    4.35 -lemma UU_Sprod: "\<bottom> \<in> Sprod"
    4.36 -by (simp add: Sprod_def)
    4.37 -
    4.38 -instance "**" :: (pcpo, pcpo) po
    4.39 -by (rule typedef_po [OF type_definition_Sprod less_sprod_def])
    4.40 -
    4.41 -instance "**" :: (pcpo, pcpo) cpo
    4.42 -by (rule typedef_cpo [OF type_definition_Sprod less_sprod_def adm_Sprod])
    4.43 -
    4.44 -instance "**" :: (pcpo, pcpo) pcpo
    4.45 -by (rule typedef_pcpo_UU [OF type_definition_Sprod less_sprod_def UU_Sprod])
    4.46 -
    4.47 -lemmas cont_Rep_Sprod =
    4.48 -  typedef_cont_Rep [OF type_definition_Sprod less_sprod_def adm_Sprod]
    4.49 -
    4.50 -lemmas cont_Abs_Sprod = 
    4.51 -  typedef_cont_Abs [OF type_definition_Sprod less_sprod_def adm_Sprod]
    4.52 -
    4.53 -lemmas Rep_Sprod_strict =
    4.54 -  typedef_Rep_strict [OF type_definition_Sprod less_sprod_def UU_Sprod]
    4.55 -
    4.56 -lemmas Abs_Sprod_strict =
    4.57 -  typedef_Abs_strict [OF type_definition_Sprod less_sprod_def UU_Sprod]
    4.58 -
    4.59  lemma UU_Abs_Sprod: "\<bottom> = Abs_Sprod <\<bottom>, \<bottom>>"
    4.60  by (simp add: Abs_Sprod_strict inst_cprod_pcpo2 [symmetric])
    4.61  
    4.62 @@ -178,7 +145,7 @@
    4.63  by (rule_tac p=p in sprodE, simp_all)
    4.64  
    4.65  lemma less_sprod: "p1 \<sqsubseteq> p2 = (sfst\<cdot>p1 \<sqsubseteq> sfst\<cdot>p2 \<and> ssnd\<cdot>p1 \<sqsubseteq> ssnd\<cdot>p2)"
    4.66 -apply (simp add: less_sprod_def sfst_def ssnd_def cont_Rep_Sprod)
    4.67 +apply (simp add: less_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
    4.68  apply (rule less_cprod)
    4.69  done
    4.70  
     5.1 --- a/src/HOLCF/Ssum.ML	Wed Jul 06 00:06:34 2005 +0200
     5.2 +++ b/src/HOLCF/Ssum.ML	Wed Jul 06 00:07:34 2005 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4  val Iwhen1 = thm "Iwhen1";
     5.5  val Iwhen2 = thm "Iwhen2";
     5.6  val Iwhen3 = thm "Iwhen3";
     5.7 -val less_ssum_def = thm "less_ssum_def";
     5.8 +val less_ssum_def = thm "less_Ssum_def";
     5.9  val sinl_def = thm "sinl_def";
    5.10  val sinr_def = thm "sinr_def";
    5.11  val sscase_def = thm "sscase_def";
     6.1 --- a/src/HOLCF/Ssum.thy	Wed Jul 06 00:06:34 2005 +0200
     6.2 +++ b/src/HOLCF/Ssum.thy	Wed Jul 06 00:07:34 2005 +0200
     6.3 @@ -8,55 +8,22 @@
     6.4  header {* The type of strict sums *}
     6.5  
     6.6  theory Ssum
     6.7 -imports Cprod TypedefPcpo
     6.8 +imports Cprod
     6.9  begin
    6.10  
    6.11  defaultsort pcpo
    6.12  
    6.13  subsection {* Definition of strict sum type *}
    6.14  
    6.15 -typedef (Ssum)  ('a, 'b) "++" (infixr 10) = 
    6.16 +pcpodef (Ssum)  ('a, 'b) "++" (infixr 10) = 
    6.17          "{p::'a \<times> 'b. cfst\<cdot>p = \<bottom> \<or> csnd\<cdot>p = \<bottom>}"
    6.18 -by (rule_tac x="<\<bottom>,\<bottom>>" in exI, simp)
    6.19 +by simp
    6.20  
    6.21  syntax (xsymbols)
    6.22    "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
    6.23  syntax (HTML output)
    6.24    "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
    6.25  
    6.26 -subsection {* Class instances *}
    6.27 -
    6.28 -instance "++" :: (pcpo, pcpo) sq_ord ..
    6.29 -defs (overloaded)
    6.30 -  less_ssum_def: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_Ssum x \<sqsubseteq> Rep_Ssum y"
    6.31 -
    6.32 -lemma adm_Ssum: "adm (\<lambda>x. x \<in> Ssum)"
    6.33 -by (simp add: Ssum_def cont_fst cont_snd)
    6.34 -
    6.35 -lemma UU_Ssum: "\<bottom> \<in> Ssum"
    6.36 -by (simp add: Ssum_def inst_cprod_pcpo2)
    6.37 -
    6.38 -instance "++" :: (pcpo, pcpo) po
    6.39 -by (rule typedef_po [OF type_definition_Ssum less_ssum_def])
    6.40 -
    6.41 -instance "++" :: (pcpo, pcpo) cpo
    6.42 -by (rule typedef_cpo [OF type_definition_Ssum less_ssum_def adm_Ssum])
    6.43 -
    6.44 -instance "++" :: (pcpo, pcpo) pcpo
    6.45 -by (rule typedef_pcpo_UU [OF type_definition_Ssum less_ssum_def UU_Ssum])
    6.46 -
    6.47 -lemmas cont_Rep_Ssum =
    6.48 -  typedef_cont_Rep [OF type_definition_Ssum less_ssum_def adm_Ssum]
    6.49 -
    6.50 -lemmas cont_Abs_Ssum = 
    6.51 -  typedef_cont_Abs [OF type_definition_Ssum less_ssum_def adm_Ssum]
    6.52 -
    6.53 -lemmas Rep_Ssum_strict =
    6.54 -  typedef_Rep_strict [OF type_definition_Ssum less_ssum_def UU_Ssum]
    6.55 -
    6.56 -lemmas Abs_Ssum_strict =
    6.57 -  typedef_Abs_strict [OF type_definition_Ssum less_ssum_def UU_Ssum]
    6.58 -
    6.59  lemma UU_Abs_Ssum: "\<bottom> = Abs_Ssum <\<bottom>, \<bottom>>"
    6.60  by (simp add: Abs_Ssum_strict inst_cprod_pcpo2 [symmetric])
    6.61  
    6.62 @@ -146,16 +113,16 @@
    6.63  subsection {* Ordering properties of @{term sinl} and @{term sinr} *}
    6.64  
    6.65  lemma sinl_less: "(sinl\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x \<sqsubseteq> y)"
    6.66 -by (simp add: less_ssum_def Rep_Ssum_sinl cpair_less)
    6.67 +by (simp add: less_Ssum_def Rep_Ssum_sinl cpair_less)
    6.68  
    6.69  lemma sinr_less: "(sinr\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x \<sqsubseteq> y)"
    6.70 -by (simp add: less_ssum_def Rep_Ssum_sinr cpair_less)
    6.71 +by (simp add: less_Ssum_def Rep_Ssum_sinr cpair_less)
    6.72  
    6.73  lemma sinl_less_sinr: "(sinl\<cdot>x \<sqsubseteq> sinr\<cdot>y) = (x = \<bottom>)"
    6.74 -by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
    6.75 +by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
    6.76  
    6.77  lemma sinr_less_sinl: "(sinr\<cdot>x \<sqsubseteq> sinl\<cdot>y) = (x = \<bottom>)"
    6.78 -by (simp add: less_ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
    6.79 +by (simp add: less_Ssum_def Rep_Ssum_sinl Rep_Ssum_sinr cpair_less eq_UU_iff)
    6.80  
    6.81  subsection {* Chains of strict sums *}
    6.82