author  nipkow 
Mon, 13 Jul 1998 16:04:22 +0200  
changeset 5133  42a7fe39a63a 
parent 5070  c42429b3e2f2 
child 5154  40fd46f3d3a1 
permissions  rwrr 
4898  1 
(* Title: HOL/Update.thy 
4896
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

2 
ID: $Id$ 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

4 
Copyright 1998 University of Cambridge 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

5 

4898  6 
Function updates: like theory Map, but for ordinary functions 
4896
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

7 
*) 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

8 

4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

9 
open Update; 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

10 

5070  11 
Goalw [update_def] "(f(x:=y) = f) = (f x = y)"; 
4896
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

12 
by Safe_tac; 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

13 
by (etac subst 1); 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

14 
by (rtac ext 2); 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

15 
by Auto_tac; 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

16 
qed "update_idem_iff"; 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

17 

5070  18 
(* f x = y ==> f(x:=y) = f *) 
4896
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

19 
bind_thm("update_idem", update_idem_iff RS iffD2); 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

20 

4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

21 
AddIffs [refl RS update_idem]; 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

22 

5133  23 
Goal "(f(x:=y))z = (if z=x then y else f z)"; 
4896
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

24 
by (simp_tac (simpset() addsimps [update_def]) 1); 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

25 
qed "update_apply"; 
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset

26 
Addsimps [update_apply]; 