summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 23 Sep 2005 16:05:42 +0200 | |

changeset 17604 | 5f30179fbf44 |

parent 17603 | f601609d3300 |

child 17605 | caed4fb770d5 |

rules -> iprover

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