# HG changeset patch
# User nipkow
# Date 829204225 -7200
# Node ID 5be64540f275ccec06441e9b235de06e726d21e7
# Parent  faa643c33ee61c0bd3aff13458512a46e8970200
Added a number of lemmas

diff -r faa643c33ee6 -r 5be64540f275 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Tue Apr 09 12:12:27 1996 +0200
+++ b/src/HOL/Arith.ML	Thu Apr 11 08:30:25 1996 +0200
@@ -27,7 +27,7 @@
 
 (** Difference **)
 
-val diff_0 = diff_def RS def_nat_rec_0;
+bind_thm("diff_0", diff_def RS def_nat_rec_0);
 
 qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def]
     "0 - n = 0"
diff -r faa643c33ee6 -r 5be64540f275 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Tue Apr 09 12:12:27 1996 +0200
+++ b/src/HOL/Prod.ML	Thu Apr 11 08:30:25 1996 +0200
@@ -110,6 +110,9 @@
 by (Asm_simp_tac 1);
 qed "surjective_pairing2";
 
+qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
+  (fn _ => [rtac ext 1, split_all_tac 1, rtac split 1]);
+
 (*For use with split_tac and the simplifier*)
 goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
 by (stac surjective_pairing 1);
diff -r faa643c33ee6 -r 5be64540f275 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Tue Apr 09 12:12:27 1996 +0200
+++ b/src/HOL/Prod.thy	Thu Apr 11 08:30:25 1996 +0200
@@ -61,7 +61,7 @@
   Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
   fst_def       "fst(p) == @a. ? b. p = (a, b)"
   snd_def       "snd(p) == @b. ? a. p = (a, b)"
-  split_def     "split c p == c (fst p) (snd p)"
+  split_def     "split == (%c p. c (fst p) (snd p))"
   prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
   Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
 
diff -r faa643c33ee6 -r 5be64540f275 src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Apr 09 12:12:27 1996 +0200
+++ b/src/HOL/simpdata.ML	Thu Apr 11 08:30:25 1996 +0200
@@ -181,3 +181,15 @@
 prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
 prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
 
+prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";
+prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
+
+qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
+  (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
+
+qed_goal "if_distrib" HOL.thy
+  "f(if c then x else y) = (if c then f x else f y)" 
+  (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
+
+qed_goalw "o_assoc" HOL.thy [o_def] "(f o g) o h = (f o g o h)"
+  (fn _=>[rtac ext 1, rtac refl 1]);