summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/AssocList.thy

changeset 32960 | 69916a850301 |

parent 30663 | 0b6aff7451b2 |

child 34975 | f099b0b20646 |

1.1 --- a/src/HOL/Library/AssocList.thy Sat Oct 17 01:05:59 2009 +0200 1.2 +++ b/src/HOL/Library/AssocList.thy Sat Oct 17 14:43:18 2009 +0200 1.3 @@ -233,9 +233,9 @@ 1.4 fix v 1.5 assume "v \<in> ran (map_of (a#al))" 1.6 then obtain x where "map_of (a#al) x = Some v" 1.7 - by (auto simp add: ran_def) 1.8 + by (auto simp add: ran_def) 1.9 then show "v \<in> {snd a} \<union> ran (map_of al)" 1.10 - by (auto split: split_if_asm simp add: ran_def) 1.11 + by (auto split: split_if_asm simp add: ran_def) 1.12 qed 1.13 next 1.14 show "{snd a} \<union> ran (map_of al) \<subseteq> ran (map_of (a # al))" 1.15 @@ -244,22 +244,22 @@ 1.16 assume v_in: "v \<in> {snd a} \<union> ran (map_of al)" 1.17 show "v \<in> ran (map_of (a#al))" 1.18 proof (cases "v=snd a") 1.19 - case True 1.20 - with v_in show ?thesis 1.21 - by (auto simp add: ran_def) 1.22 + case True 1.23 + with v_in show ?thesis 1.24 + by (auto simp add: ran_def) 1.25 next 1.26 - case False 1.27 - with v_in have "v \<in> ran (map_of al)" by auto 1.28 - then obtain x where al_x: "map_of al x = Some v" 1.29 - by (auto simp add: ran_def) 1.30 - from map_of_SomeD [OF this] 1.31 - have "x \<in> fst ` set al" 1.32 - by (force simp add: image_def) 1.33 - with Cons.prems have "x\<noteq>fst a" 1.34 - by - (rule ccontr,simp) 1.35 - with al_x 1.36 - show ?thesis 1.37 - by (auto simp add: ran_def) 1.38 + case False 1.39 + with v_in have "v \<in> ran (map_of al)" by auto 1.40 + then obtain x where al_x: "map_of al x = Some v" 1.41 + by (auto simp add: ran_def) 1.42 + from map_of_SomeD [OF this] 1.43 + have "x \<in> fst ` set al" 1.44 + by (force simp add: image_def) 1.45 + with Cons.prems have "x\<noteq>fst a" 1.46 + by - (rule ccontr,simp) 1.47 + with al_x 1.48 + show ?thesis 1.49 + by (auto simp add: ran_def) 1.50 qed 1.51 qed 1.52 qed 1.53 @@ -537,17 +537,17 @@ 1.54 case True 1.55 from True delete_notin_dom [of k xs] 1.56 have "map_of (delete (fst x) xs) k = None" 1.57 - by (simp add: map_of_eq_None_iff) 1.58 + by (simp add: map_of_eq_None_iff) 1.59 with hyp show ?thesis 1.60 - using True None 1.61 - by simp 1.62 + using True None 1.63 + by simp 1.64 next 1.65 case False 1.66 from False have "map_of (delete (fst x) xs) k = map_of xs k" 1.67 - by simp 1.68 + by simp 1.69 with hyp show ?thesis 1.70 - using False None 1.71 - by (simp add: map_comp_def) 1.72 + using False None 1.73 + by (simp add: map_comp_def) 1.74 qed 1.75 next 1.76 case (Some v) 1.77 @@ -631,12 +631,12 @@ 1.78 case True 1.79 with None hyp 1.80 show ?thesis 1.81 - by (simp add: delete_idem) 1.82 + by (simp add: delete_idem) 1.83 next 1.84 case False 1.85 from None False hyp 1.86 show ?thesis 1.87 - by (simp add: delete_twist) 1.88 + by (simp add: delete_twist) 1.89 qed 1.90 next 1.91 case (Some v) 1.92 @@ -736,30 +736,30 @@ 1.93 case True 1.94 from Cons.hyps 1.95 show ?thesis 1.96 - using x_D True 1.97 - by simp 1.98 + using x_D True 1.99 + by simp 1.100 next 1.101 case False 1.102 note not_fst_a_x = this 1.103 show ?thesis 1.104 proof (cases "fst a \<in> D") 1.105 - case True 1.106 - with not_fst_a_x 1.107 - have "delete x (restrict D (a#al)) = a#(delete x (restrict D al))" 1.108 - by (cases a) (simp add: restrict_eq) 1.109 - also from not_fst_a_x True hyp have "\<dots> = restrict (D - {x}) (a # al)" 1.110 - by (cases a) (simp add: restrict_eq) 1.111 - finally show ?thesis 1.112 - using x_D by simp 1.113 + case True 1.114 + with not_fst_a_x 1.115 + have "delete x (restrict D (a#al)) = a#(delete x (restrict D al))" 1.116 + by (cases a) (simp add: restrict_eq) 1.117 + also from not_fst_a_x True hyp have "\<dots> = restrict (D - {x}) (a # al)" 1.118 + by (cases a) (simp add: restrict_eq) 1.119 + finally show ?thesis 1.120 + using x_D by simp 1.121 next 1.122 - case False 1.123 - hence "delete x (restrict D (a#al)) = delete x (restrict D al)" 1.124 - by (cases a) (simp add: restrict_eq) 1.125 - moreover from False not_fst_a_x 1.126 - have "restrict (D - {x}) (a # al) = restrict (D - {x}) al" 1.127 - by (cases a) (simp add: restrict_eq) 1.128 - ultimately 1.129 - show ?thesis using x_D hyp by simp 1.130 + case False 1.131 + hence "delete x (restrict D (a#al)) = delete x (restrict D al)" 1.132 + by (cases a) (simp add: restrict_eq) 1.133 + moreover from False not_fst_a_x 1.134 + have "restrict (D - {x}) (a # al) = restrict (D - {x}) al" 1.135 + by (cases a) (simp add: restrict_eq) 1.136 + ultimately 1.137 + show ?thesis using x_D hyp by simp 1.138 qed 1.139 qed 1.140 next