equal
deleted
inserted
replaced
1 (* Title: HOL/Bali/Table.thy |
1 (* Title: HOL/Bali/Table.thy |
2 ID: $Id$ |
|
3 Author: David von Oheimb |
2 Author: David von Oheimb |
4 *) |
3 *) |
5 header {* Abstract tables and their implementation as lists *} |
4 header {* Abstract tables and their implementation as lists *} |
6 |
5 |
7 theory Table imports Basis begin |
6 theory Table imports Basis begin |
39 section "map of / table of" |
38 section "map of / table of" |
40 |
39 |
41 syntax |
40 syntax |
42 table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *} |
41 table_of :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) table" --{* concrete table *} |
43 |
42 |
|
43 abbreviation |
|
44 "table_of \<equiv> map_of" |
|
45 |
44 translations |
46 translations |
45 "table_of" == "map_of" |
|
46 |
|
47 (type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option" |
47 (type)"'a \<rightharpoonup> 'b" <= (type)"'a \<Rightarrow> 'b Datatype.option" |
48 (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b" |
48 (type)"('a, 'b) table" <= (type)"'a \<rightharpoonup> 'b" |
49 |
49 |
50 (* ### To map *) |
50 (* ### To map *) |
51 lemma map_add_find_left[simp]: |
51 lemma map_add_find_left[simp]: |