equal
deleted
inserted
replaced
185 case SKIP thus ?case by fastforce |
185 case SKIP thus ?case by fastforce |
186 next |
186 next |
187 case Assign thus ?case |
187 case Assign thus ?case |
188 by (auto simp: lookup_update aval'_sound) |
188 by (auto simp: lookup_update aval'_sound) |
189 next |
189 next |
190 case Semi thus ?case by fastforce |
190 case Seq thus ?case by fastforce |
191 next |
191 next |
192 case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound) |
192 case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound) |
193 next |
193 next |
194 case (While b c) |
194 case (While b c) |
195 let ?P = "pfp (\<lambda>S. AI c (bfilter b True S)) S" |
195 let ?P = "pfp (\<lambda>S. AI c (bfilter b True S)) S" |