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