adjusted dom rules
authornipkow
Sat Feb 08 14:46:22 2003 +0100 (2003-02-08)
changeset 13811f39f67982854
parent 13810 c3fbfd472365
child 13812 91713a1915ee
adjusted dom rules
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Map.ML
     1.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Feb 07 16:40:23 2003 +0100
     1.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat Feb 08 14:46:22 2003 +0100
     1.3 @@ -2247,7 +2247,7 @@
     1.4  proof -
     1.5    -- {* To properly perform induction on the evaluation relation we have to
     1.6          generalize the lemma to terms not only expressions. *}
     1.7 -  {fix t val
     1.8 +  { fix t val
     1.9     assume eval': "prg Env\<turnstile> s0 \<midarrow>t\<succ>\<rightarrow> (val,s1)"  
    1.10     assume bool': "Env\<turnstile> t\<Colon>Inl (PrimT Boolean)"
    1.11     assume expr:  "\<exists> expr. t=In1l expr"
    1.12 @@ -3634,7 +3634,7 @@
    1.13          hence "normal s2"
    1.14            by (cases s2) simp
    1.15          with nrmAss_A' nrm_A_A' s2_s3 show ?thesis
    1.16 -          by auto
    1.17 +          by blast
    1.18        qed
    1.19      qed
    1.20      moreover
     2.1 --- a/src/HOL/Map.ML	Fri Feb 07 16:40:23 2003 +0100
     2.2 +++ b/src/HOL/Map.ML	Sat Feb 08 14:46:22 2003 +0100
     2.3 @@ -221,7 +221,12 @@
     2.4  Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
     2.5  by Auto_tac;
     2.6  qed "domD";
     2.7 -AddSDs [domD];
     2.8 +
     2.9 +Goalw [dom_def] "(a : dom m) = (m a ~= None)";
    2.10 +by Auto_tac;
    2.11 +qed "domIff";
    2.12 +AddIffs [domIff];
    2.13 +Delsimps [domIff];
    2.14  
    2.15  Goalw [dom_def] "dom empty = {}";
    2.16  by (Simp_tac 1);