|
5157
|
1 |
(* Title: ZF/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 theory Map, but for ordinary functions
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Update = func +
|
|
|
10 |
|
|
|
11 |
consts
|
|
|
12 |
update :: "[i,i,i] => i"
|
|
|
13 |
|
|
|
14 |
nonterminals
|
|
|
15 |
updbinds updbind
|
|
|
16 |
|
|
|
17 |
syntax
|
|
|
18 |
|
|
|
19 |
(* Let expressions *)
|
|
|
20 |
|
|
|
21 |
"_updbind" :: [i, i] => updbind ("(2_ :=/ _)")
|
|
|
22 |
"" :: updbind => updbinds ("_")
|
|
|
23 |
"_updbinds" :: [updbind, updbinds] => updbinds ("_,/ _")
|
|
|
24 |
"_Update" :: [i, updbinds] => i ("_/'((_)')" [900,0] 900)
|
|
|
25 |
|
|
|
26 |
translations
|
|
|
27 |
"_Update (f, _updbinds(b,bs))" == "_Update (_Update(f,b), bs)"
|
|
|
28 |
"f(x:=y)" == "update(f,x,y)"
|
|
|
29 |
|
|
|
30 |
defs
|
|
|
31 |
update_def "f(a:=b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
|
|
|
32 |
|
|
|
33 |
end
|