author | paulson |
Wed, 06 May 1998 13:01:30 +0200 | |
changeset 4898 | 68fd1a2b8b7b |
parent 4896 | 4727272f3db6 |
child 5069 | 3ea049f7979d |
permissions | -rw-r--r-- |
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 |
|
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset
|
11 |
goalw thy [update_def] "(f[x:=y] = f) = (f x = y)"; |
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 |
|
4727272f3db6
New syntax for function update; moved to main HOL directory
paulson
parents:
diff
changeset
|
23 |
goal thy "(f[x:=y])z = (if x=z then y else f z)"; |
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]; |