author  wenzelm 
Mon, 22 Jun 1998 17:26:46 +0200  
changeset 5069  3ea049f7979d 
parent 4898  68fd1a2b8b7b 
child 5070  c42429b3e2f2 
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 

5069  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 

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

18 
(* f x = y ==> f[x:=y] = f *) 
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 

5069  23 
Goal "(f[x:=y])z = (if x=z 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]; 