equal
deleted
inserted
replaced
56 one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where |
56 one_case :: "'a::pcpo \<rightarrow> one \<rightarrow> 'a" where |
57 "one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)" |
57 "one_case = (\<Lambda> a x. seq\<cdot>x\<cdot>a)" |
58 |
58 |
59 translations |
59 translations |
60 "case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x" |
60 "case x of XCONST ONE \<Rightarrow> t" == "CONST one_case\<cdot>t\<cdot>x" |
|
61 "case x of XCONST ONE :: 'a \<Rightarrow> t" => "CONST one_case\<cdot>t\<cdot>x" |
61 "\<Lambda> (XCONST ONE). t" == "CONST one_case\<cdot>t" |
62 "\<Lambda> (XCONST ONE). t" == "CONST one_case\<cdot>t" |
62 |
63 |
63 lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>" |
64 lemma one_case1 [simp]: "(case \<bottom> of ONE \<Rightarrow> t) = \<bottom>" |
64 by (simp add: one_case_def) |
65 by (simp add: one_case_def) |
65 |
66 |