Table.thy

(*  Title:      isabelle/Bali/Table.thy
    ID:         $Id: Table.thy,v 1.8 1998/04/08 15:27:05 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 system, 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)
  -  awkward case distinctions, alleviated by operator 'the'
*)

Table = Basis +

types ('a, 'b) table	(* table with key type 'a and contents type 'b *)
	= "'a ~=> 'b"
      ('a, 'b) tables	(* non-unique table with key 'a and contents 'b *)
	= "'a => 'b set"

syntax
  table_of	:: "('a * 'b) list => ('a, 'b) table"	(* concrete table *)

translations
  "table_of" == "map_of"

consts

  Un_tables	:: "('a, 'b) tables set => ('a, 'b) tables"
  overrides	:: "('a, 'b) tables     => ('a, 'b) tables => ('a, 'b) tables"
						  (infixl "++++" 100)
  hidings_entails:: "('a, 'b) tables => ('a, 'c) tables => 
		     ('b => 'c => bool) => bool"	  ("_ hidings _ entails _" 20)
  (* variant for unique table: *)
  hiding_entails :: "('a, 'b) table  => ('a, 'c) table  => 
		     ('b => 'c => bool) => bool"	  ("_ hiding _ entails _"  20)

defs

  Un_tables_def	      "Un_tables ts    == %k. UN t:ts. t k"
  overrides_def	      "s ++++ t        == %k. if t k = {} then s k else t k"
  hidings_entails_def "t hidings s entails R == !k. !x:t k. !y:s k. R x y"
  hiding_entails_def  "t hiding  s entails R == 
		        !k x. t k = Some x --> (!y. s k = Some y --> R x y)"

end