prefer cpodef without extra definition;
authorwenzelm
Wed Nov 30 17:30:01 2011 +0100 (2011-11-30)
changeset 45695b108b3d7c49e
parent 45694 4a8743618257
child 45696 476ad865f125
prefer cpodef without extra definition;
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Sprod.thy
src/HOL/HOLCF/Ssum.thy
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Wed Nov 30 16:27:10 2011 +0100
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Wed Nov 30 17:30:01 2011 +0100
     1.3 @@ -13,8 +13,10 @@
     1.4  
     1.5  subsection {* Definition of continuous function type *}
     1.6  
     1.7 -cpodef ('a, 'b) cfun (infixr "->" 0) = "{f::'a => 'b. cont f}"
     1.8 -by (auto intro: cont_const adm_cont)
     1.9 +definition "cfun = {f::'a => 'b. cont f}"
    1.10 +
    1.11 +cpodef (open) ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
    1.12 +  unfolding cfun_def by (auto intro: cont_const adm_cont)
    1.13  
    1.14  type_notation (xsymbols)
    1.15    cfun  ("(_ \<rightarrow>/ _)" [1, 0] 0)
     2.1 --- a/src/HOL/HOLCF/Sprod.thy	Wed Nov 30 16:27:10 2011 +0100
     2.2 +++ b/src/HOL/HOLCF/Sprod.thy	Wed Nov 30 17:30:01 2011 +0100
     2.3 @@ -13,9 +13,10 @@
     2.4  
     2.5  subsection {* Definition of strict product type *}
     2.6  
     2.7 -pcpodef ('a, 'b) sprod (infixr "**" 20) =
     2.8 -        "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
     2.9 -by simp_all
    2.10 +definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
    2.11 +
    2.12 +pcpodef (open) ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set"
    2.13 +  unfolding sprod_def by simp_all
    2.14  
    2.15  instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    2.16  by (rule typedef_chfin [OF type_definition_sprod below_sprod_def])
     3.1 --- a/src/HOL/HOLCF/Ssum.thy	Wed Nov 30 16:27:10 2011 +0100
     3.2 +++ b/src/HOL/HOLCF/Ssum.thy	Wed Nov 30 17:30:01 2011 +0100
     3.3 @@ -13,11 +13,14 @@
     3.4  
     3.5  subsection {* Definition of strict sum type *}
     3.6  
     3.7 -pcpodef ('a, 'b) ssum (infixr "++" 10) = 
     3.8 -  "{p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
     3.9 -    (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
    3.10 -    (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>) }"
    3.11 -by simp_all
    3.12 +definition
    3.13 +  "ssum =
    3.14 +    {p :: tr \<times> ('a \<times> 'b). p = \<bottom> \<or>
    3.15 +      (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
    3.16 +      (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
    3.17 +
    3.18 +pcpodef (open) ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
    3.19 +  unfolding ssum_def by simp_all
    3.20  
    3.21  instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    3.22  by (rule typedef_chfin [OF type_definition_ssum below_ssum_def])