equal
deleted
inserted
replaced
95 \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) = |
95 \<Longrightarrow> (p1' @ p2 = drop n p1 @ drop (n - size p1) p2) = |
96 (n \<le> size p1 & p1' = drop n p1)" |
96 (n \<le> size p1 & p1' = drop n p1)" |
97 apply(rule iffI) |
97 apply(rule iffI) |
98 defer apply simp |
98 defer apply simp |
99 apply(subgoal_tac "n \<le> size p1") |
99 apply(subgoal_tac "n \<le> size p1") |
100 apply(rotate_tac -1) |
|
101 apply simp |
100 apply simp |
102 apply(rule ccontr) |
101 apply(rule ccontr) |
103 apply(rotate_tac -1) |
|
104 apply(drule_tac f = length in arg_cong) |
102 apply(drule_tac f = length in arg_cong) |
105 apply simp |
103 apply simp |
106 apply arith |
104 apply arith |
107 done |
105 done |
108 |
106 |