--- 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 {*
--- 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"
--- 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
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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) ==>
--- 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)
--- 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}
--- 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"
--- 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
--- 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.{->}";
--- 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]:
--- 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 {*
--- 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)
--- 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)
--- 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
--- 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"
--- 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)
--- 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)
--- 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> {})"
--- 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
--- 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