# HG changeset patch # User nipkow # Date 1136398973 -3600 # Node ID 8d98b7711e473a3fb8fb9ce5f6fa039899a12b5a # Parent 9ccfd1d1e874d5507c5b519e28f2d512c49284a6 Reversed Larry's option/iff change. diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Bali/Basis.thy Wed Jan 04 19:22:53 2006 +0100 @@ -30,8 +30,6 @@ declare if_weak_cong [cong del] option.weak_case_cong [cong del] declare length_Suc_conv [iff] -declare not_None_eq [iff] - (*###to be phased out *) ML {* bind_thm ("make_imp", rearrange_prems [1,0] mp) diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Bali/Decl.thy --- a/src/HOL/Bali/Decl.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Bali/Decl.thy Wed Jan 04 19:22:53 2006 +0100 @@ -675,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 iff: not_None_eq dest: subcls1I ws_prog_cdeclD) + show "P C" by (auto dest: subcls1I ws_prog_cdeclD) qed qed with clsC show ?thesis by simp @@ -712,7 +712,7 @@ case False with ws iscls obtain sc where sc: "class G (super c) = Some sc" - by (auto iff: not_None_eq dest: ws_prog_cdeclD) + by (auto dest: ws_prog_cdeclD) from iscls False have "G\C \\<^sub>C\<^sub>1 (super c)" by (rule subcls1I) with False ws step hyp iscls sc show "P C c" diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Bali/DefiniteAssignmentCorrect.thy --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy Wed Jan 04 19:22:53 2006 +0100 @@ -3381,7 +3381,7 @@ proof - from normal_s3 s3 have "normal (x1,s1)" - by (cases s2) (simp add: abrupt_if_def not_Some_eq) + by (cases s2) (simp add: abrupt_if_def) with normal_s3 nrmAss_C1 s3 s1_s2 show ?thesis by fastsimp diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Bali/Example.thy Wed Jan 04 19:22:53 2006 +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 not_Some_eq) +apply (simp (no_asm) add: wf_cdecl_def ws_cdecls) 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 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Bali/State.thy --- a/src/HOL/Bali/State.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Bali/State.thy Wed Jan 04 19:22:53 2006 +0100 @@ -268,7 +268,7 @@ "new_Addr h \ if (\a. h a \ None) then None else Some (SOME a. h a = None)" lemma new_AddrD: "new_Addr h = Some a \ h a = None" -apply (auto simp add: not_Some_eq new_Addr_def) +apply (auto simp add: new_Addr_def) apply (erule someI) done @@ -278,7 +278,7 @@ done lemma new_Addr_SomeI: "h a = None \ \b. new_Addr h = Some b \ h b = None" -apply (simp add: new_Addr_def not_Some_eq) +apply (simp add: new_Addr_def) apply (fast intro: someI2) done diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Bali/TypeSafe.thy --- a/src/HOL/Bali/TypeSafe.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Bali/TypeSafe.thy Wed Jan 04 19:22:53 2006 +0100 @@ -1466,7 +1466,7 @@ next case (VNam vn) with EName el_in_list show ?thesis - by (auto simp add: not_Some_eq dom_def dest: map_upds_cut_irrelevant) + by (auto simp add: dom_def dest: map_upds_cut_irrelevant) qed qed qed diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Datatype.thy Wed Jan 04 19:22:53 2006 +0100 @@ -140,19 +140,23 @@ datatype 'a option = None | Some 'a -lemma not_None_eq: "(x ~= None) = (EX y. x = Some y)" +lemma not_None_eq[iff]: "(x ~= None) = (EX y. x = Some y)" + by (induct x) auto + +lemma not_Some_eq[iff]: "(ALL y. x ~= Some y) = (x = None)" by (induct x) auto -lemma not_Some_eq: "(ALL y. x ~= Some y) = (x = None)" - by (induct x) auto +text{*Although it may appear that both of these equalities are helpful +only when applied to assumptions, in practice it seems better to give +them the uniform iff attribute. *} -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 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Hoare/SepLogHeap.thy --- a/src/HOL/Hoare/SepLogHeap.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Hoare/SepLogHeap.thy Wed Jan 04 19:22:53 2006 +0100 @@ -7,9 +7,9 @@ for Separation Logic. *) -theory SepLogHeap imports Main begin - -declare not_None_eq [iff] +theory SepLogHeap +imports Main +begin types heap = "(nat \ nat option)" diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/HoareParallel/RG_Hoare.thy --- a/src/HOL/HoareParallel/RG_Hoare.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/HoareParallel/RG_Hoare.thy Wed Jan 04 19:22:53 2006 +0100 @@ -5,7 +5,6 @@ subsection {* Proof System for Component Programs *} declare Un_subset_iff [iff del] -declare not_None_eq [iff] declare Cons_eq_map_conv[iff] constdefs diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Library/Nested_Environment.thy --- a/src/HOL/Library/Nested_Environment.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Library/Nested_Environment.thy Wed Jan 04 19:22:53 2006 +0100 @@ -193,7 +193,7 @@ from prems have "lookup env (xs @ ys) \ None" by simp then have "lookup env xs \ None" by (rule contrapos_nn) (simp only: lookup_append_none) - then show ?thesis by (simp add: not_None_eq) + then show ?thesis by (simp) qed text {* diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Map.thy --- a/src/HOL/Map.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Map.thy Wed Jan 04 19:22:53 2006 +0100 @@ -530,7 +530,7 @@ lemma map_add_comm: "dom m1 \ dom m2 = {} \ m1++m2 = m2++m1" apply(rule ext) -apply(force simp: map_add_def dom_def not_None_eq split:option.split) +apply(force simp: map_add_def dom_def split:option.split) done subsection {* @{term [source] ran} *} @@ -587,13 +587,13 @@ done lemma map_le_map_add [simp]: "f \\<^sub>m (g ++ f)" - by (fastsimp simp add: map_le_def not_None_eq) + by (fastsimp simp add: map_le_def) lemma map_le_iff_map_add_commute: "(f \\<^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 \\<^sub>m h \ g \\<^sub>m h" -by (fastsimp simp add: map_le_def map_add_def dom_def not_None_eq) +by (fastsimp simp add: map_le_def map_add_def dom_def) lemma map_add_le_mapI: "\ f \\<^sub>m h; g \\<^sub>m h; f \\<^sub>m f++g \ \ f++g \\<^sub>m h" by (clarsimp simp add: map_le_def map_add_def dom_def split:option.splits) diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/MicroJava/BV/Effect.thy --- a/src/HOL/MicroJava/BV/Effect.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/MicroJava/BV/Effect.thy Wed Jan 04 19:22:53 2006 +0100 @@ -208,8 +208,7 @@ "C \ set (xcpt_names (i,G,pc,et)) \ \e \ set et. the (match_exception_table G C pc et) = fst (snd (snd e))" apply (cases i) - apply (auto iff: not_None_eq - dest!: match_any_match_table match_X_match_table + apply (auto dest!: match_any_match_table match_X_match_table dest: match_exception_table_in_et) done diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/MicroJava/J/JBasis.thy --- a/src/HOL/MicroJava/J/JBasis.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/MicroJava/J/JBasis.thy Wed Jan 04 19:22:53 2006 +0100 @@ -12,7 +12,6 @@ theory JBasis imports Main begin lemmas [simp] = Let_def -declare not_None_eq [iff] section "unique" diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/MicroJava/J/TypeRel.thy --- a/src/HOL/MicroJava/J/TypeRel.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/MicroJava/J/TypeRel.thy Wed Jan 04 19:22:53 2006 +0100 @@ -44,7 +44,7 @@ lemma subcls1_def2: "subcls1 G = (SIGMA C: {C. is_class G C} . {D. C\Object \ fst (the (class G C))=D})" - by (auto simp add: is_class_def not_None_eq dest: subcls1D intro: subcls1I) + by (auto simp add: is_class_def dest: subcls1D intro: subcls1I) lemma finite_subcls1: "finite (subcls1 G)" apply(subst subcls1_def2) diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/MicroJava/J/WellForm.thy --- a/src/HOL/MicroJava/J/WellForm.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/MicroJava/J/WellForm.thy Wed Jan 04 19:22:53 2006 +0100 @@ -123,7 +123,7 @@ done lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object" - by (simp add: is_class_def not_None_eq) + by (simp add: is_class_def) lemma is_class_xcpt [simp]: "ws_prog G \ is_class G (Xcpt x)" apply (simp add: ws_prog_def wf_syscls_def) diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/Unix/Unix.thy --- a/src/HOL/Unix/Unix.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/Unix/Unix.thy Wed Jan 04 19:22:53 2006 +0100 @@ -1059,7 +1059,7 @@ lookup root ((path @ [y]) @ us) \ None" by cases (auto dest: access_some_lookup) then show ?thesis - by (simp add: not_None_eq, blast dest!: lookup_some_append) + by (simp, blast dest!: lookup_some_append) qed finally show ?thesis . qed diff -r 9ccfd1d1e874 -r 8d98b7711e47 src/HOL/ex/Reflected_Presburger.thy --- a/src/HOL/ex/Reflected_Presburger.thy Wed Jan 04 17:04:11 2006 +0100 +++ b/src/HOL/ex/Reflected_Presburger.thy Wed Jan 04 19:22:53 2006 +0100 @@ -12,8 +12,6 @@ imports Main begin -declare not_Some_eq [iff] - (* Shadow syntax for integer terms *) datatype intterm = Cst int