--- a/src/HOL/Proofs/Extraction/Euclid.thy Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Euclid.thy Fri Jul 01 16:52:35 2016 +0200
@@ -14,8 +14,8 @@
begin
text \<open>
-A constructive version of the proof of Euclid's theorem by
-Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}.
+ A constructive version of the proof of Euclid's theorem by
+ Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}.
\<close>
lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m"
@@ -24,11 +24,10 @@
lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k"
by (induct k) auto
-lemma prod_mn_less_k:
- "(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k"
+lemma prod_mn_less_k: "0 < n \<Longrightarrow> 0 < k \<Longrightarrow> Suc 0 < m \<Longrightarrow> m * n = k \<Longrightarrow> n < k"
by (induct m) auto
-lemma prime_eq: "prime (p::nat) = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))"
+lemma prime_eq: "prime p \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)"
apply (simp add: prime_def)
apply (rule iffI)
apply blast
@@ -39,29 +38,25 @@
apply (erule allE)
apply (erule impE)
apply assumption
- apply (case_tac "m=0")
+ apply (case_tac "m = 0")
apply simp
- apply (case_tac "m=Suc 0")
+ apply (case_tac "m = Suc 0")
apply simp
apply simp
done
-lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))"
+lemma prime_eq': "prime p \<longleftrightarrow> 1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p)"
by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps)
lemma not_prime_ex_mk:
assumes n: "Suc 0 < n"
shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
proof -
- {
- fix k
- from nat_eq_dec
- have "(\<exists>m<n. n = m * k) \<or> \<not> (\<exists>m<n. n = m * k)"
- by (rule search)
- }
- hence "(\<exists>k<n. \<exists>m<n. n = m * k) \<or> \<not> (\<exists>k<n. \<exists>m<n. n = m * k)"
+ from nat_eq_dec have "(\<exists>m<n. n = m * k) \<or> \<not> (\<exists>m<n. n = m * k)" for k
by (rule search)
- thus ?thesis
+ then have "(\<exists>k<n. \<exists>m<n. n = m * k) \<or> \<not> (\<exists>k<n. \<exists>m<n. n = m * k)"
+ by (rule search)
+ then show ?thesis
proof
assume "\<exists>k<n. \<exists>m<n. n = m * k"
then obtain k m where k: "k<n" and m: "m<n" and nmk: "n = m * k"
@@ -71,7 +66,7 @@
ultimately show ?thesis using k m nmk by iprover
next
assume "\<not> (\<exists>k<n. \<exists>m<n. n = m * k)"
- hence A: "\<forall>k<n. \<forall>m<n. n \<noteq> m * k" by iprover
+ then have A: "\<forall>k<n. \<forall>m<n. n \<noteq> m * k" by iprover
have "\<forall>m k. n = m * k \<longrightarrow> Suc 0 < m \<longrightarrow> m = n"
proof (intro allI impI)
fix m k
@@ -99,11 +94,11 @@
qed
with n have "prime n"
by (simp only: prime_eq' One_nat_def simp_thms)
- thus ?thesis ..
+ then show ?thesis ..
qed
qed
-lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact (n::nat)"
+lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n"
proof (induct n rule: nat_induct)
case 0
then show ?case by simp
@@ -124,30 +119,30 @@
qed
lemma dvd_prod [iff]: "n dvd (\<Prod>m::nat \<in># mset (n # ns). m)"
- by (simp add: msetprod_Un msetprod_singleton)
+ by (simp add: msetprod_Un)
-definition all_prime :: "nat list \<Rightarrow> bool" where
- "all_prime ps \<longleftrightarrow> (\<forall>p\<in>set ps. prime p)"
+definition all_prime :: "nat list \<Rightarrow> bool"
+ where "all_prime ps \<longleftrightarrow> (\<forall>p\<in>set ps. prime p)"
lemma all_prime_simps:
"all_prime []"
"all_prime (p # ps) \<longleftrightarrow> prime p \<and> all_prime ps"
by (simp_all add: all_prime_def)
-lemma all_prime_append:
- "all_prime (ps @ qs) \<longleftrightarrow> all_prime ps \<and> all_prime qs"
+lemma all_prime_append: "all_prime (ps @ qs) \<longleftrightarrow> all_prime ps \<and> all_prime qs"
by (simp add: all_prime_def ball_Un)
lemma split_all_prime:
assumes "all_prime ms" and "all_prime ns"
- shows "\<exists>qs. all_prime qs \<and> (\<Prod>m::nat \<in># mset qs. m) =
- (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs")
+ shows "\<exists>qs. all_prime qs \<and>
+ (\<Prod>m::nat \<in># mset qs. m) = (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)"
+ (is "\<exists>qs. ?P qs \<and> ?Q qs")
proof -
from assms have "all_prime (ms @ ns)"
by (simp add: all_prime_append)
- moreover from assms have "(\<Prod>m::nat \<in># mset (ms @ ns). m) =
- (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)"
- by (simp add: msetprod_Un)
+ moreover
+ have "(\<Prod>m::nat \<in># mset (ms @ ns). m) = (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)"
+ using assms by (simp add: msetprod_Un)
ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" ..
then show ?thesis ..
qed
@@ -155,8 +150,10 @@
lemma all_prime_nempty_g_one:
assumes "all_prime ps" and "ps \<noteq> []"
shows "Suc 0 < (\<Prod>m::nat \<in># mset ps. m)"
- using \<open>ps \<noteq> []\<close> \<open>all_prime ps\<close> unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct)
- (simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
+ using \<open>ps \<noteq> []\<close> \<open>all_prime ps\<close>
+ unfolding One_nat_def [symmetric]
+ by (induct ps rule: list_nonempty_induct)
+ (simp_all add: all_prime_simps msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def)
lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = n)"
proof (induct n rule: nat_wf_ind)
@@ -165,14 +162,17 @@
have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n"
by (rule not_prime_ex_mk)
then show ?case
- proof
+ proof
assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k"
then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n"
- and kn: "k < n" and nmk: "n = m * k" by iprover
- from mn and m have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = m" by (rule 1)
+ and kn: "k < n" and nmk: "n = m * k"
+ by iprover
+ from mn and m have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = m"
+ by (rule 1)
then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(\<Prod>m::nat \<in># mset ps1. m) = m"
by iprover
- from kn and k have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = k" by (rule 1)
+ from kn and k have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = k"
+ by (rule 1)
then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(\<Prod>m::nat \<in># mset ps2. m) = k"
by iprover
from \<open>all_prime ps1\<close> \<open>all_prime ps2\<close>
@@ -192,27 +192,27 @@
assumes N: "(1::nat) < n"
shows "\<exists>p. prime p \<and> p dvd n"
proof -
- from N obtain ps where "all_prime ps"
- and prod_ps: "n = (\<Prod>m::nat \<in># mset ps. m)" using factor_exists
- by simp iprover
+ from N obtain ps where "all_prime ps" and prod_ps: "n = (\<Prod>m::nat \<in># mset ps. m)"
+ using factor_exists by simp iprover
with N have "ps \<noteq> []"
- by (auto simp add: all_prime_nempty_g_one msetprod_empty)
- then obtain p qs where ps: "ps = p # qs" by (cases ps) simp
- with \<open>all_prime ps\<close> have "prime p" by (simp add: all_prime_simps)
- moreover from \<open>all_prime ps\<close> ps prod_ps
- have "p dvd n" by (simp only: dvd_prod)
+ by (auto simp add: all_prime_nempty_g_one)
+ then obtain p qs where ps: "ps = p # qs"
+ by (cases ps) simp
+ with \<open>all_prime ps\<close> have "prime p"
+ by (simp add: all_prime_simps)
+ moreover from \<open>all_prime ps\<close> ps prod_ps have "p dvd n"
+ by (simp only: dvd_prod)
ultimately show ?thesis by iprover
qed
-text \<open>
-Euclid's theorem: there are infinitely many primes.
-\<close>
+text \<open>Euclid's theorem: there are infinitely many primes.\<close>
-lemma Euclid: "\<exists>p::nat. prime p \<and> n < p"
+lemma Euclid: "\<exists>p. prime p \<and> n < p"
proof -
let ?k = "fact n + (1::nat)"
have "1 < ?k" by simp
- then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover
+ then obtain p where prime: "prime p" and dvd: "p dvd ?k"
+ using prime_factor_exists by iprover
have "n < p"
proof -
have "\<not> p \<le> n"
@@ -232,10 +232,10 @@
extract Euclid
text \<open>
-The program extracted from the proof of Euclid's theorem looks as follows.
-@{thm [display] Euclid_def}
-The program corresponding to the proof of the factorization theorem is
-@{thm [display] factor_exists_def}
+ The program extracted from the proof of Euclid's theorem looks as follows.
+ @{thm [display] Euclid_def}
+ The program corresponding to the proof of the factorization theorem is
+ @{thm [display] factor_exists_def}
\<close>
instantiation nat :: default
@@ -256,9 +256,10 @@
end
-primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where
+primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
+where
"iterate 0 f x = []"
- | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
+| "iterate (Suc n) f x = (let y = f x in y # iterate n f y)"
lemma "factor_exists 1007 = [53, 19]" by eval
lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval
--- a/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Greatest_Common_Divisor.thy Fri Jul 01 16:52:35 2016 +0200
@@ -10,8 +10,9 @@
begin
theorem greatest_common_divisor:
- "\<And>n::nat. Suc m < n \<Longrightarrow> \<exists>k n1 m1. k * n1 = n \<and> k * m1 = Suc m \<and>
- (\<forall>l l1 l2. l * l1 = n \<longrightarrow> l * l2 = Suc m \<longrightarrow> l \<le> k)"
+ "\<And>n::nat. Suc m < n \<Longrightarrow>
+ \<exists>k n1 m1. k * n1 = n \<and> k * m1 = Suc m \<and>
+ (\<forall>l l1 l2. l * l1 = n \<longrightarrow> l * l2 = Suc m \<longrightarrow> l \<le> k)"
proof (induct m rule: nat_wf_ind)
case (1 m n)
from division obtain r q where h1: "n = Suc m * q + r" and h2: "r \<le> m"
@@ -21,33 +22,28 @@
case 0
with h1 have "Suc m * q = n" by simp
moreover have "Suc m * 1 = Suc m" by simp
- moreover {
- fix l2 have "\<And>l l1. l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> Suc m"
- by (cases l2) simp_all }
+ moreover have "l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> Suc m" for l l1 l2
+ by (cases l2) simp_all
ultimately show ?thesis by iprover
next
case (Suc nat)
with h2 have h: "nat < m" by simp
moreover from h have "Suc nat < Suc m" by simp
ultimately have "\<exists>k m1 r1. k * m1 = Suc m \<and> k * r1 = Suc nat \<and>
- (\<forall>l l1 l2. l * l1 = Suc m \<longrightarrow> l * l2 = Suc nat \<longrightarrow> l \<le> k)"
+ (\<forall>l l1 l2. l * l1 = Suc m \<longrightarrow> l * l2 = Suc nat \<longrightarrow> l \<le> k)"
by (rule 1)
- then obtain k m1 r1 where
- h1': "k * m1 = Suc m"
+ then obtain k m1 r1 where h1': "k * m1 = Suc m"
and h2': "k * r1 = Suc nat"
and h3': "\<And>l l1 l2. l * l1 = Suc m \<Longrightarrow> l * l2 = Suc nat \<Longrightarrow> l \<le> k"
by iprover
have mn: "Suc m < n" by (rule 1)
- from h1 h1' h2' Suc have "k * (m1 * q + r1) = n"
+ from h1 h1' h2' Suc have "k * (m1 * q + r1) = n"
by (simp add: add_mult_distrib2 mult.assoc [symmetric])
- moreover have "\<And>l l1 l2. l * l1 = n \<Longrightarrow> l * l2 = Suc m \<Longrightarrow> l \<le> k"
+ moreover have "l \<le> k" if ll1n: "l * l1 = n" and ll2m: "l * l2 = Suc m" for l l1 l2
proof -
- fix l l1 l2
- assume ll1n: "l * l1 = n"
- assume ll2m: "l * l2 = Suc m"
- moreover have "l * (l1 - l2 * q) = Suc nat"
+ have "l * (l1 - l2 * q) = Suc nat"
by (simp add: diff_mult_distrib2 h1 Suc [symmetric] mn ll1n ll2m [symmetric])
- ultimately show "l \<le> k" by (rule h3')
+ with ll2m show "l \<le> k" by (rule h3')
qed
ultimately show ?thesis using h1' by iprover
qed
@@ -56,8 +52,8 @@
extract greatest_common_divisor
text \<open>
-The extracted program for computing the greatest common divisor is
-@{thm [display] greatest_common_divisor_def}
+ The extracted program for computing the greatest common divisor is
+ @{thm [display] greatest_common_divisor_def}
\<close>
instantiation nat :: default
--- a/src/HOL/Proofs/Extraction/Higman.thy Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Higman.thy Fri Jul 01 16:52:35 2016 +0200
@@ -18,43 +18,44 @@
inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
where
- emb0 [Pure.intro]: "emb [] bs"
- | emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
- | emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
+ emb0 [Pure.intro]: "emb [] bs"
+| emb1 [Pure.intro]: "emb as bs \<Longrightarrow> emb as (b # bs)"
+| emb2 [Pure.intro]: "emb as bs \<Longrightarrow> emb (a # as) (a # bs)"
inductive L :: "letter list \<Rightarrow> letter list list \<Rightarrow> bool"
for v :: "letter list"
where
- L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)"
- | L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"
+ L0 [Pure.intro]: "emb w v \<Longrightarrow> L v (w # ws)"
+| L1 [Pure.intro]: "L v ws \<Longrightarrow> L v (w # ws)"
inductive good :: "letter list list \<Rightarrow> bool"
where
- good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)"
- | good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"
+ good0 [Pure.intro]: "L w ws \<Longrightarrow> good (w # ws)"
+| good1 [Pure.intro]: "good ws \<Longrightarrow> good (w # ws)"
inductive R :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
for a :: letter
where
- R0 [Pure.intro]: "R a [] []"
- | R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"
+ R0 [Pure.intro]: "R a [] []"
+| R1 [Pure.intro]: "R a vs ws \<Longrightarrow> R a (w # vs) ((a # w) # ws)"
inductive T :: "letter \<Rightarrow> letter list list \<Rightarrow> letter list list \<Rightarrow> bool"
for a :: letter
where
- T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)"
- | T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)"
- | T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"
+ T0 [Pure.intro]: "a \<noteq> b \<Longrightarrow> R b ws zs \<Longrightarrow> T a (w # zs) ((a # w) # zs)"
+| T1 [Pure.intro]: "T a ws zs \<Longrightarrow> T a (w # ws) ((a # w) # zs)"
+| T2 [Pure.intro]: "a \<noteq> b \<Longrightarrow> T a ws zs \<Longrightarrow> T a ws ((b # w) # zs)"
inductive bar :: "letter list list \<Rightarrow> bool"
where
- bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws"
- | bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"
+ bar1 [Pure.intro]: "good ws \<Longrightarrow> bar ws"
+| bar2 [Pure.intro]: "(\<And>w. bar (w # ws)) \<Longrightarrow> bar ws"
-theorem prop1: "bar ([] # ws)" by iprover
+theorem prop1: "bar ([] # ws)"
+ by iprover
theorem lemma1: "L as ws \<Longrightarrow> L (a # as) ws"
- by (erule L.induct, iprover+)
+ by (erule L.induct) iprover+
lemma lemma2': "R a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"
apply (induct set: R)
@@ -123,7 +124,7 @@
apply simp
done
-lemma letter_neq: "(a::letter) \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b"
+lemma letter_neq: "a \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> c = b" for a b c :: letter
apply (case_tac a)
apply (case_tac b)
apply (case_tac c, simp, simp)
@@ -133,7 +134,7 @@
apply (case_tac c, simp, simp)
done
-lemma letter_eq_dec: "(a::letter) = b \<or> a \<noteq> b"
+lemma letter_eq_dec: "a = b \<or> a \<noteq> b" for a b :: letter
apply (case_tac a)
apply (case_tac b)
apply simp
@@ -145,42 +146,46 @@
theorem prop2:
assumes ab: "a \<noteq> b" and bar: "bar xs"
- shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs" using bar
+ shows "\<And>ys zs. bar ys \<Longrightarrow> T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
+ using bar
proof induct
- fix xs zs assume "T a xs zs" and "good xs"
- hence "good zs" by (rule lemma3)
+ fix xs zs
+ assume "T a xs zs" and "good xs"
+ then have "good zs" by (rule lemma3)
then show "bar zs" by (rule bar1)
next
fix xs ys
assume I: "\<And>w ys zs. bar ys \<Longrightarrow> T a (w # xs) zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
assume "bar ys"
- thus "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
+ then show "\<And>zs. T a xs zs \<Longrightarrow> T b ys zs \<Longrightarrow> bar zs"
proof induct
- fix ys zs assume "T b ys zs" and "good ys"
+ fix ys zs
+ assume "T b ys zs" and "good ys"
then have "good zs" by (rule lemma3)
then show "bar zs" by (rule bar1)
next
- fix ys zs assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"
- and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"
+ fix ys zs
+ assume I': "\<And>w zs. T a xs zs \<Longrightarrow> T b (w # ys) zs \<Longrightarrow> bar zs"
+ and ys: "\<And>w. bar (w # ys)" and Ta: "T a xs zs" and Tb: "T b ys zs"
show "bar zs"
proof (rule bar2)
fix w
show "bar (w # zs)"
proof (cases w)
case Nil
- thus ?thesis by simp (rule prop1)
+ then show ?thesis by simp (rule prop1)
next
case (Cons c cs)
from letter_eq_dec show ?thesis
proof
assume ca: "c = a"
from ab have "bar ((a # cs) # zs)" by (iprover intro: I ys Ta Tb)
- thus ?thesis by (simp add: Cons ca)
+ then show ?thesis by (simp add: Cons ca)
next
assume "c \<noteq> a"
with ab have cb: "c = b" by (rule letter_neq)
from ab have "bar ((b # cs) # zs)" by (iprover intro: I' Ta Tb)
- thus ?thesis by (simp add: Cons cb)
+ then show ?thesis by (simp add: Cons cb)
qed
qed
qed
@@ -189,7 +194,8 @@
theorem prop3:
assumes bar: "bar xs"
- shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs" using bar
+ shows "\<And>zs. xs \<noteq> [] \<Longrightarrow> R a xs zs \<Longrightarrow> bar zs"
+ using bar
proof induct
fix xs zs
assume "R a xs zs" and "good xs"
@@ -198,7 +204,7 @@
next
fix xs zs
assume I: "\<And>w zs. w # xs \<noteq> [] \<Longrightarrow> R a (w # xs) zs \<Longrightarrow> bar zs"
- and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs"
+ and xsb: "\<And>w. bar (w # xs)" and xsn: "xs \<noteq> []" and R: "R a xs zs"
show "bar zs"
proof (rule bar2)
fix w
@@ -211,11 +217,11 @@
from letter_eq_dec show ?case
proof
assume "c = a"
- thus ?thesis by (iprover intro: I [simplified] R)
+ then show ?thesis by (iprover intro: I [simplified] R)
next
from R xsn have T: "T a xs zs" by (rule lemma4)
assume "c \<noteq> a"
- thus ?thesis by (iprover intro: prop2 Cons xsb xsn R T)
+ then show ?thesis by (iprover intro: prop2 Cons xsb xsn R T)
qed
qed
qed
@@ -229,58 +235,60 @@
show "bar [[]]" by (rule prop1)
next
fix c cs assume "bar [cs]"
- thus "bar [c # cs]" by (rule prop3) (simp, iprover)
+ then show "bar [c # cs]" by (rule prop3) (simp, iprover)
qed
qed
-primrec
- is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
+primrec is_prefix :: "'a list \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
where
- "is_prefix [] f = True"
- | "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"
+ "is_prefix [] f = True"
+| "is_prefix (x # xs) f = (x = f (length xs) \<and> is_prefix xs f)"
theorem L_idx:
assumes L: "L w ws"
- shows "is_prefix ws f \<Longrightarrow> \<exists>i. emb (f i) w \<and> i < length ws" using L
+ shows "is_prefix ws f \<Longrightarrow> \<exists>i. emb (f i) w \<and> i < length ws"
+ using L
proof induct
case (L0 v ws)
- hence "emb (f (length ws)) w" by simp
+ then have "emb (f (length ws)) w" by simp
moreover have "length ws < length (v # ws)" by simp
ultimately show ?case by iprover
next
case (L1 ws v)
then obtain i where emb: "emb (f i) w" and "i < length ws"
by simp iprover
- hence "i < length (v # ws)" by simp
+ then have "i < length (v # ws)" by simp
with emb show ?case by iprover
qed
theorem good_idx:
assumes good: "good ws"
- shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using good
+ shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j"
+ using good
proof induct
case (good0 w ws)
- hence "w = f (length ws)" and "is_prefix ws f" by simp_all
+ then have "w = f (length ws)" and "is_prefix ws f" by simp_all
with good0 show ?case by (iprover dest: L_idx)
next
case (good1 ws w)
- thus ?case by simp
+ then show ?case by simp
qed
theorem bar_idx:
assumes bar: "bar ws"
- shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j" using bar
+ shows "is_prefix ws f \<Longrightarrow> \<exists>i j. emb (f i) (f j) \<and> i < j"
+ using bar
proof induct
case (bar1 ws)
- thus ?case by (rule good_idx)
+ then show ?case by (rule good_idx)
next
case (bar2 ws)
- hence "is_prefix (f (length ws) # ws) f" by simp
- thus ?case by (rule bar2)
+ then have "is_prefix (f (length ws) # ws) f" by simp
+ then show ?case by (rule bar2)
qed
text \<open>
-Strong version: yields indices of words that can be embedded into each other.
+ Strong version: yields indices of words that can be embedded into each other.
\<close>
theorem higman_idx: "\<exists>(i::nat) j. emb (f i) (f j) \<and> i < j"
@@ -290,26 +298,25 @@
qed
text \<open>
-Weak version: only yield sequence containing words
-that can be embedded into each other.
+ Weak version: only yield sequence containing words
+ that can be embedded into each other.
\<close>
theorem good_prefix_lemma:
assumes bar: "bar ws"
- shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> good vs" using bar
+ shows "is_prefix ws f \<Longrightarrow> \<exists>vs. is_prefix vs f \<and> good vs"
+ using bar
proof induct
case bar1
- thus ?case by iprover
+ then show ?case by iprover
next
case (bar2 ws)
from bar2.prems have "is_prefix (f (length ws) # ws) f" by simp
- thus ?case by (iprover intro: bar2)
+ then show ?case by (iprover intro: bar2)
qed
theorem good_prefix: "\<exists>vs. is_prefix vs f \<and> good vs"
using higman
by (rule good_prefix_lemma) simp+
-(*<*)
end
-(*>*)
--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy Fri Jul 01 16:52:35 2016 +0200
@@ -3,13 +3,11 @@
Author: Monika Seisenberger, LMU Muenchen
*)
-(*<*)
+subsection \<open>Extracting the program\<close>
+
theory Higman_Extraction
imports Higman "~~/src/HOL/Library/State_Monad" Random
begin
-(*>*)
-
-subsection \<open>Extracting the program\<close>
declare R.induct [ind_realizer]
declare T.induct [ind_realizer]
@@ -48,7 +46,8 @@
end
-function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
+function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed"
+where
"mk_word_aux k = exec {
i \<leftarrow> Random.range 10;
(if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
@@ -57,54 +56,58 @@
ls \<leftarrow> mk_word_aux (Suc k);
Pair (l # ls)
})}"
-by pat_completeness auto
-termination by (relation "measure ((op -) 1001)") auto
+ by pat_completeness auto
+termination
+ by (relation "measure ((op -) 1001)") auto
-definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
- "mk_word = mk_word_aux 0"
+definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed"
+ where "mk_word = mk_word_aux 0"
-primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
+primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed"
+where
"mk_word_s 0 = mk_word"
- | "mk_word_s (Suc n) = exec {
- _ \<leftarrow> mk_word;
- mk_word_s n
- }"
+| "mk_word_s (Suc n) = exec {
+ _ \<leftarrow> mk_word;
+ mk_word_s n
+ }"
-definition g1 :: "nat \<Rightarrow> letter list" where
- "g1 s = fst (mk_word_s s (20000, 1))"
+definition g1 :: "nat \<Rightarrow> letter list"
+ where "g1 s = fst (mk_word_s s (20000, 1))"
-definition g2 :: "nat \<Rightarrow> letter list" where
- "g2 s = fst (mk_word_s s (50000, 1))"
+definition g2 :: "nat \<Rightarrow> letter list"
+ where "g2 s = fst (mk_word_s s (50000, 1))"
-fun f1 :: "nat \<Rightarrow> letter list" where
+fun f1 :: "nat \<Rightarrow> letter list"
+where
"f1 0 = [A, A]"
- | "f1 (Suc 0) = [B]"
- | "f1 (Suc (Suc 0)) = [A, B]"
- | "f1 _ = []"
+| "f1 (Suc 0) = [B]"
+| "f1 (Suc (Suc 0)) = [A, B]"
+| "f1 _ = []"
-fun f2 :: "nat \<Rightarrow> letter list" where
+fun f2 :: "nat \<Rightarrow> letter list"
+where
"f2 0 = [A, A]"
- | "f2 (Suc 0) = [B]"
- | "f2 (Suc (Suc 0)) = [B, A]"
- | "f2 _ = []"
+| "f2 (Suc 0) = [B]"
+| "f2 (Suc (Suc 0)) = [B, A]"
+| "f2 _ = []"
ML_val \<open>
-local
- val higman_idx = @{code higman_idx};
- val g1 = @{code g1};
- val g2 = @{code g2};
- val f1 = @{code f1};
- val f2 = @{code f2};
-in
- val (i1, j1) = higman_idx g1;
- val (v1, w1) = (g1 i1, g1 j1);
- val (i2, j2) = higman_idx g2;
- val (v2, w2) = (g2 i2, g2 j2);
- val (i3, j3) = higman_idx f1;
- val (v3, w3) = (f1 i3, f1 j3);
- val (i4, j4) = higman_idx f2;
- val (v4, w4) = (f2 i4, f2 j4);
-end;
+ local
+ val higman_idx = @{code higman_idx};
+ val g1 = @{code g1};
+ val g2 = @{code g2};
+ val f1 = @{code f1};
+ val f2 = @{code f2};
+ in
+ val (i1, j1) = higman_idx g1;
+ val (v1, w1) = (g1 i1, g1 j1);
+ val (i2, j2) = higman_idx g2;
+ val (v2, w2) = (g2 i2, g2 j2);
+ val (i3, j3) = higman_idx f1;
+ val (v3, w3) = (f1 i3, f1 j3);
+ val (i4, j4) = higman_idx f2;
+ val (v4, w4) = (f2 i4, f2 j4);
+ end;
\<close>
end
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Fri Jul 01 16:52:35 2016 +0200
@@ -9,131 +9,126 @@
begin
text \<open>
-We formalize two proofs of the pigeonhole principle, which lead
-to extracted programs of quite different complexity. The original
-formalization of these proofs in {\sc Nuprl} is due to
-Aleksey Nogin @{cite "Nogin-ENTCS-2000"}.
+ We formalize two proofs of the pigeonhole principle, which lead
+ to extracted programs of quite different complexity. The original
+ formalization of these proofs in {\sc Nuprl} is due to
+ Aleksey Nogin @{cite "Nogin-ENTCS-2000"}.
-This proof yields a polynomial program.
+ This proof yields a polynomial program.
\<close>
theorem pigeonhole:
"\<And>f. (\<And>i. i \<le> Suc n \<Longrightarrow> f i \<le> n) \<Longrightarrow> \<exists>i j. i \<le> Suc n \<and> j < i \<and> f i = f j"
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 iprover
+ then have "Suc 0 \<le> Suc 0 \<and> 0 < Suc 0 \<and> f (Suc 0) = f 0" by simp
+ then show ?case by iprover
next
case (Suc n)
- {
- fix k
- have
- "k \<le> Suc (Suc n) \<Longrightarrow>
- (\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow>
- (\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)"
- proof (induct k)
- case 0
- let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
- have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)"
- 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 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
+ have r:
+ "k \<le> Suc (Suc n) \<Longrightarrow>
+ (\<And>i j. Suc k \<le> i \<Longrightarrow> i \<le> Suc (Suc n) \<Longrightarrow> j < i \<Longrightarrow> f i \<noteq> f j) \<Longrightarrow>
+ (\<exists>i j. i \<le> k \<and> j < i \<and> f i = f j)" for k
+ proof (induct k)
+ case 0
+ let ?f = "\<lambda>i. if f i = Suc n then f (Suc (Suc n)) else f i"
+ have "\<not> (\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j)"
+ 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 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
+ show False
+ proof cases
+ assume fi: "f i = Suc n"
+ show False
+ proof cases
+ assume fj: "f j = Suc n"
+ from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0)
+ moreover from fi have "f i = f j"
+ by (simp add: fj [symmetric])
+ ultimately show ?thesis ..
+ next
+ from i and j have "j < Suc (Suc n)" by simp
+ with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j"
+ by (rule 0)
+ moreover assume "f j \<noteq> Suc n"
+ with fi and f have "f (Suc (Suc n)) = f j" by simp
+ ultimately show False ..
+ qed
+ next
+ assume fi: "f i \<noteq> Suc n"
show False
proof cases
- assume fi: "f i = Suc n"
- show False
- proof cases
- assume fj: "f j = Suc n"
- from i_nz and iSSn and j have "f i \<noteq> f j" by (rule 0)
- moreover from fi have "f i = f j"
- by (simp add: fj [symmetric])
- ultimately show ?thesis ..
- next
- from i and j have "j < Suc (Suc n)" by simp
- with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f j"
- by (rule 0)
- moreover assume "f j \<noteq> Suc n"
- with fi and f have "f (Suc (Suc n)) = f j" by simp
- ultimately show False ..
+ from i have "i < Suc (Suc n)" by simp
+ with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f i"
+ by (rule 0)
+ moreover assume "f j = Suc n"
+ with fi and f have "f (Suc (Suc n)) = f i" by simp
+ ultimately show False ..
+ next
+ from i_nz and iSSn and j
+ have "f i \<noteq> f j" by (rule 0)
+ moreover assume "f j \<noteq> Suc n"
+ with fi and f have "f i = f j" by simp
+ ultimately show False ..
+ qed
+ qed
+ qed
+ moreover have "?f i \<le> n" if "i \<le> Suc n" for i
+ proof -
+ from that have i: "i < Suc (Suc n)" by simp
+ have "f (Suc (Suc n)) \<noteq> f i"
+ by (rule 0) (simp_all add: i)
+ moreover have "f (Suc (Suc n)) \<le> Suc n"
+ by (rule Suc) simp
+ moreover from i have "i \<le> Suc (Suc n)" by simp
+ then have "f i \<le> Suc n" by (rule Suc)
+ ultimately show ?thesis
+ by simp
+ qed
+ then have "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
+ by (rule Suc)
+ ultimately show ?case ..
+ next
+ case (Suc k)
+ from search [OF nat_eq_dec] show ?case
+ proof
+ assume "\<exists>j<Suc k. f (Suc k) = f j"
+ then show ?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"
+ proof (rule Suc)
+ from Suc show "k \<le> Suc (Suc n)" by simp
+ fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)"
+ and j: "j < i"
+ show "f i \<noteq> f j"
+ proof cases
+ assume eq: "i = Suc k"
+ show ?thesis
+ proof
+ assume "f i = f j"
+ then have "f (Suc k) = f j" by (simp add: eq)
+ with nex and j and eq show False by iprover
qed
next
- assume fi: "f i \<noteq> Suc n"
- show False
- proof cases
- from i have "i < Suc (Suc n)" by simp
- with S0SSn and le_refl have "f (Suc (Suc n)) \<noteq> f i"
- by (rule 0)
- moreover assume "f j = Suc n"
- with fi and f have "f (Suc (Suc n)) = f i" by simp
- ultimately show False ..
- next
- from i_nz and iSSn and j
- have "f i \<noteq> f j" by (rule 0)
- moreover assume "f j \<noteq> Suc n"
- with fi and f have "f i = f j" by simp
- ultimately show False ..
- qed
+ assume "i \<noteq> Suc k"
+ with k have "Suc (Suc k) \<le> i" by simp
+ then show ?thesis using i and j by (rule Suc)
qed
qed
- moreover have "\<And>i. i \<le> Suc n \<Longrightarrow> ?f i \<le> n"
- proof -
- fix i assume "i \<le> Suc n"
- hence i: "i < Suc (Suc n)" by simp
- have "f (Suc (Suc n)) \<noteq> f i"
- by (rule 0) (simp_all add: i)
- moreover have "f (Suc (Suc n)) \<le> Suc n"
- by (rule Suc) simp
- moreover from i have "i \<le> Suc (Suc n)" by simp
- hence "f i \<le> Suc n" by (rule Suc)
- ultimately show "?thesis i"
- by simp
- qed
- hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j"
- by (rule Suc)
- ultimately show ?case ..
- next
- case (Suc k)
- from search [OF nat_eq_dec] show ?case
- proof
- assume "\<exists>j<Suc k. f (Suc k) = f j"
- 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"
- proof (rule Suc)
- from Suc show "k \<le> Suc (Suc n)" by simp
- fix i j assume k: "Suc k \<le> i" and i: "i \<le> Suc (Suc n)"
- and j: "j < i"
- show "f i \<noteq> f j"
- proof cases
- assume eq: "i = Suc k"
- show ?thesis
- 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 iprover
- qed
- next
- assume "i \<noteq> Suc k"
- with k have "Suc (Suc k) \<le> i" by simp
- thus ?thesis using i and j by (rule Suc)
- qed
- qed
- thus ?thesis by (iprover intro: le_SucI)
- qed
+ then show ?thesis by (iprover intro: le_SucI)
qed
- }
- note r = this
+ qed
show ?case by (rule r) simp_all
qed
text \<open>
-The following proof, although quite elegant from a mathematical point of view,
-leads to an exponential program:
+ The following proof, although quite elegant from a mathematical point of view,
+ leads to an exponential program:
\<close>
theorem pigeonhole_slow:
@@ -149,10 +144,10 @@
from search [OF nat_eq_dec] show ?case
proof
assume "\<exists>j < Suc (Suc n). f (Suc (Suc n)) = f j"
- thus ?case by (iprover intro: le_refl)
+ then show ?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 iprover
+ then have 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 -
@@ -171,7 +166,7 @@
with False show ?thesis by simp
qed
qed
- hence "\<exists>i j. i \<le> Suc n \<and> j < i \<and> ?f i = ?f j" by (rule Suc)
+ then have "\<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 iprover
have "f i = f j"
@@ -206,16 +201,16 @@
extract pigeonhole pigeonhole_slow
text \<open>
-The programs extracted from the above proofs look as follows:
-@{thm [display] pigeonhole_def}
-@{thm [display] pigeonhole_slow_def}
-The program for searching for an element in an array is
-@{thm [display,eta_contract=false] search_def}
-The correctness statement for @{term "pigeonhole"} is
-@{thm [display] pigeonhole_correctness [no_vars]}
+ The programs extracted from the above proofs look as follows:
+ @{thm [display] pigeonhole_def}
+ @{thm [display] pigeonhole_slow_def}
+ The program for searching for an element in an array is
+ @{thm [display,eta_contract=false] search_def}
+ The correctness statement for @{term "pigeonhole"} is
+ @{thm [display] pigeonhole_correctness [no_vars]}
-In order to analyze the speed of the above programs,
-we generate ML code from them.
+ In order to analyze the speed of the above programs,
+ we generate ML code from them.
\<close>
instantiation nat :: default
@@ -236,14 +231,11 @@
end
-definition
- "test n u = pigeonhole (nat_of_integer n) (\<lambda>m. m - 1)"
-definition
- "test' n u = pigeonhole_slow (nat_of_integer n) (\<lambda>m. m - 1)"
-definition
- "test'' u = pigeonhole 8 (List.nth [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
+definition "test n u = pigeonhole (nat_of_integer n) (\<lambda>m. m - 1)"
+definition "test' n u = pigeonhole_slow (nat_of_integer n) (\<lambda>m. m - 1)"
+definition "test'' u = pigeonhole 8 (List.nth [0, 1, 2, 3, 4, 5, 6, 3, 7, 8])"
-ML_val "timeit (@{code test} 10)"
+ML_val "timeit (@{code test} 10)"
ML_val "timeit (@{code test'} 10)"
ML_val "timeit (@{code test} 20)"
ML_val "timeit (@{code test'} 20)"
--- a/src/HOL/Proofs/Extraction/QuotRem.thy Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/QuotRem.thy Fri Jul 01 16:52:35 2016 +0200
@@ -14,7 +14,7 @@
proof (induct a)
case 0
have "0 = Suc b * 0 + 0 \<and> 0 \<le> b" by simp
- thus ?case by iprover
+ then show ?case by iprover
next
case (Suc a)
then obtain r q where I: "a = Suc b * q + r" and "r \<le> b" by iprover
@@ -22,12 +22,12 @@
proof
assume "r = b"
with I have "Suc a = Suc b * (Suc q) + 0 \<and> 0 \<le> b" by simp
- thus ?case by iprover
+ then show ?case by iprover
next
assume "r \<noteq> b"
with \<open>r \<le> b\<close> have "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 iprover
+ then show ?case by iprover
qed
qed
--- a/src/HOL/Proofs/Extraction/Util.thy Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Util.thy Fri Jul 01 16:52:35 2016 +0200
@@ -8,9 +8,7 @@
imports "~~/src/HOL/Library/Old_Datatype"
begin
-text \<open>
-Decidability of equality on natural numbers.
-\<close>
+text \<open>Decidability of equality on natural numbers.\<close>
lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
apply (induct m)
@@ -20,8 +18,8 @@
done
text \<open>
-Well-founded induction on natural numbers, derived using the standard
-structural induction rule.
+ Well-founded induction on natural numbers, derived using the standard
+ structural induction rule.
\<close>
lemma nat_wf_ind:
@@ -31,7 +29,7 @@
show "\<And>y. y < z \<Longrightarrow> P y"
proof (induct z)
case 0
- thus ?case by simp
+ then show ?case by simp
next
case (Suc n y)
from nat_eq_dec show ?case
@@ -43,23 +41,22 @@
next
assume "n \<noteq> y"
with Suc have "y < n" by simp
- thus ?case by (rule Suc)
+ then show ?case by (rule Suc)
qed
qed
qed
-text \<open>
-Bounded search for a natural number satisfying a decidable predicate.
-\<close>
+text \<open>Bounded search for a natural number satisfying a decidable predicate.\<close>
lemma search:
assumes dec: "\<And>x::nat. P x \<or> \<not> P x"
shows "(\<exists>x<y. P x) \<or> \<not> (\<exists>x<y. P x)"
proof (induct y)
- case 0 show ?case by simp
+ case 0
+ show ?case by simp
next
case (Suc z)
- thus ?case
+ then show ?case
proof
assume "\<exists>x<z. P x"
then obtain x where le: "x < z" and P: "P x" by iprover
@@ -89,7 +86,7 @@
with P have "\<exists>x<z. P x" by iprover
with nex show False ..
qed
- thus ?case by iprover
+ then show ?case by iprover
qed
qed
qed
--- a/src/HOL/Proofs/Extraction/Warshall.thy Fri Jul 01 10:56:54 2016 +0200
+++ b/src/HOL/Proofs/Extraction/Warshall.thy Fri Jul 01 16:52:35 2016 +0200
@@ -15,34 +15,27 @@
datatype b = T | F
-primrec
- is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
-where
- "is_path' r x [] z = (r x z = T)"
- | "is_path' r x (y # ys) z = (r x y = T \<and> is_path' r y ys z)"
-
-definition
- is_path :: "(nat \<Rightarrow> nat \<Rightarrow> b) \<Rightarrow> (nat * nat list * nat) \<Rightarrow>
- nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+primrec is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
where
- "is_path r p i j k \<longleftrightarrow> fst p = j \<and> snd (snd p) = k \<and>
- list_all (\<lambda>x. x < i) (fst (snd p)) \<and>
- is_path' r (fst p) (fst (snd p)) (snd (snd p))"
+ "is_path' r x [] z \<longleftrightarrow> r x z = T"
+| "is_path' r x (y # ys) z \<longleftrightarrow> r x y = T \<and> is_path' r y ys z"
-definition
- conc :: "('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a) \<Rightarrow> ('a * 'a list * 'a)"
-where
- "conc p q = (fst p, fst (snd p) @ fst q # fst (snd q), snd (snd q))"
+definition is_path :: "(nat \<Rightarrow> nat \<Rightarrow> b) \<Rightarrow> (nat * nat list * nat) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
+ where "is_path r p i j k \<longleftrightarrow>
+ fst p = j \<and> snd (snd p) = k \<and>
+ list_all (\<lambda>x. x < i) (fst (snd p)) \<and>
+ is_path' r (fst p) (fst (snd p)) (snd (snd p))"
-theorem is_path'_snoc [simp]:
- "\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
+definition conc :: "'a \<times> 'a list \<times> 'a \<Rightarrow> 'a \<times> 'a list \<times> 'a \<Rightarrow> 'a \<times> 'a list * 'a"
+ where "conc p q = (fst p, fst (snd p) @ fst q # fst (snd q), snd (snd q))"
+
+theorem is_path'_snoc [simp]: "\<And>x. is_path' r x (ys @ [y]) z = (is_path' r x ys y \<and> r y z = T)"
by (induct ys) simp+
theorem list_all_scoc [simp]: "list_all P (xs @ [x]) \<longleftrightarrow> P x \<and> list_all P xs"
- by (induct xs, simp+, iprover)
+ 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"
+theorem list_all_lemma: "list_all P xs \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> list_all Q xs"
proof -
assume PQ: "\<And>x. P x \<Longrightarrow> Q x"
show "list_all P xs \<Longrightarrow> list_all Q xs"
@@ -51,7 +44,7 @@
show ?case by simp
next
case (Cons y ys)
- hence Py: "P y" by simp
+ then have Py: "P y" by simp
from Cons have Pys: "list_all P ys" by simp
show ?case
by simp (rule conjI PQ Py Cons Pys)+
@@ -59,7 +52,7 @@
qed
theorem lemma1: "\<And>p. is_path r p i j k \<Longrightarrow> is_path r p (Suc i) j k"
- apply (unfold is_path_def)
+ unfolding is_path_def
apply (simp cong add: conj_cong add: split_paired_all)
apply (erule conjE)+
apply (erule list_all_lemma)
@@ -67,7 +60,7 @@
done
theorem lemma2: "\<And>p. is_path r p 0 j k \<Longrightarrow> r j k = T"
- apply (unfold is_path_def)
+ unfolding is_path_def
apply (simp cong add: conj_cong add: split_paired_all)
apply (case_tac "aa")
apply simp+
@@ -80,11 +73,11 @@
show "\<And>j. is_path' r j xs i \<Longrightarrow> is_path' r j (xs @ i # ys) k"
proof (induct xs)
case (Nil j)
- hence "r j i = T" by simp
+ then have "r j i = T" by simp
with pys show ?case by simp
next
case (Cons z zs j)
- hence jzr: "r j z = T" by simp
+ then have jzr: "r j z = T" by simp
from Cons have pzs: "is_path' r z zs i" by simp
show ?case
by simp (rule conjI jzr Cons pzs)+
@@ -93,7 +86,7 @@
theorem lemma3:
"\<And>p q. is_path r p i j i \<Longrightarrow> is_path r q i i k \<Longrightarrow>
- is_path r (conc p q) (Suc i) j k"
+ is_path r (conc p q) (Suc i) j k"
apply (unfold is_path_def conc_def)
apply (simp cong add: conj_cong add: split_paired_all)
apply (erule conjE)+
@@ -108,8 +101,8 @@
done
theorem lemma5:
- "\<And>p. is_path r p (Suc i) j k \<Longrightarrow> ~ is_path r p i j k \<Longrightarrow>
- (\<exists>q. is_path r q i j i) \<and> (\<exists>q'. is_path r q' i i k)"
+ "\<And>p. is_path r p (Suc i) j k \<Longrightarrow> \<not> is_path r p i j k \<Longrightarrow>
+ (\<exists>q. is_path r q i j i) \<and> (\<exists>q'. is_path r q' i i k)"
proof (simp cong add: conj_cong add: split_paired_all is_path_def, (erule conjE)+)
fix xs
assume asms:
@@ -124,7 +117,7 @@
\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i" (is "PROP ?ih xs")
proof (induct xs)
case Nil
- thus ?case by simp
+ then show ?case by simp
next
case (Cons a as j)
show ?case
@@ -133,7 +126,7 @@
show ?thesis
proof
from True and Cons have "r j i = T" by simp
- thus "list_all (\<lambda>x. x < i) [] \<and> is_path' r j [] i" by simp
+ then show "list_all (\<lambda>x. x < i) [] \<and> is_path' r j [] i" by simp
qed
next
case False
@@ -157,7 +150,7 @@
\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k" (is "PROP ?ih xs")
proof (induct xs rule: rev_induct)
case Nil
- thus ?case by simp
+ then show ?case by simp
next
case (snoc a as k)
show ?case
@@ -166,7 +159,7 @@
show ?thesis
proof
from True and snoc have "r i k = T" by simp
- thus "list_all (\<lambda>x. x < i) [] \<and> is_path' r i [] k" by simp
+ then show "list_all (\<lambda>x. x < i) [] \<and> is_path' r i [] k" by simp
qed
next
case False
@@ -191,30 +184,29 @@
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)"
+ \<not> (\<forall>q. \<not> is_path r q i j i) \<and> \<not> (\<forall>q'. \<not> is_path r q' i i k)"
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)"
+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)"
proof (induct i)
case (0 j k)
show ?case
proof (cases "r j k")
assume "r j k = T"
- hence "is_path r (j, [], k) 0 j k"
+ then have "is_path r (j, [], k) 0 j k"
by (simp add: is_path_def)
- hence "\<exists>p. is_path r p 0 j k" ..
- thus ?thesis ..
+ then have "\<exists>p. is_path r p 0 j k" ..
+ then show ?thesis ..
next
assume "r j k = F"
- hence "r j k ~= T" by simp
- hence "\<not> (\<exists>p. is_path r p 0 j k)"
+ then have "r j k \<noteq> T" by simp
+ then have "\<not> (\<exists>p. is_path r p 0 j k)"
by (iprover dest: lemma2)
- thus ?thesis ..
+ then show ?thesis ..
qed
next
case (Suc i j k)
- thus ?case
+ then show ?case
proof
assume h1: "\<not> (\<exists>p. is_path r p i j k)"
from Suc show ?case
@@ -222,7 +214,7 @@
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 (iprover dest: lemma5')
- thus ?case ..
+ then show ?case ..
next
assume "\<exists>p. is_path r p i j i"
then obtain p where h2: "is_path r p i j i" ..
@@ -231,21 +223,21 @@
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 (iprover dest: lemma5')
- thus ?case ..
+ then show ?case ..
next
assume "\<exists>q. is_path r q i i k"
then obtain q where "is_path r q i i k" ..
with h2 have "is_path r (conc p q) (Suc i) j k"
by (rule lemma3)
- hence "\<exists>pq. is_path r pq (Suc i) j k" ..
- thus ?case ..
+ then have "\<exists>pq. is_path r pq (Suc i) j k" ..
+ then show ?case ..
qed
qed
next
assume "\<exists>p. is_path r p i j k"
- hence "\<exists>p. is_path r p (Suc i) j k"
+ then have "\<exists>p. is_path r p (Suc i) j k"
by (iprover intro: lemma1)
- thus ?case ..
+ then show ?case ..
qed
qed