1(* Title: HOL/Bali/Table.thy 2 Author: David von Oheimb 3*) 4subsection \<open>Abstract tables and their implementation as lists\<close> 5 6theory Table imports Basis begin 7 8text \<open> 9design issues: 10\begin{itemize} 11\item definition of table: infinite map vs. list vs. finite set 12 list chosen, because: 13 \begin{itemize} 14 \item[+] a priori finite 15 \item[+] lookup is more operational than for finite set 16 \item[-] not very abstract, but function table converts it to abstract 17 mapping 18 \end{itemize} 19\item coding of lookup result: Some/None vs. value/arbitrary 20 Some/None chosen, because: 21 \begin{itemize} 22 \item[++] makes definedness check possible (applies also to finite set), 23 which is important for the type standard, hiding/overriding, etc. 24 (though it may perhaps be possible at least for the operational semantics 25 to treat programs as infinite, i.e. where classes, fields, methods etc. 26 of any name are considered to be defined) 27 \item[-] sometimes awkward case distinctions, alleviated by operator 'the' 28 \end{itemize} 29\end{itemize} 30\<close> 31 32type_synonym ('a, 'b) table \<comment> \<open>table with key type 'a and contents type 'b\<close> 33 = "'a \<rightharpoonup> 'b" 34type_synonym ('a, 'b) tables \<comment> \<open>non-unique table with key 'a and contents 'b\<close> 35 = "'a \<Rightarrow> 'b set" 36 37 38subsubsection "map of / table of" 39 40abbreviation 41 table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" \<comment> \<open>concrete table\<close> 42 where "table_of \<equiv> map_of" 43 44translations 45 (type) "('a, 'b) table" <= (type) "'a \<rightharpoonup> 'b" 46 47(* ### To map *) 48lemma map_add_find_left[simp]: "n k = None \<Longrightarrow> (m ++ n) k = m k" 49 by (simp add: map_add_def) 50 51 52subsubsection \<open>Conditional Override\<close> 53 54definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where 55 56\<comment> \<open>when merging tables old and new, only override an entry of table old when 57 the condition cond holds\<close> 58"cond_override cond old new = 59 (\<lambda>k. 60 (case new k of 61 None \<Rightarrow> old k 62 | Some new_val \<Rightarrow> (case old k of 63 None \<Rightarrow> Some new_val 64 | Some old_val \<Rightarrow> (if cond new_val old_val 65 then Some new_val 66 else Some old_val))))" 67 68lemma cond_override_empty1[simp]: "cond_override c Map.empty t = t" 69 by (simp add: cond_override_def fun_eq_iff) 70 71lemma cond_override_empty2[simp]: "cond_override c t Map.empty = t" 72 by (simp add: cond_override_def fun_eq_iff) 73 74lemma cond_override_None[simp]: 75 "old k = None \<Longrightarrow> (cond_override c old new) k = new k" 76 by (simp add: cond_override_def) 77 78lemma cond_override_override: 79 "\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 80 \<Longrightarrow> (cond_override C old new) k = Some nv" 81 by (auto simp add: cond_override_def) 82 83lemma cond_override_noOverride: 84 "\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 85 \<Longrightarrow> (cond_override C old new) k = Some ov" 86 by (auto simp add: cond_override_def) 87 88lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t" 89 by (auto simp add: cond_override_def dom_def) 90 91lemma finite_dom_cond_override: 92 "\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))" 93apply (rule_tac B="dom s \<union> dom t" in finite_subset) 94apply (rule dom_cond_override) 95by (rule finite_UnI) 96 97 98subsubsection \<open>Filter on Tables\<close> 99 100definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" 101 where 102 "filter_tab c t = (\<lambda>k. (case t k of 103 None \<Rightarrow> None 104 | Some x \<Rightarrow> if c k x then Some x else None))" 105 106lemma filter_tab_empty[simp]: "filter_tab c Map.empty = Map.empty" 107by (simp add: filter_tab_def empty_def) 108 109lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t" 110by (simp add: fun_eq_iff filter_tab_def) 111 112lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = Map.empty" 113by (simp add: fun_eq_iff filter_tab_def empty_def) 114 115lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t" 116by (auto simp add: filter_tab_def ran_def) 117 118lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}" 119apply (auto simp add: filter_tab_def) 120apply (drule sym, blast) 121done 122 123lemma finite_range_filter_tab: 124 "finite (range t) \<Longrightarrow> finite (range (filter_tab c t))" 125apply (rule_tac B="range t \<union> {None} " in finite_subset) 126apply (rule filter_tab_range_subset) 127apply (auto intro: finite_UnI) 128done 129 130lemma filter_tab_SomeD[dest!]: 131"filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x" 132by (auto simp add: filter_tab_def) 133 134lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x" 135by (simp add: filter_tab_def) 136 137lemma filter_tab_all_True: 138 "\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t" 139apply (auto simp add: filter_tab_def fun_eq_iff) 140done 141 142lemma filter_tab_all_True_Some: 143 "\<lbrakk>\<forall> k y. t k = Some y \<longrightarrow> p k y; t k = Some v\<rbrakk> \<Longrightarrow> filter_tab p t k = Some v" 144by (auto simp add: filter_tab_def fun_eq_iff) 145 146lemma filter_tab_all_False: 147 "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = Map.empty" 148by (auto simp add: filter_tab_def fun_eq_iff) 149 150lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None" 151apply (simp add: filter_tab_def fun_eq_iff) 152done 153 154lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t" 155by (auto simp add: filter_tab_def dom_def) 156 157lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b" 158by (auto simp add: fun_eq_iff filter_tab_def) 159 160lemma finite_dom_filter_tab: 161"finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))" 162apply (rule_tac B="dom t" in finite_subset) 163by (rule filter_tab_dom_subset) 164 165 166lemma filter_tab_weaken: 167"\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 168 \<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y 169 \<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b" 170by (force simp add: filter_tab_def) 171 172lemma cond_override_filter: 173 "\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 174 \<Longrightarrow> (\<not> overC new old \<longrightarrow> \<not> filterC k new) \<and> 175 (overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new) 176 \<rbrakk> \<Longrightarrow> 177 cond_override overC (filter_tab filterC t) (filter_tab filterC s) 178 = filter_tab filterC (cond_override overC t s)" 179by (auto simp add: fun_eq_iff cond_override_def filter_tab_def ) 180 181 182subsubsection \<open>Misc\<close> 183 184lemma Ball_set_table: "(\<forall> (x,y)\<in> set l. P x y) \<Longrightarrow> \<forall> x. \<forall> y\<in> map_of l x: P x y" 185apply (erule rev_mp) 186apply (induct l) 187apply simp 188apply (simp (no_asm)) 189apply auto 190done 191 192lemma Ball_set_tableD: 193 "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> set_option (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x" 194apply (frule Ball_set_table) 195by auto 196 197declare map_of_SomeD [elim] 198 199lemma table_of_Some_in_set: 200"table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l" 201by auto 202 203lemma set_get_eq: 204 "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)" 205by (auto dest!: weak_map_of_SomeI) 206 207lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))" 208apply (rule inj_onI) 209apply auto 210done 211 212lemma table_of_mapconst_SomeI: 213 "\<lbrakk>table_of t k = Some y'; snd y=y'; fst y=c\<rbrakk> \<Longrightarrow> 214 table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y" 215 by (induct t) auto 216 217lemma table_of_mapconst_NoneI: 218 "\<lbrakk>table_of t k = None\<rbrakk> \<Longrightarrow> 219 table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None" 220 by (induct t) auto 221 222lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI] 223 224lemma table_of_map_SomeI: "table_of t k = Some x \<Longrightarrow> 225 table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)" 226 by (induct t) auto 227 228lemma table_of_remap_SomeD: 229 "table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<Longrightarrow> 230 table_of t (k, k') = Some x" 231 by (induct t) auto 232 233lemma table_of_mapf_Some: 234 "\<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow> 235 table_of (map (\<lambda>(k,x). (k,f x)) t) k = Some (f x) \<Longrightarrow> table_of t k = Some x" 236 by (induct t) auto 237 238lemma table_of_mapf_SomeD [dest!]: 239 "table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<Longrightarrow> (\<exists>y\<in>table_of t k: z=f y)" 240 by (induct t) auto 241 242lemma table_of_mapf_NoneD [dest!]: 243 "table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<Longrightarrow> (table_of t k = None)" 244 by (induct t) auto 245 246lemma table_of_mapkey_SomeD [dest!]: 247 "table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<Longrightarrow> C = D \<and> table_of t k = Some x" 248 by (induct t) auto 249 250lemma table_of_mapkey_SomeD2 [dest!]: 251 "table_of (map (\<lambda>(k,x). ((k,C),x)) t) ek = Some x \<Longrightarrow> 252 C = snd ek \<and> table_of t (fst ek) = Some x" 253 by (induct t) auto 254 255lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 256 (table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))" 257apply (simp) 258apply (rule map_add_Some_iff) 259done 260 261lemma table_of_filter_unique_SomeD [rule_format (no_asm)]: 262 "table_of (filter P xs) k = Some z \<Longrightarrow> unique xs \<longrightarrow> table_of xs k = Some z" 263 by (induct xs) (auto del: map_of_SomeD intro!: map_of_SomeD) 264 265 266definition Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables" 267 where "Un_tables ts = (\<lambda>k. \<Union>t\<in>ts. t k)" 268 269definition overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables" 270 (infixl "\<oplus>\<oplus>" 100) 271 where "s \<oplus>\<oplus> t = (\<lambda>k. if t k = {} then s k else t k)" 272 273definition 274 hidings_entails :: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" 275 ("_ hidings _ entails _" 20) 276 where "(t hidings s entails R) = (\<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y)" 277 278definition 279 \<comment> \<open>variant for unique table:\<close> 280 hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" 281 ("_ hiding _ entails _" 20) 282 where "(t hiding s entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y)" 283 284definition 285 \<comment> \<open>variant for a unique table and conditional overriding:\<close> 286 cond_hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table 287 \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" 288 ("_ hiding _ under _ entails _" 20) 289 where "(t hiding s under C entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y)" 290 291 292subsubsection "Untables" 293 294lemma Un_tablesI [intro]: "t \<in> ts \<Longrightarrow> x \<in> t k \<Longrightarrow> x \<in> Un_tables ts k" 295 by (auto simp add: Un_tables_def) 296 297lemma Un_tablesD [dest!]: "x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k" 298 by (auto simp add: Un_tables_def) 299 300lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})" 301 by (simp add: Un_tables_def) 302 303 304subsubsection "overrides" 305 306lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m" 307 by (simp add: overrides_t_def) 308 309lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m" 310 by (simp add: overrides_t_def) 311 312lemma overrides_t_Some_iff: 313 "(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)" 314 by (simp add: overrides_t_def) 315 316lemmas overrides_t_SomeD = overrides_t_Some_iff [THEN iffD1, dest!] 317 318lemma overrides_t_right_empty [simp]: "n k = {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = m k" 319 by (simp add: overrides_t_def) 320 321lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k" 322 by (simp add: overrides_t_def) 323 324 325subsubsection "hiding entails" 326 327lemma hiding_entailsD: 328 "t hiding s entails R \<Longrightarrow> t k = Some x \<Longrightarrow> s k = Some y \<Longrightarrow> R x y" 329 by (simp add: hiding_entails_def) 330 331lemma empty_hiding_entails [simp]: "Map.empty hiding s entails R" 332 by (simp add: hiding_entails_def) 333 334lemma hiding_empty_entails [simp]: "t hiding Map.empty entails R" 335 by (simp add: hiding_entails_def) 336 337 338subsubsection "cond hiding entails" 339 340lemma cond_hiding_entailsD: 341"\<lbrakk>t hiding s under C entails R; t k = Some x; s k = Some y; C x y\<rbrakk> \<Longrightarrow> R x y" 342by (simp add: cond_hiding_entails_def) 343 344lemma empty_cond_hiding_entails[simp]: "Map.empty hiding s under C entails R" 345by (simp add: cond_hiding_entails_def) 346 347lemma cond_hiding_empty_entails[simp]: "t hiding Map.empty under C entails R" 348by (simp add: cond_hiding_entails_def) 349 350lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y" 351by (simp add: hidings_entails_def) 352 353lemma hidings_empty_entails [intro!]: "t hidings (\<lambda>k. {}) entails R" 354apply (unfold hidings_entails_def) 355apply (simp (no_asm)) 356done 357 358lemma empty_hidings_entails [intro!]: 359 "(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def) 360by (simp (no_asm)) 361 362 363(*###TO Map?*) 364primrec atleast_free :: "('a \<rightharpoonup> 'b) => nat => bool" 365where 366 "atleast_free m 0 = True" 367| atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None \<and> (\<forall>b. atleast_free (m(a\<mapsto>b)) n))" 368 369lemma atleast_free_weaken [rule_format (no_asm)]: 370 "\<forall>m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n" 371apply (induct_tac "n") 372apply (simp (no_asm)) 373apply clarify 374apply (simp (no_asm)) 375apply (drule atleast_free_Suc [THEN iffD1]) 376apply fast 377done 378 379lemma atleast_free_SucI: 380"[| h a = None; \<forall>obj. atleast_free (h(a|->obj)) n |] ==> atleast_free h (Suc n)" 381by force 382 383declare fun_upd_apply [simp del] 384lemma atleast_free_SucD_lemma [rule_format (no_asm)]: 385"\<forall>m a. m a = None \<longrightarrow> (\<forall>c. atleast_free (m(a\<mapsto>c)) n) \<longrightarrow> 386 (\<forall>b d. a \<noteq> b \<longrightarrow> atleast_free (m(b\<mapsto>d)) n)" 387apply (induct_tac "n") 388apply auto 389apply (rule_tac x = "a" in exI) 390apply (rule conjI) 391apply (force simp add: fun_upd_apply) 392apply (erule_tac V = "m a = None" in thin_rl) 393apply clarify 394apply (subst fun_upd_twist) 395apply (erule not_sym) 396apply (rename_tac "ba") 397apply (drule_tac x = "ba" in spec) 398apply clarify 399apply (tactic "smp_tac \<^context> 2 1") 400apply (erule (1) notE impE) 401apply (case_tac "aa = b") 402apply fast+ 403done 404declare fun_upd_apply [simp] 405 406lemma atleast_free_SucD: "atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n" 407apply auto 408apply (case_tac "aa = a") 409apply auto 410apply (erule atleast_free_SucD_lemma) 411apply auto 412done 413 414declare atleast_free_Suc [simp del] 415 416end 417