--- a/src/FOL/simpdata.ML Mon Jan 21 14:47:47 2002 +0100
+++ b/src/FOL/simpdata.ML Mon Jan 21 14:47:55 2002 +0100
@@ -352,7 +352,7 @@
bind_thms ("cla_simps",
[de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
- not_all, not_ex, cases_simp] @
+ not_imp, not_all, not_ex, cases_simp] @
map prove_fun
["~(P&Q) <-> ~P | ~Q",
"P | ~P", "~P | P",
--- a/src/ZF/List.ML Mon Jan 21 14:47:47 2002 +0100
+++ b/src/ZF/List.ML Mon Jan 21 14:47:55 2002 +0100
@@ -705,16 +705,14 @@
by (ALLGOALS(Asm_full_simp_tac));
qed_spec_mp "nth_append";
-Goal "xs:list(A) ==> \
-\ set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x=nth(i, xs)}";
+Goal "xs:list(A) \
+\ ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x=nth(i, xs)}";
by (induct_tac "xs" 1);
by (ALLGOALS(Asm_simp_tac));
by (rtac equalityI 1);
by Auto_tac;
by (res_inst_tac [("x", "0")] bexI 1);
by Auto_tac;
-by (res_inst_tac [("x", "succ(i)")] bexI 1);
-by Auto_tac;
by (etac natE 1);
by Auto_tac;
qed "set_of_list_conv_nth";
--- a/src/ZF/OrdQuant.thy Mon Jan 21 14:47:47 2002 +0100
+++ b/src/ZF/OrdQuant.thy Mon Jan 21 14:47:55 2002 +0100
@@ -36,6 +36,28 @@
"@OUNION" :: "[idt, i, i] => i" ("(3\<Union>_<_./ _)" 10)
+(** simplification of the new quantifiers **)
+
+
+(*MOST IMPORTANT that this is added to the simpset BEFORE OrdQuant.ML
+ is loaded: it's Ord_atomize would convert this rule to
+ x < 0 ==> P(x) == True, which causes dire effects!*)
+lemma [simp]: "(ALL x<0. P(x))"
+by (simp add: oall_def)
+
+lemma [simp]: "~(EX x<0. P(x))"
+by (simp add: oex_def)
+
+lemma [simp]: "(ALL x<succ(i). P(x)) <-> (Ord(i) --> P(i) & (ALL x<i. P(x)))"
+apply (simp add: oall_def le_iff)
+apply (blast intro: lt_Ord2)
+done
+
+lemma [simp]: "(EX x<succ(i). P(x)) <-> (Ord(i) & (P(i) | (EX x<i. P(x))))"
+apply (simp add: oex_def le_iff)
+apply (blast intro: lt_Ord2)
+done
+
declare Ord_Un [intro,simp,TC]
declare Ord_UN [intro,simp,TC]
declare Ord_Union [intro,simp,TC]
@@ -62,11 +84,11 @@
lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)"
apply (simp add: Limit_def lt_Ord2, clarify)
apply (drule_tac i=y in ltD)
-apply (blast intro: lt_trans1 succ_leI ltI lt_Ord2)
+apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2)
done
lemma UN_upper_lt:
- "\<lbrakk>a\<in> A; i < b(a); Ord(\<Union>x\<in>A. b(x))\<rbrakk> \<Longrightarrow> i < (\<Union>x\<in>A. b(x))"
+ "\<lbrakk>a\<in>A; i < b(a); Ord(\<Union>x\<in>A. b(x))\<rbrakk> \<Longrightarrow> i < (\<Union>x\<in>A. b(x))"
by (unfold lt_def, blast)
lemma lt_imp_0_lt: "j<i \<Longrightarrow> 0<i"
--- a/src/ZF/Ordinal.ML Mon Jan 21 14:47:47 2002 +0100
+++ b/src/ZF/Ordinal.ML Mon Jan 21 14:47:55 2002 +0100
@@ -548,8 +548,7 @@
Goal "succ(i) le j <-> i<j";
by (REPEAT (ares_tac [iffI,succ_leI,succ_leE] 1));
qed "succ_le_iff";
-
-Addsimps [succ_le_iff];
+AddIffs [succ_le_iff];
Goal "succ(i) le succ(j) ==> i le j";
by (blast_tac (claset() addSDs [succ_leE]) 1);
--- a/src/ZF/UNITY/SubstAx.ML Mon Jan 21 14:47:47 2002 +0100
+++ b/src/ZF/UNITY/SubstAx.ML Mon Jan 21 14:47:55 2002 +0100
@@ -300,20 +300,20 @@
\ field(r)<=I; A<=f-``I; F:program |] \
\ ==> F : A LeadsTo B";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by Safe_tac;
+by Auto_tac;
by (eres_inst_tac [("I", "I"), ("f", "f")] leadsTo_wf_induct 1);
by (ALLGOALS(Clarify_tac));
by (dres_inst_tac [("x", "m")] bspec 2);
by Safe_tac;
-by (res_inst_tac
-[("A'", "reachable(F) Int (A Int f -``(converse(r)``{m}) Un B)")]leadsTo_weaken_R 2);
+by (res_inst_tac [("A'",
+ "reachable(F) Int (A Int f -``(converse(r)``{m}) Un B)")]
+ leadsTo_weaken_R 2);
by (asm_simp_tac (simpset() addsimps [Int_assoc]) 2);
by (asm_simp_tac (simpset() addsimps [Int_assoc]) 3);
by (REPEAT(Blast_tac 1));
qed "LeadsTo_wf_induct";
-
Goal "[| ALL m:nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``lessThan(m,nat)) Un B); \
\ A<=f-``nat; F:program |] ==> F : A LeadsTo B";
by (res_inst_tac [("A1", "nat"), ("I", "nat")] (wf_less_than RS LeadsTo_wf_induct) 1);
--- a/src/ZF/simpdata.ML Mon Jan 21 14:47:47 2002 +0100
+++ b/src/ZF/simpdata.ML Mon Jan 21 14:47:55 2002 +0100
@@ -72,7 +72,9 @@
in
val ball_simps = map prover
- ["(ALL x:A. P(x) | Q) <-> ((ALL x:A. P(x)) | Q)",
+ ["(ALL x:A. P(x) & Q) <-> (ALL x:A. P(x)) & (A=0 | Q)",
+ "(ALL x:A. P & Q(x)) <-> (A=0 | P) & (ALL x:A. Q(x))",
+ "(ALL x:A. P(x) | Q) <-> ((ALL x:A. P(x)) | Q)",
"(ALL x:A. P | Q(x)) <-> (P | (ALL x:A. Q(x)))",
"(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
"(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
@@ -90,6 +92,10 @@
val bex_simps = map prover
["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
"(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
+ "(EX x:A. P(x) | Q) <-> (EX x:A. P(x)) | (A~=0 & Q)",
+ "(EX x:A. P | Q(x)) <-> (A~=0 & P) | (EX x:A. Q(x))",
+ "(EX x:A. P --> Q(x)) <-> ((A=0 | P) --> (EX x:A. Q(x)))",
+ "(EX x:A. P(x) --> Q) <-> ((ALL x:A. P(x)) --> (A~=0 & Q))",
"(EX x:0.P(x)) <-> False",
"(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
"(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",