src/HOL/Bali/Table.thy
author kuncar
Fri Dec 09 18:07:04 2011 +0100 (2011-12-09)
changeset 45802 b16f976db515
parent 45605 a89b4bc311a5
child 46212 d86ef6b96097
permissions -rw-r--r--
Quotient_Info stores only relation maps
     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 type_synonym ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
    33       = "'a \<rightharpoonup> 'b"
    34 type_synonym ('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 =
    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 fun_eq_iff)
    69 
    70 lemma cond_override_empty2[simp]: "cond_override c t empty = t"
    71 by (simp add: cond_override_def fun_eq_iff)
    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
    99   filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
   100   "filter_tab c t = (\<lambda>k. (case t k of 
   101                            None   \<Rightarrow> None
   102                          | Some x \<Rightarrow> if c k x then Some x else None))"
   103 
   104 lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
   105 by (simp add: filter_tab_def empty_def)
   106 
   107 lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"
   108 by (simp add: fun_eq_iff filter_tab_def)
   109 
   110 lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
   111 by (simp add: fun_eq_iff filter_tab_def empty_def)
   112 
   113 lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"
   114 by (auto simp add: filter_tab_def ran_def)
   115 
   116 lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}"
   117 apply (auto simp add: filter_tab_def)
   118 apply (drule sym, blast)
   119 done
   120 
   121 lemma finite_range_filter_tab:
   122   "finite (range t) \<Longrightarrow> finite (range (filter_tab c t))"
   123 apply (rule_tac B="range t \<union> {None} " in finite_subset)
   124 apply (rule filter_tab_range_subset)
   125 apply (auto intro: finite_UnI)
   126 done
   127 
   128 lemma filter_tab_SomeD[dest!]: 
   129 "filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x"
   130 by (auto simp add: filter_tab_def)
   131 
   132 lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x"
   133 by (simp add: filter_tab_def)
   134 
   135 lemma filter_tab_all_True: 
   136  "\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t"
   137 apply (auto simp add: filter_tab_def fun_eq_iff)
   138 done
   139 
   140 lemma filter_tab_all_True_Some:
   141  "\<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"
   142 by (auto simp add: filter_tab_def fun_eq_iff)
   143 
   144 lemma filter_tab_all_False: 
   145  "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
   146 by (auto simp add: filter_tab_def fun_eq_iff)
   147 
   148 lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
   149 apply (simp add: filter_tab_def fun_eq_iff)
   150 done
   151 
   152 lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t"
   153 by (auto simp add: filter_tab_def dom_def)
   154 
   155 lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b"
   156 by (auto simp add: fun_eq_iff filter_tab_def)
   157 
   158 lemma finite_dom_filter_tab:
   159 "finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))"
   160 apply (rule_tac B="dom t" in finite_subset)
   161 by (rule filter_tab_dom_subset)
   162 
   163 
   164 lemma filter_tab_weaken:
   165 "\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 
   166   \<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y
   167  \<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
   168 apply (force simp add: filter_tab_def)
   169 done
   170 
   171 lemma cond_override_filter: 
   172   "\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 
   173     \<Longrightarrow> (\<not> overC new old \<longrightarrow>  \<not> filterC k new) \<and> 
   174         (overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new)
   175    \<rbrakk> \<Longrightarrow>
   176     cond_override overC (filter_tab filterC t) (filter_tab filterC s) 
   177     = filter_tab filterC (cond_override overC t s)"
   178 by (auto simp add: fun_eq_iff cond_override_def filter_tab_def )
   179 
   180 
   181 section {* Misc. *}
   182 
   183 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"
   184 apply (erule rev_mp)
   185 apply (induct l)
   186 apply simp
   187 apply (simp (no_asm))
   188 apply auto
   189 done
   190 
   191 lemma Ball_set_tableD: 
   192   "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> Option.set (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
   193 apply (frule Ball_set_table)
   194 by auto
   195 
   196 declare map_of_SomeD [elim]
   197 
   198 lemma table_of_Some_in_set:
   199 "table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l"
   200 by auto
   201 
   202 lemma set_get_eq: 
   203   "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
   204 by (auto dest!: weak_map_of_SomeI)
   205 
   206 lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
   207 apply (rule inj_onI)
   208 apply auto
   209 done
   210 
   211 lemma table_of_mapconst_SomeI:
   212   "\<lbrakk>table_of t k = Some y'; snd y=y'; fst y=c\<rbrakk> \<Longrightarrow>
   213    table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y"
   214 apply (induct t)
   215 apply auto
   216 done
   217 
   218 lemma table_of_mapconst_NoneI:
   219   "\<lbrakk>table_of t k = None\<rbrakk> \<Longrightarrow>
   220    table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None"
   221 apply (induct t)
   222 apply auto
   223 done
   224 
   225 lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI]
   226 
   227 lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow>
   228    table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"
   229 apply (induct_tac "t")
   230 apply auto
   231 done
   232 
   233 lemma table_of_remap_SomeD [rule_format (no_asm)]: 
   234   "table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<longrightarrow>
   235   table_of t (k, k') = Some x"
   236 apply (induct_tac "t")
   237 apply  auto
   238 done
   239 
   240 lemma table_of_mapf_Some [rule_format (no_asm)]: "\<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow> 
   241   table_of (map (\<lambda>(k,x). (k,f x)) t) k = Some (f x) \<longrightarrow> table_of t k = Some x"
   242 apply (induct_tac "t")
   243 apply  auto
   244 done
   245 
   246 lemma table_of_mapf_SomeD [rule_format (no_asm), dest!]: 
   247 "table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<longrightarrow> (\<exists>y\<in>table_of t k: z=f y)"
   248 apply (induct_tac "t")
   249 apply  auto
   250 done
   251 
   252 lemma table_of_mapf_NoneD [rule_format (no_asm), dest!]: 
   253 "table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<longrightarrow> (table_of t k = None)"
   254 apply (induct_tac "t")
   255 apply auto
   256 done
   257 
   258 lemma table_of_mapkey_SomeD [rule_format (no_asm), dest!]: 
   259   "table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<longrightarrow> C = D \<and> table_of t k = Some x"
   260 apply (induct_tac "t")
   261 apply  auto
   262 done
   263 lemma table_of_mapkey_SomeD2 [rule_format (no_asm), dest!]: 
   264   "table_of (map (\<lambda>(k,x). ((k,C),x)) t) ek = Some x 
   265    \<longrightarrow> C = snd ek \<and> table_of t (fst ek) = Some x"
   266 apply (induct_tac "t")
   267 apply  auto
   268 done
   269 
   270 lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 
   271  (table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"
   272 apply (simp)
   273 apply (rule map_add_Some_iff)
   274 done
   275 
   276 lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:
   277   "table_of (filter P xs) k = Some z \<Longrightarrow> unique xs \<longrightarrow> table_of xs k = Some z"
   278 apply (induct xs)
   279 apply (auto del: map_of_SomeD intro!: map_of_SomeD)
   280 done
   281 
   282 
   283 definition
   284   Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
   285   where "Un_tables ts\<spacespace>\<spacespace>= (\<lambda>k. \<Union>t\<in>ts. t k)"
   286 
   287 definition
   288   overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables"  (infixl "\<oplus>\<oplus>" 100)
   289   where "s \<oplus>\<oplus> t = (\<lambda>k. if t k = {} then s k else t k)"
   290 
   291 definition
   292   hidings_entails :: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
   293     ("_ hidings _ entails _" 20)
   294   where "(t hidings s entails R) = (\<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y)"
   295 
   296 definition
   297   --{* variant for unique table: *}
   298   hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
   299     ("_ hiding _ entails _"  20)
   300   where "(t hiding  s entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y)"
   301 
   302 definition
   303   --{* variant for a unique table and conditional overriding: *}
   304   cond_hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  
   305                           \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"  
   306                           ("_ hiding _ under _ entails _"  20)
   307   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)"
   308 
   309 section "Untables"
   310 
   311 lemma Un_tablesI [intro]:  "\<And>x. \<lbrakk>t \<in> ts; x \<in> t k\<rbrakk> \<Longrightarrow> x \<in> Un_tables ts k"
   312 apply (simp add: Un_tables_def)
   313 apply auto
   314 done
   315 
   316 lemma Un_tablesD [dest!]: "\<And>x. x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k"
   317 apply (simp add: Un_tables_def)
   318 apply auto
   319 done
   320 
   321 lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})"
   322 apply (unfold Un_tables_def)
   323 apply (simp (no_asm))
   324 done
   325 
   326 
   327 section "overrides"
   328 
   329 lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m"
   330 apply (unfold overrides_t_def)
   331 apply (simp (no_asm))
   332 done
   333 lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m"
   334 apply (unfold overrides_t_def)
   335 apply (simp (no_asm))
   336 done
   337 
   338 lemma overrides_t_Some_iff: 
   339  "(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)"
   340 by (simp add: overrides_t_def)
   341 
   342 lemmas overrides_t_SomeD = overrides_t_Some_iff [THEN iffD1, dest!]
   343 
   344 lemma overrides_t_right_empty [simp]: "n k = {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = m k"  
   345 by (simp add: overrides_t_def)
   346 
   347 lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k"  
   348 by (simp add: overrides_t_def)
   349 
   350 section "hiding entails"
   351 
   352 lemma hiding_entailsD: 
   353   "\<lbrakk>t hiding s entails R; t k = Some x; s k = Some y\<rbrakk> \<Longrightarrow> R x y"
   354 by (simp add: hiding_entails_def)
   355 
   356 lemma empty_hiding_entails: "empty hiding s entails R"
   357 by (simp add: hiding_entails_def)
   358 
   359 lemma hiding_empty_entails: "t hiding empty entails R"
   360 by (simp add: hiding_entails_def)
   361 declare empty_hiding_entails [simp] hiding_empty_entails [simp]
   362 
   363 section "cond hiding entails"
   364 
   365 lemma cond_hiding_entailsD: 
   366 "\<lbrakk>t hiding s under C entails R; t k = Some x; s k = Some y; C x y\<rbrakk> \<Longrightarrow> R x y"
   367 by (simp add: cond_hiding_entails_def)
   368 
   369 lemma empty_cond_hiding_entails[simp]: "empty hiding s under C entails R"
   370 by (simp add: cond_hiding_entails_def)
   371 
   372 lemma cond_hiding_empty_entails[simp]: "t hiding empty under C entails R"
   373 by (simp add: cond_hiding_entails_def)
   374 
   375 lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"
   376 by (simp add: hidings_entails_def)
   377 
   378 lemma hidings_empty_entails: "t hidings (\<lambda>k. {}) entails R"
   379 apply (unfold hidings_entails_def)
   380 apply (simp (no_asm))
   381 done
   382 
   383 lemma empty_hidings_entails: 
   384   "(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def)
   385 by (simp (no_asm))
   386 declare empty_hidings_entails [intro!] hidings_empty_entails [intro!]
   387 
   388 
   389 
   390 (*###TO Map?*)
   391 primrec atleast_free :: "('a ~=> 'b) => nat => bool"
   392 where
   393   "atleast_free m 0 = True"
   394 | atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>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