Up to index of Isabelle/Bali5
theory Table = Basis:(* Title: isabelle/Bali/Table.thy
ID: $Id: Table.thy,v 1.31 2001/05/11 14:41:59 oheimb Exp $
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
Abstract tables and their implementation as lists
design issues:
* definition of table: infinite map vs. list vs. finite set
list chosen, because:
+ a priori finite
+ lookup is more operational than for finite set
- not very abstract, but function table converts it to abstract mapping
* coding of lookup result: Some/None vs. value/arbitrary
Some/None chosen, because:
++ makes definedness check possible (applies also to finite set),
which is important for the type standard, hiding/overriding, etc.
(though it may perhaps be possible at least for the operational semantics
to treat programs as infinite, i.e. where classes, fields, methods etc.
of any name are considered to be defined)
- sometimes awkward case distinctions, alleviated by operator 'the'
*)
theory Table = Basis:
types ('a, 'b) table (* table with key type 'a and contents type 'b *)
= "'a \<leadsto> 'b"
('a, 'b) tables (* non-unique table with key 'a and contents 'b *)
= "'a \<Rightarrow> 'b set"
section "map_of / table_of"
syntax
table_of :: "('a × 'b) list \<Rightarrow> ('a, 'b) table" (* concrete table *)
translations
"table_of" == "map_of"
(type)"'a \<leadsto> 'b" <= (type)"'a \<Rightarrow> 'b Option.option"
(type)"('a, 'b) table" <= (type)"'a \<leadsto> 'b"
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"
apply (erule make_imp)
apply (induct l)
apply simp
apply (simp (no_asm))
apply auto
done
lemma Ball_set_tableD:
"\<lbrakk>(\<forall> (x,y)\<in> set l. P x y); x \<in> o2s (table_of l xa)\<rbrakk> \<Longrightarrow> P xa x"
apply (frule Ball_set_table)
by auto
declare map_of_SomeD [elim]
lemma set_get_eq:
"unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
apply safe
apply (fast dest!: weak_map_of_SomeI)
apply auto
done
lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
apply (rule injI)
apply auto
done
lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard]
lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow>
table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"
apply (induct_tac "t")
apply auto
done
lemma table_of_remap_SomeD [rule_format (no_asm)]:
"table_of (map (\<lambda>((k,k'),x). (k,(k',x))) t) k = Some (k',x) \<longrightarrow>
table_of t (k, k') = Some x"
apply (induct_tac "t")
apply auto
done
lemma table_of_mapf_Some [rule_format (no_asm)]: "\<forall>x y. f x = f y \<longrightarrow> x = y \<Longrightarrow>
table_of (map (\<lambda>(k,x). (k,f x)) t) k = Some (f x) \<longrightarrow> table_of t k = Some x"
apply (induct_tac "t")
apply auto
done
lemma table_of_mapf_SomeD [rule_format (no_asm), dest!]:
"table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some z \<longrightarrow> (\<exists>y\<in>table_of t k: z=f y)"
apply (induct_tac "t")
apply auto
done
lemma table_of_mapkey_SomeD [rule_format (no_asm), dest!]:
"table_of (map (\<lambda>(k,x). ((k,C),x)) t) (k,D) = Some x \<longrightarrow> C = D \<and> table_of t k = Some x"
apply (induct_tac "t")
apply auto
done
lemma table_append_Some_iff: "table_of (xs@ys) k = Some z =
(table_of xs k = Some z \<or> (table_of xs k = None \<and> table_of ys k = Some z))"
apply (simp only: map_of_override [THEN sym])
apply (rule override_Some_iff)
done
lemma table_of_filter_unique_SomeD [rule_format (no_asm)]:
"table_of (filter P xs) k = Some z \<Longrightarrow> unique xs \<longrightarrow> table_of xs k = Some z"
apply (induct xs)
apply (auto del: map_of_SomeD intro!: map_of_SomeD)
done
consts
Un_tables :: "('a, 'b) tables set \<Rightarrow> ('a, 'b) tables"
overrides :: "('a, 'b) tables \<Rightarrow> ('a, 'b) tables \<Rightarrow>
('a, 'b) tables" (infixl "\<oplus>\<oplus>" 100)
hidings_entails:: "('a, 'b) tables \<Rightarrow> ('a, 'c) tables \<Rightarrow>
('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" ("_ hidings _ entails _" 20)
(* variant for unique table: *)
hiding_entails :: "('a, 'b) table \<Rightarrow> ('a, 'c) table \<Rightarrow>
('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> bool" ("_ hiding _ entails _" 20)
defs
Un_tables_def: "Un_tables ts \<equiv> \<lambda>k. \<Union>t\<in>ts. t k"
overrides_def: "s \<oplus>\<oplus> t \<equiv> \<lambda>k. if t k = {} then s k else t k"
hidings_entails_def: "t hidings s entails R \<equiv> \<forall>k. \<forall>x\<in>t k. \<forall>y\<in>s k. R x y"
hiding_entails_def: "t hiding s entails R \<equiv> \<forall>k. \<forall>x\<in>t k: \<forall>y\<in>s k: R x y"
section "Un_tables"
lemma Un_tablesI [intro]: "\<And>x. \<lbrakk>t \<in> ts; x \<in> t k\<rbrakk> \<Longrightarrow> x \<in> Un_tables ts k"
apply (simp add: Un_tables_def)
apply auto
done
lemma Un_tablesD [dest!]: "\<And>x. x \<in> Un_tables ts k \<Longrightarrow> \<exists>t. t \<in> ts \<and> x \<in> t k"
apply (simp add: Un_tables_def)
apply auto
done
lemma Un_tables_empty [simp]: "Un_tables {} = (\<lambda>k. {})"
apply (unfold Un_tables_def)
apply (simp (no_asm))
done
section "overrides"
lemma empty_overrides [simp]: "(\<lambda>k. {}) \<oplus>\<oplus> m = m"
apply (unfold overrides_def)
apply (simp (no_asm))
done
lemma overrides_empty [simp]: "m \<oplus>\<oplus> (\<lambda>k. {}) = m"apply (unfold overrides_def)
apply (simp (no_asm))
done
lemma overrides_Some_iff: "(x \<in> (s \<oplus>\<oplus> t) k) = (x \<in> t k \<or> t k = {} \<and> x \<in> s k)"
by (simp add: overrides_def)
lemmas overrides_SomeD = overrides_Some_iff [THEN iffD1, dest!]
section "hiding_entails"
lemma hiding_entailsD: "\<lbrakk>t hiding s entails R; t k = Some x; s k = Some y\<rbrakk> \<Longrightarrow> R x y"
by (simp add: hiding_entails_def)
lemma empty_hiding_entails: "empty hiding s entails R"
by (simp add: hiding_entails_def)
lemma hiding_empty_entails: "t hiding empty entails R"
by (simp add: hiding_entails_def)
declare empty_hiding_entails [simp] hiding_empty_entails [simp]
section "hidings_entails"
lemma hidings_entailsD: "\<lbrakk>t hidings s entails R; x \<in> t k; y \<in> s k\<rbrakk> \<Longrightarrow> R x y"
by (simp add: hidings_entails_def)
lemma hidings_empty_entails: "t hidings (\<lambda>k. {}) entails R"
apply (unfold hidings_entails_def)
apply (simp (no_asm))
done
lemma empty_hidings_entails:
"(\<lambda>k. {}) hidings s entails R"apply (unfold hidings_entails_def)
by (simp (no_asm))
declare empty_hidings_entails [intro!] hidings_empty_entails [intro!]
(*###TO Map?*)
consts
atleast_free :: "('a ~=> 'b) => nat => bool"
primrec
"atleast_free m 0 = True"
atleast_free_Suc:
"atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a|->b)) n))"
lemma atleast_free_weaken [rule_format (no_asm)]:
"!m. atleast_free m (Suc n) \<longrightarrow> atleast_free m n"
apply (induct_tac "n")
apply (simp (no_asm))
apply clarify
apply (simp (no_asm))
apply (drule atleast_free_Suc [THEN iffD1])
apply fast
done
lemma atleast_free_SucI:
"[| h a = None; !obj. atleast_free (h(a|->obj)) n |] ==> atleast_free h (Suc n)"
by force
declare fun_upd_apply [simp del]
lemma atleast_free_SucD_lemma [rule_format (no_asm)]:
" !m a. m a = None --> (!c. atleast_free (m(a|->c)) n) -->
(!b d. a ~= b --> atleast_free (m(b|->d)) n)"
apply (induct_tac "n")
apply auto
apply (rule_tac x = "a" in exI)
apply (rule conjI)
apply (force simp add: fun_upd_apply)
apply (erule_tac V = "m a = None" in thin_rl)
apply clarify
apply (subst fun_upd_twist)
apply (erule not_sym)
apply (rename_tac "ba")
apply (drule_tac x = "ba" in spec)
apply clarify
apply (tactic "smp_tac 2 1")
apply (erule (1) notE impE)
apply (case_tac "aa = b")
apply fast+
done
declare fun_upd_apply [simp]
lemma atleast_free_SucD [rule_format (no_asm)]: "atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n"
apply auto
apply (case_tac "aa = a")
apply auto
apply (erule atleast_free_SucD_lemma)
apply auto
done
declare atleast_free_Suc [simp del]
end
lemma Ball_set_table:
Ball (set l) (split P) ==> ALL x. Ball (o2s (table_of l x)) (P x)
lemma Ball_set_tableD:
[| Ball (set l) (split P); x : o2s (table_of l xa) |] ==> P xa x
lemma set_get_eq:
unique l ==> ((k, the (table_of l k)) : set l) = (table_of l k ~= None)
lemma inj_Pair_const2:
inj (%k. (k, C))
lemmas table_of_map2_SomeI:
table_of t k = Some x ==> table_of (map (split (%k. Pair (k, C))) t) (k, C) = Some x
lemma table_of_map_SomeI:
table_of t k = Some x ==> table_of (map (%(k, x). (k, f x)) t) k = Some (f x)
lemma table_of_remap_SomeD:
table_of (map (%((k, k'), x). (k, k', x)) t) k = Some (k', x) ==> table_of t (k, k') = Some x
lemma table_of_mapf_Some:
[| ALL x y. f x = f y --> x = y;
table_of (map (%(k, x). (k, f x)) t) k = Some (f x) |]
==> table_of t k = Some x
lemma table_of_mapf_SomeD:
table_of (map (%(k, x). (k, f x)) t) k = Some z ==> ? y:table_of t k: z = f y
lemma table_of_mapkey_SomeD:
table_of (map (split (%k. Pair (k, C))) t) (k, D) = Some x ==> C = D & table_of t k = Some x
lemma table_append_Some_iff:
(table_of (xs @ ys) k = Some z) = (table_of xs k = Some z | table_of xs k = None & table_of ys k = Some z)
lemma table_of_filter_unique_SomeD:
[| table_of (filter P xs) k = Some z; unique xs |] ==> table_of xs k = Some z
lemma Un_tablesI:
[| t : ts; x : t k |] ==> x : Un_tables ts k
lemma Un_tablesD:
x : Un_tables ts k ==> EX t. t : ts & x : t k
lemma Un_tables_empty:
Un_tables {} = (%k. {})
lemma empty_overrides:
(%k. {}) \<oplus>\<oplus> m = m
lemma overrides_empty:
m \<oplus>\<oplus> (%k. {}) = m
lemma overrides_Some_iff:
(x : (s \<oplus>\<oplus> t) k) = (x : t k | t k = {} & x : s k)
lemmas overrides_SomeD:
x_1 : (s_1 \<oplus>\<oplus> t_1) k_1
==> x_1 : t_1 k_1 | t_1 k_1 = {} & x_1 : s_1 k_1
lemma hiding_entailsD:
[| t hiding s entails R; t k = Some x; s k = Some y |] ==> R x y
lemma empty_hiding_entails:
empty hiding s entails R
lemma hiding_empty_entails:
t hiding empty entails R
lemma hidings_entailsD:
[| t hidings s entails R; x : t k; y : s k |] ==> R x y
lemma hidings_empty_entails:
t hidings %k. {} entails R
lemma empty_hidings_entails:
%k. {} hidings s entails R
lemma atleast_free_weaken:
atleast_free m (Suc n) ==> atleast_free m n
lemma atleast_free_SucI:
[| h a = None; ALL obj. atleast_free (h(a|->obj)) n |] ==> atleast_free h (Suc n)
lemma atleast_free_SucD_lemma:
[| m a = None; ALL c. atleast_free (m(a|->c)) n; a ~= b |] ==> atleast_free (m(b|->d)) n
lemma atleast_free_SucD:
atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n