src/HOL/Library/AssocList.thy
changeset 26304 02fbd0e7954a
parent 26152 cf2cccf17d6d
child 27368 9f90ac19e32b
     1.1 --- a/src/HOL/Library/AssocList.thy	Mon Mar 17 18:37:04 2008 +0100
     1.2 +++ b/src/HOL/Library/AssocList.thy	Mon Mar 17 18:37:05 2008 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5  subsection {* @{const delete} *}
     1.6  
     1.7 -lemma delete_def:
     1.8 +lemma delete_eq:
     1.9    "delete k xs = filter (\<lambda>p. fst p \<noteq> k) xs"
    1.10    by (induct xs) auto
    1.11  
    1.12 @@ -163,14 +163,14 @@
    1.13    by (induct ps) auto
    1.14  
    1.15  lemma dom_clearjunk: "fst ` set (clearjunk al) = fst ` set al"
    1.16 -  by (induct al rule: clearjunk.induct) (simp_all add: insert_fst_filter delete_def)
    1.17 +  by (induct al rule: clearjunk.induct) (simp_all add: insert_fst_filter delete_eq)
    1.18  
    1.19  lemma notin_filter_fst: "a \<notin> fst ` {x \<in> set ps. fst x \<noteq> a}"
    1.20    by (induct ps) auto
    1.21  
    1.22  lemma distinct_clearjunk [simp]: "distinct (map fst (clearjunk al))"
    1.23    by (induct al rule: clearjunk.induct) 
    1.24 -     (simp_all add: dom_clearjunk notin_filter_fst delete_def)
    1.25 +     (simp_all add: dom_clearjunk notin_filter_fst delete_eq)
    1.26  
    1.27  lemma map_of_filter: "k \<noteq> a \<Longrightarrow> map_of [q\<leftarrow>ps . fst q \<noteq> a] k = map_of ps k"
    1.28    by (induct ps) auto
    1.29 @@ -188,11 +188,11 @@
    1.30  next
    1.31    case (Cons p ps)
    1.32    from Cons have "length (clearjunk [q\<leftarrow>ps . fst q \<noteq> fst p]) \<le> length [q\<leftarrow>ps . fst q \<noteq> fst p]" 
    1.33 -    by (simp add: delete_def)
    1.34 +    by (simp add: delete_eq)
    1.35    also have "\<dots> \<le> length ps"
    1.36      by simp
    1.37    finally show ?case
    1.38 -    by (simp add: delete_def)
    1.39 +    by (simp add: delete_eq)
    1.40  qed
    1.41  
    1.42  lemma notin_fst_filter: "a \<notin> fst ` set ps \<Longrightarrow> [q\<leftarrow>ps . fst q \<noteq> a] = ps"
    1.43 @@ -319,7 +319,7 @@
    1.44    by (induct ps) auto
    1.45  
    1.46  lemma clearjunk_update: "clearjunk (update k v al) = update k v (clearjunk al)"
    1.47 -  by (induct al rule: clearjunk.induct) (auto simp add: update_filter delete_def)
    1.48 +  by (induct al rule: clearjunk.induct) (auto simp add: update_filter delete_eq)
    1.49  
    1.50  lemma update_triv: "map_of al k = Some v \<Longrightarrow> update k v al = al"
    1.51    by (induct al) auto
    1.52 @@ -442,7 +442,7 @@
    1.53    by (induct ps) auto
    1.54  
    1.55  lemma clearjunk_map_ran: "clearjunk (map_ran f al) = map_ran f (clearjunk al)"
    1.56 -  by (induct al rule: clearjunk.induct) (auto simp add: delete_def map_ran_filter)
    1.57 +  by (induct al rule: clearjunk.induct) (auto simp add: delete_eq map_ran_filter)
    1.58  
    1.59  
    1.60  subsection {* @{const merge} *}
    1.61 @@ -673,7 +673,7 @@
    1.62  
    1.63  subsection {* @{const restrict} *}
    1.64  
    1.65 -lemma restrict_def:
    1.66 +lemma restrict_eq:
    1.67    "restrict A = filter (\<lambda>p. fst p \<in> A)"
    1.68  proof
    1.69    fix xs
    1.70 @@ -682,13 +682,13 @@
    1.71  qed
    1.72  
    1.73  lemma distinct_restr: "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
    1.74 -  by (induct al) (auto simp add: restrict_def)
    1.75 +  by (induct al) (auto simp add: restrict_eq)
    1.76  
    1.77  lemma restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
    1.78    apply (induct al)
    1.79 -  apply  (simp add: restrict_def)
    1.80 +  apply  (simp add: restrict_eq)
    1.81    apply (cases "k\<in>A")
    1.82 -  apply (auto simp add: restrict_def)
    1.83 +  apply (auto simp add: restrict_eq)
    1.84    done
    1.85  
    1.86  lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
    1.87 @@ -697,7 +697,7 @@
    1.88  lemma restr_empty [simp]: 
    1.89    "restrict {} al = []" 
    1.90    "restrict A [] = []"
    1.91 -  by (induct al) (auto simp add: restrict_def)
    1.92 +  by (induct al) (auto simp add: restrict_eq)
    1.93  
    1.94  lemma restr_in [simp]: "x \<in> A \<Longrightarrow> map_of (restrict A al) x = map_of al x"
    1.95    by (simp add: restr_conv')
    1.96 @@ -706,13 +706,13 @@
    1.97    by (simp add: restr_conv')
    1.98  
    1.99  lemma dom_restr [simp]: "fst ` set (restrict A al) = fst ` set al \<inter> A"
   1.100 -  by (induct al) (auto simp add: restrict_def)
   1.101 +  by (induct al) (auto simp add: restrict_eq)
   1.102  
   1.103  lemma restr_upd_same [simp]: "restrict (-{x}) (update x y al) = restrict (-{x}) al"
   1.104 -  by (induct al) (auto simp add: restrict_def)
   1.105 +  by (induct al) (auto simp add: restrict_eq)
   1.106  
   1.107  lemma restr_restr [simp]: "restrict A (restrict B al) = restrict (A\<inter>B) al"
   1.108 -  by (induct al) (auto simp add: restrict_def)
   1.109 +  by (induct al) (auto simp add: restrict_eq)
   1.110  
   1.111  lemma restr_update[simp]:
   1.112   "map_of (restrict D (update x y al)) = 
   1.113 @@ -747,18 +747,18 @@
   1.114  	case True 
   1.115  	with not_fst_a_x 
   1.116  	have "delete x (restrict D (a#al)) = a#(delete x (restrict D al))"
   1.117 -	  by (cases a) (simp add: restrict_def)
   1.118 +	  by (cases a) (simp add: restrict_eq)
   1.119  	also from not_fst_a_x True hyp have "\<dots> = restrict (D - {x}) (a # al)"
   1.120 -	  by (cases a) (simp add: restrict_def)
   1.121 +	  by (cases a) (simp add: restrict_eq)
   1.122  	finally show ?thesis
   1.123  	  using x_D by simp
   1.124        next
   1.125  	case False
   1.126  	hence "delete x (restrict D (a#al)) = delete x (restrict D al)"
   1.127 -	  by (cases a) (simp add: restrict_def)
   1.128 +	  by (cases a) (simp add: restrict_eq)
   1.129  	moreover from False not_fst_a_x
   1.130  	have "restrict (D - {x}) (a # al) = restrict (D - {x}) al"
   1.131 -	  by (cases a) (simp add: restrict_def)
   1.132 +	  by (cases a) (simp add: restrict_eq)
   1.133  	ultimately
   1.134  	show ?thesis using x_D hyp by simp
   1.135        qed