equal
deleted
inserted
replaced
160 case WhileTrue thus ?case by (metis Its_Suc) |
160 case WhileTrue thus ?case by (metis Its_Suc) |
161 qed |
161 qed |
162 |
162 |
163 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" |
163 lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" |
164 proof (induction c arbitrary: Q) |
164 proof (induction c arbitrary: Q) |
165 case SKIP show ?case by simp (blast intro:hoaret.Skip) |
165 case SKIP show ?case by (auto intro:hoaret.Skip) |
166 next |
166 next |
167 case Assign show ?case by simp (blast intro:hoaret.Assign) |
167 case Assign show ?case by (auto intro:hoaret.Assign) |
168 next |
168 next |
169 case Seq thus ?case by simp (blast intro:hoaret.Seq) |
169 case Seq thus ?case by (auto intro:hoaret.Seq) |
170 next |
170 next |
171 case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq) |
171 case If thus ?case by (auto intro:hoaret.If hoaret.conseq) |
172 next |
172 next |
173 case (While b c) |
173 case (While b c) |
174 let ?w = "WHILE b DO c" |
174 let ?w = "WHILE b DO c" |
175 let ?T = "Its b c" |
175 let ?T = "Its b c" |
176 have "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> wp\<^sub>t ?w Q s \<and> (\<exists>n. Its b c s n)" |
176 have "\<forall>s. wp\<^sub>t ?w Q s \<longrightarrow> wp\<^sub>t ?w Q s \<and> (\<exists>n. Its b c s n)" |