src/HOL/List.ML
changeset 5283 0027ddfbc831
parent 5281 f4d16517b360
child 5296 bdef7d349d27
     1.1 --- a/src/HOL/List.ML	Sat Aug 08 14:12:25 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Mon Aug 10 11:30:12 1998 +0200
     1.3 @@ -915,6 +915,30 @@
     1.4  by(Simp_tac 1);
     1.5  qed "lexico_conv";
     1.6  
     1.7 +Goal "([],ys) ~: lex r";
     1.8 +by(simp_tac (simpset() addsimps [lex_conv]) 1);
     1.9 +qed "Nil_notin_lex";
    1.10 +
    1.11 +Goal "(xs,[]) ~: lex r";
    1.12 +by(simp_tac (simpset() addsimps [lex_conv]) 1);
    1.13 +qed "Nil2_notin_lex";
    1.14 +
    1.15 +AddIffs [Nil_notin_lex,Nil2_notin_lex];
    1.16 +
    1.17 +Goal "((x#xs,y#ys) : lex r) = \
    1.18 +\     ((x,y) : r & length xs = length ys | x=y & (xs,ys) : lex r)";
    1.19 +by(simp_tac (simpset() addsimps [lex_conv]) 1);
    1.20 +br iffI 1;
    1.21 + by(blast_tac (claset() addIs [Cons_eq_appendI]) 2);
    1.22 +by(REPEAT(eresolve_tac [conjE, exE] 1));
    1.23 +by(exhaust_tac "xys" 1);
    1.24 +by(Asm_full_simp_tac 1);
    1.25 +by(Asm_full_simp_tac 1);
    1.26 +by(Blast_tac 1);
    1.27 +qed "Cons_in_lex";
    1.28 +AddIffs [Cons_in_lex];
    1.29 +
    1.30 +
    1.31  (***
    1.32  Simplification procedure for all list equalities.
    1.33  Currently only tries to rearranges @ to see if