converted Update to Isar
authorpaulson
Fri May 24 15:24:29 2002 +0200 (2002-05-24)
changeset 13177ba734cc2887d
parent 13176 312bd350579b
child 13178 bc54319f6875
converted Update to Isar
src/ZF/IsaMakefile
src/ZF/Update.ML
src/ZF/Update.thy
     1.1 --- a/src/ZF/IsaMakefile	Fri May 24 13:15:37 2002 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Fri May 24 15:24:29 2002 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4    Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
     1.5    Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML	\
     1.6    Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML	\
     1.7 -  Trancl.ML Trancl.thy Univ.thy Update.ML Update.thy \
     1.8 +  Trancl.ML Trancl.thy Univ.thy Update.thy \
     1.9    WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML equalities.thy func.thy	\
    1.10    ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML		\
    1.11    subset.ML subset.thy thy_syntax.ML upair.ML upair.thy
     2.1 --- a/src/ZF/Update.ML	Fri May 24 13:15:37 2002 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,39 +0,0 @@
     2.4 -(*  Title:      ZF/Update.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1998  University of Cambridge
     2.8 -
     2.9 -Function updates: like theory Map, but for ordinary functions
    2.10 -*)
    2.11 -
    2.12 -Goal "f(x:=y) ` z = (if z=x then y else f`z)";
    2.13 -by (simp_tac (simpset() addsimps [update_def]) 1);
    2.14 -by (case_tac "z : domain(f)" 1);
    2.15 -by (Asm_simp_tac 1);
    2.16 -by (asm_simp_tac (simpset() addsimps [apply_0]) 1);
    2.17 -qed "update_apply";
    2.18 -Addsimps [update_apply];
    2.19 -
    2.20 -Goalw [update_def] "[| f`x = y;  f: Pi(A,B);  x: A |] ==> f(x:=y) = f";
    2.21 -by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb]) 1);
    2.22 -by (rtac fun_extension 1);
    2.23 -by (best_tac (claset() addIs [apply_type, if_type, lam_type]) 1);
    2.24 -by (assume_tac 1);
    2.25 -by (Asm_simp_tac 1);
    2.26 -qed "update_idem";
    2.27 -
    2.28 -
    2.29 -(* [| f: Pi(A, B); x:A |] ==> f(x := f`x) = f *)
    2.30 -Addsimps [refl RS update_idem];
    2.31 -
    2.32 -Goalw [update_def] "domain(f(x:=y)) = cons(x, domain(f))";
    2.33 -by (Asm_simp_tac 1);
    2.34 -qed "domain_update";
    2.35 -Addsimps [domain_update];
    2.36 -
    2.37 -Goalw [update_def] "[| f: A -> B;  x : A;  y: B |] ==> f(x:=y) : A -> B";
    2.38 -by (asm_simp_tac (simpset() addsimps [domain_of_fun, cons_absorb, 
    2.39 -				      apply_funtype, lam_type]) 1);
    2.40 -qed "update_type";
    2.41 -
    2.42 -
     3.1 --- a/src/ZF/Update.thy	Fri May 24 13:15:37 2002 +0200
     3.2 +++ b/src/ZF/Update.thy	Fri May 24 15:24:29 2002 +0200
     3.3 @@ -6,10 +6,11 @@
     3.4  Function updates: like theory Map, but for ordinary functions
     3.5  *)
     3.6  
     3.7 -Update = func +
     3.8 +theory Update = func:
     3.9  
    3.10 -consts
    3.11 +constdefs
    3.12    update  :: "[i,i,i] => i"
    3.13 +   "update(f,a,b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
    3.14  
    3.15  nonterminals
    3.16    updbinds  updbind
    3.17 @@ -18,16 +19,50 @@
    3.18  
    3.19    (* Let expressions *)
    3.20  
    3.21 -  "_updbind"       :: [i, i] => updbind             ("(2_ :=/ _)")
    3.22 -  ""               :: updbind => updbinds             ("_")
    3.23 -  "_updbinds"      :: [updbind, updbinds] => updbinds ("_,/ _")
    3.24 -  "_Update"        :: [i, updbinds] => i            ("_/'((_)')" [900,0] 900)
    3.25 +  "_updbind"    :: "[i, i] => updbind"               ("(2_ :=/ _)")
    3.26 +  ""            :: "updbind => updbinds"             ("_")
    3.27 +  "_updbinds"   :: "[updbind, updbinds] => updbinds" ("_,/ _")
    3.28 +  "_Update"     :: "[i, updbinds] => i"              ("_/'((_)')" [900,0] 900)
    3.29  
    3.30  translations
    3.31    "_Update (f, _updbinds(b,bs))"  == "_Update (_Update(f,b), bs)"
    3.32 -  "f(x:=y)"                     == "update(f,x,y)"
    3.33 +  "f(x:=y)"                       == "update(f,x,y)"
    3.34 +
    3.35 +
    3.36 +lemma update_apply [simp]: "f(x:=y) ` z = (if z=x then y else f`z)"
    3.37 +apply (simp add: update_def)
    3.38 +apply (rule_tac P="z \<in> domain(f)" in case_split_thm)   
    3.39 +apply (simp_all add: apply_0)
    3.40 +done
    3.41 +
    3.42 +lemma update_idem: "[| f`x = y;  f: Pi(A,B);  x: A |] ==> f(x:=y) = f"
    3.43 +apply (unfold update_def)
    3.44 +apply (simp add: domain_of_fun cons_absorb)
    3.45 +apply (rule fun_extension)
    3.46 +apply (best intro: apply_type if_type lam_type, assumption)
    3.47 +apply simp
    3.48 +done
    3.49 +
    3.50  
    3.51 -defs
    3.52 -  update_def "f(a:=b) == lam x: cons(a, domain(f)). if(x=a, b, f`x)"
    3.53 +(* [| f: Pi(A, B); x:A |] ==> f(x := f`x) = f *)
    3.54 +declare refl [THEN update_idem, simp]
    3.55 +
    3.56 +lemma domain_update [simp]: "domain(f(x:=y)) = cons(x, domain(f))"
    3.57 +by (unfold update_def, simp)
    3.58 +
    3.59 +lemma update_type: "[| f: A -> B;  x : A;  y: B |] ==> f(x:=y) : A -> B"
    3.60 +apply (unfold update_def)
    3.61 +apply (simp add: domain_of_fun cons_absorb apply_funtype lam_type)
    3.62 +done
    3.63 +
    3.64 +ML
    3.65 +{*
    3.66 +val update_def = thm "update_def";
    3.67 +val update_apply = thm "update_apply";
    3.68 +val update_idem = thm "update_idem";
    3.69 +val domain_update = thm "domain_update";
    3.70 +val update_type = thm "update_type";
    3.71 +*}
    3.72 +
    3.73  
    3.74  end