src/HOLCF/Fixrec.thy
changeset 28891 f199def7a6a5
parent 26046 1624b3304bb9
child 29063 7619f0561cd7
     1.1 --- a/src/HOLCF/Fixrec.thy	Tue Nov 25 23:28:06 2008 +0100
     1.2 +++ b/src/HOLCF/Fixrec.thy	Tue Nov 25 23:29:01 2008 +0100
     1.3 @@ -89,7 +89,7 @@
     1.4  subsubsection {* Run operator *}
     1.5  
     1.6  definition
     1.7 -  run:: "'a maybe \<rightarrow> 'a::pcpo" where
     1.8 +  run :: "'a maybe \<rightarrow> 'a::pcpo" where
     1.9    "run = maybe_when\<cdot>\<bottom>\<cdot>ID"
    1.10  
    1.11  text {* rewrite rules for run *}
    1.12 @@ -177,6 +177,22 @@
    1.13  lemma branch_return [simp]: "branch return\<cdot>r\<cdot>x = return\<cdot>(r\<cdot>x)"
    1.14  by (simp add: branch_def)
    1.15  
    1.16 +subsubsection {* Cases operator *}
    1.17 +
    1.18 +definition
    1.19 +  cases :: "'a maybe \<rightarrow> 'a::pcpo" where
    1.20 +  "cases = maybe_when\<cdot>\<bottom>\<cdot>ID"
    1.21 +
    1.22 +text {* rewrite rules for cases *}
    1.23 +
    1.24 +lemma cases_strict [simp]: "cases\<cdot>\<bottom> = \<bottom>"
    1.25 +by (simp add: cases_def)
    1.26 +
    1.27 +lemma cases_fail [simp]: "cases\<cdot>fail = \<bottom>"
    1.28 +by (simp add: cases_def)
    1.29 +
    1.30 +lemma cases_return [simp]: "cases\<cdot>(return\<cdot>x) = x"
    1.31 +by (simp add: cases_def)
    1.32  
    1.33  subsection {* Case syntax *}
    1.34  
    1.35 @@ -193,7 +209,7 @@
    1.36    "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    1.37  
    1.38  translations
    1.39 -  "_Case_syntax x ms" == "CONST Fixrec.run\<cdot>(ms\<cdot>x)"
    1.40 +  "_Case_syntax x ms" == "CONST Fixrec.cases\<cdot>(ms\<cdot>x)"
    1.41    "_Case2 m ms" == "m \<parallel> ms"
    1.42  
    1.43  text {* Parsing Case expressions *}
    1.44 @@ -411,7 +427,7 @@
    1.45  
    1.46  definition
    1.47    lazy_pat :: "('a \<rightarrow> 'b::pcpo maybe) \<Rightarrow> ('a \<rightarrow> 'b maybe)" where
    1.48 -  "lazy_pat p = (\<Lambda> x. return\<cdot>(run\<cdot>(p\<cdot>x)))"
    1.49 +  "lazy_pat p = (\<Lambda> x. return\<cdot>(cases\<cdot>(p\<cdot>x)))"
    1.50  
    1.51  text {* Parse translations (patterns) *}
    1.52  translations
    1.53 @@ -433,7 +449,7 @@
    1.54  
    1.55  text {* Lazy patterns in lambda abstractions *}
    1.56  translations
    1.57 -  "_cabs (_lazy_pat p) r" == "CONST Fixrec.run oo (_Case1 (_lazy_pat p) r)"
    1.58 +  "_cabs (_lazy_pat p) r" == "CONST Fixrec.cases oo (_Case1 (_lazy_pat p) r)"
    1.59  
    1.60  lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
    1.61  by (simp add: branch_def wild_pat_def)
    1.62 @@ -566,6 +582,6 @@
    1.63  
    1.64  use "Tools/fixrec_package.ML"
    1.65  
    1.66 -hide (open) const return bind fail run
    1.67 +hide (open) const return bind fail run cases
    1.68  
    1.69  end