Made empty a translation rather than a constant.
authornipkow
Tue Apr 01 17:43:10 2003 +0200 (2003-04-01)
changeset 1389090611b4e0054
parent 13889 6676ac2527fa
child 13891 ae9a2a433388
Made empty a translation rather than a constant.
src/HOL/Map.ML
src/HOL/Map.thy
src/HOL/MicroJava/J/JListExample.thy
src/HOL/W0/W0.thy
     1.1 --- a/src/HOL/Map.ML	Tue Apr 01 16:08:34 2003 +0200
     1.2 +++ b/src/HOL/Map.ML	Tue Apr 01 17:43:10 2003 +0200
     1.3 @@ -8,17 +8,13 @@
     1.4  
     1.5  section "empty";
     1.6  
     1.7 -Goalw [empty_def] "empty k = None";
     1.8 -by (Simp_tac 1);
     1.9 -qed "empty_def2";
    1.10 -Addsimps [empty_def2];
    1.11 -
    1.12  Goal "empty(x := None) = empty";
    1.13  by (rtac ext 1);
    1.14  by (Simp_tac 1);
    1.15  qed "empty_upd_none";
    1.16  Addsimps [empty_upd_none];
    1.17  
    1.18 +(* FIXME: what is this sum_case nonsense?? *)
    1.19  Goal "sum_case empty empty = empty";
    1.20  by (rtac ext 1);
    1.21  by (simp_tac (simpset() addsplits [sum.split]) 1);
    1.22 @@ -48,6 +44,7 @@
    1.23  qed "finite_range_updI";
    1.24  
    1.25  
    1.26 +(* FIXME: what is this sum_case nonsense?? *)
    1.27  section "sum_case and empty/map_upd";
    1.28  
    1.29  Goal "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)";
     2.1 --- a/src/HOL/Map.thy	Tue Apr 01 16:08:34 2003 +0200
     2.2 +++ b/src/HOL/Map.thy	Tue Apr 01 17:43:10 2003 +0200
     2.3 @@ -11,7 +11,6 @@
     2.4  types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
     2.5  
     2.6  consts
     2.7 -empty	::  "'a ~=> 'b"
     2.8  chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
     2.9  override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
    2.10  dom	:: "('a ~=> 'b) => 'a set"
    2.11 @@ -20,6 +19,7 @@
    2.12  map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
    2.13  	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
    2.14  syntax
    2.15 +empty	::  "'a ~=> 'b"
    2.16  map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
    2.17  					         ("_/'(_/|->_')"   [900,0,0]900)
    2.18  
    2.19 @@ -31,13 +31,13 @@
    2.20  				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
    2.21  
    2.22  translations
    2.23 +  "empty"    => "_K None"
    2.24 +  "empty"    <= "%x. None"
    2.25  
    2.26    "m(a|->b)" == "m(a:=Some b)"
    2.27  
    2.28  defs
    2.29  
    2.30 -empty_def    "empty == %x. None"
    2.31 -
    2.32  chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
    2.33  
    2.34  override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
     3.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Tue Apr 01 16:08:34 2003 +0200
     3.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Apr 01 17:43:10 2003 +0200
     3.3 @@ -89,7 +89,7 @@
     3.4  *}
     3.5  
     3.6  generate_code
     3.7 -  test = "example_prg\<turnstile>Norm (Map.empty, Map.empty)
     3.8 +  test = "example_prg\<turnstile>Norm (empty, empty)
     3.9      -(Expr (l1_name::=NewC list_name);;
    3.10        Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
    3.11        Expr (l2_name::=NewC list_name);;
     4.1 --- a/src/HOL/W0/W0.thy	Tue Apr 01 16:08:34 2003 +0200
     4.2 +++ b/src/HOL/W0/W0.thy	Tue Apr 01 17:43:10 2003 +0200
     4.3 @@ -133,7 +133,7 @@
     4.4    by (rule ext) (simp add: id_subst_def)
     4.5  
     4.6  lemma dom_id_subst [simp]: "dom id_subst = {}"
     4.7 -  by (simp add: dom_def id_subst_def empty_def)
     4.8 +  by (simp add: dom_def id_subst_def)
     4.9  
    4.10  lemma cod_id_subst [simp]: "cod id_subst = {}"
    4.11    by (simp add: cod_def)