# HG changeset patch # User paulson # Date 1124199388 -7200 # Node ID fb0a80aef0becc7551647c57f96b379594476801 # Parent 051b0897bc983ce7c0d0f45bed696a11595df9c3 classical rules must have names for ATP integration diff -r 051b0897bc98 -r fb0a80aef0be src/HOL/Datatype_Universe.thy --- 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 \ 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 \ 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) \ 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) \ 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) diff -r 051b0897bc98 -r fb0a80aef0be src/HOL/Divides.thy --- 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) = (\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 \q::nat. m = r + q*d" diff -r 051b0897bc98 -r fb0a80aef0be src/HOL/Fun.thy --- 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 *) diff -r 051b0897bc98 -r fb0a80aef0be src/HOL/Integ/IntDiv.thy --- 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 diff -r 051b0897bc98 -r fb0a80aef0be src/HOL/Set.thy --- 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 diff -r 051b0897bc98 -r fb0a80aef0be src/HOL/Sum_Type.thy --- 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] diff -r 051b0897bc98 -r fb0a80aef0be src/HOL/Tools/datatype_package.ML --- 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])]); diff -r 051b0897bc98 -r fb0a80aef0be src/Provers/clasimp.ML --- 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) = diff -r 051b0897bc98 -r fb0a80aef0be src/Provers/classical.ML --- 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