81 by (Clarify_tac 1); |
81 by (Clarify_tac 1); |
82 by (rename_tac "xs1 ys1 xss1 ys" 1); |
82 by (rename_tac "xs1 ys1 xss1 ys" 1); |
83 by (split_asm_tac [list.split_asm] 1); |
83 by (split_asm_tac [list.split_asm] 1); |
84 by (Asm_full_simp_tac 1); |
84 by (Asm_full_simp_tac 1); |
85 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
85 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
86 by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1); |
86 by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1); |
87 by (rtac conjI 1); |
87 by (rtac conjI 1); |
88 by (Clarify_tac 1); |
88 by (Clarify_tac 1); |
89 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
89 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
90 by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1); |
90 by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1); |
91 by (Clarify_tac 1); |
91 by (Clarify_tac 1); |
92 by (rename_tac "us uss" 1); |
92 by (rename_tac "us uss" 1); |
93 by (subgoal_tac "xs1=us" 1); |
93 by (subgoal_tac "xs1=us" 1); |
94 by (Asm_full_simp_tac 1); |
94 by (Asm_full_simp_tac 1); |
95 by (Asm_full_simp_tac 1); |
95 by (Asm_full_simp_tac 1); |
96 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
96 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); |
97 by (blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1); |
97 by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2, order_antisym]) 1); |
98 qed "is_maxchopper_chop"; |
98 qed "is_maxchopper_chop"; |