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