23 "fail = Abs_match (sinl\<cdot>ONE)" |
23 "fail = Abs_match (sinl\<cdot>ONE)" |
24 |
24 |
25 definition |
25 definition |
26 succeed :: "'a \<rightarrow> 'a match" where |
26 succeed :: "'a \<rightarrow> 'a match" where |
27 "succeed = (\<Lambda> x. Abs_match (sinr\<cdot>(up\<cdot>x)))" |
27 "succeed = (\<Lambda> x. Abs_match (sinr\<cdot>(up\<cdot>x)))" |
28 |
|
29 definition |
|
30 match_case :: "'b \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a match \<rightarrow> 'b::pcpo" where |
|
31 "match_case = (\<Lambda> f r m. sscase\<cdot>(\<Lambda> x. f)\<cdot>(fup\<cdot>r)\<cdot>(Rep_match m))" |
|
32 |
28 |
33 lemma matchE [case_names bottom fail succeed, cases type: match]: |
29 lemma matchE [case_names bottom fail succeed, cases type: match]: |
34 "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = succeed\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
30 "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = succeed\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
35 unfolding fail_def succeed_def |
31 unfolding fail_def succeed_def |
36 apply (cases p, rename_tac r) |
32 apply (cases p, rename_tac r) |
50 |
46 |
51 lemma succeed_neq_fail [simp]: |
47 lemma succeed_neq_fail [simp]: |
52 "succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x" |
48 "succeed\<cdot>x \<noteq> fail" "fail \<noteq> succeed\<cdot>x" |
53 by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject) |
49 by (simp_all add: succeed_def fail_def cont_Abs_match Abs_match_inject) |
54 |
50 |
55 lemma match_case_simps [simp]: |
|
56 "match_case\<cdot>f\<cdot>r\<cdot>\<bottom> = \<bottom>" |
|
57 "match_case\<cdot>f\<cdot>r\<cdot>fail = f" |
|
58 "match_case\<cdot>f\<cdot>r\<cdot>(succeed\<cdot>x) = r\<cdot>x" |
|
59 by (simp_all add: succeed_def fail_def match_case_def cont_Rep_match |
|
60 cont2cont_LAM |
|
61 cont_Abs_match Abs_match_inverse Rep_match_strict) |
|
62 |
|
63 translations |
|
64 "case m of XCONST fail \<Rightarrow> t1 | XCONST succeed\<cdot>x \<Rightarrow> t2" |
|
65 == "CONST match_case\<cdot>t1\<cdot>(\<Lambda> x. t2)\<cdot>m" |
|
66 |
|
67 subsubsection {* Run operator *} |
51 subsubsection {* Run operator *} |
68 |
52 |
69 definition |
53 definition |
70 run :: "'a match \<rightarrow> 'a::pcpo" where |
54 run :: "'a match \<rightarrow> 'a::pcpo" where |
71 "run = match_case\<cdot>\<bottom>\<cdot>ID" |
55 "run = (\<Lambda> m. sscase\<cdot>\<bottom>\<cdot>(fup\<cdot>ID)\<cdot>(Rep_match m))" |
72 |
56 |
73 text {* rewrite rules for run *} |
57 text {* rewrite rules for run *} |
74 |
58 |
75 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>" |
59 lemma run_strict [simp]: "run\<cdot>\<bottom> = \<bottom>" |
76 by (simp add: run_def) |
60 unfolding run_def |
|
61 by (simp add: cont_Rep_match Rep_match_strict) |
77 |
62 |
78 lemma run_fail [simp]: "run\<cdot>fail = \<bottom>" |
63 lemma run_fail [simp]: "run\<cdot>fail = \<bottom>" |
79 by (simp add: run_def) |
64 unfolding run_def fail_def |
|
65 by (simp add: cont_Rep_match Abs_match_inverse) |
80 |
66 |
81 lemma run_succeed [simp]: "run\<cdot>(succeed\<cdot>x) = x" |
67 lemma run_succeed [simp]: "run\<cdot>(succeed\<cdot>x) = x" |
82 by (simp add: run_def) |
68 unfolding run_def succeed_def |
|
69 by (simp add: cont_Rep_match cont_Abs_match Abs_match_inverse) |
83 |
70 |
84 subsubsection {* Monad plus operator *} |
71 subsubsection {* Monad plus operator *} |
85 |
72 |
86 definition |
73 definition |
87 mplus :: "'a match \<rightarrow> 'a match \<rightarrow> 'a match" where |
74 mplus :: "'a match \<rightarrow> 'a match \<rightarrow> 'a match" where |
88 "mplus = (\<Lambda> m1 m2. case m1 of fail \<Rightarrow> m2 | succeed\<cdot>x \<Rightarrow> m1)" |
75 "mplus = (\<Lambda> m1 m2. sscase\<cdot>(\<Lambda> _. m2)\<cdot>(\<Lambda> _. m1)\<cdot>(Rep_match m1))" |
89 |
76 |
90 abbreviation |
77 abbreviation |
91 mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match" (infixr "+++" 65) where |
78 mplus_syn :: "['a match, 'a match] \<Rightarrow> 'a match" (infixr "+++" 65) where |
92 "m1 +++ m2 == mplus\<cdot>m1\<cdot>m2" |
79 "m1 +++ m2 == mplus\<cdot>m1\<cdot>m2" |
93 |
80 |
94 text {* rewrite rules for mplus *} |
81 text {* rewrite rules for mplus *} |
95 |
82 |
|
83 lemmas cont2cont_Rep_match = cont_Rep_match [THEN cont_compose] |
|
84 |
96 lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>" |
85 lemma mplus_strict [simp]: "\<bottom> +++ m = \<bottom>" |
97 by (simp add: mplus_def) |
86 unfolding mplus_def |
|
87 by (simp add: cont2cont_Rep_match Rep_match_strict) |
98 |
88 |
99 lemma mplus_fail [simp]: "fail +++ m = m" |
89 lemma mplus_fail [simp]: "fail +++ m = m" |
100 by (simp add: mplus_def) |
90 unfolding mplus_def fail_def |
|
91 by (simp add: cont2cont_Rep_match Abs_match_inverse) |
101 |
92 |
102 lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x" |
93 lemma mplus_succeed [simp]: "succeed\<cdot>x +++ m = succeed\<cdot>x" |
103 by (simp add: mplus_def) |
94 unfolding mplus_def succeed_def |
|
95 by (simp add: cont2cont_Rep_match cont_Abs_match Abs_match_inverse) |
104 |
96 |
105 lemma mplus_fail2 [simp]: "m +++ fail = m" |
97 lemma mplus_fail2 [simp]: "m +++ fail = m" |
106 by (cases m, simp_all) |
98 by (cases m, simp_all) |
107 |
99 |
108 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)" |
100 lemma mplus_assoc: "(x +++ y) +++ z = x +++ (y +++ z)" |