equal
deleted
inserted
replaced
111 next |
111 next |
112 case IfFalse thus ?thesis by blast |
112 case IfFalse thus ?thesis by blast |
113 qed |
113 qed |
114 qed |
114 qed |
115 |
115 |
|
116 (* Using rule inversion to prove simplification rules: *) |
|
117 lemma assign_simp: |
|
118 "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))" |
|
119 by auto |
116 |
120 |
117 subsection "Command Equivalence" |
121 subsection "Command Equivalence" |
118 |
122 |
119 text {* |
123 text {* |
120 We call two statements @{text c} and @{text c'} equivalent wrt.\ the |
124 We call two statements @{text c} and @{text c'} equivalent wrt.\ the |