equal
deleted
inserted
replaced
130 next |
130 next |
131 case (And b1 b2) thus ?case |
131 case (And b1 b2) thus ?case |
132 by simp (metis And(1) And(2) in_gamma_sup_UpI) |
132 by simp (metis And(1) And(2) in_gamma_sup_UpI) |
133 next |
133 next |
134 case (Less e1 e2) thus ?case |
134 case (Less e1 e2) thus ?case |
135 by(auto split: prod.split) |
135 apply hypsubst_thin |
136 (metis (lifting) inv_aval'_correct aval''_correct inv_less') |
136 apply (auto split: prod.split) |
|
137 apply (metis (lifting) inv_aval'_correct aval''_correct inv_less') |
|
138 done |
137 qed |
139 qed |
138 |
140 |
139 definition "step' = Step |
141 definition "step' = Step |
140 (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))) |
142 (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S))) |
141 (\<lambda>b S. inv_bval' b True S)" |
143 (\<lambda>b S. inv_bval' b True S)" |