src/HOL/Bali/Table.thy
author schirmer
Mon Jan 28 17:00:19 2002 +0100 (2002-01-28)
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
permissions -rw-r--r--
Isabelle/Bali sources;
     1 (*  Title:      isabelle/Bali/Table.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   1997 Technische Universitaet Muenchen
     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 
    35 types ('a, 'b) table    (* table with key type 'a and contents type 'b *)
    36       = "'a \<leadsto> 'b"
    37       ('a, 'b) tables   (* non-unique table with key 'a and contents 'b *)
    38       = "'a \<Rightarrow> 'b set"
    39 
    40 
    41 section "map of / table of"
    42 
    43 syntax
    44   table_of      :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"    (* concrete table *)
    45 
    46 translations
    47   "table_of" == "map_of"
    48   
    49   (type)"'a \<leadsto> 'b"       <= (type)"'a \<Rightarrow> 'b Option.option"
    50   (type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
    51 
    52 (* ### To map *)
    53 lemma override_find_left[simp]:
    54 "n k = None \<Longrightarrow> (m ++ n) k = m k"
    55 by (simp add: override_def)
    56 
    57 section {* Conditional Override *}
    58 constdefs
    59 cond_override:: 
    60   "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table"
    61 
    62 (* when merging tables old and new, only override an entry of table old when  
    63    the condition cond holds *)
    64 "cond_override cond old new \<equiv>
    65  \<lambda> k.
    66   (case new k of
    67      None         \<Rightarrow> old k                       
    68    | Some new_val \<Rightarrow> (case old k of
    69                         None         \<Rightarrow> Some new_val          
    70                       | Some old_val \<Rightarrow> (if cond new_val old_val
    71                                          then Some new_val     
    72                                          else Some old_val)))"
    73 
    74 lemma cond_override_empty1[simp]: "cond_override c empty t = t"
    75 by (simp add: cond_override_def expand_fun_eq)
    76 
    77 lemma cond_override_empty2[simp]: "cond_override c t empty = t"
    78 by (simp add: cond_override_def expand_fun_eq)
    79 
    80 lemma cond_override_None[simp]:
    81  "old k = None \<Longrightarrow> (cond_override c old new) k = new k"
    82 by (simp add: cond_override_def)
    83 
    84 lemma cond_override_override:
    85  "\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 
    86   \<Longrightarrow> (cond_override C old new) k = Some nv"
    87 by (auto simp add: cond_override_def)
    88 
    89 lemma cond_override_noOverride:
    90  "\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 
    91   \<Longrightarrow> (cond_override C old new) k = Some ov"
    92 by (auto simp add: cond_override_def)
    93 
    94 lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t"
    95 by (auto simp add: cond_override_def dom_def)
    96 
    97 lemma finite_dom_cond_override:
    98  "\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))"
    99 apply (rule_tac B="dom s \<union> dom t" in finite_subset)
   100 apply (rule dom_cond_override)
   101 by (rule finite_UnI)
   102 
   103 section {* Filter on Tables *}
   104 
   105 constdefs
   106 filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
   107 "filter_tab c t \<equiv> \<lambda> k. (case t k of 
   108                            None   \<Rightarrow> None
   109                          | Some x \<Rightarrow> if c k x then Some x else None)"
   110 
   111 lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
   112 by (simp add: filter_tab_def empty_def)
   113 
   114 lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"
   115 by (simp add: expand_fun_eq filter_tab_def)
   116 
   117 lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
   118 by (simp add: expand_fun_eq filter_tab_def empty_def)
   119 
   120 lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"
   121 by (auto simp add: filter_tab_def ran_def)
   122 
   123 lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}"
   124 apply (auto simp add: filter_tab_def)
   125 apply (drule sym, blast)
   126 done
   127 
   128 lemma finite_range_filter_tab:
   129   "finite (range t) \<Longrightarrow> finite (range (filter_tab c t))"
   130 apply (rule_tac B="range t \<union> {None} " in finite_subset)
   131 apply (rule filter_tab_range_subset)
   132 apply (auto intro: finite_UnI)
   133 done
   134 
   135 lemma filter_tab_SomeD[dest!]: 
   136 "filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x"
   137 by (auto simp add: filter_tab_def)
   138 
   139 lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x"
   140 by (simp add: filter_tab_def)
   141 
   142 lemma filter_tab_all_True: 
   143  "\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t"
   144 apply (auto simp add: filter_tab_def expand_fun_eq)
   145 done
   146 
   147 lemma filter_tab_all_True_Some:
   148  "\<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"
   149 by (auto simp add: filter_tab_def expand_fun_eq)
   150 
   151 lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
   152 apply (simp add: filter_tab_def expand_fun_eq)
   153 done
   154 
   155 lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t"
   156 by (auto simp add: filter_tab_def dom_def)
   157 
   158 lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b"
   159 by (auto simp add: expand_fun_eq filter_tab_def)
   160 
   161 lemma finite_dom_filter_tab:
   162 "finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))"
   163 apply (rule_tac B="dom t" in finite_subset)
   164 by (rule filter_tab_dom_subset)
   165 
   166 
   167 lemma filter_tab_weaken:
   168 "\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 
   169   \<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y
   170  \<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
   171 apply (auto simp add: filter_tab_def)
   172 done
   173 
   174 lemma cond_override_filter: 
   175   "\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 
   176     \<Longrightarrow> (\<not> overC new old \<longrightarrow>  \<not> filterC k new) \<and> 
   177         (overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new)
   178    \<rbrakk> \<Longrightarrow>
   179     cond_override overC (filter_tab filterC t) (filter_tab filterC s) 
   180     = filter_tab filterC (cond_override overC t s)"
   181 by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )
   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 make_imp)
   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> o2s (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 apply safe
   207 apply (fast dest!: weak_map_of_SomeI)
   208 apply auto
   209 done
   210 
   211 lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
   212 apply (rule injI)
   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 only: map_of_override [THEN sym])
   278 apply (rule override_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