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

src/HOL/Library/AssocList.thy

changeset 22916 | 8caf6da610e2 |

parent 22803 | 5129e02f4df2 |

child 23281 | e26ec695c9b3 |

1.1 --- a/src/HOL/Library/AssocList.thy Thu May 10 04:06:56 2007 +0200 1.2 +++ b/src/HOL/Library/AssocList.thy Thu May 10 10:21:44 2007 +0200 1.3 @@ -7,7 +7,6 @@ 1.4 1.5 theory AssocList 1.6 imports Map 1.7 - 1.8 begin 1.9 1.10 text {* 1.11 @@ -541,32 +540,20 @@ 1.12 subsection {* @{const compose} *} 1.13 (* ******************************************************************************** *) 1.14 1.15 -lemma compose_induct [case_names Nil Cons]: 1.16 - fixes xs ys 1.17 - assumes Nil: "P [] ys" 1.18 - assumes Cons: "\<And>x xs. 1.19 - (\<And>v. map_of ys (snd x) = Some v \<Longrightarrow> P xs ys) 1.20 - \<Longrightarrow> (map_of ys (snd x) = None \<Longrightarrow> P (delete (fst x) xs) ys) 1.21 - \<Longrightarrow> P (x # xs) ys" 1.22 - shows "P xs ys" 1.23 -by (induct xs rule: compose.induct [where ?P="\<lambda>xs zs. P xs ys"]) 1.24 - (auto intro: Nil Cons) 1.25 lemma compose_first_None [simp]: 1.26 assumes "map_of xs k = None" 1.27 shows "map_of (compose xs ys) k = None" 1.28 -using prems 1.29 -by (induct xs ys rule: compose_induct) (auto split: option.splits split_if_asm) 1.30 +using prems by (induct xs ys rule: compose.induct) 1.31 + (auto split: option.splits split_if_asm) 1.32 1.33 lemma compose_conv: 1.34 shows "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k" 1.35 -proof (induct xs ys rule: compose_induct) 1.36 - case Nil thus ?case by simp 1.37 +proof (induct xs ys rule: compose.induct) 1.38 + case 1 then show ?case by simp 1.39 next 1.40 - case (Cons x xs) 1.41 - show ?case 1.42 + case (2 x xs ys) show ?case 1.43 proof (cases "map_of ys (snd x)") 1.44 - case None 1.45 - with Cons 1.46 + case None with 2 1.47 have hyp: "map_of (compose (delete (fst x) xs) ys) k = 1.48 (map_of ys \<circ>\<^sub>m map_of (delete (fst x) xs)) k" 1.49 by simp 1.50 @@ -589,7 +576,7 @@ 1.51 qed 1.52 next 1.53 case (Some v) 1.54 - with Cons 1.55 + with 2 1.56 have "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k" 1.57 by simp 1.58 with Some show ?thesis 1.59 @@ -607,14 +594,14 @@ 1.60 using prems by (simp add: compose_conv) 1.61 1.62 lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs" 1.63 -proof (induct xs ys rule: compose_induct) 1.64 - case Nil thus ?case by simp 1.65 +proof (induct xs ys rule: compose.induct) 1.66 + case 1 thus ?case by simp 1.67 next 1.68 - case (Cons x xs) 1.69 + case (2 x xs ys) 1.70 show ?case 1.71 proof (cases "map_of ys (snd x)") 1.72 case None 1.73 - with Cons.hyps 1.74 + with "2.hyps" 1.75 have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)" 1.76 by simp 1.77 also 1.78 @@ -625,7 +612,7 @@ 1.79 by auto 1.80 next 1.81 case (Some v) 1.82 - with Cons.hyps 1.83 + with "2.hyps" 1.84 have "fst ` set (compose xs ys) \<subseteq> fst ` set xs" 1.85 by simp 1.86 with Some show ?thesis 1.87 @@ -637,30 +624,30 @@ 1.88 assumes "distinct (map fst xs)" 1.89 shows "distinct (map fst (compose xs ys))" 1.90 using prems 1.91 -proof (induct xs ys rule: compose_induct) 1.92 - case Nil thus ?case by simp 1.93 +proof (induct xs ys rule: compose.induct) 1.94 + case 1 thus ?case by simp 1.95 next 1.96 - case (Cons x xs) 1.97 + case (2 x xs ys) 1.98 show ?case 1.99 proof (cases "map_of ys (snd x)") 1.100 case None 1.101 - with Cons show ?thesis by simp 1.102 + with 2 show ?thesis by simp 1.103 next 1.104 case (Some v) 1.105 - with Cons dom_compose [of xs ys] show ?thesis 1.106 + with 2 dom_compose [of xs ys] show ?thesis 1.107 by (auto) 1.108 qed 1.109 qed 1.110 1.111 lemma compose_delete_twist: "(compose (delete k xs) ys) = delete k (compose xs ys)" 1.112 -proof (induct xs ys rule: compose_induct) 1.113 - case Nil thus ?case by simp 1.114 +proof (induct xs ys rule: compose.induct) 1.115 + case 1 thus ?case by simp 1.116 next 1.117 - case (Cons x xs) 1.118 + case (2 x xs ys) 1.119 show ?case 1.120 proof (cases "map_of ys (snd x)") 1.121 case None 1.122 - with Cons have 1.123 + with 2 have 1.124 hyp: "compose (delete k (delete (fst x) xs)) ys = 1.125 delete k (compose (delete (fst x) xs) ys)" 1.126 by simp 1.127 @@ -678,14 +665,14 @@ 1.128 qed 1.129 next 1.130 case (Some v) 1.131 - with Cons have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp 1.132 + with 2 have hyp: "compose (delete k xs) ys = delete k (compose xs ys)" by simp 1.133 with Some show ?thesis 1.134 by simp 1.135 qed 1.136 qed 1.137 1.138 lemma compose_clearjunk: "compose xs (clearjunk ys) = compose xs ys" 1.139 - by (induct xs ys rule: compose_induct) 1.140 + by (induct xs ys rule: compose.induct) 1.141 (auto simp add: map_of_clearjunk split: option.splits) 1.142 1.143 lemma clearjunk_compose: "clearjunk (compose xs ys) = compose (clearjunk xs) ys" 1.144 @@ -695,8 +682,7 @@ 1.145 1.146 lemma compose_empty [simp]: 1.147 "compose xs [] = []" 1.148 - by (induct xs rule: compose_induct [where ys="[]"]) auto 1.149 - 1.150 + by (induct xs) (auto simp add: compose_delete_twist) 1.151 1.152 lemma compose_Some_iff: 1.153 "(map_of (compose xs ys) k = Some v) =