added theorems Id_o, o_Id
authoroheimb
Wed Aug 12 16:49:25 1998 +0200 (1998-08-12)
changeset 53063d1368a3a2a2
parent 5305 513925de8962
child 5307 6a699d5cdef4
added theorems Id_o, o_Id
corrected name of theorem: fund_upd_other -> fun_upd_other
src/HOL/Fun.ML
     1.1 --- a/src/HOL/Fun.ML	Wed Aug 12 16:23:25 1998 +0200
     1.2 +++ b/src/HOL/Fun.ML	Wed Aug 12 16:49:25 1998 +0200
     1.3 @@ -7,17 +7,6 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
     1.8 - (K [rtac refl 1]);
     1.9 -Addsimps [o_apply];
    1.10 -
    1.11 -qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
    1.12 -  (K [rtac ext 1, rtac refl 1]);
    1.13 -
    1.14 -Goalw [o_def] "(f o g)``r = f``(g``r)";
    1.15 -by (Blast_tac 1);
    1.16 -qed "image_compose";
    1.17 -
    1.18  Goal "(f = g) = (!x. f(x)=g(x))";
    1.19  by (rtac iffI 1);
    1.20  by (Asm_simp_tac 1);
    1.21 @@ -42,6 +31,30 @@
    1.22  qed "bchoice";
    1.23  
    1.24  
    1.25 +section "o";
    1.26 +
    1.27 +qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
    1.28 + (K [rtac refl 1]);
    1.29 +Addsimps [o_apply];
    1.30 +
    1.31 +qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
    1.32 +  (K [rtac ext 1, rtac refl 1]);
    1.33 +
    1.34 +qed_goalw "Id_o" thy [Id_def] "Id o g = g"
    1.35 + (K [rtac ext 1, Simp_tac 1]);
    1.36 +Addsimps [Id_o];
    1.37 +
    1.38 +qed_goalw "o_Id" thy [Id_def] "f o Id = f"
    1.39 + (K [rtac ext 1, Simp_tac 1]);
    1.40 +Addsimps [o_Id];
    1.41 +
    1.42 +Goalw [o_def] "(f o g)``r = f``(g``r)";
    1.43 +by (Blast_tac 1);
    1.44 +qed "image_compose";
    1.45 +
    1.46 +
    1.47 +section "inj";
    1.48 +
    1.49  (*** inj(f): f is a one-to-one function ***)
    1.50  
    1.51  val prems = goalw thy [inj_def]
    1.52 @@ -195,7 +208,7 @@
    1.53  
    1.54  qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 
    1.55  	(K [Simp_tac 1]);
    1.56 -qed_goal "fund_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
    1.57 +qed_goal "fun_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
    1.58  	(K [Asm_simp_tac 1]);
    1.59  (*Addsimps [fun_upd_same, fun_upd_other];*)
    1.60