Various new lemmas. Improved conversion of equations to rewrite rules:
authornipkow
Thu Oct 16 14:12:15 1997 +0200 (1997-10-16)
changeset 3896ee8ebb74ec00
parent 3895 b2463861c86a
child 3897 7cd00b628e32
Various new lemmas. Improved conversion of equations to rewrite rules:
(s=t becomes (s=t)==True if s=t loops).
src/HOL/Arith.ML
src/HOL/List.ML
src/HOL/List.thy
src/HOL/Set.ML
src/HOL/equalities.ML
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Arith.ML	Thu Oct 16 14:00:20 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Oct 16 14:12:15 1997 +0200
     1.3 @@ -38,6 +38,12 @@
     1.4  by(simp_tac (!simpset setloop (split_tac[expand_nat_case])) 1);
     1.5  qed_spec_mp "pred_le_mono";
     1.6  
     1.7 +goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
     1.8 +by(exhaust_tac "n" 1);
     1.9 +by(ALLGOALS Asm_full_simp_tac);
    1.10 +qed "pred_less";
    1.11 +Addsimps [pred_less];
    1.12 +
    1.13  (** Difference **)
    1.14  
    1.15  qed_goalw "diff_0_eq_0" Arith.thy [pred_def]
     2.1 --- a/src/HOL/List.ML	Thu Oct 16 14:00:20 1997 +0200
     2.2 +++ b/src/HOL/List.ML	Thu Oct 16 14:12:15 1997 +0200
     2.3 @@ -92,6 +92,12 @@
     2.4  qed "length_rev";
     2.5  Addsimps [length_rev];
     2.6  
     2.7 +goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = pred(length xs)";
     2.8 +by(exhaust_tac "xs" 1);
     2.9 +by(ALLGOALS Asm_full_simp_tac);
    2.10 +qed "length_tl";
    2.11 +Addsimps [length_tl];
    2.12 +
    2.13  goal thy "(length xs = 0) = (xs = [])";
    2.14  by (induct_tac "xs" 1);
    2.15  by (ALLGOALS Asm_simp_tac);
    2.16 @@ -167,35 +173,22 @@
    2.17  qed_spec_mp "append_eq_append_conv";
    2.18  Addsimps [append_eq_append_conv];
    2.19  
    2.20 -(* Still needed? Unconditional and hence AddIffs.
    2.21 +goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
    2.22 +by (Simp_tac 1);
    2.23 +qed "same_append_eq";
    2.24  
    2.25 -goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
    2.26 -by (induct_tac "xs" 1);
    2.27 -by (ALLGOALS Asm_simp_tac);
    2.28 -qed "same_append_eq";
    2.29 -AddIffs [same_append_eq];
    2.30 +goal thy "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
    2.31 +by (Simp_tac 1);
    2.32 +qed "append1_eq_conv";
    2.33  
    2.34 -goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
    2.35 -by (induct_tac "xs" 1);
    2.36 - by (rtac allI 1);
    2.37 - by (induct_tac "ys" 1);
    2.38 -  by (ALLGOALS Asm_simp_tac);
    2.39 -by (rtac allI 1);
    2.40 -by (induct_tac "ys" 1);
    2.41 - by (ALLGOALS Asm_simp_tac);
    2.42 -qed_spec_mp "append1_eq_conv";
    2.43 -AddIffs [append1_eq_conv];
    2.44 +goal thy "(ys @ xs = zs @ xs) = (ys=zs)";
    2.45 +by (Simp_tac 1);
    2.46 +qed "append_same_eq";
    2.47  
    2.48 -goal thy "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)";
    2.49 -by (induct_tac "xs" 1);
    2.50 -by (Simp_tac 1);
    2.51 -by (Clarify_tac 1);
    2.52 -by (subgoal_tac "((ys @ [a]) @ list = (zs @ [a]) @ list) = (ys=zs)" 1);
    2.53 -by (Asm_full_simp_tac 1);
    2.54 -by (Blast_tac 1);
    2.55 -qed_spec_mp "append_same_eq";
    2.56 -AddIffs [append_same_eq];
    2.57 -*)
    2.58 +AddSIs
    2.59 + [same_append_eq RS iffD2, append1_eq_conv RS iffD2, append_same_eq RS iffD2];
    2.60 +AddSDs
    2.61 + [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
    2.62  
    2.63  goal thy "xs ~= [] --> hd xs # tl xs = xs";
    2.64  by (induct_tac "xs" 1);
    2.65 @@ -415,6 +408,18 @@
    2.66  qed"concat_append";
    2.67  Addsimps [concat_append];
    2.68  
    2.69 +goal thy "(concat xss = []) = (!xs:set xss. xs=[])";
    2.70 +by(induct_tac "xss" 1);
    2.71 +by(ALLGOALS Asm_simp_tac);
    2.72 +qed "concat_eq_Nil_conv";
    2.73 +AddIffs [concat_eq_Nil_conv];
    2.74 +
    2.75 +goal thy "([] = concat xss) = (!xs:set xss. xs=[])";
    2.76 +by(induct_tac "xss" 1);
    2.77 +by(ALLGOALS Asm_simp_tac);
    2.78 +qed "Nil_eq_concat_conv";
    2.79 +AddIffs [Nil_eq_concat_conv];
    2.80 +
    2.81  goal thy  "set(concat xs) = Union(set `` set xs)";
    2.82  by (induct_tac "xs" 1);
    2.83  by (ALLGOALS Asm_simp_tac);
    2.84 @@ -488,7 +493,47 @@
    2.85  qed_spec_mp "nth_mem";
    2.86  Addsimps [nth_mem];
    2.87  
    2.88 +(** last & butlast **)
    2.89  
    2.90 +goal thy "last(xs@[x]) = x";
    2.91 +by(induct_tac "xs" 1);
    2.92 +by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
    2.93 +qed "last_snoc";
    2.94 +Addsimps [last_snoc];
    2.95 +
    2.96 +goal thy "butlast(xs@[x]) = xs";
    2.97 +by(induct_tac "xs" 1);
    2.98 +by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
    2.99 +qed "butlast_snoc";
   2.100 +Addsimps [butlast_snoc];
   2.101 +
   2.102 +goal thy
   2.103 +  "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
   2.104 +by(induct_tac "xs" 1);
   2.105 +by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
   2.106 +qed_spec_mp "butlast_append";
   2.107 +
   2.108 +goal thy "x:set(butlast xs) --> x:set xs";
   2.109 +by(induct_tac "xs" 1);
   2.110 +by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
   2.111 +qed_spec_mp "in_set_butlastD";
   2.112 +
   2.113 +goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
   2.114 +by(asm_simp_tac (!simpset addsimps [butlast_append]
   2.115 +                          setloop (split_tac[expand_if])) 1);
   2.116 +by(blast_tac (!claset addDs [in_set_butlastD]) 1);
   2.117 +qed "in_set_butlast_appendI1";
   2.118 +
   2.119 +goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
   2.120 +by(asm_simp_tac (!simpset addsimps [butlast_append]
   2.121 +                          setloop (split_tac[expand_if])) 1);
   2.122 +by(Clarify_tac 1);
   2.123 +by(Full_simp_tac 1);
   2.124 +qed "in_set_butlast_appendI2";
   2.125 +(* FIXME
   2.126 +Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2];
   2.127 +AddIs    [in_set_butlast_appendI1,in_set_butlast_appendI2];
   2.128 +*)
   2.129  (** take  & drop **)
   2.130  section "take & drop";
   2.131  
     3.1 --- a/src/HOL/List.thy	Thu Oct 16 14:00:20 1997 +0200
     3.2 +++ b/src/HOL/List.thy	Thu Oct 16 14:12:15 1997 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4    filter      :: ['a => bool, 'a list] => 'a list
     3.5    concat      :: 'a list list => 'a list
     3.6    foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
     3.7 -  hd          :: 'a list => 'a
     3.8 +  hd, last    :: 'a list => 'a
     3.9    set         :: 'a list => 'a set
    3.10    list_all    :: ('a => bool) => ('a list => bool)
    3.11    map         :: ('a=>'b) => ('a list => 'b list)
    3.12 @@ -24,7 +24,7 @@
    3.13    take, drop  :: [nat, 'a list] => 'a list
    3.14    takeWhile,
    3.15    dropWhile   :: ('a => bool) => 'a list => 'a list
    3.16 -  tl,ttl      :: 'a list => 'a list
    3.17 +  tl, butlast :: 'a list => 'a list
    3.18    rev         :: 'a list => 'a list
    3.19    replicate   :: nat => 'a => 'a list
    3.20  
    3.21 @@ -62,12 +62,14 @@
    3.22    "hd([]) = arbitrary"
    3.23    "hd(x#xs) = x"
    3.24  primrec tl list
    3.25 -  "tl([]) = arbitrary"
    3.26 +  "tl([]) = []"
    3.27    "tl(x#xs) = xs"
    3.28 -primrec ttl list
    3.29 -  (* a "total" version of tl: *)
    3.30 -  "ttl([]) = []"
    3.31 -  "ttl(x#xs) = xs"
    3.32 +primrec last list
    3.33 +  "last [] = arbitrary"
    3.34 +  "last(x#xs) = (if xs=[] then x else last xs)"
    3.35 +primrec butlast list
    3.36 +  "butlast [] = []"
    3.37 +  "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
    3.38  primrec "op mem" list
    3.39    "x mem [] = False"
    3.40    "x mem (y#ys) = (if y=x then True else x mem ys)"
     4.1 --- a/src/HOL/Set.ML	Thu Oct 16 14:00:20 1997 +0200
     4.2 +++ b/src/HOL/Set.ML	Thu Oct 16 14:12:15 1997 +0200
     4.3 @@ -601,6 +601,7 @@
     4.4  val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
     4.5  by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
     4.6  qed "image_eqI";
     4.7 +(* FIXME: Addsimps [image_eqI];*)
     4.8  
     4.9  bind_thm ("imageI", refl RS image_eqI);
    4.10  
     5.1 --- a/src/HOL/equalities.ML	Thu Oct 16 14:00:20 1997 +0200
     5.2 +++ b/src/HOL/equalities.ML	Thu Oct 16 14:12:15 1997 +0200
     5.3 @@ -625,6 +625,11 @@
     5.4  by (Blast_tac 1);
     5.5  qed "subset_iff_psubset_eq";
     5.6  
     5.7 +goal Set.thy "(!x. x ~: A) = (A={})";
     5.8 +by(Blast_tac 1);
     5.9 +qed "all_not_in_conv";
    5.10 +(* FIXME: AddIffs [all_not_in_conv]; *)
    5.11 +
    5.12  goalw Set.thy [Pow_def] "Pow {} = {{}}";
    5.13  by (Auto_tac());
    5.14  qed "Pow_empty";
     6.1 --- a/src/HOL/simpdata.ML	Thu Oct 16 14:00:20 1997 +0200
     6.2 +++ b/src/HOL/simpdata.ML	Thu Oct 16 14:12:15 1997 +0200
     6.3 @@ -80,9 +80,14 @@
     6.4  
     6.5  in
     6.6  
     6.7 -  fun mk_meta_eq r = case concl_of r of
     6.8 +  fun mk_meta_eq r = r RS eq_reflection;
     6.9 +
    6.10 +  fun mk_meta_eq_simp r = case concl_of r of
    6.11            Const("==",_)$_$_ => r
    6.12 -      |   _$(Const("op =",_)$_$_) => r RS eq_reflection
    6.13 +      |   _$(Const("op =",_)$lhs$rhs) =>
    6.14 +             (case fst(Logic.loops (#sign(rep_thm r)) (prems_of r) lhs rhs) of
    6.15 +                None => mk_meta_eq r
    6.16 +              | Some _ => r RS P_imp_P_eq_True)
    6.17        |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
    6.18        |   _ => r RS P_imp_P_eq_True;
    6.19    (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
    6.20 @@ -114,7 +119,7 @@
    6.21  fun Addcongs congs = (simpset := !simpset addcongs congs);
    6.22  fun Delcongs congs = (simpset := !simpset delcongs congs);
    6.23  
    6.24 -fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
    6.25 +fun mksimps pairs = map mk_meta_eq_simp o atomize pairs o gen_all;
    6.26  
    6.27  val imp_cong = impI RSN
    6.28      (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"