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