src/HOLCF/Sprod.thy
changeset 16699 24b494ff8f0f
parent 16553 aa36d41e4263
child 16751 7af6723ad741
     1.1 --- a/src/HOLCF/Sprod.thy	Wed Jul 06 00:06:34 2005 +0200
     1.2 +++ b/src/HOLCF/Sprod.thy	Wed Jul 06 00:07:34 2005 +0200
     1.3 @@ -8,55 +8,22 @@
     1.4  header {* The type of strict products *}
     1.5  
     1.6  theory Sprod
     1.7 -imports Cprod TypedefPcpo
     1.8 +imports Cprod
     1.9  begin
    1.10  
    1.11  defaultsort pcpo
    1.12  
    1.13  subsection {* Definition of strict product type *}
    1.14  
    1.15 -typedef (Sprod)  ('a, 'b) "**" (infixr 20) =
    1.16 +pcpodef (Sprod)  ('a, 'b) "**" (infixr 20) =
    1.17          "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
    1.18 -by (auto simp add: inst_cprod_pcpo)
    1.19 +by simp
    1.20  
    1.21  syntax (xsymbols)
    1.22    "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
    1.23  syntax (HTML output)
    1.24    "**"		:: "[type, type] => type"	 ("(_ \<otimes>/ _)" [21,20] 20)
    1.25  
    1.26 -subsection {* Class instances *}
    1.27 -
    1.28 -instance "**" :: (pcpo, pcpo) sq_ord ..
    1.29 -defs (overloaded)
    1.30 -  less_sprod_def: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep_Sprod x \<sqsubseteq> Rep_Sprod y"
    1.31 -
    1.32 -lemma adm_Sprod: "adm (\<lambda>x. x \<in> Sprod)"
    1.33 -by (simp add: Sprod_def)
    1.34 -
    1.35 -lemma UU_Sprod: "\<bottom> \<in> Sprod"
    1.36 -by (simp add: Sprod_def)
    1.37 -
    1.38 -instance "**" :: (pcpo, pcpo) po
    1.39 -by (rule typedef_po [OF type_definition_Sprod less_sprod_def])
    1.40 -
    1.41 -instance "**" :: (pcpo, pcpo) cpo
    1.42 -by (rule typedef_cpo [OF type_definition_Sprod less_sprod_def adm_Sprod])
    1.43 -
    1.44 -instance "**" :: (pcpo, pcpo) pcpo
    1.45 -by (rule typedef_pcpo_UU [OF type_definition_Sprod less_sprod_def UU_Sprod])
    1.46 -
    1.47 -lemmas cont_Rep_Sprod =
    1.48 -  typedef_cont_Rep [OF type_definition_Sprod less_sprod_def adm_Sprod]
    1.49 -
    1.50 -lemmas cont_Abs_Sprod = 
    1.51 -  typedef_cont_Abs [OF type_definition_Sprod less_sprod_def adm_Sprod]
    1.52 -
    1.53 -lemmas Rep_Sprod_strict =
    1.54 -  typedef_Rep_strict [OF type_definition_Sprod less_sprod_def UU_Sprod]
    1.55 -
    1.56 -lemmas Abs_Sprod_strict =
    1.57 -  typedef_Abs_strict [OF type_definition_Sprod less_sprod_def UU_Sprod]
    1.58 -
    1.59  lemma UU_Abs_Sprod: "\<bottom> = Abs_Sprod <\<bottom>, \<bottom>>"
    1.60  by (simp add: Abs_Sprod_strict inst_cprod_pcpo2 [symmetric])
    1.61  
    1.62 @@ -178,7 +145,7 @@
    1.63  by (rule_tac p=p in sprodE, simp_all)
    1.64  
    1.65  lemma less_sprod: "p1 \<sqsubseteq> p2 = (sfst\<cdot>p1 \<sqsubseteq> sfst\<cdot>p2 \<and> ssnd\<cdot>p1 \<sqsubseteq> ssnd\<cdot>p2)"
    1.66 -apply (simp add: less_sprod_def sfst_def ssnd_def cont_Rep_Sprod)
    1.67 +apply (simp add: less_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
    1.68  apply (rule less_cprod)
    1.69  done
    1.70