# HG changeset patch # User nipkow # Date 900758469 -7200 # Node ID e7457679e26df01e9b88769f419da3bf388466b7 # Parent 1ff6679144b90e3fca1ed3a6bb82a8856eb4f27c Simplified last proof. diff -r 1ff6679144b9 -r e7457679e26d src/HOL/Lex/MaxChop.ML --- a/src/HOL/Lex/MaxChop.ML Fri Jul 17 11:25:20 1998 +0200 +++ b/src/HOL/Lex/MaxChop.ML Sat Jul 18 12:41:09 1998 +0200 @@ -80,26 +80,22 @@ by (Clarify_tac 1); by (assume_tac 1); by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1); - by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem] +by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem] addsplits [split_split]) 1); by (Clarify_tac 1); -by (rtac conjI 1); - by (Clarify_tac 1); - by (exhaust_tac "yss" 1); - by (Asm_simp_tac 1); +by(rename_tac "xs1 ys1 xss1 ys" 1); +by(split_asm_tac [split_list_case_asm] 1); by (Asm_full_simp_tac 1); by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1); -by (exhaust_tac "yss" 1); - by (Asm_full_simp_tac 1); +by (rtac conjI 1); + by (Clarify_tac 1); by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1); by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -by (subgoal_tac "x=a" 1); - by (Clarify_tac 1); +by(rename_tac "us uss" 1); +by (subgoal_tac "xs1=us" 1); by (Asm_full_simp_tac 1); -by (rotate_tac ~2 1); by (Asm_full_simp_tac 1); by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1); by (blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1);