empty_upd_none;
authorwenzelm
Wed Jan 24 20:55:29 2001 +0100 (2001-01-24)
changeset 109735b0d04078d2a
parent 10972 af160f8d3bd7
child 10974 f23a58cf12a4
empty_upd_none;
src/HOL/Map.ML
     1.1 --- a/src/HOL/Map.ML	Wed Jan 24 17:53:01 2001 +0100
     1.2 +++ b/src/HOL/Map.ML	Wed Jan 24 20:55:29 2001 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Tobias Nipkow
     1.5      Copyright   1997 TU Muenchen
     1.6  
     1.7 -Map lemmas
     1.8 +Map lemmas.
     1.9  *)
    1.10  
    1.11  section "empty";
    1.12 @@ -13,6 +13,12 @@
    1.13  qed "empty_def2";
    1.14  Addsimps [empty_def2];
    1.15  
    1.16 +Goal "empty(x := None) = empty";
    1.17 +by (rtac ext 1);
    1.18 +by (Simp_tac 1);
    1.19 +qed "empty_upd_none";
    1.20 +Addsimps [empty_upd_none];
    1.21 +
    1.22  Goal "sum_case empty empty = empty";
    1.23  by (rtac ext 1);
    1.24  by (simp_tac (simpset() addsplits [sum.split]) 1);
    1.25 @@ -202,8 +208,8 @@
    1.26  
    1.27  Goalw [dom_def] "finite (dom (map_of l))";
    1.28  by (induct_tac "l" 1);
    1.29 -by (auto_tac (claset(), 
    1.30 -	      simpset() addsimps [insert_Collect RS sym]));
    1.31 +by (auto_tac (claset(),
    1.32 +              simpset() addsimps [insert_Collect RS sym]));
    1.33  qed "finite_dom_map_of";
    1.34  
    1.35  Goalw [dom_def] "dom(m++n) = dom n Un dom m";