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