equal
deleted
inserted
replaced
1 theory Relational |
1 theory Relational |
2 imports Array Ref |
2 imports Array Ref |
3 begin |
3 begin |
4 |
|
5 lemma crel_assert_eq: "(\<And>h h' r. crel f h h' r \<Longrightarrow> P r) \<Longrightarrow> f \<guillemotright>= assert P = f" |
|
6 unfolding crel_def bind_def Let_def assert_def |
|
7 raise_def return_def prod_case_beta |
|
8 apply (cases f) |
|
9 apply simp |
|
10 apply (simp add: expand_fun_eq split_def) |
|
11 apply (auto split: option.split) |
|
12 done |
|
13 |
|
14 lemma crel_option_caseI: |
|
15 assumes "\<And>y. x = Some y \<Longrightarrow> crel (s y) h h' r" |
|
16 assumes "x = None \<Longrightarrow> crel n h h' r" |
|
17 shows "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r" |
|
18 using assms |
|
19 by (auto split: option.split) |
|
20 |
|
21 lemma crelI2: |
|
22 assumes "\<exists>h' rs'. crel f h h' rs' \<and> (\<exists>h'' rs. crel (g rs') h' h'' rs)" |
|
23 shows "\<exists>h'' rs. crel (f\<guillemotright>= g) h h'' rs" |
|
24 oops |
|
25 |
|
26 lemma crel_ifI2: |
|
27 assumes "c \<Longrightarrow> \<exists>h' r. crel t h h' r" |
|
28 "\<not> c \<Longrightarrow> \<exists>h' r. crel e h h' r" |
|
29 shows "\<exists> h' r. crel (if c then t else e) h h' r" |
|
30 oops |
|
31 |
4 |
32 lemma crel_option_case: |
5 lemma crel_option_case: |
33 assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r" |
6 assumes "crel (case x of None \<Rightarrow> n | Some y \<Rightarrow> s y) h h' r" |
34 obtains "x = None" "crel n h h' r" |
7 obtains "x = None" "crel n h h' r" |
35 | y where "x = Some y" "crel (s y) h h' r" |
8 | y where "x = Some y" "crel (s y) h h' r" |