# HG changeset patch
# User paulson
# Date 1022246669 -7200
# Node ID ba734cc2887d998b12b40be40b66e11670878369
# Parent  312bd350579bf7958a7615f5be7f33ce40d4f75c
converted Update to Isar

diff -r 312bd350579b -r ba734cc2887d src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Fri May 24 13:15:37 2002 +0200
+++ b/src/ZF/IsaMakefile	Fri May 24 15:24:29 2002 +0200
@@ -43,7 +43,7 @@
   Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
   Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
   Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
-  Trancl.ML Trancl.thy Univ.thy Update.ML Update.thy \
+  Trancl.ML Trancl.thy Univ.thy Update.thy \
   WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy	\
   ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML		\
   subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
diff -r 312bd350579b -r ba734cc2887d src/ZF/Update.ML
--- a/src/ZF/Update.ML	Fri May 24 13:15:37 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-(*  Title:      ZF/Update.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1998  University of Cambridge
-
-Function updates: like theory Map, but for ordinary functions
-*)
-
-Goal "f(x:=y) ` z = (if z=x then y else 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);
-by (assume_tac 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];
-
-Goalw [update_def] "[| f: A -> B;  x : A;  y: B |] ==> f(x:=y) : A -> B";
-by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb, 
-				      apply_funtype, lam_type]) 1);
-qed "update_type";
-
-
diff -r 312bd350579b -r ba734cc2887d src/ZF/Update.thy
--- a/src/ZF/Update.thy	Fri May 24 13:15:37 2002 +0200
+++ b/src/ZF/Update.thy	Fri May 24 15:24:29 2002 +0200
@@ -6,10 +6,11 @@
 Function updates: like theory Map, but for ordinary functions
 *)
 
-Update = func +
+theory Update = func:
 
-consts
+constdefs
   update  :: "[i,i,i] => i"
+   "update(f,a,b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
 
 nonterminals
   updbinds  updbind
@@ -18,16 +19,50 @@
 
   (* Let expressions *)
 
-  "_updbind"       :: [i, i] => updbind             ("(2_ :=/ _)")
-  ""               :: updbind => updbinds             ("_")
-  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
-  "_Update"        :: [i, updbinds] => i            ("_/'((_)')" [900,0] 900)
+  "_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)"
+  "f(x:=y)"                       == "update(f,x,y)"
+
+
+lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)"
+apply (simp add: update_def)
+apply (rule_tac P="z \<in> domain(f)" in case_split_thm)   
+apply (simp_all add: apply_0)
+done
+
+lemma update_idem: "[| f`x = y;  f: Pi(A,B);  x: A |] ==> f(x:=y) = f"
+apply (unfold update_def)
+apply (simp add: domain_of_fun cons_absorb)
+apply (rule fun_extension)
+apply (best intro: apply_type if_type lam_type, assumption)
+apply simp
+done
+
 
-defs
-  update_def "f(a:=b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
+(* [| f: Pi(A, B); x:A |] ==> f(x := f`x) = f *)
+declare refl [THEN update_idem, simp]
+
+lemma domain_update [simp]: "domain(f(x:=y)) = cons(x, domain(f))"
+by (unfold update_def, simp)
+
+lemma update_type: "[| f: A -> B;  x : A;  y: B |] ==> f(x:=y) : A -> B"
+apply (unfold update_def)
+apply (simp add: domain_of_fun cons_absorb apply_funtype lam_type)
+done
+
+ML
+{*
+val update_def = thm "update_def";
+val update_apply = thm "update_apply";
+val update_idem = thm "update_idem";
+val domain_update = thm "domain_update";
+val update_type = thm "update_type";
+*}
+
 
 end