src/HOL/Map.thy

 primrec
   "map_of [] = empty"
   "map_of (p#ps) = (map_of ps)(fst p |-> snd p)"
 
 
-subsection {* @{term empty} *}
+subsection {* @{term [source] empty} *}
 
 lemma empty_upd_none[simp]: "empty(x := None) = empty"
 apply (rule ext)
 apply (simp (no_asm))
 done

 lemma sum_case_empty_empty[simp]: "sum_case empty empty = empty"
 apply (rule ext)
 apply (simp (no_asm) split add: sum.split)
 done
 
-subsection {* @{term map_upd} *}
+subsection {* @{term [source] map_upd} *}
 
 lemma map_upd_triv: "t k = Some x ==> t(k|->x) = t"
 apply (rule ext)
 apply (simp (no_asm_simp))
 done

 apply auto
 done
 
 
 (* FIXME: what is this sum_case nonsense?? *)
-subsection {* @{term sum_case} and @{term empty}/@{term map_upd} *}
+subsection {* @{term [source] sum_case} and @{term [source] empty}/@{term [source] map_upd} *}
 
 lemma sum_case_map_upd_empty[simp]:
  "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)"
 apply (rule ext)
 apply (simp (no_asm) split add: sum.split)

 apply (rule ext)
 apply (simp (no_asm) split add: sum.split)
 done
 
 
-subsection {* @{term chg_map} *}
+subsection {* @{term [source] chg_map} *}
 
 lemma chg_map_new[simp]: "m a = None   ==> chg_map f a m = m"
 by (unfold chg_map_def, auto)
 
 lemma chg_map_upd[simp]: "m a = Some b ==> chg_map f a m = m(a|->f b)"

 
 lemma chg_map_other [simp]: "a \<noteq> b \<Longrightarrow> chg_map f a m b = m b"
 by (auto simp: chg_map_def split add: option.split)
 
 
-subsection {* @{term map_of} *}
+subsection {* @{term [source] map_of} *}
 
 lemma map_of_eq_None_iff:
  "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
 by (induct xys) simp_all
 

 
 lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
 by (induct "xs", auto)
 
 
-subsection {* @{term option_map} related *}
+subsection {* @{term [source] option_map} related *}
 
 lemma option_map_o_empty[simp]: "option_map f o empty = empty"
 apply (rule ext)
 apply (simp (no_asm))
 done

  "option_map f o m(a|->b) = (option_map f o m)(a|->f b)"
 apply (rule ext)
 apply (simp (no_asm))
 done
 
-subsection {* @{term map_comp} related *}
+subsection {* @{term [source] map_comp} related *}
 
 lemma map_comp_empty [simp]: 
   "m \<circ>\<^sub>m empty = empty"
   "empty \<circ>\<^sub>m m = empty"
   by (auto simp add: map_comp_def intro: ext split: option.splits)

 
 lemma inj_on_map_add_dom[iff]:
  "inj_on (m ++ m') (dom m') = inj_on m' (dom m')"
 by(fastsimp simp add:map_add_def dom_def inj_on_def split:option.splits)
 
-subsection {* @{term restrict_map} *}
+subsection {* @{term [source] restrict_map} *}
 
 lemma restrict_map_to_empty[simp]: "m|`{} = empty"
 by(simp add: restrict_map_def)
 
 lemma restrict_map_empty[simp]: "empty|`D = empty"

 lemma fun_upd_restrict_conv[simp]:
  "x \<in> D \<Longrightarrow> (m|`D)(x := y) = (m|`(D-{x}))(x := y)"
 by(simp add: restrict_map_def expand_fun_eq)
 
 
-subsection {* @{term map_upds} *}
+subsection {* @{term [source] map_upds} *}
 
 lemma map_upds_Nil1[simp]: "m([] [|->] bs) = m"
 by(simp add:map_upds_def)
 
 lemma map_upds_Nil2[simp]: "m(as [|->] []) = m"

 apply(simp add:Diff_insert[symmetric] insert_absorb)
 apply(simp add: map_upd_upds_conv_if)
 done
 
 
-subsection {* @{term map_upd_s} *}
+subsection {* @{term [source] map_upd_s} *}
 
 lemma map_upd_s_apply [simp]: 
   "(m(as{|->}b)) x = (if x : as then Some b else m x)"
 by (simp add: map_upd_s_def)
 
 lemma map_subst_apply [simp]: 
   "(m(a~>b)) x = (if m x = Some a then Some b else m x)" 
 by (simp add: map_subst_def)
 
-subsection {* @{term dom} *}
+subsection {* @{term [source] dom} *}
 
 lemma domI: "m a = Some b ==> a : dom m"
 by (unfold dom_def, auto)
 (* declare domI [intro]? *)
 

 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
 apply(rule ext)
 apply(fastsimp simp:map_add_def split:option.split)
 done
 
-subsection {* @{term ran} *}
+subsection {* @{term [source] ran} *}
 
 lemma ranI: "m a = Some b ==> b : ran m" 
 by (auto simp add: ran_def)
 (* declare ranI [intro]? *)