--- a/src/Doc/Prog_Prove/Isar.thy Mon Apr 03 23:12:16 2017 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy Mon Apr 03 23:12:44 2017 +0200
@@ -227,6 +227,10 @@
default. The patterns are phrased in terms of \isacom{show} but work for
\isacom{have} and \isacom{lemma}, too.
+\ifsem\else
+\subsection{Logic}
+\fi
+
We start with two forms of \concept{case analysis}:
starting from a formula @{text P} we have the two cases @{text P} and
@{prop"~P"}, and starting from a fact @{prop"P \<or> Q"}
@@ -241,11 +245,11 @@
proof cases
assume "P"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "R" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
next
assume "\<not> P"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "R" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
qed(*<*)oops(*>*)
text_raw {* }
\end{minipage}\index{cases@@{text cases}}
@@ -254,16 +258,16 @@
\isa{%
*}
(*<*)lemma "R" proof-(*>*)
-have "P \<or> Q" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+have "P \<or> Q" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
then show "R"
proof
assume "P"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "R" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
next
assume "Q"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "R" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
qed(*<*)oops(*>*)
text_raw {* }
@@ -280,11 +284,11 @@
proof
assume "P"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "Q" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
+ show "Q" (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
next
assume "Q"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "P" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
+ show "P" (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
qed(*<*)qed(*>*)
text_raw {* }
\medskip
@@ -300,7 +304,7 @@
proof
assume "P"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "False" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "False" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
qed(*<*)oops(*>*)
text_raw {* }
@@ -314,7 +318,7 @@
proof (rule ccontr)
assume "\<not>P"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "False" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "False" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
qed(*<*)oops(*>*)
text_raw {* }
@@ -333,7 +337,7 @@
proof
fix x
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "P(x)" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "P(x)" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
qed(*<*)oops(*>*)
text_raw {* }
@@ -346,7 +350,7 @@
show "\<exists>x. P(x)"
proof
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "P(witness)" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "P(witness)" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
qed
(*<*)oops(*>*)
@@ -367,7 +371,7 @@
\end{isamarkuptext}%
*}
(*<*)lemma True proof- assume 1: "EX x. P x"(*>*)
-have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)text_raw{*\ $\dots$\\*}
+have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)text_raw{*\ \isasymproof\\*}
then obtain x where p: "P(x)" by blast
(*<*)oops(*>*)
text{*
@@ -401,9 +405,9 @@
(*<*)lemma "A = (B::'a set)" proof-(*>*)
show "A = B"
proof
- show "A \<subseteq> B" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "A \<subseteq> B" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
next
- show "B \<subseteq> A" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "B \<subseteq> A" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
qed(*<*)qed(*>*)
text_raw {* }
@@ -418,13 +422,92 @@
fix x
assume "x \<in> A"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "x \<in> B" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show "x \<in> B" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
qed(*<*)qed(*>*)
text_raw {* }
\end{minipage}
\end{tabular}
\begin{isamarkuptext}%
+
+\ifsem\else
+\subsection{Chains of (In)Equations}
+
+In textbooks, chains of equations (and inequations) are often displayed like this:
+\begin{quote}
+\begin{tabular}{@ {}l@ {\qquad}l@ {}}
+$t_1 = t_2$ & \isamath{\,\langle\mathit{justification}\rangle}\\
+$\phantom{t_1} = t_3$ & \isamath{\,\langle\mathit{justification}\rangle}\\
+\quad $\vdots$\\
+$\phantom{t_1} = t_n$ & \isamath{\,\langle\mathit{justification}\rangle}
+\end{tabular}
+\end{quote}
+The Isar equivalent is this:
+
+\begin{samepage}
+\begin{quote}
+\isakeyword{have} \<open>"t\<^sub>1 = t\<^sub>2"\<close> \isasymproof\\
+\isakeyword{also have} \<open>"... = t\<^sub>3"\<close> \isasymproof\\
+\quad $\vdots$\\
+\isakeyword{also have} \<open>"... = t\<^sub>n"\<close> \isasymproof \\
+\isakeyword{finally show} \<open>"t\<^sub>1 = t\<^sub>n"\<close>\ \texttt{.}
+\end{quote}
+\end{samepage}
+
+\noindent
+The ``\<open>...\<close>'' and ``\<open>.\<close>'' deserve some explanation:
+\begin{description}
+\item[``\<open>...\<close>''] is literally three dots. It is the name of an unknown that Isar
+automatically instantiates with the right-hand side of the previous equation.
+In general, if \<open>this\<close> is the theorem @{term "p t\<^sub>1 t\<^sub>2"} then ``\<open>...\<close>''
+stands for \<open>t\<^sub>2\<close>.
+\item[``\<open>.\<close>''] (a single dot) is a proof method that solves a goal by one of the
+assumptions. This works here because the result of \isakeyword{finally}
+is the theorem \mbox{\<open>t\<^sub>1 = t\<^sub>n\<close>},
+\isakeyword{show} \<open>"t\<^sub>1 = t\<^sub>n"\<close> states the theorem explicitly,
+and ``\<open>.\<close>'' proves the theorem with the result of \isakeyword{finally}.
+\end{description}
+The above proof template also works for arbitrary mixtures of \<open>=\<close>, \<open>\<le>\<close> and \<open><\<close>,
+for example:
+\begin{quote}
+\isakeyword{have} \<open>"t\<^sub>1 < t\<^sub>2"\<close> \isasymproof\\
+\isakeyword{also have} \<open>"... = t\<^sub>3"\<close> \isasymproof\\
+\quad $\vdots$\\
+\isakeyword{also have} \<open>"... \<le> t\<^sub>n"\<close> \isasymproof \\
+\isakeyword{finally show} \<open>"t\<^sub>1 < t\<^sub>n"\<close>\ \texttt{.}
+\end{quote}
+The relation symbol in the \isakeyword{finally} step needs to be the most precise one
+possible. In the example above, you must not write \<open>t\<^sub>1 \<le> t\<^sub>n\<close> instead of \mbox{\<open>t\<^sub>1 < t\<^sub>n\<close>}.
+
+\begin{warn}
+Isabelle only supports \<open>=\<close>, \<open>\<le>\<close> and \<open><\<close> but not \<open>\<ge>\<close> and \<open>>\<close>
+in (in)equation chains (by default).
+\end{warn}
+
+If you want to go beyond merely using the above proof patterns and want to
+understand what \isakeyword{also} and \isakeyword{finally} mean, read on.
+There is an Isar theorem variable called \<open>calculation\<close>, similar to \<open>this\<close>.
+When the first \isakeyword{also} in a chain is encountered, Isabelle sets
+\<open>calculation := this\<close>. In each subsequent \isakeyword{also} step,
+Isabelle composes the theorems \<open>calculation\<close> and \<open>this\<close> (i.e.\ the two previous
+(in)equalities) using some predefined set of rules including transitivity
+of \<open>=\<close>, \<open>\<le>\<close> and \<open><\<close> but also mixed rules like @{prop"\<lbrakk> x \<le> y; y < z \<rbrakk> \<Longrightarrow> x < z"}.
+The result of this composition is assigned to \<open>calculation\<close>. Consider
+\begin{quote}
+\isakeyword{have} \<open>"t\<^sub>1 \<le> t\<^sub>2"\<close> \isasymproof\\
+\isakeyword{also} \isakeyword{have} \<open>"... < t\<^sub>3"\<close> \isasymproof\\
+\isakeyword{also} \isakeyword{have} \<open>"... = t\<^sub>4"\<close> \isasymproof\\
+\isakeyword{finally show} \<open>"t\<^sub>1 < t\<^sub>4"\<close>\ \texttt{.}
+\end{quote}
+After the first \isakeyword{also}, \<open>calculation\<close> is \<open>"t\<^sub>1 \<le> t\<^sub>2"\<close>,
+and after the second \isakeyword{also}, \<open>calculation\<close> is \<open>"t\<^sub>1 < t\<^sub>3"\<close>.
+The command \isakeyword{finally} is short for \isakeyword{also from} \<open>calculation\<close>.
+Therefore the \isakeyword{also} hidden in \isakeyword{finally} sets \<open>calculation\<close>
+to \<open>t\<^sub>1 < t\<^sub>4\<close> and the final ``\texttt{.}'' succeeds.
+
+For more information on this style of proof see \cite{BauerW-TPHOLs01}.
+\fi
+
\section{Streamlining Proofs}
\subsection{Pattern Matching and Quotations}
@@ -445,11 +528,11 @@
proof
assume "?L"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "?R" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
+ show "?R" (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
next
assume "?R"
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show "?L" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
+ show "?L" (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
qed(*<*)qed(*>*)
text{* Instead of duplicating @{text"formula\<^sub>i"} in the text, we introduce
@@ -463,7 +546,7 @@
lemma "formula"
proof -
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*}
- show ?thesis (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
+ show ?thesis (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
qed
text{*
@@ -511,12 +594,12 @@
\isa{%
*}
(*<*)lemma "P" proof-(*>*)
-have "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
-moreover have "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+have "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
+moreover have "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
moreover
text_raw{*\\$\vdots$\\\hspace{-1.4ex}*}(*<*)have "True" ..(*>*)
-moreover have "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
-ultimately have "P" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+moreover have "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
+ultimately have "P" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
(*<*)oops(*>*)
text_raw {* }
@@ -527,20 +610,20 @@
\isa{%
*}
(*<*)lemma "P" proof-(*>*)
-have lab\<^sub>1: "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
-have lab\<^sub>2: "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ $\dots$*}
+have lab\<^sub>1: "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
+have lab\<^sub>2: "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ \isasymproof*}
text_raw{*\\$\vdots$\\\hspace{-1.4ex}*}
-have lab\<^sub>n: "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+have lab\<^sub>n: "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
from lab\<^sub>1 lab\<^sub>2 text_raw{*\ $\dots$\\*}
-have "P" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+have "P" (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
(*<*)oops(*>*)
text_raw {* }
\end{minipage}
\end{tabular}
\begin{isamarkuptext}%
-The \isacom{moreover} version is no shorter but expresses the structure more
-clearly and avoids new names.
+The \isacom{moreover} version is no shorter but expresses the structure
+a bit more clearly and avoids new names.
\subsection{Raw Proof Blocks}
@@ -550,9 +633,9 @@
variables at the end. This is what a \concept{raw proof block} does:
\begin{quote}\index{$IMP053@@{text"{ ... }"} (proof block)}
@{text"{"} \isacom{fix} @{text"x\<^sub>1 \<dots> x\<^sub>n"}\\
-\mbox{}\ \ \ \isacom{assume} @{text"A\<^sub>1 \<dots> A\<^sub>m"}\\
-\mbox{}\ \ \ $\vdots$\\
-\mbox{}\ \ \ \isacom{have} @{text"B"}\\
+\mbox{}\ \ \isacom{assume} @{text"A\<^sub>1 \<dots> A\<^sub>m"}\\
+\mbox{}\ \ $\vdots$\\
+\mbox{}\ \ \isacom{have} @{text"B"}\ \isasymproof\\
@{text"}"}
\end{quote}
proves @{text"\<lbrakk> A\<^sub>1; \<dots> ; A\<^sub>m \<rbrakk> \<Longrightarrow> B"}
@@ -734,11 +817,11 @@
proof (induction n)
case 0
text_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
- show ?case (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
+ show ?case (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
next
case (Suc n)
text_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*}
- show ?case (*<*)sorry(*>*) text_raw{*\ $\dots$\\*}
+ show ?case (*<*)sorry(*>*) text_raw{*\ \isasymproof\\*}
qed(*<*)qed(*>*)
text_raw {* }
@@ -905,7 +988,7 @@
proof(induction rule: I.induct)
case rule\<^sub>1
text_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
- show ?case (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show ?case (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
next
text_raw{*\\[-.4ex]$\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
(*<*)
@@ -915,7 +998,7 @@
next
case rule\<^sub>n
text_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*}
- show ?case (*<*)sorry(*>*)text_raw{*\ $\dots$\\*}
+ show ?case (*<*)sorry(*>*)text_raw{*\ \isasymproof\\*}
qed(*<*)qed(*>*)
text{*
--- a/src/Doc/Prog_Prove/document/root.bib Mon Apr 03 23:12:16 2017 +0200
+++ b/src/Doc/Prog_Prove/document/root.bib Mon Apr 03 23:12:44 2017 +0200
@@ -1,6 +1,12 @@
@string{CUP="Cambridge University Press"}
@string{LNCS="Lect.\ Notes in Comp.\ Sci."}
-@string{Springer="Springer-Verlag"}
+@string{Springer="Springer"}
+
+@InProceedings{BauerW-TPHOLs01,author={Gertrud Bauer and Markus Wenzel},
+title={Calculational Reasoning Revisited --- An {Isabelle/Isar} Experience},
+booktitle={Theorem Proving in Higher Order Logics, TPHOLs 2001},
+editor={R. Boulton and P. Jackson},
+year=2001,publisher=Springer,series=LNCS,volume=2152,pages="75--90"}
@book{HuthRyan,author="Michael Huth and Mark Ryan",
title={Logic in Computer Science},publisher=CUP,year=2004}
--- a/src/HOL/Binomial.thy Mon Apr 03 23:12:16 2017 +0200
+++ b/src/HOL/Binomial.thy Mon Apr 03 23:12:44 2017 +0200
@@ -755,13 +755,8 @@
by (simp add: binomial_eq_0 gbinomial_prod_rev prod_zero)
next
case True
- then have "inj_on (op - n) {0..<k}"
- by (auto intro: inj_onI)
- then have "\<Prod>(op - n ` {0..<k}) = prod (op - n) {0..<k}"
- by (auto dest: prod.reindex)
- also have "op - n ` {0..<k} = {Suc (n - k)..n}"
- using True by (auto simp add: image_def Bex_def) presburger (* FIXME slow *)
- finally have *: "prod (\<lambda>q. n - q) {0..<k} = \<Prod>{Suc (n - k)..n}" ..
+ from True have *: "prod (op - n) {0..<k} = \<Prod>{Suc (n - k)..n}"
+ by (intro prod.reindex_bij_witness[of _ "\<lambda>i. n - i" "\<lambda>i. n - i"]) auto
from True have "n choose k = fact n div (fact k * fact (n - k))"
by (rule binomial_fact')
with * show ?thesis
@@ -1558,8 +1553,7 @@
(auto simp: member_le_sum_list_nat less_Suc_eq_le fin)
have uni: "?C = ?A' \<union> ?B'"
by auto
- have disj: "?A' \<inter> ?B' = {}"
- by auto
+ have disj: "?A' \<inter> ?B' = {}" by blast
have "card ?C = card(?A' \<union> ?B')"
using uni by simp
also have "\<dots> = card ?A + card ?B"
@@ -1622,6 +1616,29 @@
qed
qed
+lemma card_disjoint_shuffle:
+ assumes "set xs \<inter> set ys = {}"
+ shows "card (shuffle xs ys) = (length xs + length ys) choose length xs"
+using assms
+proof (induction xs ys rule: shuffle.induct)
+ case (3 x xs y ys)
+ have "shuffle (x # xs) (y # ys) = op # x ` shuffle xs (y # ys) \<union> op # y ` shuffle (x # xs) ys"
+ by (rule shuffle.simps)
+ also have "card \<dots> = card (op # x ` shuffle xs (y # ys)) + card (op # y ` shuffle (x # xs) ys)"
+ by (rule card_Un_disjoint) (insert "3.prems", auto)
+ also have "card (op # x ` shuffle xs (y # ys)) = card (shuffle xs (y # ys))"
+ by (rule card_image) auto
+ also have "\<dots> = (length xs + length (y # ys)) choose length xs"
+ using "3.prems" by (intro "3.IH") auto
+ also have "card (op # y ` shuffle (x # xs) ys) = card (shuffle (x # xs) ys)"
+ by (rule card_image) auto
+ also have "\<dots> = (length (x # xs) + length ys) choose length (x # xs)"
+ using "3.prems" by (intro "3.IH") auto
+ also have "length xs + length (y # ys) choose length xs + \<dots> =
+ (length (x # xs) + length (y # ys)) choose length (x # xs)" by simp
+ finally show ?case .
+qed auto
+
lemma Suc_times_binomial_add: "Suc a * (Suc (a + b) choose Suc a) = Suc b * (Suc (a + b) choose a)"
\<comment> \<open>by Lukas Bulwahn\<close>
proof -
--- a/src/HOL/Library/Multiset.thy Mon Apr 03 23:12:16 2017 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Apr 03 23:12:44 2017 +0200
@@ -1894,6 +1894,9 @@
ultimately show ?case by simp
qed
+lemma mset_shuffle: "zs \<in> shuffle xs ys \<Longrightarrow> mset zs = mset xs + mset ys"
+ by (induction xs ys arbitrary: zs rule: shuffle.induct) auto
+
lemma mset_insort [simp]: "mset (insort x xs) = add_mset x (mset xs)"
by (induct xs) simp_all
--- a/src/HOL/List.thy Mon Apr 03 23:12:16 2017 +0200
+++ b/src/HOL/List.thy Mon Apr 03 23:12:44 2017 +0200
@@ -260,6 +260,13 @@
"splice xs [] = xs" |
"splice (x#xs) (y#ys) = x # y # splice xs ys"
+function shuffle where
+ "shuffle [] ys = {ys}"
+| "shuffle xs [] = {xs}"
+| "shuffle (x # xs) (y # ys) = op # x ` shuffle xs (y # ys) \<union> op # y ` shuffle (x # xs) ys"
+ by pat_completeness simp_all
+termination by lexicographic_order
+
text\<open>
\begin{figure}[htbp]
\fbox{
@@ -285,6 +292,8 @@
@{lemma "product_lists [[a,b], [c], [d,e]] = [[a,c,d], [a,c,e], [b,c,d], [b,c,e]]" by simp}\\
@{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
@{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
+@{lemma "shuffle [a,b] [c,d] = {[a,b,c,d],[a,c,b,d],[a,c,d,b],[c,a,b,d],[c,a,d,b],[c,d,a,b]}"
+ by (simp add: insert_commute)}\\
@{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
@{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
@{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\
@@ -4481,7 +4490,149 @@
declare splice.simps(2)[simp del]
lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
-by (induct xs ys rule: splice.induct) auto
+ by (induct xs ys rule: splice.induct) auto
+
+
+subsubsection \<open>@{const shuffle}\<close>
+
+lemma Nil_in_shuffle[simp]: "[] \<in> shuffle xs ys \<longleftrightarrow> xs = [] \<and> ys = []"
+ by (induct xs ys rule: shuffle.induct) auto
+
+lemma shuffleE:
+ "zs \<in> shuffle xs ys \<Longrightarrow>
+ (zs = xs \<Longrightarrow> ys = [] \<Longrightarrow> P) \<Longrightarrow>
+ (zs = ys \<Longrightarrow> xs = [] \<Longrightarrow> P) \<Longrightarrow>
+ (\<And>x xs' z zs'. xs = x # xs' \<Longrightarrow> zs = z # zs' \<Longrightarrow> x = z \<Longrightarrow> zs' \<in> shuffle xs' ys \<Longrightarrow> P) \<Longrightarrow>
+ (\<And>y ys' z zs'. ys = y # ys' \<Longrightarrow> zs = z # zs' \<Longrightarrow> y = z \<Longrightarrow> zs' \<in> shuffle xs ys' \<Longrightarrow> P) \<Longrightarrow> P"
+ by (induct xs ys rule: shuffle.induct) auto
+
+lemma Cons_in_shuffle_iff:
+ "z # zs \<in> shuffle xs ys \<longleftrightarrow>
+ (xs \<noteq> [] \<and> hd xs = z \<and> zs \<in> shuffle (tl xs) ys \<or>
+ ys \<noteq> [] \<and> hd ys = z \<and> zs \<in> shuffle xs (tl ys))"
+ by (induct xs ys rule: shuffle.induct) auto
+
+lemma splice_in_shuffle [simp, intro]: "splice xs ys \<in> shuffle xs ys"
+ by (induction xs ys rule: splice.induct) (simp_all add: Cons_in_shuffle_iff)
+
+lemma Nil_in_shuffleI: "xs = [] \<Longrightarrow> ys = [] \<Longrightarrow> [] \<in> shuffle xs ys"
+ by simp
+
+lemma Cons_in_shuffle_leftI: "zs \<in> shuffle xs ys \<Longrightarrow> z # zs \<in> shuffle (z # xs) ys"
+ by (cases ys) auto
+
+lemma Cons_in_shuffle_rightI: "zs \<in> shuffle xs ys \<Longrightarrow> z # zs \<in> shuffle xs (z # ys)"
+ by (cases xs) auto
+
+lemma finite_shuffle [simp, intro]: "finite (shuffle xs ys)"
+ by (induction xs ys rule: shuffle.induct) simp_all
+
+lemma length_shuffle: "zs \<in> shuffle xs ys \<Longrightarrow> length zs = length xs + length ys"
+ by (induction xs ys arbitrary: zs rule: shuffle.induct) auto
+
+lemma set_shuffle: "zs \<in> shuffle xs ys \<Longrightarrow> set zs = set xs \<union> set ys"
+ by (induction xs ys arbitrary: zs rule: shuffle.induct) auto
+
+lemma distinct_disjoint_shuffle:
+ assumes "distinct xs" "distinct ys" "set xs \<inter> set ys = {}" "zs \<in> shuffle xs ys"
+ shows "distinct zs"
+using assms
+proof (induction xs ys arbitrary: zs rule: shuffle.induct)
+ case (3 x xs y ys)
+ show ?case
+ proof (cases zs)
+ case (Cons z zs')
+ with "3.prems" and "3.IH"[of zs'] show ?thesis by (force dest: set_shuffle)
+ qed simp_all
+qed simp_all
+
+lemma shuffle_commutes: "shuffle xs ys = shuffle ys xs"
+ by (induction xs ys rule: shuffle.induct) (simp_all add: Un_commute)
+
+lemma Cons_shuffle_subset1: "op # x ` shuffle xs ys \<subseteq> shuffle (x # xs) ys"
+ by (cases ys) auto
+
+lemma Cons_shuffle_subset2: "op # y ` shuffle xs ys \<subseteq> shuffle xs (y # ys)"
+ by (cases xs) auto
+
+lemma filter_shuffle:
+ "filter P ` shuffle xs ys = shuffle (filter P xs) (filter P ys)"
+proof -
+ have *: "filter P ` op # x ` A = (if P x then op # x ` filter P ` A else filter P ` A)" for x A
+ by (auto simp: image_image)
+ show ?thesis
+ by (induction xs ys rule: shuffle.induct)
+ (simp_all split: if_splits add: image_Un * Un_absorb1 Un_absorb2
+ Cons_shuffle_subset1 Cons_shuffle_subset2)
+qed
+
+lemma filter_shuffle_disjoint1:
+ assumes "set xs \<inter> set ys = {}" "zs \<in> shuffle xs ys"
+ shows "filter (\<lambda>x. x \<in> set xs) zs = xs" (is "filter ?P _ = _")
+ and "filter (\<lambda>x. x \<notin> set xs) zs = ys" (is "filter ?Q _ = _")
+ using assms
+proof -
+ from assms have "filter ?P zs \<in> filter ?P ` shuffle xs ys" by blast
+ also have "filter ?P ` shuffle xs ys = shuffle (filter ?P xs) (filter ?P ys)"
+ by (rule filter_shuffle)
+ also have "filter ?P xs = xs" by (rule filter_True) simp_all
+ also have "filter ?P ys = []" by (rule filter_False) (insert assms(1), auto)
+ also have "shuffle xs [] = {xs}" by simp
+ finally show "filter ?P zs = xs" by simp
+next
+ from assms have "filter ?Q zs \<in> filter ?Q ` shuffle xs ys" by blast
+ also have "filter ?Q ` shuffle xs ys = shuffle (filter ?Q xs) (filter ?Q ys)"
+ by (rule filter_shuffle)
+ also have "filter ?Q ys = ys" by (rule filter_True) (insert assms(1), auto)
+ also have "filter ?Q xs = []" by (rule filter_False) (insert assms(1), auto)
+ also have "shuffle [] ys = {ys}" by simp
+ finally show "filter ?Q zs = ys" by simp
+qed
+
+lemma filter_shuffle_disjoint2:
+ assumes "set xs \<inter> set ys = {}" "zs \<in> shuffle xs ys"
+ shows "filter (\<lambda>x. x \<in> set ys) zs = ys" "filter (\<lambda>x. x \<notin> set ys) zs = xs"
+ using filter_shuffle_disjoint1[of ys xs zs] assms
+ by (simp_all add: shuffle_commutes Int_commute)
+
+lemma partition_in_shuffle:
+ "xs \<in> shuffle (filter P xs) (filter (\<lambda>x. \<not>P x) xs)"
+proof (induction xs)
+ case (Cons x xs)
+ show ?case
+ proof (cases "P x")
+ case True
+ hence "x # xs \<in> op # x ` shuffle (filter P xs) (filter (\<lambda>x. \<not>P x) xs)"
+ by (intro imageI Cons.IH)
+ also have "\<dots> \<subseteq> shuffle (filter P (x # xs)) (filter (\<lambda>x. \<not>P x) (x # xs))"
+ by (simp add: True Cons_shuffle_subset1)
+ finally show ?thesis .
+ next
+ case False
+ hence "x # xs \<in> op # x ` shuffle (filter P xs) (filter (\<lambda>x. \<not>P x) xs)"
+ by (intro imageI Cons.IH)
+ also have "\<dots> \<subseteq> shuffle (filter P (x # xs)) (filter (\<lambda>x. \<not>P x) (x # xs))"
+ by (simp add: False Cons_shuffle_subset2)
+ finally show ?thesis .
+ qed
+qed auto
+
+lemma inv_image_partition:
+ assumes "\<And>x. x \<in> set xs \<Longrightarrow> P x" "\<And>y. y \<in> set ys \<Longrightarrow> \<not>P y"
+ shows "partition P -` {(xs, ys)} = shuffle xs ys"
+proof (intro equalityI subsetI)
+ fix zs assume zs: "zs \<in> shuffle xs ys"
+ hence [simp]: "set zs = set xs \<union> set ys" by (rule set_shuffle)
+ from assms have "filter P zs = filter (\<lambda>x. x \<in> set xs) zs"
+ "filter (\<lambda>x. \<not>P x) zs = filter (\<lambda>x. x \<in> set ys) zs"
+ by (intro filter_cong refl; force)+
+ moreover from assms have "set xs \<inter> set ys = {}" by auto
+ ultimately show "zs \<in> partition P -` {(xs, ys)}" using zs
+ by (simp add: o_def filter_shuffle_disjoint1 filter_shuffle_disjoint2)
+next
+ fix zs assume "zs \<in> partition P -` {(xs, ys)}"
+ thus "zs \<in> shuffle xs ys" using partition_in_shuffle[of zs] by (auto simp: o_def)
+qed
subsubsection \<open>Transpose\<close>
@@ -4862,14 +5013,14 @@
assumes "a \<in> set xs" and "sorted xs"
shows "insort a (remove1 a xs) = xs"
proof (rule insort_key_remove1)
+ define n where "n = length (filter (op = a) xs) - 1"
from \<open>a \<in> set xs\<close> show "a \<in> set xs" .
from \<open>sorted xs\<close> show "sorted (map (\<lambda>x. x) xs)" by simp
from \<open>a \<in> set xs\<close> have "a \<in> set (filter (op = a) xs)" by auto
then have "set (filter (op = a) xs) \<noteq> {}" by auto
then have "filter (op = a) xs \<noteq> []" by (auto simp only: set_empty)
then have "length (filter (op = a) xs) > 0" by simp
- then obtain n where n: "Suc n = length (filter (op = a) xs)"
- by (cases "length (filter (op = a) xs)") simp_all
+ then have n: "Suc n = length (filter (op = a) xs)" by (simp add: n_def)
moreover have "replicate (Suc n) a = a # replicate n a"
by simp
ultimately show "hd (filter (op = a) xs) = a" by (simp add: replicate_length_filter)
@@ -7045,6 +7196,26 @@
apply (rule rel_funI)
apply (erule_tac xs=x in list_all2_induct, simp, simp add: rel_fun_def)
done
+
+lemma shuffle_transfer [transfer_rule]:
+ "(list_all2 A ===> list_all2 A ===> rel_set (list_all2 A)) shuffle shuffle"
+proof (intro rel_funI, goal_cases)
+ case (1 xs xs' ys ys')
+ thus ?case
+ proof (induction xs ys arbitrary: xs' ys' rule: shuffle.induct)
+ case (3 x xs y ys xs' ys')
+ from "3.prems" obtain x' xs'' where xs': "xs' = x' # xs''" by (cases xs') auto
+ from "3.prems" obtain y' ys'' where ys': "ys' = y' # ys''" by (cases ys') auto
+ have [transfer_rule]: "A x x'" "A y y'" "list_all2 A xs xs''" "list_all2 A ys ys''"
+ using "3.prems" by (simp_all add: xs' ys')
+ have [transfer_rule]: "rel_set (list_all2 A) (shuffle xs (y # ys)) (shuffle xs'' ys')" and
+ [transfer_rule]: "rel_set (list_all2 A) (shuffle (x # xs) ys) (shuffle xs' ys'')"
+ using "3.prems" by (auto intro!: "3.IH" simp: xs' ys')
+ have "rel_set (list_all2 A) (op # x ` shuffle xs (y # ys) \<union> op # y ` shuffle (x # xs) ys)
+ (op # x' ` shuffle xs'' ys' \<union> op # y' ` shuffle xs' ys'')" by transfer_prover
+ thus ?case by (simp add: xs' ys')
+ qed (auto simp: rel_set_def)
+qed
lemma rtrancl_parametric [transfer_rule]:
assumes [transfer_rule]: "bi_unique A" "bi_total A"