misc tuning and modernization;
authorwenzelm
Tue Jul 12 15:45:32 2016 +0200 (2016-07-12)
changeset 63462c1fe30f2bc32
parent 63461 f10feaa9b14a
child 63463 b6a1047bc164
misc tuning and modernization;
src/HOL/Library/AList.thy
src/HOL/Library/AList_Mapping.thy
src/HOL/Library/BigO.thy
src/HOL/Library/Bit.thy
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Combine_PER.thy
src/HOL/Library/Mapping.thy
     1.1 --- a/src/HOL/Library/AList.thy	Tue Jul 12 14:53:47 2016 +0200
     1.2 +++ b/src/HOL/Library/AList.thy	Tue Jul 12 15:45:32 2016 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  section \<open>Implementation of Association Lists\<close>
     1.5  
     1.6  theory AList
     1.7 -imports Main
     1.8 +  imports Main
     1.9  begin
    1.10  
    1.11  context
    1.12 @@ -21,9 +21,9 @@
    1.13  subsection \<open>\<open>update\<close> and \<open>updates\<close>\<close>
    1.14  
    1.15  qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.16 -where
    1.17 -  "update k v [] = [(k, v)]"
    1.18 -| "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    1.19 +  where
    1.20 +    "update k v [] = [(k, v)]"
    1.21 +  | "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    1.22  
    1.23  lemma update_conv': "map_of (update k v al)  = (map_of al)(k\<mapsto>v)"
    1.24    by (induct al) (auto simp add: fun_eq_iff)
    1.25 @@ -82,12 +82,11 @@
    1.26      x = k \<and> v = y \<or> x \<noteq> k \<and> map_of al x = Some y"
    1.27    by (simp add: update_conv' map_upd_Some_unfold)
    1.28  
    1.29 -lemma image_update [simp]:
    1.30 -  "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
    1.31 +lemma image_update [simp]: "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
    1.32    by (simp add: update_conv')
    1.33  
    1.34 -qualified definition
    1.35 -    updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.36 +qualified definition updates
    1.37 +    :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.38    where "updates ks vs = fold (case_prod update) (zip ks vs)"
    1.39  
    1.40  lemma updates_simps [simp]:
    1.41 @@ -217,66 +216,75 @@
    1.42  
    1.43  subsection \<open>\<open>update_with_aux\<close> and \<open>delete_aux\<close>\<close>
    1.44  
    1.45 -qualified primrec update_with_aux :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.46 -where
    1.47 -  "update_with_aux v k f [] = [(k, f v)]"
    1.48 -| "update_with_aux v k f (p # ps) = (if (fst p = k) then (k, f (snd p)) # ps else p # update_with_aux v k f ps)"
    1.49 +qualified primrec update_with_aux
    1.50 +    :: "'val \<Rightarrow> 'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.51 +  where
    1.52 +    "update_with_aux v k f [] = [(k, f v)]"
    1.53 +  | "update_with_aux v k f (p # ps) =
    1.54 +      (if (fst p = k) then (k, f (snd p)) # ps else p # update_with_aux v k f ps)"
    1.55  
    1.56  text \<open>
    1.57    The above @{term "delete"} traverses all the list even if it has found the key.
    1.58    This one does not have to keep going because is assumes the invariant that keys are distinct.
    1.59  \<close>
    1.60  qualified fun delete_aux :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    1.61 -where
    1.62 -  "delete_aux k [] = []"
    1.63 -| "delete_aux k ((k', v) # xs) = (if k = k' then xs else (k', v) # delete_aux k xs)"
    1.64 +  where
    1.65 +    "delete_aux k [] = []"
    1.66 +  | "delete_aux k ((k', v) # xs) = (if k = k' then xs else (k', v) # delete_aux k xs)"
    1.67  
    1.68  lemma map_of_update_with_aux':
    1.69 -  "map_of (update_with_aux v k f ps) k' = ((map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))) k'"
    1.70 -by(induct ps) auto
    1.71 +  "map_of (update_with_aux v k f ps) k' =
    1.72 +    ((map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))) k'"
    1.73 +  by (induct ps) auto
    1.74  
    1.75  lemma map_of_update_with_aux:
    1.76 -  "map_of (update_with_aux v k f ps) = (map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))"
    1.77 -by(simp add: fun_eq_iff map_of_update_with_aux')
    1.78 +  "map_of (update_with_aux v k f ps) =
    1.79 +    (map_of ps)(k \<mapsto> (case map_of ps k of None \<Rightarrow> f v | Some v \<Rightarrow> f v))"
    1.80 +  by (simp add: fun_eq_iff map_of_update_with_aux')
    1.81  
    1.82  lemma dom_update_with_aux: "fst ` set (update_with_aux v k f ps) = {k} \<union> fst ` set ps"
    1.83    by (induct ps) auto
    1.84  
    1.85  lemma distinct_update_with_aux [simp]:
    1.86    "distinct (map fst (update_with_aux v k f ps)) = distinct (map fst ps)"
    1.87 -by(induct ps)(auto simp add: dom_update_with_aux)
    1.88 +  by (induct ps) (auto simp add: dom_update_with_aux)
    1.89  
    1.90  lemma set_update_with_aux:
    1.91 -  "distinct (map fst xs) 
    1.92 -  \<Longrightarrow> set (update_with_aux v k f xs) = (set xs - {k} \<times> UNIV \<union> {(k, f (case map_of xs k of None \<Rightarrow> v | Some v \<Rightarrow> v))})"
    1.93 -by(induct xs)(auto intro: rev_image_eqI)
    1.94 +  "distinct (map fst xs) \<Longrightarrow>
    1.95 +    set (update_with_aux v k f xs) =
    1.96 +      (set xs - {k} \<times> UNIV \<union> {(k, f (case map_of xs k of None \<Rightarrow> v | Some v \<Rightarrow> v))})"
    1.97 +  by (induct xs) (auto intro: rev_image_eqI)
    1.98  
    1.99  lemma set_delete_aux: "distinct (map fst xs) \<Longrightarrow> set (delete_aux k xs) = set xs - {k} \<times> UNIV"
   1.100 -apply(induct xs)
   1.101 -apply simp_all
   1.102 -apply clarsimp
   1.103 -apply(fastforce intro: rev_image_eqI)
   1.104 -done
   1.105 +  apply (induct xs)
   1.106 +  apply simp_all
   1.107 +  apply clarsimp
   1.108 +  apply (fastforce intro: rev_image_eqI)
   1.109 +  done
   1.110  
   1.111  lemma dom_delete_aux: "distinct (map fst ps) \<Longrightarrow> fst ` set (delete_aux k ps) = fst ` set ps - {k}"
   1.112 -by(auto simp add: set_delete_aux)
   1.113 +  by (auto simp add: set_delete_aux)
   1.114  
   1.115 -lemma distinct_delete_aux [simp]:
   1.116 -  "distinct (map fst ps) \<Longrightarrow> distinct (map fst (delete_aux k ps))"
   1.117 -proof(induct ps)
   1.118 -  case Nil thus ?case by simp
   1.119 +lemma distinct_delete_aux [simp]: "distinct (map fst ps) \<Longrightarrow> distinct (map fst (delete_aux k ps))"
   1.120 +proof (induct ps)
   1.121 +  case Nil
   1.122 +  then show ?case by simp
   1.123  next
   1.124    case (Cons a ps)
   1.125 -  obtain k' v where a: "a = (k', v)" by(cases a)
   1.126 +  obtain k' v where a: "a = (k', v)"
   1.127 +    by (cases a)
   1.128    show ?case
   1.129 -  proof(cases "k' = k")
   1.130 -    case True with Cons a show ?thesis by simp
   1.131 +  proof (cases "k' = k")
   1.132 +    case True
   1.133 +    with Cons a show ?thesis by simp
   1.134    next
   1.135      case False
   1.136 -    with Cons a have "k' \<notin> fst ` set ps" "distinct (map fst ps)" by simp_all
   1.137 +    with Cons a have "k' \<notin> fst ` set ps" "distinct (map fst ps)"
   1.138 +      by simp_all
   1.139      with False a have "k' \<notin> fst ` set (delete_aux k ps)"
   1.140 -      by(auto dest!: dom_delete_aux[where k=k])
   1.141 -    with Cons a show ?thesis by simp
   1.142 +      by (auto dest!: dom_delete_aux[where k=k])
   1.143 +    with Cons a show ?thesis
   1.144 +      by simp
   1.145    qed
   1.146  qed
   1.147  
   1.148 @@ -290,10 +298,10 @@
   1.149  
   1.150  lemma map_of_delete_aux:
   1.151    "distinct (map fst xs) \<Longrightarrow> map_of (delete_aux k xs) k' = ((map_of xs)(k := None)) k'"
   1.152 -by(simp add: map_of_delete_aux')
   1.153 +  by (simp add: map_of_delete_aux')
   1.154  
   1.155  lemma delete_aux_eq_Nil_conv: "delete_aux k ts = [] \<longleftrightarrow> ts = [] \<or> (\<exists>v. ts = [(k, v)])"
   1.156 -by(cases ts)(auto split: if_split_asm)
   1.157 +  by (cases ts) (auto split: if_split_asm)
   1.158  
   1.159  
   1.160  subsection \<open>\<open>restrict\<close>\<close>
   1.161 @@ -308,16 +316,18 @@
   1.162  
   1.163  lemma restr_conv': "map_of (restrict A al) = ((map_of al)|` A)"
   1.164  proof
   1.165 -  fix k
   1.166 -  show "map_of (restrict A al) k = ((map_of al)|` A) k"
   1.167 -    by (induct al) (simp, cases "k \<in> A", auto)
   1.168 +  show "map_of (restrict A al) k = ((map_of al)|` A) k" for k
   1.169 +    apply (induct al)
   1.170 +    apply simp
   1.171 +    apply (cases "k \<in> A")
   1.172 +    apply auto
   1.173 +    done
   1.174  qed
   1.175  
   1.176  corollary restr_conv: "map_of (restrict A al) k = ((map_of al)|` A) k"
   1.177    by (simp add: restr_conv')
   1.178  
   1.179 -lemma distinct_restr:
   1.180 -  "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
   1.181 +lemma distinct_restr: "distinct (map fst al) \<Longrightarrow> distinct (map fst (restrict A al))"
   1.182    by (induct al) (auto simp add: restrict_eq)
   1.183  
   1.184  lemma restr_empty [simp]:
   1.185 @@ -341,8 +351,8 @@
   1.186    by (induct al) (auto simp add: restrict_eq)
   1.187  
   1.188  lemma restr_update[simp]:
   1.189 - "map_of (restrict D (update x y al)) =
   1.190 -  map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
   1.191 +  "map_of (restrict D (update x y al)) =
   1.192 +    map_of ((if x \<in> D then (update x y (restrict (D-{x}) al)) else restrict D al))"
   1.193    by (simp add: restr_conv' update_conv')
   1.194  
   1.195  lemma restr_delete [simp]:
   1.196 @@ -350,12 +360,12 @@
   1.197    apply (simp add: delete_eq restrict_eq)
   1.198    apply (auto simp add: split_def)
   1.199  proof -
   1.200 -  have "\<And>y. y \<noteq> x \<longleftrightarrow> x \<noteq> y"
   1.201 +  have "y \<noteq> x \<longleftrightarrow> x \<noteq> y" for y
   1.202      by auto
   1.203    then show "[p \<leftarrow> al. fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al. fst p \<in> D \<and> fst p \<noteq> x]"
   1.204      by simp
   1.205    assume "x \<notin> D"
   1.206 -  then have "\<And>y. y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y"
   1.207 +  then have "y \<in> D \<longleftrightarrow> y \<in> D \<and> x \<noteq> y" for y
   1.208      by auto
   1.209    then show "[p \<leftarrow> al . fst p \<in> D \<and> x \<noteq> fst p] = [p \<leftarrow> al . fst p \<in> D]"
   1.210      by simp
   1.211 @@ -383,9 +393,9 @@
   1.212  subsection \<open>\<open>clearjunk\<close>\<close>
   1.213  
   1.214  qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   1.215 -where
   1.216 -  "clearjunk [] = []"
   1.217 -| "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
   1.218 +  where
   1.219 +    "clearjunk [] = []"
   1.220 +  | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
   1.221    by pat_completeness auto
   1.222  termination
   1.223    by (relation "measure length") (simp_all add: less_Suc_eq_le length_delete_le)
   1.224 @@ -420,7 +430,7 @@
   1.225  lemma clearjunk_updates: "clearjunk (updates ks vs al) = updates ks vs (clearjunk al)"
   1.226  proof -
   1.227    have "clearjunk \<circ> fold (case_prod update) (zip ks vs) =
   1.228 -    fold (case_prod update) (zip ks vs) \<circ> clearjunk"
   1.229 +      fold (case_prod update) (zip ks vs) \<circ> clearjunk"
   1.230      by (rule fold_commute) (simp add: clearjunk_update case_prod_beta o_def)
   1.231    then show ?thesis
   1.232      by (simp add: updates_def fun_eq_iff)
   1.233 @@ -506,10 +516,8 @@
   1.234  lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   1.235    by (induct ys arbitrary: xs) (auto simp add: dom_update)
   1.236  
   1.237 -lemma distinct_merge:
   1.238 -  assumes "distinct (map fst xs)"
   1.239 -  shows "distinct (map fst (merge xs ys))"
   1.240 -  using assms by (simp add: merge_updates distinct_updates)
   1.241 +lemma distinct_merge: "distinct (map fst xs) \<Longrightarrow> distinct (map fst (merge xs ys))"
   1.242 +  by (simp add: merge_updates distinct_updates)
   1.243  
   1.244  lemma clearjunk_merge: "clearjunk (merge xs ys) = merge (clearjunk xs) ys"
   1.245    by (simp add: merge_updates clearjunk_updates)
   1.246 @@ -542,12 +550,10 @@
   1.247  lemma merge_find_right [simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
   1.248    by (simp add: merge_conv')
   1.249  
   1.250 -lemma merge_None [iff]:
   1.251 -  "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
   1.252 +lemma merge_None [iff]: "(map_of (merge m n) k = None) = (map_of n k = None \<and> map_of m k = None)"
   1.253    by (simp add: merge_conv')
   1.254  
   1.255 -lemma merge_upd [simp]:
   1.256 -  "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
   1.257 +lemma merge_upd [simp]: "map_of (merge m (update k v n)) = map_of (update k v (merge m n))"
   1.258    by (simp add: update_conv' merge_conv')
   1.259  
   1.260  lemma merge_updatess [simp]:
   1.261 @@ -561,20 +567,18 @@
   1.262  subsection \<open>\<open>compose\<close>\<close>
   1.263  
   1.264  qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
   1.265 -where
   1.266 -  "compose [] ys = []"
   1.267 -| "compose (x # xs) ys =
   1.268 -    (case map_of ys (snd x) of
   1.269 -      None \<Rightarrow> compose (delete (fst x) xs) ys
   1.270 -    | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
   1.271 +  where
   1.272 +    "compose [] ys = []"
   1.273 +  | "compose (x # xs) ys =
   1.274 +      (case map_of ys (snd x) of
   1.275 +        None \<Rightarrow> compose (delete (fst x) xs) ys
   1.276 +      | Some v \<Rightarrow> (fst x, v) # compose xs ys)"
   1.277    by pat_completeness auto
   1.278  termination
   1.279    by (relation "measure (length \<circ> fst)") (simp_all add: less_Suc_eq_le length_delete_le)
   1.280  
   1.281 -lemma compose_first_None [simp]:
   1.282 -  assumes "map_of xs k = None"
   1.283 -  shows "map_of (compose xs ys) k = None"
   1.284 -  using assms by (induct xs ys rule: compose.induct) (auto split: option.splits if_split_asm)
   1.285 +lemma compose_first_None [simp]: "map_of xs k = None \<Longrightarrow> map_of (compose xs ys) k = None"
   1.286 +  by (induct xs ys rule: compose.induct) (auto split: option.splits if_split_asm)
   1.287  
   1.288  lemma compose_conv: "map_of (compose xs ys) k = (map_of ys \<circ>\<^sub>m map_of xs) k"
   1.289  proof (induct xs ys rule: compose.induct)
   1.290 @@ -617,10 +621,8 @@
   1.291  lemma compose_conv': "map_of (compose xs ys) = (map_of ys \<circ>\<^sub>m map_of xs)"
   1.292    by (rule ext) (rule compose_conv)
   1.293  
   1.294 -lemma compose_first_Some [simp]:
   1.295 -  assumes "map_of xs k = Some v"
   1.296 -  shows "map_of (compose xs ys) k = map_of ys v"
   1.297 -  using assms by (simp add: compose_conv)
   1.298 +lemma compose_first_Some [simp]: "map_of xs k = Some v \<Longrightarrow> map_of (compose xs ys) k = map_of ys v"
   1.299 +  by (simp add: compose_conv)
   1.300  
   1.301  lemma dom_compose: "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   1.302  proof (induct xs ys rule: compose.induct)
   1.303 @@ -631,19 +633,15 @@
   1.304    show ?case
   1.305    proof (cases "map_of ys (snd x)")
   1.306      case None
   1.307 -    with "2.hyps"
   1.308 -    have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
   1.309 +    with "2.hyps" have "fst ` set (compose (delete (fst x) xs) ys) \<subseteq> fst ` set (delete (fst x) xs)"
   1.310        by simp
   1.311 -    also
   1.312 -    have "\<dots> \<subseteq> fst ` set xs"
   1.313 +    also have "\<dots> \<subseteq> fst ` set xs"
   1.314        by (rule dom_delete_subset)
   1.315      finally show ?thesis
   1.316 -      using None
   1.317 -      by auto
   1.318 +      using None by auto
   1.319    next
   1.320      case (Some v)
   1.321 -    with "2.hyps"
   1.322 -    have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   1.323 +    with "2.hyps" have "fst ` set (compose xs ys) \<subseteq> fst ` set xs"
   1.324        by simp
   1.325      with Some show ?thesis
   1.326        by auto
   1.327 @@ -726,10 +724,10 @@
   1.328  subsection \<open>\<open>map_entry\<close>\<close>
   1.329  
   1.330  qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   1.331 -where
   1.332 -  "map_entry k f [] = []"
   1.333 -| "map_entry k f (p # ps) =
   1.334 -    (if fst p = k then (k, f (snd p)) # ps else p # map_entry k f ps)"
   1.335 +  where
   1.336 +    "map_entry k f [] = []"
   1.337 +  | "map_entry k f (p # ps) =
   1.338 +      (if fst p = k then (k, f (snd p)) # ps else p # map_entry k f ps)"
   1.339  
   1.340  lemma map_of_map_entry:
   1.341    "map_of (map_entry k f xs) =
   1.342 @@ -748,10 +746,10 @@
   1.343  subsection \<open>\<open>map_default\<close>\<close>
   1.344  
   1.345  fun map_default :: "'key \<Rightarrow> 'val \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   1.346 -where
   1.347 -  "map_default k v f [] = [(k, v)]"
   1.348 -| "map_default k v f (p # ps) =
   1.349 -    (if fst p = k then (k, f (snd p)) # ps else p # map_default k v f ps)"
   1.350 +  where
   1.351 +    "map_default k v f [] = [(k, v)]"
   1.352 +  | "map_default k v f (p # ps) =
   1.353 +      (if fst p = k then (k, f (snd p)) # ps else p # map_default k v f ps)"
   1.354  
   1.355  lemma map_of_map_default:
   1.356    "map_of (map_default k v f xs) =
     2.1 --- a/src/HOL/Library/AList_Mapping.thy	Tue Jul 12 14:53:47 2016 +0200
     2.2 +++ b/src/HOL/Library/AList_Mapping.thy	Tue Jul 12 15:45:32 2016 +0200
     2.3 @@ -1,51 +1,43 @@
     2.4 -(* Title: HOL/Library/AList_Mapping.thy
     2.5 -   Author: Florian Haftmann, TU Muenchen
     2.6 +(*  Title:      HOL/Library/AList_Mapping.thy
     2.7 +    Author:     Florian Haftmann, TU Muenchen
     2.8  *)
     2.9  
    2.10  section \<open>Implementation of mappings with Association Lists\<close>
    2.11  
    2.12  theory AList_Mapping
    2.13 -imports AList Mapping
    2.14 +  imports AList Mapping
    2.15  begin
    2.16  
    2.17  lift_definition Mapping :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) mapping" is map_of .
    2.18  
    2.19  code_datatype Mapping
    2.20  
    2.21 -lemma lookup_Mapping [simp, code]:
    2.22 -  "Mapping.lookup (Mapping xs) = map_of xs"
    2.23 +lemma lookup_Mapping [simp, code]: "Mapping.lookup (Mapping xs) = map_of xs"
    2.24    by transfer rule
    2.25  
    2.26 -lemma keys_Mapping [simp, code]:
    2.27 -  "Mapping.keys (Mapping xs) = set (map fst xs)" 
    2.28 +lemma keys_Mapping [simp, code]: "Mapping.keys (Mapping xs) = set (map fst xs)"
    2.29    by transfer (simp add: dom_map_of_conv_image_fst)
    2.30  
    2.31 -lemma empty_Mapping [code]:
    2.32 -  "Mapping.empty = Mapping []"
    2.33 +lemma empty_Mapping [code]: "Mapping.empty = Mapping []"
    2.34    by transfer simp
    2.35  
    2.36 -lemma is_empty_Mapping [code]:
    2.37 -  "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
    2.38 +lemma is_empty_Mapping [code]: "Mapping.is_empty (Mapping xs) \<longleftrightarrow> List.null xs"
    2.39    by (case_tac xs) (simp_all add: is_empty_def null_def)
    2.40  
    2.41 -lemma update_Mapping [code]:
    2.42 -  "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
    2.43 +lemma update_Mapping [code]: "Mapping.update k v (Mapping xs) = Mapping (AList.update k v xs)"
    2.44    by transfer (simp add: update_conv')
    2.45  
    2.46 -lemma delete_Mapping [code]:
    2.47 -  "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)"
    2.48 +lemma delete_Mapping [code]: "Mapping.delete k (Mapping xs) = Mapping (AList.delete k xs)"
    2.49    by transfer (simp add: delete_conv')
    2.50  
    2.51  lemma ordered_keys_Mapping [code]:
    2.52    "Mapping.ordered_keys (Mapping xs) = sort (remdups (map fst xs))"
    2.53    by (simp only: ordered_keys_def keys_Mapping sorted_list_of_set_sort_remdups) simp
    2.54  
    2.55 -lemma size_Mapping [code]:
    2.56 -  "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
    2.57 +lemma size_Mapping [code]: "Mapping.size (Mapping xs) = length (remdups (map fst xs))"
    2.58    by (simp add: size_def length_remdups_card_conv dom_map_of_conv_image_fst)
    2.59  
    2.60 -lemma tabulate_Mapping [code]:
    2.61 -  "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
    2.62 +lemma tabulate_Mapping [code]: "Mapping.tabulate ks f = Mapping (map (\<lambda>k. (k, f k)) ks)"
    2.63    by transfer (simp add: map_of_map_restrict)
    2.64  
    2.65  lemma bulkload_Mapping [code]:
    2.66 @@ -55,63 +47,69 @@
    2.67  lemma equal_Mapping [code]:
    2.68    "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
    2.69      (let ks = map fst xs; ls = map fst ys
    2.70 -    in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
    2.71 +     in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
    2.72  proof -
    2.73 -  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
    2.74 +  have *: "(a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" for a b xs
    2.75      by (auto simp add: image_def intro!: bexI)
    2.76    show ?thesis apply transfer
    2.77 -    by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
    2.78 +    by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: *)
    2.79  qed
    2.80  
    2.81  lemma map_values_Mapping [code]:
    2.82 -  fixes f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b" and xs :: "('c \<times> 'a) list"
    2.83 -  shows "Mapping.map_values f (Mapping xs) = Mapping (map (\<lambda>(x,y). (x, f x y)) xs)"
    2.84 -proof (transfer, rule ext, goal_cases)
    2.85 -  case (1 f xs x)
    2.86 -  thus ?case by (induction xs) auto
    2.87 -qed
    2.88 +  "Mapping.map_values f (Mapping xs) = Mapping (map (\<lambda>(x,y). (x, f x y)) xs)"
    2.89 +  for f :: "'c \<Rightarrow> 'a \<Rightarrow> 'b" and xs :: "('c \<times> 'a) list"
    2.90 +  apply transfer
    2.91 +  apply (rule ext)
    2.92 +  subgoal for f xs x by (induct xs) auto
    2.93 +  done
    2.94  
    2.95 -lemma combine_with_key_code [code]: 
    2.96 +lemma combine_with_key_code [code]:
    2.97    "Mapping.combine_with_key f (Mapping xs) (Mapping ys) =
    2.98 -     Mapping.tabulate (remdups (map fst xs @ map fst ys)) 
    2.99 +     Mapping.tabulate (remdups (map fst xs @ map fst ys))
   2.100         (\<lambda>x. the (combine_options (f x) (map_of xs x) (map_of ys x)))"
   2.101 -proof (transfer, rule ext, rule sym, goal_cases)
   2.102 -  case (1 f xs ys x)
   2.103 -  show ?case
   2.104 -  by (cases "map_of xs x"; cases "map_of ys x"; simp)
   2.105 -     (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
   2.106 -            dest: map_of_SomeD split: option.splits)+
   2.107 -qed
   2.108 +  apply transfer
   2.109 +  apply (rule ext)
   2.110 +  apply (rule sym)
   2.111 +  subgoal for f xs ys x
   2.112 +    apply (cases "map_of xs x"; cases "map_of ys x"; simp)
   2.113 +    apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
   2.114 +      dest: map_of_SomeD split: option.splits)+
   2.115 +    done
   2.116 +  done
   2.117  
   2.118 -lemma combine_code [code]: 
   2.119 +lemma combine_code [code]:
   2.120    "Mapping.combine f (Mapping xs) (Mapping ys) =
   2.121 -     Mapping.tabulate (remdups (map fst xs @ map fst ys)) 
   2.122 +     Mapping.tabulate (remdups (map fst xs @ map fst ys))
   2.123         (\<lambda>x. the (combine_options f (map_of xs x) (map_of ys x)))"
   2.124 -proof (transfer, rule ext, rule sym, goal_cases)
   2.125 -  case (1 f xs ys x)
   2.126 -  show ?case
   2.127 -  by (cases "map_of xs x"; cases "map_of ys x"; simp)
   2.128 -     (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
   2.129 -            dest: map_of_SomeD split: option.splits)+
   2.130 -qed
   2.131 +  apply transfer
   2.132 +  apply (rule ext)
   2.133 +  apply (rule sym)
   2.134 +  subgoal for f xs ys x
   2.135 +    apply (cases "map_of xs x"; cases "map_of ys x"; simp)
   2.136 +    apply (force simp: map_of_eq_None_iff combine_options_def option.the_def o_def image_iff
   2.137 +      dest: map_of_SomeD split: option.splits)+
   2.138 +    done
   2.139 +  done
   2.140  
   2.141 -(* TODO: Move? *)
   2.142 -lemma map_of_filter_distinct:
   2.143 +lemma map_of_filter_distinct:  (* TODO: move? *)
   2.144    assumes "distinct (map fst xs)"
   2.145 -  shows   "map_of (filter P xs) x = 
   2.146 -             (case map_of xs x of None \<Rightarrow> None | Some y \<Rightarrow> if P (x,y) then Some y else None)"
   2.147 +  shows "map_of (filter P xs) x =
   2.148 +    (case map_of xs x of
   2.149 +      None \<Rightarrow> None
   2.150 +    | Some y \<Rightarrow> if P (x,y) then Some y else None)"
   2.151    using assms
   2.152    by (auto simp: map_of_eq_None_iff filter_map distinct_map_filter dest: map_of_SomeD
   2.153 -           simp del: map_of_eq_Some_iff intro!: map_of_is_SomeI split: option.splits)
   2.154 -(* END TODO *)
   2.155 -  
   2.156 +      simp del: map_of_eq_Some_iff intro!: map_of_is_SomeI split: option.splits)
   2.157 +
   2.158  lemma filter_Mapping [code]:
   2.159    "Mapping.filter P (Mapping xs) = Mapping (filter (\<lambda>(k,v). P k v) (AList.clearjunk xs))"
   2.160 - by (transfer, rule ext)
   2.161 -    (subst map_of_filter_distinct, simp_all add: map_of_clearjunk split: option.split)
   2.162 +  apply transfer
   2.163 +  apply (rule ext)
   2.164 +  apply (subst map_of_filter_distinct)
   2.165 +  apply (simp_all add: map_of_clearjunk split: option.split)
   2.166 +  done
   2.167  
   2.168 -lemma [code nbe]:
   2.169 -  "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
   2.170 +lemma [code nbe]: "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True"
   2.171    by (fact equal_refl)
   2.172  
   2.173  end
     3.1 --- a/src/HOL/Library/BigO.thy	Tue Jul 12 14:53:47 2016 +0200
     3.2 +++ b/src/HOL/Library/BigO.thy	Tue Jul 12 15:45:32 2016 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  section \<open>Big O notation\<close>
     3.5  
     3.6  theory BigO
     3.7 -imports Complex_Main Function_Algebras Set_Algebras
     3.8 +  imports Complex_Main Function_Algebras Set_Algebras
     3.9  begin
    3.10  
    3.11  text \<open>
     4.1 --- a/src/HOL/Library/Bit.thy	Tue Jul 12 14:53:47 2016 +0200
     4.2 +++ b/src/HOL/Library/Bit.thy	Tue Jul 12 15:45:32 2016 +0200
     4.3 @@ -11,17 +11,14 @@
     4.4  subsection \<open>Bits as a datatype\<close>
     4.5  
     4.6  typedef bit = "UNIV :: bool set"
     4.7 -  morphisms set Bit
     4.8 -  ..
     4.9 +  morphisms set Bit ..
    4.10  
    4.11  instantiation bit :: "{zero, one}"
    4.12  begin
    4.13  
    4.14 -definition zero_bit_def:
    4.15 -  "0 = Bit False"
    4.16 +definition zero_bit_def: "0 = Bit False"
    4.17  
    4.18 -definition one_bit_def:
    4.19 -  "1 = Bit True"
    4.20 +definition one_bit_def: "1 = Bit True"
    4.21  
    4.22  instance ..
    4.23  
    4.24 @@ -29,8 +26,9 @@
    4.25  
    4.26  old_rep_datatype "0::bit" "1::bit"
    4.27  proof -
    4.28 -  fix P and x :: bit
    4.29 -  assume "P (0::bit)" and "P (1::bit)"
    4.30 +  fix P :: "bit \<Rightarrow> bool"
    4.31 +  fix x :: bit
    4.32 +  assume "P 0" and "P 1"
    4.33    then have "\<forall>b. P (Bit b)"
    4.34      unfolding zero_bit_def one_bit_def
    4.35      by (simp add: all_bool_eq)
    4.36 @@ -42,21 +40,17 @@
    4.37      by (simp add: Bit_inject)
    4.38  qed
    4.39  
    4.40 -lemma Bit_set_eq [simp]:
    4.41 -  "Bit (set b) = b"
    4.42 +lemma Bit_set_eq [simp]: "Bit (set b) = b"
    4.43    by (fact set_inverse)
    4.44 -  
    4.45 -lemma set_Bit_eq [simp]:
    4.46 -  "set (Bit P) = P"
    4.47 +
    4.48 +lemma set_Bit_eq [simp]: "set (Bit P) = P"
    4.49    by (rule Bit_inverse) rule
    4.50  
    4.51 -lemma bit_eq_iff:
    4.52 -  "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
    4.53 +lemma bit_eq_iff: "x = y \<longleftrightarrow> (set x \<longleftrightarrow> set y)"
    4.54    by (auto simp add: set_inject)
    4.55  
    4.56 -lemma Bit_inject [simp]:
    4.57 -  "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
    4.58 -  by (auto simp add: Bit_inject)  
    4.59 +lemma Bit_inject [simp]: "Bit P = Bit Q \<longleftrightarrow> (P \<longleftrightarrow> Q)"
    4.60 +  by (auto simp add: Bit_inject)
    4.61  
    4.62  lemma set [iff]:
    4.63    "\<not> set 0"
    4.64 @@ -68,8 +62,7 @@
    4.65    "set 1 \<longleftrightarrow> True"
    4.66    by simp_all
    4.67  
    4.68 -lemma set_iff:
    4.69 -  "set b \<longleftrightarrow> b = 1"
    4.70 +lemma set_iff: "set b \<longleftrightarrow> b = 1"
    4.71    by (cases b) simp_all
    4.72  
    4.73  lemma bit_eq_iff_set:
    4.74 @@ -82,42 +75,34 @@
    4.75    "Bit True = 1"
    4.76    by (simp_all add: zero_bit_def one_bit_def)
    4.77  
    4.78 -lemma bit_not_0_iff [iff]:
    4.79 -  "(x::bit) \<noteq> 0 \<longleftrightarrow> x = 1"
    4.80 +lemma bit_not_0_iff [iff]: "x \<noteq> 0 \<longleftrightarrow> x = 1" for x :: bit
    4.81    by (simp add: bit_eq_iff)
    4.82  
    4.83 -lemma bit_not_1_iff [iff]:
    4.84 -  "(x::bit) \<noteq> 1 \<longleftrightarrow> x = 0"
    4.85 +lemma bit_not_1_iff [iff]: "x \<noteq> 1 \<longleftrightarrow> x = 0" for x :: bit
    4.86    by (simp add: bit_eq_iff)
    4.87  
    4.88  lemma [code]:
    4.89    "HOL.equal 0 b \<longleftrightarrow> \<not> set b"
    4.90    "HOL.equal 1 b \<longleftrightarrow> set b"
    4.91 -  by (simp_all add: equal set_iff)  
    4.92 +  by (simp_all add: equal set_iff)
    4.93  
    4.94 -  
    4.95 +
    4.96  subsection \<open>Type @{typ bit} forms a field\<close>
    4.97  
    4.98  instantiation bit :: field
    4.99  begin
   4.100  
   4.101 -definition plus_bit_def:
   4.102 -  "x + y = case_bit y (case_bit 1 0 y) x"
   4.103 +definition plus_bit_def: "x + y = case_bit y (case_bit 1 0 y) x"
   4.104  
   4.105 -definition times_bit_def:
   4.106 -  "x * y = case_bit 0 y x"
   4.107 +definition times_bit_def: "x * y = case_bit 0 y x"
   4.108  
   4.109 -definition uminus_bit_def [simp]:
   4.110 -  "- x = (x :: bit)"
   4.111 +definition uminus_bit_def [simp]: "- x = x" for x :: bit
   4.112  
   4.113 -definition minus_bit_def [simp]:
   4.114 -  "x - y = (x + y :: bit)"
   4.115 +definition minus_bit_def [simp]: "x - y = x + y" for x y :: bit
   4.116  
   4.117 -definition inverse_bit_def [simp]:
   4.118 -  "inverse x = (x :: bit)"
   4.119 +definition inverse_bit_def [simp]: "inverse x = x" for x :: bit
   4.120  
   4.121 -definition divide_bit_def [simp]:
   4.122 -  "x div y = (x * y :: bit)"
   4.123 +definition divide_bit_def [simp]: "x div y = x * y" for x y :: bit
   4.124  
   4.125  lemmas field_bit_defs =
   4.126    plus_bit_def times_bit_def minus_bit_def uminus_bit_def
   4.127 @@ -128,18 +113,18 @@
   4.128  
   4.129  end
   4.130  
   4.131 -lemma bit_add_self: "x + x = (0 :: bit)"
   4.132 +lemma bit_add_self: "x + x = 0" for x :: bit
   4.133    unfolding plus_bit_def by (simp split: bit.split)
   4.134  
   4.135 -lemma bit_mult_eq_1_iff [simp]: "x * y = (1 :: bit) \<longleftrightarrow> x = 1 \<and> y = 1"
   4.136 +lemma bit_mult_eq_1_iff [simp]: "x * y = 1 \<longleftrightarrow> x = 1 \<and> y = 1" for x y :: bit
   4.137    unfolding times_bit_def by (simp split: bit.split)
   4.138  
   4.139  text \<open>Not sure whether the next two should be simp rules.\<close>
   4.140  
   4.141 -lemma bit_add_eq_0_iff: "x + y = (0 :: bit) \<longleftrightarrow> x = y"
   4.142 +lemma bit_add_eq_0_iff: "x + y = 0 \<longleftrightarrow> x = y" for x y :: bit
   4.143    unfolding plus_bit_def by (simp split: bit.split)
   4.144  
   4.145 -lemma bit_add_eq_1_iff: "x + y = (1 :: bit) \<longleftrightarrow> x \<noteq> y"
   4.146 +lemma bit_add_eq_1_iff: "x + y = 1 \<longleftrightarrow> x \<noteq> y" for x y :: bit
   4.147    unfolding plus_bit_def by (simp split: bit.split)
   4.148  
   4.149  
   4.150 @@ -166,37 +151,23 @@
   4.151  begin
   4.152  
   4.153  definition of_bit :: "bit \<Rightarrow> 'a"
   4.154 -where
   4.155 -  "of_bit b = case_bit 0 1 b" 
   4.156 +  where "of_bit b = case_bit 0 1 b"
   4.157  
   4.158  lemma of_bit_eq [simp, code]:
   4.159    "of_bit 0 = 0"
   4.160    "of_bit 1 = 1"
   4.161    by (simp_all add: of_bit_def)
   4.162  
   4.163 -lemma of_bit_eq_iff:
   4.164 -  "of_bit x = of_bit y \<longleftrightarrow> x = y"
   4.165 -  by (cases x) (cases y, simp_all)+
   4.166 -
   4.167 -end  
   4.168 -
   4.169 -context semiring_1
   4.170 -begin
   4.171 -
   4.172 -lemma of_nat_of_bit_eq:
   4.173 -  "of_nat (of_bit b) = of_bit b"
   4.174 -  by (cases b) simp_all
   4.175 +lemma of_bit_eq_iff: "of_bit x = of_bit y \<longleftrightarrow> x = y"
   4.176 +  by (cases x) (cases y; simp)+
   4.177  
   4.178  end
   4.179  
   4.180 -context ring_1
   4.181 -begin
   4.182 -
   4.183 -lemma of_int_of_bit_eq:
   4.184 -  "of_int (of_bit b) = of_bit b"
   4.185 +lemma (in semiring_1) of_nat_of_bit_eq: "of_nat (of_bit b) = of_bit b"
   4.186    by (cases b) simp_all
   4.187  
   4.188 -end
   4.189 +lemma (in ring_1) of_int_of_bit_eq: "of_int (of_bit b) = of_bit b"
   4.190 +  by (cases b) simp_all
   4.191  
   4.192  hide_const (open) set
   4.193  
     5.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Tue Jul 12 14:53:47 2016 +0200
     5.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Tue Jul 12 15:45:32 2016 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4  section \<open>Boolean Algebras\<close>
     5.5  
     5.6  theory Boolean_Algebra
     5.7 -imports Main
     5.8 +  imports Main
     5.9  begin
    5.10  
    5.11  locale boolean =
    5.12 @@ -40,18 +40,18 @@
    5.13  lemmas disj_ac = disj.assoc disj.commute disj.left_commute
    5.14  
    5.15  lemma dual: "boolean disj conj compl one zero"
    5.16 -apply (rule boolean.intro)
    5.17 -apply (rule disj_assoc)
    5.18 -apply (rule conj_assoc)
    5.19 -apply (rule disj_commute)
    5.20 -apply (rule conj_commute)
    5.21 -apply (rule disj_conj_distrib)
    5.22 -apply (rule conj_disj_distrib)
    5.23 -apply (rule disj_zero_right)
    5.24 -apply (rule conj_one_right)
    5.25 -apply (rule disj_cancel_right)
    5.26 -apply (rule conj_cancel_right)
    5.27 -done
    5.28 +  apply (rule boolean.intro)
    5.29 +  apply (rule disj_assoc)
    5.30 +  apply (rule conj_assoc)
    5.31 +  apply (rule disj_commute)
    5.32 +  apply (rule conj_commute)
    5.33 +  apply (rule disj_conj_distrib)
    5.34 +  apply (rule conj_disj_distrib)
    5.35 +  apply (rule disj_zero_right)
    5.36 +  apply (rule conj_one_right)
    5.37 +  apply (rule disj_cancel_right)
    5.38 +  apply (rule conj_cancel_right)
    5.39 +  done
    5.40  
    5.41  
    5.42  subsection \<open>Complement\<close>
    5.43 @@ -63,99 +63,111 @@
    5.44    assumes 4: "a \<squnion> y = \<one>"
    5.45    shows "x = y"
    5.46  proof -
    5.47 -  have "(a \<sqinter> x) \<squnion> (x \<sqinter> y) = (a \<sqinter> y) \<squnion> (x \<sqinter> y)" using 1 3 by simp
    5.48 -  hence "(x \<sqinter> a) \<squnion> (x \<sqinter> y) = (y \<sqinter> a) \<squnion> (y \<sqinter> x)" using conj_commute by simp
    5.49 -  hence "x \<sqinter> (a \<squnion> y) = y \<sqinter> (a \<squnion> x)" using conj_disj_distrib by simp
    5.50 -  hence "x \<sqinter> \<one> = y \<sqinter> \<one>" using 2 4 by simp
    5.51 -  thus "x = y" using conj_one_right by simp
    5.52 +  have "(a \<sqinter> x) \<squnion> (x \<sqinter> y) = (a \<sqinter> y) \<squnion> (x \<sqinter> y)"
    5.53 +    using 1 3 by simp
    5.54 +  then have "(x \<sqinter> a) \<squnion> (x \<sqinter> y) = (y \<sqinter> a) \<squnion> (y \<sqinter> x)"
    5.55 +    using conj_commute by simp
    5.56 +  then have "x \<sqinter> (a \<squnion> y) = y \<sqinter> (a \<squnion> x)"
    5.57 +    using conj_disj_distrib by simp
    5.58 +  then have "x \<sqinter> \<one> = y \<sqinter> \<one>"
    5.59 +    using 2 4 by simp
    5.60 +  then show "x = y"
    5.61 +    using conj_one_right by simp
    5.62  qed
    5.63  
    5.64 -lemma compl_unique: "\<lbrakk>x \<sqinter> y = \<zero>; x \<squnion> y = \<one>\<rbrakk> \<Longrightarrow> \<sim> x = y"
    5.65 -by (rule complement_unique [OF conj_cancel_right disj_cancel_right])
    5.66 +lemma compl_unique: "x \<sqinter> y = \<zero> \<Longrightarrow> x \<squnion> y = \<one> \<Longrightarrow> \<sim> x = y"
    5.67 +  by (rule complement_unique [OF conj_cancel_right disj_cancel_right])
    5.68  
    5.69  lemma double_compl [simp]: "\<sim> (\<sim> x) = x"
    5.70  proof (rule compl_unique)
    5.71 -  from conj_cancel_right show "\<sim> x \<sqinter> x = \<zero>" by (simp only: conj_commute)
    5.72 -  from disj_cancel_right show "\<sim> x \<squnion> x = \<one>" by (simp only: disj_commute)
    5.73 +  from conj_cancel_right show "\<sim> x \<sqinter> x = \<zero>"
    5.74 +    by (simp only: conj_commute)
    5.75 +  from disj_cancel_right show "\<sim> x \<squnion> x = \<one>"
    5.76 +    by (simp only: disj_commute)
    5.77  qed
    5.78  
    5.79 -lemma compl_eq_compl_iff [simp]: "(\<sim> x = \<sim> y) = (x = y)"
    5.80 -by (rule inj_eq [OF inj_on_inverseI], rule double_compl)
    5.81 +lemma compl_eq_compl_iff [simp]: "\<sim> x = \<sim> y \<longleftrightarrow> x = y"
    5.82 +  by (rule inj_eq [OF inj_on_inverseI]) (rule double_compl)
    5.83  
    5.84  
    5.85  subsection \<open>Conjunction\<close>
    5.86  
    5.87  lemma conj_absorb [simp]: "x \<sqinter> x = x"
    5.88  proof -
    5.89 -  have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>" using disj_zero_right by simp
    5.90 -  also have "... = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)" using conj_cancel_right by simp
    5.91 -  also have "... = x \<sqinter> (x \<squnion> \<sim> x)" using conj_disj_distrib by (simp only:)
    5.92 -  also have "... = x \<sqinter> \<one>" using disj_cancel_right by simp
    5.93 -  also have "... = x" using conj_one_right by simp
    5.94 +  have "x \<sqinter> x = (x \<sqinter> x) \<squnion> \<zero>"
    5.95 +    using disj_zero_right by simp
    5.96 +  also have "... = (x \<sqinter> x) \<squnion> (x \<sqinter> \<sim> x)"
    5.97 +    using conj_cancel_right by simp
    5.98 +  also have "... = x \<sqinter> (x \<squnion> \<sim> x)"
    5.99 +    using conj_disj_distrib by (simp only:)
   5.100 +  also have "... = x \<sqinter> \<one>"
   5.101 +    using disj_cancel_right by simp
   5.102 +  also have "... = x"
   5.103 +    using conj_one_right by simp
   5.104    finally show ?thesis .
   5.105  qed
   5.106  
   5.107  lemma conj_zero_right [simp]: "x \<sqinter> \<zero> = \<zero>"
   5.108  proof -
   5.109 -  have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)" using conj_cancel_right by simp
   5.110 -  also have "... = (x \<sqinter> x) \<sqinter> \<sim> x" using conj_assoc by (simp only:)
   5.111 -  also have "... = x \<sqinter> \<sim> x" using conj_absorb by simp
   5.112 -  also have "... = \<zero>" using conj_cancel_right by simp
   5.113 +  have "x \<sqinter> \<zero> = x \<sqinter> (x \<sqinter> \<sim> x)"
   5.114 +    using conj_cancel_right by simp
   5.115 +  also have "... = (x \<sqinter> x) \<sqinter> \<sim> x"
   5.116 +    using conj_assoc by (simp only:)
   5.117 +  also have "... = x \<sqinter> \<sim> x"
   5.118 +    using conj_absorb by simp
   5.119 +  also have "... = \<zero>"
   5.120 +    using conj_cancel_right by simp
   5.121    finally show ?thesis .
   5.122  qed
   5.123  
   5.124  lemma compl_one [simp]: "\<sim> \<one> = \<zero>"
   5.125 -by (rule compl_unique [OF conj_zero_right disj_zero_right])
   5.126 +  by (rule compl_unique [OF conj_zero_right disj_zero_right])
   5.127  
   5.128  lemma conj_zero_left [simp]: "\<zero> \<sqinter> x = \<zero>"
   5.129 -by (subst conj_commute) (rule conj_zero_right)
   5.130 +  by (subst conj_commute) (rule conj_zero_right)
   5.131  
   5.132  lemma conj_one_left [simp]: "\<one> \<sqinter> x = x"
   5.133 -by (subst conj_commute) (rule conj_one_right)
   5.134 +  by (subst conj_commute) (rule conj_one_right)
   5.135  
   5.136  lemma conj_cancel_left [simp]: "\<sim> x \<sqinter> x = \<zero>"
   5.137 -by (subst conj_commute) (rule conj_cancel_right)
   5.138 +  by (subst conj_commute) (rule conj_cancel_right)
   5.139  
   5.140  lemma conj_left_absorb [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
   5.141 -by (simp only: conj_assoc [symmetric] conj_absorb)
   5.142 +  by (simp only: conj_assoc [symmetric] conj_absorb)
   5.143  
   5.144 -lemma conj_disj_distrib2:
   5.145 -  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   5.146 -by (simp only: conj_commute conj_disj_distrib)
   5.147 +lemma conj_disj_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   5.148 +  by (simp only: conj_commute conj_disj_distrib)
   5.149  
   5.150 -lemmas conj_disj_distribs =
   5.151 -   conj_disj_distrib conj_disj_distrib2
   5.152 +lemmas conj_disj_distribs = conj_disj_distrib conj_disj_distrib2
   5.153  
   5.154  
   5.155  subsection \<open>Disjunction\<close>
   5.156  
   5.157  lemma disj_absorb [simp]: "x \<squnion> x = x"
   5.158 -by (rule boolean.conj_absorb [OF dual])
   5.159 +  by (rule boolean.conj_absorb [OF dual])
   5.160  
   5.161  lemma disj_one_right [simp]: "x \<squnion> \<one> = \<one>"
   5.162 -by (rule boolean.conj_zero_right [OF dual])
   5.163 +  by (rule boolean.conj_zero_right [OF dual])
   5.164  
   5.165  lemma compl_zero [simp]: "\<sim> \<zero> = \<one>"
   5.166 -by (rule boolean.compl_one [OF dual])
   5.167 +  by (rule boolean.compl_one [OF dual])
   5.168  
   5.169  lemma disj_zero_left [simp]: "\<zero> \<squnion> x = x"
   5.170 -by (rule boolean.conj_one_left [OF dual])
   5.171 +  by (rule boolean.conj_one_left [OF dual])
   5.172  
   5.173  lemma disj_one_left [simp]: "\<one> \<squnion> x = \<one>"
   5.174 -by (rule boolean.conj_zero_left [OF dual])
   5.175 +  by (rule boolean.conj_zero_left [OF dual])
   5.176  
   5.177  lemma disj_cancel_left [simp]: "\<sim> x \<squnion> x = \<one>"
   5.178 -by (rule boolean.conj_cancel_left [OF dual])
   5.179 +  by (rule boolean.conj_cancel_left [OF dual])
   5.180  
   5.181  lemma disj_left_absorb [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
   5.182 -by (rule boolean.conj_left_absorb [OF dual])
   5.183 +  by (rule boolean.conj_left_absorb [OF dual])
   5.184  
   5.185 -lemma disj_conj_distrib2:
   5.186 -  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   5.187 -by (rule boolean.conj_disj_distrib2 [OF dual])
   5.188 +lemma disj_conj_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   5.189 +  by (rule boolean.conj_disj_distrib2 [OF dual])
   5.190  
   5.191 -lemmas disj_conj_distribs =
   5.192 -   disj_conj_distrib disj_conj_distrib2
   5.193 +lemmas disj_conj_distribs = disj_conj_distrib disj_conj_distrib2
   5.194  
   5.195  
   5.196  subsection \<open>De Morgan's Laws\<close>
   5.197 @@ -178,7 +190,7 @@
   5.198  qed
   5.199  
   5.200  lemma de_Morgan_disj [simp]: "\<sim> (x \<squnion> y) = \<sim> x \<sqinter> \<sim> y"
   5.201 -by (rule boolean.de_Morgan_conj [OF dual])
   5.202 +  by (rule boolean.de_Morgan_conj [OF dual])
   5.203  
   5.204  end
   5.205  
   5.206 @@ -198,7 +210,7 @@
   5.207    have "?t \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> y \<sqinter> \<sim> y) =
   5.208          ?t \<squnion> (x \<sqinter> y \<sqinter> \<sim> y) \<squnion> (x \<sqinter> z \<sqinter> \<sim> z)"
   5.209      by (simp only: conj_cancel_right conj_zero_right)
   5.210 -  thus "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
   5.211 +  then show "(x \<oplus> y) \<oplus> z = x \<oplus> (y \<oplus> z)"
   5.212      apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   5.213      apply (simp only: conj_disj_distribs conj_ac disj_ac)
   5.214      done
   5.215 @@ -212,57 +224,55 @@
   5.216  
   5.217  lemmas xor_ac = xor.assoc xor.commute xor.left_commute
   5.218  
   5.219 -lemma xor_def2:
   5.220 -  "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
   5.221 -by (simp only: xor_def conj_disj_distribs
   5.222 -               disj_ac conj_ac conj_cancel_right disj_zero_left)
   5.223 +lemma xor_def2: "x \<oplus> y = (x \<squnion> y) \<sqinter> (\<sim> x \<squnion> \<sim> y)"
   5.224 +  by (simp only: xor_def conj_disj_distribs disj_ac conj_ac conj_cancel_right disj_zero_left)
   5.225  
   5.226  lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"
   5.227 -by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)
   5.228 +  by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)
   5.229  
   5.230  lemma xor_zero_left [simp]: "\<zero> \<oplus> x = x"
   5.231 -by (subst xor_commute) (rule xor_zero_right)
   5.232 +  by (subst xor_commute) (rule xor_zero_right)
   5.233  
   5.234  lemma xor_one_right [simp]: "x \<oplus> \<one> = \<sim> x"
   5.235 -by (simp only: xor_def compl_one conj_zero_right conj_one_right disj_zero_left)
   5.236 +  by (simp only: xor_def compl_one conj_zero_right conj_one_right disj_zero_left)
   5.237  
   5.238  lemma xor_one_left [simp]: "\<one> \<oplus> x = \<sim> x"
   5.239 -by (subst xor_commute) (rule xor_one_right)
   5.240 +  by (subst xor_commute) (rule xor_one_right)
   5.241  
   5.242  lemma xor_self [simp]: "x \<oplus> x = \<zero>"
   5.243 -by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right)
   5.244 +  by (simp only: xor_def conj_cancel_right conj_cancel_left disj_zero_right)
   5.245  
   5.246  lemma xor_left_self [simp]: "x \<oplus> (x \<oplus> y) = y"
   5.247 -by (simp only: xor_assoc [symmetric] xor_self xor_zero_left)
   5.248 +  by (simp only: xor_assoc [symmetric] xor_self xor_zero_left)
   5.249  
   5.250  lemma xor_compl_left [simp]: "\<sim> x \<oplus> y = \<sim> (x \<oplus> y)"
   5.251 -apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   5.252 -apply (simp only: conj_disj_distribs)
   5.253 -apply (simp only: conj_cancel_right conj_cancel_left)
   5.254 -apply (simp only: disj_zero_left disj_zero_right)
   5.255 -apply (simp only: disj_ac conj_ac)
   5.256 -done
   5.257 +  apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   5.258 +  apply (simp only: conj_disj_distribs)
   5.259 +  apply (simp only: conj_cancel_right conj_cancel_left)
   5.260 +  apply (simp only: disj_zero_left disj_zero_right)
   5.261 +  apply (simp only: disj_ac conj_ac)
   5.262 +  done
   5.263  
   5.264  lemma xor_compl_right [simp]: "x \<oplus> \<sim> y = \<sim> (x \<oplus> y)"
   5.265 -apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   5.266 -apply (simp only: conj_disj_distribs)
   5.267 -apply (simp only: conj_cancel_right conj_cancel_left)
   5.268 -apply (simp only: disj_zero_left disj_zero_right)
   5.269 -apply (simp only: disj_ac conj_ac)
   5.270 -done
   5.271 +  apply (simp only: xor_def de_Morgan_disj de_Morgan_conj double_compl)
   5.272 +  apply (simp only: conj_disj_distribs)
   5.273 +  apply (simp only: conj_cancel_right conj_cancel_left)
   5.274 +  apply (simp only: disj_zero_left disj_zero_right)
   5.275 +  apply (simp only: disj_ac conj_ac)
   5.276 +  done
   5.277  
   5.278  lemma xor_cancel_right: "x \<oplus> \<sim> x = \<one>"
   5.279 -by (simp only: xor_compl_right xor_self compl_zero)
   5.280 +  by (simp only: xor_compl_right xor_self compl_zero)
   5.281  
   5.282  lemma xor_cancel_left: "\<sim> x \<oplus> x = \<one>"
   5.283 -by (simp only: xor_compl_left xor_self compl_zero)
   5.284 +  by (simp only: xor_compl_left xor_self compl_zero)
   5.285  
   5.286  lemma conj_xor_distrib: "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
   5.287  proof -
   5.288 -  have "(x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z) =
   5.289 +  have *: "(x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z) =
   5.290          (y \<sqinter> x \<sqinter> \<sim> x) \<squnion> (z \<sqinter> x \<sqinter> \<sim> x) \<squnion> (x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> z)"
   5.291      by (simp only: conj_cancel_right conj_zero_right disj_zero_left)
   5.292 -  thus "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
   5.293 +  then show "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
   5.294      by (simp (no_asm_use) only:
   5.295          xor_def de_Morgan_disj de_Morgan_conj double_compl
   5.296          conj_disj_distribs conj_ac disj_ac)
   5.297 @@ -272,7 +282,7 @@
   5.298  proof -
   5.299    have "x \<sqinter> (y \<oplus> z) = (x \<sqinter> y) \<oplus> (x \<sqinter> z)"
   5.300      by (rule conj_xor_distrib)
   5.301 -  thus "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
   5.302 +  then show "(y \<oplus> z) \<sqinter> x = (y \<sqinter> x) \<oplus> (z \<sqinter> x)"
   5.303      by (simp only: conj_commute)
   5.304  qed
   5.305  
     6.1 --- a/src/HOL/Library/Char_ord.thy	Tue Jul 12 14:53:47 2016 +0200
     6.2 +++ b/src/HOL/Library/Char_ord.thy	Tue Jul 12 15:45:32 2016 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  section \<open>Order on characters\<close>
     6.5  
     6.6  theory Char_ord
     6.7 -imports Main
     6.8 +  imports Main
     6.9  begin
    6.10  
    6.11  instantiation char :: linorder
    6.12 @@ -20,17 +20,19 @@
    6.13  end
    6.14  
    6.15  lemma less_eq_char_simps:
    6.16 -  "(0 :: char) \<le> c"
    6.17 +  "0 \<le> c"
    6.18    "Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)"
    6.19    "Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)"
    6.20 +  for c :: char
    6.21    by (simp_all add: Char_def less_eq_char_def)
    6.22  
    6.23  lemma less_char_simps:
    6.24 -  "\<not> c < (0 :: char)"
    6.25 +  "\<not> c < 0"
    6.26    "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
    6.27    "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
    6.28 +  for c :: char
    6.29    by (simp_all add: Char_def less_char_def)
    6.30 -  
    6.31 +
    6.32  instantiation char :: distrib_lattice
    6.33  begin
    6.34  
    6.35 @@ -45,28 +47,34 @@
    6.36  instantiation String.literal :: linorder
    6.37  begin
    6.38  
    6.39 -context includes literal.lifting begin
    6.40 -lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp op <" .
    6.41 -lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool" is "ord.lexordp_eq op <" .
    6.42 +context includes literal.lifting
    6.43 +begin
    6.44 +
    6.45 +lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
    6.46 +  is "ord.lexordp op <" .
    6.47 +
    6.48 +lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
    6.49 +  is "ord.lexordp_eq op <" .
    6.50  
    6.51  instance
    6.52  proof -
    6.53    interpret linorder "ord.lexordp_eq op <" "ord.lexordp op < :: string \<Rightarrow> string \<Rightarrow> bool"
    6.54 -    by(rule linorder.lexordp_linorder[where less_eq="op \<le>"])(unfold_locales)
    6.55 +    by (rule linorder.lexordp_linorder[where less_eq="op \<le>"]) unfold_locales
    6.56    show "PROP ?thesis"
    6.57 -    by(intro_classes)(transfer, simp add: less_le_not_le linear)+
    6.58 +    by intro_classes (transfer, simp add: less_le_not_le linear)+
    6.59  qed
    6.60  
    6.61  end
    6.62 +
    6.63  end
    6.64  
    6.65 -lemma less_literal_code [code]: 
    6.66 +lemma less_literal_code [code]:
    6.67    "op < = (\<lambda>xs ys. ord.lexordp op < (String.explode xs) (String.explode ys))"
    6.68 -by(simp add: less_literal.rep_eq fun_eq_iff)
    6.69 +  by (simp add: less_literal.rep_eq fun_eq_iff)
    6.70  
    6.71  lemma less_eq_literal_code [code]:
    6.72    "op \<le> = (\<lambda>xs ys. ord.lexordp_eq op < (String.explode xs) (String.explode ys))"
    6.73 -by(simp add: less_eq_literal.rep_eq fun_eq_iff)
    6.74 +  by (simp add: less_eq_literal.rep_eq fun_eq_iff)
    6.75  
    6.76  lifting_update literal.lifting
    6.77  lifting_forget literal.lifting
     7.1 --- a/src/HOL/Library/Combine_PER.thy	Tue Jul 12 14:53:47 2016 +0200
     7.2 +++ b/src/HOL/Library/Combine_PER.thy	Tue Jul 12 15:45:32 2016 +0200
     7.3 @@ -1,47 +1,37 @@
     7.4 -(* Author: Florian Haftmann, TU Muenchen *)
     7.5 +(*  Author:     Florian Haftmann, TU Muenchen *)
     7.6  
     7.7  section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
     7.8  
     7.9  theory Combine_PER
    7.10 -imports Main "~~/src/HOL/Library/Lattice_Syntax"
    7.11 +  imports Main "~~/src/HOL/Library/Lattice_Syntax"
    7.12  begin
    7.13  
    7.14  definition combine_per :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
    7.15 -where
    7.16 -  "combine_per P R = (\<lambda>x y. P x \<and> P y) \<sqinter> R"
    7.17 +  where "combine_per P R = (\<lambda>x y. P x \<and> P y) \<sqinter> R"
    7.18  
    7.19  lemma combine_per_simp [simp]:
    7.20 -  fixes R (infixl "\<approx>" 50)
    7.21 -  shows "combine_per P R x y \<longleftrightarrow> P x \<and> P y \<and> x \<approx> y"
    7.22 +  "combine_per P R x y \<longleftrightarrow> P x \<and> P y \<and> x \<approx> y" for R (infixl "\<approx>" 50)
    7.23    by (simp add: combine_per_def)
    7.24  
    7.25 -lemma combine_per_top [simp]:
    7.26 -  "combine_per \<top> R = R"
    7.27 +lemma combine_per_top [simp]: "combine_per \<top> R = R"
    7.28    by (simp add: fun_eq_iff)
    7.29  
    7.30 -lemma combine_per_eq [simp]:
    7.31 -  "combine_per P HOL.eq = HOL.eq \<sqinter> (\<lambda>x y. P x)"
    7.32 +lemma combine_per_eq [simp]: "combine_per P HOL.eq = HOL.eq \<sqinter> (\<lambda>x y. P x)"
    7.33    by (auto simp add: fun_eq_iff)
    7.34  
    7.35 -lemma symp_combine_per:
    7.36 -  "symp R \<Longrightarrow> symp (combine_per P R)"
    7.37 +lemma symp_combine_per: "symp R \<Longrightarrow> symp (combine_per P R)"
    7.38    by (auto simp add: symp_def sym_def combine_per_def)
    7.39  
    7.40 -lemma transp_combine_per:
    7.41 -  "transp R \<Longrightarrow> transp (combine_per P R)"
    7.42 +lemma transp_combine_per: "transp R \<Longrightarrow> transp (combine_per P R)"
    7.43    by (auto simp add: transp_def trans_def combine_per_def)
    7.44  
    7.45 -lemma combine_perI:
    7.46 -  fixes R (infixl "\<approx>" 50)
    7.47 -  shows "P x \<Longrightarrow> P y \<Longrightarrow> x \<approx> y \<Longrightarrow> combine_per P R x y"
    7.48 +lemma combine_perI: "P x \<Longrightarrow> P y \<Longrightarrow> x \<approx> y \<Longrightarrow> combine_per P R x y" for R (infixl "\<approx>" 50)
    7.49    by (simp add: combine_per_def)
    7.50  
    7.51 -lemma symp_combine_per_symp:
    7.52 -  "symp R \<Longrightarrow> symp (combine_per P R)"
    7.53 +lemma symp_combine_per_symp: "symp R \<Longrightarrow> symp (combine_per P R)"
    7.54    by (auto intro!: sympI elim: sympE)
    7.55  
    7.56 -lemma transp_combine_per_transp:
    7.57 -  "transp R \<Longrightarrow> transp (combine_per P R)"
    7.58 +lemma transp_combine_per_transp: "transp R \<Longrightarrow> transp (combine_per P R)"
    7.59    by (auto intro!: transpI elim: transpE)
    7.60  
    7.61  lemma equivp_combine_per_part_equivp [intro?]:
    7.62 @@ -50,8 +40,10 @@
    7.63    shows "part_equivp (combine_per P R)"
    7.64  proof -
    7.65    from \<open>\<exists>x. P x\<close> obtain x where "P x" ..
    7.66 -  moreover from \<open>equivp R\<close> have "x \<approx> x" by (rule equivp_reflp)
    7.67 -  ultimately have "\<exists>x. P x \<and> x \<approx> x" by blast
    7.68 +  moreover from \<open>equivp R\<close> have "x \<approx> x"
    7.69 +    by (rule equivp_reflp)
    7.70 +  ultimately have "\<exists>x. P x \<and> x \<approx> x"
    7.71 +    by blast
    7.72    with \<open>equivp R\<close> show ?thesis
    7.73      by (auto intro!: part_equivpI symp_combine_per_symp transp_combine_per_transp
    7.74        elim: equivpE)
     8.1 --- a/src/HOL/Library/Mapping.thy	Tue Jul 12 14:53:47 2016 +0200
     8.2 +++ b/src/HOL/Library/Mapping.thy	Tue Jul 12 15:45:32 2016 +0200
     8.3 @@ -10,15 +10,13 @@
     8.4  
     8.5  subsection \<open>Parametricity transfer rules\<close>
     8.6  
     8.7 -lemma map_of_foldr: \<comment> \<open>FIXME move\<close>
     8.8 -  "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty"
     8.9 +lemma map_of_foldr: "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty"  (* FIXME move *)
    8.10    using map_add_map_of_foldr [of Map.empty] by auto
    8.11  
    8.12  context includes lifting_syntax
    8.13  begin
    8.14  
    8.15 -lemma empty_parametric:
    8.16 -  "(A ===> rel_option B) Map.empty Map.empty"
    8.17 +lemma empty_parametric: "(A ===> rel_option B) Map.empty Map.empty"
    8.18    by transfer_prover
    8.19  
    8.20  lemma lookup_parametric: "((A ===> B) ===> A ===> B) (\<lambda>m k. m k) (\<lambda>m k. m k)"
    8.21 @@ -32,7 +30,7 @@
    8.22  
    8.23  lemma delete_parametric:
    8.24    assumes [transfer_rule]: "bi_unique A"
    8.25 -  shows "(A ===> (A ===> rel_option B) ===> A ===> rel_option B) 
    8.26 +  shows "(A ===> (A ===> rel_option B) ===> A ===> rel_option B)
    8.27      (\<lambda>k m. m(k := None)) (\<lambda>k m. m(k := None))"
    8.28    by transfer_prover
    8.29  
    8.30 @@ -42,7 +40,7 @@
    8.31  
    8.32  lemma dom_parametric:
    8.33    assumes [transfer_rule]: "bi_total A"
    8.34 -  shows "((A ===> rel_option B) ===> rel_set A) dom dom" 
    8.35 +  shows "((A ===> rel_option B) ===> rel_set A) dom dom"
    8.36    unfolding dom_def [abs_def] Option.is_none_def [symmetric] by transfer_prover
    8.37  
    8.38  lemma map_of_parametric [transfer_rule]:
    8.39 @@ -52,51 +50,53 @@
    8.40  
    8.41  lemma map_entry_parametric [transfer_rule]:
    8.42    assumes [transfer_rule]: "bi_unique A"
    8.43 -  shows "(A ===> (B ===> B) ===> (A ===> rel_option B) ===> A ===> rel_option B) 
    8.44 +  shows "(A ===> (B ===> B) ===> (A ===> rel_option B) ===> A ===> rel_option B)
    8.45      (\<lambda>k f m. (case m k of None \<Rightarrow> m
    8.46        | Some v \<Rightarrow> m (k \<mapsto> (f v)))) (\<lambda>k f m. (case m k of None \<Rightarrow> m
    8.47        | Some v \<Rightarrow> m (k \<mapsto> (f v))))"
    8.48    by transfer_prover
    8.49  
    8.50 -lemma tabulate_parametric: 
    8.51 +lemma tabulate_parametric:
    8.52    assumes [transfer_rule]: "bi_unique A"
    8.53 -  shows "(list_all2 A ===> (A ===> B) ===> A ===> rel_option B) 
    8.54 +  shows "(list_all2 A ===> (A ===> B) ===> A ===> rel_option B)
    8.55      (\<lambda>ks f. (map_of (map (\<lambda>k. (k, f k)) ks))) (\<lambda>ks f. (map_of (map (\<lambda>k. (k, f k)) ks)))"
    8.56    by transfer_prover
    8.57  
    8.58 -lemma bulkload_parametric: 
    8.59 -  "(list_all2 A ===> HOL.eq ===> rel_option A) 
    8.60 -    (\<lambda>xs k. if k < length xs then Some (xs ! k) else None) (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)"
    8.61 +lemma bulkload_parametric:
    8.62 +  "(list_all2 A ===> HOL.eq ===> rel_option A)
    8.63 +    (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)
    8.64 +    (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)"
    8.65  proof
    8.66    fix xs ys
    8.67    assume "list_all2 A xs ys"
    8.68 -  then show "(HOL.eq ===> rel_option A)
    8.69 -    (\<lambda>k. if k < length xs then Some (xs ! k) else None)
    8.70 -    (\<lambda>k. if k < length ys then Some (ys ! k) else None)"
    8.71 +  then show
    8.72 +    "(HOL.eq ===> rel_option A)
    8.73 +      (\<lambda>k. if k < length xs then Some (xs ! k) else None)
    8.74 +      (\<lambda>k. if k < length ys then Some (ys ! k) else None)"
    8.75      apply induct
    8.76      apply auto
    8.77      unfolding rel_fun_def
    8.78 -    apply clarsimp 
    8.79 -    apply (case_tac xa) 
    8.80 +    apply clarsimp
    8.81 +    apply (case_tac xa)
    8.82      apply (auto dest: list_all2_lengthD list_all2_nthD)
    8.83      done
    8.84  qed
    8.85  
    8.86 -lemma map_parametric: 
    8.87 -  "((A ===> B) ===> (C ===> D) ===> (B ===> rel_option C) ===> A ===> rel_option D) 
    8.88 +lemma map_parametric:
    8.89 +  "((A ===> B) ===> (C ===> D) ===> (B ===> rel_option C) ===> A ===> rel_option D)
    8.90       (\<lambda>f g m. (map_option g \<circ> m \<circ> f)) (\<lambda>f g m. (map_option g \<circ> m \<circ> f))"
    8.91    by transfer_prover
    8.92 -  
    8.93 -lemma combine_with_key_parametric: 
    8.94 -  shows "((A ===> B ===> B ===> B) ===> (A ===> rel_option B) ===> (A ===> rel_option B) ===>
    8.95 -           (A ===> rel_option B)) (\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x))
    8.96 -           (\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x))"
    8.97 +
    8.98 +lemma combine_with_key_parametric:
    8.99 +  "((A ===> B ===> B ===> B) ===> (A ===> rel_option B) ===> (A ===> rel_option B) ===>
   8.100 +    (A ===> rel_option B)) (\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x))
   8.101 +    (\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x))"
   8.102    unfolding combine_options_def by transfer_prover
   8.103 -  
   8.104 -lemma combine_parametric: 
   8.105 -  shows "((B ===> B ===> B) ===> (A ===> rel_option B) ===> (A ===> rel_option B) ===>
   8.106 -           (A ===> rel_option B)) (\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x))
   8.107 -           (\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x))"
   8.108 +
   8.109 +lemma combine_parametric:
   8.110 +  "((B ===> B ===> B) ===> (A ===> rel_option B) ===> (A ===> rel_option B) ===>
   8.111 +    (A ===> rel_option B)) (\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x))
   8.112 +    (\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x))"
   8.113    unfolding combine_options_def by transfer_prover
   8.114  
   8.115  end
   8.116 @@ -105,8 +105,7 @@
   8.117  subsection \<open>Type definition and primitive operations\<close>
   8.118  
   8.119  typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
   8.120 -  morphisms rep Mapping
   8.121 -  ..
   8.122 +  morphisms rep Mapping ..
   8.123  
   8.124  setup_lifting type_definition_mapping
   8.125  
   8.126 @@ -119,7 +118,7 @@
   8.127  definition "lookup_default d m k = (case Mapping.lookup m k of None \<Rightarrow> d | Some v \<Rightarrow> v)"
   8.128  
   8.129  declare [[code drop: Mapping.lookup]]
   8.130 -setup \<open>Code.add_eqn (Code.Equation, true) @{thm Mapping.lookup.abs_eq}\<close> \<comment> \<open>FIXME lifting\<close>
   8.131 +setup \<open>Code.add_eqn (Code.Equation, true) @{thm Mapping.lookup.abs_eq}\<close>  (* FIXME lifting *)
   8.132  
   8.133  lift_definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   8.134    is "\<lambda>k v m. m(k \<mapsto> v)" parametric update_parametric .
   8.135 @@ -128,7 +127,7 @@
   8.136    is "\<lambda>k m. m(k := None)" parametric delete_parametric .
   8.137  
   8.138  lift_definition filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   8.139 -  is "\<lambda>P m k. case m k of None \<Rightarrow> None | Some v \<Rightarrow> if P k v then Some v else None" . 
   8.140 +  is "\<lambda>P m k. case m k of None \<Rightarrow> None | Some v \<Rightarrow> if P k v then Some v else None" .
   8.141  
   8.142  lift_definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set"
   8.143    is dom parametric dom_parametric .
   8.144 @@ -141,20 +140,20 @@
   8.145  
   8.146  lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping"
   8.147    is "\<lambda>f g m. (map_option g \<circ> m \<circ> f)" parametric map_parametric .
   8.148 -  
   8.149 +
   8.150  lift_definition map_values :: "('c \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> ('c, 'a) mapping \<Rightarrow> ('c, 'b) mapping"
   8.151 -  is "\<lambda>f m x. map_option (f x) (m x)" . 
   8.152 +  is "\<lambda>f m x. map_option (f x) (m x)" .
   8.153  
   8.154 -lift_definition combine_with_key :: 
   8.155 +lift_definition combine_with_key ::
   8.156    "('a \<Rightarrow> 'b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping"
   8.157    is "\<lambda>f m1 m2 x. combine_options (f x) (m1 x) (m2 x)" parametric combine_with_key_parametric .
   8.158  
   8.159 -lift_definition combine :: 
   8.160 +lift_definition combine ::
   8.161    "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping \<Rightarrow> ('a,'b) mapping"
   8.162    is "\<lambda>f m1 m2 x. combine_options f (m1 x) (m2 x)" parametric combine_parametric .
   8.163  
   8.164 -definition All_mapping where
   8.165 -  "All_mapping m P \<longleftrightarrow> (\<forall>x. case Mapping.lookup m x of None \<Rightarrow> True | Some y \<Rightarrow> P x y)"
   8.166 +definition "All_mapping m P \<longleftrightarrow>
   8.167 +  (\<forall>x. case Mapping.lookup m x of None \<Rightarrow> True | Some y \<Rightarrow> P x y)"
   8.168  
   8.169  declare [[code drop: map]]
   8.170  
   8.171 @@ -168,52 +167,52 @@
   8.172  subsection \<open>Derived operations\<close>
   8.173  
   8.174  definition ordered_keys :: "('a::linorder, 'b) mapping \<Rightarrow> 'a list"
   8.175 -where
   8.176 -  "ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])"
   8.177 +  where "ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])"
   8.178  
   8.179  definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool"
   8.180 -where
   8.181 -  "is_empty m \<longleftrightarrow> keys m = {}"
   8.182 +  where "is_empty m \<longleftrightarrow> keys m = {}"
   8.183  
   8.184  definition size :: "('a, 'b) mapping \<Rightarrow> nat"
   8.185 -where
   8.186 -  "size m = (if finite (keys m) then card (keys m) else 0)"
   8.187 +  where "size m = (if finite (keys m) then card (keys m) else 0)"
   8.188  
   8.189  definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   8.190 -where
   8.191 -  "replace k v m = (if k \<in> keys m then update k v m else m)"
   8.192 +  where "replace k v m = (if k \<in> keys m then update k v m else m)"
   8.193  
   8.194  definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   8.195 -where
   8.196 -  "default k v m = (if k \<in> keys m then m else update k v m)"
   8.197 +  where "default k v m = (if k \<in> keys m then m else update k v m)"
   8.198  
   8.199  text \<open>Manual derivation of transfer rule is non-trivial\<close>
   8.200  
   8.201  lift_definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" is
   8.202 -  "\<lambda>k f m. (case m k of None \<Rightarrow> m
   8.203 +  "\<lambda>k f m.
   8.204 +    (case m k of
   8.205 +      None \<Rightarrow> m
   8.206      | Some v \<Rightarrow> m (k \<mapsto> (f v)))" parametric map_entry_parametric .
   8.207  
   8.208  lemma map_entry_code [code]:
   8.209 -  "map_entry k f m = (case lookup m k of None \<Rightarrow> m
   8.210 +  "map_entry k f m =
   8.211 +    (case lookup m k of
   8.212 +      None \<Rightarrow> m
   8.213      | Some v \<Rightarrow> update k (f v) m)"
   8.214    by transfer rule
   8.215  
   8.216  definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping"
   8.217 -where
   8.218 -  "map_default k v f m = map_entry k f (default k v m)" 
   8.219 +  where "map_default k v f m = map_entry k f (default k v m)"
   8.220  
   8.221  definition of_alist :: "('k \<times> 'v) list \<Rightarrow> ('k, 'v) mapping"
   8.222 -where
   8.223 -  "of_alist xs = foldr (\<lambda>(k, v) m. update k v m) xs empty"
   8.224 +  where "of_alist xs = foldr (\<lambda>(k, v) m. update k v m) xs empty"
   8.225  
   8.226  instantiation mapping :: (type, type) equal
   8.227  begin
   8.228  
   8.229 -definition
   8.230 -  "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
   8.231 +definition "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
   8.232  
   8.233  instance
   8.234 -  by standard (unfold equal_mapping_def, transfer, auto)
   8.235 +  apply standard
   8.236 +  unfolding equal_mapping_def
   8.237 +  apply transfer
   8.238 +  apply auto
   8.239 +  done
   8.240  
   8.241  end
   8.242  
   8.243 @@ -222,9 +221,9 @@
   8.244  
   8.245  lemma [transfer_rule]:
   8.246    assumes [transfer_rule]: "bi_total A"
   8.247 -  assumes [transfer_rule]: "bi_unique B"
   8.248 +    and [transfer_rule]: "bi_unique B"
   8.249    shows "(pcr_mapping A B ===> pcr_mapping A B ===> op=) HOL.eq HOL.equal"
   8.250 -  by (unfold equal) transfer_prover
   8.251 +  unfolding equal by transfer_prover
   8.252  
   8.253  lemma of_alist_transfer [transfer_rule]:
   8.254    assumes [transfer_rule]: "bi_unique R1"
   8.255 @@ -236,195 +235,186 @@
   8.256  
   8.257  subsection \<open>Properties\<close>
   8.258  
   8.259 -lemma mapping_eqI:
   8.260 -  "(\<And>x. lookup m x = lookup m' x) \<Longrightarrow> m = m'"
   8.261 +lemma mapping_eqI: "(\<And>x. lookup m x = lookup m' x) \<Longrightarrow> m = m'"
   8.262    by transfer (simp add: fun_eq_iff)
   8.263  
   8.264 -lemma mapping_eqI': 
   8.265 -  assumes "\<And>x. x \<in> Mapping.keys m \<Longrightarrow> Mapping.lookup_default d m x = Mapping.lookup_default d m' x" 
   8.266 -      and "Mapping.keys m = Mapping.keys m'"
   8.267 -  shows   "m = m'"
   8.268 +lemma mapping_eqI':
   8.269 +  assumes "\<And>x. x \<in> Mapping.keys m \<Longrightarrow> Mapping.lookup_default d m x = Mapping.lookup_default d m' x"
   8.270 +    and "Mapping.keys m = Mapping.keys m'"
   8.271 +  shows "m = m'"
   8.272  proof (intro mapping_eqI)
   8.273 -  fix x
   8.274 -  show "Mapping.lookup m x = Mapping.lookup m' x"
   8.275 +  show "Mapping.lookup m x = Mapping.lookup m' x" for x
   8.276    proof (cases "Mapping.lookup m x")
   8.277      case None
   8.278 -    hence "x \<notin> Mapping.keys m" by transfer (simp add: dom_def)
   8.279 -    hence "x \<notin> Mapping.keys m'" by (simp add: assms)
   8.280 -    hence "Mapping.lookup m' x = None" by transfer (simp add: dom_def)
   8.281 -    with None show ?thesis by simp
   8.282 +    then have "x \<notin> Mapping.keys m"
   8.283 +      by transfer (simp add: dom_def)
   8.284 +    then have "x \<notin> Mapping.keys m'"
   8.285 +      by (simp add: assms)
   8.286 +    then have "Mapping.lookup m' x = None"
   8.287 +      by transfer (simp add: dom_def)
   8.288 +    with None show ?thesis
   8.289 +      by simp
   8.290    next
   8.291      case (Some y)
   8.292 -    hence A: "x \<in> Mapping.keys m" by transfer (simp add: dom_def)
   8.293 -    hence "x \<in> Mapping.keys m'" by (simp add: assms)
   8.294 -    hence "\<exists>y'. Mapping.lookup m' x = Some y'" by transfer (simp add: dom_def)
   8.295 -    with Some assms(1)[OF A] show ?thesis by (auto simp add: lookup_default_def)
   8.296 +    then have A: "x \<in> Mapping.keys m"
   8.297 +      by transfer (simp add: dom_def)
   8.298 +    then have "x \<in> Mapping.keys m'"
   8.299 +      by (simp add: assms)
   8.300 +    then have "\<exists>y'. Mapping.lookup m' x = Some y'"
   8.301 +      by transfer (simp add: dom_def)
   8.302 +    with Some assms(1)[OF A] show ?thesis
   8.303 +      by (auto simp add: lookup_default_def)
   8.304    qed
   8.305  qed
   8.306  
   8.307 -lemma lookup_update:
   8.308 -  "lookup (update k v m) k = Some v" 
   8.309 +lemma lookup_update: "lookup (update k v m) k = Some v"
   8.310    by transfer simp
   8.311  
   8.312 -lemma lookup_update_neq:
   8.313 -  "k \<noteq> k' \<Longrightarrow> lookup (update k v m) k' = lookup m k'" 
   8.314 +lemma lookup_update_neq: "k \<noteq> k' \<Longrightarrow> lookup (update k v m) k' = lookup m k'"
   8.315    by transfer simp
   8.316  
   8.317 -lemma lookup_update': 
   8.318 -  "Mapping.lookup (update k v m) k' = (if k = k' then Some v else lookup m k')"
   8.319 +lemma lookup_update': "Mapping.lookup (update k v m) k' = (if k = k' then Some v else lookup m k')"
   8.320    by (auto simp: lookup_update lookup_update_neq)
   8.321  
   8.322 -lemma lookup_empty:
   8.323 -  "lookup empty k = None" 
   8.324 +lemma lookup_empty: "lookup empty k = None"
   8.325    by transfer simp
   8.326  
   8.327  lemma lookup_filter:
   8.328 -  "lookup (filter P m) k = 
   8.329 -     (case lookup m k of None \<Rightarrow> None | Some v \<Rightarrow> if P k v then Some v else None)"
   8.330 +  "lookup (filter P m) k =
   8.331 +    (case lookup m k of
   8.332 +      None \<Rightarrow> None
   8.333 +    | Some v \<Rightarrow> if P k v then Some v else None)"
   8.334    by transfer simp_all
   8.335  
   8.336 -lemma lookup_map_values:
   8.337 -  "lookup (map_values f m) k = map_option (f k) (lookup m k)"
   8.338 +lemma lookup_map_values: "lookup (map_values f m) k = map_option (f k) (lookup m k)"
   8.339    by transfer simp_all
   8.340  
   8.341  lemma lookup_default_empty: "lookup_default d empty k = d"
   8.342    by (simp add: lookup_default_def lookup_empty)
   8.343  
   8.344 -lemma lookup_default_update:
   8.345 -  "lookup_default d (update k v m) k = v" 
   8.346 +lemma lookup_default_update: "lookup_default d (update k v m) k = v"
   8.347    by (simp add: lookup_default_def lookup_update)
   8.348  
   8.349  lemma lookup_default_update_neq:
   8.350 -  "k \<noteq> k' \<Longrightarrow> lookup_default d (update k v m) k' = lookup_default d m k'" 
   8.351 +  "k \<noteq> k' \<Longrightarrow> lookup_default d (update k v m) k' = lookup_default d m k'"
   8.352    by (simp add: lookup_default_def lookup_update_neq)
   8.353  
   8.354 -lemma lookup_default_update': 
   8.355 +lemma lookup_default_update':
   8.356    "lookup_default d (update k v m) k' = (if k = k' then v else lookup_default d m k')"
   8.357    by (auto simp: lookup_default_update lookup_default_update_neq)
   8.358  
   8.359  lemma lookup_default_filter:
   8.360 -  "lookup_default d (filter P m) k =  
   8.361 +  "lookup_default d (filter P m) k =
   8.362       (if P k (lookup_default d m k) then lookup_default d m k else d)"
   8.363    by (simp add: lookup_default_def lookup_filter split: option.splits)
   8.364  
   8.365  lemma lookup_default_map_values:
   8.366    "lookup_default (f k d) (map_values f m) k = f k (lookup_default d m k)"
   8.367 -  by (simp add: lookup_default_def lookup_map_values split: option.splits)  
   8.368 +  by (simp add: lookup_default_def lookup_map_values split: option.splits)
   8.369  
   8.370  lemma lookup_combine_with_key:
   8.371 -  "Mapping.lookup (combine_with_key f m1 m2) x = 
   8.372 -     combine_options (f x) (Mapping.lookup m1 x) (Mapping.lookup m2 x)"
   8.373 +  "Mapping.lookup (combine_with_key f m1 m2) x =
   8.374 +    combine_options (f x) (Mapping.lookup m1 x) (Mapping.lookup m2 x)"
   8.375    by transfer (auto split: option.splits)
   8.376 -  
   8.377 +
   8.378  lemma combine_altdef: "combine f m1 m2 = combine_with_key (\<lambda>_. f) m1 m2"
   8.379    by transfer' (rule refl)
   8.380  
   8.381  lemma lookup_combine:
   8.382 -  "Mapping.lookup (combine f m1 m2) x = 
   8.383 +  "Mapping.lookup (combine f m1 m2) x =
   8.384       combine_options f (Mapping.lookup m1 x) (Mapping.lookup m2 x)"
   8.385    by transfer (auto split: option.splits)
   8.386 -  
   8.387 -lemma lookup_default_neutral_combine_with_key: 
   8.388 +
   8.389 +lemma lookup_default_neutral_combine_with_key:
   8.390    assumes "\<And>x. f k d x = x" "\<And>x. f k x d = x"
   8.391 -  shows   "Mapping.lookup_default d (combine_with_key f m1 m2) k = 
   8.392 -             f k (Mapping.lookup_default d m1 k) (Mapping.lookup_default d m2 k)"
   8.393 +  shows "Mapping.lookup_default d (combine_with_key f m1 m2) k =
   8.394 +    f k (Mapping.lookup_default d m1 k) (Mapping.lookup_default d m2 k)"
   8.395    by (auto simp: lookup_default_def lookup_combine_with_key assms split: option.splits)
   8.396 -  
   8.397 -lemma lookup_default_neutral_combine: 
   8.398 +
   8.399 +lemma lookup_default_neutral_combine:
   8.400    assumes "\<And>x. f d x = x" "\<And>x. f x d = x"
   8.401 -  shows   "Mapping.lookup_default d (combine f m1 m2) x = 
   8.402 -             f (Mapping.lookup_default d m1 x) (Mapping.lookup_default d m2 x)"
   8.403 +  shows "Mapping.lookup_default d (combine f m1 m2) x =
   8.404 +    f (Mapping.lookup_default d m1 x) (Mapping.lookup_default d m2 x)"
   8.405    by (auto simp: lookup_default_def lookup_combine assms split: option.splits)
   8.406  
   8.407 -lemma lookup_map_entry:
   8.408 -  "lookup (map_entry x f m) x = map_option f (lookup m x)"
   8.409 +lemma lookup_map_entry: "lookup (map_entry x f m) x = map_option f (lookup m x)"
   8.410    by transfer (auto split: option.splits)
   8.411  
   8.412 -lemma lookup_map_entry_neq:
   8.413 -  "x \<noteq> y \<Longrightarrow> lookup (map_entry x f m) y = lookup m y"
   8.414 +lemma lookup_map_entry_neq: "x \<noteq> y \<Longrightarrow> lookup (map_entry x f m) y = lookup m y"
   8.415    by transfer (auto split: option.splits)
   8.416  
   8.417  lemma lookup_map_entry':
   8.418 -  "lookup (map_entry x f m) y = 
   8.419 +  "lookup (map_entry x f m) y =
   8.420       (if x = y then map_option f (lookup m y) else lookup m y)"
   8.421    by transfer (auto split: option.splits)
   8.422 -  
   8.423 -lemma lookup_default:
   8.424 -  "lookup (default x d m) x = Some (lookup_default d m x)"
   8.425 -    unfolding lookup_default_def default_def
   8.426 -    by transfer (auto split: option.splits)
   8.427  
   8.428 -lemma lookup_default_neq:
   8.429 -  "x \<noteq> y \<Longrightarrow> lookup (default x d m) y = lookup m y"
   8.430 -    unfolding lookup_default_def default_def
   8.431 -    by transfer (auto split: option.splits)
   8.432 +lemma lookup_default: "lookup (default x d m) x = Some (lookup_default d m x)"
   8.433 +  unfolding lookup_default_def default_def
   8.434 +  by transfer (auto split: option.splits)
   8.435 +
   8.436 +lemma lookup_default_neq: "x \<noteq> y \<Longrightarrow> lookup (default x d m) y = lookup m y"
   8.437 +  unfolding lookup_default_def default_def
   8.438 +  by transfer (auto split: option.splits)
   8.439  
   8.440  lemma lookup_default':
   8.441 -  "lookup (default x d m) y = 
   8.442 -     (if x = y then Some (lookup_default d m x) else lookup m y)"
   8.443 +  "lookup (default x d m) y =
   8.444 +    (if x = y then Some (lookup_default d m x) else lookup m y)"
   8.445    unfolding lookup_default_def default_def
   8.446    by transfer (auto split: option.splits)
   8.447 -  
   8.448 -lemma lookup_map_default:
   8.449 -  "lookup (map_default x d f m) x = Some (f (lookup_default d m x))"
   8.450 -    unfolding lookup_default_def default_def
   8.451 -    by (simp add: map_default_def lookup_map_entry lookup_default lookup_default_def)
   8.452  
   8.453 -lemma lookup_map_default_neq:
   8.454 -  "x \<noteq> y \<Longrightarrow> lookup (map_default x d f m) y = lookup m y"
   8.455 -    unfolding lookup_default_def default_def
   8.456 -    by (simp add: map_default_def lookup_map_entry_neq lookup_default_neq) 
   8.457 +lemma lookup_map_default: "lookup (map_default x d f m) x = Some (f (lookup_default d m x))"
   8.458 +  unfolding lookup_default_def default_def
   8.459 +  by (simp add: map_default_def lookup_map_entry lookup_default lookup_default_def)
   8.460 +
   8.461 +lemma lookup_map_default_neq: "x \<noteq> y \<Longrightarrow> lookup (map_default x d f m) y = lookup m y"
   8.462 +  unfolding lookup_default_def default_def
   8.463 +  by (simp add: map_default_def lookup_map_entry_neq lookup_default_neq)
   8.464  
   8.465  lemma lookup_map_default':
   8.466 -  "lookup (map_default x d f m) y = 
   8.467 -     (if x = y then Some (f (lookup_default d m x)) else lookup m y)"
   8.468 -    unfolding lookup_default_def default_def
   8.469 -    by (simp add: map_default_def lookup_map_entry' lookup_default' lookup_default_def)  
   8.470 +  "lookup (map_default x d f m) y =
   8.471 +    (if x = y then Some (f (lookup_default d m x)) else lookup m y)"
   8.472 +  unfolding lookup_default_def default_def
   8.473 +  by (simp add: map_default_def lookup_map_entry' lookup_default' lookup_default_def)
   8.474  
   8.475 -lemma lookup_tabulate: 
   8.476 +lemma lookup_tabulate:
   8.477    assumes "distinct xs"
   8.478 -  shows   "Mapping.lookup (Mapping.tabulate xs f) x = (if x \<in> set xs then Some (f x) else None)"
   8.479 +  shows "Mapping.lookup (Mapping.tabulate xs f) x = (if x \<in> set xs then Some (f x) else None)"
   8.480    using assms by transfer (auto simp: map_of_eq_None_iff o_def dest!: map_of_SomeD)
   8.481  
   8.482  lemma lookup_of_alist: "Mapping.lookup (Mapping.of_alist xs) k = map_of xs k"
   8.483    by transfer simp_all
   8.484  
   8.485 -lemma keys_is_none_rep [code_unfold]:
   8.486 -  "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
   8.487 +lemma keys_is_none_rep [code_unfold]: "k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))"
   8.488    by transfer (auto simp add: Option.is_none_def)
   8.489  
   8.490  lemma update_update:
   8.491    "update k v (update k w m) = update k v m"
   8.492    "k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)"
   8.493 -  by (transfer, simp add: fun_upd_twist)+
   8.494 +  by (transfer; simp add: fun_upd_twist)+
   8.495  
   8.496 -lemma update_delete [simp]:
   8.497 -  "update k v (delete k m) = update k v m"
   8.498 +lemma update_delete [simp]: "update k v (delete k m) = update k v m"
   8.499    by transfer simp
   8.500  
   8.501  lemma delete_update:
   8.502    "delete k (update k v m) = delete k m"
   8.503    "k \<noteq> l \<Longrightarrow> delete k (update l v m) = update l v (delete k m)"
   8.504 -  by (transfer, simp add: fun_upd_twist)+
   8.505 +  by (transfer; simp add: fun_upd_twist)+
   8.506  
   8.507 -lemma delete_empty [simp]:
   8.508 -  "delete k empty = empty"
   8.509 +lemma delete_empty [simp]: "delete k empty = empty"
   8.510    by transfer simp
   8.511  
   8.512  lemma replace_update:
   8.513    "k \<notin> keys m \<Longrightarrow> replace k v m = m"
   8.514    "k \<in> keys m \<Longrightarrow> replace k v m = update k v m"
   8.515 -  by (transfer, auto simp add: replace_def fun_upd_twist)+
   8.516 -  
   8.517 +  by (transfer; auto simp add: replace_def fun_upd_twist)+
   8.518 +
   8.519  lemma map_values_update: "map_values f (update k v m) = update k (f k v) (map_values f m)"
   8.520    by transfer (simp_all add: fun_eq_iff)
   8.521 -  
   8.522 -lemma size_mono:
   8.523 -  "finite (keys m') \<Longrightarrow> keys m \<subseteq> keys m' \<Longrightarrow> size m \<le> size m'"
   8.524 +
   8.525 +lemma size_mono: "finite (keys m') \<Longrightarrow> keys m \<subseteq> keys m' \<Longrightarrow> size m \<le> size m'"
   8.526    unfolding size_def by (auto intro: card_mono)
   8.527  
   8.528 -lemma size_empty [simp]:
   8.529 -  "size empty = 0"
   8.530 +lemma size_empty [simp]: "size empty = 0"
   8.531    unfolding size_def by transfer simp
   8.532  
   8.533  lemma size_update:
   8.534 @@ -432,13 +422,11 @@
   8.535      (if k \<in> keys m then size m else Suc (size m))"
   8.536    unfolding size_def by transfer (auto simp add: insert_dom)
   8.537  
   8.538 -lemma size_delete:
   8.539 -  "size (delete k m) = (if k \<in> keys m then size m - 1 else size m)"
   8.540 +lemma size_delete: "size (delete k m) = (if k \<in> keys m then size m - 1 else size m)"
   8.541    unfolding size_def by transfer simp
   8.542  
   8.543 -lemma size_tabulate [simp]:
   8.544 -  "size (tabulate ks f) = length (remdups ks)"
   8.545 -  unfolding size_def by transfer (auto simp add: map_of_map_restrict  card_set comp_def)
   8.546 +lemma size_tabulate [simp]: "size (tabulate ks f) = length (remdups ks)"
   8.547 +  unfolding size_def by transfer (auto simp add: map_of_map_restrict card_set comp_def)
   8.548  
   8.549  lemma keys_filter: "keys (filter P m) \<subseteq> keys m"
   8.550    by transfer (auto split: option.splits)
   8.551 @@ -446,131 +434,113 @@
   8.552  lemma size_filter: "finite (keys m) \<Longrightarrow> size (filter P m) \<le> size m"
   8.553    by (intro size_mono keys_filter)
   8.554  
   8.555 -
   8.556 -lemma bulkload_tabulate:
   8.557 -  "bulkload xs = tabulate [0..<length xs] (nth xs)"
   8.558 +lemma bulkload_tabulate: "bulkload xs = tabulate [0..<length xs] (nth xs)"
   8.559    by transfer (auto simp add: map_of_map_restrict)
   8.560  
   8.561 -lemma is_empty_empty [simp]:
   8.562 -  "is_empty empty"
   8.563 -  unfolding is_empty_def by transfer simp 
   8.564 -
   8.565 -lemma is_empty_update [simp]:
   8.566 -  "\<not> is_empty (update k v m)"
   8.567 +lemma is_empty_empty [simp]: "is_empty empty"
   8.568    unfolding is_empty_def by transfer simp
   8.569  
   8.570 -lemma is_empty_delete:
   8.571 -  "is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}"
   8.572 +lemma is_empty_update [simp]: "\<not> is_empty (update k v m)"
   8.573 +  unfolding is_empty_def by transfer simp
   8.574 +
   8.575 +lemma is_empty_delete: "is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}"
   8.576    unfolding is_empty_def by transfer (auto simp del: dom_eq_empty_conv)
   8.577  
   8.578 -lemma is_empty_replace [simp]:
   8.579 -  "is_empty (replace k v m) \<longleftrightarrow> is_empty m"
   8.580 +lemma is_empty_replace [simp]: "is_empty (replace k v m) \<longleftrightarrow> is_empty m"
   8.581    unfolding is_empty_def replace_def by transfer auto
   8.582  
   8.583 -lemma is_empty_default [simp]:
   8.584 -  "\<not> is_empty (default k v m)"
   8.585 +lemma is_empty_default [simp]: "\<not> is_empty (default k v m)"
   8.586    unfolding is_empty_def default_def by transfer auto
   8.587  
   8.588 -lemma is_empty_map_entry [simp]:
   8.589 -  "is_empty (map_entry k f m) \<longleftrightarrow> is_empty m"
   8.590 +lemma is_empty_map_entry [simp]: "is_empty (map_entry k f m) \<longleftrightarrow> is_empty m"
   8.591    unfolding is_empty_def by transfer (auto split: option.split)
   8.592  
   8.593 -lemma is_empty_map_values [simp]:
   8.594 -  "is_empty (map_values f m) \<longleftrightarrow> is_empty m"
   8.595 +lemma is_empty_map_values [simp]: "is_empty (map_values f m) \<longleftrightarrow> is_empty m"
   8.596    unfolding is_empty_def by transfer (auto simp: fun_eq_iff)
   8.597  
   8.598 -lemma is_empty_map_default [simp]:
   8.599 -  "\<not> is_empty (map_default k v f m)"
   8.600 +lemma is_empty_map_default [simp]: "\<not> is_empty (map_default k v f m)"
   8.601    by (simp add: map_default_def)
   8.602  
   8.603 -lemma keys_dom_lookup:
   8.604 -  "keys m = dom (Mapping.lookup m)"
   8.605 +lemma keys_dom_lookup: "keys m = dom (Mapping.lookup m)"
   8.606    by transfer rule
   8.607  
   8.608 -lemma keys_empty [simp]:
   8.609 -  "keys empty = {}"
   8.610 +lemma keys_empty [simp]: "keys empty = {}"
   8.611    by transfer simp
   8.612  
   8.613 -lemma keys_update [simp]:
   8.614 -  "keys (update k v m) = insert k (keys m)"
   8.615 +lemma keys_update [simp]: "keys (update k v m) = insert k (keys m)"
   8.616    by transfer simp
   8.617  
   8.618 -lemma keys_delete [simp]:
   8.619 -  "keys (delete k m) = keys m - {k}"
   8.620 +lemma keys_delete [simp]: "keys (delete k m) = keys m - {k}"
   8.621    by transfer simp
   8.622  
   8.623 -lemma keys_replace [simp]:
   8.624 -  "keys (replace k v m) = keys m"
   8.625 +lemma keys_replace [simp]: "keys (replace k v m) = keys m"
   8.626    unfolding replace_def by transfer (simp add: insert_absorb)
   8.627  
   8.628 -lemma keys_default [simp]:
   8.629 -  "keys (default k v m) = insert k (keys m)"
   8.630 +lemma keys_default [simp]: "keys (default k v m) = insert k (keys m)"
   8.631    unfolding default_def by transfer (simp add: insert_absorb)
   8.632  
   8.633 -lemma keys_map_entry [simp]:
   8.634 -  "keys (map_entry k f m) = keys m"
   8.635 +lemma keys_map_entry [simp]: "keys (map_entry k f m) = keys m"
   8.636    by transfer (auto split: option.split)
   8.637  
   8.638 -lemma keys_map_default [simp]:
   8.639 -  "keys (map_default k v f m) = insert k (keys m)"
   8.640 +lemma keys_map_default [simp]: "keys (map_default k v f m) = insert k (keys m)"
   8.641    by (simp add: map_default_def)
   8.642  
   8.643 -lemma keys_map_values [simp]:
   8.644 -  "keys (map_values f m) = keys m"
   8.645 +lemma keys_map_values [simp]: "keys (map_values f m) = keys m"
   8.646    by transfer (simp_all add: dom_def)
   8.647  
   8.648 -lemma keys_combine_with_key [simp]: 
   8.649 +lemma keys_combine_with_key [simp]:
   8.650    "Mapping.keys (combine_with_key f m1 m2) = Mapping.keys m1 \<union> Mapping.keys m2"
   8.651 -  by transfer (auto simp: dom_def combine_options_def split: option.splits)  
   8.652 +  by transfer (auto simp: dom_def combine_options_def split: option.splits)
   8.653  
   8.654  lemma keys_combine [simp]: "Mapping.keys (combine f m1 m2) = Mapping.keys m1 \<union> Mapping.keys m2"
   8.655    by (simp add: combine_altdef)
   8.656  
   8.657 -lemma keys_tabulate [simp]:
   8.658 -  "keys (tabulate ks f) = set ks"
   8.659 +lemma keys_tabulate [simp]: "keys (tabulate ks f) = set ks"
   8.660    by transfer (simp add: map_of_map_restrict o_def)
   8.661  
   8.662  lemma keys_of_alist [simp]: "keys (of_alist xs) = set (List.map fst xs)"
   8.663    by transfer (simp_all add: dom_map_of_conv_image_fst)
   8.664  
   8.665 -lemma keys_bulkload [simp]:
   8.666 -  "keys (bulkload xs) = {0..<length xs}"
   8.667 +lemma keys_bulkload [simp]: "keys (bulkload xs) = {0..<length xs}"
   8.668    by (simp add: bulkload_tabulate)
   8.669  
   8.670 -lemma distinct_ordered_keys [simp]:
   8.671 -  "distinct (ordered_keys m)"
   8.672 +lemma distinct_ordered_keys [simp]: "distinct (ordered_keys m)"
   8.673    by (simp add: ordered_keys_def)
   8.674  
   8.675 -lemma ordered_keys_infinite [simp]:
   8.676 -  "\<not> finite (keys m) \<Longrightarrow> ordered_keys m = []"
   8.677 +lemma ordered_keys_infinite [simp]: "\<not> finite (keys m) \<Longrightarrow> ordered_keys m = []"
   8.678    by (simp add: ordered_keys_def)
   8.679  
   8.680 -lemma ordered_keys_empty [simp]:
   8.681 -  "ordered_keys empty = []"
   8.682 +lemma ordered_keys_empty [simp]: "ordered_keys empty = []"
   8.683    by (simp add: ordered_keys_def)
   8.684  
   8.685  lemma ordered_keys_update [simp]:
   8.686    "k \<in> keys m \<Longrightarrow> ordered_keys (update k v m) = ordered_keys m"
   8.687 -  "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (update k v m) = insort k (ordered_keys m)"
   8.688 -  by (simp_all add: ordered_keys_def) (auto simp only: sorted_list_of_set_insert [symmetric] insert_absorb)
   8.689 +  "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow>
   8.690 +    ordered_keys (update k v m) = insort k (ordered_keys m)"
   8.691 +  by (simp_all add: ordered_keys_def)
   8.692 +    (auto simp only: sorted_list_of_set_insert [symmetric] insert_absorb)
   8.693  
   8.694 -lemma ordered_keys_delete [simp]:
   8.695 -  "ordered_keys (delete k m) = remove1 k (ordered_keys m)"
   8.696 +lemma ordered_keys_delete [simp]: "ordered_keys (delete k m) = remove1 k (ordered_keys m)"
   8.697  proof (cases "finite (keys m)")
   8.698 -  case False then show ?thesis by simp
   8.699 +  case False
   8.700 +  then show ?thesis by simp
   8.701  next
   8.702 -  case True note fin = True
   8.703 +  case fin: True
   8.704    show ?thesis
   8.705    proof (cases "k \<in> keys m")
   8.706 -    case False with fin have "k \<notin> set (sorted_list_of_set (keys m))" by simp
   8.707 -    with False show ?thesis by (simp add: ordered_keys_def remove1_idem)
   8.708 +    case False
   8.709 +    with fin have "k \<notin> set (sorted_list_of_set (keys m))"
   8.710 +      by simp
   8.711 +    with False show ?thesis
   8.712 +      by (simp add: ordered_keys_def remove1_idem)
   8.713    next
   8.714 -    case True with fin show ?thesis by (simp add: ordered_keys_def sorted_list_of_set_remove)
   8.715 +    case True
   8.716 +    with fin show ?thesis
   8.717 +      by (simp add: ordered_keys_def sorted_list_of_set_remove)
   8.718    qed
   8.719  qed
   8.720  
   8.721 -lemma ordered_keys_replace [simp]:
   8.722 -  "ordered_keys (replace k v m) = ordered_keys m"
   8.723 +lemma ordered_keys_replace [simp]: "ordered_keys (replace k v m) = ordered_keys m"
   8.724    by (simp add: replace_def)
   8.725  
   8.726  lemma ordered_keys_default [simp]:
   8.727 @@ -578,8 +548,7 @@
   8.728    "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (default k v m) = insort k (ordered_keys m)"
   8.729    by (simp_all add: default_def)
   8.730  
   8.731 -lemma ordered_keys_map_entry [simp]:
   8.732 -  "ordered_keys (map_entry k f m) = ordered_keys m"
   8.733 +lemma ordered_keys_map_entry [simp]: "ordered_keys (map_entry k f m) = ordered_keys m"
   8.734    by (simp add: ordered_keys_def)
   8.735  
   8.736  lemma ordered_keys_map_default [simp]:
   8.737 @@ -587,16 +556,13 @@
   8.738    "finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = insort k (ordered_keys m)"
   8.739    by (simp_all add: map_default_def)
   8.740  
   8.741 -lemma ordered_keys_tabulate [simp]:
   8.742 -  "ordered_keys (tabulate ks f) = sort (remdups ks)"
   8.743 +lemma ordered_keys_tabulate [simp]: "ordered_keys (tabulate ks f) = sort (remdups ks)"
   8.744    by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups)
   8.745  
   8.746 -lemma ordered_keys_bulkload [simp]:
   8.747 -  "ordered_keys (bulkload ks) = [0..<length ks]"
   8.748 +lemma ordered_keys_bulkload [simp]: "ordered_keys (bulkload ks) = [0..<length ks]"
   8.749    by (simp add: ordered_keys_def)
   8.750  
   8.751 -lemma tabulate_fold:
   8.752 -  "tabulate xs f = fold (\<lambda>k m. update k (f k) m) xs empty"
   8.753 +lemma tabulate_fold: "tabulate xs f = fold (\<lambda>k m. update k (f k) m) xs empty"
   8.754  proof transfer
   8.755    fix f :: "'a \<Rightarrow> 'b" and xs
   8.756    have "map_of (List.map (\<lambda>k. (k, f k)) xs) = foldr (\<lambda>k m. m(k \<mapsto> f k)) xs Map.empty"
   8.757 @@ -613,21 +579,23 @@
   8.758  
   8.759  lemma All_mapping_empty [simp]: "All_mapping Mapping.empty P"
   8.760    by (auto simp: All_mapping_def lookup_empty)
   8.761 -  
   8.762 -lemma All_mapping_update_iff: 
   8.763 +
   8.764 +lemma All_mapping_update_iff:
   8.765    "All_mapping (Mapping.update k v m) P \<longleftrightarrow> P k v \<and> All_mapping m (\<lambda>k' v'. k = k' \<or> P k' v')"
   8.766 -  unfolding All_mapping_def 
   8.767 +  unfolding All_mapping_def
   8.768  proof safe
   8.769    assume "\<forall>x. case Mapping.lookup (Mapping.update k v m) x of None \<Rightarrow> True | Some y \<Rightarrow> P x y"
   8.770 -  hence A: "case Mapping.lookup (Mapping.update k v m) x of None \<Rightarrow> True | Some y \<Rightarrow> P x y" for x
   8.771 +  then have *: "case Mapping.lookup (Mapping.update k v m) x of None \<Rightarrow> True | Some y \<Rightarrow> P x y" for x
   8.772      by blast
   8.773 -  from A[of k] show "P k v" by (simp add: lookup_update)
   8.774 +  from *[of k] show "P k v"
   8.775 +    by (simp add: lookup_update)
   8.776    show "case Mapping.lookup m x of None \<Rightarrow> True | Some v' \<Rightarrow> k = x \<or> P x v'" for x
   8.777 -    using A[of x] by (auto simp add: lookup_update' split: if_splits option.splits)
   8.778 +    using *[of x] by (auto simp add: lookup_update' split: if_splits option.splits)
   8.779  next
   8.780    assume "P k v"
   8.781    assume "\<forall>x. case Mapping.lookup m x of None \<Rightarrow> True | Some v' \<Rightarrow> k = x \<or> P x v'"
   8.782 -  hence A: "case Mapping.lookup m x of None \<Rightarrow> True | Some v' \<Rightarrow> k = x \<or> P x v'" for x by blast
   8.783 +  then have A: "case Mapping.lookup m x of None \<Rightarrow> True | Some v' \<Rightarrow> k = x \<or> P x v'" for x
   8.784 +    by blast
   8.785    show "case Mapping.lookup (Mapping.update k v m) x of None \<Rightarrow> True | Some xa \<Rightarrow> P x xa" for x
   8.786      using \<open>P k v\<close> A[of x] by (auto simp: lookup_update' split: option.splits)
   8.787  qed
   8.788 @@ -636,31 +604,28 @@
   8.789    "P k v \<Longrightarrow> All_mapping m (\<lambda>k' v'. k = k' \<or> P k' v') \<Longrightarrow> All_mapping (Mapping.update k v m) P"
   8.790    by (simp add: All_mapping_update_iff)
   8.791  
   8.792 -lemma All_mapping_filter_iff:
   8.793 -  "All_mapping (filter P m) Q \<longleftrightarrow> All_mapping m (\<lambda>k v. P k v \<longrightarrow> Q k v)"
   8.794 +lemma All_mapping_filter_iff: "All_mapping (filter P m) Q \<longleftrightarrow> All_mapping m (\<lambda>k v. P k v \<longrightarrow> Q k v)"
   8.795    by (auto simp: All_mapping_def lookup_filter split: option.splits)
   8.796  
   8.797 -lemma All_mapping_filter:
   8.798 -  "All_mapping m Q \<Longrightarrow> All_mapping (filter P m) Q"
   8.799 +lemma All_mapping_filter: "All_mapping m Q \<Longrightarrow> All_mapping (filter P m) Q"
   8.800    by (auto simp: All_mapping_filter_iff intro: All_mapping_mono)
   8.801  
   8.802 -lemma All_mapping_map_values:
   8.803 -  "All_mapping (map_values f m) P \<longleftrightarrow> All_mapping m (\<lambda>k v. P k (f k v))"
   8.804 +lemma All_mapping_map_values: "All_mapping (map_values f m) P \<longleftrightarrow> All_mapping m (\<lambda>k v. P k (f k v))"
   8.805    by (auto simp: All_mapping_def lookup_map_values split: option.splits)
   8.806  
   8.807 -lemma All_mapping_tabulate: 
   8.808 -  "(\<forall>x\<in>set xs. P x (f x)) \<Longrightarrow> All_mapping (Mapping.tabulate xs f) P"
   8.809 -  unfolding All_mapping_def 
   8.810 -  by (intro allI,  transfer) (auto split: option.split dest!: map_of_SomeD)
   8.811 +lemma All_mapping_tabulate: "(\<forall>x\<in>set xs. P x (f x)) \<Longrightarrow> All_mapping (Mapping.tabulate xs f) P"
   8.812 +  unfolding All_mapping_def
   8.813 +  apply (intro allI)
   8.814 +  apply transfer
   8.815 +  apply (auto split: option.split dest!: map_of_SomeD)
   8.816 +  done
   8.817  
   8.818  lemma All_mapping_alist:
   8.819    "(\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v) \<Longrightarrow> All_mapping (Mapping.of_alist xs) P"
   8.820    by (auto simp: All_mapping_def lookup_of_alist dest!: map_of_SomeD split: option.splits)
   8.821  
   8.822 -
   8.823 -lemma combine_empty [simp]:
   8.824 -  "combine f Mapping.empty y = y" "combine f y Mapping.empty = y"
   8.825 -  by (transfer, force)+
   8.826 +lemma combine_empty [simp]: "combine f Mapping.empty y = y" "combine f y Mapping.empty = y"
   8.827 +  by (transfer; force)+
   8.828  
   8.829  lemma (in abel_semigroup) comm_monoid_set_combine: "comm_monoid_set (combine f) Mapping.empty"
   8.830    by standard (transfer fixing: f, simp add: combine_options_ac[of f] ac_simps)+
   8.831 @@ -679,19 +644,16 @@
   8.832      using that by (induction xs) simp_all
   8.833    from this[of "remdups xs"] show ?thesis by simp
   8.834  qed
   8.835 -  
   8.836 -lemma keys_fold_combine:
   8.837 -  assumes "finite A"
   8.838 -  shows   "Mapping.keys (combine.F g A) = (\<Union>x\<in>A. Mapping.keys (g x))"
   8.839 -  using assms by (induction A rule: finite_induct) simp_all
   8.840 +
   8.841 +lemma keys_fold_combine: "finite A \<Longrightarrow> Mapping.keys (combine.F g A) = (\<Union>x\<in>A. Mapping.keys (g x))"
   8.842 +  by (induct A rule: finite_induct) simp_all
   8.843  
   8.844  end
   8.845  
   8.846 -  
   8.847 +
   8.848  subsection \<open>Code generator setup\<close>
   8.849  
   8.850  hide_const (open) empty is_empty rep lookup lookup_default filter update delete ordered_keys
   8.851    keys size replace default map_entry map_default tabulate bulkload map map_values combine of_alist
   8.852  
   8.853  end
   8.854 -