src/HOL/Lex/Prefix.ML
changeset 5619 76a8c72e3fd4
parent 5609 03d74c85a818
child 6675 63e53327f5e5
equal deleted inserted replaced
5618:721671c68324 5619:76a8c72e3fd4
    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";