12857

1 
(* Title: HOL/Bali/Table.thy

12854

2 
ID: $Id$


3 
Author: David von Oheimb


4 
Copyright 1997 Technische Universitaet Muenchen


5 
*)


6 
header {* Abstract tables and their implementation as lists *}


7 


8 
theory Table = Basis:


9 


10 
text {*


11 
design issues:


12 
\begin{itemize}


13 
\item definition of table: infinite map vs. list vs. finite set


14 
list chosen, because:


15 
\begin{itemize}


16 
\item[+] a priori finite


17 
\item[+] lookup is more operational than for finite set


18 
\item[] not very abstract, but function table converts it to abstract


19 
mapping


20 
\end{itemize}


21 
\item coding of lookup result: Some/None vs. value/arbitrary


22 
Some/None chosen, because:


23 
\begin{itemize}


24 
\item[++] makes definedness check possible (applies also to finite set),


25 
which is important for the type standard, hiding/overriding, etc.


26 
(though it may perhaps be possible at least for the operational semantics


27 
to treat programs as infinite, i.e. where classes, fields, methods etc.


28 
of any name are considered to be defined)


29 
\item[] sometimes awkward case distinctions, alleviated by operator 'the'


30 
\end{itemize}


31 
\end{itemize}


32 
*}


33 


34 


35 
types ('a, 'b) table (* table with key type 'a and contents type 'b *)


36 
= "'a \<leadsto> 'b"


37 
('a, 'b) tables (* nonunique table with key 'a and contents 'b *)


38 
= "'a \<Rightarrow> 'b set"


39 


40 


41 
section "map of / table of"


42 


43 
syntax


44 
table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" (* concrete table *)


45 


46 
translations


47 
"table_of" == "map_of"


48 


49 
(type)"'a \<leadsto> 'b" <= (type)"'a \<Rightarrow> 'b Option.option"


50 
(type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"


51 


52 
(* ### To map *)


53 
lemma override_find_left[simp]:


54 
"n k = None \<Longrightarrow> (m ++ n) k = m k"


55 
by (simp add: override_def)


56 


57 
section {* Conditional Override *}


58 
constdefs


59 
cond_override::


60 
"('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table"


61 


62 
(* when merging tables old and new, only override an entry of table old when


63 
the condition cond holds *)


64 
"cond_override cond old new \<equiv>


65 
\<lambda> k.


66 
(case new k of


67 
None \<Rightarrow> old k


68 
 Some new_val \<Rightarrow> (case old k of


69 
None \<Rightarrow> Some new_val


70 
 Some old_val \<Rightarrow> (if cond new_val old_val


71 
then Some new_val


72 
else Some old_val)))"


73 


74 
lemma cond_override_empty1[simp]: "cond_override c empty t = t"


75 
by (simp add: cond_override_def expand_fun_eq)


76 


77 
lemma cond_override_empty2[simp]: "cond_override c t empty = t"


78 
by (simp add: cond_override_def expand_fun_eq)


79 


80 
lemma cond_override_None[simp]:


81 
"old k = None \<Longrightarrow> (cond_override c old new) k = new k"


82 
by (simp add: cond_override_def)


83 


84 
lemma cond_override_override:


85 
"\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk>


86 
\<Longrightarrow> (cond_override C old new) k = Some nv"


87 
by (auto simp add: cond_override_def)


88 


89 
lemma cond_override_noOverride:


90 
"\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk>


91 
\<Longrightarrow> (cond_override C old new) k = Some ov"


92 
by (auto simp add: cond_override_def)


93 


94 
lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t"


95 
by (auto simp add: cond_override_def dom_def)


96 


97 
lemma finite_dom_cond_override:


98 
"\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))"


99 
apply (rule_tac B="dom s \<union> dom t" in finite_subset)


100 
apply (rule dom_cond_override)


101 
by (rule finite_UnI)


102 


103 
section {* Filter on Tables *}


104 


105 
constdefs


106 
filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"


107 
"filter_tab c t \<equiv> \<lambda> k. (case t k of


108 
None \<Rightarrow> None


109 
 Some x \<Rightarrow> if c k x then Some x else None)"


110 


111 
lemma filter_tab_empty[simp]: "filter_tab c empty = empty"


112 
by (simp add: filter_tab_def empty_def)


113 


114 
lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"


115 
by (simp add: expand_fun_eq filter_tab_def)


116 


117 
lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"


118 
by (simp add: expand_fun_eq filter_tab_def empty_def)


119 


120 
lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"


121 
by (auto simp add: filter_tab_def ran_def)


122 


123 
lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}"


124 
apply (auto simp add: filter_tab_def)


125 
apply (drule sym, blast)


126 
done


127 


128 
lemma finite_range_filter_tab:


129 
"finite (range t) \<Longrightarrow> finite (range (filter_tab c t))"


130 
apply (rule_tac B="range t \<union> {None} " in finite_subset)


131 
apply (rule filter_tab_range_subset)


132 
apply (auto intro: finite_UnI)


133 
done


134 


135 
lemma filter_tab_SomeD[dest!]:


136 
"filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x"


137 
by (auto simp add: filter_tab_def)


138 


139 
lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x"


140 
by (simp add: filter_tab_def)


141 


142 
lemma filter_tab_all_True:


143 
"\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t"


144 
apply (auto simp add: filter_tab_def expand_fun_eq)


145 
done


146 


147 
lemma filter_tab_all_True_Some:


148 
"\<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"


149 
by (auto simp add: filter_tab_def expand_fun_eq)


150 


151 
lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"


152 
apply (simp add: filter_tab_def expand_fun_eq)


153 
done


154 


155 
lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t"


156 
by (auto simp add: filter_tab_def dom_def)


157 


158 
lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b"


159 
by (auto simp add: expand_fun_eq filter_tab_def)


160 


161 
lemma finite_dom_filter_tab:


162 
"finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))"


163 
apply (rule_tac B="dom t" in finite_subset)


164 
by (rule filter_tab_dom_subset)


165 


166 


167 
lemma filter_tab_weaken:


168 
"\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b;


169 
\<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y


170 
\<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"


171 
apply (auto simp add: filter_tab_def)


172 
done


173 


174 
lemma cond_override_filter:


175 
"\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk>


176 
\<Longrightarrow> (\<not> overC new old \<longrightarrow> \<not> filterC k new) \<and>


177 
(overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new)


178 
\<rbrakk> \<Longrightarrow>


179 
cond_override overC (filter_tab filterC t) (filter_tab filterC s)


180 
= filter_tab filterC (cond_override overC t s)"


181 
by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )


182 


183 
section {* Misc. *}


184 


185 
lemma 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"


186 
apply (erule make_imp)


187 
apply (induct l)


188 
apply simp


189 
apply (simp (no_asm))


190 
apply auto


191 
done


192 


193 
lemma Ball_set_tableD:


194 
"\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> o2s (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"


195 
apply (frule Ball_set_table)


196 
by auto


197 


198 
declare map_of_SomeD [elim]


199 


200 
lemma table_of_Some_in_set:


201 
"table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l"


202 
by auto


203 


204 
lemma set_get_eq:


205 
"unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"


206 
apply safe


207 
apply (fast dest!: weak_map_of_SomeI)


208 
apply auto


209 
done


210 


211 
lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"


212 
apply (rule injI)


213 
apply auto


214 
done


215 


216 
lemma table_of_mapconst_SomeI:


217 
"\<lbrakk>table_of t k = Some y'; snd y=y'; fst y=c\<rbrakk> \<Longrightarrow>


218 
table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y"


219 
apply (induct t)


220 
apply auto


221 
done


222 


223 
lemma table_of_mapconst_NoneI:


224 
"\<lbrakk>table_of t k = None\<rbrakk> \<Longrightarrow>


225 
table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None"


226 
apply (induct t)


227 
apply auto


228 
done


229 


230 
lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard]


231 


232 
lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow>


233 
table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"


234 
apply (induct_tac "t")


235 
apply auto


236 
done


237 


238 
lemma table_of_remap_SomeD [rule_format (no_asm)]:


239 
"table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<longrightarrow>


240 
table_of t (k, k') = Some x"


241 
apply (induct_tac "t")


242 
apply auto


243 
done


244 


245 
lemma table_of_mapf_Some [rule_format (no_asm)]: "\<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow>


246 
table_of (map (\<lambda>(k,x). (k,f x)) t) k = Some (f x) \<longrightarrow> table_of t k = Some x"


247 
apply (induct_tac "t")


248 
apply auto


249 
done


250 


251 
lemma table_of_mapf_SomeD [rule_format (no_asm), dest!]:


252 
"table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<longrightarrow> (\<exists>y\<in>table_of t k: z=f y)"


253 
apply (induct_tac "t")


254 
apply auto


255 
done


256 


257 
lemma table_of_mapf_NoneD [rule_format (no_asm), dest!]:


258 
"table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<longrightarrow> (table_of t k = None)"


259 
apply (induct_tac "t")


260 
apply auto


261 
done


262 


263 
lemma table_of_mapkey_SomeD [rule_format (no_asm), dest!]:


264 
"table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<longrightarrow> C = D \<and> table_of t k = Some x"


265 
apply (induct_tac "t")


266 
apply auto


267 
done


268 
lemma table_of_mapkey_SomeD2 [rule_format (no_asm), dest!]:


269 
"table_of (map (\<lambda>(k,x). ((k,C),x)) t) ek = Some x


270 
\<longrightarrow> C = snd ek \<and> table_of t (fst ek) = Some x"


271 
apply (induct_tac "t")


272 
apply auto


273 
done


274 


275 
lemma table_append_Some_iff: "table_of (xs@ys) k = Some z =


276 
(table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"


277 
apply (simp only: map_of_override [THEN sym])


278 
apply (rule override_Some_iff)


279 
done


280 


281 
lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:


282 
"table_of (filter P xs) k = Some z \<Longrightarrow> unique xs \<longrightarrow> table_of xs k = Some z"


283 
apply (induct xs)


284 
apply (auto del: map_of_SomeD intro!: map_of_SomeD)


285 
done


286 


287 


288 
consts


289 
Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"


290 
overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow>


291 
('a, 'b) tables" (infixl "\<oplus>\<oplus>" 100)


292 
hidings_entails:: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow>


293 
('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" ("_ hidings _ entails _" 20)


294 
(* variant for unique table: *)


295 
hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table \<Rightarrow>


296 
('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" ("_ hiding _ entails _" 20)


297 
(* variant for a unique table and conditional overriding: *)


298 
cond_hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table


299 
\<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"


300 
("_ hiding _ under _ entails _" 20)


301 


302 
defs


303 
Un_tables_def: "Un_tables ts\<spacespace>\<spacespace>\<equiv> \<lambda>k. \<Union>t\<in>ts. t k"


304 
overrides_t_def: "s \<oplus>\<oplus> t \<equiv> \<lambda>k. if t k = {} then s k else t k"


305 
hidings_entails_def: "t hidings s entails R \<equiv> \<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y"


306 
hiding_entails_def: "t hiding s entails R \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y"


307 
cond_hiding_entails_def: "t hiding s under C entails R


308 
\<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y"


309 


310 
section "Untables"


311 


312 
lemma Un_tablesI [intro]: "\<And>x. \<lbrakk>t \<in> ts; x \<in> t k\<rbrakk> \<Longrightarrow> x \<in> Un_tables ts k"


313 
apply (simp add: Un_tables_def)


314 
apply auto


315 
done


316 


317 
lemma Un_tablesD [dest!]: "\<And>x. x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k"


318 
apply (simp add: Un_tables_def)


319 
apply auto


320 
done


321 


322 
lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})"


323 
apply (unfold Un_tables_def)


324 
apply (simp (no_asm))


325 
done


326 


327 


328 
section "overrides"


329 


330 
lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m"


331 
apply (unfold overrides_t_def)


332 
apply (simp (no_asm))


333 
done


334 
lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m"


335 
apply (unfold overrides_t_def)


336 
apply (simp (no_asm))


337 
done


338 


339 
lemma overrides_t_Some_iff:


340 
"(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)"


341 
by (simp add: overrides_t_def)


342 


343 
lemmas overrides_t_SomeD = overrides_t_Some_iff [THEN iffD1, dest!]


344 


345 
lemma overrides_t_right_empty [simp]: "n k = {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = m k"


346 
by (simp add: overrides_t_def)


347 


348 
lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k"


349 
by (simp add: overrides_t_def)


350 


351 
section "hiding entails"


352 


353 
lemma hiding_entailsD:


354 
"\<lbrakk>t hiding s entails R; t k = Some x; s k = Some y\<rbrakk> \<Longrightarrow> R x y"


355 
by (simp add: hiding_entails_def)


356 


357 
lemma empty_hiding_entails: "empty hiding s entails R"


358 
by (simp add: hiding_entails_def)


359 


360 
lemma hiding_empty_entails: "t hiding empty entails R"


361 
by (simp add: hiding_entails_def)


362 
declare empty_hiding_entails [simp] hiding_empty_entails [simp]


363 


364 
section "cond hiding entails"


365 


366 
lemma cond_hiding_entailsD:


367 
"\<lbrakk>t hiding s under C entails R; t k = Some x; s k = Some y; C x y\<rbrakk> \<Longrightarrow> R x y"


368 
by (simp add: cond_hiding_entails_def)


369 


370 
lemma empty_cond_hiding_entails[simp]: "empty hiding s under C entails R"


371 
by (simp add: cond_hiding_entails_def)


372 


373 
lemma cond_hiding_empty_entails[simp]: "t hiding empty under C entails R"


374 
by (simp add: cond_hiding_entails_def)


375 


376 
lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"


377 
by (simp add: hidings_entails_def)


378 


379 
lemma hidings_empty_entails: "t hidings (\<lambda>k. {}) entails R"


380 
apply (unfold hidings_entails_def)


381 
apply (simp (no_asm))


382 
done


383 


384 
lemma empty_hidings_entails:


385 
"(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def)


386 
by (simp (no_asm))


387 
declare empty_hidings_entails [intro!] hidings_empty_entails [intro!]


388 


389 


390 


391 
(*###TO Map?*)


392 
consts


393 
atleast_free :: "('a ~=> 'b) => nat => bool"


394 
primrec


395 
"atleast_free m 0 = True"


396 
atleast_free_Suc:


397 
"atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a>b)) n))"


398 


399 
lemma atleast_free_weaken [rule_format (no_asm)]:


400 
"!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n"


401 
apply (induct_tac "n")


402 
apply (simp (no_asm))


403 
apply clarify


404 
apply (simp (no_asm))


405 
apply (drule atleast_free_Suc [THEN iffD1])


406 
apply fast


407 
done


408 


409 
lemma atleast_free_SucI:


410 
"[ h a = None; !obj. atleast_free (h(a>obj)) n ] ==> atleast_free h (Suc n)"


411 
by force


412 


413 
declare fun_upd_apply [simp del]


414 
lemma atleast_free_SucD_lemma [rule_format (no_asm)]:


415 
" !m a. m a = None > (!c. atleast_free (m(a>c)) n) >


416 
(!b d. a ~= b > atleast_free (m(b>d)) n)"


417 
apply (induct_tac "n")


418 
apply auto


419 
apply (rule_tac x = "a" in exI)


420 
apply (rule conjI)


421 
apply (force simp add: fun_upd_apply)


422 
apply (erule_tac V = "m a = None" in thin_rl)


423 
apply clarify


424 
apply (subst fun_upd_twist)


425 
apply (erule not_sym)


426 
apply (rename_tac "ba")


427 
apply (drule_tac x = "ba" in spec)


428 
apply clarify


429 
apply (tactic "smp_tac 2 1")


430 
apply (erule (1) notE impE)


431 
apply (case_tac "aa = b")


432 
apply fast+


433 
done


434 
declare fun_upd_apply [simp]


435 


436 
lemma atleast_free_SucD [rule_format (no_asm)]: "atleast_free h (Suc n) ==> atleast_free (h(a>b)) n"


437 
apply auto


438 
apply (case_tac "aa = a")


439 
apply auto


440 
apply (erule atleast_free_SucD_lemma)


441 
apply auto


442 
done


443 


444 
declare atleast_free_Suc [simp del]


445 
end
