fixed anomalies in the installed classical rules
authorpaulson
Wed Feb 19 10:53:27 2003 +0100 (2003-02-19)
changeset 13823d49ffd9f9662
parent 13822 bb5eda7416e5
child 13824 e4d8dea6dfc2
fixed anomalies in the installed classical rules
src/ZF/Nat.thy
src/ZF/OrderArith.thy
src/ZF/QPair.thy
src/ZF/Sum.thy
     1.1 --- a/src/ZF/Nat.thy	Tue Feb 18 19:13:47 2003 +0100
     1.2 +++ b/src/ZF/Nat.thy	Wed Feb 19 10:53:27 2003 +0100
     1.3 @@ -113,11 +113,11 @@
     1.4  lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
     1.5  by (induct a rule: nat_induct, auto)
     1.6  
     1.7 -lemma succ_natD [dest!]: "succ(i): nat ==> i: nat"
     1.8 +lemma succ_natD: "succ(i): nat ==> i: nat"
     1.9  by (rule Ord_trans [OF succI1], auto)
    1.10  
    1.11  lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
    1.12 -by blast
    1.13 +by (blast dest!: succ_natD)
    1.14  
    1.15  lemma nat_le_Limit: "Limit(i) ==> nat le i"
    1.16  apply (rule subset_imp_le)
     2.1 --- a/src/ZF/OrderArith.thy	Tue Feb 18 19:13:47 2003 +0100
     2.2 +++ b/src/ZF/OrderArith.thy	Wed Feb 19 10:53:27 2003 +0100
     2.3 @@ -49,10 +49,12 @@
     2.4      "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
     2.5  by (unfold radd_def, blast)
     2.6  
     2.7 -lemma radd_Inr_Inl_iff [iff]: 
     2.8 -    "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False"
     2.9 +lemma radd_Inr_Inl_iff [simp]: 
    2.10 +    "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"
    2.11  by (unfold radd_def, blast)
    2.12  
    2.13 +declare radd_Inr_Inl_iff [THEN iffD1, dest!] 
    2.14 +
    2.15  subsubsection{*Elimination Rule*}
    2.16  
    2.17  lemma raddE:
     3.1 --- a/src/ZF/QPair.thy	Tue Feb 18 19:13:47 2003 +0100
     3.2 +++ b/src/ZF/QPair.thy	Wed Feb 19 10:53:27 2003 +0100
     3.3 @@ -233,10 +233,10 @@
     3.4  lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
     3.5  by (simp add: qsum_defs )
     3.6  
     3.7 -lemma QInl_QInr_iff [iff]: "QInl(a)=QInr(b) <-> False"
     3.8 +lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <-> False"
     3.9  by (simp add: qsum_defs )
    3.10  
    3.11 -lemma QInr_QInl_iff [iff]: "QInr(b)=QInl(a) <-> False"
    3.12 +lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <-> False"
    3.13  by (simp add: qsum_defs )
    3.14  
    3.15  lemma qsum_empty [simp]: "0<+>0 = 0"
    3.16 @@ -246,8 +246,8 @@
    3.17  
    3.18  lemmas QInl_inject = QInl_iff [THEN iffD1, standard]
    3.19  lemmas QInr_inject = QInr_iff [THEN iffD1, standard]
    3.20 -lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE]
    3.21 -lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE]
    3.22 +lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!]
    3.23 +lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!]
    3.24  
    3.25  lemma QInlD: "QInl(a): A<+>B ==> a: A"
    3.26  by blast
     4.1 --- a/src/ZF/Sum.thy	Tue Feb 18 19:13:47 2003 +0100
     4.2 +++ b/src/ZF/Sum.thy	Wed Feb 19 10:53:27 2003 +0100
     4.3 @@ -90,10 +90,10 @@
     4.4  lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
     4.5  by (simp add: sum_defs)
     4.6  
     4.7 -lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) <-> False"
     4.8 +lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) <-> False"
     4.9  by (simp add: sum_defs)
    4.10  
    4.11 -lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) <-> False"
    4.12 +lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) <-> False"
    4.13  by (simp add: sum_defs)
    4.14  
    4.15  lemma sum_empty [simp]: "0+0 = 0"
    4.16 @@ -103,8 +103,8 @@
    4.17  
    4.18  lemmas Inl_inject = Inl_iff [THEN iffD1, standard]
    4.19  lemmas Inr_inject = Inr_iff [THEN iffD1, standard]
    4.20 -lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE]
    4.21 -lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE]
    4.22 +lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!]
    4.23 +lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!]
    4.24  
    4.25  
    4.26  lemma InlD: "Inl(a): A+B ==> a: A"