equal
deleted
inserted
replaced
318 \<comment>\<open>Seq2\<close> |
318 \<comment>\<open>Seq2\<close> |
319 apply(rule cptn_append_is_cptn) |
319 apply(rule cptn_append_is_cptn) |
320 apply(drule_tac P=P1 in lift_is_cptn) |
320 apply(drule_tac P=P1 in lift_is_cptn) |
321 apply(simp add:lift_def) |
321 apply(simp add:lift_def) |
322 apply simp |
322 apply simp |
323 apply(simp split: split_if_asm) |
323 apply(simp split: if_split_asm) |
324 apply(frule_tac P=P1 in last_lift) |
324 apply(frule_tac P=P1 in last_lift) |
325 apply(rule last_fst_esp) |
325 apply(rule last_fst_esp) |
326 apply (simp add:last_length) |
326 apply (simp add:last_length) |
327 apply(simp add:Cons_lift lift_def split_def last_conv_nth) |
327 apply(simp add:Cons_lift lift_def split_def last_conv_nth) |
328 \<comment>\<open>While1\<close> |
328 \<comment>\<open>While1\<close> |
335 apply(rule WhileT,simp) |
335 apply(rule WhileT,simp) |
336 apply(rule cptn_append_is_cptn) |
336 apply(rule cptn_append_is_cptn) |
337 apply(drule_tac P="While b P" in lift_is_cptn) |
337 apply(drule_tac P="While b P" in lift_is_cptn) |
338 apply(simp add:lift_def) |
338 apply(simp add:lift_def) |
339 apply simp |
339 apply simp |
340 apply(simp split: split_if_asm) |
340 apply(simp split: if_split_asm) |
341 apply(frule_tac P="While b P" in last_lift) |
341 apply(frule_tac P="While b P" in last_lift) |
342 apply(rule last_fst_esp,simp add:last_length) |
342 apply(rule last_fst_esp,simp add:last_length) |
343 apply(simp add:Cons_lift lift_def split_def last_conv_nth) |
343 apply(simp add:Cons_lift lift_def split_def last_conv_nth) |
344 done |
344 done |
345 |
345 |