removed or modified some instances of [iff]
authorpaulson
Wed Dec 21 12:02:57 2005 +0100 (2005-12-21)
changeset 18447da548623916a
parent 18446 6c558efcc754
child 18448 6e805f389355
removed or modified some instances of [iff]
src/HOL/Bali/Basis.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Bali/Example.thy
src/HOL/Bali/State.thy
src/HOL/Bali/Table.thy
src/HOL/Bali/TypeRel.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Datatype.thy
src/HOL/Hoare/SepLogHeap.thy
src/HOL/Hoare/Separation.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/IMP/Transition.thy
src/HOL/IMPP/Hoare.ML
src/HOL/Induct/QuoNestedDataType.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/List.thy
src/HOL/Map.thy
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/J/JBasis.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/Set.thy
src/HOL/Unix/Unix.thy
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Tue Dec 20 22:06:00 2005 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Wed Dec 21 12:02:57 2005 +0100
     1.3 @@ -28,7 +28,9 @@
     1.4  change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac));
     1.5  *}
     1.6  declare if_weak_cong [cong del] option.weak_case_cong [cong del]
     1.7 -declare length_Suc_conv [iff];
     1.8 +declare length_Suc_conv [iff]
     1.9 +
    1.10 +declare not_None_eq [iff]
    1.11  
    1.12  (*###to be phased out *)
    1.13  ML {*
     2.1 --- a/src/HOL/Bali/Decl.thy	Tue Dec 20 22:06:00 2005 +0100
     2.2 +++ b/src/HOL/Bali/Decl.thy	Wed Dec 21 12:02:57 2005 +0100
     2.3 @@ -636,8 +636,9 @@
     2.4  apply (erule make_imp)
     2.5  apply (rule subint1_induct)
     2.6  apply  assumption
     2.7 +apply (simp (no_asm)) 
     2.8  apply safe
     2.9 -apply (fast dest: subint1I ws_prog_ideclD)
    2.10 +apply (blast dest: subint1I ws_prog_ideclD)
    2.11  done
    2.12  
    2.13  
    2.14 @@ -649,6 +650,7 @@
    2.15  apply (erule make_imp)
    2.16  apply (rule subcls1_induct)
    2.17  apply  assumption
    2.18 +apply (simp (no_asm)) 
    2.19  apply safe
    2.20  apply (fast dest: subcls1I ws_prog_cdeclD)
    2.21  done
    2.22 @@ -673,7 +675,7 @@
    2.23        case True with iscls init show "P C" by auto
    2.24      next
    2.25        case False with ws step hyp iscls 
    2.26 -      show "P C" by (auto dest: subcls1I ws_prog_cdeclD)
    2.27 +      show "P C" by (auto iff: not_None_eq dest: subcls1I ws_prog_cdeclD)
    2.28      qed
    2.29    qed
    2.30    with clsC show ?thesis by simp
    2.31 @@ -684,7 +686,7 @@
    2.32    \<And> co. class G Object = Some co \<Longrightarrow> P Object; 
    2.33    \<And> C c. \<lbrakk>class G C = Some c; C \<noteq> Object; P (super c)\<rbrakk> \<Longrightarrow> P C
    2.34   \<rbrakk> \<Longrightarrow> P C"
    2.35 -by (blast intro: ws_class_induct)
    2.36 +by (auto intro: ws_class_induct)
    2.37  
    2.38  lemma ws_class_induct'' [consumes 2, case_names Object Subcls]:
    2.39  "\<lbrakk>class G C = Some c; ws_prog G; 
    2.40 @@ -710,7 +712,7 @@
    2.41        case False
    2.42        with ws iscls obtain sc where
    2.43  	sc: "class G (super c) = Some sc"
    2.44 -	by (auto dest: ws_prog_cdeclD)
    2.45 +	by (auto iff: not_None_eq dest: ws_prog_cdeclD)
    2.46        from iscls False have "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 (super c)" by (rule subcls1I)
    2.47        with False ws step hyp iscls sc
    2.48        show "P C c" 
     3.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Tue Dec 20 22:06:00 2005 +0100
     3.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed Dec 21 12:02:57 2005 +0100
     3.3 @@ -3381,7 +3381,7 @@
     3.4          proof -
     3.5            from normal_s3 s3
     3.6            have "normal (x1,s1)"
     3.7 -            by (cases s2) (simp add: abrupt_if_def)
     3.8 +            by (cases s2) (simp add: abrupt_if_def not_Some_eq)
     3.9            with normal_s3 nrmAss_C1 s3 s1_s2
    3.10            show ?thesis
    3.11              by fastsimp
     4.1 --- a/src/HOL/Bali/Example.thy	Tue Dec 20 22:06:00 2005 +0100
     4.2 +++ b/src/HOL/Bali/Example.thy	Wed Dec 21 12:02:57 2005 +0100
     4.3 @@ -1018,7 +1018,7 @@
     4.4    "Ball (set standard_classes) (wf_cdecl tprg)"
     4.5  apply (unfold standard_classes_def Let_def 
     4.6         ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def)
     4.7 -apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
     4.8 +apply (simp (no_asm) add: wf_cdecl_def ws_cdecls not_Some_eq)
     4.9  apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def 
    4.10              intro: da.Skip)
    4.11  apply (auto simp add: Object_def Classes_def standard_classes_def 
     5.1 --- a/src/HOL/Bali/State.thy	Tue Dec 20 22:06:00 2005 +0100
     5.2 +++ b/src/HOL/Bali/State.thy	Wed Dec 21 12:02:57 2005 +0100
     5.3 @@ -268,11 +268,8 @@
     5.4   "new_Addr h   \<equiv> if (\<forall>a. h a \<noteq> None) then None else Some (SOME a. h a = None)"
     5.5  
     5.6  lemma new_AddrD: "new_Addr h = Some a \<Longrightarrow> h a = None"
     5.7 -apply (unfold new_Addr_def)
     5.8 -apply auto
     5.9 -apply (case_tac "h (SOME a\<Colon>loc. h a = None)")
    5.10 -apply simp
    5.11 -apply (fast intro: someI2)
    5.12 +apply (auto simp add: not_Some_eq new_Addr_def)
    5.13 +apply (erule someI) 
    5.14  done
    5.15  
    5.16  lemma new_AddrD2: "new_Addr h = Some a \<Longrightarrow> \<forall>b. h b \<noteq> None \<longrightarrow> b \<noteq> a"
    5.17 @@ -281,12 +278,8 @@
    5.18  done
    5.19  
    5.20  lemma new_Addr_SomeI: "h a = None \<Longrightarrow> \<exists>b. new_Addr h = Some b \<and> h b = None"
    5.21 -apply (unfold new_Addr_def)
    5.22 -apply (frule not_Some_eq [THEN iffD2])
    5.23 -apply auto
    5.24 -apply  (drule not_Some_eq [THEN iffD2])
    5.25 -apply  auto
    5.26 -apply (fast intro!: someI2)
    5.27 +apply (simp add: new_Addr_def not_Some_eq)
    5.28 +apply (fast intro: someI2)
    5.29  done
    5.30  
    5.31  
     6.1 --- a/src/HOL/Bali/Table.thy	Tue Dec 20 22:06:00 2005 +0100
     6.2 +++ b/src/HOL/Bali/Table.thy	Wed Dec 21 12:02:57 2005 +0100
     6.3 @@ -206,10 +206,7 @@
     6.4  
     6.5  lemma set_get_eq: 
     6.6    "unique l \<Longrightarrow> (k, the (table_of l k)) \<in> set l = (table_of l k \<noteq> None)"
     6.7 -apply safe
     6.8 -apply (fast dest!: weak_map_of_SomeI)
     6.9 -apply auto
    6.10 -done
    6.11 +by (auto dest!: weak_map_of_SomeI)
    6.12  
    6.13  lemma inj_Pair_const2: "inj (\<lambda>k. (k, C))"
    6.14  apply (rule inj_onI)
     7.1 --- a/src/HOL/Bali/TypeRel.thy	Tue Dec 20 22:06:00 2005 +0100
     7.2 +++ b/src/HOL/Bali/TypeRel.thy	Wed Dec 21 12:02:57 2005 +0100
     7.3 @@ -393,7 +393,7 @@
     7.4  
     7.5  lemma implmt_is_class: "G\<turnstile>C\<leadsto>I \<Longrightarrow> is_class G C"
     7.6  apply (erule implmt.induct)
     7.7 -apply (blast dest: implmt1D subcls1D)+
     7.8 +apply (auto dest: implmt1D subcls1D)
     7.9  done
    7.10  
    7.11  
     8.1 --- a/src/HOL/Bali/TypeSafe.thy	Tue Dec 20 22:06:00 2005 +0100
     8.2 +++ b/src/HOL/Bali/TypeSafe.thy	Wed Dec 21 12:02:57 2005 +0100
     8.3 @@ -1466,7 +1466,7 @@
     8.4        next
     8.5  	case (VNam vn)
     8.6  	with EName el_in_list show ?thesis 
     8.7 -	  by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
     8.8 +	  by (auto simp add: not_Some_eq dom_def dest: map_upds_cut_irrelevant)
     8.9        qed
    8.10      qed
    8.11    qed
     9.1 --- a/src/HOL/Datatype.thy	Tue Dec 20 22:06:00 2005 +0100
     9.2 +++ b/src/HOL/Datatype.thy	Wed Dec 21 12:02:57 2005 +0100
     9.3 @@ -140,11 +140,19 @@
     9.4  
     9.5  datatype 'a option = None | Some 'a
     9.6  
     9.7 -lemma not_None_eq [iff]: "(x ~= None) = (EX y. x = Some y)"
     9.8 +lemma not_None_eq: "(x ~= None) = (EX y. x = Some y)"
     9.9 +  by (induct x) auto
    9.10 +
    9.11 +lemma not_Some_eq: "(ALL y. x ~= Some y) = (x = None)"
    9.12    by (induct x) auto
    9.13  
    9.14 -lemma not_Some_eq [iff]: "(ALL y. x ~= Some y) = (x = None)"
    9.15 -  by (induct x) auto
    9.16 +text{*Both of these equalities are helpful only when applied to assumptions.*}
    9.17 +
    9.18 +lemmas not_None_eq_D = not_None_eq [THEN iffD1]
    9.19 +declare not_None_eq_D [dest!]
    9.20 +
    9.21 +lemmas not_Some_eq_D = not_Some_eq [THEN iffD1]
    9.22 +declare not_Some_eq_D [dest!]
    9.23  
    9.24  lemma option_caseE:
    9.25    "(case x of None => P | Some y => Q y) ==>
    10.1 --- a/src/HOL/Hoare/SepLogHeap.thy	Tue Dec 20 22:06:00 2005 +0100
    10.2 +++ b/src/HOL/Hoare/SepLogHeap.thy	Wed Dec 21 12:02:57 2005 +0100
    10.3 @@ -9,6 +9,8 @@
    10.4  
    10.5  theory SepLogHeap imports Main begin
    10.6  
    10.7 +declare not_None_eq [iff]
    10.8 +
    10.9  types heap = "(nat \<Rightarrow> nat option)"
   10.10  
   10.11  text{* @{text "Some"} means allocated, @{text "None"} means
   10.12 @@ -86,6 +88,7 @@
   10.13   "\<And>p. \<lbrakk> List h1 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
   10.14  by (induct ps) (auto simp add:map_add_def split:option.split)
   10.15  
   10.16 +
   10.17  lemma list_ortho_sum2[simp]:
   10.18   "\<And>p. \<lbrakk> List h2 p ps; dom h1 \<inter> dom h2 = {}\<rbrakk> \<Longrightarrow> List (h1++h2) p ps"
   10.19  by (induct ps) (auto simp add:map_add_def split:option.split)
    11.1 --- a/src/HOL/Hoare/Separation.thy	Tue Dec 20 22:06:00 2005 +0100
    11.2 +++ b/src/HOL/Hoare/Separation.thy	Wed Dec 21 12:02:57 2005 +0100
    11.3 @@ -159,9 +159,7 @@
    11.4  
    11.5  (* a law of separation logic *)
    11.6  lemma star_comm: "P ** Q = Q ** P"
    11.7 -apply(simp add:star_def ortho_def)
    11.8 -apply(blast intro:map_add_comm)
    11.9 -done
   11.10 +  by(auto simp add:star_def ortho_def dest: map_add_comm)
   11.11  
   11.12  lemma "VARS H x y z w
   11.13   {P ** Q}
    12.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Tue Dec 20 22:06:00 2005 +0100
    12.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed Dec 21 12:02:57 2005 +0100
    12.3 @@ -5,6 +5,8 @@
    12.4  subsection {* Proof System for Component Programs *}
    12.5  
    12.6  declare Un_subset_iff [iff del]
    12.7 +declare not_None_eq [iff]
    12.8 +declare Cons_eq_map_conv[iff]
    12.9  
   12.10  constdefs
   12.11    stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool"  
    13.1 --- a/src/HOL/IMP/Transition.thy	Tue Dec 20 22:06:00 2005 +0100
    13.2 +++ b/src/HOL/IMP/Transition.thy	Wed Dec 21 12:02:57 2005 +0100
    13.3 @@ -672,9 +672,7 @@
    13.4  lemma FB_lemma2:
    13.5    "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<Longrightarrow>
    13.6     \<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"
    13.7 -  apply (induct rule: converse_rtrancl_induct2)
    13.8 -   apply simp
    13.9 -  apply clarsimp
   13.10 +  apply (induct rule: converse_rtrancl_induct2, force)
   13.11    apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
   13.12    done
   13.13  
    14.1 --- a/src/HOL/IMPP/Hoare.ML	Tue Dec 20 22:06:00 2005 +0100
    14.2 +++ b/src/HOL/IMPP/Hoare.ML	Wed Dec 21 12:02:57 2005 +0100
    14.3 @@ -220,6 +220,7 @@
    14.4  qed "MGF_complete";
    14.5  
    14.6  AddSEs WTs_elim_cases;
    14.7 +AddIffs [not_None_eq];
    14.8  (* requires com_det, escape (i.e. hoare_derivs.conseq) *)
    14.9  Goal "state_not_singleton ==> \
   14.10  \ !pn:dom body. G|-{=}.BODY pn.{->} ==> WT c --> G|-{=}.c.{->}";
    15.1 --- a/src/HOL/Induct/QuoNestedDataType.thy	Tue Dec 20 22:06:00 2005 +0100
    15.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy	Wed Dec 21 12:02:57 2005 +0100
    15.3 @@ -222,7 +222,7 @@
    15.4  lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us"
    15.5  apply (induct z)
    15.6  apply (rule_tac [2] z=a in eq_Abs_Exp)
    15.7 -apply (auto simp add: Abs_ExpList_def intro: exprel_refl)
    15.8 +apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv intro: exprel_refl)
    15.9  done
   15.10  
   15.11  lemma eq_Abs_ExpList [case_names Abs_ExpList]:
    16.1 --- a/src/HOL/Library/Nested_Environment.thy	Tue Dec 20 22:06:00 2005 +0100
    16.2 +++ b/src/HOL/Library/Nested_Environment.thy	Wed Dec 21 12:02:57 2005 +0100
    16.3 @@ -193,7 +193,7 @@
    16.4    from prems have "lookup env (xs @ ys) \<noteq> None" by simp
    16.5    then have "lookup env xs \<noteq> None"
    16.6      by (rule contrapos_nn) (simp only: lookup_append_none)
    16.7 -  then show ?thesis by simp
    16.8 +  then show ?thesis by (simp add: not_None_eq)
    16.9  qed
   16.10  
   16.11  text {*
    17.1 --- a/src/HOL/List.thy	Tue Dec 20 22:06:00 2005 +0100
    17.2 +++ b/src/HOL/List.thy	Wed Dec 21 12:02:57 2005 +0100
    17.3 @@ -505,17 +505,21 @@
    17.4  lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
    17.5  by (cases xs) auto
    17.6  
    17.7 -lemma map_eq_Cons_conv[iff]:
    17.8 +lemma map_eq_Cons_conv:
    17.9   "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
   17.10  by (cases xs) auto
   17.11  
   17.12 -lemma Cons_eq_map_conv[iff]:
   17.13 +lemma Cons_eq_map_conv:
   17.14   "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
   17.15  by (cases ys) auto
   17.16  
   17.17 +lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]
   17.18 +lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]
   17.19 +declare map_eq_Cons_D [dest!]  Cons_eq_map_D [dest!]
   17.20 +
   17.21  lemma ex_map_conv:
   17.22    "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
   17.23 -by(induct ys, auto)
   17.24 +by(induct ys, auto simp add: Cons_eq_map_conv)
   17.25  
   17.26  lemma map_eq_imp_length_eq:
   17.27    "!!xs. map f xs = map f ys ==> length xs = length ys"
   17.28 @@ -867,10 +871,10 @@
   17.29  lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
   17.30  by (induct xs) auto
   17.31  
   17.32 -lemma concat_eq_Nil_conv [iff]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
   17.33 +lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
   17.34  by (induct xss) auto
   17.35  
   17.36 -lemma Nil_eq_concat_conv [iff]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
   17.37 +lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
   17.38  by (induct xss) auto
   17.39  
   17.40  lemma set_concat [simp]: "set (concat xs) = \<Union>(set ` set xs)"
   17.41 @@ -2238,8 +2242,8 @@
   17.42  by (induct xs) simp_all
   17.43  
   17.44  lemma filtermap_conv:
   17.45 - "filtermap f xs = map (%x. the(f x)) (filter (%x. f x \<noteq> None) xs)"
   17.46 -by (induct xs) auto
   17.47 +     "filtermap f xs = map (%x. the(f x)) (filter (%x. f x \<noteq> None) xs)"
   17.48 +  by (induct xs) (simp_all split: option.split) 
   17.49  
   17.50  lemma map_filter_conv[simp]: "map_filter f P xs = map f (filter P xs)"
   17.51  by (induct xs) auto
   17.52 @@ -2388,7 +2392,7 @@
   17.53  lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
   17.54  by (simp add:lex_conv)
   17.55  
   17.56 -lemma Cons_in_lex [iff]:
   17.57 +lemma Cons_in_lex [simp]:
   17.58      "((x # xs, y # ys) : lex r) =
   17.59        ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
   17.60  apply (simp add: lex_conv)
    18.1 --- a/src/HOL/Map.thy	Tue Dec 20 22:06:00 2005 +0100
    18.2 +++ b/src/HOL/Map.thy	Wed Dec 21 12:02:57 2005 +0100
    18.3 @@ -478,7 +478,9 @@
    18.4  (* declare domI [intro]? *)
    18.5  
    18.6  lemma domD: "a : dom m ==> \<exists>b. m a = Some b"
    18.7 -by (unfold dom_def, auto)
    18.8 +apply (case_tac "m a") 
    18.9 +apply (auto simp add: dom_def) 
   18.10 +done
   18.11  
   18.12  lemma domIff[iff]: "(a : dom m) = (m a ~= None)"
   18.13  by (unfold dom_def, auto)
   18.14 @@ -528,7 +530,7 @@
   18.15  
   18.16  lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
   18.17  apply(rule ext)
   18.18 -apply(fastsimp simp:map_add_def split:option.split)
   18.19 +apply(force simp: map_add_def dom_def not_None_eq  split:option.split) 
   18.20  done
   18.21  
   18.22  subsection {* @{term [source] ran} *}
   18.23 @@ -575,7 +577,7 @@
   18.24    by (simp add: map_le_def)
   18.25  
   18.26  lemma map_le_trans[trans]: "\<lbrakk> m1 \<subseteq>\<^sub>m m2; m2 \<subseteq>\<^sub>m m3\<rbrakk> \<Longrightarrow> m1 \<subseteq>\<^sub>m m3"
   18.27 -by(force simp add:map_le_def)
   18.28 +  by (auto simp add: map_le_def dom_def)
   18.29  
   18.30  lemma map_le_antisym: "\<lbrakk> f \<subseteq>\<^sub>m g; g \<subseteq>\<^sub>m f \<rbrakk> \<Longrightarrow> f = g"
   18.31    apply (unfold map_le_def)
   18.32 @@ -585,13 +587,13 @@
   18.33  done
   18.34  
   18.35  lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
   18.36 -  by (fastsimp simp add: map_le_def)
   18.37 +  by (fastsimp simp add: map_le_def not_None_eq)
   18.38  
   18.39  lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
   18.40  by(fastsimp simp add:map_add_def map_le_def expand_fun_eq split:option.splits)
   18.41  
   18.42  lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
   18.43 -by (fastsimp simp add: map_le_def map_add_def dom_def)
   18.44 +by (fastsimp simp add: map_le_def map_add_def dom_def not_None_eq)
   18.45  
   18.46  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"
   18.47  by (clarsimp simp add: map_le_def map_add_def dom_def split:option.splits)
    19.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Tue Dec 20 22:06:00 2005 +0100
    19.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Dec 21 12:02:57 2005 +0100
    19.3 @@ -208,7 +208,8 @@
    19.4    "C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow> 
    19.5    \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"
    19.6    apply (cases i)
    19.7 -  apply (auto dest!: match_any_match_table match_X_match_table 
    19.8 +  apply (auto iff: not_None_eq
    19.9 +	      dest!: match_any_match_table match_X_match_table 
   19.10                dest: match_exception_table_in_et)
   19.11    done
   19.12  
    20.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Tue Dec 20 22:06:00 2005 +0100
    20.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Wed Dec 21 12:02:57 2005 +0100
    20.3 @@ -12,6 +12,7 @@
    20.4  theory JBasis imports Main begin 
    20.5  
    20.6  lemmas [simp] = Let_def
    20.7 +declare not_None_eq [iff]
    20.8  
    20.9  section "unique"
   20.10   
    21.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Tue Dec 20 22:06:00 2005 +0100
    21.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Dec 21 12:02:57 2005 +0100
    21.3 @@ -44,7 +44,7 @@
    21.4  lemma subcls1_def2: 
    21.5    "subcls1 G = 
    21.6       (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
    21.7 -  by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
    21.8 +  by (auto simp add: is_class_def not_None_eq dest: subcls1D intro: subcls1I)
    21.9  
   21.10  lemma finite_subcls1: "finite (subcls1 G)"
   21.11  apply(subst subcls1_def2)
    22.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Tue Dec 20 22:06:00 2005 +0100
    22.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Dec 21 12:02:57 2005 +0100
    22.3 @@ -123,9 +123,7 @@
    22.4  done
    22.5  
    22.6  lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object"
    22.7 -apply (unfold is_class_def)
    22.8 -apply (simp (no_asm_simp))
    22.9 -done
   22.10 +  by (simp add: is_class_def not_None_eq)
   22.11  
   22.12  lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)"
   22.13    apply (simp add: ws_prog_def wf_syscls_def)
   22.14 @@ -213,7 +211,7 @@
   22.15  apply( rule impI)
   22.16  apply( case_tac "C = Object")
   22.17  apply(  fast)
   22.18 -apply safe
   22.19 +apply auto
   22.20  apply( frule (1) class_wf) apply (erule conjE)+
   22.21  apply (frule wf_cdecl_ws_cdecl)
   22.22  apply( frule (1) wf_cdecl_supD)
   22.23 @@ -263,7 +261,7 @@
   22.24  apply( rule impI)
   22.25  apply( case_tac "C = Object")
   22.26  apply(  fast)
   22.27 -apply safe
   22.28 +apply auto
   22.29  apply( frule (1) class_wf_struct)
   22.30  apply( frule (1) wf_cdecl_supD)
   22.31  
    23.1 --- a/src/HOL/Set.thy	Tue Dec 20 22:06:00 2005 +0100
    23.2 +++ b/src/HOL/Set.thy	Wed Dec 21 12:02:57 2005 +0100
    23.3 @@ -1452,10 +1452,10 @@
    23.4  lemma Union_Int_subset: "\<Union>(A \<inter> B) \<subseteq> \<Union>A \<inter> \<Union>B"
    23.5    by blast
    23.6  
    23.7 -lemma Union_empty_conv [iff]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
    23.8 +lemma Union_empty_conv [simp]: "(\<Union>A = {}) = (\<forall>x\<in>A. x = {})"
    23.9    by blast
   23.10  
   23.11 -lemma empty_Union_conv [iff]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
   23.12 +lemma empty_Union_conv [simp]: "({} = \<Union>A) = (\<forall>x\<in>A. x = {})"
   23.13    by blast
   23.14  
   23.15  lemma Union_disjoint: "(\<Union>C \<inter> A = {}) = (\<forall>B\<in>C. B \<inter> A = {})"
   23.16 @@ -1479,7 +1479,7 @@
   23.17  lemma Inter_Un_distrib: "\<Inter>(A \<union> B) = \<Inter>A \<inter> \<Inter>B"
   23.18    by blast
   23.19  
   23.20 -lemma Inter_UNIV_conv [iff]:
   23.21 +lemma Inter_UNIV_conv [simp]:
   23.22    "(\<Inter>A = UNIV) = (\<forall>x\<in>A. x = UNIV)"
   23.23    "(UNIV = \<Inter>A) = (\<forall>x\<in>A. x = UNIV)"
   23.24    by blast+
   23.25 @@ -1555,12 +1555,12 @@
   23.26    -- {* Look: it has an \emph{existential} quantifier *}
   23.27    by blast
   23.28  
   23.29 -lemma UNION_empty_conv[iff]:
   23.30 +lemma UNION_empty_conv[simp]:
   23.31    "({} = (UN x:A. B x)) = (\<forall>x\<in>A. B x = {})"
   23.32    "((UN x:A. B x) = {}) = (\<forall>x\<in>A. B x = {})"
   23.33  by blast+
   23.34  
   23.35 -lemma INTER_UNIV_conv[iff]:
   23.36 +lemma INTER_UNIV_conv[simp]:
   23.37   "(UNIV = (INT x:A. B x)) = (\<forall>x\<in>A. B x = UNIV)"
   23.38   "((INT x:A. B x) = UNIV) = (\<forall>x\<in>A. B x = UNIV)"
   23.39  by blast+
   23.40 @@ -1790,7 +1790,7 @@
   23.41  lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
   23.42    by (unfold psubset_def) blast
   23.43  
   23.44 -lemma all_not_in_conv [iff]: "(\<forall>x. x \<notin> A) = (A = {})"
   23.45 +lemma all_not_in_conv [simp]: "(\<forall>x. x \<notin> A) = (A = {})"
   23.46    by blast
   23.47  
   23.48  lemma ex_in_conv: "(\<exists>x. x \<in> A) = (A \<noteq> {})"
    24.1 --- a/src/HOL/Unix/Unix.thy	Tue Dec 20 22:06:00 2005 +0100
    24.2 +++ b/src/HOL/Unix/Unix.thy	Wed Dec 21 12:02:57 2005 +0100
    24.3 @@ -1058,7 +1058,8 @@
    24.4                have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
    24.5                    lookup root ((path @ [y]) @ us) \<noteq> None"
    24.6                  by cases (auto dest: access_some_lookup)
    24.7 -              then show ?thesis by (blast dest!: lookup_some_append)
    24.8 +              then show ?thesis 
    24.9 +                by (simp add: not_None_eq, blast dest!: lookup_some_append)
   24.10              qed
   24.11              finally show ?thesis .
   24.12            qed
    25.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Tue Dec 20 22:06:00 2005 +0100
    25.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Dec 21 12:02:57 2005 +0100
    25.3 @@ -12,6 +12,8 @@
    25.4  imports Main
    25.5  begin
    25.6  
    25.7 +declare not_Some_eq [iff]
    25.8 +
    25.9  (* Shadow syntax for integer terms *)
   25.10  datatype intterm =
   25.11      Cst int
   25.12 @@ -968,7 +970,7 @@
   25.13      moreover 
   25.14      {
   25.15        assume lini: "\<exists>li. linearize i = Some li"
   25.16 -      from lini have lini2: "linearize i \<noteq> None" by simp
   25.17 +      from lini have lini2: "linearize i \<noteq> None" by auto
   25.18        from lini obtain "li" where  "linearize i = Some li" by blast
   25.19        from lini2 lini have "islinintterm (the (linearize i))"
   25.20  	by (simp add: linearize_linear1[OF lini2])
   25.21 @@ -1001,8 +1003,8 @@
   25.22      {
   25.23        assume lini: "\<exists>li. linearize i = Some li"
   25.24  	and linj: "\<exists>lj. linearize j = Some lj"
   25.25 -      from lini have lini2: "linearize i \<noteq> None" by simp
   25.26 -      from linj have linj2: "linearize j \<noteq> None" by simp
   25.27 +      from lini have lini2: "linearize i \<noteq> None" by auto
   25.28 +      from linj have linj2: "linearize j \<noteq> None" by auto
   25.29        from lini obtain "li" where  "linearize i = Some li" by blast
   25.30        from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
   25.31        then have linli: "islinintterm li" using prems by simp
   25.32 @@ -1036,8 +1038,8 @@
   25.33      {
   25.34        assume lini: "\<exists>li. linearize i = Some li"
   25.35  	and linj: "\<exists>lj. linearize j = Some lj"
   25.36 -      from lini have lini2: "linearize i \<noteq> None" by simp
   25.37 -      from linj have linj2: "linearize j \<noteq> None" by simp
   25.38 +      from lini have lini2: "linearize i \<noteq> None" by auto
   25.39 +      from linj have linj2: "linearize j \<noteq> None" by auto
   25.40        from lini obtain "li" where  "linearize i = Some li" by blast
   25.41        from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
   25.42        with prems have linli: "islinintterm li" by simp
   25.43 @@ -1081,7 +1083,7 @@
   25.44      {
   25.45        assume lini: "\<exists>li. linearize i = Some li"
   25.46  	and linj: "\<exists>bj. linearize j = Some (Cst bj)"
   25.47 -      from lini have lini2: "linearize i \<noteq> None" by simp
   25.48 +      from lini have lini2: "linearize i \<noteq> None" by auto
   25.49        from linj have linj2: "linearize j \<noteq> None" by auto
   25.50        from lini obtain "li" where  "linearize i = Some li" by blast
   25.51        from lini2 have "islinintterm (the (linearize i))" by (simp add: linearize_linear1)
   25.52 @@ -1143,7 +1145,7 @@
   25.53  qed  simp_all
   25.54  
   25.55  
   25.56 -(* linearize, when successfull, preserves semantics *)
   25.57 +(* linearize, when successful, preserves semantics *)
   25.58  lemma linearize_corr: "\<And> t'. linearize t = Some t' \<Longrightarrow> I_intterm ats t = I_intterm ats t' "
   25.59  proof-
   25.60    fix t'
   25.61 @@ -1612,7 +1614,7 @@
   25.62  qed (simp_all)
   25.63  
   25.64  
   25.65 -(* linform, if successfull, preserves quantifier freeness *)
   25.66 +(* linform, if successful, preserves quantifier freeness *)
   25.67  lemma linform_isnnf: "islinform p \<Longrightarrow> isnnf p"
   25.68  by (induct p rule: islinform.induct) auto
   25.69