equal
deleted
inserted
replaced
|
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]; |