# HG changeset patch
# User paulson
# Date 900666839 -7200
# Node ID 6e03de8ec2b4116be9a43c99460710854b55fe69
# Parent  f23494fa8dc1c7ac6420a0988cf436c64c6f6c87
as in HOL

diff -r f23494fa8dc1 -r 6e03de8ec2b4 src/ZF/Main.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Main.thy	Fri Jul 17 11:13:59 1998 +0200
@@ -0,0 +1,6 @@
+
+(*$Id$
+  theory Main includes everything*)
+
+Main = Update + InfDatatype + List + EquivClass;
+
diff -r f23494fa8dc1 -r 6e03de8ec2b4 src/ZF/Update.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Update.ML	Fri Jul 17 11:13:59 1998 +0200
@@ -0,0 +1,35 @@
+(*  Title:      ZF/Update.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Function updates: like theory Map, but for ordinary functions
+*)
+
+open Update;
+
+Goal "f(x:=y) ` z = if(z=x, y, f`z)";
+by (simp_tac (simpset() addsimps [update_def]) 1);
+by (case_tac "z : domain(f)" 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [apply_0]) 1);
+qed "update_apply";
+Addsimps [update_apply];
+
+Goalw [update_def] "[| f`x = y;  f: Pi(A,B);  x: A |] ==> f(x:=y) = f";
+by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb]) 1);
+by (rtac fun_extension 1);
+by (best_tac (claset() addIs [apply_type, if_type, lam_type]) 1);
+ba 1;
+by (Asm_simp_tac 1);
+qed "update_idem";
+
+
+(* [| f: Pi(A, B); x:A |] ==> f(x := f`x) = f *)
+Addsimps [refl RS update_idem];
+
+Goalw [update_def] "domain(f(x:=y)) = cons(x, domain(f))";
+by (Asm_simp_tac 1);
+qed "domain_update";
+Addsimps [domain_update];
+
diff -r f23494fa8dc1 -r 6e03de8ec2b4 src/ZF/Update.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Update.thy	Fri Jul 17 11:13:59 1998 +0200
@@ -0,0 +1,33 @@
+(*  Title:      ZF/Update.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
+
+Function updates: like theory Map, but for ordinary functions
+*)
+
+Update = func +
+
+consts
+  update  :: "[i,i,i] => i"
+
+nonterminals
+  updbinds  updbind
+
+syntax
+
+  (* Let expressions *)
+
+  "_updbind"       :: [i, i] => updbind             ("(2_ :=/ _)")
+  ""               :: updbind => updbinds             ("_")
+  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
+  "_Update"        :: [i, updbinds] => i            ("_/'((_)')" [900,0] 900)
+
+translations
+  "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"
+  "f(x:=y)"                     == "update(f,x,y)"
+
+defs
+  update_def "f(a:=b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
+
+end