# HG changeset patch
# User nipkow
# Date 1127484342 -7200
# Node ID 5f30179fbf44f3fe69ac6691d0fc563c6c2cb206
# Parent  f601609d3300ce26f48b82e6bacb7c7d05a9a45b
rules -> iprover

diff -r f601609d3300 -r 5f30179fbf44 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Fri Sep 23 16:05:10 2005 +0200
+++ b/src/HOL/Extraction/Higman.thy	Fri Sep 23 16:05:42 2005 +0200
@@ -65,10 +65,10 @@
   bar1 [Pure.intro]: "ws \<in> good \<Longrightarrow> ws \<in> bar"
   bar2 [Pure.intro]: "(\<And>w. w # ws \<in> bar) \<Longrightarrow> ws \<in> bar"
 
-theorem prop1: "([] # ws) \<in> bar" by rules
+theorem prop1: "([] # ws) \<in> bar" by iprover
 
 theorem lemma1: "ws \<in> L as \<Longrightarrow> ws \<in> L (a # as)"
-  by (erule L.induct, rules+)
+  by (erule L.induct, iprover+)
 
 lemma lemma2': "(vs, ws) \<in> R a \<Longrightarrow> vs \<in> L as \<Longrightarrow> ws \<in> L (a # as)"
   apply (induct set: R)
@@ -83,7 +83,7 @@
 
 lemma lemma2: "(vs, ws) \<in> R a \<Longrightarrow> vs \<in> good \<Longrightarrow> ws \<in> good"
   apply (induct set: R)
-  apply rules
+  apply iprover
   apply (erule good.elims)
   apply simp_all
   apply (rule good0)
@@ -102,7 +102,7 @@
   apply (erule lemma1)
   apply (erule L.elims)
   apply simp_all
-  apply rules+
+  apply iprover+
   done
 
 lemma lemma3: "(ws, zs) \<in> T a \<Longrightarrow> ws \<in> good \<Longrightarrow> zs \<in> good"
@@ -116,12 +116,12 @@
   apply simp_all
   apply (rule good0)
   apply (erule lemma3')
-  apply rules+
+  apply iprover+
   done
 
 lemma lemma4: "(ws, zs) \<in> R a \<Longrightarrow> ws \<noteq> [] \<Longrightarrow> (ws, zs) \<in> T a"
   apply (induct set: R)
-  apply rules
+  apply iprover
   apply (case_tac vs)
   apply (erule R.elims)
   apply simp
@@ -186,12 +186,12 @@
 	from letter_eq_dec show ?thesis
 	proof
 	  assume ca: "c = a"
-	  from ab have "(a # cs) # zs \<in> bar" by (rules intro: I ys Ta Tb)
+	  from ab have "(a # cs) # zs \<in> bar" by (iprover intro: I ys Ta Tb)
 	  thus ?thesis by (simp add: Cons ca)
 	next
 	  assume "c \<noteq> a"
 	  with ab have cb: "c = b" by (rule letter_neq)
-	  from ab have "(b # cs) # zs \<in> bar" by (rules intro: I' Ta Tb)
+	  from ab have "(b # cs) # zs \<in> bar" by (iprover intro: I' Ta Tb)
 	  thus ?thesis by (simp add: Cons cb)
 	qed
       qed
@@ -222,11 +222,11 @@
       from letter_eq_dec show ?case
       proof
 	assume "c = a"
-	thus ?thesis by (rules intro: I [simplified] R)
+	thus ?thesis by (iprover intro: I [simplified] R)
       next
 	from R xsn have T: "(xs, zs) \<in> T a" by (rule lemma4)
 	assume "c \<noteq> a"
-	thus ?thesis by (rules intro: prop2 Cons xsb xsn R T)
+	thus ?thesis by (iprover intro: prop2 Cons xsb xsn R T)
       qed
     qed
   qed
@@ -240,7 +240,7 @@
     show "[[]] \<in> bar" by (rule prop1)
   next
     fix c cs assume "[cs] \<in> bar"
-    thus "[c # cs] \<in> bar" by (rule prop3) (simp, rules)
+    thus "[c # cs] \<in> bar" by (rule prop3) (simp, iprover)
   qed
 qed
 
@@ -256,11 +256,11 @@
   shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> vs \<in> good" using bar
 proof induct
   case bar1
-  thus ?case by rules
+  thus ?case by iprover
 next
   case (bar2 ws)
   have "is_prefix (f (length ws) # ws) f" by simp
-  thus ?case by (rules intro: bar2)
+  thus ?case by (iprover intro: bar2)
 qed
 
 theorem good_prefix: "\<exists>vs. is_prefix vs f \<and> vs \<in> good"
diff -r f601609d3300 -r 5f30179fbf44 src/HOL/Extraction/Pigeonhole.thy
--- 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 [3] 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
 
diff -r f601609d3300 -r 5f30179fbf44 src/HOL/Extraction/QuotRem.thy
--- a/src/HOL/Extraction/QuotRem.thy	Fri Sep 23 16:05:10 2005 +0200
+++ b/src/HOL/Extraction/QuotRem.thy	Fri Sep 23 16:05:42 2005 +0200
@@ -12,27 +12,27 @@
   apply (induct m)
   apply (case_tac n)
   apply (case_tac [3] n)
-  apply (simp only: nat.simps, rules?)+
+  apply (simp only: nat.simps, iprover?)+
   done
 
 theorem division: "\<exists>r q. a = Suc b * q + r \<and> r \<le> b"
 proof (induct a)
   case 0
   have "0 = Suc b * 0 + 0 \<and> 0 \<le> b" by simp
-  thus ?case by rules
+  thus ?case by iprover
 next
   case (Suc a)
-  then obtain r q where I: "a = Suc b * q + r" and "r \<le> b" by rules
+  then obtain r q where I: "a = Suc b * q + r" and "r \<le> b" by iprover
   from nat_eq_dec show ?case
   proof
     assume "r = b"
     with I have "Suc a = Suc b * (Suc q) + 0 \<and> 0 \<le> b" by simp
-    thus ?case by rules
+    thus ?case by iprover
   next
     assume "r \<noteq> b"
     hence "r < b" by (simp add: order_less_le)
     with I have "Suc a = Suc b * q + (Suc r) \<and> (Suc r) \<le> b" by simp
-    thus ?case by rules
+    thus ?case by iprover
   qed
 qed
 
diff -r f601609d3300 -r 5f30179fbf44 src/HOL/Extraction/Warshall.thy
--- a/src/HOL/Extraction/Warshall.thy	Fri Sep 23 16:05:10 2005 +0200
+++ b/src/HOL/Extraction/Warshall.thy	Fri Sep 23 16:05:42 2005 +0200
@@ -38,7 +38,7 @@
   by (induct ys) simp+
 
 theorem list_all_scoc [simp]: "list_all P (xs @ [x]) = (P x \<and> list_all P xs)"
-  by (induct xs, simp+, rules)
+  by (induct xs, simp+, iprover)
 
 theorem list_all_lemma: 
   "list_all P xs \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> list_all Q xs"
@@ -188,7 +188,7 @@
 theorem lemma5':
   "\<And>p. is_path r p (Suc i) j k \<Longrightarrow> \<not> is_path r p i j k \<Longrightarrow>
    \<not> (\<forall>q. \<not> is_path r q i j i) \<and> \<not> (\<forall>q'. \<not> is_path r q' i i k)"
-  by (rules dest: lemma5)
+  by (iprover dest: lemma5)
 
 theorem warshall: 
   "\<And>j k. \<not> (\<exists>p. is_path r p i j k) \<or> (\<exists>p. is_path r p i j k)"
@@ -205,7 +205,7 @@
     assume "r j k = F"
     hence "r j k ~= T" by simp
     hence "\<not> (\<exists>p. is_path r p 0 j k)"
-      by (rules dest: lemma2)
+      by (iprover dest: lemma2)
     thus ?thesis ..
   qed
 next
@@ -217,7 +217,7 @@
     proof
       assume "\<not> (\<exists>p. is_path r p i j i)"
       with h1 have "\<not> (\<exists>p. is_path r p (Suc i) j k)"
-	by (rules dest: lemma5')
+	by (iprover dest: lemma5')
       thus ?case ..
     next
       assume "\<exists>p. is_path r p i j i"
@@ -226,7 +226,7 @@
       proof
 	assume "\<not> (\<exists>p. is_path r p i i k)"
 	with h1 have "\<not> (\<exists>p. is_path r p (Suc i) j k)"
-	  by (rules dest: lemma5')
+	  by (iprover dest: lemma5')
 	thus ?case ..
       next
 	assume "\<exists>q. is_path r q i i k"
@@ -240,7 +240,7 @@
   next
     assume "\<exists>p. is_path r p i j k"
     hence "\<exists>p. is_path r p (Suc i) j k"
-      by (rules intro: lemma1)
+      by (iprover intro: lemma1)
     thus ?case ..
   qed
 qed