# HG changeset patch
# User oheimb
# Date 902931805 -7200
# Node ID 513925de8962c4cb7cdabea95b1cae068514302a
# Parent  c133f16febc72df10ac7ffd17743dba3fa6434ac
cleanup for Fun.thy:
merged Update.{thy|ML} into Fun.{thy|ML}
moved o_def from HOL.thy to Fun.thy
added Id_def to Fun.thy
moved image_compose from Set.ML to Fun.ML
moved o_apply and o_assoc from simpdata.ML to Fun.ML
moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML
added fun_upd_twist to Fun.ML

diff -r c133f16febc7 -r 513925de8962 src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Wed Aug 12 16:21:18 1998 +0200
+++ b/src/HOL/Fun.ML	Wed Aug 12 16:23:25 1998 +0200
@@ -7,6 +7,17 @@
 *)
 
 
+qed_goalw "o_apply" thy [o_def] "(f o g) x = f (g x)"
+ (K [rtac refl 1]);
+Addsimps [o_apply];
+
+qed_goalw "o_assoc" thy [o_def] "f o (g o h) = f o g o h"
+  (K [rtac ext 1, rtac refl 1]);
+
+Goalw [o_def] "(f o g)``r = f``(g``r)";
+by (Blast_tac 1);
+qed "image_compose";
+
 Goal "(f = g) = (!x. f(x)=g(x))";
 by (rtac iffI 1);
 by (Asm_simp_tac 1);
@@ -160,3 +171,35 @@
 
 
 val set_cs = claset() delrules [equalityI];
+
+
+section "fun_upd";
+
+Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
+by Safe_tac;
+by (etac subst 1);
+by (rtac ext 2);
+by Auto_tac;
+qed "fun_upd_idem_iff";
+
+(* f x = y ==> f(x:=y) = f *)
+bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
+
+(* f(x := f x) = f *)
+AddIffs [refl RS fun_upd_idem];
+
+Goal "(f(x:=y))z = (if z=x then y else f z)";
+by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
+qed "fun_upd_apply";
+Addsimps [fun_upd_apply];
+
+qed_goal "fun_upd_same" thy "(f(x:=y)) x = y" 
+	(K [Simp_tac 1]);
+qed_goal "fund_upd_other" thy "!!X. z~=x ==> (f(x:=y)) z = f z"
+	(K [Asm_simp_tac 1]);
+(*Addsimps [fun_upd_same, fun_upd_other];*)
+
+Goal "a ~= c ==> m(a:=b)(c:=d) = m(c:=d)(a:=b)";
+by (rtac ext 1);
+by (Auto_tac);
+qed "fun_upd_twist";
diff -r c133f16febc7 -r 513925de8962 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Aug 12 16:21:18 1998 +0200
+++ b/src/HOL/Fun.thy	Wed Aug 12 16:23:25 1998 +0200
@@ -12,15 +12,37 @@
                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
 consts
 
+  Id          ::  'a => 'a
+  o           :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
   inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
   inj_on      :: ['a => 'b, 'a set] => bool
   inv         :: ('a => 'b) => ('b => 'a)
+  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+
+nonterminals
+  updbinds  updbind
+
+syntax
+
+  (* Let expressions *)
+
+  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
+  ""               :: updbind => updbinds             ("_")
+  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
+  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
+
+translations
+  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
+  "f(x:=y)"                     == "fun_upd f x y"
 
 defs
 
-  inj_def     "inj f          == ! x y. f(x)=f(y) --> x=y"
-  inj_on_def  "inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
-  surj_def    "surj f         == ! y. ? x. y=f(x)"
-  inv_def     "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
+  Id_def	"Id             == %x. x"
+  o_def   	"f o g          == %x. f(g(x))"
+  inj_def	"inj f          == ! x y. f(x)=f(y) --> x=y"
+  inj_on_def	"inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
+  surj_def	"surj f         == ! y. ? x. y=f(x)"
+  inv_def	"inv(f::'a=>'b) == % y. @x. f(x)=y"
+  fun_upd_def	"f(a:=b)        == % x. if x=a then b else f x"
 
 end
diff -r c133f16febc7 -r 513925de8962 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Aug 12 16:21:18 1998 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 12 16:23:25 1998 +0200
@@ -47,7 +47,6 @@
 
   (* Infixes *)
 
-  o             :: ['b => 'c, 'a => 'b, 'a] => 'c   (infixl 55)
   "="           :: ['a, 'a] => bool                 (infixl 50)
   "&"           :: [bool, bool] => bool             (infixr 35)
   "|"           :: [bool, bool] => bool             (infixr 30)
@@ -180,7 +179,6 @@
 defs
   (*misc definitions*)
   Let_def       "Let s f == f(s)"
-  o_def         "(f::'b=>'c) o g == (%(x::'a). f(g(x)))"
   if_def        "If P x y == @z::'a. (P=True --> z=x) & (P=False --> z=y)"
 
   (*arbitrary is completely unspecified, but is made to appear as a
diff -r c133f16febc7 -r 513925de8962 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Aug 12 16:21:18 1998 +0200
+++ b/src/HOL/IsaMakefile	Wed Aug 12 16:23:25 1998 +0200
@@ -52,7 +52,7 @@
   Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
   Tools/inductive_package.ML Tools/primrec_package.ML Tools/record_package.ML \
   Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
-  Update.ML Update.thy Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
+  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML \
   WF_Rel.thy arith_data.ML cladata.ML equalities.ML \
   equalities.thy hologic.ML mono.ML mono.thy simpdata.ML subset.ML \
   subset.thy thy_syntax.ML
diff -r c133f16febc7 -r 513925de8962 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Aug 12 16:21:18 1998 +0200
+++ b/src/HOL/Main.thy	Wed Aug 12 16:23:25 1998 +0200
@@ -1,4 +1,4 @@
 
 (*theory Main includes everything*)
 
-Main = Update + Map + Record + Bin + RelPow + Sexp + String + Recdef
+Main = Map + Record + Bin + RelPow + Sexp + String + Recdef
diff -r c133f16febc7 -r 513925de8962 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Aug 12 16:21:18 1998 +0200
+++ b/src/HOL/Set.ML	Wed Aug 12 16:23:25 1998 +0200
@@ -606,10 +606,6 @@
 AddIs  [image_eqI];
 AddSEs [imageE]; 
 
-Goalw [o_def] "(f o g)``r = f``(g``r)";
-by (Blast_tac 1);
-qed "image_compose";
-
 Goal "f``(A Un B) = f``A Un f``B";
 by (Blast_tac 1);
 qed "image_Un";
diff -r c133f16febc7 -r 513925de8962 src/HOL/Update.ML
--- a/src/HOL/Update.ML	Wed Aug 12 16:21:18 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-(*  Title:      HOL/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;
-
-Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
-by Safe_tac;
-by (etac subst 1);
-by (rtac ext 2);
-by Auto_tac;
-qed "fun_upd_idem_iff";
-
-(* f x = y ==> f(x:=y) = f *)
-bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
-
-(* f(x := f x) = f *)
-AddIffs [refl RS fun_upd_idem];
-
-Goal "(f(x:=y))z = (if z=x then y else f z)";
-by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
-qed "fun_upd_apply";
-Addsimps [fun_upd_apply];
diff -r c133f16febc7 -r 513925de8962 src/HOL/Update.thy
--- a/src/HOL/Update.thy	Wed Aug 12 16:21:18 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(*  Title:      HOL/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 = Fun +
-
-consts
-  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
-
-nonterminals
-  updbinds  updbind
-
-syntax
-
-  (* Let expressions *)
-
-  "_updbind"       :: ['a, 'a] => updbind             ("(2_ :=/ _)")
-  ""               :: updbind => updbinds             ("_")
-  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
-  "_Update"        :: ['a, updbinds] => 'a            ("_/'((_)')" [900,0] 900)
-
-translations
-  "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
-  "f(x:=y)"                     == "fun_upd f x y"
-
-defs
-  fun_upd_def "f(a:=b) == %x. if x=a then b else f x"
-
-end