Added the new theory Map.
authornipkow
Fri Oct 24 10:31:31 1997 +0200 (1997-10-24)
changeset 3981b4f93a8da835
parent 3980 21ef91734970
child 3982 2a903ba8d39e
Added the new theory Map.
src/HOL/IsaMakefile
src/HOL/Map.ML
src/HOL/Map.thy
src/HOL/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Oct 23 12:49:16 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Fri Oct 24 10:31:31 1997 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  NAMES = HOL Ord Set Fun subset equalities Prod Relation Trancl Sum WF WF_Rel \
     1.6  	mono Lfp Gfp NatDef Nat intr_elim indrule Inductive Finite Arith \
     1.7 -	Divides Power Sexp Univ List RelPow Option
     1.8 +	Divides Power Sexp Univ List RelPow Option Map
     1.9  
    1.10  PROVERS = hypsubst.ML classical.ML blast.ML \
    1.11  	simplifier.ML splitter.ML nat_transitive.ML 
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Map.ML	Fri Oct 24 10:31:31 1997 +0200
     2.3 @@ -0,0 +1,78 @@
     2.4 +(*  Title:      HOL/Map.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow
     2.7 +    Copyright   1997 TU Muenchen
     2.8 +
     2.9 +Map lemmas
    2.10 +*)
    2.11 +
    2.12 +goalw thy [empty_def] "empty k = None";
    2.13 +by(Simp_tac 1);
    2.14 +qed "empty_def2";
    2.15 +Addsimps [empty_def2];
    2.16 +
    2.17 +goalw thy [update_def] "(m[a|->b])x = (if x=a then Some b else m x)";
    2.18 +by(Simp_tac 1);
    2.19 +qed "update_def2";
    2.20 +Addsimps [update_def2];
    2.21 +
    2.22 +section "++";
    2.23 +
    2.24 +goalw thy [override_def] "m ++ empty = m";
    2.25 +by(Simp_tac 1);
    2.26 +qed "override_empty";
    2.27 +Addsimps [override_empty];
    2.28 +
    2.29 +goalw thy [override_def] "empty ++ m = m";
    2.30 +by(Simp_tac 1);
    2.31 +br ext 1;
    2.32 +by(split_tac [expand_option_case] 1);
    2.33 +by(Simp_tac 1);
    2.34 +qed "empty_override";
    2.35 +Addsimps [empty_override];
    2.36 +
    2.37 +goalw thy [override_def]
    2.38 + "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
    2.39 +by(simp_tac (!simpset addsplits [expand_option_case]) 1);
    2.40 +qed_spec_mp "override_Some_iff";
    2.41 +
    2.42 +bind_thm("override_SomeD", standard(override_Some_iff RS iffD1));
    2.43 +
    2.44 +goalw thy [override_def]
    2.45 + "((m ++ n) k = None) = (n k = None & m k = None)";
    2.46 +by(simp_tac (!simpset addsplits [expand_option_case]) 1);
    2.47 +qed "override_None";
    2.48 +AddIffs [override_None];
    2.49 +
    2.50 +goalw thy [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs";
    2.51 +by(induct_tac "xs" 1);
    2.52 +by(Simp_tac 1);
    2.53 +br ext 1;
    2.54 +by(asm_simp_tac (!simpset addsplits [expand_if,expand_option_case]) 1);
    2.55 +qed "map_of_append";
    2.56 +Addsimps [map_of_append];
    2.57 +
    2.58 +section "dom";
    2.59 +
    2.60 +goalw thy [dom_def] "dom empty = {}";
    2.61 +by(Simp_tac 1);
    2.62 +qed "dom_empty";
    2.63 +Addsimps [dom_empty];
    2.64 +
    2.65 +goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
    2.66 +by(simp_tac (!simpset addsplits [expand_if]) 1);
    2.67 +by(Blast_tac 1);
    2.68 +qed "dom_update";
    2.69 +Addsimps [dom_update];
    2.70 +
    2.71 +goalw thy [dom_def] "dom(m++n) = dom n Un dom m";
    2.72 +by(Blast_tac 1);
    2.73 +qed "dom_override";
    2.74 +Addsimps [dom_override];
    2.75 +
    2.76 +section "ran";
    2.77 +
    2.78 +goalw thy [ran_def] "ran empty = {}";
    2.79 +by(Simp_tac 1);
    2.80 +qed "ran_empty";
    2.81 +Addsimps [ran_empty];
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Map.thy	Fri Oct 24 10:31:31 1997 +0200
     3.3 @@ -0,0 +1,44 @@
     3.4 +(*  Title:      HOL/Map.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow, based on a theory by David von Oheimb
     3.7 +    Copyright   1997 TU Muenchen
     3.8 +
     3.9 +The datatype of `maps' (written ~=>); strongly resembles maps in VDM.
    3.10 +*)
    3.11 +
    3.12 +Map = List + Option +
    3.13 +
    3.14 +types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
    3.15 +
    3.16 +consts
    3.17 +empty   :: "'a ~=> 'b"
    3.18 +update  :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    3.19 +           ("_/[_/|->/_]" [900,0,0] 900)
    3.20 +override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    3.21 +dom     :: "('a ~=> 'b) => 'a set"
    3.22 +ran     :: "('a ~=> 'b) => 'b set"
    3.23 +map_of  :: "('a * 'b)list => 'a ~=> 'b"
    3.24 +
    3.25 +syntax (symbols)
    3.26 +  "~=>"     :: [type, type] => type
    3.27 +               (infixr "\\<leadsto>" 0)
    3.28 +  update    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    3.29 +               ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
    3.30 +  override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
    3.31 +               (infixl "\\<oplus>" 100)
    3.32 +
    3.33 +defs
    3.34 +empty_def "empty == %x. None"
    3.35 +
    3.36 +update_def "m[a|->b] == %x. if x=a then Some b else m x"
    3.37 +
    3.38 +override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
    3.39 +
    3.40 +dom_def "dom(m) == {a. m a ~= None}"
    3.41 +ran_def "ran(m) == {b. ? a. m a = Some b}"
    3.42 +
    3.43 +primrec map_of list
    3.44 +"map_of [] = empty"
    3.45 +"map_of (p#ps) = (map_of ps)[fst p |-> snd p]"
    3.46 +
    3.47 +end
     4.1 --- a/src/HOL/ROOT.ML	Thu Oct 23 12:49:16 1997 +0200
     4.2 +++ b/src/HOL/ROOT.ML	Fri Oct 24 10:31:31 1997 +0200
     4.3 @@ -43,9 +43,9 @@
     4.4  use_thy "RelPow";
     4.5  use_thy "Finite";
     4.6  use_thy "Sexp";
     4.7 -use_thy "Option";
     4.8  use_thy "WF_Rel";
     4.9  use_thy "List";
    4.10 +use_thy "Map";
    4.11  
    4.12  (*TFL: recursive function definitions*)
    4.13  cd "../TFL";