src/HOL/Bali/Table.thy
author berghofe
Sat Jan 30 17:03:46 2010 +0100 (2010-01-30)
changeset 34990 81e8fdfeb849
parent 34939 44294cfecb1d
child 35355 613e133966ea
child 35416 d8d7d1b785af
permissions -rw-r--r--
Adapted to changes in cases method.
     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 syntax
    41   table_of      :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"   --{* concrete table *}
    42   
    43 abbreviation
    44   "table_of \<equiv> map_of"
    45 
    46 translations
    47   (type)"'a \<rightharpoonup> 'b"       <= (type)"'a \<Rightarrow> 'b Datatype.option"
    48   (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b"
    49 
    50 (* ### To map *)
    51 lemma map_add_find_left[simp]:
    52 "n k = None \<Longrightarrow> (m ++ n) k = m k"
    53 by (simp add: map_add_def)
    54 
    55 section {* Conditional Override *}
    56 constdefs
    57 cond_override:: 
    58   "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table"
    59 
    60 --{* when merging tables old and new, only override an entry of table old when  
    61    the condition cond holds *}
    62 "cond_override cond old new \<equiv>
    63  \<lambda> k.
    64   (case new k of
    65      None         \<Rightarrow> old k                       
    66    | Some new_val \<Rightarrow> (case old k of
    67                         None         \<Rightarrow> Some new_val          
    68                       | Some old_val \<Rightarrow> (if cond new_val old_val
    69                                          then Some new_val     
    70                                          else Some old_val)))"
    71 
    72 lemma cond_override_empty1[simp]: "cond_override c empty t = t"
    73 by (simp add: cond_override_def expand_fun_eq)
    74 
    75 lemma cond_override_empty2[simp]: "cond_override c t empty = t"
    76 by (simp add: cond_override_def expand_fun_eq)
    77 
    78 lemma cond_override_None[simp]:
    79  "old k = None \<Longrightarrow> (cond_override c old new) k = new k"
    80 by (simp add: cond_override_def)
    81 
    82 lemma cond_override_override:
    83  "\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 
    84   \<Longrightarrow> (cond_override C old new) k = Some nv"
    85 by (auto simp add: cond_override_def)
    86 
    87 lemma cond_override_noOverride:
    88  "\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 
    89   \<Longrightarrow> (cond_override C old new) k = Some ov"
    90 by (auto simp add: cond_override_def)
    91 
    92 lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t"
    93 by (auto simp add: cond_override_def dom_def)
    94 
    95 lemma finite_dom_cond_override:
    96  "\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))"
    97 apply (rule_tac B="dom s \<union> dom t" in finite_subset)
    98 apply (rule dom_cond_override)
    99 by (rule finite_UnI)
   100 
   101 section {* Filter on Tables *}
   102 
   103 constdefs
   104 filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
   105 "filter_tab c t \<equiv> \<lambda> k. (case t k of 
   106                            None   \<Rightarrow> None
   107                          | Some x \<Rightarrow> if c k x then Some x else None)"
   108 
   109 lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
   110 by (simp add: filter_tab_def empty_def)
   111 
   112 lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"
   113 by (simp add: expand_fun_eq filter_tab_def)
   114 
   115 lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
   116 by (simp add: expand_fun_eq filter_tab_def empty_def)
   117 
   118 lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"
   119 by (auto simp add: filter_tab_def ran_def)
   120 
   121 lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}"
   122 apply (auto simp add: filter_tab_def)
   123 apply (drule sym, blast)
   124 done
   125 
   126 lemma finite_range_filter_tab:
   127   "finite (range t) \<Longrightarrow> finite (range (filter_tab c t))"
   128 apply (rule_tac B="range t \<union> {None} " in finite_subset)
   129 apply (rule filter_tab_range_subset)
   130 apply (auto intro: finite_UnI)
   131 done
   132 
   133 lemma filter_tab_SomeD[dest!]: 
   134 "filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x"
   135 by (auto simp add: filter_tab_def)
   136 
   137 lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x"
   138 by (simp add: filter_tab_def)
   139 
   140 lemma filter_tab_all_True: 
   141  "\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t"
   142 apply (auto simp add: filter_tab_def expand_fun_eq)
   143 done
   144 
   145 lemma filter_tab_all_True_Some:
   146  "\<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"
   147 by (auto simp add: filter_tab_def expand_fun_eq)
   148 
   149 lemma filter_tab_all_False: 
   150  "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
   151 by (auto simp add: filter_tab_def expand_fun_eq)
   152 
   153 lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
   154 apply (simp add: filter_tab_def expand_fun_eq)
   155 done
   156 
   157 lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t"
   158 by (auto simp add: filter_tab_def dom_def)
   159 
   160 lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b"
   161 by (auto simp add: expand_fun_eq filter_tab_def)
   162 
   163 lemma finite_dom_filter_tab:
   164 "finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))"
   165 apply (rule_tac B="dom t" in finite_subset)
   166 by (rule filter_tab_dom_subset)
   167 
   168 
   169 lemma filter_tab_weaken:
   170 "\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 
   171   \<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y
   172  \<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
   173 apply (force simp add: filter_tab_def)
   174 done
   175 
   176 lemma cond_override_filter: 
   177   "\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 
   178     \<Longrightarrow> (\<not> overC new old \<longrightarrow>  \<not> filterC k new) \<and> 
   179         (overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new)
   180    \<rbrakk> \<Longrightarrow>
   181     cond_override overC (filter_tab filterC t) (filter_tab filterC s) 
   182     = filter_tab filterC (cond_override overC t s)"
   183 by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )
   184 
   185 
   186 section {* Misc. *}
   187 
   188 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"
   189 apply (erule rev_mp)
   190 apply (induct l)
   191 apply simp
   192 apply (simp (no_asm))
   193 apply auto
   194 done
   195 
   196 lemma Ball_set_tableD: 
   197   "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> Option.set (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
   198 apply (frule Ball_set_table)
   199 by auto
   200 
   201 declare map_of_SomeD [elim]
   202 
   203 lemma table_of_Some_in_set:
   204 "table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l"
   205 by auto
   206 
   207 lemma set_get_eq: 
   208   "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
   209 by (auto dest!: weak_map_of_SomeI)
   210 
   211 lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
   212 apply (rule inj_onI)
   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)
   278 apply (rule map_add_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