equal
deleted
inserted
replaced
24 lemma maybeE: |
24 lemma maybeE: |
25 "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
25 "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; p = fail \<Longrightarrow> Q; \<And>x. p = return\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q" |
26 apply (unfold fail_def return_def) |
26 apply (unfold fail_def return_def) |
27 apply (rule_tac p=p in ssumE, simp) |
27 apply (rule_tac p=p in ssumE, simp) |
28 apply (rule_tac p=x in oneE, simp, simp) |
28 apply (rule_tac p=x in oneE, simp, simp) |
29 apply (rule_tac p=y in upE1, simp, simp) |
29 apply (rule_tac p=y in upE, simp, simp) |
30 done |
30 done |
31 |
31 |
32 subsection {* Monadic bind operator *} |
32 subsection {* Monadic bind operator *} |
33 |
33 |
34 constdefs |
34 constdefs |