src/HOL/Fun.ML
changeset 5305 513925de8962
parent 5148 74919e8f221c
child 5306 3d1368a3a2a2
     1.1 --- a/src/HOL/Fun.ML	Wed Aug 12 16:21:18 1998 +0200
     1.2 +++ b/src/HOL/Fun.ML	Wed Aug 12 16:23:25 1998 +0200
     1.3 @@ -7,6 +7,17 @@
     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 @@ -160,3 +171,35 @@
    1.22  
    1.23  
    1.24  val set_cs = claset() delrules [equalityI];
    1.25 +
    1.26 +
    1.27 +section "fun_upd";
    1.28 +
    1.29 +Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
    1.30 +by Safe_tac;
    1.31 +by (etac subst 1);
    1.32 +by (rtac ext 2);
    1.33 +by Auto_tac;
    1.34 +qed "fun_upd_idem_iff";
    1.35 +
    1.36 +(* f x = y ==> f(x:=y) = f *)
    1.37 +bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
    1.38 +
    1.39 +(* f(x := f x) = f *)
    1.40 +AddIffs [refl RS fun_upd_idem];
    1.41 +
    1.42 +Goal "(f(x:=y))z = (if z=x then y else f z)";
    1.43 +by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
    1.44 +qed "fun_upd_apply";
    1.45 +Addsimps [fun_upd_apply];
    1.46 +
    1.47 +qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 
    1.48 +	(K [Simp_tac 1]);
    1.49 +qed_goal "fund_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
    1.50 +	(K [Asm_simp_tac 1]);
    1.51 +(*Addsimps [fun_upd_same, fun_upd_other];*)
    1.52 +
    1.53 +Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
    1.54 +by (rtac ext 1);
    1.55 +by (Auto_tac);
    1.56 +qed "fun_upd_twist";