equal
deleted
inserted
replaced
187 lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>" |
187 lemma evalc_None_retrancl [simp, dest!]: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = \<langle>s\<rangle>" |
188 by (induct set: rtrancl) auto |
188 by (induct set: rtrancl) auto |
189 |
189 |
190 (*<*) |
190 (*<*) |
191 (* FIXME: relpow.simps don't work *) |
191 (* FIXME: relpow.simps don't work *) |
192 lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp |
|
193 lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp |
|
194 lemmas [simp del] = relpow.simps |
192 lemmas [simp del] = relpow.simps |
|
193 lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by (simp add: relpow.simps) |
|
194 lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by (simp add: relpow.simps) |
|
195 |
195 (*>*) |
196 (*>*) |
196 lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)" |
197 lemma evalc1_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)" |
197 by (cases n) auto |
198 by (cases n) auto |
198 |
199 |
199 lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" |
200 lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" |