--- 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"
--- 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
--- 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
--- 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