Reversed Larry's option/iff change.
authornipkow
Wed Jan 04 19:22:53 2006 +0100 (2006-01-04)
changeset 185768d98b7711e47
parent 18575 9ccfd1d1e874
child 18577 a636846a02c7
Reversed Larry's option/iff change.
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/TypeSafe.thy
src/HOL/Datatype.thy
src/HOL/Hoare/SepLogHeap.thy
src/HOL/HoareParallel/RG_Hoare.thy
src/HOL/Library/Nested_Environment.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/Unix/Unix.thy
src/HOL/ex/Reflected_Presburger.thy
     1.1 --- a/src/HOL/Bali/Basis.thy	Wed Jan 04 17:04:11 2006 +0100
     1.2 +++ b/src/HOL/Bali/Basis.thy	Wed Jan 04 19:22:53 2006 +0100
     1.3 @@ -30,8 +30,6 @@
     1.4  declare if_weak_cong [cong del] option.weak_case_cong [cong del]
     1.5  declare length_Suc_conv [iff]
     1.6  
     1.7 -declare not_None_eq [iff]
     1.8 -
     1.9  (*###to be phased out *)
    1.10  ML {*
    1.11  bind_thm ("make_imp", rearrange_prems [1,0] mp)
     2.1 --- a/src/HOL/Bali/Decl.thy	Wed Jan 04 17:04:11 2006 +0100
     2.2 +++ b/src/HOL/Bali/Decl.thy	Wed Jan 04 19:22:53 2006 +0100
     2.3 @@ -675,7 +675,7 @@
     2.4        case True with iscls init show "P C" by auto
     2.5      next
     2.6        case False with ws step hyp iscls 
     2.7 -      show "P C" by (auto iff: not_None_eq dest: subcls1I ws_prog_cdeclD)
     2.8 +      show "P C" by (auto dest: subcls1I ws_prog_cdeclD)
     2.9      qed
    2.10    qed
    2.11    with clsC show ?thesis by simp
    2.12 @@ -712,7 +712,7 @@
    2.13        case False
    2.14        with ws iscls obtain sc where
    2.15  	sc: "class G (super c) = Some sc"
    2.16 -	by (auto iff: not_None_eq dest: ws_prog_cdeclD)
    2.17 +	by (auto dest: ws_prog_cdeclD)
    2.18        from iscls False have "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 (super c)" by (rule subcls1I)
    2.19        with False ws step hyp iscls sc
    2.20        show "P C c" 
     3.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed Jan 04 17:04:11 2006 +0100
     3.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Wed Jan 04 19:22:53 2006 +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 not_Some_eq)
     3.8 +            by (cases s2) (simp add: abrupt_if_def)
     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	Wed Jan 04 17:04:11 2006 +0100
     4.2 +++ b/src/HOL/Bali/Example.thy	Wed Jan 04 19:22:53 2006 +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 not_Some_eq)
     4.8 +apply (simp (no_asm) add: wf_cdecl_def ws_cdecls)
     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	Wed Jan 04 17:04:11 2006 +0100
     5.2 +++ b/src/HOL/Bali/State.thy	Wed Jan 04 19:22:53 2006 +0100
     5.3 @@ -268,7 +268,7 @@
     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 (auto simp add: not_Some_eq new_Addr_def)
     5.8 +apply (auto simp add: new_Addr_def)
     5.9  apply (erule someI) 
    5.10  done
    5.11  
    5.12 @@ -278,7 +278,7 @@
    5.13  done
    5.14  
    5.15  lemma new_Addr_SomeI: "h a = None \<Longrightarrow> \<exists>b. new_Addr h = Some b \<and> h b = None"
    5.16 -apply (simp add: new_Addr_def not_Some_eq)
    5.17 +apply (simp add: new_Addr_def)
    5.18  apply (fast intro: someI2)
    5.19  done
    5.20  
     6.1 --- a/src/HOL/Bali/TypeSafe.thy	Wed Jan 04 17:04:11 2006 +0100
     6.2 +++ b/src/HOL/Bali/TypeSafe.thy	Wed Jan 04 19:22:53 2006 +0100
     6.3 @@ -1466,7 +1466,7 @@
     6.4        next
     6.5  	case (VNam vn)
     6.6  	with EName el_in_list show ?thesis 
     6.7 -	  by (auto simp add: not_Some_eq dom_def dest: map_upds_cut_irrelevant)
     6.8 +	  by (auto simp add: dom_def dest: map_upds_cut_irrelevant)
     6.9        qed
    6.10      qed
    6.11    qed
     7.1 --- a/src/HOL/Datatype.thy	Wed Jan 04 17:04:11 2006 +0100
     7.2 +++ b/src/HOL/Datatype.thy	Wed Jan 04 19:22:53 2006 +0100
     7.3 @@ -140,19 +140,23 @@
     7.4  
     7.5  datatype 'a option = None | Some 'a
     7.6  
     7.7 -lemma not_None_eq: "(x ~= None) = (EX y. x = Some y)"
     7.8 +lemma not_None_eq[iff]: "(x ~= None) = (EX y. x = Some y)"
     7.9 +  by (induct x) auto
    7.10 +
    7.11 +lemma not_Some_eq[iff]: "(ALL y. x ~= Some y) = (x = None)"
    7.12    by (induct x) auto
    7.13  
    7.14 -lemma not_Some_eq: "(ALL y. x ~= Some y) = (x = None)"
    7.15 -  by (induct x) auto
    7.16 +text{*Although it may appear that both of these equalities are helpful
    7.17 +only when applied to assumptions, in practice it seems better to give
    7.18 +them the uniform iff attribute. *}
    7.19  
    7.20 -text{*Both of these equalities are helpful only when applied to assumptions.*}
    7.21 -
    7.22 +(*
    7.23  lemmas not_None_eq_D = not_None_eq [THEN iffD1]
    7.24  declare not_None_eq_D [dest!]
    7.25  
    7.26  lemmas not_Some_eq_D = not_Some_eq [THEN iffD1]
    7.27  declare not_Some_eq_D [dest!]
    7.28 +*)
    7.29  
    7.30  lemma option_caseE:
    7.31    "(case x of None => P | Some y => Q y) ==>
     8.1 --- a/src/HOL/Hoare/SepLogHeap.thy	Wed Jan 04 17:04:11 2006 +0100
     8.2 +++ b/src/HOL/Hoare/SepLogHeap.thy	Wed Jan 04 19:22:53 2006 +0100
     8.3 @@ -7,9 +7,9 @@
     8.4  for Separation Logic.
     8.5  *)
     8.6  
     8.7 -theory SepLogHeap imports Main begin
     8.8 -
     8.9 -declare not_None_eq [iff]
    8.10 +theory SepLogHeap
    8.11 +imports Main
    8.12 +begin
    8.13  
    8.14  types heap = "(nat \<Rightarrow> nat option)"
    8.15  
     9.1 --- a/src/HOL/HoareParallel/RG_Hoare.thy	Wed Jan 04 17:04:11 2006 +0100
     9.2 +++ b/src/HOL/HoareParallel/RG_Hoare.thy	Wed Jan 04 19:22:53 2006 +0100
     9.3 @@ -5,7 +5,6 @@
     9.4  subsection {* Proof System for Component Programs *}
     9.5  
     9.6  declare Un_subset_iff [iff del]
     9.7 -declare not_None_eq [iff]
     9.8  declare Cons_eq_map_conv[iff]
     9.9  
    9.10  constdefs
    10.1 --- a/src/HOL/Library/Nested_Environment.thy	Wed Jan 04 17:04:11 2006 +0100
    10.2 +++ b/src/HOL/Library/Nested_Environment.thy	Wed Jan 04 19:22:53 2006 +0100
    10.3 @@ -193,7 +193,7 @@
    10.4    from prems have "lookup env (xs @ ys) \<noteq> None" by simp
    10.5    then have "lookup env xs \<noteq> None"
    10.6      by (rule contrapos_nn) (simp only: lookup_append_none)
    10.7 -  then show ?thesis by (simp add: not_None_eq)
    10.8 +  then show ?thesis by (simp)
    10.9  qed
   10.10  
   10.11  text {*
    11.1 --- a/src/HOL/Map.thy	Wed Jan 04 17:04:11 2006 +0100
    11.2 +++ b/src/HOL/Map.thy	Wed Jan 04 19:22:53 2006 +0100
    11.3 @@ -530,7 +530,7 @@
    11.4  
    11.5  lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
    11.6  apply(rule ext)
    11.7 -apply(force simp: map_add_def dom_def not_None_eq  split:option.split) 
    11.8 +apply(force simp: map_add_def dom_def split:option.split) 
    11.9  done
   11.10  
   11.11  subsection {* @{term [source] ran} *}
   11.12 @@ -587,13 +587,13 @@
   11.13  done
   11.14  
   11.15  lemma map_le_map_add [simp]: "f \<subseteq>\<^sub>m (g ++ f)"
   11.16 -  by (fastsimp simp add: map_le_def not_None_eq)
   11.17 +  by (fastsimp simp add: map_le_def)
   11.18  
   11.19  lemma map_le_iff_map_add_commute: "(f \<subseteq>\<^sub>m f ++ g) = (f++g = g++f)"
   11.20  by(fastsimp simp add:map_add_def map_le_def expand_fun_eq split:option.splits)
   11.21  
   11.22  lemma map_add_le_mapE: "f++g \<subseteq>\<^sub>m h \<Longrightarrow> g \<subseteq>\<^sub>m h"
   11.23 -by (fastsimp simp add: map_le_def map_add_def dom_def not_None_eq)
   11.24 +by (fastsimp simp add: map_le_def map_add_def dom_def)
   11.25  
   11.26  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"
   11.27  by (clarsimp simp add: map_le_def map_add_def dom_def split:option.splits)
    12.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Wed Jan 04 17:04:11 2006 +0100
    12.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Wed Jan 04 19:22:53 2006 +0100
    12.3 @@ -208,8 +208,7 @@
    12.4    "C \<in> set (xcpt_names (i,G,pc,et)) \<Longrightarrow> 
    12.5    \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"
    12.6    apply (cases i)
    12.7 -  apply (auto iff: not_None_eq
    12.8 -	      dest!: match_any_match_table match_X_match_table 
    12.9 +  apply (auto dest!: match_any_match_table match_X_match_table 
   12.10                dest: match_exception_table_in_et)
   12.11    done
   12.12  
    13.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Wed Jan 04 17:04:11 2006 +0100
    13.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Wed Jan 04 19:22:53 2006 +0100
    13.3 @@ -12,7 +12,6 @@
    13.4  theory JBasis imports Main begin 
    13.5  
    13.6  lemmas [simp] = Let_def
    13.7 -declare not_None_eq [iff]
    13.8  
    13.9  section "unique"
   13.10   
    14.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Wed Jan 04 17:04:11 2006 +0100
    14.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Wed Jan 04 19:22:53 2006 +0100
    14.3 @@ -44,7 +44,7 @@
    14.4  lemma subcls1_def2: 
    14.5    "subcls1 G = 
    14.6       (SIGMA C: {C. is_class G C} . {D. C\<noteq>Object \<and> fst (the (class G C))=D})"
    14.7 -  by (auto simp add: is_class_def not_None_eq dest: subcls1D intro: subcls1I)
    14.8 +  by (auto simp add: is_class_def dest: subcls1D intro: subcls1I)
    14.9  
   14.10  lemma finite_subcls1: "finite (subcls1 G)"
   14.11  apply(subst subcls1_def2)
    15.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Wed Jan 04 17:04:11 2006 +0100
    15.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Wed Jan 04 19:22:53 2006 +0100
    15.3 @@ -123,7 +123,7 @@
    15.4  done
    15.5  
    15.6  lemma is_class_Object [simp]: "ws_prog G ==> is_class G Object"
    15.7 -  by (simp add: is_class_def not_None_eq)
    15.8 +  by (simp add: is_class_def)
    15.9  
   15.10  lemma is_class_xcpt [simp]: "ws_prog G \<Longrightarrow> is_class G (Xcpt x)"
   15.11    apply (simp add: ws_prog_def wf_syscls_def)
    16.1 --- a/src/HOL/Unix/Unix.thy	Wed Jan 04 17:04:11 2006 +0100
    16.2 +++ b/src/HOL/Unix/Unix.thy	Wed Jan 04 19:22:53 2006 +0100
    16.3 @@ -1059,7 +1059,7 @@
    16.4                    lookup root ((path @ [y]) @ us) \<noteq> None"
    16.5                  by cases (auto dest: access_some_lookup)
    16.6                then show ?thesis 
    16.7 -                by (simp add: not_None_eq, blast dest!: lookup_some_append)
    16.8 +                by (simp, blast dest!: lookup_some_append)
    16.9              qed
   16.10              finally show ?thesis .
   16.11            qed
    17.1 --- a/src/HOL/ex/Reflected_Presburger.thy	Wed Jan 04 17:04:11 2006 +0100
    17.2 +++ b/src/HOL/ex/Reflected_Presburger.thy	Wed Jan 04 19:22:53 2006 +0100
    17.3 @@ -12,8 +12,6 @@
    17.4  imports Main
    17.5  begin
    17.6  
    17.7 -declare not_Some_eq [iff]
    17.8 -
    17.9  (* Shadow syntax for integer terms *)
   17.10  datatype intterm =
   17.11      Cst int