equal
deleted
inserted
replaced
112 fix b c and s::state |
112 fix b c and s::state |
113 assume b: "\<not>bval b s" |
113 assume b: "\<not>bval b s" |
114 let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP" |
114 let ?if = "IF b THEN c; WHILE b DO c ELSE SKIP" |
115 have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast |
115 have "(WHILE b DO c,s) \<rightarrow> (?if, s)" by blast |
116 moreover have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b) |
116 moreover have "(?if,s) \<rightarrow> (SKIP, s)" by (simp add: b) |
117 ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by (metis refl step) |
117 ultimately show "(WHILE b DO c,s) \<rightarrow>* (SKIP,s)" by(metis star.refl star.step) |
118 next |
118 next |
119 fix b c s s' t |
119 fix b c s s' t |
120 let ?w = "WHILE b DO c" |
120 let ?w = "WHILE b DO c" |
121 let ?if = "IF b THEN c; ?w ELSE SKIP" |
121 let ?if = "IF b THEN c; ?w ELSE SKIP" |
122 assume w: "(?w,s') \<rightarrow>* (SKIP,t)" |
122 assume w: "(?w,s') \<rightarrow>* (SKIP,t)" |
135 next |
135 next |
136 case Assign show ?case by blast |
136 case Assign show ?case by blast |
137 next |
137 next |
138 case Semi thus ?case by (blast intro: semi_comp) |
138 case Semi thus ?case by (blast intro: semi_comp) |
139 next |
139 next |
140 case IfTrue thus ?case by (blast intro: step) |
140 case IfTrue thus ?case by (blast intro: star.step) |
141 next |
141 next |
142 case IfFalse thus ?case by (blast intro: step) |
142 case IfFalse thus ?case by (blast intro: star.step) |
143 next |
143 next |
144 case WhileFalse thus ?case |
144 case WhileFalse thus ?case |
145 by (metis step step1 small_step.IfFalse small_step.While) |
145 by (metis star.step star_step1 small_step.IfFalse small_step.While) |
146 next |
146 next |
147 case WhileTrue |
147 case WhileTrue |
148 thus ?case |
148 thus ?case |
149 by(metis While semi_comp small_step.IfTrue step[of small_step]) |
149 by(metis While semi_comp small_step.IfTrue star.step[of small_step]) |
150 qed |
150 qed |
151 |
151 |
152 lemma small1_big_continue: |
152 lemma small1_big_continue: |
153 "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t" |
153 "cs \<rightarrow> cs' \<Longrightarrow> cs' \<Rightarrow> t \<Longrightarrow> cs \<Rightarrow> t" |
154 apply (induction arbitrary: t rule: small_step.induct) |
154 apply (induction arbitrary: t rule: small_step.induct) |