|
4776
|
1 |
(* Title: HOL/UNITY/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 the standard theory Map, but for ordinary functions
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
open Update;
|
|
|
10 |
|
|
|
11 |
goalw thy [update_def] "(f[x|->y] = f) = (f x = y)";
|
|
|
12 |
by Safe_tac;
|
|
|
13 |
by (etac subst 1);
|
|
|
14 |
by (rtac ext 2);
|
|
|
15 |
by Auto_tac;
|
|
|
16 |
qed "update_idem_iff";
|
|
|
17 |
|
|
|
18 |
(* f x = y ==> f[x|->y] = f *)
|
|
|
19 |
bind_thm("update_idem", update_idem_iff RS iffD2);
|
|
|
20 |
|
|
|
21 |
AddIffs [refl RS update_idem];
|
|
|
22 |
|
|
|
23 |
goal thy "(f[x|->y])z = (if x=z then y else f z)";
|
|
|
24 |
by (simp_tac (simpset() addsimps [update_def]) 1);
|
|
|
25 |
qed "update_apply";
|
|
|
26 |
Addsimps [update_apply];
|