Added some lemmas.
authornipkow
Tue Feb 24 10:44:53 1998 +0100 (1998-02-24)
changeset 464742af8ae6e2c1
parent 4646 f6298426f5a7
child 4648 f04da668581c
Added some lemmas.
src/HOL/Lex/Prefix.ML
src/HOL/List.ML
     1.1 --- a/src/HOL/Lex/Prefix.ML	Mon Feb 23 11:24:49 1998 +0100
     1.2 +++ b/src/HOL/Lex/Prefix.ML	Tue Feb 24 10:44:53 1998 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  goalw thy [prefix_def] "xs <= (xs::'a list)";
     1.5  by(Simp_tac 1);
     1.6  qed "prefix_refl";
     1.7 -Addsimps[prefix_refl];
     1.8 +AddIffs[prefix_refl];
     1.9  
    1.10  goalw thy [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
    1.11  by(Clarify_tac 1);
    1.12 @@ -34,7 +34,7 @@
    1.13  goalw Prefix.thy [prefix_def] "[] <= xs";
    1.14  by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
    1.15  qed "Nil_prefix";
    1.16 -Addsimps[Nil_prefix];
    1.17 +AddIffs[Nil_prefix];
    1.18  
    1.19  goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
    1.20  by (list.induct_tac "xs" 1);
    1.21 @@ -65,6 +65,15 @@
    1.22  qed"Cons_prefix_Cons";
    1.23  Addsimps [Cons_prefix_Cons];
    1.24  
    1.25 +goal thy "(xs@ys <= xs@zs) = (ys <= zs)";
    1.26 +by (induct_tac "xs" 1);
    1.27 +by(ALLGOALS Asm_simp_tac);
    1.28 +qed "same_prefix_prefix";
    1.29 +Addsimps [same_prefix_prefix];
    1.30 +
    1.31 +AddIffs
    1.32 + [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
    1.33 +
    1.34  goalw thy [prefix_def] "!!xs. xs <= ys ==> xs <= ys@zs";
    1.35  by(Clarify_tac 1);
    1.36  by (Simp_tac 1);
    1.37 @@ -79,3 +88,13 @@
    1.38  by (Simp_tac 1);
    1.39  by (Fast_tac 1);
    1.40  qed "prefix_Cons";
    1.41 +
    1.42 +goal thy "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
    1.43 +by(res_inst_tac [("xs","zs")] snoc_induct 1);
    1.44 + by(Simp_tac 1);
    1.45 + by(Blast_tac 1);
    1.46 +by(asm_full_simp_tac (simpset() delsimps [append_assoc]
    1.47 +                                addsimps [append_assoc RS sym])1);
    1.48 +by(Simp_tac 1);
    1.49 +by(Blast_tac 1);
    1.50 +qed "prefix_append";
     2.1 --- a/src/HOL/List.ML	Mon Feb 23 11:24:49 1998 +0100
     2.2 +++ b/src/HOL/List.ML	Tue Feb 24 10:44:53 1998 +0100
     2.3 @@ -180,6 +180,18 @@
     2.4  AddSDs
     2.5   [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
     2.6  
     2.7 +goal thy "(xs @ ys = ys) = (xs=[])";
     2.8 +by(cut_inst_tac [("zs","[]")] append_same_eq 1);
     2.9 +by(Asm_full_simp_tac 1);
    2.10 +qed "append_self_conv2";
    2.11 +
    2.12 +goal thy "(ys = xs @ ys) = (xs=[])";
    2.13 +by(simp_tac (simpset() addsimps
    2.14 +     [simplify (simpset()) (read_instantiate[("ys","[]")]append_same_eq)]) 1);
    2.15 +by(Blast_tac 1);
    2.16 +qed "self_append_conv2";
    2.17 +AddIffs [append_self_conv2,self_append_conv2];
    2.18 +
    2.19  goal thy "xs ~= [] --> hd xs # tl xs = xs";
    2.20  by (induct_tac "xs" 1);
    2.21  by (ALLGOALS Asm_simp_tac);