# HG changeset patch
# User paulson
# Date 1135162977 -3600
# Node ID da548623916a260421d8b56fefb61c749cc9d1a0
# Parent  6c558efcc754cc204c434248e9e9efda950900a0
removed or modified some instances of [iff]

diff -r 6c558efcc754 -r da548623916a src/HOL/Bali/Basis.thy
--- a/src/HOL/Bali/Basis.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/Basis.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -28,7 +28,9 @@
 change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
 *}
 declare if_weak_cong [cong del] option.weak_case_cong [cong del]
-declare length_Suc_conv [iff];
+declare length_Suc_conv [iff]
+
+declare not_None_eq [iff]
 
 (*###to be phased out *)
 ML {*
diff -r 6c558efcc754 -r da548623916a src/HOL/Bali/Decl.thy
--- a/src/HOL/Bali/Decl.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/Decl.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -636,8 +636,9 @@
 apply (erule make_imp)
 apply (rule subint1_induct)
 apply  assumption
+apply (simp (no_asm)) 
 apply safe
-apply (fast dest: subint1I ws_prog_ideclD)
+apply (blast dest: subint1I ws_prog_ideclD)
 done
 
 
@@ -649,6 +650,7 @@
 apply (erule make_imp)
 apply (rule subcls1_induct)
 apply  assumption
+apply (simp (no_asm)) 
 apply safe
 apply (fast dest: subcls1I ws_prog_cdeclD)
 done
@@ -673,7 +675,7 @@
       case True with iscls init show "P C" by auto
     next
       case False with ws step hyp iscls 
-      show "P C" by (auto dest: subcls1I ws_prog_cdeclD)
+      show "P C" by (auto iff: not_None_eq dest: subcls1I ws_prog_cdeclD)
     qed
   qed
   with clsC show ?thesis by simp
@@ -684,7 +686,7 @@
   \<And> co. class G Object = Some co \<Longrightarrow> P Object; 
   \<And> C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C
  \<rbrakk> \<Longrightarrow> P C"
-by (blast intro: ws_class_induct)
+by (auto intro: ws_class_induct)
 
 lemma ws_class_induct'' [consumes 2, case_names Object Subcls]:
 "\<lbrakk>class G C = Some c; ws_prog G; 
@@ -710,7 +712,7 @@
       case False
       with ws iscls obtain sc where
 	sc: "class G (super c) = Some sc"
-	by (auto dest: ws_prog_cdeclD)
+	by (auto iff: not_None_eq dest: ws_prog_cdeclD)
       from iscls False have "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 (super c)" by (rule subcls1I)
       with False ws step hyp iscls sc
       show "P C c" 
diff -r 6c558efcc754 -r da548623916a src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -3381,7 +3381,7 @@
         proof -
           from normal_s3 s3
           have "normal (x1,s1)"
-            by (cases s2) (simp add: abrupt_if_def)
+            by (cases s2) (simp add: abrupt_if_def not_Some_eq)
           with normal_s3 nrmAss_C1 s3 s1_s2
           show ?thesis
             by fastsimp
diff -r 6c558efcc754 -r da548623916a src/HOL/Bali/Example.thy
--- a/src/HOL/Bali/Example.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/Example.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -1018,7 +1018,7 @@
   "Ball (set standard_classes) (wf_cdecl tprg)"
 apply (unfold standard_classes_def Let_def 
        ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
-apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
+apply (simp (no_asm) add: wf_cdecl_def ws_cdecls not_Some_eq)
 apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def 
             intro: da.Skip)
 apply (auto simp add: Object_def Classes_def standard_classes_def 
diff -r 6c558efcc754 -r da548623916a src/HOL/Bali/State.thy
--- a/src/HOL/Bali/State.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/State.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -268,11 +268,8 @@
  "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None)"
 
 lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
-apply (unfold new_Addr_def)
-apply auto
-apply (case_tac "h (SOME a\<Colon>loc. h a = None)")
-apply simp
-apply (fast intro: someI2)
+apply (auto simp add: not_Some_eq new_Addr_def)
+apply (erule someI) 
 done
 
 lemma new_AddrD2: "new_Addr h = Some a \<Longrightarrow> \<forall>b. h b \<noteq> None \<longrightarrow> b \<noteq> a"
@@ -281,12 +278,8 @@
 done
 
 lemma new_Addr_SomeI: "h a = None \<Longrightarrow> \<exists>b. new_Addr h = Some b \<and> h b = None"
-apply (unfold new_Addr_def)
-apply (frule not_Some_eq [THEN iffD2])
-apply auto
-apply  (drule not_Some_eq [THEN iffD2])
-apply  auto
-apply (fast intro!: someI2)
+apply (simp add: new_Addr_def not_Some_eq)
+apply (fast intro: someI2)
 done
 
 
diff -r 6c558efcc754 -r da548623916a src/HOL/Bali/Table.thy
--- a/src/HOL/Bali/Table.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/Table.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -206,10 +206,7 @@
 
 lemma set_get_eq: 
   "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
-apply safe
-apply (fast dest!: weak_map_of_SomeI)
-apply auto
-done
+by (auto dest!: weak_map_of_SomeI)
 
 lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
 apply (rule inj_onI)
diff -r 6c558efcc754 -r da548623916a src/HOL/Bali/TypeRel.thy
--- a/src/HOL/Bali/TypeRel.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/TypeRel.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -393,7 +393,7 @@
 
 lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C"
 apply (erule implmt.induct)
-apply (blast dest: implmt1D subcls1D)+
+apply (auto dest: implmt1D subcls1D)
 done
 
 
diff -r 6c558efcc754 -r da548623916a src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -1466,7 +1466,7 @@
       next
 	case (VNam vn)
 	with EName el_in_list show ?thesis 
-	  by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
+	  by (auto simp add: not_Some_eq dom_def dest: map_upds_cut_irrelevant)
       qed
     qed
   qed
diff -r 6c558efcc754 -r da548623916a src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Datatype.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -140,11 +140,19 @@
 
 datatype 'a option = None | Some 'a
 
-lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
+lemma not_None_eq: "(x ~= None) = (EX y. x = Some y)"
+  by (induct x) auto
+
+lemma not_Some_eq: "(ALL y. x ~= Some y) = (x = None)"
   by (induct x) auto
 
-lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
-  by (induct x) auto
+text{*Both of these equalities are helpful only when applied to assumptions.*}
+
+lemmas not_None_eq_D = not_None_eq [THEN iffD1]
+declare not_None_eq_D [dest!]
+
+lemmas not_Some_eq_D = not_Some_eq [THEN iffD1]
+declare not_Some_eq_D [dest!]
 
 lemma option_caseE:
   "(case x of None => P | Some y => Q y) ==>
diff -r 6c558efcc754 -r da548623916a src/HOL/Hoare/SepLogHeap.thy
--- a/src/HOL/Hoare/SepLogHeap.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Hoare/SepLogHeap.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -9,6 +9,8 @@
 
 theory SepLogHeap imports Main begin
 
+declare not_None_eq [iff]
+
 types heap = "(nat \<Rightarrow> nat option)"
 
 text{* @{text "Some"} means allocated, @{text "None"} means
@@ -86,6 +88,7 @@
  "\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
 by (induct ps) (auto simp add:map_add_def split:option.split)
 
+
 lemma list_ortho_sum2[simp]:
  "\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
 by (induct ps) (auto simp add:map_add_def split:option.split)
diff -r 6c558efcc754 -r da548623916a src/HOL/Hoare/Separation.thy
--- a/src/HOL/Hoare/Separation.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Hoare/Separation.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -159,9 +159,7 @@
 
 (* a law of separation logic *)
 lemma star_comm: "P ** Q = Q ** P"
-apply(simp add:star_def ortho_def)
-apply(blast intro:map_add_comm)
-done
+  by(auto simp add:star_def ortho_def dest: map_add_comm)
 
 lemma "VARS H x y z w
  {P ** Q}
diff -r 6c558efcc754 -r da548623916a src/HOL/HoareParallel/RG_Hoare.thy
--- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -5,6 +5,8 @@
 subsection {* Proof System for Component Programs *}
 
 declare Un_subset_iff [iff del]
+declare not_None_eq [iff]
+declare Cons_eq_map_conv[iff]
 
 constdefs
   stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  
diff -r 6c558efcc754 -r da548623916a src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/IMP/Transition.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -672,9 +672,7 @@
 lemma FB_lemma2:
   "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
    \<langle>if c' = None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
-  apply (induct rule: converse_rtrancl_induct2)
-   apply simp
-  apply clarsimp
+  apply (induct rule: converse_rtrancl_induct2, force)
   apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
   done
 
diff -r 6c558efcc754 -r da548623916a src/HOL/IMPP/Hoare.ML
--- a/src/HOL/IMPP/Hoare.ML	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/IMPP/Hoare.ML	Wed Dec 21 12:02:57 2005 +0100
@@ -220,6 +220,7 @@
 qed "MGF_complete";
 
 AddSEs WTs_elim_cases;
+AddIffs [not_None_eq];
 (* requires com_det, escape (i.e. hoare_derivs.conseq) *)
 Goal "state_not_singleton ==> \
 \ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}";
diff -r 6c558efcc754 -r da548623916a src/HOL/Induct/QuoNestedDataType.thy
--- a/src/HOL/Induct/QuoNestedDataType.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Induct/QuoNestedDataType.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -222,7 +222,7 @@
 lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us"
 apply (induct z)
 apply (rule_tac [2] z=a in eq_Abs_Exp)
-apply (auto simp add: Abs_ExpList_def intro: exprel_refl)
+apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv intro: exprel_refl)
 done
 
 lemma eq_Abs_ExpList [case_names Abs_ExpList]:
diff -r 6c558efcc754 -r da548623916a src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Library/Nested_Environment.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -193,7 +193,7 @@
   from prems have "lookup env (xs @ ys) \<noteq> None" by simp
   then have "lookup env xs \<noteq> None"
     by (rule contrapos_nn) (simp only: lookup_append_none)
-  then show ?thesis by simp
+  then show ?thesis by (simp add: not_None_eq)
 qed
 
 text {*
diff -r 6c558efcc754 -r da548623916a src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/List.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -505,17 +505,21 @@
 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
 by (cases xs) auto
 
-lemma map_eq_Cons_conv[iff]:
+lemma map_eq_Cons_conv:
  "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
 by (cases xs) auto
 
-lemma Cons_eq_map_conv[iff]:
+lemma Cons_eq_map_conv:
  "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
 by (cases ys) auto
 
+lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]
+lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]
+declare map_eq_Cons_D [dest!]  Cons_eq_map_D [dest!]
+
 lemma ex_map_conv:
   "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
-by(induct ys, auto)
+by(induct ys, auto simp add: Cons_eq_map_conv)
 
 lemma map_eq_imp_length_eq:
   "!!xs. map f xs = map f ys ==> length xs = length ys"
@@ -867,10 +871,10 @@
 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
 by (induct xs) auto
 
-lemma concat_eq_Nil_conv [iff]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
+lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
 by (induct xss) auto
 
-lemma Nil_eq_concat_conv [iff]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
+lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
 by (induct xss) auto
 
 lemma set_concat [simp]: "set (concat xs) = \<Union>(set ` set xs)"
@@ -2238,8 +2242,8 @@
 by (induct xs) simp_all
 
 lemma filtermap_conv:
- "filtermap f xs = map (%x. the(f x)) (filter (%x. f x \<noteq> None) xs)"
-by (induct xs) auto
+     "filtermap f xs = map (%x. the(f x)) (filter (%x. f x \<noteq> None) xs)"
+  by (induct xs) (simp_all split: option.split) 
 
 lemma map_filter_conv[simp]: "map_filter f P xs = map f (filter P xs)"
 by (induct xs) auto
@@ -2388,7 +2392,7 @@
 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
 by (simp add:lex_conv)
 
-lemma Cons_in_lex [iff]:
+lemma Cons_in_lex [simp]:
     "((x # xs, y # ys) : lex r) =
       ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
 apply (simp add: lex_conv)
diff -r 6c558efcc754 -r da548623916a src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Map.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -478,7 +478,9 @@
 (* declare domI [intro]? *)
 
 lemma domD: "a : dom m ==> \<exists>b. m a = Some b"
-by (unfold dom_def, auto)
+apply (case_tac "m a") 
+apply (auto simp add: dom_def) 
+done
 
 lemma domIff[iff]: "(a : dom m) = (m a ~= None)"
 by (unfold dom_def, auto)
@@ -528,7 +530,7 @@
 
 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
 apply(rule ext)
-apply(fastsimp simp:map_add_def split:option.split)
+apply(force simp: map_add_def dom_def not_None_eq  split:option.split) 
 done
 
 subsection {* @{term [source] ran} *}
@@ -575,7 +577,7 @@
   by (simp add: map_le_def)
 
 lemma map_le_trans[trans]: "\<lbrakk> m1 \<subseteq>\<^sub>m m2; m2 \<subseteq>\<^sub>m m3\<rbrakk> \<Longrightarrow> m1 \<subseteq>\<^sub>m m3"
-by(force simp add:map_le_def)
+  by (auto simp add: map_le_def dom_def)
 
 lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
   apply (unfold map_le_def)
@@ -585,13 +587,13 @@
 done
 
 lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
-  by (fastsimp simp add: map_le_def)
+  by (fastsimp simp add: map_le_def not_None_eq)
 
 lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
 by(fastsimp simp add:map_add_def map_le_def expand_fun_eq split:option.splits)
 
 lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
-by (fastsimp simp add: map_le_def map_add_def dom_def)
+by (fastsimp simp add: map_le_def map_add_def dom_def not_None_eq)
 
 lemma map_add_le_mapI: "\<lbrakk> f \<subseteq>\<^sub>m h; g \<subseteq>\<^sub>m h; f \<subseteq>\<^sub>m f++g \<rbrakk> \<Longrightarrow> f++g \<subseteq>\<^sub>m h"
 by (clarsimp simp add: map_le_def map_add_def dom_def split:option.splits)
diff -r 6c558efcc754 -r da548623916a src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -208,7 +208,8 @@
   "C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow> 
   \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"
   apply (cases i)
-  apply (auto dest!: match_any_match_table match_X_match_table 
+  apply (auto iff: not_None_eq
+	      dest!: match_any_match_table match_X_match_table 
               dest: match_exception_table_in_et)
   done
 
diff -r 6c558efcc754 -r da548623916a src/HOL/MicroJava/J/JBasis.thy
--- a/src/HOL/MicroJava/J/JBasis.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -12,6 +12,7 @@
 theory JBasis imports Main begin 
 
 lemmas [simp] = Let_def
+declare not_None_eq [iff]
 
 section "unique"
  
diff -r 6c558efcc754 -r da548623916a src/HOL/MicroJava/J/TypeRel.thy
--- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -44,7 +44,7 @@
 lemma subcls1_def2: 
   "subcls1 G = 
      (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
-  by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
+  by (auto simp add: is_class_def not_None_eq dest: subcls1D intro: subcls1I)
 
 lemma finite_subcls1: "finite (subcls1 G)"
 apply(subst subcls1_def2)
diff -r 6c558efcc754 -r da548623916a src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -123,9 +123,7 @@
 done
 
 lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object"
-apply (unfold is_class_def)
-apply (simp (no_asm_simp))
-done
+  by (simp add: is_class_def not_None_eq)
 
 lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)"
   apply (simp add: ws_prog_def wf_syscls_def)
@@ -213,7 +211,7 @@
 apply( rule impI)
 apply( case_tac "C = Object")
 apply(  fast)
-apply safe
+apply auto
 apply( frule (1) class_wf) apply (erule conjE)+
 apply (frule wf_cdecl_ws_cdecl)
 apply( frule (1) wf_cdecl_supD)
@@ -263,7 +261,7 @@
 apply( rule impI)
 apply( case_tac "C = Object")
 apply(  fast)
-apply safe
+apply auto
 apply( frule (1) class_wf_struct)
 apply( frule (1) wf_cdecl_supD)
 
diff -r 6c558efcc754 -r da548623916a src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Set.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -1452,10 +1452,10 @@
 lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
   by blast
 
-lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
+lemma Union_empty_conv [simp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
   by blast
 
-lemma empty_Union_conv [iff]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
+lemma empty_Union_conv [simp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
   by blast
 
 lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
@@ -1479,7 +1479,7 @@
 lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   by blast
 
-lemma Inter_UNIV_conv [iff]:
+lemma Inter_UNIV_conv [simp]:
   "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
   "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
   by blast+
@@ -1555,12 +1555,12 @@
   -- {* Look: it has an \emph{existential} quantifier *}
   by blast
 
-lemma UNION_empty_conv[iff]:
+lemma UNION_empty_conv[simp]:
   "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
   "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
 by blast+
 
-lemma INTER_UNIV_conv[iff]:
+lemma INTER_UNIV_conv[simp]:
  "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
  "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
 by blast+
@@ -1790,7 +1790,7 @@
 lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
   by (unfold psubset_def) blast
 
-lemma all_not_in_conv [iff]: "(\<forall>x. x \<notin> A) = (A = {})"
+lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"
   by blast
 
 lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
diff -r 6c558efcc754 -r da548623916a src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/Unix/Unix.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -1058,7 +1058,8 @@
               have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
                   lookup root ((path @ [y]) @ us) \<noteq> None"
                 by cases (auto dest: access_some_lookup)
-              then show ?thesis by (blast dest!: lookup_some_append)
+              then show ?thesis 
+                by (simp add: not_None_eq, blast dest!: lookup_some_append)
             qed
             finally show ?thesis .
           qed
diff -r 6c558efcc754 -r da548623916a src/HOL/ex/Reflected_Presburger.thy
--- a/src/HOL/ex/Reflected_Presburger.thy	Tue Dec 20 22:06:00 2005 +0100
+++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Dec 21 12:02:57 2005 +0100
@@ -12,6 +12,8 @@
 imports Main
 begin
 
+declare not_Some_eq [iff]
+
 (* Shadow syntax for integer terms *)
 datatype intterm =
     Cst int
@@ -968,7 +970,7 @@
     moreover 
     {
       assume lini: "\<exists>li. linearize i = Some li"
-      from lini have lini2: "linearize i \<noteq> None" by simp
+      from lini have lini2: "linearize i \<noteq> None" by auto
       from lini obtain "li" where  "linearize i = Some li" by blast
       from lini2 lini have "islinintterm (the (linearize i))"
 	by (simp add: linearize_linear1[OF lini2])
@@ -1001,8 +1003,8 @@
     {
       assume lini: "\<exists>li. linearize i = Some li"
 	and linj: "\<exists>lj. linearize j = Some lj"
-      from lini have lini2: "linearize i \<noteq> None" by simp
-      from linj have linj2: "linearize j \<noteq> None" by simp
+      from lini have lini2: "linearize i \<noteq> None" by auto
+      from linj have linj2: "linearize j \<noteq> None" by auto
       from lini obtain "li" where  "linearize i = Some li" by blast
       from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
       then have linli: "islinintterm li" using prems by simp
@@ -1036,8 +1038,8 @@
     {
       assume lini: "\<exists>li. linearize i = Some li"
 	and linj: "\<exists>lj. linearize j = Some lj"
-      from lini have lini2: "linearize i \<noteq> None" by simp
-      from linj have linj2: "linearize j \<noteq> None" by simp
+      from lini have lini2: "linearize i \<noteq> None" by auto
+      from linj have linj2: "linearize j \<noteq> None" by auto
       from lini obtain "li" where  "linearize i = Some li" by blast
       from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
       with prems have linli: "islinintterm li" by simp
@@ -1081,7 +1083,7 @@
     {
       assume lini: "\<exists>li. linearize i = Some li"
 	and linj: "\<exists>bj. linearize j = Some (Cst bj)"
-      from lini have lini2: "linearize i \<noteq> None" by simp
+      from lini have lini2: "linearize i \<noteq> None" by auto
       from linj have linj2: "linearize j \<noteq> None" by auto
       from lini obtain "li" where  "linearize i = Some li" by blast
       from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
@@ -1143,7 +1145,7 @@
 qed  simp_all
 
 
-(* linearize, when successfull, preserves semantics *)
+(* linearize, when successful, preserves semantics *)
 lemma linearize_corr: "\<And> t'. linearize t = Some t' \<Longrightarrow> I_intterm ats t = I_intterm ats t' "
 proof-
   fix t'
@@ -1612,7 +1614,7 @@
 qed (simp_all)
 
 
-(* linform, if successfull, preserves quantifier freeness *)
+(* linform, if successful, preserves quantifier freeness *)
 lemma linform_isnnf: "islinform p \<Longrightarrow> isnnf p"
 by (induct p rule: islinform.induct) auto