equal
deleted
inserted
replaced
164 case (Not b) thus ?case by simp |
164 case (Not b) thus ?case by simp |
165 next |
165 next |
166 case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI) |
166 case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI) |
167 next |
167 next |
168 case (Less e1 e2) thus ?case |
168 case (Less e1 e2) thus ?case |
169 by (auto split: prod.split) |
169 apply hypsubst_thin |
170 (metis afilter_sound filter_less' aval'_sound Less) |
170 apply (auto split: prod.split) |
|
171 apply (metis afilter_sound filter_less' aval'_sound Less) |
|
172 done |
171 qed |
173 qed |
172 |
174 |
173 fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where |
175 fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where |
174 "AI SKIP S = S" | |
176 "AI SKIP S = S" | |
175 "AI (x ::= a) S = |
177 "AI (x ::= a) S = |