src/HOL/Bali/Table.thy
changeset 12854 00d4a435777f
child 12857 a4386cc9b1c3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Bali/Table.thy	Mon Jan 28 17:00:19 2002 +0100
     1.3 @@ -0,0 +1,445 @@
     1.4 +(*  Title:      isabelle/Bali/Table.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     David von Oheimb
     1.7 +    Copyright   1997 Technische Universitaet Muenchen
     1.8 +*)
     1.9 +header {* Abstract tables and their implementation as lists *}
    1.10 +
    1.11 +theory Table = Basis:
    1.12 +
    1.13 +text {*
    1.14 +design issues:
    1.15 +\begin{itemize}
    1.16 +\item definition of table: infinite map vs. list vs. finite set
    1.17 +      list chosen, because:
    1.18 +  \begin{itemize} 
    1.19 +  \item[+]  a priori finite
    1.20 +  \item[+]  lookup is more operational than for finite set
    1.21 +  \item[-]  not very abstract, but function table converts it to abstract 
    1.22 +            mapping
    1.23 +  \end{itemize}
    1.24 +\item coding of lookup result: Some/None vs. value/arbitrary
    1.25 +   Some/None chosen, because:
    1.26 +  \begin{itemize}
    1.27 +  \item[++] makes definedness check possible (applies also to finite set),
    1.28 +     which is important for the type standard, hiding/overriding, etc.
    1.29 +     (though it may perhaps be possible at least for the operational semantics
    1.30 +      to treat programs as infinite, i.e. where classes, fields, methods etc.
    1.31 +      of any name are considered to be defined)
    1.32 +  \item[-]  sometimes awkward case distinctions, alleviated by operator 'the'
    1.33 +  \end{itemize}
    1.34 +\end{itemize}
    1.35 +*}
    1.36 +
    1.37 +
    1.38 +types ('a, 'b) table    (* table with key type 'a and contents type 'b *)
    1.39 +      = "'a \<leadsto> 'b"
    1.40 +      ('a, 'b) tables   (* non-unique table with key 'a and contents 'b *)
    1.41 +      = "'a \<Rightarrow> 'b set"
    1.42 +
    1.43 +
    1.44 +section "map of / table of"
    1.45 +
    1.46 +syntax
    1.47 +  table_of      :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"    (* concrete table *)
    1.48 +
    1.49 +translations
    1.50 +  "table_of" == "map_of"
    1.51 +  
    1.52 +  (type)"'a \<leadsto> 'b"       <= (type)"'a \<Rightarrow> 'b Option.option"
    1.53 +  (type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
    1.54 +
    1.55 +(* ### To map *)
    1.56 +lemma override_find_left[simp]:
    1.57 +"n k = None \<Longrightarrow> (m ++ n) k = m k"
    1.58 +by (simp add: override_def)
    1.59 +
    1.60 +section {* Conditional Override *}
    1.61 +constdefs
    1.62 +cond_override:: 
    1.63 +  "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table"
    1.64 +
    1.65 +(* when merging tables old and new, only override an entry of table old when  
    1.66 +   the condition cond holds *)
    1.67 +"cond_override cond old new \<equiv>
    1.68 + \<lambda> k.
    1.69 +  (case new k of
    1.70 +     None         \<Rightarrow> old k                       
    1.71 +   | Some new_val \<Rightarrow> (case old k of
    1.72 +                        None         \<Rightarrow> Some new_val          
    1.73 +                      | Some old_val \<Rightarrow> (if cond new_val old_val
    1.74 +                                         then Some new_val     
    1.75 +                                         else Some old_val)))"
    1.76 +
    1.77 +lemma cond_override_empty1[simp]: "cond_override c empty t = t"
    1.78 +by (simp add: cond_override_def expand_fun_eq)
    1.79 +
    1.80 +lemma cond_override_empty2[simp]: "cond_override c t empty = t"
    1.81 +by (simp add: cond_override_def expand_fun_eq)
    1.82 +
    1.83 +lemma cond_override_None[simp]:
    1.84 + "old k = None \<Longrightarrow> (cond_override c old new) k = new k"
    1.85 +by (simp add: cond_override_def)
    1.86 +
    1.87 +lemma cond_override_override:
    1.88 + "\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 
    1.89 +  \<Longrightarrow> (cond_override C old new) k = Some nv"
    1.90 +by (auto simp add: cond_override_def)
    1.91 +
    1.92 +lemma cond_override_noOverride:
    1.93 + "\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 
    1.94 +  \<Longrightarrow> (cond_override C old new) k = Some ov"
    1.95 +by (auto simp add: cond_override_def)
    1.96 +
    1.97 +lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t"
    1.98 +by (auto simp add: cond_override_def dom_def)
    1.99 +
   1.100 +lemma finite_dom_cond_override:
   1.101 + "\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))"
   1.102 +apply (rule_tac B="dom s \<union> dom t" in finite_subset)
   1.103 +apply (rule dom_cond_override)
   1.104 +by (rule finite_UnI)
   1.105 +
   1.106 +section {* Filter on Tables *}
   1.107 +
   1.108 +constdefs
   1.109 +filter_tab:: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table"
   1.110 +"filter_tab c t \<equiv> \<lambda> k. (case t k of 
   1.111 +                           None   \<Rightarrow> None
   1.112 +                         | Some x \<Rightarrow> if c k x then Some x else None)"
   1.113 +
   1.114 +lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
   1.115 +by (simp add: filter_tab_def empty_def)
   1.116 +
   1.117 +lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"
   1.118 +by (simp add: expand_fun_eq filter_tab_def)
   1.119 +
   1.120 +lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
   1.121 +by (simp add: expand_fun_eq filter_tab_def empty_def)
   1.122 +
   1.123 +lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"
   1.124 +by (auto simp add: filter_tab_def ran_def)
   1.125 +
   1.126 +lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}"
   1.127 +apply (auto simp add: filter_tab_def)
   1.128 +apply (drule sym, blast)
   1.129 +done
   1.130 +
   1.131 +lemma finite_range_filter_tab:
   1.132 +  "finite (range t) \<Longrightarrow> finite (range (filter_tab c t))"
   1.133 +apply (rule_tac B="range t \<union> {None} " in finite_subset)
   1.134 +apply (rule filter_tab_range_subset)
   1.135 +apply (auto intro: finite_UnI)
   1.136 +done
   1.137 +
   1.138 +lemma filter_tab_SomeD[dest!]: 
   1.139 +"filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x"
   1.140 +by (auto simp add: filter_tab_def)
   1.141 +
   1.142 +lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x"
   1.143 +by (simp add: filter_tab_def)
   1.144 +
   1.145 +lemma filter_tab_all_True: 
   1.146 + "\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t"
   1.147 +apply (auto simp add: filter_tab_def expand_fun_eq)
   1.148 +done
   1.149 +
   1.150 +lemma filter_tab_all_True_Some:
   1.151 + "\<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"
   1.152 +by (auto simp add: filter_tab_def expand_fun_eq)
   1.153 +
   1.154 +lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
   1.155 +apply (simp add: filter_tab_def expand_fun_eq)
   1.156 +done
   1.157 +
   1.158 +lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t"
   1.159 +by (auto simp add: filter_tab_def dom_def)
   1.160 +
   1.161 +lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b"
   1.162 +by (auto simp add: expand_fun_eq filter_tab_def)
   1.163 +
   1.164 +lemma finite_dom_filter_tab:
   1.165 +"finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))"
   1.166 +apply (rule_tac B="dom t" in finite_subset)
   1.167 +by (rule filter_tab_dom_subset)
   1.168 +
   1.169 +
   1.170 +lemma filter_tab_weaken:
   1.171 +"\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 
   1.172 +  \<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y
   1.173 + \<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
   1.174 +apply (auto simp add: filter_tab_def)
   1.175 +done
   1.176 +
   1.177 +lemma cond_override_filter: 
   1.178 +  "\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 
   1.179 +    \<Longrightarrow> (\<not> overC new old \<longrightarrow>  \<not> filterC k new) \<and> 
   1.180 +        (overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new)
   1.181 +   \<rbrakk> \<Longrightarrow>
   1.182 +    cond_override overC (filter_tab filterC t) (filter_tab filterC s) 
   1.183 +    = filter_tab filterC (cond_override overC t s)"
   1.184 +by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )
   1.185 +
   1.186 +section {* Misc. *}
   1.187 +
   1.188 +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"
   1.189 +apply (erule make_imp)
   1.190 +apply (induct l)
   1.191 +apply simp
   1.192 +apply (simp (no_asm))
   1.193 +apply auto
   1.194 +done
   1.195 +
   1.196 +lemma Ball_set_tableD: 
   1.197 +  "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> o2s (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
   1.198 +apply (frule Ball_set_table)
   1.199 +by auto
   1.200 +
   1.201 +declare map_of_SomeD [elim]
   1.202 +
   1.203 +lemma table_of_Some_in_set:
   1.204 +"table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l"
   1.205 +by auto
   1.206 +
   1.207 +lemma set_get_eq: 
   1.208 +  "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
   1.209 +apply safe
   1.210 +apply (fast dest!: weak_map_of_SomeI)
   1.211 +apply auto
   1.212 +done
   1.213 +
   1.214 +lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
   1.215 +apply (rule injI)
   1.216 +apply auto
   1.217 +done
   1.218 +
   1.219 +lemma table_of_mapconst_SomeI:
   1.220 +  "\<lbrakk>table_of t k = Some y'; snd y=y'; fst y=c\<rbrakk> \<Longrightarrow>
   1.221 +   table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y"
   1.222 +apply (induct t)
   1.223 +apply auto
   1.224 +done
   1.225 +
   1.226 +lemma table_of_mapconst_NoneI:
   1.227 +  "\<lbrakk>table_of t k = None\<rbrakk> \<Longrightarrow>
   1.228 +   table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None"
   1.229 +apply (induct t)
   1.230 +apply auto
   1.231 +done
   1.232 +
   1.233 +lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard]
   1.234 +
   1.235 +lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow>
   1.236 +   table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"
   1.237 +apply (induct_tac "t")
   1.238 +apply auto
   1.239 +done
   1.240 +
   1.241 +lemma table_of_remap_SomeD [rule_format (no_asm)]: 
   1.242 +  "table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<longrightarrow>
   1.243 +  table_of t (k, k') = Some x"
   1.244 +apply (induct_tac "t")
   1.245 +apply  auto
   1.246 +done
   1.247 +
   1.248 +lemma table_of_mapf_Some [rule_format (no_asm)]: "\<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow> 
   1.249 +  table_of (map (\<lambda>(k,x). (k,f x)) t) k = Some (f x) \<longrightarrow> table_of t k = Some x"
   1.250 +apply (induct_tac "t")
   1.251 +apply  auto
   1.252 +done
   1.253 +
   1.254 +lemma table_of_mapf_SomeD [rule_format (no_asm), dest!]: 
   1.255 +"table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<longrightarrow> (\<exists>y\<in>table_of t k: z=f y)"
   1.256 +apply (induct_tac "t")
   1.257 +apply  auto
   1.258 +done
   1.259 +
   1.260 +lemma table_of_mapf_NoneD [rule_format (no_asm), dest!]: 
   1.261 +"table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<longrightarrow> (table_of t k = None)"
   1.262 +apply (induct_tac "t")
   1.263 +apply auto
   1.264 +done
   1.265 +
   1.266 +lemma table_of_mapkey_SomeD [rule_format (no_asm), dest!]: 
   1.267 +  "table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<longrightarrow> C = D \<and> table_of t k = Some x"
   1.268 +apply (induct_tac "t")
   1.269 +apply  auto
   1.270 +done
   1.271 +lemma table_of_mapkey_SomeD2 [rule_format (no_asm), dest!]: 
   1.272 +  "table_of (map (\<lambda>(k,x). ((k,C),x)) t) ek = Some x 
   1.273 +   \<longrightarrow> C = snd ek \<and> table_of t (fst ek) = Some x"
   1.274 +apply (induct_tac "t")
   1.275 +apply  auto
   1.276 +done
   1.277 +
   1.278 +lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 
   1.279 + (table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"
   1.280 +apply (simp only: map_of_override [THEN sym])
   1.281 +apply (rule override_Some_iff)
   1.282 +done
   1.283 +
   1.284 +lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:
   1.285 +  "table_of (filter P xs) k = Some z \<Longrightarrow> unique xs \<longrightarrow> table_of xs k = Some z"
   1.286 +apply (induct xs)
   1.287 +apply (auto del: map_of_SomeD intro!: map_of_SomeD)
   1.288 +done
   1.289 +
   1.290 +
   1.291 +consts
   1.292 +  Un_tables      :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
   1.293 +  overrides_t    :: "('a, 'b) tables     \<Rightarrow> ('a, 'b) tables \<Rightarrow>
   1.294 +                     ('a, 'b) tables"             (infixl "\<oplus>\<oplus>" 100)
   1.295 +  hidings_entails:: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> 
   1.296 +                     ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hidings _ entails _" 20)
   1.297 +  (* variant for unique table: *)
   1.298 +  hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> 
   1.299 +                     ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hiding _ entails _"  20)
   1.300 +  (* variant for a unique table and conditional overriding: *)
   1.301 +  cond_hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  
   1.302 +                          \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"  
   1.303 +                          ("_ hiding _ under _ entails _"  20)
   1.304 +
   1.305 +defs
   1.306 +  Un_tables_def:       "Un_tables ts\<spacespace>\<spacespace>\<equiv> \<lambda>k. \<Union>t\<in>ts. t k"
   1.307 +  overrides_t_def:     "s \<oplus>\<oplus> t        \<equiv> \<lambda>k. if t k = {} then s k else t k"
   1.308 +  hidings_entails_def: "t hidings s entails R \<equiv> \<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y"
   1.309 +  hiding_entails_def:  "t hiding  s entails R \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y"
   1.310 +  cond_hiding_entails_def: "t hiding  s under C entails R
   1.311 +                            \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y"
   1.312 +
   1.313 +section "Untables"
   1.314 +
   1.315 +lemma Un_tablesI [intro]:  "\<And>x. \<lbrakk>t \<in> ts; x \<in> t k\<rbrakk> \<Longrightarrow> x \<in> Un_tables ts k"
   1.316 +apply (simp add: Un_tables_def)
   1.317 +apply auto
   1.318 +done
   1.319 +
   1.320 +lemma Un_tablesD [dest!]: "\<And>x. x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k"
   1.321 +apply (simp add: Un_tables_def)
   1.322 +apply auto
   1.323 +done
   1.324 +
   1.325 +lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})"
   1.326 +apply (unfold Un_tables_def)
   1.327 +apply (simp (no_asm))
   1.328 +done
   1.329 +
   1.330 +
   1.331 +section "overrides"
   1.332 +
   1.333 +lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m"
   1.334 +apply (unfold overrides_t_def)
   1.335 +apply (simp (no_asm))
   1.336 +done
   1.337 +lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m"
   1.338 +apply (unfold overrides_t_def)
   1.339 +apply (simp (no_asm))
   1.340 +done
   1.341 +
   1.342 +lemma overrides_t_Some_iff: 
   1.343 + "(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)"
   1.344 +by (simp add: overrides_t_def)
   1.345 +
   1.346 +lemmas overrides_t_SomeD = overrides_t_Some_iff [THEN iffD1, dest!]
   1.347 +
   1.348 +lemma overrides_t_right_empty [simp]: "n k = {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = m k"  
   1.349 +by (simp add: overrides_t_def)
   1.350 +
   1.351 +lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k"  
   1.352 +by (simp add: overrides_t_def)
   1.353 +
   1.354 +section "hiding entails"
   1.355 +
   1.356 +lemma hiding_entailsD: 
   1.357 +  "\<lbrakk>t hiding s entails R; t k = Some x; s k = Some y\<rbrakk> \<Longrightarrow> R x y"
   1.358 +by (simp add: hiding_entails_def)
   1.359 +
   1.360 +lemma empty_hiding_entails: "empty hiding s entails R"
   1.361 +by (simp add: hiding_entails_def)
   1.362 +
   1.363 +lemma hiding_empty_entails: "t hiding empty entails R"
   1.364 +by (simp add: hiding_entails_def)
   1.365 +declare empty_hiding_entails [simp] hiding_empty_entails [simp]
   1.366 +
   1.367 +section "cond hiding entails"
   1.368 +
   1.369 +lemma cond_hiding_entailsD: 
   1.370 +"\<lbrakk>t hiding s under C entails R; t k = Some x; s k = Some y; C x y\<rbrakk> \<Longrightarrow> R x y"
   1.371 +by (simp add: cond_hiding_entails_def)
   1.372 +
   1.373 +lemma empty_cond_hiding_entails[simp]: "empty hiding s under C entails R"
   1.374 +by (simp add: cond_hiding_entails_def)
   1.375 +
   1.376 +lemma cond_hiding_empty_entails[simp]: "t hiding empty under C entails R"
   1.377 +by (simp add: cond_hiding_entails_def)
   1.378 +
   1.379 +lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"
   1.380 +by (simp add: hidings_entails_def)
   1.381 +
   1.382 +lemma hidings_empty_entails: "t hidings (\<lambda>k. {}) entails R"
   1.383 +apply (unfold hidings_entails_def)
   1.384 +apply (simp (no_asm))
   1.385 +done
   1.386 +
   1.387 +lemma empty_hidings_entails: 
   1.388 +  "(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def)
   1.389 +by (simp (no_asm))
   1.390 +declare empty_hidings_entails [intro!] hidings_empty_entails [intro!]
   1.391 +
   1.392 +
   1.393 +
   1.394 +(*###TO Map?*)
   1.395 +consts
   1.396 +  atleast_free :: "('a ~=> 'b) => nat => bool"
   1.397 +primrec
   1.398 + "atleast_free m 0       = True"
   1.399 + atleast_free_Suc: 
   1.400 + "atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a|->b)) n))"
   1.401 +
   1.402 +lemma atleast_free_weaken [rule_format (no_asm)]: 
   1.403 +  "!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n"
   1.404 +apply (induct_tac "n")
   1.405 +apply (simp (no_asm))
   1.406 +apply clarify
   1.407 +apply (simp (no_asm))
   1.408 +apply (drule atleast_free_Suc [THEN iffD1])
   1.409 +apply fast
   1.410 +done
   1.411 +
   1.412 +lemma atleast_free_SucI: 
   1.413 +"[| h a = None; !obj. atleast_free (h(a|->obj)) n |] ==> atleast_free h (Suc n)"
   1.414 +by force
   1.415 +
   1.416 +declare fun_upd_apply [simp del]
   1.417 +lemma atleast_free_SucD_lemma [rule_format (no_asm)]: 
   1.418 +" !m a. m a = None --> (!c. atleast_free (m(a|->c)) n) -->  
   1.419 +  (!b d. a ~= b --> atleast_free (m(b|->d)) n)"
   1.420 +apply (induct_tac "n")
   1.421 +apply  auto
   1.422 +apply (rule_tac x = "a" in exI)
   1.423 +apply  (rule conjI)
   1.424 +apply  (force simp add: fun_upd_apply)
   1.425 +apply (erule_tac V = "m a = None" in thin_rl)
   1.426 +apply clarify
   1.427 +apply (subst fun_upd_twist)
   1.428 +apply  (erule not_sym)
   1.429 +apply (rename_tac "ba")
   1.430 +apply (drule_tac x = "ba" in spec)
   1.431 +apply clarify
   1.432 +apply (tactic "smp_tac 2 1")
   1.433 +apply (erule (1) notE impE)
   1.434 +apply (case_tac "aa = b")
   1.435 +apply fast+
   1.436 +done
   1.437 +declare fun_upd_apply [simp]
   1.438 +
   1.439 +lemma atleast_free_SucD [rule_format (no_asm)]: "atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n"
   1.440 +apply auto
   1.441 +apply (case_tac "aa = a")
   1.442 +apply auto
   1.443 +apply (erule atleast_free_SucD_lemma)
   1.444 +apply auto
   1.445 +done
   1.446 +
   1.447 +declare atleast_free_Suc [simp del]
   1.448 +end