src/HOL/Map.thy
changeset 15251 bb6f072c8d10
parent 15140 322485b816ac
child 15303 eedbb8d22ca2
     1.1 --- a/src/HOL/Map.thy	Mon Oct 18 13:40:45 2004 +0200
     1.2 +++ b/src/HOL/Map.thy	Tue Oct 19 18:18:45 2004 +0200
     1.3 @@ -180,7 +180,7 @@
     1.4  by (induct rule:list_induct2, simp_all)
     1.5  
     1.6  lemma finite_range_map_of: "finite (range (map_of xys))"
     1.7 -apply (induct_tac xys)
     1.8 +apply (induct xys)
     1.9  apply  (simp_all (no_asm) add: image_constant)
    1.10  apply (rule finite_subset)
    1.11  prefer 2 apply assumption
    1.12 @@ -188,27 +188,27 @@
    1.13  done
    1.14  
    1.15  lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y --> (k,y):set xs"
    1.16 -by (induct_tac "xs", auto)
    1.17 +by (induct "xs", auto)
    1.18  
    1.19  lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x -->  
    1.20     map_of (map (split (%k. Pair (f k))) t) (f k) = Some x"
    1.21 -apply (induct_tac "t")
    1.22 +apply (induct "t")
    1.23  apply  (auto simp add: inj_eq)
    1.24  done
    1.25  
    1.26  lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l --> (? x. map_of l k = Some x)"
    1.27 -by (induct_tac "l", auto)
    1.28 +by (induct "l", auto)
    1.29  
    1.30  lemma map_of_filter_in: 
    1.31  "[| map_of xs k = Some z; P k z |] ==> map_of (filter (split P) xs) k = Some z"
    1.32  apply (rule mp)
    1.33  prefer 2 apply assumption
    1.34  apply (erule thin_rl)
    1.35 -apply (induct_tac "xs", auto)
    1.36 +apply (induct "xs", auto)
    1.37  done
    1.38  
    1.39  lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)"
    1.40 -by (induct_tac "xs", auto)
    1.41 +by (induct "xs", auto)
    1.42  
    1.43  
    1.44  subsection {* @{term option_map} related *}
    1.45 @@ -270,7 +270,7 @@
    1.46  
    1.47  lemma map_of_append[simp]: "map_of (xs@ys) = map_of ys ++ map_of xs"
    1.48  apply (unfold map_add_def)
    1.49 -apply (induct_tac "xs")
    1.50 +apply (induct "xs")
    1.51  apply (simp (no_asm))
    1.52  apply (rule ext)
    1.53  apply (simp (no_asm_simp) split add: option.split)
    1.54 @@ -279,7 +279,7 @@
    1.55  declare fun_upd_apply [simp del]
    1.56  lemma finite_range_map_of_map_add:
    1.57   "finite (range f) ==> finite (range (f ++ map_of l))"
    1.58 -apply (induct_tac "l", auto)
    1.59 +apply (induct "l", auto)
    1.60  apply (erule finite_range_updI)
    1.61  done
    1.62  declare fun_upd_apply [simp]
    1.63 @@ -445,7 +445,7 @@
    1.64  
    1.65  lemma finite_dom_map_of: "finite (dom (map_of l))"
    1.66  apply (unfold dom_def)
    1.67 -apply (induct_tac "l")
    1.68 +apply (induct "l")
    1.69  apply (auto simp add: insert_Collect [symmetric])
    1.70  done
    1.71