defined map_upd by translation via fun_upd
authoroheimb
Wed Aug 12 16:04:27 1998 +0200 (1998-08-12)
changeset 53002b1ca524ace8
parent 5299 d15a4155b96b
child 5301 e24d15594edd
defined map_upd by translation via fun_upd
changed syntax of map_upd to be consistent with that of fun_upd
added chg_map, map_upds
src/HOL/Map.ML
src/HOL/Map.thy
     1.1 --- a/src/HOL/Map.ML	Wed Aug 12 15:40:47 1998 +0200
     1.2 +++ b/src/HOL/Map.ML	Wed Aug 12 16:04:27 1998 +0200
     1.3 @@ -6,23 +6,43 @@
     1.4  Map lemmas
     1.5  *)
     1.6  
     1.7 +section "empty";
     1.8 +
     1.9  Goalw [empty_def] "empty k = None";
    1.10  by (Simp_tac 1);
    1.11  qed "empty_def2";
    1.12  Addsimps [empty_def2];
    1.13  
    1.14 -Goalw [map_upd_def] "(m[a|->b])x = (if x=a then Some b else m x)";
    1.15 -by (Simp_tac 1);
    1.16 -qed "map_upd_def2";
    1.17 -Addsimps [map_upd_def2];
    1.18 +
    1.19 +section "map_upd";
    1.20 +
    1.21 +qed_goal "map_upd_triv" thy "!!X. t k = Some x ==> t(k|->x) = t"
    1.22 +	(K [rtac ext 1, Asm_simp_tac 1]);
    1.23 +(*Addsimps [map_upd_triv];*)
    1.24 +
    1.25 +
    1.26 +section "map_upds";
    1.27  
    1.28 -qed_goal "map_upd_same" thy "(t[k|->x]) k = Some x" 
    1.29 -	(K [Simp_tac 1]);
    1.30 -qed_goal "map_upd_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
    1.31 -	(K [Asm_simp_tac 1]);
    1.32 -qed_goal "map_upd_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
    1.33 -	(K [rtac ext 1, Asm_simp_tac 1]);
    1.34 -(*Addsimps [map_upd_same, map_upd_other, map_upd_triv];*)
    1.35 +Goal "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))";
    1.36 +by (induct_tac "as" 1);
    1.37 +by  (auto_tac (claset(), simpset() delsimps[fun_upd_apply]));
    1.38 +by (REPEAT(dtac spec 1));
    1.39 +by (rotate_tac ~1 1);
    1.40 +by (etac subst 1);
    1.41 +by (etac (fun_upd_twist RS subst) 1);
    1.42 +by (rtac refl 1);
    1.43 +qed_spec_mp "map_upds_twist";
    1.44 +Addsimps [map_upds_twist];
    1.45 +
    1.46 +
    1.47 +section "chg_map";
    1.48 +
    1.49 +qed_goalw "chg_map_new" thy [chg_map_def]
    1.50 +	"!!s. m a = None   ==> chg_map f a m = m"          (K [Auto_tac]);
    1.51 +qed_goalw "chg_map_upd" thy [chg_map_def]
    1.52 +	"!!s. m a = Some b ==> chg_map f a m = m(a|->f b)" (K [Auto_tac]);
    1.53 +Addsimps[chg_map_new, chg_map_upd];
    1.54 +
    1.55  
    1.56  section "option_map";
    1.57  
    1.58 @@ -30,10 +50,11 @@
    1.59           "option_map f o empty = empty" (K [rtac ext 1, Simp_tac 1]);
    1.60  
    1.61  qed_goal "option_map_o_map_upd" thy 
    1.62 -	 "option_map f o m[a|->b] = (option_map f o m)[a|->f b]" 
    1.63 +	 "option_map f o m(a|->b) = (option_map f o m)(a|->f b)" 
    1.64  	(K [rtac ext 1, Simp_tac 1]);
    1.65  Addsimps[option_map_o_empty, option_map_o_map_upd];
    1.66  
    1.67 +
    1.68  section "++";
    1.69  
    1.70  Goalw [override_def] "m ++ empty = m";
    1.71 @@ -77,6 +98,7 @@
    1.72  by (Asm_simp_tac 1);
    1.73  qed_spec_mp "map_of_SomeD";
    1.74  
    1.75 +
    1.76  section "dom";
    1.77  
    1.78  Goalw [dom_def] "dom empty = {}";
    1.79 @@ -84,7 +106,7 @@
    1.80  qed "dom_empty";
    1.81  Addsimps [dom_empty];
    1.82  
    1.83 -Goalw [dom_def] "dom(m[a|->b]) = insert a (dom m)";
    1.84 +Goalw [dom_def] "dom(m(a|->b)) = insert a (dom m)";
    1.85  by (Simp_tac 1);
    1.86  by (Blast_tac 1);
    1.87  qed "dom_map_upd";
    1.88 @@ -108,7 +130,7 @@
    1.89  qed "ran_empty";
    1.90  Addsimps [ran_empty];
    1.91  
    1.92 -Goalw [ran_def] "m a = None ==> ran(m[a|->b]) = insert b (ran m)";
    1.93 +Goalw [ran_def] "m a = None ==> ran(m(a|->b)) = insert b (ran m)";
    1.94  by Auto_tac;
    1.95  by (subgoal_tac "~(aa = a)" 1);
    1.96  by Auto_tac;
     2.1 --- a/src/HOL/Map.thy	Wed Aug 12 15:40:47 1998 +0200
     2.2 +++ b/src/HOL/Map.thy	Wed Aug 12 16:04:27 1998 +0200
     2.3 @@ -11,26 +11,38 @@
     2.4  types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
     2.5  
     2.6  consts
     2.7 -empty   :: "'a ~=> 'b"
     2.8 -map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
     2.9 -           ("_/[_/|->/_]" [900,0,0] 900)
    2.10 +empty	::  "'a ~=> 'b"
    2.11 +chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
    2.12  override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    2.13 -dom     :: "('a ~=> 'b) => 'a set"
    2.14 -ran     :: "('a ~=> 'b) => 'b set"
    2.15 -map_of  :: "('a * 'b)list => 'a ~=> 'b"
    2.16 +dom	:: "('a ~=> 'b) => 'a set"
    2.17 +ran	:: "('a ~=> 'b) => 'b set"
    2.18 +map_of	:: "('a * 'b)list => 'a ~=> 'b"
    2.19 +map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
    2.20 +	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
    2.21 +
    2.22 +
    2.23 +syntax
    2.24 +map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    2.25 +					         ("_/'(_/|->_')"   [900,0,0]900)
    2.26  
    2.27  syntax (symbols)
    2.28 -  "~=>"     :: [type, type] => type
    2.29 -               (infixr "\\<leadsto>" 0)
    2.30 -  map_upd    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    2.31 -               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
    2.32 +  "~=>"     :: [type, type] => type      (infixr "\\<leadsto>" 0)
    2.33 +  map_upd   :: "('a ~=> 'b) => 'a      => 'b      => ('a ~=> 'b)"
    2.34 +					  ("_/'(_/\\<mapsto>/_')"  [900,0,0]900)
    2.35 +  map_upds  :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
    2.36 +				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
    2.37    override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
    2.38 -               (infixl "\\<oplus>" 100)
    2.39 +				         (infixl "\\<oplus>" 100)
    2.40 +
    2.41 +translations
    2.42 +
    2.43 +  "m(a|->b)" == "m(a:=Some b)"
    2.44  
    2.45  defs
    2.46 -empty_def "empty == %x. None"
    2.47  
    2.48 -map_upd_def "m[a|->b] == %x. if x=a then Some b else m x"
    2.49 +empty_def    "empty == %x. None"
    2.50 +
    2.51 +chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    2.52  
    2.53  override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    2.54  
    2.55 @@ -39,6 +51,9 @@
    2.56  
    2.57  primrec
    2.58    "map_of [] = empty"
    2.59 -  "map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
    2.60 +  "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
    2.61 +
    2.62 +primrec "t([]  [|->]bs) = t"
    2.63 +        "t(a#as[|->]bs) = t(a|->hd bs)(as[|->]tl bs)"
    2.64  
    2.65  end