--- a/src/HOL/Datatype_Universe.thy Tue Aug 16 13:54:24 2005 +0200
+++ b/src/HOL/Datatype_Universe.thy Tue Aug 16 15:36:28 2005 +0200
@@ -156,8 +156,8 @@
elim!: apfst_convE sym [THEN Push_neq_K0])
done
-lemmas Atom_not_Scons = Scons_not_Atom [THEN not_sym, standard, iff]
-
+lemmas Atom_not_Scons = Scons_not_Atom [THEN not_sym, standard]
+declare Atom_not_Scons [iff]
(*** Injectiveness ***)
@@ -178,7 +178,8 @@
apply (erule Atom_inject [THEN Inl_inject])
done
-lemmas Leaf_inject = inj_Leaf [THEN injD, standard, dest!]
+lemmas Leaf_inject = inj_Leaf [THEN injD, standard]
+declare Leaf_inject [dest!]
lemma inj_Numb: "inj(Numb)"
apply (simp add: Numb_def o_def)
@@ -186,7 +187,8 @@
apply (erule Atom_inject [THEN Inr_inject])
done
-lemmas Numb_inject = inj_Numb [THEN injD, standard, dest!]
+lemmas Numb_inject = inj_Numb [THEN injD, standard]
+declare Numb_inject [dest!]
(** Injectiveness of Push_Node **)
@@ -238,16 +240,16 @@
lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
by (simp add: Leaf_def o_def Scons_not_Atom)
-lemmas Leaf_not_Scons = Scons_not_Leaf [THEN not_sym, standard, iff]
-
+lemmas Leaf_not_Scons = Scons_not_Leaf [THEN not_sym, standard]
+declare Leaf_not_Scons [iff]
(** Scons vs Numb **)
lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
by (simp add: Numb_def o_def Scons_not_Atom)
-lemmas Numb_not_Scons = Scons_not_Numb [THEN not_sym, standard, iff]
-
+lemmas Numb_not_Scons = Scons_not_Numb [THEN not_sym, standard]
+declare Numb_not_Scons [iff]
(** Leaf vs Numb **)
@@ -255,8 +257,8 @@
lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
by (simp add: Leaf_def Numb_def)
-lemmas Numb_not_Leaf = Leaf_not_Numb [THEN not_sym, standard, iff]
-
+lemmas Numb_not_Leaf = Leaf_not_Numb [THEN not_sym, standard]
+declare Numb_not_Leaf [iff]
(*** ndepth -- the depth of a node ***)
@@ -362,7 +364,8 @@
lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
by (auto simp add: In0_def In1_def One_nat_def)
-lemmas In1_not_In0 = In0_not_In1 [THEN not_sym, standard, iff]
+lemmas In1_not_In0 = In0_not_In1 [THEN not_sym, standard]
+declare In1_not_In0 [iff]
lemma In0_inject: "In0(M) = In0(N) ==> M=N"
by (simp add: In0_def)
--- a/src/HOL/Divides.thy Tue Aug 16 13:54:24 2005 +0200
+++ b/src/HOL/Divides.thy Tue Aug 16 15:36:28 2005 +0200
@@ -562,8 +562,11 @@
apply (erule dvd_mult)
done
-(* k dvd (m*k) *)
-declare dvd_refl [THEN dvd_mult, iff] dvd_refl [THEN dvd_mult2, iff]
+lemma dvd_triv_right [iff]: "k dvd (m*k :: nat)"
+by (rule dvd_refl [THEN dvd_mult])
+
+lemma dvd_triv_left [iff]: "k dvd (k*m :: nat)"
+by (rule dvd_refl [THEN dvd_mult2])
lemma dvd_reduce: "(k dvd n + k) = (k dvd (n::nat))"
apply (rule iffI)
@@ -648,7 +651,9 @@
lemma mod_eq_0_iff: "(m mod d = 0) = (\<exists>q::nat. m = d*q)"
by (auto simp add: dvd_eq_mod_eq_0 [symmetric] dvd_def)
-declare mod_eq_0_iff [THEN iffD1, dest!]
+
+lemmas mod_eq_0D = mod_eq_0_iff [THEN iffD1]
+declare mod_eq_0D [dest!]
(*Loses information, namely we also have r<d provided d is nonzero*)
lemma mod_eqD: "(m mod d = r) ==> \<exists>q::nat. m = r + q*d"
--- a/src/HOL/Fun.thy Tue Aug 16 13:54:24 2005 +0200
+++ b/src/HOL/Fun.thy Tue Aug 16 15:36:28 2005 +0200
@@ -367,11 +367,11 @@
lemmas fun_upd_idem = fun_upd_idem_iff [THEN iffD2, standard]
(* f(x := f x) = f *)
-declare refl [THEN fun_upd_idem, iff]
+lemmas fun_upd_triv = refl [THEN fun_upd_idem]
+declare fun_upd_triv [iff]
lemma fun_upd_apply [simp]: "(f(x:=y))z = (if z=x then y else f z)"
-apply (simp (no_asm) add: fun_upd_def)
-done
+by (simp add: fun_upd_def)
(* fun_upd_apply supersedes these two, but they are useful
if fun_upd_apply is intentionally removed from the simpset *)
--- a/src/HOL/Integ/IntDiv.thy Tue Aug 16 13:54:24 2005 +0200
+++ b/src/HOL/Integ/IntDiv.thy Tue Aug 16 15:36:28 2005 +0200
@@ -634,7 +634,8 @@
thus "m mod d = 0" by auto
qed
-declare zmod_eq_0_iff [THEN iffD1, dest!]
+lemmas zmod_eq_0D = zmod_eq_0_iff [THEN iffD1]
+declare zmod_eq_0D [dest!]
text{*proving (a+b) div c = a div c + b div c + ((a mod c + b mod c) div c) *}
@@ -1052,12 +1053,12 @@
apply (erule zdvd_zmult)
done
-lemma [iff]: "(k::int) dvd m * k"
+lemma zdvd_triv_right [iff]: "(k::int) dvd m * k"
apply (rule zdvd_zmult)
apply (rule zdvd_refl)
done
-lemma [iff]: "(k::int) dvd k * m"
+lemma zdvd_triv_left [iff]: "(k::int) dvd k * m"
apply (rule zdvd_zmult2)
apply (rule zdvd_refl)
done
--- a/src/HOL/Set.thy Tue Aug 16 13:54:24 2005 +0200
+++ b/src/HOL/Set.thy Tue Aug 16 15:36:28 2005 +0200
@@ -671,10 +671,10 @@
Classical prover. Negated assumptions behave like formulae on the
right side of the notional turnstile ... *}
-lemma ComplD: "c : -A ==> c~:A"
+lemma ComplD [dest!]: "c : -A ==> c~:A"
by (unfold Compl_def) blast
-lemmas ComplE [elim!] = ComplD [elim_format]
+lemmas ComplE = ComplD [elim_format]
subsubsection {* Binary union -- Un *}
@@ -764,10 +764,10 @@
-- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
by (rule insertI1)
-lemma singletonD: "b : {a} ==> b = a"
+lemma singletonD [dest!]: "b : {a} ==> b = a"
by blast
-lemmas singletonE [elim!] = singletonD [elim_format]
+lemmas singletonE = singletonD [elim_format]
lemma singleton_iff: "(b : {a}) = (b = a)"
by blast
--- a/src/HOL/Sum_Type.thy Tue Aug 16 13:54:24 2005 +0200
+++ b/src/HOL/Sum_Type.thy Tue Aug 16 15:36:28 2005 +0200
@@ -78,7 +78,8 @@
apply (rule Inr_RepI)
done
-lemmas Inr_not_Inl = Inl_not_Inr [THEN not_sym, standard, iff]
+lemmas Inr_not_Inl = Inl_not_Inr [THEN not_sym, standard]
+declare Inr_not_Inl [iff]
lemmas Inl_neq_Inr = Inl_not_Inr [THEN notE, standard]
lemmas Inr_neq_Inl = sym [THEN Inl_neq_Inr, standard]
--- a/src/HOL/Tools/datatype_package.ML Tue Aug 16 13:54:24 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Tue Aug 16 15:36:28 2005 +0200
@@ -281,6 +281,9 @@
end;
+fun name_notE th =
+ Thm.name_thm (Thm.name_of_thm th ^ "_E", th RS notE);
+
fun add_rules simps case_thms size_thms rec_thms inject distinct
weak_case_congs cong_att =
(#1 o PureThy.add_thmss [(("simps", simps), []),
@@ -288,7 +291,7 @@
List.concat distinct @ rec_thms), [Simplifier.simp_add_global]),
(("", size_thms @ rec_thms), [RecfunCodegen.add NONE]),
(("", List.concat inject), [iff_add_global]),
- (("", List.concat distinct RL [notE]), [Classical.safe_elim_global]),
+ (("", map name_notE (List.concat distinct)), [Classical.safe_elim_global]),
(("", weak_case_congs), [cong_att])]);
--- a/src/Provers/clasimp.ML Tue Aug 16 13:54:24 2005 +0200
+++ b/src/Provers/clasimp.ML Tue Aug 16 15:36:28 2005 +0200
@@ -114,6 +114,9 @@
fun cs addss' ss = Classical.addbefore (cs, ("asm_full_simp_tac",
CHANGED o Simplifier.asm_lr_simp_tac ss));
+(*Attach a suffix, provided we have a name to start with.*)
+fun suffix_thm "" _ th = th
+ | suffix_thm a b th = Thm.name_thm (a^b, th);
(* iffs: addition of rules to simpsets and clasets simultaneously *)
@@ -126,12 +129,14 @@
fun addIff decls1 decls2 simp ((cs, ss), th) =
let
+ val name = Thm.name_of_thm th;
val n = nprems_of th;
- val (dest, elim, intro) = if n = 0 then decls1 else decls2;
+ val (elim, intro) = if n = 0 then decls1 else decls2;
val zero_rotate = zero_var_indexes o rotate_prems n;
in
- (dest (intro (cs, [zero_rotate (th RS Data.iffD2)]), [zero_rotate (th RS Data.iffD1)])
- handle THM _ => (elim (cs, [zero_rotate (th RS Data.notE)])
+ (elim (intro (cs, [suffix_thm name "_iff2" (zero_rotate (th RS Data.iffD2))]),
+ [suffix_thm name "_iff1" (Data.cla_make_elim (zero_rotate (th RS Data.iffD1)))])
+ handle THM _ => (elim (cs, [suffix_thm name "_iff" (zero_rotate (th RS Data.notE))])
handle THM _ => intro (cs, [th])),
simp (ss, [th]))
end;
@@ -151,8 +156,10 @@
in
val op addIffs =
- Library.foldl (addIff (Classical.addSDs, Classical.addSEs, Classical.addSIs)
- (Classical.addDs, Classical.addEs, Classical.addIs) Simplifier.addsimps);
+ Library.foldl
+ (addIff (Classical.addSEs, Classical.addSIs)
+ (Classical.addEs, Classical.addIs)
+ Simplifier.addsimps);
val op delIffs = Library.foldl (delIff Classical.delrules Simplifier.delsimps);
fun AddIffs thms = store_clasimp (clasimpset () addIffs thms);
@@ -160,14 +167,14 @@
fun addIffs_global (thy, ths) =
Library.foldl (addIff
- (ContextRules.addXDs_global, ContextRules.addXEs_global, ContextRules.addXIs_global)
- (ContextRules.addXDs_global, ContextRules.addXEs_global, ContextRules.addXIs_global) #1)
+ (ContextRules.addXEs_global, ContextRules.addXIs_global)
+ (ContextRules.addXEs_global, ContextRules.addXIs_global) #1)
((thy, ()), ths) |> #1;
fun addIffs_local (ctxt, ths) =
Library.foldl (addIff
- (ContextRules.addXDs_local, ContextRules.addXEs_local, ContextRules.addXIs_local)
- (ContextRules.addXDs_local, ContextRules.addXEs_local, ContextRules.addXIs_local) #1)
+ (ContextRules.addXEs_local, ContextRules.addXIs_local)
+ (ContextRules.addXEs_local, ContextRules.addXIs_local) #1)
((ctxt, ()), ths) |> #1;
fun delIffs_global (thy, ths) =
--- a/src/Provers/classical.ML Tue Aug 16 13:54:24 2005 +0200
+++ b/src/Provers/classical.ML Tue Aug 16 15:36:28 2005 +0200
@@ -391,7 +391,13 @@
val op addSIs = rev_foldl addSI;
val op addSEs = rev_foldl addSE;
-fun cs addSDs ths = cs addSEs (map Data.make_elim ths);
+(*Give new theorem a name, if it has one already.*)
+fun name_make_elim th =
+ case Thm.name_of_thm th of
+ "" => Data.make_elim th
+ | a => Thm.name_thm (a ^ "_dest", Data.make_elim th);
+
+fun cs addSDs ths = cs addSEs (map name_make_elim ths);
(*** Hazardous (unsafe) rules ***)
@@ -445,7 +451,7 @@
val op addIs = rev_foldl addI;
val op addEs = rev_foldl addE;
-fun cs addDs ths = cs addEs (map Data.make_elim ths);
+fun cs addDs ths = cs addEs (map name_make_elim ths);
(*** Deletion of rules