src/HOL/Map.thy
changeset 17399 56a3a4affedc
parent 17391 c6338ed6caf8
child 17724 e969fc0a4925
     1.1 --- a/src/HOL/Map.thy	Wed Sep 14 23:31:09 2005 +0200
     1.2 +++ b/src/HOL/Map.thy	Wed Sep 14 23:55:49 2005 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4    "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
     1.5  
     1.6  
     1.7 -subsection {* @{term empty} *}
     1.8 +subsection {* @{term [source] empty} *}
     1.9  
    1.10  lemma empty_upd_none[simp]: "empty(x := None) = empty"
    1.11  apply (rule ext)
    1.12 @@ -112,7 +112,7 @@
    1.13  apply (simp (no_asm) split add: sum.split)
    1.14  done
    1.15  
    1.16 -subsection {* @{term map_upd} *}
    1.17 +subsection {* @{term [source] map_upd} *}
    1.18  
    1.19  lemma map_upd_triv: "t k = Some x ==> t(k|->x) = t"
    1.20  apply (rule ext)
    1.21 @@ -145,7 +145,7 @@
    1.22  
    1.23  
    1.24  (* FIXME: what is this sum_case nonsense?? *)
    1.25 -subsection {* @{term sum_case} and @{term empty}/@{term map_upd} *}
    1.26 +subsection {* @{term [source] sum_case} and @{term [source] empty}/@{term [source] map_upd} *}
    1.27  
    1.28  lemma sum_case_map_upd_empty[simp]:
    1.29   "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
    1.30 @@ -166,7 +166,7 @@
    1.31  done
    1.32  
    1.33  
    1.34 -subsection {* @{term chg_map} *}
    1.35 +subsection {* @{term [source] chg_map} *}
    1.36  
    1.37  lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
    1.38  by (unfold chg_map_def, auto)
    1.39 @@ -178,7 +178,7 @@
    1.40  by (auto simp: chg_map_def split add: option.split)
    1.41  
    1.42  
    1.43 -subsection {* @{term map_of} *}
    1.44 +subsection {* @{term [source] map_of} *}
    1.45  
    1.46  lemma map_of_eq_None_iff:
    1.47   "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
    1.48 @@ -247,7 +247,7 @@
    1.49  by (induct "xs", auto)
    1.50  
    1.51  
    1.52 -subsection {* @{term option_map} related *}
    1.53 +subsection {* @{term [source] option_map} related *}
    1.54  
    1.55  lemma option_map_o_empty[simp]: "option_map f o empty = empty"
    1.56  apply (rule ext)
    1.57 @@ -260,7 +260,7 @@
    1.58  apply (simp (no_asm))
    1.59  done
    1.60  
    1.61 -subsection {* @{term map_comp} related *}
    1.62 +subsection {* @{term [source] map_comp} related *}
    1.63  
    1.64  lemma map_comp_empty [simp]: 
    1.65    "m \<circ>\<^sub>m empty = empty"
    1.66 @@ -343,7 +343,7 @@
    1.67   "inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
    1.68  by(fastsimp simp add:map_add_def dom_def inj_on_def split:option.splits)
    1.69  
    1.70 -subsection {* @{term restrict_map} *}
    1.71 +subsection {* @{term [source] restrict_map} *}
    1.72  
    1.73  lemma restrict_map_to_empty[simp]: "m|`{} = empty"
    1.74  by(simp add: restrict_map_def)
    1.75 @@ -386,7 +386,7 @@
    1.76  by(simp add: restrict_map_def expand_fun_eq)
    1.77  
    1.78  
    1.79 -subsection {* @{term map_upds} *}
    1.80 +subsection {* @{term [source] map_upds} *}
    1.81  
    1.82  lemma map_upds_Nil1[simp]: "m([] [|->] bs) = m"
    1.83  by(simp add:map_upds_def)
    1.84 @@ -461,7 +461,7 @@
    1.85  done
    1.86  
    1.87  
    1.88 -subsection {* @{term map_upd_s} *}
    1.89 +subsection {* @{term [source] map_upd_s} *}
    1.90  
    1.91  lemma map_upd_s_apply [simp]: 
    1.92    "(m(as{|->}b)) x = (if x : as then Some b else m x)"
    1.93 @@ -471,7 +471,7 @@
    1.94    "(m(a~>b)) x = (if m x = Some a then Some b else m x)" 
    1.95  by (simp add: map_subst_def)
    1.96  
    1.97 -subsection {* @{term dom} *}
    1.98 +subsection {* @{term [source] dom} *}
    1.99  
   1.100  lemma domI: "m a = Some b ==> a : dom m"
   1.101  by (unfold dom_def, auto)
   1.102 @@ -531,7 +531,7 @@
   1.103  apply(fastsimp simp:map_add_def split:option.split)
   1.104  done
   1.105  
   1.106 -subsection {* @{term ran} *}
   1.107 +subsection {* @{term [source] ran} *}
   1.108  
   1.109  lemma ranI: "m a = Some b ==> b : ran m" 
   1.110  by (auto simp add: ran_def)