src/HOL/Extraction/Pigeonhole.thy
 changeset 17604 5f30179fbf44 parent 17145 e623e57b0f44 child 20593 5af400cc64d5
```--- a/src/HOL/Extraction/Pigeonhole.thy	Fri Sep 23 16:05:10 2005 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Fri Sep 23 16:05:42 2005 +0200
@@ -20,7 +20,7 @@
apply (induct m)
apply (case_tac n)
apply (case_tac  n)
-  apply (simp only: nat.simps, rules?)+
+  apply (simp only: nat.simps, iprover?)+
done

text {*
@@ -34,7 +34,7 @@
have "\<not> (\<exists>j<0. x = f j)"
proof
assume "\<exists>j<0. x = f j"
-    then obtain j where j: "j < (0::nat)" by rules
+    then obtain j where j: "j < (0::nat)" by iprover
thus "False" by simp
qed
thus ?case ..
@@ -44,23 +44,23 @@
proof
assume "\<exists>j<l. x = f j"
then obtain j where j: "j < l"
-      and eq: "x = f j" by rules
+      and eq: "x = f j" by iprover
from j have "j < Suc l" by simp
-    with eq show ?case by rules
+    with eq show ?case by iprover
next
assume nex: "\<not> (\<exists>j<l. x = f j)"
from nat_eq_dec show ?case
proof
assume eq: "x = f l"
have "l < Suc l" by simp
-      with eq show ?case by rules
+      with eq show ?case by iprover
next
assume neq: "x \<noteq> f l"
have "\<not> (\<exists>j<Suc l. x = f j)"
proof
assume "\<exists>j<Suc l. x = f j"
then obtain j where j: "j < Suc l"
-	  and eq: "x = f j" by rules
+	  and eq: "x = f j" by iprover
show False
proof cases
assume "j = l"
@@ -69,7 +69,7 @@
next
assume "j \<noteq> l"
with j have "j < l" by simp
-	  with nex and eq show False by rules
+	  with nex and eq show False by iprover
qed
qed
thus ?case ..
@@ -86,7 +86,7 @@
proof (induct n)
case 0
hence "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp
-  thus ?case by rules
+  thus ?case by iprover
next
case (Suc n)
{
@@ -102,7 +102,7 @@
proof
assume "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
then obtain i j where i: "i \<le> Suc n" and j: "j < i"
-	  and f: "?f i = ?f j" by rules
+	  and f: "?f i = ?f j" by iprover
from j have i_nz: "Suc 0 \<le> i" by simp
from i have iSSn: "i \<le> Suc (Suc n)" by simp
have S0SSn: "Suc 0 \<le> Suc (Suc n)" by simp
@@ -164,7 +164,7 @@
from search show ?case
proof
assume "\<exists>j<Suc k. f (Suc k) = f j"
-	thus ?case by (rules intro: le_refl)
+	thus ?case by (iprover intro: le_refl)
next
assume nex: "\<not> (\<exists>j<Suc k. f (Suc k) = f j)"
have "\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j"
@@ -179,7 +179,7 @@
proof
assume "f i = f j"
hence "f (Suc k) = f j" by (simp add: eq)
-	      with nex and j and eq show False by rules
+	      with nex and j and eq show False by iprover
qed
next
assume "i \<noteq> Suc k"
@@ -187,7 +187,7 @@
thus ?thesis using i and j by (rule Suc)
qed
qed
-	thus ?thesis by (rules intro: le_SucI)
+	thus ?thesis by (iprover intro: le_SucI)
qed
qed
}
@@ -207,16 +207,16 @@
have "Suc 0 \<le> Suc 0" ..
moreover have "0 < Suc 0" ..
moreover from 0 have "f (Suc 0) = f 0" by simp
-  ultimately show ?case by rules
+  ultimately show ?case by iprover
next
case (Suc n)
from search show ?case
proof
assume "\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j"
-    thus ?case by (rules intro: le_refl)
+    thus ?case by (iprover intro: le_refl)
next
assume "\<not> (\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j)"
-    hence nex: "\<forall>j < Suc (Suc n). f (Suc (Suc n)) \<noteq> f j" by rules
+    hence nex: "\<forall>j < Suc (Suc n). f (Suc (Suc n)) \<noteq> f j" by iprover
let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"
proof -
@@ -237,7 +237,7 @@
qed
hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" by (rule Suc)
then obtain i j where i: "i \<le> Suc n" and ji: "j < i" and f: "?f i = ?f j"
-      by rules
+      by iprover
have "f i = f j"
proof (cases "f i = Suc n")
case True
@@ -263,7 +263,7 @@
qed
qed
moreover from i have "i \<le> Suc (Suc n)" by simp
-    ultimately show ?thesis using ji by rules
+    ultimately show ?thesis using ji by iprover
qed
qed
```