More lemmas, esp. ~Bex and ~Ball conversions.

--- a/src/HOL/List.ML	Tue Oct 14 12:41:11 1997 +0200
+++ b/src/HOL/List.ML	Tue Oct 14 13:58:47 1997 +0200
@@ -69,6 +69,47 @@
   impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
 
 
+(** length **)
+(* needs to come before "@" because of thm append_eq_append_conv *)
+
+section "length";
+
+goal thy "length(xs@ys) = length(xs)+length(ys)";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed"length_append";
+Addsimps [length_append];
+
+goal thy "length (map f l) = length l";
+by (induct_tac "l" 1);
+by (ALLGOALS Simp_tac);
+qed "length_map";
+Addsimps [length_map];
+
+goal thy "length(rev xs) = length(xs)";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "length_rev";
+Addsimps [length_rev];
+
+goal thy "(length xs = 0) = (xs = [])";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "length_0_conv";
+AddIffs [length_0_conv];
+
+goal thy "(0 = length xs) = (xs = [])";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "zero_length_conv";
+AddIffs [zero_length_conv];
+
+goal thy "(0 < length xs) = (xs ~= [])";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "length_greater_0_conv";
+AddIffs [length_greater_0_conv];
+
 (** @ - append **)
 
 section "@ - append";
@@ -110,6 +151,24 @@
 qed "self_append_conv";
 AddIffs [append_self_conv,self_append_conv];
 
+goal thy "!ys. length xs = length ys | length us = length vs \
+\              --> (xs@us = ys@vs) = (xs=ys & us=vs)";
+by(induct_tac "xs" 1);
+ by(rtac allI 1);
+ by(exhaust_tac "ys" 1);
+  by(Asm_simp_tac 1);
+ by(fast_tac (!claset addIs [less_add_Suc2] addss !simpset
+                      addEs [less_not_refl2 RSN (2,rev_notE)]) 1);
+by(rtac allI 1);
+by(exhaust_tac "ys" 1);
+ by(fast_tac (!claset addIs [less_add_Suc2] addss !simpset
+                      addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
+by(Asm_simp_tac 1);
+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 (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
@@ -136,6 +195,7 @@
 by (Blast_tac 1);
 qed_spec_mp "append_same_eq";
 AddIffs [append_same_eq];
+*)
 
 goal thy "xs ~= [] --> hd xs # tl xs = xs";
 by (induct_tac "xs" 1);
@@ -208,6 +268,19 @@
 val lemma = result();
 bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
 
+goal List.thy "(map f xs = []) = (xs = [])";
+by(induct_tac "xs" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "map_is_Nil_conv";
+AddIffs [map_is_Nil_conv];
+
+goal List.thy "([] = map f xs) = (xs = [])";
+by(induct_tac "xs" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "Nil_is_map_conv";
+AddIffs [Nil_is_map_conv];
+
+
 (** rev **)
 
 section "rev";
@@ -224,6 +297,18 @@
 qed "rev_rev_ident";
 Addsimps[rev_rev_ident];
 
+goal thy "(rev xs = []) = (xs = [])";
+by(induct_tac "xs" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "rev_is_Nil_conv";
+AddIffs [rev_is_Nil_conv];
+
+goal thy "([] = rev xs) = (xs = [])";
+by(induct_tac "xs" 1);
+by(ALLGOALS Asm_simp_tac);
+qed "Nil_is_rev_conv";
+AddIffs [Nil_is_rev_conv];
+
 
 (** mem **)
 
@@ -351,41 +436,6 @@
 by (ALLGOALS Asm_simp_tac);
 qed "rev_concat";
 
-(** length **)
-
-section "length";
-
-goal thy "length(xs@ys) = length(xs)+length(ys)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed"length_append";
-Addsimps [length_append];
-
-goal thy "length (map f l) = length l";
-by (induct_tac "l" 1);
-by (ALLGOALS Simp_tac);
-qed "length_map";
-Addsimps [length_map];
-
-goal thy "length(rev xs) = length(xs)";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "length_rev";
-Addsimps [length_rev];
-
-goal thy "(length xs = 0) = (xs = [])";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "length_0_conv";
-AddIffs [length_0_conv];
-
-goal thy "(0 < length xs) = (xs ~= [])";
-by (induct_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "length_greater_0_conv";
-AddIffs [length_greater_0_conv];
-
-
 (** nth **)
 
 section "nth";

--- a/src/HOL/equalities.ML	Tue Oct 14 12:41:11 1997 +0200
+++ b/src/HOL/equalities.ML	Tue Oct 14 13:58:47 1997 +0200
@@ -103,9 +103,6 @@
 by (Blast_tac 1);
 qed "image_range";
 
-qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
- (fn _ => [Blast_tac 1]);
-
 goal Set.thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
 by (Blast_tac 1);
 qed "insert_image";
@@ -521,8 +518,8 @@
 
 section"Bounded quantifiers";
 
-(** These are not added to the default simpset because (a) they duplicate the
-    body and (b) there are no similar rules for Int. **)
+(** The following are not added to the default simpset because
+    (a) they duplicate the body and (b) there are no similar rules for Int. **)
 
 goal Set.thy "(ALL x:A Un B. P x) = ((ALL x:A. P x) & (ALL x:B. P x))";
 by (Blast_tac 1);
@@ -686,7 +683,9 @@
      "(ALL x:{}. P x) = True",
      "(ALL x:insert a B. P x) = (P(a) & (ALL x:B. P x))",
      "(ALL x:Union(A). P x) = (ALL y:A. ALL x:y. P x)",
-     "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)"];
+     "(ALL x:Collect Q. P x) = (ALL x. Q x --> P x)",
+     "(ALL x:f``A. P x) = (ALL x:A. P(f x))",
+     "(~(ALL x:A. P x)) = (EX x:A. ~P x)"];
 
 val ball_conj_distrib = 
     prover "(ALL x:A. P x & Q x) = ((ALL x:A. P x) & (ALL x:A. Q x))";
@@ -697,7 +696,9 @@
      "(EX x:{}. P x) = False",
      "(EX x:insert a B. P x) = (P(a) | (EX x:B. P x))",
      "(EX x:Union(A). P x) = (EX y:A. EX x:y.  P x)",
-     "(EX x:Collect Q. P x) = (EX x. Q x & P x)"];
+     "(EX x:Collect Q. P x) = (EX x. Q x & P x)",
+     "(EX x:f``A. P x) = (EX x:A. P(f x))",
+     "(~(EX x:A. P x)) = (ALL x:A. ~P x)"];
 
 val bex_disj_distrib = 
     prover "(EX x:A. P x | Q x) = ((EX x:A. P x) | (EX x:A. Q x))";