# 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 \ 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