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

author | paulson |

Wed, 07 Feb 2001 16:37:24 +0100 | |

changeset 11080 | 22855d091249 |

parent 11079 | a378479996f7 |

child 11081 | ce9a6746cd1e |

various revisions in response to comments from Tobias

--- a/doc-src/TutorialI/Rules/Basic.thy Wed Feb 07 12:15:59 2001 +0100 +++ b/doc-src/TutorialI/Rules/Basic.thy Wed Feb 07 16:37:24 2001 +0100 @@ -124,6 +124,11 @@ --{* @{subgoals[display,indent=0,margin=65]} *} by (erule notE) +text {* +@{thm[display] disjCI} +\rulename{disjCI} +*}; + lemma "(P \<or> Q) \<and> R \<Longrightarrow> P \<or> Q \<and> R" apply intro --{* @{subgoals[display,indent=0,margin=65]} *} @@ -145,6 +150,18 @@ text{*Quantifiers*} + +text {* +@{thm[display] allI} +\rulename{allI} + +@{thm[display] allE} +\rulename{allE} + +@{thm[display] spec} +\rulename{spec} +*}; + lemma "\<forall>x. P x \<longrightarrow> P x" apply (rule allI) by (rule impI) @@ -154,7 +171,7 @@ apply (drule spec) by (drule mp) -text{*NEW: rename_tac*} +text{*rename_tac*} lemma "x < y \<Longrightarrow> \<forall>x y. P x (f y)" apply intro --{* @{subgoals[display,indent=0,margin=65]} *} @@ -188,6 +205,9 @@ @{thm[display] someI2[no_vars]} \rulename{someI2} +@{thm[display] someI_ex[no_vars]} +\rulename{someI_ex} + needed for examples @{thm[display] inv_def[no_vars]} @@ -201,7 +221,7 @@ *} -lemma "inv Suc (Suc x) = x" +lemma "inv Suc (Suc n) = n" by (simp add: inv_def) text{*but we know nothing about inv Suc 0*} @@ -225,7 +245,7 @@ theorem axiom_of_choice: - "(\<forall>x. \<exists> y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)" + "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)" apply (rule exI, rule allI) txt{* @@ -249,7 +269,7 @@ apply (simp add: Least_def) by (blast intro: some_equality order_antisym); -theorem axiom_of_choice: "(\<forall>x. \<exists> y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)" +theorem axiom_of_choice: "(\<forall>x. \<exists>y. P x y) \<Longrightarrow> \<exists>f. \<forall>x. P x (f x)" apply (rule exI [of _ "\<lambda>x. SOME y. P x y"]) by (blast intro: someI); @@ -298,10 +318,13 @@ apply assumption oops -lemma "\<forall> z. R z z \<Longrightarrow> \<exists>x. \<forall> y. R x y" -apply (rule exI) -apply (rule allI) -apply (drule spec) +lemma "\<forall> y. R y y \<Longrightarrow> \<exists>x. \<forall> y. R x y" +apply (rule exI) + --{* @{subgoals[display,indent=0,margin=65]} *} +apply (rule allI) + --{* @{subgoals[display,indent=0,margin=65]} *} +apply (drule spec) + --{* @{subgoals[display,indent=0,margin=65]} *} oops lemma "\<forall>x. \<exists> y. x=y"

--- a/doc-src/TutorialI/Rules/Primes.thy Wed Feb 07 12:15:59 2001 +0100 +++ b/doc-src/TutorialI/Rules/Primes.thy Wed Feb 07 16:37:24 2001 +0100 @@ -1,7 +1,8 @@ (* ID: $Id$ *) (* EXTRACT from HOL/ex/Primes.thy*) -(*Euclid's algorithm *) +(*Euclid's algorithm + This material now appears AFTER that of Forward.thy *) theory Primes = Main: consts gcd :: "nat*nat \<Rightarrow> nat" @@ -37,8 +38,13 @@ (*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*) lemma gcd_dvd_both: "(gcd(m,n) dvd m) \<and> (gcd(m,n) dvd n)" apply (induct_tac m n rule: gcd.induct) + --{* @{subgoals[display,indent=0,margin=65]} *} apply (case_tac "n=0") -apply (simp_all) +txt{*subgoals after the case tac +@{subgoals[display,indent=0,margin=65]} +*}; +apply (simp_all) + --{* @{subgoals[display,indent=0,margin=65]} *} by (blast dest: dvd_mod_imp_dvd) @@ -49,17 +55,7 @@ @{thm[display] dvd_trans} \rulename{dvd_trans} - -\begin{isabelle} -proof\ (prove):\ step\ 3\isanewline -\isanewline -goal\ (lemma\ gcd_dvd_both):\isanewline -gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n\isanewline -\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk 0\ <\ n;\ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n)\isasymrbrakk \isanewline -\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ gcd\ (n,\ m\ mod\ n)\ dvd\ m -\end{isabelle} -*}; - +*} lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1] lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2]; @@ -87,11 +83,18 @@ apply (simp_all add: dvd_mod) done +text {* +@{thm[display] dvd_mod} +\rulename{dvd_mod} +*} + (*just checking the claim that case_tac "n" works too*) lemma "k dvd m \<longrightarrow> k dvd n \<longrightarrow> k dvd gcd(m,n)" apply (induct_tac m n rule: gcd.induct) apply (case_tac "n") -by (simp_all add: dvd_mod) +apply (simp_all add: dvd_mod) +done + theorem gcd_greatest_iff [iff]: "(k dvd gcd(m,n)) = (k dvd m \<and> k dvd n)"

--- a/doc-src/TutorialI/Rules/rules.tex Wed Feb 07 12:15:59 2001 +0100 +++ b/doc-src/TutorialI/Rules/rules.tex Wed Feb 07 16:37:24 2001 +0100 @@ -1426,8 +1426,7 @@ \end{isabelle} % This fact about multiplication is also appropriate for -the \isa{iff} attribute:\REMARK{the ?s are ugly here but we need - them again when talking about \isa{of}; we need a consistent style} +the \isa{iff} attribute: \begin{isabelle} (\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0) \end{isabelle} @@ -1449,189 +1448,6 @@ \index{*blast (method)|)}% - -\section{Proving the Correctness of Euclid's Algorithm} -\label{sec:proving-euclid} - -\index{Euclid's algorithm|(}\index{*gcd (function)|(}% -A brief development will illustrate the advanced use of -\isa{blast}. We shall also see \isa{case_tac} used to perform a Boolean -case split. - -In \S\ref{sec:recdef-simplification}, we declared the -recursive function \isa{gcd}: -\begin{isabelle} -\isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline -\isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n))"\isanewline -\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))" -\end{isabelle} -Let us prove that it computes the greatest common -divisor of its two arguments. -The theorem is expressed in terms of the familiar -\emph{divides} relation from number theory: -\begin{isabelle} -?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k -\rulename{dvd_def} -\end{isabelle} -% -A simple induction proves the theorem. Here \isa{gcd.induct} refers to the -induction rule returned by \isa{recdef}. The proof relies on the simplification -rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the -definition of \isa{gcd} can cause looping. -\begin{isabelle} -\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\ n)"\isanewline -\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline -\isacommand{apply}\ (case_tac\ "n=0")\isanewline -\isacommand{apply}\ (simp_all)\isanewline -\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline -\isacommand{done}% -\end{isabelle} -Notice that the induction formula -is a conjunction. This is necessary: in the inductive step, each -half of the conjunction establishes the other. The first three proof steps -are applying induction, performing a case analysis on \isa{n}, -and simplifying. Let us pass over these quickly --- we shall discuss -\isa{case_tac} below --- and consider the use of \isa{blast}. We have reached the -following subgoal: -\begin{isabelle} -%gcd\ (m,\ n)\ dvd\ m\ \isasymand\ gcd\ (m,\ n)\ dvd\ n\isanewline -\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline - \ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n)\isasymrbrakk\isanewline -\ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ gcd\ (n,\ m\ mod\ n)\ dvd\ m -\end{isabelle} -% -One of the assumptions, the induction hypothesis, is a conjunction. -The two divides relationships it asserts are enough to prove -the conclusion, for we have the following theorem at our disposal: -\begin{isabelle} -\isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m% -\rulename{dvd_mod_imp_dvd} -\end{isabelle} -% -This theorem can be applied in various ways. As an introduction rule, it -would cause backward chaining from the conclusion (namely -\isa{?k~dvd~?m}) to the two premises, which -also involve the divides relation. This process does not look promising -and could easily loop. More sensible is to apply the rule in the forward -direction; each step would eliminate an occurrence of the \isa{mod} symbol, so the -process must terminate. - -So the final proof step applies the \isa{blast} method. -Attaching the {\isa{dest}} attribute to \isa{dvd_mod_imp_dvd} tells \isa{blast} -to use it as destruction rule: in the forward direction. - -\medskip -We have proved a conjunction. Now, let us give names to each of the -two halves: -\begin{isabelle} -\isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline -\isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]% -\end{isabelle} - -Several things are happening here. The keyword \isacommand{lemmas} -tells Isabelle to transform a theorem in some way and to -give a name to the resulting theorem. Attributes can be given, -here \isa{iff}, which supplies the new theorems to the classical reasoner -and the simplifier. The directive \isa{THEN},\indexbold{*THEN (directive)} -described in -\S\ref{sec:forward} below, supplies the lemma -\isa{gcd_dvd_both} to the -destruction rule \isa{conjunct1}. The effect is to extract the first part: -\begin{isabelle} -\ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?m1 -\end{isabelle} -The variable names \isa{?m1} and \isa{?n1} arise because -Isabelle renames schematic variables to prevent -clashes. The second \isacommand{lemmas} declaration yields -\begin{isabelle} -\ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?n1 -\end{isabelle} - -\medskip -To complete the verification of the \isa{gcd} function, we must -prove that it returns the greatest of all the common divisors -of its arguments. The proof is by induction, case analysis and simplification. -\begin{isabelle} -\isacommand{lemma}\ gcd_greatest\ -[rule_format]:\isanewline -\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\ -k\ dvd\ gcd(m,n)"\isanewline -\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline -\isacommand{apply}\ (case_tac\ "n=0")\isanewline -\isacommand{apply}\ (simp_all\ add:\ gcd_non_0\ dvd_mod)\isanewline -\isacommand{done} -\end{isabelle} - -The case analysis is performed by \isa{case_tac~"n=0"}: the operand has type -\isa{bool}. Until now, we have used \isa{case_tac} only with datatypes, and since -\isa{nat} is a datatype, we could have written -\isa{case_tac~"n"} with a similar effect. However, the definition of \isa{gcd} -makes a Boolean decision: -\begin{isabelle} -\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))" -\end{isabelle} -Proofs about a function frequently follow the function's definition, so we perform -case analysis over the same formula. - -\begingroup\samepage -\begin{isabelle} -\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline -\ \ \ \ \ \ \ \ \ \ \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ n\ =\ 0\isasymrbrakk \isanewline -\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n) -\pagebreak[0]\isanewline -\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline -\ \ \ \ \ \ \ \ \ \ \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline -\ \ \ \ \ \ \ \ \ \ \ \ \ n\ \isasymnoteq \ 0\isasymrbrakk \isanewline -\ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n) -\end{isabelle} -\endgroup - -\begin{warn} -Note that the theorem has been expressed using HOL implication, -\isa{\isasymlongrightarrow}, because the induction affects the two -preconditions. The directive \isa{rule_format} tells Isabelle to replace -each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before -storing the theorem we have proved. This directive can also remove outer -universal quantifiers, converting a theorem into the usual format for -inference rules. (See \S\ref{sec:forward}.) -\end{warn} - -The facts proved above can be summarized as a single logical -equivalence. This step gives us a chance to see another application -of \isa{blast}, and it is worth doing for sound logical reasons. -\begin{isabelle} -\isacommand{theorem}\ gcd_greatest_iff\ [iff]:\isanewline -\ \ \ \ \ \ \ \ \ "(k\ dvd\ gcd(m,n))\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ -n)"\isanewline -\isacommand{by}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans) -\end{isabelle} -This theorem concisely expresses the correctness of the \isa{gcd} -function. -We state it with the \isa{iff} attribute so that -Isabelle can use it to remove some occurrences of \isa{gcd}. -The theorem has a one-line -proof using \isa{blast} supplied with two additional introduction -rules. The exclamation mark -({\isa{intro}}{\isa{!}})\ signifies safe rules, which are -applied aggressively. Rules given without the exclamation mark -are applied reluctantly and their uses can be undone if -the search backtracks. Here the unsafe rule expresses transitivity -of the divides relation: -\begin{isabelle} -\isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p% -\rulename{dvd_trans} -\end{isabelle} -Applying \isa{dvd_trans} as -an introduction rule entails a risk of looping, for it multiplies -occurrences of the divides symbol. However, this proof relies -on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply -aggressively because it yields simpler subgoals. The proof implicitly -uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were -declared using \isa{iff}.% -\index{Euclid's algorithm|)}\index{*gcd (function)|)} - - \section{Other Classical Reasoning Methods} The \isa{blast} method is our main workhorse for proving theorems @@ -1762,13 +1578,12 @@ not always the best way of presenting the proof so found. Forward proof is particularly good for reasoning from the general to the specific. For example, consider the following distributive law for -the -\isa{gcd} function: +the greatest common divisor: \[ k\times\gcd(m,n) = \gcd(k\times m,k\times n)\] Putting $m=1$ we get (since $\gcd(1,n)=1$ and $k\times1=k$) \[ k = \gcd(k,k\times n)\] -We have derived a new fact about \isa{gcd}; if re-oriented, it might be +We have derived a new fact; if re-oriented, it might be useful for simplification. After re-orienting it and putting $n=1$, we derive another useful law: \[ \gcd(k,k)=k \] @@ -1778,13 +1593,23 @@ \subsection{The {\tt\slshape of} and {\tt\slshape THEN} Directives} -Now let us reproduce our examples in Isabelle. Here is the distributive -law: +Let us reproduce our examples in Isabelle. Recall that in +\S\ref{sec:recdef-simplification} we declared the recursive function +\isa{gcd}: +\begin{isabelle} +\isacommand{consts}\ gcd\ ::\ "nat*nat\ \isasymRightarrow\ nat"\isanewline +\isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n))"\isanewline +\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))" +\end{isabelle} +% +From this definition, it is possible to prove the +distributive law. \begin{isabelle} ?k\ *\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ *\ ?m,\ ?k\ *\ ?n) \rulename{gcd_mult_distrib2} -\end{isabelle}% -The first step is to replace \isa{?m} by~1 in this law. +\end{isabelle} +Now we can carry out the derivation shown above. +The first step is to replace \isa{?m} by~1. The \isa{of}\indexbold{*of (directive)} directive refers to variables not by name but by their order of occurrence in the theorem. @@ -1796,9 +1621,12 @@ \isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1] \end{isabelle} % +The keyword \isacommand{lemmas}\index{lemmas@\isacommand{lemmas}|bold} +declares a new theorem, which can be derived +from an existing one using attributes such as \isa{[of~k~1]}. The command \isa{thm gcd_mult_0} -displays the resulting theorem: +displays the result: \begin{isabelle} \ \ \ \ \ k\ *\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ *\ 1,\ k\ *\ ?n) \end{isabelle} @@ -1819,8 +1647,7 @@ and returns the result of simplifying it, with respect to the default simplification rules: \begin{isabelle} -\isacommand{lemmas}\ -gcd_mult_1\ =\ gcd_mult_0\ +\isacommand{lemmas}\ gcd_mult_1\ =\ gcd_mult_0\ [simplified]% \end{isabelle} % @@ -1848,13 +1675,11 @@ \isa{THEN~sym}\indexbold{*THEN (directive)} gives the current theorem to the rule \isa{sym} and returns the resulting conclusion. The effect is to exchange the two operands of the equality. Typically \isa{THEN} is used -with destruction rules. Above we have used -\isa{THEN~conjunct1} to extract the first part of the theorem -\isa{gcd_dvd_both}. Also useful is \isa{THEN~spec}, which removes the quantifier -from a theorem of the form $\forall x.\,P$, and \isa{THEN~mp}, which converts the -implication $P\imp Q$ into the rule $\vcenter{\infer{Q}{P}}$. -Similar to \isa{mp} are the following two rules, which extract -the two directions of reasoning about a boolean equivalence: +with destruction rules. Also useful is \isa{THEN~spec}, which removes the +quantifier from a theorem of the form $\forall x.\,P$, and \isa{THEN~mp}, +which converts the implication $P\imp Q$ into the rule +$\vcenter{\infer{Q}{P}}$. Similar to \isa{mp} are the following two rules, +which extract the two directions of reasoning about a boolean equivalence: \begin{isabelle} \isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% \rulename{iffD1}% @@ -1895,44 +1720,29 @@ \isacommand{by}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified]) \end{isabelle} -\medskip -The \isaindexbold{rule_format} directive replaces a common usage -of \isa{THEN}\@. It is needed in proofs by induction when the induction formula must be -expressed using -\isa{\isasymlongrightarrow} and \isa{\isasymforall}. For example, in -Sect.\ts\ref{sec:proving-euclid} above we were able to write just this: -\begin{isabelle} -\isacommand{lemma}\ gcd_greatest\ -[rule_format]:\isanewline -\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\ -k\ dvd\ gcd(m,n)" -\end{isabelle} -% -It replaces a clumsy use of \isa{THEN}: -\begin{isabelle} -\isacommand{lemma}\ gcd_greatest\ -[THEN mp, THEN mp]:\isanewline -\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\ -k\ dvd\ gcd(m,n)" -\end{isabelle} -% -Through \isa{rule_format} we can replace any number of applications of \isa{THEN} -with the rules \isa{mp} and \isa{spec}, eliminating the outermost occurrences of -\isa{\isasymlongrightarrow} and \isa{\isasymforall}. - \subsection{The {\tt\slshape OF} Directive} \index{*OF (directive)|(}% Recall that \isa{of} generates an instance of a rule by specifying values for its variables. Analogous is \isa{OF}, which -generates an instance of a rule by specifying facts for its premises. Let -us try it with this rule: +generates an instance of a rule by specifying facts for its premises. + +Below we shall need the +\emph{divides} relation of number theory: +\begin{isabelle} +?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k +\rulename{dvd_def} +\end{isabelle} +% +For example, this rule states that if $k$ and $n$ are relatively prime +and if $k$ divides $m\times n$ then $k$ divides $m$. \begin{isabelle} \isasymlbrakk gcd(?k,?n){=}1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m \rulename{relprime_dvd_mult} \end{isabelle} +We can use \isa{OF} to create an instance of this rule. First, we prove an instance of its first premise: \begin{isabelle} @@ -1941,11 +1751,10 @@ \end{isabelle} We have evaluated an application of the \isa{gcd} function by simplification. Expression evaluation involving recursive functions is not -guaranteed to terminate, and it certainly is not efficient; Isabelle -performs arithmetic operations by rewriting symbolic bit strings. Here, -however, the simplification above takes less than one second. We can -specify this new lemma to \isa{OF}, generating an instance of -\isa{relprime_dvd_mult}. The expression +guaranteed to terminate, and it can be slow; Isabelle +performs arithmetic by rewriting symbolic bit strings. Here, +however, the simplification takes less than one second. We can +give this new lemma to \isa{OF}. The expression \begin{isabelle} \ \ \ \ \ relprime_dvd_mult [OF relprime_20_81] \end{isabelle} @@ -1997,9 +1806,11 @@ \item \isa{OF} applies a rule to a list of theorems \item \isa{THEN} gives a theorem to a named rule and returns the conclusion -\item \isa{rule_format} puts a theorem into standard form - by removing \isa{\isasymlongrightarrow} and~\isa{\isasymforall} +%\item \isa{rule_format} puts a theorem into standard form +% by removing \isa{\isasymlongrightarrow} and~\isa{\isasymforall} \item \isa{simplified} applies the simplifier to a theorem +\item \isacommand{lemmas} assigns a name to the theorem produced by the +attributes above \end{itemize} @@ -2054,18 +1865,18 @@ \rulename{mod_Suc} \end{isabelle} -\medskip +\subsection{The Method {\tt\slshape insert}} + \index{*insert(method)|(}% -The methods designed for supporting forward reasoning are -\isa{insert} and \isa{subgoal_tac}. The \isa{insert} method +The \isa{insert} method inserts a given theorem as a new assumption of the current subgoal. This already is a forward step; moreover, we may (as always when using a theorem) apply \isa{of}, \isa{THEN} and other directives. The new assumption can then be used to help prove the subgoal. -For example, consider this theorem about the divides relation. -Only the first proof step is given; it inserts the distributive law for +For example, consider this theorem about the divides relation. The first +proof step inserts the distributive law for \isa{gcd}. We specify its variables as shown. \begin{isabelle} \isacommand{lemma}\ @@ -2085,20 +1896,20 @@ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m \end{isabelle} -The next proof step, \isa{\isacommand{apply}(simp)}, -utilizes the assumption \isa{gcd(k,n)\ =\ -1}. Here is the result: +The next proof step utilizes the assumption \isa{gcd(k,n)\ =\ 1}: \begin{isabelle} -\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ *\ n){;} +\isacommand{apply}(simp)\isanewline +\ 1.\ \isasymlbrakk gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ +(m\ *\ n){;} \ m\ =\ gcd\ (m\ *\ k,\ m\ *\ n)\isasymrbrakk\isanewline \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m \end{isabelle} -Simplification has yielded an equation for \isa{m} that will be used to -complete the proof. +Simplification has yielded an equation for~\isa{m}. The rest of the proof +is omitted. \medskip -Here is another proof using \isa{insert}. \REMARK{Effect with unknowns?} -Division and remainder obey a well-known law: +Here is another demonstration of \isa{insert}. \REMARK{Effect with +unknowns?} Division and remainder obey a well-known law: \begin{isabelle} (?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m \rulename{mod_div_equality} @@ -2131,8 +1942,10 @@ sides of the equation, proving the theorem.% \index{*insert(method)|)} -\medskip -A similar method is \isa{subgoal_tac}.\index{*subgoal_tac (method)} +\subsection{The Method {\tt\slshape subgoal_tac}} + +\index{*subgoal_tac (method)}% +A similar method is \isa{subgoal_tac}. Instead of inserting a theorem as an assumption, it inserts an arbitrary formula. This formula must be proved later as a separate subgoal. The @@ -2357,9 +2170,216 @@ \end{itemize} \begin{exercise} -This proof uses \isa? and \isa+ to \ldots{} can you explain? +Explain the use of \isa? and \isa+ in this proof. \begin{isabelle} \isacommand{lemma}\ "\isasymlbrakk P\isasymand Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ R"\isanewline \isacommand{by}\ (drule\ mp,\ intro?,\ assumption+)+ \end{isabelle} \end{exercise} + + + +\section{Proving the Correctness of Euclid's Algorithm} +\label{sec:proving-euclid} + +\index{Euclid's algorithm|(}\index{*gcd (function)|(}% +A brief development will demonstrate the techniques of this chapter, +including \isa{blast} applied with additional rules. We shall also see +\isa{case_tac} used to perform a Boolean case split. + +Let us prove that \isa{gcd} computes the greatest common +divisor of its two arguments. +% +We use induction: \isa{gcd.induct} is the +induction rule returned by \isa{recdef}. We simplify using +rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the +definition of \isa{gcd} can loop. +\begin{isabelle} +\isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\ +n)" +\end{isabelle} +The induction formula must be a conjunction. In the +inductive step, each conjunct establishes the other. +\begin{isabelle} +\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline +\ 1.\ \isasymAnd m\ n.\ n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline +\isaindent{\ 1.\ \isasymAnd m\ n.\ }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand +\ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n\isanewline +\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow\ gcd\ (m,\ n)\ +dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n% +\end{isabelle} + +The conditional induction hypothesis suggests doing a case +analysis on \isa{n=0}. We apply \isa{case_tac} with type +\isa{bool} --- and not with a datatype, as we have done until now. Since +\isa{nat} is a datatype, we could have written +\isa{case_tac~"n"} instead of \isa{case_tac~"n=0"}. However, the definition +of \isa{gcd} makes a Boolean decision: +\begin{isabelle} +\ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))" +\end{isabelle} +Proofs about a function frequently follow the function's definition, so we perform +case analysis over the same formula. +\begin{isabelle} +\isacommand{apply}\ (case_tac\ "n=0")\isanewline +\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline +\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline +\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline +\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n\isanewline +\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline +\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline +\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk +\isanewline +\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (m,\ n)\ dvd\ m\ \isasymand \ gcd\ (m,\ n)\ dvd\ n% +\end{isabelle} +% +Simplification leaves one subgoal: +\begin{isabelle} +\isacommand{apply}\ (simp_all)\isanewline +\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk 0\ <\ n;\isanewline +\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }gcd\ (n,\ m\ mod\ n)\ dvd\ n\ +\isasymand \ gcd\ (n,\ m\ mod\ n)\ dvd\ m\ mod\ +n\isasymrbrakk \isanewline +\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ (n,\ m\ mod\ n)\ dvd\ m% +\end{isabelle} +% +Here, we can use \isa{blast}. +One of the assumptions, the induction hypothesis, is a conjunction. +The two divides relationships it asserts are enough to prove +the conclusion, for we have the following theorem at our disposal: +\begin{isabelle} +\isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m% +\rulename{dvd_mod_imp_dvd} +\end{isabelle} +% +This theorem can be applied in various ways. As an introduction rule, it +would cause backward chaining from the conclusion (namely +\isa{?k~dvd~?m}) to the two premises, which +also involve the divides relation. This process does not look promising +and could easily loop. More sensible is to apply the rule in the forward +direction; each step would eliminate an occurrence of the \isa{mod} symbol, so the +process must terminate. +\begin{isabelle} +\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline +\isacommand{done} +\end{isabelle} +Attaching the {\isa{dest}} attribute to \isa{dvd_mod_imp_dvd} tells +\isa{blast} to use it as destruction rule: in the forward direction. + +\medskip +We have proved a conjunction. Now, let us give names to each of the +two halves: +\begin{isabelle} +\isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline +\isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]% +\end{isabelle} +Here we see \isacommand{lemmas}\index{lemmas@\isacommand{lemmas}} +used with the \isa{iff} attribute, which supplies the new theorems to the +classical reasoner and the simplifier. Recall that \isa{THEN} is +frequently used with destruction rules; \isa{THEN conjunct1} extracts the +first half of a conjunctive theorem. Given \isa{gcd_dvd_both} it yields +\begin{isabelle} +\ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?m1 +\end{isabelle} +The variable names \isa{?m1} and \isa{?n1} arise because +Isabelle renames schematic variables to prevent +clashes. The second \isacommand{lemmas} declaration yields +\begin{isabelle} +\ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?n1 +\end{isabelle} + +\medskip +To complete the verification of the \isa{gcd} function, we must +prove that it returns the greatest of all the common divisors +of its arguments. The proof is by induction, case analysis and simplification. +\begin{isabelle} +\isacommand{lemma}\ gcd_greatest\ +[rule_format]:\isanewline +\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\ +k\ dvd\ gcd(m,n)" +\end{isabelle} +% +The goal is expressed using HOL implication, +\isa{\isasymlongrightarrow}, because the induction affects the two +preconditions. The directive \isa{rule_format} tells Isabelle to replace +each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before +storing the eventual theorem. This directive can also remove outer +universal quantifiers, converting the theorem into the usual format for +inference rules. It can replace any series of applications of +\isa{THEN} to the rules \isa{mp} and \isa{spec}. We did not have to +write this: +\begin{isabelle} +\ \ \ \ \ \isacommand{lemma}\ gcd_greatest\ +[THEN mp, THEN mp]:\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ +\isasymlongrightarrow\ k\ dvd\ gcd(m,n)" +\end{isabelle} + +Because we are again reasoning about \isa{gcd}, we perform the same +induction and case analysis as in the previous proof: +\begingroup\samepage +\begin{isabelle} +\isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline +\isacommand{apply}\ (case_tac\ "n=0")\isanewline +\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ +\isasymlongrightarrow \isanewline +\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline +\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline +\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n)\isanewline +\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymlongrightarrow \isanewline +\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (n,\ m\ mod\ n);\isanewline +\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk +\isanewline +\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ (m,\ n) +\end{isabelle} +\endgroup + +\noindent Simplification proves both subgoals. +\begin{isabelle} +\isacommand{apply}\ (simp_all\ add:\ dvd_mod)\isanewline +\isacommand{done} +\end{isabelle} +In the first, where \isa{n=0}, the implication becomes trivial: \isa{k\ dvd\ +gcd\ (m,\ n)} goes to~\isa{k\ dvd\ m}. The second subgoal is proved by +an unfolding of \isa{gcd}, using this rule about divides: +\begin{isabelle} +\isasymlbrakk ?f\ dvd\ ?m;\ ?f\ dvd\ ?n\isasymrbrakk \ +\isasymLongrightarrow \ ?f\ dvd\ ?m\ mod\ ?n% +\rulename{dvd_mod} +\end{isabelle} + + +\medskip +The facts proved above can be summarized as a single logical +equivalence. This step gives us a chance to see another application +of \isa{blast}. +\begin{isabelle} +\isacommand{theorem}\ gcd_greatest_iff\ [iff]:\isanewline +\ \ \ \ \ \ \ \ \ "(k\ dvd\ gcd(m,n))\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ +n)"\isanewline +\isacommand{by}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans) +\end{isabelle} +This theorem concisely expresses the correctness of the \isa{gcd} +function. +We state it with the \isa{iff} attribute so that +Isabelle can use it to remove some occurrences of \isa{gcd}. +The theorem has a one-line +proof using \isa{blast} supplied with two additional introduction +rules. The exclamation mark +({\isa{intro}}{\isa{!}})\ signifies safe rules, which are +applied aggressively. Rules given without the exclamation mark +are applied reluctantly and their uses can be undone if +the search backtracks. Here the unsafe rule expresses transitivity +of the divides relation: +\begin{isabelle} +\isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p% +\rulename{dvd_trans} +\end{isabelle} +Applying \isa{dvd_trans} as +an introduction rule entails a risk of looping, for it multiplies +occurrences of the divides symbol. However, this proof relies +on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply +aggressively because it yields simpler subgoals. The proof implicitly +uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were +declared using \isa{iff}.% +\index{Euclid's algorithm|)}\index{*gcd (function)|)}

--- a/doc-src/TutorialI/Sets/Relations.thy Wed Feb 07 12:15:59 2001 +0100 +++ b/doc-src/TutorialI/Sets/Relations.thy Wed Feb 07 16:37:24 2001 +0100 @@ -93,26 +93,26 @@ text{*Relations. transitive closure*} -lemma rtrancl_converseD: "(x,y) \<in> (r^-1)^* \<Longrightarrow> (y,x) \<in> r^*" +lemma rtrancl_converseD: "(x,y) \<in> (r\<inverse>)\<^sup>* \<Longrightarrow> (y,x) \<in> r\<^sup>*" apply (erule rtrancl_induct) txt{* @{subgoals[display,indent=0,margin=65]} *}; apply (rule rtrancl_refl) -apply (blast intro: r_into_rtrancl rtrancl_trans) +apply (blast intro: rtrancl_trans) done -lemma rtrancl_converseI: "(y,x) \<in> r^* \<Longrightarrow> (x,y) \<in> (r^-1)^*" +lemma rtrancl_converseI: "(y,x) \<in> r\<^sup>* \<Longrightarrow> (x,y) \<in> (r\<inverse>)\<^sup>*" apply (erule rtrancl_induct) apply (rule rtrancl_refl) -apply (blast intro: r_into_rtrancl rtrancl_trans) +apply (blast intro: rtrancl_trans) done -lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" +lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>" by (auto intro: rtrancl_converseI dest: rtrancl_converseD) -lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" +lemma rtrancl_converse: "(r\<inverse>)\<^sup>* = (r\<^sup>*)\<inverse>" apply (intro equalityI subsetI) txt{* after intro rules

--- a/doc-src/TutorialI/Sets/sets.tex Wed Feb 07 12:15:59 2001 +0100 +++ b/doc-src/TutorialI/Sets/sets.tex Wed Feb 07 16:37:24 2001 +0100 @@ -1,22 +1,19 @@ % $Id$ \chapter{Sets, Functions and Relations} -\REMARK{The old version used lots of bold. I've cut down, -changing some \texttt{textbf} to \texttt{relax}. This can be undone. -See the source.} -Mathematics relies heavily on set theory: not just unions and intersections -but images, least fixed points and other concepts. In computer science, -sets are used to formalize grammars, state transition systems, etc. The set -theory of Isabelle/HOL should not be confused with traditional, untyped set -theory, in which everything is a set. Our sets are typed. In a given set, -all elements have the same type, say~$\tau$, and the set itself has type -\isa{$\tau$~set}. +This chapter describes the formalization of typed set theory, which is +the basis of much else in HOL\@. For example, an +inductive definition yields a set, and the abstract theories of relations +regard a relation as a set of pairs. The chapter introduces the well-known +constants such as union and intersection, as well as the main operations on relations, such as converse, composition and +transitive closure. Functions are also covered. They are not sets in +HOL, but many of their properties concern sets: the range of a +function is a set, and the inverse image of a function maps sets to sets. -Relations are simply sets of pairs. This chapter describes -the main operations on relations, such as converse, composition and -transitive closure. Functions are also covered. They are not sets in -Isabelle/HOL, but many of their properties concern sets. The range of a -function is a set, and the inverse image of a function maps sets to sets. +This chapter will be useful to anybody who plans to develop a substantial +proof. sets are convenient for formalizing computer science concepts such +as grammars, logical calculi and state transition systems. Isabelle can +prove many statements involving sets automatically. This chapter ends with a case study concerning model checking for the temporal logic CTL\@. Most of the other examples are simple. The @@ -25,17 +22,20 @@ the notation. Natural deduction rules are provided for the set theory constants, but they -are seldom used directly, so only a few are presented here. Many formulas -involving sets can be proved automatically or simplified to a great extent. -Expressing your concepts in terms of sets will probably make your proofs -easier. +are seldom used directly, so only a few are presented here. \section{Sets} -We begin with \relax{intersection}, \relax{union} and -\relax{complement}. In addition to the -\relax{membership} relation, there is a symbol for its negation. These +\index{sets|(}% +HOL's set theory should not be confused with traditional, untyped set +theory, in which everything is a set. Our sets are typed. In a given set, +all elements have the same type, say~$\tau$, and the set itself has type +\isa{$\tau$~set}. + +We begin with \bfindex{intersection}, \bfindex{union} and +\bfindex{complement}. In addition to the +\bfindex{membership relation}, there is a symbol for its negation. These points can be seen below. Here are the natural deduction rules for intersection. Note the @@ -59,9 +59,9 @@ \rulename{Compl_Un} \end{isabelle} -Set \relax{difference} is the intersection of a set with the -complement of another set. Here we also see the syntax for the -empty set and for the universal set. +Set \textbf{difference}\indexbold{difference!of sets} is the intersection +of a set with the complement of another set. Here we also see the syntax +for the empty set and for the universal set. \begin{isabelle} A\ \isasyminter\ (B\ -\ A)\ =\ \isacharbraceleft\isacharbraceright \rulename{Diff_disjoint}\isanewline @@ -69,7 +69,7 @@ \rulename{Compl_partition} \end{isabelle} -The \relax{subset} relation holds between two sets just if every element +The \bfindex{subset relation} holds between two sets just if every element of one is also an element of the other. This relation is reflexive. These are its natural deduction rules: \begin{isabelle} @@ -117,9 +117,10 @@ disjoint. \medskip -Two sets are \relax{equal} if they contain the same elements. -This is -the principle of \textbf{extensionality} for sets. +Two sets are \textbf{equal}\indexbold{equality!of sets} if they contain the +same elements. This is +the principle of \textbf{extensionality}\indexbold{extensionality!for sets} +for sets. \begin{isabelle} ({\isasymAnd}x.\ (x\ {\isasymin}\ A)\ =\ (x\ {\isasymin}\ B))\ {\isasymLongrightarrow}\ A\ =\ B @@ -144,7 +145,8 @@ \subsection{Finite Set Notation} -Finite sets are expressed using the constant {\isa{insert}}, which is +\indexbold{sets!notation for finite}\index{*insert (constant)} +Finite sets are expressed using the constant \isa{insert}, which is a form of union: \begin{isabelle} insert\ a\ A\ =\ \isacharbraceleft a\isacharbraceright\ \isasymunion\ A @@ -193,6 +195,7 @@ \subsection{Set Comprehension} +\index{set comprehensions|(}% The set comprehension \isa{\isacharbraceleft x.\ P\isacharbraceright} expresses the set of all elements that satisfy the predicate~\isa{P}. Two laws describe the relationship between set @@ -246,10 +249,12 @@ require writing \isa{A(x)} and \isa{{\isasymlambda}z.\ P}. +\index{set comprehensions|)} \subsection{Binding Operators} +\index{quantifiers!for sets|(}% Universal and existential quantifications may range over sets, with the obvious meaning. Here are the natural deduction rules for the bounded universal quantifier. Occasionally you will need to apply @@ -285,7 +290,9 @@ Q\isasymrbrakk\ \isasymLongrightarrow\ Q% \rulename{bexE} \end{isabelle} +\index{quantifiers!for sets|)} +\index{union!indexed}% Unions can be formed over the values of a given set. The syntax is \mbox{\isa{\isasymUnion x\isasymin A.\ B}} or \isa{UN x\isasymin A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law: @@ -337,6 +344,7 @@ \rulename{Union_iff} \end{isabelle} +\index{intersection!indexed}% Intersections are treated dually, although they seem to be used less often than unions. The syntax below would be \isa{INT x:\ A.\ B} and \isa{Inter\ C} in \textsc{ascii}. Among others, these @@ -363,13 +371,24 @@ A\cup B$ is replaced by $x\in A\vee x\in B$. The internal form of a comprehension involves the constant -\isa{Collect}, which occasionally appears when a goal or theorem +\isa{Collect},\index{*Collect (constant)} +which occasionally appears when a goal or theorem is displayed. For example, \isa{Collect\ P} is the same term as \isa{\isacharbraceleft z.\ P\ x\isacharbraceright}. The same thing can -happen with quantifiers: for example, \isa{Ball\ A\ P} is -\isa{{\isasymforall}z\isasymin A.\ P\ x} and \isa{Bex\ A\ P} is +happen with quantifiers: \hbox{\isa{All\ P}}\index{*All (constant)} +is +\isa{{\isasymforall}z.\ P\ x} and +\hbox{\isa{Ex\ P}}\index{*Ex (constant)} is \isa{\isasymexists z.\ P\ x}; +also \isa{Ball\ A\ P}\index{*Ball (constant)} is +\isa{{\isasymforall}z\isasymin A.\ P\ x} and +\isa{Bex\ A\ P}\index{*Bex (constant)} is \isa{\isasymexists z\isasymin A.\ P\ x}. For indexed unions and -intersections, you may see the constants \isa{UNION} and \isa{INTER}\@. +intersections, you may see the constants +\isa{UNION}\index{*UNION (constant)} and +\isa{INTER}\index{*INTER (constant)}\@. +The internal constant for $\varepsilon x.P(x)$ is +\isa{Eps}\index{*Eps (constant)}. + We have only scratched the surface of Isabelle/HOL's set theory. One primitive not mentioned here is the powerset operator @@ -379,10 +398,11 @@ \subsection{Finiteness and Cardinality} +\index{sets!finite}% The predicate \isa{finite} holds of all finite sets. Isabelle/HOL includes many familiar theorems about finiteness and cardinality (\isa{card}). For example, we have theorems concerning the cardinalities -of unions, intersections and the powerset: +of unions, intersections and the powerset:\index{cardinality} % \begin{isabelle} {\isasymlbrakk}finite\ A;\ finite\ B\isasymrbrakk\isanewline @@ -402,7 +422,8 @@ \rulename{n_subsets} \end{isabelle} Writing $|A|$ as $n$, the last of these theorems says that the number of -$k$-element subsets of~$A$ is $\binom{n}{k}$. +$k$-element subsets of~$A$ is \index{binomial coefficients} +$\binom{n}{k}$. \begin{warn} The term \isa{Finite\ A} is an abbreviation for @@ -410,26 +431,31 @@ set of all finite sets of a given type. There is no constant \isa{Finite}. \end{warn} - +\index{sets|)} + \section{Functions} -This section describes a few concepts that involve functions. -Some of the more important theorems are given along with the +\index{functions|(}% +This section describes a few concepts that involve +functions. Some of the more important theorems are given along with the names. A few sample proofs appear. Unlike with set theory, however, we cannot simply state lemmas and expect them to be proved using \isa{blast}. \subsection{Function Basics} -Two functions are \relax{equal} if they yield equal results given equal arguments. -This is the principle of \textbf{extensionality} for functions: +Two functions are \textbf{equal}\indexbold{equality!of functions} +if they yield equal results given equal +arguments. This is the principle of +\textbf{extensionality}\indexbold{extensionality!for functions} for +functions: \begin{isabelle} ({\isasymAnd}x.\ f\ x\ =\ g\ x)\ {\isasymLongrightarrow}\ f\ =\ g \rulename{ext} \end{isabelle} - +\indexbold{function updates}% Function \textbf{update} is useful for modelling machine states. It has the obvious definition and many useful facts are proved about it. In particular, the following equation is installed as a simplification @@ -450,7 +476,9 @@ when it is not being applied to an argument. \medskip -The \relax{identity} function and function \relax{composition} are defined: +The \bfindex{identity function} and function +\textbf{composition}\indexbold{composition!of functions} are +defined: \begin{isabelle}% id\ \isasymequiv\ {\isasymlambda}x.\ x% \rulename{id_def}\isanewline @@ -469,7 +497,8 @@ \subsection{Injections, Surjections, Bijections} -A function may be \relax{injective}, \relax{surjective} or \relax{bijective}: +\index{injections}\index{surjections}\index{bijections}% +A function may be \textbf{injective}, \textbf{surjective} or \textbf{bijective}: \begin{isabelle} inj_on\ f\ A\ \isasymequiv\ {\isasymforall}x\isasymin A.\ {\isasymforall}y\isasymin A.\ f\ x\ =\ f\ y\ \isasymlongrightarrow\ x\ @@ -488,7 +517,9 @@ of its domain type. Writing \isa{inj\ f} abbreviates \isa{inj_on\ f\ UNIV}, for when \isa{f} is injective everywhere. -The operator {\isa{inv}} expresses the \relax{inverse} of a function. In +The operator \isa{inv} expresses the +\textbf{inverse}\indexbold{inverse!of a function} +of a function. In general the inverse may not be well behaved. We have the usual laws, such as these: \begin{isabelle} @@ -552,7 +583,8 @@ \subsection{Function Image} -The \relax{image} of a set under a function is a most useful notion. It +The \textbf{image}\indexbold{image!under a function} +of a set under a function is a most useful notion. It has the obvious definition: \begin{isabelle} f\ `\ A\ \isasymequiv\ \isacharbraceleft y.\ \isasymexists x\isasymin @@ -601,7 +633,8 @@ theorem concerning images. \medskip -\relax{Inverse image} is also useful. It is defined as follows: +\textbf{Inverse image}\index{inverse image!of a function} is also useful. +It is defined as follows: \begin{isabelle} f\ -`\ B\ \isasymequiv\ \isacharbraceleft x.\ f\ x\ \isasymin\ B\isacharbraceright \rulename{vimage_def} @@ -612,25 +645,28 @@ f\ -`\ (-\ A)\ =\ -\ f\ -`\ A% \rulename{vimage_Compl} \end{isabelle} +\index{functions|)} \section{Relations} \label{sec:Relations} -A \relax{relation} is a set of pairs. As such, the set operations apply +\index{relations|(}% +A \textbf{relation} is a set of pairs. As such, the set operations apply to them. For instance, we may form the union of two relations. Other primitives are defined specifically for relations. \subsection{Relation Basics} -The \relax{identity} relation, also known as equality, has the obvious +The \bfindex{identity relation}, also known as equality, has the obvious definition: \begin{isabelle} Id\ \isasymequiv\ \isacharbraceleft p.\ \isasymexists x.\ p\ =\ (x,x){\isacharbraceright}% \rulename{Id_def} \end{isabelle} -\relax{Composition} of relations (the infix \isa{O}) is also available: +\indexbold{composition!of relations}% +\textbf{Composition} of relations (the infix \isa{O}) is also available: \begin{isabelle} r\ O\ s\ \isasymequiv\ \isacharbraceleft(x,z).\ \isasymexists y.\ (x,y)\ \isasymin\ s\ \isasymand\ (y,z)\ \isasymin\ r\isacharbraceright \rulename{comp_def} @@ -652,23 +688,27 @@ \rulename{comp_mono} \end{isabelle} -The \relax{converse} or inverse of a relation exchanges the roles -of the two operands. Note that \isa{\isacharcircum-1} is a postfix -operator. +\indexbold{converse!of a relation}% +\indexbold{inverse!of a relation}% +The \textbf{converse} or inverse of a +relation exchanges the roles of the two operands. We use the postfix +notation~\isa{r\isasyminverse} or +\isa{r\isacharcircum-1} in ASCII\@. \begin{isabelle} -((a,b)\ \isasymin\ r\isacharcircum-1)\ =\ +((a,b)\ \isasymin\ r\isasyminverse)\ =\ ((b,a)\ \isasymin\ r) \rulename{converse_iff} \end{isabelle} % Here is a typical law proved about converse and composition: \begin{isabelle} -(r\ O\ s){\isacharcircum}-1\ =\ s\isacharcircum-1\ O\ r\isacharcircum-1 +(r\ O\ s)\isasyminverse\ =\ s\isasyminverse\ O\ r\isasyminverse \rulename{converse_comp} \end{isabelle} -The \relax{image} of a set under a relation is defined analogously -to image under a function: +\indexbold{image!under a relation}% +The \textbf{image} of a set under a relation is defined +analogously to image under a function: \begin{isabelle} (b\ \isasymin\ r\ ``\ A)\ =\ (\isasymexists x\isasymin A.\ (x,b)\ \isasymin\ r) @@ -689,7 +729,7 @@ %\end{isabelle} -The \relax{domain} and \relax{range} of a relation are defined in the +The \bfindex{domain} and \bfindex{range} of a relation are defined in the standard way: \begin{isabelle} (a\ \isasymin\ Domain\ r)\ =\ (\isasymexists y.\ (a,y)\ \isasymin\ @@ -708,15 +748,17 @@ \begin{isabelle} R\ \isacharcircum\ \isadigit{0}\ =\ Id\isanewline R\ \isacharcircum\ Suc\ n\ =\ R\ O\ R\isacharcircum n -\rulename{RelPow.relpow.simps} +\rulename{relpow.simps} \end{isabelle} -\subsection{The Reflexive Transitive Closure} +\subsection{The Reflexive and Transitive Closure} -The \relax{reflexive transitive closure} of the -relation~\isa{r} is written with the -postfix syntax \isa{r\isacharcircum{*}} and appears in X-symbol notation -as~\isa{r\isactrlsup *}. It is the least solution of the equation +\index{closure!reflexive and transitive|(}% +The \textbf{reflexive and transitive closure} of the +relation~\isa{r} is written with a +postfix syntax. In ASCII we write \isa{r\isacharcircum*} and in +X-symbol notation~\isa{r\isactrlsup *}. It is the least solution of the +equation \begin{isabelle} r\isactrlsup *\ =\ Id\ \isasymunion \ (r\ O\ r\isactrlsup *) \rulename{rtrancl_unfold} @@ -750,8 +792,8 @@ \end{isabelle} \smallskip -The transitive closure is similar. It has two -introduction rules: +The transitive closure is similar. The ASCII syntax is +\isa{r\isacharcircum+}. It has two introduction rules: \begin{isabelle} p\ \isasymin \ r\ \isasymLongrightarrow \ p\ \isasymin \ r\isactrlsup + \rulename{r_into_trancl}\isanewline @@ -774,18 +816,21 @@ proved separately. The two proofs are almost identical. Here is the first one: \begin{isabelle} -\isacommand{lemma}\ rtrancl_converseD:\ "(x,y)\ \isasymin \ (r\isacharcircum -1)\isacharcircum *\ \isasymLongrightarrow \ (y,x)\ \isasymin \ r\isacharcircum *"\isanewline +\isacommand{lemma}\ rtrancl_converseD:\ "(x,y)\ \isasymin \ +(r\isasyminverse)\isactrlsup *\ \isasymLongrightarrow \ (y,x)\ \isasymin +\ r\isactrlsup *"\isanewline \isacommand{apply}\ (erule\ rtrancl_induct)\isanewline \ \isacommand{apply}\ (rule\ rtrancl_refl)\isanewline -\isacommand{apply}\ (blast\ intro:\ r_into_rtrancl\ -rtrancl_trans)\isanewline +\isacommand{apply}\ (blast\ intro:\ rtrancl_trans)\isanewline \isacommand{done} \end{isabelle} % The first step of the proof applies induction, leaving these subgoals: \begin{isabelle} \ 1.\ (x,\ x)\ \isasymin \ r\isactrlsup *\isanewline -\ 2.\ \isasymAnd y\ z.\ \isasymlbrakk (x,y)\ \isasymin \ (r\isasyminverse )\isactrlsup *;\ (y,z)\ \isasymin \ r\isasyminverse ;\ (y,x)\ \isasymin \ r\isactrlsup *\isasymrbrakk \isanewline +\ 2.\ \isasymAnd y\ z.\ \isasymlbrakk (x,y)\ \isasymin \ +(r\isasyminverse)\isactrlsup *;\ (y,z)\ \isasymin \ r\isasyminverse ;\ +(y,x)\ \isasymin \ r\isactrlsup *\isasymrbrakk \isanewline \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow \ (z,x)\ \isasymin \ r\isactrlsup * \end{isabelle} % @@ -796,17 +841,17 @@ applying the introduction rules shown above. The same proof script handles the other direction: \begin{isabelle} -\isacommand{lemma}\ rtrancl_converseI:\ "(y,x)\ \isasymin \ r\isacharcircum *\ \isasymLongrightarrow \ (x,y)\ \isasymin \ (r\isacharcircum -1)\isacharcircum *"\isanewline +\isacommand{lemma}\ rtrancl_converseI:\ "(y,x)\ \isasymin \ r\isactrlsup *\ \isasymLongrightarrow \ (x,y)\ \isasymin \ (r\isasyminverse)\isactrlsup *"\isanewline \isacommand{apply}\ (erule\ rtrancl_induct)\isanewline \ \isacommand{apply}\ (rule\ rtrancl_refl)\isanewline -\isacommand{apply}\ (blast\ intro:\ r_into_rtrancl\ rtrancl_trans)\isanewline +\isacommand{apply}\ (blast\ intro:\ rtrancl_trans)\isanewline \isacommand{done} \end{isabelle} Finally, we combine the two lemmas to prove the desired equation: \begin{isabelle} -\isacommand{lemma}\ rtrancl_converse:\ "(r\isacharcircum-1){\isacharcircum}*\ =\ (r\isacharcircum{*}){\isacharcircum}-1"\isanewline +\isacommand{lemma}\ rtrancl_converse:\ "(r\isasyminverse)\isactrlsup *\ =\ (r\isactrlsup *)\isasyminverse"\isanewline \isacommand{by}\ (auto\ intro:\ rtrancl_converseI\ dest:\ rtrancl_converseD) \end{isabelle} @@ -832,55 +877,43 @@ * \end{isabelle} Now that \isa{x} has been replaced by the pair \isa{(a,b)}, we can -proceed. Other methods that split variables in this way are \isa{force} -and \isa{auto}. Section~\ref{sec:products} will discuss proof techniques -for ordered pairs in more detail. +proceed. Other methods that split variables in this way are \isa{force}, +\isa{auto}, \isa{fast} and \isa{best}. Section~\ref{sec:products} will discuss proof +techniques for ordered pairs in more detail. \end{warn} - +\index{relations|)}\index{closure!reflexive and transitive|)} \section{Well-Founded Relations and Induction} \label{sec:Well-founded} -Induction comes in many forms, including traditional mathematical -induction, structural induction on lists and induction on size. -More general than these is induction over a well-founded relation. -Such a relation expresses the notion of a terminating process. +\index{relations!well-founded|(}% +A well-founded relation captures the notion of a terminating process. +Each \isacommand{recdef}\index{recdef@\isacommand{recdef}} +declaration must specify a well-founded relation that +justifies the termination of the desired recursive function. Most of the +forms of induction found in mathematics are merely special cases of +induction over a well-founded relation. + Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no infinite descending chains \[ \cdots \prec a@2 \prec a@1 \prec a@0. \] -If $\prec$ is well-founded then it can be used with the well-founded -induction rule: -\[ \infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}} \] -To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for -arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$. -Intuitively, the well-foundedness of $\prec$ ensures that the chains of -reasoning are finite. - -\smallskip -In Isabelle, the induction rule is expressed like this: -\begin{isabelle} -{\isasymlbrakk}wf\ r;\ - {\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\ -\isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\ -\isasymLongrightarrow\ P\ a -\rulename{wf_induct} -\end{isabelle} -Here \isa{wf\ r} expresses that the relation~\isa{r} is well-founded. - -Many familiar induction principles are instances of this rule. -For example, the predecessor relation on the natural numbers -is well-founded; induction over it is mathematical induction. -The ``tail of'' relation on lists is well-founded; induction over -it is structural induction. - -Well-foundedness can be difficult to show. The various +Well-foundedness can be hard to show. The various formulations are all complicated. However, often a relation is well-founded by construction. HOL provides -theorems concerning ways of constructing a well-founded relation. -For example, a relation can be defined by means of a measure function -involving an existing relation, or two relations can be -combined lexicographically. +theorems concerning ways of constructing a well-founded relation. The +most familiar way is to specify a \bfindex{measure function}~\isa{f} into +the natural numbers, when $\isa{x}\prec \isa{y}\iff \isa{f x} < \isa{f y}$; +we write this particular relation as +\isa{measure~f}. + +\begin{warn} +You may want to skip the rest of this section until you need to perform a +complex recursive function definition or induction. The induction rule +returned by +\isacommand{recdef} is good enough for most purposes. We use an explicit +well-founded induction only in \S\ref{sec:CTL-revisited}. +\end{warn} Isabelle/HOL declares \isa{less_than} as a relation object, that is, a set of pairs of natural numbers. Two theorems tell us that this @@ -892,11 +925,12 @@ \rulename{wf_less_than} \end{isabelle} -The notion of measure generalizes to the \textbf{inverse image} of +The notion of measure generalizes to the +\index{inverse image!of a relation}\textbf{inverse image} of a relation. Given a relation~\isa{r} and a function~\isa{f}, we express a new relation using \isa{f} as a measure. An infinite descending chain on this new relation would give rise to an infinite descending chain -on~\isa{r}. Isabelle/HOL holds the definition of this concept and a +on~\isa{r}. Isabelle/HOL defines this concept and proves a theorem stating that it preserves well-foundedness: \begin{isabelle} inv_image\ r\ f\ \isasymequiv\ \isacharbraceleft(x,y).\ (f\ x,\ f\ y)\ @@ -906,10 +940,10 @@ \rulename{wf_inv_image} \end{isabelle} -The most familiar notion of measure involves the natural numbers. This yields, -for example, induction on the length of a list (\isa{measure length}). -Isabelle/HOL defines -\isa{measure} specifically: +A measure function involves the natural numbers. The relation \isa{measure +size} justifies primitive recursion and structural induction over a +datatype. Isabelle/HOL defines +\isa{measure} as shown: \begin{isabelle} measure\ \isasymequiv\ inv_image\ less_than% \rulename{measure_def}\isanewline @@ -938,22 +972,58 @@ \textbf{recdef} declaration (\S\ref{sec:recdef-simplification}) to define the well-founded relation used to prove termination. -The \textbf{multiset ordering}, useful for hard termination proofs, is available -in the Library. Baader and Nipkow \cite[\S2.5]{Baader-Nipkow} discuss it. +The \bfindex{multiset ordering}, useful for hard termination proofs, is +available in the Library. Baader and Nipkow \cite[\S2.5]{Baader-Nipkow} +discuss it. + +\medskip +Induction comes in many forms, including traditional mathematical +induction, structural induction on lists and induction on size. All are +instances of the following rule, for a suitable well-founded +relation~$\prec$: +\[ \infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}} \] +To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for +arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$. +Intuitively, the well-foundedness of $\prec$ ensures that the chains of +reasoning are finite. + +\smallskip +In Isabelle, the induction rule is expressed like this: +\begin{isabelle} +{\isasymlbrakk}wf\ r;\ + {\isasymAnd}x.\ {\isasymforall}y.\ (y,x)\ \isasymin\ r\ +\isasymlongrightarrow\ P\ y\ \isasymLongrightarrow\ P\ x\isasymrbrakk\ +\isasymLongrightarrow\ P\ a +\rulename{wf_induct} +\end{isabelle} +Here \isa{wf\ r} expresses that the relation~\isa{r} is well-founded. + +Many familiar induction principles are instances of this rule. +For example, the predecessor relation on the natural numbers +is well-founded; induction over it is mathematical induction. +The ``tail of'' relation on lists is well-founded; induction over +it is structural induction. +\index{relations!well-founded|)} \section{Fixed Point Operators} -Fixed point operators define sets recursively. They are invoked -implicitly when making an inductive definition, as discussed in -Chap.\ts\ref{chap:inductive} below. However, they can be used directly, too. -The -\relax{least} or \relax{strongest} fixed point yields an inductive -definition; the \relax{greatest} or \relax{weakest} fixed point yields a +\index{fixed points|(}% +Fixed point operators define sets +recursively. They are invoked implicitly when making an inductive +definition, as discussed in Chap.\ts\ref{chap:inductive} below. However, +they can be used directly, too. The +\emph{least} or \emph{strongest} fixed point yields an inductive +definition; the \emph{greatest} or \emph{weakest} fixed point yields a coinductive definition. Mathematicians may wish to note that the existence of these fixed points is guaranteed by the Knaster-Tarski theorem. +\begin{warn} +Casual readers should skip the rest of this section. We use fixed point +operators only in \S\ref{sec:VMC}. +\end{warn} + The theory applies only to monotonic functions. Isabelle's definition of monotone is overloaded over all orderings: \begin{isabelle} @@ -992,7 +1062,7 @@ one derived from the minimality of {\isa{lfp}}. Observe that both theorems demand \isa{mono\ f} as a premise. -The greatest fixed point is similar, but it has a \relax{coinduction} rule: +The greatest fixed point is similar, but it has a \bfindex{coinduction} rule: \begin{isabelle} mono\ f\ \isasymLongrightarrow\ gfp\ f\ =\ f\ (gfp\ f) \rulename{gfp_unfold}% @@ -1002,8 +1072,9 @@ gfp\ f% \rulename{coinduct} \end{isabelle} -A \relax{bisimulation} is perhaps the best-known concept defined as a +A \bfindex{bisimulation} is perhaps the best-known concept defined as a greatest fixed point. Exhibiting a bisimulation to prove the equality of two agents in a process algebra is an example of coinduction. The coinduction rule can be strengthened in various ways; see theory \isa{Gfp} for details. +\index{fixed points|)} \ No newline at end of file