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) =