Added a number of lemmas
authornipkow
Thu Apr 11 08:30:25 1996 +0200 (1996-04-11)
changeset 16555be64540f275
parent 1654 faa643c33ee6
child 1656 cbba49da5139
Added a number of lemmas
src/HOL/Arith.ML
src/HOL/Prod.ML
src/HOL/Prod.thy
src/HOL/simpdata.ML
     1.1 --- a/src/HOL/Arith.ML	Tue Apr 09 12:12:27 1996 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Apr 11 08:30:25 1996 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  (** Difference **)
     1.6  
     1.7 -val diff_0 = diff_def RS def_nat_rec_0;
     1.8 +bind_thm("diff_0", diff_def RS def_nat_rec_0);
     1.9  
    1.10  qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def]
    1.11      "0 - n = 0"
     2.1 --- a/src/HOL/Prod.ML	Tue Apr 09 12:12:27 1996 +0200
     2.2 +++ b/src/HOL/Prod.ML	Thu Apr 11 08:30:25 1996 +0200
     2.3 @@ -110,6 +110,9 @@
     2.4  by (Asm_simp_tac 1);
     2.5  qed "surjective_pairing2";
     2.6  
     2.7 +qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f"
     2.8 +  (fn _ => [rtac ext 1, split_all_tac 1, rtac split 1]);
     2.9 +
    2.10  (*For use with split_tac and the simplifier*)
    2.11  goal Prod.thy "R(split c p) = (! x y. p = (x,y) --> R(c x y))";
    2.12  by (stac surjective_pairing 1);
     3.1 --- a/src/HOL/Prod.thy	Tue Apr 09 12:12:27 1996 +0200
     3.2 +++ b/src/HOL/Prod.thy	Thu Apr 11 08:30:25 1996 +0200
     3.3 @@ -61,7 +61,7 @@
     3.4    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
     3.5    fst_def       "fst(p) == @a. ? b. p = (a, b)"
     3.6    snd_def       "snd(p) == @b. ? a. p = (a, b)"
     3.7 -  split_def     "split c p == c (fst p) (snd p)"
     3.8 +  split_def     "split == (%c p. c (fst p) (snd p))"
     3.9    prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
    3.10    Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    3.11  
     4.1 --- a/src/HOL/simpdata.ML	Tue Apr 09 12:12:27 1996 +0200
     4.2 +++ b/src/HOL/simpdata.ML	Thu Apr 11 08:30:25 1996 +0200
     4.3 @@ -181,3 +181,15 @@
     4.4  prove "de_Morgan_disj" "(~(P | Q)) = (~P & ~Q)";
     4.5  prove "de_Morgan_conj" "(~(P & Q)) = (~P | ~Q)";
     4.6  
     4.7 +prove "ex_disj_distrib" "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))";
     4.8 +prove "all_conj_distrib" "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
     4.9 +
    4.10 +qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
    4.11 +  (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
    4.12 +
    4.13 +qed_goal "if_distrib" HOL.thy
    4.14 +  "f(if c then x else y) = (if c then f x else f y)" 
    4.15 +  (fn _ => [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
    4.16 +
    4.17 +qed_goalw "o_assoc" HOL.thy [o_def] "(f o g) o h = (f o g o h)"
    4.18 +  (fn _=>[rtac ext 1, rtac refl 1]);