# HG changeset patch # User wenzelm # Date 1163069925 -3600 # Node ID 58223c67fd8b12724b3fdd3f69b1ee285728c3aa # Parent 11ba04d15f36d6202f9a901e96446fae87a2d6eb updated; diff -r 11ba04d15f36 -r 58223c67fd8b doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Thu Nov 09 11:58:43 2006 +0100 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Thu Nov 09 11:58:45 2006 +0100 @@ -141,7 +141,7 @@ for a change, we do not use fixed point induction. Park-induction, named after David Park, is weaker but sufficient for this proof: \begin{center} -\isa{f\ S\ {\isasymsubseteq}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymsubseteq}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound}) +\isa{f\ S\ {\isasymle}\ S\ {\isasymLongrightarrow}\ lfp\ f\ {\isasymle}\ S} \hfill (\isa{lfp{\isacharunderscore}lowerbound}) \end{center} The instance of the premise \isa{f\ S\ {\isasymsubseteq}\ S} is proved pointwise, a decision that \isa{auto} takes for us:% diff -r 11ba04d15f36 -r 58223c67fd8b doc-src/TutorialI/CTL/document/PDL.tex --- a/doc-src/TutorialI/CTL/document/PDL.tex Thu Nov 09 11:58:43 2006 +0100 +++ b/doc-src/TutorialI/CTL/document/PDL.tex Thu Nov 09 11:58:45 2006 +0100 @@ -155,7 +155,7 @@ \end{isamarkuptxt}% \isamarkuptrue% \ \isacommand{apply}\isamarkupfalse% -{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharparenright}\isanewline +{\isacharparenleft}erule\ lfp{\isacharunderscore}induct{\isacharunderscore}set{\isacharparenright}\isanewline \ \ \isacommand{apply}\isamarkupfalse% {\isacharparenleft}rule\ mono{\isacharunderscore}ef{\isacharparenright}\isanewline \ \isacommand{apply}\isamarkupfalse% diff -r 11ba04d15f36 -r 58223c67fd8b doc-src/TutorialI/Inductive/document/Advanced.tex --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Nov 09 11:58:43 2006 +0100 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Thu Nov 09 11:58:45 2006 +0100 @@ -66,8 +66,7 @@ % \begin{isamarkuptext}% \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\isanewline -\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P% +\ \ \ \ \ {\isasymlbrakk}a\ {\isasymin}\ even{\isacharsemicolon}\ a\ {\isacharequal}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}a\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% \end{isabelle} \rulename{even.cases} @@ -84,7 +83,7 @@ \ Suc{\isacharunderscore}Suc{\isacharunderscore}cases% \begin{isamarkuptext}% \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% +\ \ \ \ \ {\isasymlbrakk}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P% \end{isabelle} \rulename{Suc_Suc_cases} diff -r 11ba04d15f36 -r 58223c67fd8b doc-src/TutorialI/Inductive/document/Even.tex --- a/doc-src/TutorialI/Inductive/document/Even.tex Thu Nov 09 11:58:43 2006 +0100 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Thu Nov 09 11:58:45 2006 +0100 @@ -30,13 +30,12 @@ An inductive definition consists of introduction rules. \begin{isabelle}% -\ \ \ \ \ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ Even{\isachardot}even% +\ \ \ \ \ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isasymin}\ even% \end{isabelle} \rulename{even.step} \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}xa\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ P\ {\isadigit{0}}{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ P\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\isanewline -\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ P\ xa% +\ \ \ \ \ {\isasymlbrakk}xa\ {\isasymin}\ even{\isacharsemicolon}\ P\ {\isadigit{0}}{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ P\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ xa% \end{isabelle} \rulename{even.induct} @@ -60,8 +59,8 @@ The first step is induction on the natural number \isa{k}, which leaves two subgoals: \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ Even{\isachardot}even\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ Even{\isachardot}even% +\ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isadigit{0}}\ {\isasymin}\ even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isadigit{2}}\ {\isacharasterisk}\ Suc\ n\ {\isasymin}\ even% \end{isabelle} Here \isa{auto} simplifies both subgoals so that they match the introduction rules, which then are applied automatically.% @@ -119,7 +118,7 @@ \begin{isamarkuptxt}% \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ dvd\ {\isadigit{0}}\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isadigit{2}}\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isadigit{2}}\ dvd\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% \end{isabelle}% \end{isamarkuptxt}% \isamarkuptrue% @@ -127,7 +126,7 @@ \ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ dvd{\isacharunderscore}def{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ {\isasymexists}k{\isachardot}\ n\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymexists}k{\isachardot}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ k% \end{isabelle}% \end{isamarkuptxt}% \isamarkuptrue% @@ -135,7 +134,7 @@ \ clarify% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ Even{\isachardot}even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ ka% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}n\ k{\isachardot}\ {\isadigit{2}}\ {\isacharasterisk}\ k\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isasymexists}ka{\isachardot}\ Suc\ {\isacharparenleft}Suc\ {\isacharparenleft}{\isadigit{2}}\ {\isacharasterisk}\ k{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ ka% \end{isabelle}% \end{isamarkuptxt}% \isamarkuptrue% @@ -187,8 +186,8 @@ \ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ Even{\isachardot}even\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ Even{\isachardot}even% +\ {\isadigit{1}}{\isachardot}\ n\ {\isasymin}\ even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}na{\isachardot}\ {\isasymlbrakk}na\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ n\ {\isasymin}\ even% \end{isabelle}% \end{isamarkuptxt}% \isamarkuptrue% @@ -217,9 +216,8 @@ \ {\isacharparenleft}erule\ even{\isachardot}induct{\isacharparenright}% \begin{isamarkuptxt}% \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even\isanewline -\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ Even{\isachardot}even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even{\isasymrbrakk}\isanewline -\isaindent{\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ }{\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ Even{\isachardot}even% +\ {\isadigit{1}}{\isachardot}\ {\isadigit{0}}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even\isanewline +\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ n\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even{\isasymrbrakk}\ {\isasymLongrightarrow}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharminus}\ {\isadigit{2}}\ {\isasymin}\ even% \end{isabelle}% \end{isamarkuptxt}% \isamarkuptrue% diff -r 11ba04d15f36 -r 58223c67fd8b doc-src/TutorialI/Recdef/document/simplification.tex --- a/doc-src/TutorialI/Recdef/document/simplification.tex Thu Nov 09 11:58:43 2006 +0100 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Thu Nov 09 11:58:45 2006 +0100 @@ -47,17 +47,17 @@ condition simplifies to \isa{True} or \isa{False}. For example, simplification reduces \begin{isabelle}% -\ \ \ \ \ simplification{\isachardot}gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k% +\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k% \end{isabelle} in one step to \begin{isabelle}% -\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ simplification{\isachardot}gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k% +\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ {\isadigit{0}}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k% \end{isabelle} where the condition cannot be reduced further, and splitting leads to \begin{isabelle}% -\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ simplification{\isachardot}gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}% +\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}% \end{isabelle} -Since the recursive call \isa{simplification{\isachardot}gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by +Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by an \isa{if}, it is unfolded again, which leads to an infinite chain of simplification steps. Fortunately, this problem can be avoided in many different ways. @@ -69,7 +69,7 @@ \isa{if} is involved. If possible, the definition should be given by pattern matching on the left -rather than \isa{if} on the right. In the case of \isa{simplification{\isachardot}gcd} the +rather than \isa{if} on the right. In the case of \isa{gcd} the following alternative definition suggests itself:% \end{isamarkuptext}% \isamarkuptrue% @@ -100,7 +100,7 @@ always available. A final alternative is to replace the offending simplification rules by -derived conditional ones. For \isa{simplification{\isachardot}gcd} it means we have to prove +derived conditional ones. For \isa{gcd} it means we have to prove these lemmas:% \end{isamarkuptext}% \isamarkuptrue% diff -r 11ba04d15f36 -r 58223c67fd8b doc-src/TutorialI/Types/document/Numbers.tex --- a/doc-src/TutorialI/Types/document/Numbers.tex Thu Nov 09 11:58:43 2006 +0100 +++ b/doc-src/TutorialI/Types/document/Numbers.tex Thu Nov 09 11:58:45 2006 +0100 @@ -572,8 +572,9 @@ effect of show sorts on the above \begin{isabelle}% -{\isacharparenleft}{\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\isanewline -{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}field{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% +{\isacharparenleft}{\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isacharequal}\isanewline +\isaindent{{\isacharparenleft}}{\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\isanewline +{\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}division{\isacharunderscore}ring{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% \end{isabelle} \rulename{field_mult_cancel_right}% \end{isamarkuptext}%