src/HOLCF/Sprod.thy
changeset 35525 fa231b86cb1e
parent 35491 92e0028a46f2
child 35547 991a6af75978
     1.1 --- a/src/HOLCF/Sprod.thy	Tue Mar 02 17:20:03 2010 -0800
     1.2 +++ b/src/HOLCF/Sprod.thy	Tue Mar 02 17:21:10 2010 -0800
     1.3 @@ -12,20 +12,20 @@
     1.4  
     1.5  subsection {* Definition of strict product type *}
     1.6  
     1.7 -pcpodef (Sprod)  ('a, 'b) "**" (infixr "**" 20) =
     1.8 +pcpodef (Sprod)  ('a, 'b) sprod (infixr "**" 20) =
     1.9          "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
    1.10  by simp_all
    1.11  
    1.12 -instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
    1.13 +instance sprod :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
    1.14  by (rule typedef_finite_po [OF type_definition_Sprod])
    1.15  
    1.16 -instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    1.17 +instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    1.18  by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
    1.19  
    1.20  syntax (xsymbols)
    1.21 -  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    1.22 +  sprod          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    1.23  syntax (HTML output)
    1.24 -  "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    1.25 +  sprod          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    1.26  
    1.27  lemma spair_lemma:
    1.28    "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
    1.29 @@ -80,11 +80,11 @@
    1.30  apply fast
    1.31  done
    1.32  
    1.33 -lemma sprodE [cases type: **]:
    1.34 +lemma sprodE [cases type: sprod]:
    1.35    "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    1.36  by (cut_tac z=p in Exh_Sprod, auto)
    1.37  
    1.38 -lemma sprod_induct [induct type: **]:
    1.39 +lemma sprod_induct [induct type: sprod]:
    1.40    "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
    1.41  by (cases x, simp_all)
    1.42  
    1.43 @@ -221,7 +221,7 @@
    1.44  
    1.45  subsection {* Strict product preserves flatness *}
    1.46  
    1.47 -instance "**" :: (flat, flat) flat
    1.48 +instance sprod :: (flat, flat) flat
    1.49  proof
    1.50    fix x y :: "'a \<otimes> 'b"
    1.51    assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
    1.52 @@ -312,7 +312,7 @@
    1.53  
    1.54  subsection {* Strict product is a bifinite domain *}
    1.55  
    1.56 -instantiation "**" :: (bifinite, bifinite) bifinite
    1.57 +instantiation sprod :: (bifinite, bifinite) bifinite
    1.58  begin
    1.59  
    1.60  definition