# HG changeset patch # User paulson # Date 1026652281 -7200 # Node ID d19cdbd8b559546eb20c8a53cafb54b45b8c42f6 # Parent 8c8eafb63746e33e9aa6107c0791051705f80e5a merged Update with func diff -r 8c8eafb63746 -r d19cdbd8b559 src/ZF/Update.thy --- a/src/ZF/Update.thy Fri Jul 12 17:16:22 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,67 +0,0 @@ -(* 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 -*) - -theory Update = func: - -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 - -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)" - - -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 \ 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, simp) -done - - -(* [| 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 diff -r 8c8eafb63746 -r d19cdbd8b559 src/ZF/func.thy --- a/src/ZF/func.thy Fri Jul 12 17:16:22 2002 +0200 +++ b/src/ZF/func.thy Sun Jul 14 15:11:21 2002 +0200 @@ -3,11 +3,14 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge -Functions in Zermelo-Fraenkel Set Theory *) +header{*Functions, Function Spaces, Lambda-Abstraction*} + theory func = equalities: +subsection{*The Pi Operator: Dependent Function Space*} + lemma subset_Sigma_imp_relation: "r <= Sigma(A,B) ==> relation(r)" by (simp add: relation_def, blast) @@ -18,8 +21,6 @@ lemma relation_restrict [simp]: "relation(restrict(r,A))" by (simp add: restrict_def relation_def, blast) -(*** The Pi operator -- dependent function space ***) - lemma Pi_iff: "f: Pi(A,B) <-> function(f) & f<=Sigma(A,B) & A<=domain(f)" by (unfold Pi_def, blast) @@ -56,7 +57,7 @@ lemma fun_weaken_type: "[| f: A->B; B<=D |] ==> f: A->D" by (unfold Pi_def, best) -(*** Function Application ***) +subsection{*Function Application*} lemma apply_equality2: "[| : f; : f; f: Pi(A,B) |] ==> b=c" by (unfold Pi_def function_def, blast) @@ -130,7 +131,7 @@ lemma Pair_mem_PiD: "[| : f; f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b" by (blast intro: domain_type range_type apply_equality) -(*** Lambda Abstraction ***) +subsection{*Lambda Abstraction*} lemma lamI: "a:A ==> : (lam x:A. b(x))" apply (unfold lam_def) @@ -203,7 +204,7 @@ done -(** Extensionality **) +subsection{*Extensionality*} (*Semi-extensionality!*) @@ -243,7 +244,7 @@ done -(** Images of functions **) +subsection{*Images of Functions*} lemma image_lam: "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}" by (unfold lam_def, blast) @@ -275,7 +276,7 @@ by (blast dest: apply_equality apply_Pair) -(*** properties of "restrict" ***) +subsection{*Properties of @{term "restrict(f,A)"}*} lemma restrict_subset: "restrict(f,A) <= f" by (unfold restrict_def, blast) @@ -335,7 +336,7 @@ done -(*** Unions of functions ***) +subsection{*Unions of Functions*} (** The Union of a set of COMPATIBLE functions is a function **) @@ -378,7 +379,7 @@ lemma fun_disjoint_apply2: "c \ domain(f) ==> (f Un g)`c = g`c" by (simp add: apply_def, blast) -(** Domain and range of a function/relation **) +subsection{*Domain and Range of a Function or Relation*} lemma domain_of_fun: "f : Pi(A,B) ==> domain(f)=A" by (unfold Pi_def, blast) @@ -389,7 +390,7 @@ lemma range_of_fun: "f : Pi(A,B) ==> f : A->range(f)" by (blast intro: Pi_type apply_rangeI) -(*** Extensions of functions ***) +subsection{*Extensions of Functions*} lemma fun_extend: "[| f: A->B; c~:A |] ==> cons(,f) : cons(c,A) -> cons(b,B)" @@ -435,6 +436,56 @@ lemma succ_fun_eq: "succ(n) -> B = (\f \ n->B. \b\B. {cons(, f)})" by (simp add: succ_def mem_not_refl cons_fun_eq) + +subsection{*Function Updates*} + +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 + +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)" + + +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 \ 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, simp) +done + + +(* [| 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 Pi_iff = thm "Pi_iff"; @@ -508,6 +559,12 @@ val fun_extend_apply = thm "fun_extend_apply"; val singleton_apply = thm "singleton_apply"; val cons_fun_eq = thm "cons_fun_eq"; + +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