# HG changeset patch
# User nipkow
# Date 877003935 -7200
# Node ID ee8ebb74ec00db3d8945c41c83130ae69a9b7add
# Parent  b2463861c86ae6b92d40a4d89e01d3ecaa1e8361
Various new lemmas. Improved conversion of equations to rewrite rules:
(s=t becomes (s=t)==True if s=t loops).

diff -r b2463861c86a -r ee8ebb74ec00 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Thu Oct 16 14:00:20 1997 +0200
+++ b/src/HOL/Arith.ML	Thu Oct 16 14:12:15 1997 +0200
@@ -38,6 +38,12 @@
 by(simp_tac (!simpset setloop (split_tac[expand_nat_case])) 1);
 qed_spec_mp "pred_le_mono";
 
+goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
+by(exhaust_tac "n" 1);
+by(ALLGOALS Asm_full_simp_tac);
+qed "pred_less";
+Addsimps [pred_less];
+
 (** Difference **)
 
 qed_goalw "diff_0_eq_0" Arith.thy [pred_def]
diff -r b2463861c86a -r ee8ebb74ec00 src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Oct 16 14:00:20 1997 +0200
+++ b/src/HOL/List.ML	Thu Oct 16 14:12:15 1997 +0200
@@ -92,6 +92,12 @@
 qed "length_rev";
 Addsimps [length_rev];
 
+goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = pred(length xs)";
+by(exhaust_tac "xs" 1);
+by(ALLGOALS Asm_full_simp_tac);
+qed "length_tl";
+Addsimps [length_tl];
+
 goal thy "(length xs = 0) = (xs = [])";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -167,35 +173,22 @@
 qed_spec_mp "append_eq_append_conv";
 Addsimps [append_eq_append_conv];
 
-(* Still needed? Unconditional and hence AddIffs.
+goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
+by (Simp_tac 1);
+qed "same_append_eq";
 
-goal thy "(xs @ ys = xs @ zs) = (ys=zs)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "same_append_eq";
-AddIffs [same_append_eq];
+goal thy "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
+by (Simp_tac 1);
+qed "append1_eq_conv";
 
-goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
-by (induct_tac "xs" 1);
- by (rtac allI 1);
- by (induct_tac "ys" 1);
-  by (ALLGOALS Asm_simp_tac);
-by (rtac allI 1);
-by (induct_tac "ys" 1);
- by (ALLGOALS Asm_simp_tac);
-qed_spec_mp "append1_eq_conv";
-AddIffs [append1_eq_conv];
+goal thy "(ys @ xs = zs @ xs) = (ys=zs)";
+by (Simp_tac 1);
+qed "append_same_eq";
 
-goal thy "!ys zs. (ys @ xs = zs @ xs) = (ys=zs)";
-by (induct_tac "xs" 1);
-by (Simp_tac 1);
-by (Clarify_tac 1);
-by (subgoal_tac "((ys @ [a]) @ list = (zs @ [a]) @ list) = (ys=zs)" 1);
-by (Asm_full_simp_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "append_same_eq";
-AddIffs [append_same_eq];
-*)
+AddSIs
+ [same_append_eq RS iffD2, append1_eq_conv RS iffD2, append_same_eq RS iffD2];
+AddSDs
+ [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
 
 goal thy "xs ~= [] --> hd xs # tl xs = xs";
 by (induct_tac "xs" 1);
@@ -415,6 +408,18 @@
 qed"concat_append";
 Addsimps [concat_append];
 
+goal thy "(concat xss = []) = (!xs:set xss. xs=[])";
+by(induct_tac "xss" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "concat_eq_Nil_conv";
+AddIffs [concat_eq_Nil_conv];
+
+goal thy "([] = concat xss) = (!xs:set xss. xs=[])";
+by(induct_tac "xss" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "Nil_eq_concat_conv";
+AddIffs [Nil_eq_concat_conv];
+
 goal thy  "set(concat xs) = Union(set `` set xs)";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -488,7 +493,47 @@
 qed_spec_mp "nth_mem";
 Addsimps [nth_mem];
 
+(** last & butlast **)
 
+goal thy "last(xs@[x]) = x";
+by(induct_tac "xs" 1);
+by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
+qed "last_snoc";
+Addsimps [last_snoc];
+
+goal thy "butlast(xs@[x]) = xs";
+by(induct_tac "xs" 1);
+by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
+qed "butlast_snoc";
+Addsimps [butlast_snoc];
+
+goal thy
+  "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
+by(induct_tac "xs" 1);
+by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
+qed_spec_mp "butlast_append";
+
+goal thy "x:set(butlast xs) --> x:set xs";
+by(induct_tac "xs" 1);
+by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac[expand_if]))));
+qed_spec_mp "in_set_butlastD";
+
+goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
+by(asm_simp_tac (!simpset addsimps [butlast_append]
+                          setloop (split_tac[expand_if])) 1);
+by(blast_tac (!claset addDs [in_set_butlastD]) 1);
+qed "in_set_butlast_appendI1";
+
+goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
+by(asm_simp_tac (!simpset addsimps [butlast_append]
+                          setloop (split_tac[expand_if])) 1);
+by(Clarify_tac 1);
+by(Full_simp_tac 1);
+qed "in_set_butlast_appendI2";
+(* FIXME
+Addsimps [in_set_butlast_appendI1,in_set_butlast_appendI2];
+AddIs    [in_set_butlast_appendI1,in_set_butlast_appendI2];
+*)
 (** take  & drop **)
 section "take & drop";
 
diff -r b2463861c86a -r ee8ebb74ec00 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Oct 16 14:00:20 1997 +0200
+++ b/src/HOL/List.thy	Thu Oct 16 14:12:15 1997 +0200
@@ -15,7 +15,7 @@
   filter      :: ['a => bool, 'a list] => 'a list
   concat      :: 'a list list => 'a list
   foldl       :: [['b,'a] => 'b, 'b, 'a list] => 'b
-  hd          :: 'a list => 'a
+  hd, last    :: 'a list => 'a
   set         :: 'a list => 'a set
   list_all    :: ('a => bool) => ('a list => bool)
   map         :: ('a=>'b) => ('a list => 'b list)
@@ -24,7 +24,7 @@
   take, drop  :: [nat, 'a list] => 'a list
   takeWhile,
   dropWhile   :: ('a => bool) => 'a list => 'a list
-  tl,ttl      :: 'a list => 'a list
+  tl, butlast :: 'a list => 'a list
   rev         :: 'a list => 'a list
   replicate   :: nat => 'a => 'a list
 
@@ -62,12 +62,14 @@
   "hd([]) = arbitrary"
   "hd(x#xs) = x"
 primrec tl list
-  "tl([]) = arbitrary"
+  "tl([]) = []"
   "tl(x#xs) = xs"
-primrec ttl list
-  (* a "total" version of tl: *)
-  "ttl([]) = []"
-  "ttl(x#xs) = xs"
+primrec last list
+  "last [] = arbitrary"
+  "last(x#xs) = (if xs=[] then x else last xs)"
+primrec butlast list
+  "butlast [] = []"
+  "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
 primrec "op mem" list
   "x mem [] = False"
   "x mem (y#ys) = (if y=x then True else x mem ys)"
diff -r b2463861c86a -r ee8ebb74ec00 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Oct 16 14:00:20 1997 +0200
+++ b/src/HOL/Set.ML	Thu Oct 16 14:12:15 1997 +0200
@@ -601,6 +601,7 @@
 val prems = goalw thy [image_def] "[| b=f(x);  x:A |] ==> b : f``A";
 by (REPEAT (resolve_tac (prems @ [CollectI,bexI,prem]) 1));
 qed "image_eqI";
+(* FIXME: Addsimps [image_eqI];*)
 
 bind_thm ("imageI", refl RS image_eqI);
 
diff -r b2463861c86a -r ee8ebb74ec00 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Thu Oct 16 14:00:20 1997 +0200
+++ b/src/HOL/equalities.ML	Thu Oct 16 14:12:15 1997 +0200
@@ -625,6 +625,11 @@
 by (Blast_tac 1);
 qed "subset_iff_psubset_eq";
 
+goal Set.thy "(!x. x ~: A) = (A={})";
+by(Blast_tac 1);
+qed "all_not_in_conv";
+(* FIXME: AddIffs [all_not_in_conv]; *)
+
 goalw Set.thy [Pow_def] "Pow {} = {{}}";
 by (Auto_tac());
 qed "Pow_empty";
diff -r b2463861c86a -r ee8ebb74ec00 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Thu Oct 16 14:00:20 1997 +0200
+++ b/src/HOL/simpdata.ML	Thu Oct 16 14:12:15 1997 +0200
@@ -80,9 +80,14 @@
 
 in
 
-  fun mk_meta_eq r = case concl_of r of
+  fun mk_meta_eq r = r RS eq_reflection;
+
+  fun mk_meta_eq_simp r = case concl_of r of
           Const("==",_)$_$_ => r
-      |   _$(Const("op =",_)$_$_) => r RS eq_reflection
+      |   _$(Const("op =",_)$lhs$rhs) =>
+             (case fst(Logic.loops (#sign(rep_thm r)) (prems_of r) lhs rhs) of
+                None => mk_meta_eq r
+              | Some _ => r RS P_imp_P_eq_True)
       |   _$(Const("Not",_)$_) => r RS not_P_imp_P_eq_False
       |   _ => r RS P_imp_P_eq_True;
   (* last 2 lines requires all formulae to be of the from Trueprop(.) *)
@@ -114,7 +119,7 @@
 fun Addcongs congs = (simpset := !simpset addcongs congs);
 fun Delcongs congs = (simpset := !simpset delcongs congs);
 
-fun mksimps pairs = map mk_meta_eq o atomize pairs o gen_all;
+fun mksimps pairs = map mk_meta_eq_simp o atomize pairs o gen_all;
 
 val imp_cong = impI RSN
     (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P-->Q) = (P'-->Q'))"