# HG changeset patch
# User paulson
# Date 1011620875 -3600
# Node ID f1f7964ed05c960fed830729ddd5e0f511b35bce
# Parent  cdf586d56b8a1ac9c2e9c485dc240dcb3696f241
new simprules and classical rules

diff -r cdf586d56b8a -r f1f7964ed05c src/FOL/simpdata.ML
--- 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",
diff -r cdf586d56b8a -r f1f7964ed05c src/ZF/List.ML
--- 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";
diff -r cdf586d56b8a -r f1f7964ed05c src/ZF/OrdQuant.thy
--- 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"
diff -r cdf586d56b8a -r f1f7964ed05c src/ZF/Ordinal.ML
--- 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);
diff -r cdf586d56b8a -r f1f7964ed05c src/ZF/UNITY/SubstAx.ML
--- 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);
diff -r cdf586d56b8a -r f1f7964ed05c src/ZF/simpdata.ML
--- 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))",