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