Reversed Larry's option/iff change.
--- 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)
--- 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\<turnstile>C \<prec>\<^sub>C\<^sub>1 (super c)" by (rule subcls1I)
with False ws step hyp iscls sc
show "P C c"
--- 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
--- 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
--- 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 \<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 (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 \<Longrightarrow> \<exists>b. new_Addr h = Some b \<and> h b = None"
-apply (simp add: new_Addr_def not_Some_eq)
+apply (simp add: new_Addr_def)
apply (fast intro: someI2)
done
--- 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
--- 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) ==>
--- 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 \<Rightarrow> nat option)"
--- 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
--- 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) \<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 add: not_None_eq)
+ then show ?thesis by (simp)
qed
text {*
--- 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 \<inter> dom m2 = {} \<Longrightarrow> 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 \<subseteq>\<^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 \<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 not_None_eq)
+by (fastsimp simp add: map_le_def map_add_def dom_def)
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)
--- 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 \<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 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
--- 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"
--- 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\<noteq>Object \<and> 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)
--- 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 \<Longrightarrow> is_class G (Xcpt x)"
apply (simp add: ws_prog_def wf_syscls_def)
--- 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) \<noteq> 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
--- 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