Up to index of Isabelle/Bali5
theory Table = Basis(* Title: isabelle/Bali/Table.thy
ID: $Id: Table.thy,v 1.29 2000/11/27 15:20:15 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'
*)
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"
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"
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"
consts
atleast_free :: "('a ~=> 'b) => nat => bool"
primrec
"atleast_free m 0 = True"
"atleast_free m (Suc n) = (? a. m a = None & (!b. atleast_free (m(a|->b)) n))"
end
theorem Ball_set_table:
Ball (set l) (split P) ==> ALL x. Ball (o2s (table_of l x)) (P x)
theorem Ball_set_tableD:
[| Ball (set l) (split P); x : o2s (table_of l xa) |] ==> P xa x
theorem Un_tablesI:
[| t : ts; x : t k |] ==> x : Un_tables ts k
theorem Un_tablesD:
x : Un_tables ts k ==> EX t. t : ts & x : t k
theorem Un_tables_empty:
Un_tables {} = (%k. {})
theorem empty_overrides:
(%k. {}) \<oplus>\<oplus> m = m
theorem overrides_empty:
m \<oplus>\<oplus> (%k. {}) = m
theorem overrides_Some_iff:
(x : (s \<oplus>\<oplus> t) k) = (x : t k | t k = {} & x : s k)
theorem hiding_entailsD:
[| t hiding s entails R; t k = Some x; s k = Some y |] ==> R x y
theorem empty_hiding_entails:
empty hiding s entails R
theorem hiding_empty_entails:
t hiding empty entails R
theorem hidings_entailsD:
[| t hidings s entails R; x : t k; y : s k |] ==> R x y
theorem hidings_empty_entails:
t hidings %k. {} entails R
theorem empty_hidings_entails:
%k. {} hidings s entails R
theorem set_get_eq:
unique l ==> ((k, the (table_of l k)) : set l) = (table_of l k ~= None)
theorem inj_Pair_const2:
inj (%k. (k, C))
theorem table_of_map2_SomeI:
table_of t k = Some x ==> table_of (map (split (%k. Pair (k, C))) t) (k, C) = Some x
theorem table_of_map_SomeI:
table_of t k = Some x ==> table_of (map (%(k, x). (k, f x)) t) k = Some (f x)
theorem 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
theorem 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
theorem table_of_mapf_SomeD:
table_of (map (%(k, x). (k, f x)) t) k = Some z ==> ? y:table_of t k: z = f y
theorem 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
theorem 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)
theorem table_of_filter_unique_SomeD:
[| table_of (filter P xs) k = Some z; unique xs |] ==> table_of xs k = Some z
theorem atleast_free_weaken:
atleast_free m (Suc n) ==> atleast_free m n
theorem atleast_free_SucI:
[| h a = None; ALL obj. atleast_free (h(a|->obj)) n |] ==> atleast_free h (Suc n)
theorem atleast_free_SucD_lemma:
[| m a = None; ALL c. atleast_free (m(a|->c)) n; a ~= b |] ==> atleast_free (m(b|->d)) n
theorem atleast_free_SucD:
atleast_free h (Suc n) ==> atleast_free (h(a|->b)) n