--- a/src/ZF/Nat.thy Tue Feb 18 19:13:47 2003 +0100
+++ b/src/ZF/Nat.thy Wed Feb 19 10:53:27 2003 +0100
@@ -113,11 +113,11 @@
lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)"
by (induct a rule: nat_induct, auto)
-lemma succ_natD [dest!]: "succ(i): nat ==> i: nat"
+lemma succ_natD: "succ(i): nat ==> i: nat"
by (rule Ord_trans [OF succI1], auto)
lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat"
-by blast
+by (blast dest!: succ_natD)
lemma nat_le_Limit: "Limit(i) ==> nat le i"
apply (rule subset_imp_le)
--- a/src/ZF/OrderArith.thy Tue Feb 18 19:13:47 2003 +0100
+++ b/src/ZF/OrderArith.thy Wed Feb 19 10:53:27 2003 +0100
@@ -49,10 +49,12 @@
"<Inr(b'), Inr(b)> : radd(A,r,B,s) <-> b':B & b:B & <b',b>:s"
by (unfold radd_def, blast)
-lemma radd_Inr_Inl_iff [iff]:
- "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"
+lemma radd_Inr_Inl_iff [simp]:
+ "<Inr(b), Inl(a)> : radd(A,r,B,s) <-> False"
by (unfold radd_def, blast)
+declare radd_Inr_Inl_iff [THEN iffD1, dest!]
+
subsubsection{*Elimination Rule*}
lemma raddE:
--- a/src/ZF/QPair.thy Tue Feb 18 19:13:47 2003 +0100
+++ b/src/ZF/QPair.thy Wed Feb 19 10:53:27 2003 +0100
@@ -233,10 +233,10 @@
lemma QInr_iff [iff]: "QInr(a)=QInr(b) <-> a=b"
by (simp add: qsum_defs )
-lemma QInl_QInr_iff [iff]: "QInl(a)=QInr(b) <-> False"
+lemma QInl_QInr_iff [simp]: "QInl(a)=QInr(b) <-> False"
by (simp add: qsum_defs )
-lemma QInr_QInl_iff [iff]: "QInr(b)=QInl(a) <-> False"
+lemma QInr_QInl_iff [simp]: "QInr(b)=QInl(a) <-> False"
by (simp add: qsum_defs )
lemma qsum_empty [simp]: "0<+>0 = 0"
@@ -246,8 +246,8 @@
lemmas QInl_inject = QInl_iff [THEN iffD1, standard]
lemmas QInr_inject = QInr_iff [THEN iffD1, standard]
-lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE]
-lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE]
+lemmas QInl_neq_QInr = QInl_QInr_iff [THEN iffD1, THEN FalseE, elim!]
+lemmas QInr_neq_QInl = QInr_QInl_iff [THEN iffD1, THEN FalseE, elim!]
lemma QInlD: "QInl(a): A<+>B ==> a: A"
by blast
--- a/src/ZF/Sum.thy Tue Feb 18 19:13:47 2003 +0100
+++ b/src/ZF/Sum.thy Wed Feb 19 10:53:27 2003 +0100
@@ -90,10 +90,10 @@
lemma Inr_iff [iff]: "Inr(a)=Inr(b) <-> a=b"
by (simp add: sum_defs)
-lemma Inl_Inr_iff [iff]: "Inl(a)=Inr(b) <-> False"
+lemma Inl_Inr_iff [simp]: "Inl(a)=Inr(b) <-> False"
by (simp add: sum_defs)
-lemma Inr_Inl_iff [iff]: "Inr(b)=Inl(a) <-> False"
+lemma Inr_Inl_iff [simp]: "Inr(b)=Inl(a) <-> False"
by (simp add: sum_defs)
lemma sum_empty [simp]: "0+0 = 0"
@@ -103,8 +103,8 @@
lemmas Inl_inject = Inl_iff [THEN iffD1, standard]
lemmas Inr_inject = Inr_iff [THEN iffD1, standard]
-lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE]
-lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE]
+lemmas Inl_neq_Inr = Inl_Inr_iff [THEN iffD1, THEN FalseE, elim!]
+lemmas Inr_neq_Inl = Inr_Inl_iff [THEN iffD1, THEN FalseE, elim!]
lemma InlD: "Inl(a): A+B ==> a: A"