Table.thy

(*  Title:      isabelle/Bali/Table.thy
    ID:         $Id: Table.thy,v 1.2 1997/10/22 12:00:10 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1997 Technische Universitaet Muenchen

Abstract tables and their implementation as lists

design concerns:
* definition of table: infinite mapping vs. list vs. finite set
  list chosen, because: 
  +  a priori finite
  +  lookup is computable
  -  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 any class, field, method etc.
      is considered to be defined)
  -  awkward distinction of cases, alleviated by operator 'the'

*)

Table = Basis +

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

consts

  etable	:: "('a, 'b) table"
  update	:: "('a, 'b) table => 'a => 'b => 
		    ('a, 'b) table"		("_[_:=_]" [1000,0,0] 1000)

  Un_tables	:: "('a, 'b) table set => ('a, 'b) tables"

  override	:: "('a, 'b) table => ('a, 'b) table => ('a, 'b) table"
						(infixl "++" 200)
  hiding_entails:: "('a, 'b) table => ('a, 'c) table => 
		    ('b => 'c => bool) => bool"	("_ hiding _ entails _")

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











defs

  etable_def	"etable	      == %k. None"
  update_def	"t[x:=y]      == %k. if k=x then Some y else t k"
  Un_tables_def	"Un_tables ts == %k. UN t:ts. o2s (t k)"


  override_def	"s ++ t == %k. case t k of None => s k | Some x => Some x"
  hiding_entails_def "t hiding s entails R == 
		      !k x. t k = Some x --> (!y. s k = Some y --> R x y)"

primrec table list

  table_Nil	"table []    = etable"
  table_Cons	"table (x#t) = (table t)[fst x:=snd x]"

end