new simprules and classical rules
authorpaulson
Mon Jan 21 14:47:55 2002 +0100 (2002-01-21)
changeset 12825f1f7964ed05c
parent 12824 cdf586d56b8a
child 12826 dfb214fa310b
new simprules and classical rules
src/FOL/simpdata.ML
src/ZF/List.ML
src/ZF/OrdQuant.thy
src/ZF/Ordinal.ML
src/ZF/UNITY/SubstAx.ML
src/ZF/simpdata.ML
     1.1 --- a/src/FOL/simpdata.ML	Mon Jan 21 14:47:47 2002 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Mon Jan 21 14:47:55 2002 +0100
     1.3 @@ -352,7 +352,7 @@
     1.4  
     1.5  bind_thms ("cla_simps",
     1.6    [de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2,
     1.7 -   not_all, not_ex, cases_simp] @
     1.8 +   not_imp, not_all, not_ex, cases_simp] @
     1.9    map prove_fun
    1.10     ["~(P&Q) <-> ~P | ~Q",
    1.11      "P | ~P",             "~P | P",
     2.1 --- a/src/ZF/List.ML	Mon Jan 21 14:47:47 2002 +0100
     2.2 +++ b/src/ZF/List.ML	Mon Jan 21 14:47:55 2002 +0100
     2.3 @@ -705,16 +705,14 @@
     2.4  by (ALLGOALS(Asm_full_simp_tac));
     2.5  qed_spec_mp "nth_append";
     2.6  
     2.7 -Goal "xs:list(A) ==> \
     2.8 -\ set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x=nth(i, xs)}";
     2.9 +Goal "xs:list(A) \
    2.10 +\     ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x=nth(i, xs)}";
    2.11  by (induct_tac "xs" 1);
    2.12  by (ALLGOALS(Asm_simp_tac));
    2.13  by (rtac equalityI 1);
    2.14  by Auto_tac;
    2.15  by (res_inst_tac [("x", "0")] bexI 1);
    2.16  by Auto_tac;
    2.17 -by (res_inst_tac [("x", "succ(i)")] bexI 1);
    2.18 -by Auto_tac;
    2.19  by (etac natE 1);
    2.20  by Auto_tac;
    2.21  qed "set_of_list_conv_nth";
     3.1 --- a/src/ZF/OrdQuant.thy	Mon Jan 21 14:47:47 2002 +0100
     3.2 +++ b/src/ZF/OrdQuant.thy	Mon Jan 21 14:47:55 2002 +0100
     3.3 @@ -36,6 +36,28 @@
     3.4    "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
     3.5  
     3.6  
     3.7 +(** simplification of the new quantifiers **)
     3.8 +
     3.9 +
    3.10 +(*MOST IMPORTANT that this is added to the simpset BEFORE OrdQuant.ML
    3.11 +  is loaded: it's Ord_atomize would convert this rule to 
    3.12 +    x < 0 ==> P(x) == True, which causes dire effects!*)
    3.13 +lemma [simp]: "(ALL x<0. P(x))"
    3.14 +by (simp add: oall_def) 
    3.15 +
    3.16 +lemma [simp]: "~(EX x<0. P(x))"
    3.17 +by (simp add: oex_def) 
    3.18 +
    3.19 +lemma [simp]: "(ALL x<succ(i). P(x)) <-> (Ord(i) --> P(i) & (ALL x<i. P(x)))"
    3.20 +apply (simp add: oall_def le_iff) 
    3.21 +apply (blast intro: lt_Ord2) 
    3.22 +done
    3.23 +
    3.24 +lemma [simp]: "(EX x<succ(i). P(x)) <-> (Ord(i) & (P(i) | (EX x<i. P(x))))"
    3.25 +apply (simp add: oex_def le_iff) 
    3.26 +apply (blast intro: lt_Ord2) 
    3.27 +done
    3.28 +
    3.29  declare Ord_Un [intro,simp,TC]
    3.30  declare Ord_UN [intro,simp,TC]
    3.31  declare Ord_Union [intro,simp,TC]
    3.32 @@ -62,11 +84,11 @@
    3.33  lemma increasing_LimitI: "\<lbrakk>0<l; \<forall>x\<in>l. \<exists>y\<in>l. x<y\<rbrakk> \<Longrightarrow> Limit(l)"
    3.34  apply (simp add: Limit_def lt_Ord2, clarify)
    3.35  apply (drule_tac i=y in ltD) 
    3.36 -apply (blast intro: lt_trans1 succ_leI ltI lt_Ord2)
    3.37 +apply (blast intro: lt_trans1 [OF _ ltI] lt_Ord2)
    3.38  done
    3.39  
    3.40  lemma UN_upper_lt:
    3.41 -     "\<lbrakk>a\<in> A;  i < b(a);  Ord(\<Union>x\<in>A. b(x))\<rbrakk> \<Longrightarrow> i < (\<Union>x\<in>A. b(x))"
    3.42 +     "\<lbrakk>a\<in>A;  i < b(a);  Ord(\<Union>x\<in>A. b(x))\<rbrakk> \<Longrightarrow> i < (\<Union>x\<in>A. b(x))"
    3.43  by (unfold lt_def, blast) 
    3.44  
    3.45  lemma lt_imp_0_lt: "j<i \<Longrightarrow> 0<i"
     4.1 --- a/src/ZF/Ordinal.ML	Mon Jan 21 14:47:47 2002 +0100
     4.2 +++ b/src/ZF/Ordinal.ML	Mon Jan 21 14:47:55 2002 +0100
     4.3 @@ -548,8 +548,7 @@
     4.4  Goal "succ(i) le j <-> i<j";
     4.5  by (REPEAT (ares_tac [iffI,succ_leI,succ_leE] 1));
     4.6  qed "succ_le_iff";
     4.7 -
     4.8 -Addsimps [succ_le_iff];
     4.9 +AddIffs [succ_le_iff];
    4.10  
    4.11  Goal "succ(i) le succ(j) ==> i le j";
    4.12  by (blast_tac (claset() addSDs [succ_leE]) 1);
     5.1 --- a/src/ZF/UNITY/SubstAx.ML	Mon Jan 21 14:47:47 2002 +0100
     5.2 +++ b/src/ZF/UNITY/SubstAx.ML	Mon Jan 21 14:47:55 2002 +0100
     5.3 @@ -300,20 +300,20 @@
     5.4  \        field(r)<=I; A<=f-``I; F:program |] \
     5.5  \     ==> F : A LeadsTo B";
     5.6  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
     5.7 -by Safe_tac;
     5.8 +by Auto_tac; 
     5.9  by (eres_inst_tac [("I", "I"), ("f", "f")] leadsTo_wf_induct 1);
    5.10  by (ALLGOALS(Clarify_tac));
    5.11  by (dres_inst_tac [("x", "m")] bspec 2);
    5.12  by Safe_tac;
    5.13 -by (res_inst_tac 
    5.14 -[("A'", "reachable(F) Int (A Int f -``(converse(r)``{m}) Un B)")]leadsTo_weaken_R 2);
    5.15 +by (res_inst_tac [("A'", 
    5.16 +                   "reachable(F) Int (A Int f -``(converse(r)``{m}) Un B)")]
    5.17 +    leadsTo_weaken_R 2);
    5.18  by (asm_simp_tac (simpset() addsimps [Int_assoc]) 2);
    5.19  by (asm_simp_tac (simpset() addsimps [Int_assoc]) 3);
    5.20  by (REPEAT(Blast_tac 1));
    5.21  qed "LeadsTo_wf_induct";
    5.22  
    5.23  
    5.24 -
    5.25  Goal "[| ALL m:nat. F:(A Int f-``{m}) LeadsTo ((A Int f-``lessThan(m,nat)) Un B); \
    5.26  \     A<=f-``nat; F:program |] ==> F : A LeadsTo B";
    5.27  by (res_inst_tac [("A1", "nat"), ("I", "nat")] (wf_less_than RS LeadsTo_wf_induct) 1);
     6.1 --- a/src/ZF/simpdata.ML	Mon Jan 21 14:47:47 2002 +0100
     6.2 +++ b/src/ZF/simpdata.ML	Mon Jan 21 14:47:55 2002 +0100
     6.3 @@ -72,7 +72,9 @@
     6.4  in
     6.5  
     6.6  val ball_simps = map prover
     6.7 -    ["(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)",
     6.8 +    ["(ALL x:A. P(x) & Q)   <-> (ALL x:A. P(x)) & (A=0 | Q)",
     6.9 +     "(ALL x:A. P & Q(x))   <-> (A=0 | P) & (ALL x:A. Q(x))",
    6.10 +     "(ALL x:A. P(x) | Q)   <-> ((ALL x:A. P(x)) | Q)",
    6.11       "(ALL x:A. P | Q(x))   <-> (P | (ALL x:A. Q(x)))",
    6.12       "(ALL x:A. P --> Q(x)) <-> (P --> (ALL x:A. Q(x)))",
    6.13       "(ALL x:A. P(x) --> Q) <-> ((EX x:A. P(x)) --> Q)",
    6.14 @@ -90,6 +92,10 @@
    6.15  val bex_simps = map prover
    6.16      ["(EX x:A. P(x) & Q) <-> ((EX x:A. P(x)) & Q)",
    6.17       "(EX x:A. P & Q(x)) <-> (P & (EX x:A. Q(x)))",
    6.18 +     "(EX x:A. P(x) | Q) <-> (EX x:A. P(x)) | (A~=0 & Q)",
    6.19 +     "(EX x:A. P | Q(x)) <-> (A~=0 & P) | (EX x:A. Q(x))",
    6.20 +     "(EX x:A. P --> Q(x)) <-> ((A=0 | P) --> (EX x:A. Q(x)))",
    6.21 +     "(EX x:A. P(x) --> Q) <-> ((ALL x:A. P(x)) --> (A~=0 & Q))",
    6.22       "(EX x:0.P(x)) <-> False",
    6.23       "(EX x:succ(i).P(x)) <-> P(i) | (EX x:i. P(x))",
    6.24       "(EX x:cons(a,B).P(x)) <-> P(a) | (EX x:B. P(x))",