147 apply(erule CPrf.cases) |
151 apply(erule CPrf.cases) |
148 apply(simp_all)[7] |
152 apply(simp_all)[7] |
149 apply(erule CPrf.cases) |
153 apply(erule CPrf.cases) |
150 apply(simp_all)[7] |
154 apply(simp_all)[7] |
151 apply(clarify) |
155 apply(clarify) |
|
156 apply(frule val_ord_shorterE) |
|
157 apply(subst (asm) QQ) |
|
158 apply(erule disjE) |
152 apply(drule val_ord_SeqE) |
159 apply(drule val_ord_SeqE) |
153 apply(erule disjE) |
160 apply(erule disjE) |
154 apply(drule_tac x="v1a" in meta_spec) |
161 apply(drule_tac x="v1a" in meta_spec) |
155 apply(rotate_tac 7) |
162 apply(rotate_tac 8) |
156 apply(drule_tac x="v1b" in meta_spec) |
163 apply(drule_tac x="v1b" in meta_spec) |
157 apply(drule_tac x="flat v1a @ flat v2a @ s'" in meta_spec) |
164 apply(drule_tac x="flat v1a @ flat v2a @ s'" in meta_spec) |
158 apply(simp) |
165 apply(simp) |
159 apply(drule meta_mp) |
166 apply(drule meta_mp) |
160 apply(auto simp add: CPTpre_def)[1] |
167 apply(auto simp add: CPTpre_def)[1] |
161 apply(drule meta_mp) |
168 apply(drule meta_mp) |
162 apply(auto simp add: CPTpre_def)[1] |
169 apply(auto simp add: CPTpre_def)[1] |
163 apply(rule ValOrd.intros) |
170 apply(rule ValOrd.intros(2)) |
|
171 apply(assumption) |
|
172 apply(frule val_ord_shorterE) |
|
173 apply(subst (asm) append_eq_append_conv_if) |
|
174 apply(simp) |
|
175 apply (metis append_assoc append_eq_append_conv_if length_append) |
|
176 |
|
177 |
|
178 thm le |
|
179 apply(clarify) |
|
180 apply(rule ValOrd.intros) |
|
181 apply(simp) |
|
182 |
164 apply(subst (asm) (3) CPTpre_def) |
183 apply(subst (asm) (3) CPTpre_def) |
165 apply(subst (asm) (3) CPTpre_def) |
184 apply(subst (asm) (3) CPTpre_def) |
166 apply(auto)[1] |
185 apply(auto)[1] |
167 apply(drule_tac meta_mp) |
186 apply(drule_tac meta_mp) |
168 apply(auto simp add: CPTpre_def)[1] |
187 apply(auto simp add: CPTpre_def)[1] |