5157

1 
(* Title: ZF/Update.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1998 University of Cambridge


5 


6 
Function updates: like theory Map, but for ordinary functions


7 
*)


8 


9 
open Update;


10 


11 
Goal "f(x:=y) ` z = if(z=x, y, f`z)";


12 
by (simp_tac (simpset() addsimps [update_def]) 1);


13 
by (case_tac "z : domain(f)" 1);


14 
by (Asm_simp_tac 1);


15 
by (asm_simp_tac (simpset() addsimps [apply_0]) 1);


16 
qed "update_apply";


17 
Addsimps [update_apply];


18 


19 
Goalw [update_def] "[ f`x = y; f: Pi(A,B); x: A ] ==> f(x:=y) = f";


20 
by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb]) 1);


21 
by (rtac fun_extension 1);


22 
by (best_tac (claset() addIs [apply_type, if_type, lam_type]) 1);


23 
ba 1;


24 
by (Asm_simp_tac 1);


25 
qed "update_idem";


26 


27 


28 
(* [ f: Pi(A, B); x:A ] ==> f(x := f`x) = f *)


29 
Addsimps [refl RS update_idem];


30 


31 
Goalw [update_def] "domain(f(x:=y)) = cons(x, domain(f))";


32 
by (Asm_simp_tac 1);


33 
qed "domain_update";


34 
Addsimps [domain_update];


35 
