Map.update -> map_upd, Unpdate.update -> fun_upd
authornipkow
Fri Jul 24 17:18:15 1998 +0200 (1998-07-24)
changeset 5195277831ae7eac
parent 5194 650bf0ce0229
child 5196 1dd4ec921f71
Map.update -> map_upd, Unpdate.update -> fun_upd
Problem: macros get confused about two updates.
src/HOL/Map.ML
src/HOL/Map.thy
src/HOL/Update.ML
src/HOL/Update.thy
     1.1 --- a/src/HOL/Map.ML	Fri Jul 24 14:53:23 1998 +0200
     1.2 +++ b/src/HOL/Map.ML	Fri Jul 24 17:18:15 1998 +0200
     1.3 @@ -11,28 +11,28 @@
     1.4  qed "empty_def2";
     1.5  Addsimps [empty_def2];
     1.6  
     1.7 -Goalw [update_def] "(m[a|->b])x = (if x=a then Some b else m x)";
     1.8 +Goalw [map_upd_def] "(m[a|->b])x = (if x=a then Some b else m x)";
     1.9  by (Simp_tac 1);
    1.10 -qed "update_def2";
    1.11 -Addsimps [update_def2];
    1.12 +qed "map_upd_def2";
    1.13 +Addsimps [map_upd_def2];
    1.14  
    1.15 -qed_goal "update_same" thy "(t[k|->x]) k = Some x" 
    1.16 +qed_goal "map_upd_same" thy "(t[k|->x]) k = Some x" 
    1.17  	(K [Simp_tac 1]);
    1.18 -qed_goal "update_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
    1.19 +qed_goal "map_upd_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
    1.20  	(K [Asm_simp_tac 1]);
    1.21 -qed_goal "update_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
    1.22 +qed_goal "map_upd_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
    1.23  	(K [rtac ext 1, Asm_simp_tac 1]);
    1.24 -(*Addsimps [update_same, update_other, update_triv];*)
    1.25 +(*Addsimps [map_upd_same, map_upd_other, map_upd_triv];*)
    1.26  
    1.27  section "option_map";
    1.28  
    1.29  qed_goal "option_map_o_empty" thy 
    1.30           "option_map f o empty = empty" (K [rtac ext 1, Simp_tac 1]);
    1.31  
    1.32 -qed_goal "option_map_o_update" thy 
    1.33 +qed_goal "option_map_o_map_upd" thy 
    1.34  	 "option_map f o m[a|->b] = (option_map f o m)[a|->f b]" 
    1.35  	(K [rtac ext 1, Simp_tac 1]);
    1.36 -Addsimps[option_map_o_empty, option_map_o_update];
    1.37 +Addsimps[option_map_o_empty, option_map_o_map_upd];
    1.38  
    1.39  section "++";
    1.40  
    1.41 @@ -87,8 +87,8 @@
    1.42  Goalw [dom_def] "dom(m[a|->b]) = insert a (dom m)";
    1.43  by (Simp_tac 1);
    1.44  by (Blast_tac 1);
    1.45 -qed "dom_update";
    1.46 -Addsimps [dom_update];
    1.47 +qed "dom_map_upd";
    1.48 +Addsimps [dom_map_upd];
    1.49  
    1.50  qed_goalw "finite_dom_map_of" Map.thy [dom_def] "finite (dom (map_of l))" (K[
    1.51  	induct_tac "l" 1,
    1.52 @@ -112,5 +112,5 @@
    1.53  by Auto_tac;
    1.54  by (subgoal_tac "~(aa = a)" 1);
    1.55  by Auto_tac;
    1.56 -qed "ran_update";
    1.57 -Addsimps [ran_update];
    1.58 +qed "ran_map_upd";
    1.59 +Addsimps [ran_map_upd];
     2.1 --- a/src/HOL/Map.thy	Fri Jul 24 14:53:23 1998 +0200
     2.2 +++ b/src/HOL/Map.thy	Fri Jul 24 17:18:15 1998 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  
     2.5  consts
     2.6  empty   :: "'a ~=> 'b"
     2.7 -update  :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
     2.8 +map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
     2.9             ("_/[_/|->/_]" [900,0,0] 900)
    2.10  override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    2.11  dom     :: "('a ~=> 'b) => 'a set"
    2.12 @@ -22,7 +22,7 @@
    2.13  syntax (symbols)
    2.14    "~=>"     :: [type, type] => type
    2.15                 (infixr "\\<leadsto>" 0)
    2.16 -  update    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    2.17 +  map_upd    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    2.18                 ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
    2.19    override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
    2.20                 (infixl "\\<oplus>" 100)
    2.21 @@ -30,7 +30,7 @@
    2.22  defs
    2.23  empty_def "empty == %x. None"
    2.24  
    2.25 -update_def "m[a|->b] == %x. if x=a then Some b else m x"
    2.26 +map_upd_def "m[a|->b] == %x. if x=a then Some b else m x"
    2.27  
    2.28  override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    2.29  
     3.1 --- a/src/HOL/Update.ML	Fri Jul 24 14:53:23 1998 +0200
     3.2 +++ b/src/HOL/Update.ML	Fri Jul 24 17:18:15 1998 +0200
     3.3 @@ -8,20 +8,20 @@
     3.4  
     3.5  open Update;
     3.6  
     3.7 -Goalw [update_def] "(f(x:=y) = f) = (f x = y)";
     3.8 +Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
     3.9  by Safe_tac;
    3.10  by (etac subst 1);
    3.11  by (rtac ext 2);
    3.12  by Auto_tac;
    3.13 -qed "update_idem_iff";
    3.14 +qed "fun_upd_idem_iff";
    3.15  
    3.16  (* f x = y ==> f(x:=y) = f *)
    3.17 -bind_thm("update_idem", update_idem_iff RS iffD2);
    3.18 +bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
    3.19  
    3.20  (* f(x := f x) = f *)
    3.21 -AddIffs [refl RS update_idem];
    3.22 +AddIffs [refl RS fun_upd_idem];
    3.23  
    3.24  Goal "(f(x:=y))z = (if z=x then y else f z)";
    3.25 -by (simp_tac (simpset() addsimps [update_def]) 1);
    3.26 -qed "update_apply";
    3.27 -Addsimps [update_apply];
    3.28 +by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
    3.29 +qed "fun_upd_apply";
    3.30 +Addsimps [fun_upd_apply];
     4.1 --- a/src/HOL/Update.thy	Fri Jul 24 14:53:23 1998 +0200
     4.2 +++ b/src/HOL/Update.thy	Fri Jul 24 17:18:15 1998 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  Update = Fun +
     4.5  
     4.6  consts
     4.7 -  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
     4.8 +  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
     4.9  
    4.10  nonterminals
    4.11    updbinds  updbind
    4.12 @@ -25,9 +25,9 @@
    4.13  
    4.14  translations
    4.15    "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
    4.16 -  "f(x:=y)"                     == "update f x y"
    4.17 +  "f(x:=y)"                     == "fun_upd f x y"
    4.18  
    4.19  defs
    4.20 -  update_def "f(a:=b) == %x. if x=a then b else f x"
    4.21 +  fun_upd_def "f(a:=b) == %x. if x=a then b else f x"
    4.22  
    4.23  end