constdefs -> definition
authorhuffman
Thu Dec 18 11:00:13 2008 -0800 (2008-12-18)
changeset 29141d5582ab1311f
parent 29139 6e0b7b114072
child 29142 98b49d151093
constdefs -> definition
src/HOLCF/Fixrec.thy
src/HOLCF/One.thy
     1.1 --- a/src/HOLCF/Fixrec.thy	Thu Dec 18 09:30:36 2008 -0800
     1.2 +++ b/src/HOLCF/Fixrec.thy	Thu Dec 18 11:00:13 2008 -0800
     1.3 @@ -16,13 +16,13 @@
     1.4  pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set"
     1.5  by simp_all
     1.6  
     1.7 -constdefs
     1.8 -  fail :: "'a maybe"
     1.9 -  "fail \<equiv> Abs_maybe (sinl\<cdot>ONE)"
    1.10 +definition
    1.11 +  fail :: "'a maybe" where
    1.12 +  "fail = Abs_maybe (sinl\<cdot>ONE)"
    1.13  
    1.14 -constdefs
    1.15 +definition
    1.16    return :: "'a \<rightarrow> 'a maybe" where
    1.17 -  "return \<equiv> \<Lambda> x. Abs_maybe (sinr\<cdot>(up\<cdot>x))"
    1.18 +  "return = (\<Lambda> x. Abs_maybe (sinr\<cdot>(up\<cdot>x)))"
    1.19  
    1.20  definition
    1.21    maybe_when :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a maybe \<rightarrow> 'b::pcpo" where
    1.22 @@ -58,7 +58,8 @@
    1.23                    cont_Abs_maybe Abs_maybe_inverse Rep_maybe_strict)
    1.24  
    1.25  translations
    1.26 -  "case m of fail \<Rightarrow> t1 | return\<cdot>x \<Rightarrow> t2" == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
    1.27 +  "case m of XCONST fail \<Rightarrow> t1 | XCONST return\<cdot>x \<Rightarrow> t2"
    1.28 +    == "CONST maybe_when\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m"
    1.29  
    1.30  
    1.31  subsubsection {* Monadic bind operator *}
    1.32 @@ -163,8 +164,8 @@
    1.33  
    1.34  subsection {* Case branch combinator *}
    1.35  
    1.36 -constdefs
    1.37 -  branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)"
    1.38 +definition
    1.39 +  branch :: "('a \<rightarrow> 'b maybe) \<Rightarrow> ('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'c maybe)" where
    1.40    "branch p \<equiv> \<Lambda> r x. bind\<cdot>(p\<cdot>x)\<cdot>(\<Lambda> y. return\<cdot>(r\<cdot>y))"
    1.41  
    1.42  lemma branch_rews:
     2.1 --- a/src/HOLCF/One.thy	Thu Dec 18 09:30:36 2008 -0800
     2.2 +++ b/src/HOLCF/One.thy	Thu Dec 18 11:00:13 2008 -0800
     2.3 @@ -12,8 +12,9 @@
     2.4  translations
     2.5    "one" <= (type) "unit lift" 
     2.6  
     2.7 -constdefs
     2.8 +definition
     2.9    ONE :: "one"
    2.10 +where
    2.11    "ONE == Def ()"
    2.12  
    2.13  text {* Exhaustion and Elimination for type @{typ one} *}