equal
deleted
inserted
replaced
103 apply auto |
103 apply auto |
104 done |
104 done |
105 |
105 |
106 lemma raise_if_Some2 [simp]: |
106 lemma raise_if_Some2 [simp]: |
107 "raise_if c z (if x = None then Some y else x) \<noteq> None" |
107 "raise_if c z (if x = None then Some y else x) \<noteq> None" |
108 apply (unfold raise_if_def) |
108 unfolding raise_if_def by (induct x) auto |
109 apply(induct_tac "x") |
|
110 apply auto |
|
111 done |
|
112 |
109 |
113 lemma raise_if_SomeD [rule_format (no_asm)]: |
110 lemma raise_if_SomeD [rule_format (no_asm)]: |
114 "raise_if c x y = Some z \<longrightarrow> c \<and> Some z = Some (Addr (XcptRef x)) | y = Some z" |
111 "raise_if c x y = Some z \<longrightarrow> c \<and> Some z = Some (Addr (XcptRef x)) | y = Some z" |
115 apply (unfold raise_if_def) |
112 apply (unfold raise_if_def) |
116 apply auto |
113 apply auto |