equal
deleted
inserted
replaced
17 by (Clarify_tac 1); |
17 by (Clarify_tac 1); |
18 by (case_tac "? us. us <= list & P (ps @ a # us)" 1); |
18 by (case_tac "? us. us <= list & P (ps @ a # us)" 1); |
19 by (Asm_simp_tac 1); |
19 by (Asm_simp_tac 1); |
20 by (subgoal_tac "? us. us <= a # list & P (ps @ us)" 1); |
20 by (subgoal_tac "? us. us <= a # list & P (ps @ us)" 1); |
21 by (Asm_simp_tac 1); |
21 by (Asm_simp_tac 1); |
22 by (blast_tac (claset() addIs [prefix_Cons RS iffD2]) 1); |
22 by (blast_tac (claset() addIs [thm "prefix_Cons" RS iffD2]) 1); |
23 by (subgoal_tac "~P(ps@[a])" 1); |
23 by (subgoal_tac "~P(ps@[a])" 1); |
24 by (Blast_tac 2); |
24 by (Blast_tac 2); |
25 by (Asm_simp_tac 1); |
25 by (Asm_simp_tac 1); |
26 by (case_tac "? us. us <= a#list & P (ps @ us)" 1); |
26 by (case_tac "? us. us <= a#list & P (ps @ us)" 1); |
27 by (Asm_simp_tac 1); |
27 by (Asm_simp_tac 1); |
28 by (Clarify_tac 1); |
28 by (Clarify_tac 1); |
29 by (case_tac "us" 1); |
29 by (case_tac "us" 1); |
30 by (rtac iffI 1); |
30 by (rtac iffI 1); |
31 by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1); |
31 by (asm_full_simp_tac (simpset() addsimps [thm "prefix_Cons", thm "prefix_append"]) 1); |
32 by (Blast_tac 1); |
32 by (Blast_tac 1); |
33 by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1); |
33 by (asm_full_simp_tac (simpset() addsimps [thm "prefix_Cons", thm "prefix_append"]) 1); |
34 by (Clarify_tac 1); |
34 by (Clarify_tac 1); |
35 by (etac disjE 1); |
35 by (etac disjE 1); |
36 by (fast_tac (claset() addDs [prefix_antisym]) 1); |
36 by (fast_tac (claset() addDs [order_antisym]) 1); |
37 by (Clarify_tac 1); |
37 by (Clarify_tac 1); |
38 by (etac disjE 1); |
38 by (etac disjE 1); |
39 by (Clarify_tac 1); |
39 by (Clarify_tac 1); |
40 by (Asm_full_simp_tac 1); |
40 by (Asm_full_simp_tac 1); |
41 by (etac disjE 1); |
41 by (etac disjE 1); |