src/HOL/Map.ML
author paulson
Wed Mar 03 11:15:18 1999 +0100 (1999-03-03)
changeset 6301 08245f5a436d
parent 5444 ffc64812a70b
child 7958 f531589c9fc1
permissions -rw-r--r--
expandshort
     1 (*  Title:      HOL/Map.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1997 TU Muenchen
     5 
     6 Map lemmas
     7 *)
     8 
     9 section "empty";
    10 
    11 Goalw [empty_def] "empty k = None";
    12 by (Simp_tac 1);
    13 qed "empty_def2";
    14 Addsimps [empty_def2];
    15 
    16 
    17 section "map_upd";
    18 
    19 qed_goal "map_upd_triv" thy "!!X. t k = Some x ==> t(k|->x) = t"
    20 	(K [rtac ext 1, Asm_simp_tac 1]);
    21 (*Addsimps [map_upd_triv];*)
    22 
    23 
    24 section "map_upds";
    25 
    26 Goal "a ~: set as --> (!m bs. (m(a|->b)(as[|->]bs)) = (m(as[|->]bs)(a|->b)))";
    27 by (induct_tac "as" 1);
    28 by  (auto_tac (claset(), simpset() delsimps[fun_upd_apply]));
    29 by (REPEAT(dtac spec 1));
    30 by (rotate_tac ~1 1);
    31 by (etac subst 1);
    32 by (etac (fun_upd_twist RS subst) 1);
    33 by (rtac refl 1);
    34 qed_spec_mp "map_upds_twist";
    35 Addsimps [map_upds_twist];
    36 
    37 
    38 section "chg_map";
    39 
    40 qed_goalw "chg_map_new" thy [chg_map_def]
    41 	"!!s. m a = None   ==> chg_map f a m = m"          (K [Auto_tac]);
    42 qed_goalw "chg_map_upd" thy [chg_map_def]
    43 	"!!s. m a = Some b ==> chg_map f a m = m(a|->f b)" (K [Auto_tac]);
    44 Addsimps[chg_map_new, chg_map_upd];
    45 
    46 
    47 section "option_map";
    48 
    49 qed_goal "option_map_o_empty" thy 
    50          "option_map f o empty = empty" (K [rtac ext 1, Simp_tac 1]);
    51 
    52 qed_goal "option_map_o_map_upd" thy 
    53 	 "option_map f o m(a|->b) = (option_map f o m)(a|->f b)" 
    54 	(K [rtac ext 1, Simp_tac 1]);
    55 Addsimps[option_map_o_empty, option_map_o_map_upd];
    56 
    57 
    58 section "++";
    59 
    60 Goalw [override_def] "m ++ empty = m";
    61 by (Simp_tac 1);
    62 qed "override_empty";
    63 Addsimps [override_empty];
    64 
    65 Goalw [override_def] "empty ++ m = m";
    66 by (Simp_tac 1);
    67 by (rtac ext 1);
    68 by (split_tac [option.split] 1);
    69 by (Simp_tac 1);
    70 qed "empty_override";
    71 Addsimps [empty_override];
    72 
    73 Goalw [override_def]
    74  "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
    75 by (simp_tac (simpset() addsplits [option.split]) 1);
    76 qed_spec_mp "override_Some_iff";
    77 
    78 bind_thm ("override_SomeD", standard(override_Some_iff RS iffD1));
    79 AddSDs[override_SomeD];
    80 
    81 Goalw [override_def] "((m ++ n) k = None) = (n k = None & m k = None)";
    82 by (simp_tac (simpset() addsplits [option.split]) 1);
    83 qed "override_None";
    84 AddIffs [override_None];
    85 
    86 Goalw [override_def] "map_of ys ++ map_of xs = map_of (xs@ys)";
    87 by (rtac sym 1);
    88 by (induct_tac "xs" 1);
    89 by (Simp_tac 1);
    90 by (rtac ext 1);
    91 by (asm_simp_tac (simpset() addsplits [option.split]) 1);
    92 qed "map_of_override";
    93 Addsimps [map_of_override];
    94 
    95 Goal "map_of xs k = Some y --> (k,y):set xs";
    96 by (induct_tac "xs" 1);
    97 by  (Simp_tac 1);
    98 by (split_all_tac 1);
    99 by (Asm_simp_tac 1);
   100 qed_spec_mp "map_of_SomeD";
   101 
   102 
   103 section "dom";
   104 
   105 Goalw [dom_def] "dom empty = {}";
   106 by (Simp_tac 1);
   107 qed "dom_empty";
   108 Addsimps [dom_empty];
   109 
   110 Goalw [dom_def] "dom(m(a|->b)) = insert a (dom m)";
   111 by (Simp_tac 1);
   112 by (Blast_tac 1);
   113 qed "dom_map_upd";
   114 Addsimps [dom_map_upd];
   115 
   116 qed_goalw "finite_dom_map_of" Map.thy [dom_def] "finite (dom (map_of l))" (K[
   117 	induct_tac "l" 1,
   118 	 ALLGOALS Simp_tac,
   119 	stac (insert_Collect RS sym) 1,
   120 	Asm_full_simp_tac 1]);
   121 
   122 Goalw [dom_def] "dom(m++n) = dom n Un dom m";
   123 by (Simp_tac 1);
   124 by (Blast_tac 1);
   125 qed "dom_override";
   126 Addsimps [dom_override];
   127 
   128 section "ran";
   129 
   130 Goalw [ran_def] "ran empty = {}";
   131 by (Simp_tac 1);
   132 qed "ran_empty";
   133 Addsimps [ran_empty];
   134 
   135 Goalw [ran_def] "m a = None ==> ran(m(a|->b)) = insert b (ran m)";
   136 by Auto_tac;
   137 by (subgoal_tac "~(aa = a)" 1);
   138 by Auto_tac;
   139 qed "ran_map_upd";
   140 Addsimps [ran_map_upd];