# HG changeset patch
# User nipkow
# Date 877681891 -7200
# Node ID b4f93a8da8359181d0fa5245a7e86adc8062000b
# Parent  21ef91734970fdc0d6165de669329ff3a4009afc
Added the new theory Map.

diff -r 21ef91734970 -r b4f93a8da835 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Oct 23 12:49:16 1997 +0200
+++ b/src/HOL/IsaMakefile	Fri Oct 24 10:31:31 1997 +0200
@@ -10,7 +10,7 @@
 
 NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
 	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
-	Divides Power Sexp Univ List RelPow Option
+	Divides Power Sexp Univ List RelPow Option Map
 
 PROVERS = hypsubst.ML classical.ML blast.ML \
 	simplifier.ML splitter.ML nat_transitive.ML 
diff -r 21ef91734970 -r b4f93a8da835 src/HOL/Map.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Map.ML	Fri Oct 24 10:31:31 1997 +0200
@@ -0,0 +1,78 @@
+(*  Title:      HOL/Map.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TU Muenchen
+
+Map lemmas
+*)
+
+goalw thy [empty_def] "empty k = None";
+by(Simp_tac 1);
+qed "empty_def2";
+Addsimps [empty_def2];
+
+goalw thy [update_def] "(m[a|->b])x = (if x=a then Some b else m x)";
+by(Simp_tac 1);
+qed "update_def2";
+Addsimps [update_def2];
+
+section "++";
+
+goalw thy [override_def] "m ++ empty = m";
+by(Simp_tac 1);
+qed "override_empty";
+Addsimps [override_empty];
+
+goalw thy [override_def] "empty ++ m = m";
+by(Simp_tac 1);
+br ext 1;
+by(split_tac [expand_option_case] 1);
+by(Simp_tac 1);
+qed "empty_override";
+Addsimps [empty_override];
+
+goalw thy [override_def]
+ "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
+by(simp_tac (!simpset addsplits [expand_option_case]) 1);
+qed_spec_mp "override_Some_iff";
+
+bind_thm("override_SomeD", standard(override_Some_iff RS iffD1));
+
+goalw thy [override_def]
+ "((m ++ n) k = None) = (n k = None & m k = None)";
+by(simp_tac (!simpset addsplits [expand_option_case]) 1);
+qed "override_None";
+AddIffs [override_None];
+
+goalw thy [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs";
+by(induct_tac "xs" 1);
+by(Simp_tac 1);
+br ext 1;
+by(asm_simp_tac (!simpset addsplits [expand_if,expand_option_case]) 1);
+qed "map_of_append";
+Addsimps [map_of_append];
+
+section "dom";
+
+goalw thy [dom_def] "dom empty = {}";
+by(Simp_tac 1);
+qed "dom_empty";
+Addsimps [dom_empty];
+
+goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
+by(simp_tac (!simpset addsplits [expand_if]) 1);
+by(Blast_tac 1);
+qed "dom_update";
+Addsimps [dom_update];
+
+goalw thy [dom_def] "dom(m++n) = dom n Un dom m";
+by(Blast_tac 1);
+qed "dom_override";
+Addsimps [dom_override];
+
+section "ran";
+
+goalw thy [ran_def] "ran empty = {}";
+by(Simp_tac 1);
+qed "ran_empty";
+Addsimps [ran_empty];
diff -r 21ef91734970 -r b4f93a8da835 src/HOL/Map.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Map.thy	Fri Oct 24 10:31:31 1997 +0200
@@ -0,0 +1,44 @@
+(*  Title:      HOL/Map.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow, based on a theory by David von Oheimb
+    Copyright   1997 TU Muenchen
+
+The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
+*)
+
+Map = List + Option +
+
+types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
+
+consts
+empty   :: "'a ~=> 'b"
+update  :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
+           ("_/[_/|->/_]" [900,0,0] 900)
+override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
+dom     :: "('a ~=> 'b) => 'a set"
+ran     :: "('a ~=> 'b) => 'b set"
+map_of  :: "('a * 'b)list => 'a ~=> 'b"
+
+syntax (symbols)
+  "~=>"     :: [type, type] => type
+               (infixr "\\<leadsto>" 0)
+  update    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
+               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
+  override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
+               (infixl "\\<oplus>" 100)
+
+defs
+empty_def "empty == %x. None"
+
+update_def "m[a|->b] == %x. if x=a then Some b else m x"
+
+override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
+
+dom_def "dom(m) == {a. m a ~= None}"
+ran_def "ran(m) == {b. ? a. m a = Some b}"
+
+primrec map_of list
+"map_of [] = empty"
+"map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
+
+end
diff -r 21ef91734970 -r b4f93a8da835 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Thu Oct 23 12:49:16 1997 +0200
+++ b/src/HOL/ROOT.ML	Fri Oct 24 10:31:31 1997 +0200
@@ -43,9 +43,9 @@
 use_thy "RelPow";
 use_thy "Finite";
 use_thy "Sexp";
-use_thy "Option";
 use_thy "WF_Rel";
 use_thy "List";
+use_thy "Map";
 
 (*TFL: recursive function definitions*)
 cd "../TFL";