src/HOL/Bali/Table.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62042 6c6ccf573479
child 67443 3abf6a722518
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 (*  Title:      HOL/Bali/Table.thy
     2     Author:     David von Oheimb
     3 *)
     4 subsection \<open>Abstract tables and their implementation as lists\<close>
     5 
     6 theory Table imports Basis begin
     7 
     8 text \<open>
     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 \<close>
    31 
    32 type_synonym ('a, 'b) table    \<comment>\<open>table with key type 'a and contents type 'b\<close>
    33       = "'a \<rightharpoonup> 'b"
    34 type_synonym ('a, 'b) tables   \<comment>\<open>non-unique table with key 'a and contents 'b\<close>
    35       = "'a \<Rightarrow> 'b set"
    36 
    37 
    38 subsubsection "map of / table of"
    39 
    40 abbreviation
    41   table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"   \<comment>\<open>concrete table\<close>
    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]: "n k = None \<Longrightarrow> (m ++ n) k = m k"
    49   by (simp add: map_add_def)
    50 
    51 
    52 subsubsection \<open>Conditional Override\<close>
    53 
    54 definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where
    55 
    56 \<comment>\<open>when merging tables old and new, only override an entry of table old when  
    57    the condition cond holds\<close>
    58 "cond_override cond old new =
    59  (\<lambda>k.
    60   (case new k of
    61      None         \<Rightarrow> old k                       
    62    | Some new_val \<Rightarrow> (case old k of
    63                         None         \<Rightarrow> Some new_val          
    64                       | Some old_val \<Rightarrow> (if cond new_val old_val
    65                                          then Some new_val     
    66                                          else Some old_val))))"
    67 
    68 lemma cond_override_empty1[simp]: "cond_override c empty t = t"
    69   by (simp add: cond_override_def fun_eq_iff)
    70 
    71 lemma cond_override_empty2[simp]: "cond_override c t empty = t"
    72   by (simp add: cond_override_def fun_eq_iff)
    73 
    74 lemma cond_override_None[simp]:
    75   "old k = None \<Longrightarrow> (cond_override c old new) k = new k"
    76   by (simp add: cond_override_def)
    77 
    78 lemma cond_override_override:
    79   "\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 
    80     \<Longrightarrow> (cond_override C old new) k = Some nv"
    81   by (auto simp add: cond_override_def)
    82 
    83 lemma cond_override_noOverride:
    84   "\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 
    85     \<Longrightarrow> (cond_override C old new) k = Some ov"
    86   by (auto simp add: cond_override_def)
    87 
    88 lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t"
    89   by (auto simp add: cond_override_def dom_def)
    90 
    91 lemma finite_dom_cond_override:
    92  "\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))"
    93 apply (rule_tac B="dom s \<union> dom t" in finite_subset)
    94 apply (rule dom_cond_override)
    95 by (rule finite_UnI)
    96 
    97 
    98 subsubsection \<open>Filter on Tables\<close>
    99 
   100 definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
   101   where
   102     "filter_tab c t = (\<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: fun_eq_iff filter_tab_def)
   111 
   112 lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
   113 by (simp add: fun_eq_iff 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 fun_eq_iff)
   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 fun_eq_iff)
   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 fun_eq_iff)
   149 
   150 lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
   151 apply (simp add: filter_tab_def fun_eq_iff)
   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: fun_eq_iff 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 by (force simp add: filter_tab_def)
   171 
   172 lemma cond_override_filter: 
   173   "\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 
   174     \<Longrightarrow> (\<not> overC new old \<longrightarrow>  \<not> filterC k new) \<and> 
   175         (overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new)
   176    \<rbrakk> \<Longrightarrow>
   177     cond_override overC (filter_tab filterC t) (filter_tab filterC s) 
   178     = filter_tab filterC (cond_override overC t s)"
   179 by (auto simp add: fun_eq_iff cond_override_def filter_tab_def )
   180 
   181 
   182 subsubsection \<open>Misc\<close>
   183 
   184 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"
   185 apply (erule rev_mp)
   186 apply (induct l)
   187 apply simp
   188 apply (simp (no_asm))
   189 apply auto
   190 done
   191 
   192 lemma Ball_set_tableD: 
   193   "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> set_option (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
   194 apply (frule Ball_set_table)
   195 by auto
   196 
   197 declare map_of_SomeD [elim]
   198 
   199 lemma table_of_Some_in_set:
   200 "table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l"
   201 by auto
   202 
   203 lemma set_get_eq: 
   204   "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
   205 by (auto dest!: weak_map_of_SomeI)
   206 
   207 lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
   208 apply (rule inj_onI)
   209 apply auto
   210 done
   211 
   212 lemma table_of_mapconst_SomeI:
   213   "\<lbrakk>table_of t k = Some y'; snd y=y'; fst y=c\<rbrakk> \<Longrightarrow>
   214     table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y"
   215   by (induct t) auto
   216 
   217 lemma table_of_mapconst_NoneI:
   218   "\<lbrakk>table_of t k = None\<rbrakk> \<Longrightarrow>
   219     table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None"
   220   by (induct t) auto
   221 
   222 lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI]
   223 
   224 lemma table_of_map_SomeI: "table_of t k = Some x \<Longrightarrow>
   225    table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"
   226   by (induct t) auto
   227 
   228 lemma table_of_remap_SomeD:
   229   "table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<Longrightarrow>
   230     table_of t (k, k') = Some x"
   231   by (induct t) auto
   232 
   233 lemma table_of_mapf_Some:
   234   "\<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow>
   235     table_of (map (\<lambda>(k,x). (k,f x)) t) k = Some (f x) \<Longrightarrow> table_of t k = Some x"
   236   by (induct t) auto
   237 
   238 lemma table_of_mapf_SomeD [dest!]:
   239   "table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<Longrightarrow> (\<exists>y\<in>table_of t k: z=f y)"
   240   by (induct t) auto
   241 
   242 lemma table_of_mapf_NoneD [dest!]:
   243   "table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<Longrightarrow> (table_of t k = None)"
   244   by (induct t) auto
   245 
   246 lemma table_of_mapkey_SomeD [dest!]:
   247   "table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<Longrightarrow> C = D \<and> table_of t k = Some x"
   248   by (induct t) auto
   249 
   250 lemma table_of_mapkey_SomeD2 [dest!]:
   251   "table_of (map (\<lambda>(k,x). ((k,C),x)) t) ek = Some x \<Longrightarrow>
   252     C = snd ek \<and> table_of t (fst ek) = Some x"
   253   by (induct t) auto
   254 
   255 lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 
   256  (table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"
   257 apply (simp)
   258 apply (rule map_add_Some_iff)
   259 done
   260 
   261 lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:
   262   "table_of (filter P xs) k = Some z \<Longrightarrow> unique xs \<longrightarrow> table_of xs k = Some z"
   263   by (induct xs) (auto del: map_of_SomeD intro!: map_of_SomeD)
   264 
   265 
   266 definition Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
   267   where "Un_tables ts = (\<lambda>k. \<Union>t\<in>ts. t k)"
   268 
   269 definition overrides_t :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow> ('a, 'b) tables"
   270     (infixl "\<oplus>\<oplus>" 100)
   271   where "s \<oplus>\<oplus> t = (\<lambda>k. if t k = {} then s k else t k)"
   272 
   273 definition
   274   hidings_entails :: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
   275     ("_ hidings _ entails _" 20)
   276   where "(t hidings s entails R) = (\<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y)"
   277 
   278 definition
   279   \<comment>\<open>variant for unique table:\<close>
   280   hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"
   281     ("_ hiding _ entails _"  20)
   282   where "(t hiding  s entails R) = (\<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y)"
   283 
   284 definition
   285   \<comment>\<open>variant for a unique table and conditional overriding:\<close>
   286   cond_hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  
   287                           \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"  
   288                           ("_ hiding _ under _ entails _"  20)
   289   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)"
   290 
   291 
   292 subsubsection "Untables"
   293 
   294 lemma Un_tablesI [intro]:  "t \<in> ts \<Longrightarrow> x \<in> t k \<Longrightarrow> x \<in> Un_tables ts k"
   295   by (auto simp add: Un_tables_def)
   296 
   297 lemma Un_tablesD [dest!]: "x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k"
   298   by (auto simp add: Un_tables_def)
   299 
   300 lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})"
   301   by (simp add: Un_tables_def)
   302 
   303 
   304 subsubsection "overrides"
   305 
   306 lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m"
   307   by (simp add: overrides_t_def)
   308 
   309 lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m"
   310   by (simp add: overrides_t_def)
   311 
   312 lemma overrides_t_Some_iff: 
   313   "(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)"
   314   by (simp add: overrides_t_def)
   315 
   316 lemmas overrides_t_SomeD = overrides_t_Some_iff [THEN iffD1, dest!]
   317 
   318 lemma overrides_t_right_empty [simp]: "n k = {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = m k"  
   319   by (simp add: overrides_t_def)
   320 
   321 lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k"  
   322   by (simp add: overrides_t_def)
   323 
   324 
   325 subsubsection "hiding entails"
   326 
   327 lemma hiding_entailsD: 
   328   "t hiding s entails R \<Longrightarrow> t k = Some x \<Longrightarrow> s k = Some y \<Longrightarrow> R x y"
   329   by (simp add: hiding_entails_def)
   330 
   331 lemma empty_hiding_entails [simp]: "empty hiding s entails R"
   332   by (simp add: hiding_entails_def)
   333 
   334 lemma hiding_empty_entails [simp]: "t hiding empty entails R"
   335   by (simp add: hiding_entails_def)
   336 
   337 
   338 subsubsection "cond hiding entails"
   339 
   340 lemma cond_hiding_entailsD: 
   341 "\<lbrakk>t hiding s under C entails R; t k = Some x; s k = Some y; C x y\<rbrakk> \<Longrightarrow> R x y"
   342 by (simp add: cond_hiding_entails_def)
   343 
   344 lemma empty_cond_hiding_entails[simp]: "empty hiding s under C entails R"
   345 by (simp add: cond_hiding_entails_def)
   346 
   347 lemma cond_hiding_empty_entails[simp]: "t hiding empty under C entails R"
   348 by (simp add: cond_hiding_entails_def)
   349 
   350 lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"
   351 by (simp add: hidings_entails_def)
   352 
   353 lemma hidings_empty_entails [intro!]: "t hidings (\<lambda>k. {}) entails R"
   354 apply (unfold hidings_entails_def)
   355 apply (simp (no_asm))
   356 done
   357 
   358 lemma empty_hidings_entails [intro!]:
   359   "(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def)
   360 by (simp (no_asm))
   361 
   362 
   363 (*###TO Map?*)
   364 primrec atleast_free :: "('a \<rightharpoonup> 'b) => nat => bool"
   365 where
   366   "atleast_free m 0 = True"
   367 | atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None & (!b. atleast_free (m(a|->b)) n))"
   368 
   369 lemma atleast_free_weaken [rule_format (no_asm)]: 
   370   "!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n"
   371 apply (induct_tac "n")
   372 apply (simp (no_asm))
   373 apply clarify
   374 apply (simp (no_asm))
   375 apply (drule atleast_free_Suc [THEN iffD1])
   376 apply fast
   377 done
   378 
   379 lemma atleast_free_SucI: 
   380 "[| h a = None; !obj. atleast_free (h(a|->obj)) n |] ==> atleast_free h (Suc n)"
   381 by force
   382 
   383 declare fun_upd_apply [simp del]
   384 lemma atleast_free_SucD_lemma [rule_format (no_asm)]: 
   385 " !m a. m a = None --> (!c. atleast_free (m(a|->c)) n) -->  
   386   (!b d. a ~= b --> atleast_free (m(b|->d)) n)"
   387 apply (induct_tac "n")
   388 apply  auto
   389 apply (rule_tac x = "a" in exI)
   390 apply  (rule conjI)
   391 apply  (force simp add: fun_upd_apply)
   392 apply (erule_tac V = "m a = None" in thin_rl)
   393 apply clarify
   394 apply (subst fun_upd_twist)
   395 apply  (erule not_sym)
   396 apply (rename_tac "ba")
   397 apply (drule_tac x = "ba" in spec)
   398 apply clarify
   399 apply (tactic "smp_tac @{context} 2 1")
   400 apply (erule (1) notE impE)
   401 apply (case_tac "aa = b")
   402 apply fast+
   403 done
   404 declare fun_upd_apply [simp]
   405 
   406 lemma atleast_free_SucD: "atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n"
   407 apply auto
   408 apply (case_tac "aa = a")
   409 apply auto
   410 apply (erule atleast_free_SucD_lemma)
   411 apply auto
   412 done
   413 
   414 declare atleast_free_Suc [simp del]
   415 
   416 end