wenzelm@12857: (*  Title:      HOL/Bali/Table.thy
schirmer@12854:     Author:     David von Oheimb
schirmer@12854: *)
schirmer@12854: header {* Abstract tables and their implementation as lists *}
schirmer@12854: 
haftmann@16417: theory Table imports Basis begin
schirmer@12854: 
schirmer@12854: text {*
schirmer@12854: design issues:
schirmer@12854: \begin{itemize}
schirmer@12854: \item definition of table: infinite map vs. list vs. finite set
schirmer@12854:       list chosen, because:
schirmer@12854:   \begin{itemize} 
schirmer@12854:   \item[+]  a priori finite
schirmer@12854:   \item[+]  lookup is more operational than for finite set
schirmer@12854:   \item[-]  not very abstract, but function table converts it to abstract 
schirmer@12854:             mapping
schirmer@12854:   \end{itemize}
schirmer@12854: \item coding of lookup result: Some/None vs. value/arbitrary
schirmer@12854:    Some/None chosen, because:
schirmer@12854:   \begin{itemize}
schirmer@12854:   \item[++] makes definedness check possible (applies also to finite set),
schirmer@12854:      which is important for the type standard, hiding/overriding, etc.
schirmer@12854:      (though it may perhaps be possible at least for the operational semantics
schirmer@12854:       to treat programs as infinite, i.e. where classes, fields, methods etc.
schirmer@12854:       of any name are considered to be defined)
schirmer@12854:   \item[-]  sometimes awkward case distinctions, alleviated by operator 'the'
schirmer@12854:   \end{itemize}
schirmer@12854: \end{itemize}
schirmer@12854: *}
schirmer@12854: 
schirmer@13688: types ('a, 'b) table    --{* table with key type 'a and contents type 'b *}
nipkow@14134:       = "'a \<rightharpoonup> 'b"
schirmer@13688:       ('a, 'b) tables   --{* non-unique table with key 'a and contents 'b *}
schirmer@12854:       = "'a \<Rightarrow> 'b set"
schirmer@12854: 
schirmer@12854: 
schirmer@12854: section "map of / table of"
schirmer@12854: 
haftmann@34939: abbreviation
wenzelm@35355:   table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table"   --{* concrete table *}
wenzelm@35355:   where "table_of \<equiv> map_of"
haftmann@34939: 
schirmer@12854: translations
wenzelm@35431:   (type) "('a, 'b) table" <= (type) "'a \<rightharpoonup> 'b"
schirmer@12854: 
schirmer@12854: (* ### To map *)
nipkow@14025: lemma map_add_find_left[simp]:
schirmer@12854: "n k = None \<Longrightarrow> (m ++ n) k = m k"
nipkow@14025: by (simp add: map_add_def)
schirmer@12854: 
schirmer@12854: section {* Conditional Override *}
haftmann@35416: definition cond_override :: "('b \<Rightarrow>'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b)table \<Rightarrow> ('a, 'b) table" where
schirmer@12854: 
schirmer@13688: --{* when merging tables old and new, only override an entry of table old when  
schirmer@13688:    the condition cond holds *}
schirmer@12854: "cond_override cond old new \<equiv>
schirmer@12854:  \<lambda> k.
schirmer@12854:   (case new k of
schirmer@12854:      None         \<Rightarrow> old k                       
schirmer@12854:    | Some new_val \<Rightarrow> (case old k of
schirmer@12854:                         None         \<Rightarrow> Some new_val          
schirmer@12854:                       | Some old_val \<Rightarrow> (if cond new_val old_val
schirmer@12854:                                          then Some new_val     
schirmer@12854:                                          else Some old_val)))"
schirmer@12854: 
schirmer@12854: lemma cond_override_empty1[simp]: "cond_override c empty t = t"
schirmer@12854: by (simp add: cond_override_def expand_fun_eq)
schirmer@12854: 
schirmer@12854: lemma cond_override_empty2[simp]: "cond_override c t empty = t"
schirmer@12854: by (simp add: cond_override_def expand_fun_eq)
schirmer@12854: 
schirmer@12854: lemma cond_override_None[simp]:
schirmer@12854:  "old k = None \<Longrightarrow> (cond_override c old new) k = new k"
schirmer@12854: by (simp add: cond_override_def)
schirmer@12854: 
schirmer@12854: lemma cond_override_override:
schirmer@12854:  "\<lbrakk>old k = Some ov;new k = Some nv; C nv ov\<rbrakk> 
schirmer@12854:   \<Longrightarrow> (cond_override C old new) k = Some nv"
schirmer@12854: by (auto simp add: cond_override_def)
schirmer@12854: 
schirmer@12854: lemma cond_override_noOverride:
schirmer@12854:  "\<lbrakk>old k = Some ov;new k = Some nv; \<not> (C nv ov)\<rbrakk> 
schirmer@12854:   \<Longrightarrow> (cond_override C old new) k = Some ov"
schirmer@12854: by (auto simp add: cond_override_def)
schirmer@12854: 
schirmer@12854: lemma dom_cond_override: "dom (cond_override C s t) \<subseteq> dom s \<union> dom t"
schirmer@12854: by (auto simp add: cond_override_def dom_def)
schirmer@12854: 
schirmer@12854: lemma finite_dom_cond_override:
schirmer@12854:  "\<lbrakk> finite (dom s); finite (dom t) \<rbrakk> \<Longrightarrow> finite (dom (cond_override C s t))"
schirmer@12854: apply (rule_tac B="dom s \<union> dom t" in finite_subset)
schirmer@12854: apply (rule dom_cond_override)
schirmer@12854: by (rule finite_UnI)
schirmer@12854: 
schirmer@12854: section {* Filter on Tables *}
schirmer@12854: 
haftmann@35416: definition filter_tab :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
schirmer@12854: "filter_tab c t \<equiv> \<lambda> k. (case t k of 
schirmer@12854:                            None   \<Rightarrow> None
schirmer@12854:                          | Some x \<Rightarrow> if c k x then Some x else None)"
schirmer@12854: 
schirmer@12854: lemma filter_tab_empty[simp]: "filter_tab c empty = empty"
schirmer@12854: by (simp add: filter_tab_def empty_def)
schirmer@12854: 
schirmer@12854: lemma filter_tab_True[simp]: "filter_tab (\<lambda>x y. True) t = t"
schirmer@12854: by (simp add: expand_fun_eq filter_tab_def)
schirmer@12854: 
schirmer@12854: lemma filter_tab_False[simp]: "filter_tab (\<lambda>x y. False) t = empty"
schirmer@12854: by (simp add: expand_fun_eq filter_tab_def empty_def)
schirmer@12854: 
schirmer@12854: lemma filter_tab_ran_subset: "ran (filter_tab c t) \<subseteq> ran t"
schirmer@12854: by (auto simp add: filter_tab_def ran_def)
schirmer@12854: 
schirmer@12854: lemma filter_tab_range_subset: "range (filter_tab c t) \<subseteq> range t \<union> {None}"
schirmer@12854: apply (auto simp add: filter_tab_def)
schirmer@12854: apply (drule sym, blast)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma finite_range_filter_tab:
schirmer@12854:   "finite (range t) \<Longrightarrow> finite (range (filter_tab c t))"
schirmer@12854: apply (rule_tac B="range t \<union> {None} " in finite_subset)
schirmer@12854: apply (rule filter_tab_range_subset)
schirmer@12854: apply (auto intro: finite_UnI)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma filter_tab_SomeD[dest!]: 
schirmer@12854: "filter_tab c t k = Some x \<Longrightarrow> (t k = Some x) \<and> c k x"
schirmer@12854: by (auto simp add: filter_tab_def)
schirmer@12854: 
schirmer@12854: lemma filter_tab_SomeI: "\<lbrakk>t k = Some x;C k x\<rbrakk> \<Longrightarrow>filter_tab C t k = Some x"
schirmer@12854: by (simp add: filter_tab_def)
schirmer@12854: 
schirmer@12854: lemma filter_tab_all_True: 
schirmer@12854:  "\<forall> k y. t k = Some y \<longrightarrow> p k y \<Longrightarrow>filter_tab p t = t"
schirmer@12854: apply (auto simp add: filter_tab_def expand_fun_eq)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma filter_tab_all_True_Some:
schirmer@12854:  "\<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: by (auto simp add: filter_tab_def expand_fun_eq)
schirmer@12854: 
schirmer@12925: lemma filter_tab_all_False: 
schirmer@12925:  "\<forall> k y. t k = Some y \<longrightarrow> \<not> p k y \<Longrightarrow>filter_tab p t = empty"
schirmer@12925: by (auto simp add: filter_tab_def expand_fun_eq)
schirmer@12925: 
schirmer@12854: lemma filter_tab_None: "t k = None \<Longrightarrow> filter_tab p t k = None"
schirmer@12854: apply (simp add: filter_tab_def expand_fun_eq)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma filter_tab_dom_subset: "dom (filter_tab C t) \<subseteq> dom t"
schirmer@12854: by (auto simp add: filter_tab_def dom_def)
schirmer@12854: 
schirmer@12854: lemma filter_tab_eq: "\<lbrakk>a=b\<rbrakk> \<Longrightarrow> filter_tab C a = filter_tab C b"
schirmer@12854: by (auto simp add: expand_fun_eq filter_tab_def)
schirmer@12854: 
schirmer@12854: lemma finite_dom_filter_tab:
schirmer@12854: "finite (dom t) \<Longrightarrow> finite (dom (filter_tab C t))"
schirmer@12854: apply (rule_tac B="dom t" in finite_subset)
schirmer@12854: by (rule filter_tab_dom_subset)
schirmer@12854: 
schirmer@12854: 
schirmer@12854: lemma filter_tab_weaken:
schirmer@12854: "\<lbrakk>\<forall> a \<in> t k: \<exists> b \<in> s k: P a b; 
schirmer@12854:   \<And> k x y. \<lbrakk>t k = Some x;s k = Some y\<rbrakk> \<Longrightarrow> cond k x \<longrightarrow> cond k y
schirmer@12854:  \<rbrakk> \<Longrightarrow> \<forall> a \<in> filter_tab cond t k: \<exists> b \<in> filter_tab cond s k: P a b"
berghofe@13601: apply (force simp add: filter_tab_def)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma cond_override_filter: 
schirmer@12854:   "\<lbrakk>\<And> k old new. \<lbrakk>s k = Some new; t k = Some old\<rbrakk> 
schirmer@12854:     \<Longrightarrow> (\<not> overC new old \<longrightarrow>  \<not> filterC k new) \<and> 
schirmer@12854:         (overC new old \<longrightarrow> filterC k old \<longrightarrow> filterC k new)
schirmer@12854:    \<rbrakk> \<Longrightarrow>
schirmer@12854:     cond_override overC (filter_tab filterC t) (filter_tab filterC s) 
schirmer@12854:     = filter_tab filterC (cond_override overC t s)"
schirmer@12854: by (auto simp add: expand_fun_eq cond_override_def filter_tab_def )
schirmer@12854: 
schirmer@12925: 
schirmer@12854: section {* Misc. *}
schirmer@12854: 
schirmer@12854: 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: apply (erule rev_mp)
schirmer@12854: apply (induct l)
schirmer@12854: apply simp
schirmer@12854: apply (simp (no_asm))
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Ball_set_tableD: 
nipkow@30235:   "\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> Option.set (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
schirmer@12854: apply (frule Ball_set_table)
schirmer@12854: by auto
schirmer@12854: 
schirmer@12854: declare map_of_SomeD [elim]
schirmer@12854: 
schirmer@12854: lemma table_of_Some_in_set:
schirmer@12854: "table_of l k = Some x \<Longrightarrow> (k,x) \<in> set l"
schirmer@12854: by auto
schirmer@12854: 
schirmer@12854: lemma set_get_eq: 
schirmer@12854:   "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
paulson@18447: by (auto dest!: weak_map_of_SomeI)
schirmer@12854: 
schirmer@12854: lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
paulson@13585: apply (rule inj_onI)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_of_mapconst_SomeI:
schirmer@12854:   "\<lbrakk>table_of t k = Some y'; snd y=y'; fst y=c\<rbrakk> \<Longrightarrow>
schirmer@12854:    table_of (map (\<lambda>(k,x). (k,c,x)) t) k = Some y"
schirmer@12854: apply (induct t)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_of_mapconst_NoneI:
schirmer@12854:   "\<lbrakk>table_of t k = None\<rbrakk> \<Longrightarrow>
schirmer@12854:    table_of (map (\<lambda>(k,x). (k,c,x)) t) k = None"
schirmer@12854: apply (induct t)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard]
schirmer@12854: 
schirmer@12854: lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow>
schirmer@12854:    table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"
schirmer@12854: apply (induct_tac "t")
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_of_remap_SomeD [rule_format (no_asm)]: 
schirmer@12854:   "table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<longrightarrow>
schirmer@12854:   table_of t (k, k') = Some x"
schirmer@12854: apply (induct_tac "t")
schirmer@12854: apply  auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_of_mapf_Some [rule_format (no_asm)]: "\<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow> 
schirmer@12854:   table_of (map (\<lambda>(k,x). (k,f x)) t) k = Some (f x) \<longrightarrow> table_of t k = Some x"
schirmer@12854: apply (induct_tac "t")
schirmer@12854: apply  auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_of_mapf_SomeD [rule_format (no_asm), dest!]: 
schirmer@12854: "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: apply (induct_tac "t")
schirmer@12854: apply  auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_of_mapf_NoneD [rule_format (no_asm), dest!]: 
schirmer@12854: "table_of (map (\<lambda>(k,x). (k, f x)) t) k = None \<longrightarrow> (table_of t k = None)"
schirmer@12854: apply (induct_tac "t")
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_of_mapkey_SomeD [rule_format (no_asm), dest!]: 
schirmer@12854:   "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: apply (induct_tac "t")
schirmer@12854: apply  auto
schirmer@12854: done
schirmer@12854: lemma table_of_mapkey_SomeD2 [rule_format (no_asm), dest!]: 
schirmer@12854:   "table_of (map (\<lambda>(k,x). ((k,C),x)) t) ek = Some x 
schirmer@12854:    \<longrightarrow> C = snd ek \<and> table_of t (fst ek) = Some x"
schirmer@12854: apply (induct_tac "t")
schirmer@12854: apply  auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_append_Some_iff: "table_of (xs@ys) k = Some z = 
schirmer@12854:  (table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"
nipkow@14025: apply (simp)
nipkow@14025: apply (rule map_add_Some_iff)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:
schirmer@12854:   "table_of (filter P xs) k = Some z \<Longrightarrow> unique xs \<longrightarrow> table_of xs k = Some z"
schirmer@12854: apply (induct xs)
schirmer@12854: apply (auto del: map_of_SomeD intro!: map_of_SomeD)
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12854: consts
schirmer@12854:   Un_tables      :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
schirmer@12854:   overrides_t    :: "('a, 'b) tables     \<Rightarrow> ('a, 'b) tables \<Rightarrow>
schirmer@12854:                      ('a, 'b) tables"             (infixl "\<oplus>\<oplus>" 100)
schirmer@12854:   hidings_entails:: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow> 
schirmer@12854:                      ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hidings _ entails _" 20)
schirmer@13688:   --{* variant for unique table: *}
schirmer@12854:   hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  \<Rightarrow> 
schirmer@12854:                      ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"   ("_ hiding _ entails _"  20)
schirmer@13688:   --{* variant for a unique table and conditional overriding: *}
schirmer@12854:   cond_hiding_entails :: "('a, 'b) table  \<Rightarrow> ('a, 'c) table  
schirmer@12854:                           \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool"  
schirmer@12854:                           ("_ hiding _ under _ entails _"  20)
schirmer@12854: 
schirmer@12854: defs
schirmer@12854:   Un_tables_def:       "Un_tables ts\<spacespace>\<spacespace>\<equiv> \<lambda>k. \<Union>t\<in>ts. t k"
schirmer@12854:   overrides_t_def:     "s \<oplus>\<oplus> t        \<equiv> \<lambda>k. if t k = {} then s k else t k"
schirmer@12854:   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:   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:   cond_hiding_entails_def: "t hiding  s under C entails R
schirmer@12854:                             \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: C x y \<longrightarrow> R x y"
schirmer@12854: 
schirmer@12854: section "Untables"
schirmer@12854: 
schirmer@12854: lemma Un_tablesI [intro]:  "\<And>x. \<lbrakk>t \<in> ts; x \<in> t k\<rbrakk> \<Longrightarrow> x \<in> Un_tables ts k"
schirmer@12854: apply (simp add: Un_tables_def)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 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: apply (simp add: Un_tables_def)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})"
schirmer@12854: apply (unfold Un_tables_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: 
schirmer@12854: section "overrides"
schirmer@12854: 
schirmer@12854: lemma empty_overrides_t [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m"
schirmer@12854: apply (unfold overrides_t_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: lemma overrides_empty_t [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m"
schirmer@12854: apply (unfold overrides_t_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma overrides_t_Some_iff: 
schirmer@12854:  "(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)"
schirmer@12854: by (simp add: overrides_t_def)
schirmer@12854: 
schirmer@12854: lemmas overrides_t_SomeD = overrides_t_Some_iff [THEN iffD1, dest!]
schirmer@12854: 
schirmer@12854: lemma overrides_t_right_empty [simp]: "n k = {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = m k"  
schirmer@12854: by (simp add: overrides_t_def)
schirmer@12854: 
schirmer@12854: lemma overrides_t_find_right [simp]: "n k \<noteq> {} \<Longrightarrow> (m \<oplus>\<oplus> n) k = n k"  
schirmer@12854: by (simp add: overrides_t_def)
schirmer@12854: 
schirmer@12854: section "hiding entails"
schirmer@12854: 
schirmer@12854: lemma hiding_entailsD: 
schirmer@12854:   "\<lbrakk>t hiding s entails R; t k = Some x; s k = Some y\<rbrakk> \<Longrightarrow> R x y"
schirmer@12854: by (simp add: hiding_entails_def)
schirmer@12854: 
schirmer@12854: lemma empty_hiding_entails: "empty hiding s entails R"
schirmer@12854: by (simp add: hiding_entails_def)
schirmer@12854: 
schirmer@12854: lemma hiding_empty_entails: "t hiding empty entails R"
schirmer@12854: by (simp add: hiding_entails_def)
schirmer@12854: declare empty_hiding_entails [simp] hiding_empty_entails [simp]
schirmer@12854: 
schirmer@12854: section "cond hiding entails"
schirmer@12854: 
schirmer@12854: lemma cond_hiding_entailsD: 
schirmer@12854: "\<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: by (simp add: cond_hiding_entails_def)
schirmer@12854: 
schirmer@12854: lemma empty_cond_hiding_entails[simp]: "empty hiding s under C entails R"
schirmer@12854: by (simp add: cond_hiding_entails_def)
schirmer@12854: 
schirmer@12854: lemma cond_hiding_empty_entails[simp]: "t hiding empty under C entails R"
schirmer@12854: by (simp add: cond_hiding_entails_def)
schirmer@12854: 
schirmer@12854: lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"
schirmer@12854: by (simp add: hidings_entails_def)
schirmer@12854: 
schirmer@12854: lemma hidings_empty_entails: "t hidings (\<lambda>k. {}) entails R"
schirmer@12854: apply (unfold hidings_entails_def)
schirmer@12854: apply (simp (no_asm))
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma empty_hidings_entails: 
schirmer@12854:   "(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def)
schirmer@12854: by (simp (no_asm))
schirmer@12854: declare empty_hidings_entails [intro!] hidings_empty_entails [intro!]
schirmer@12854: 
schirmer@12854: 
schirmer@12854: 
schirmer@12854: (*###TO Map?*)
schirmer@12854: consts
schirmer@12854:   atleast_free :: "('a ~=> 'b) => nat => bool"
schirmer@12854: primrec
schirmer@12854:  "atleast_free m 0       = True"
schirmer@12854:  atleast_free_Suc: 
schirmer@12854:  "atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a|->b)) n))"
schirmer@12854: 
schirmer@12854: lemma atleast_free_weaken [rule_format (no_asm)]: 
schirmer@12854:   "!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n"
schirmer@12854: apply (induct_tac "n")
schirmer@12854: apply (simp (no_asm))
schirmer@12854: apply clarify
schirmer@12854: apply (simp (no_asm))
schirmer@12854: apply (drule atleast_free_Suc [THEN iffD1])
schirmer@12854: apply fast
schirmer@12854: done
schirmer@12854: 
schirmer@12854: lemma atleast_free_SucI: 
schirmer@12854: "[| h a = None; !obj. atleast_free (h(a|->obj)) n |] ==> atleast_free h (Suc n)"
schirmer@12854: by force
schirmer@12854: 
schirmer@12854: declare fun_upd_apply [simp del]
schirmer@12854: lemma atleast_free_SucD_lemma [rule_format (no_asm)]: 
schirmer@12854: " !m a. m a = None --> (!c. atleast_free (m(a|->c)) n) -->  
schirmer@12854:   (!b d. a ~= b --> atleast_free (m(b|->d)) n)"
schirmer@12854: apply (induct_tac "n")
schirmer@12854: apply  auto
schirmer@12854: apply (rule_tac x = "a" in exI)
schirmer@12854: apply  (rule conjI)
schirmer@12854: apply  (force simp add: fun_upd_apply)
schirmer@12854: apply (erule_tac V = "m a = None" in thin_rl)
schirmer@12854: apply clarify
schirmer@12854: apply (subst fun_upd_twist)
schirmer@12854: apply  (erule not_sym)
schirmer@12854: apply (rename_tac "ba")
schirmer@12854: apply (drule_tac x = "ba" in spec)
schirmer@12854: apply clarify
schirmer@12854: apply (tactic "smp_tac 2 1")
schirmer@12854: apply (erule (1) notE impE)
schirmer@12854: apply (case_tac "aa = b")
schirmer@12854: apply fast+
schirmer@12854: done
schirmer@12854: declare fun_upd_apply [simp]
schirmer@12854: 
schirmer@12854: lemma atleast_free_SucD [rule_format (no_asm)]: "atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n"
schirmer@12854: apply auto
schirmer@12854: apply (case_tac "aa = a")
schirmer@12854: apply auto
schirmer@12854: apply (erule atleast_free_SucD_lemma)
schirmer@12854: apply auto
schirmer@12854: done
schirmer@12854: 
schirmer@12854: declare atleast_free_Suc [simp del]
schirmer@12854: end