equal
deleted
inserted
replaced
85 by (asm_full_simp_tac (simpset() delsimps [append_assoc] |
85 by (asm_full_simp_tac (simpset() delsimps [append_assoc] |
86 addsimps [append_assoc RS sym])1); |
86 addsimps [append_assoc RS sym])1); |
87 by (Simp_tac 1); |
87 by (Simp_tac 1); |
88 by (Blast_tac 1); |
88 by (Blast_tac 1); |
89 qed "prefix_append"; |
89 qed "prefix_append"; |
|
90 |
|
91 Goalw [prefix_def] |
|
92 "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"; |
|
93 by (auto_tac(claset(), simpset() addsimps [nth_append])); |
|
94 by (exhaust_tac "ys" 1); |
|
95 by Auto_tac; |
|
96 qed "append_one_prefix"; |
|
97 |
|
98 Goalw [prefix_def] "xs <= ys ==> length xs <= length ys"; |
|
99 by Auto_tac; |
|
100 qed "prefix_length_le"; |