# HG changeset patch # User nipkow # Date 1212162730 -7200 # Node ID 63f0b638355cf76f585979f1c041bc69df7bcfb8 # Parent 3602b81665b59d28af0a7cf53a85cea2274d9d0b *** empty log message *** diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/CTL/CTL.thy Fri May 30 17:52:10 2008 +0200 @@ -337,12 +337,12 @@ an auxiliary function: *} -consts until:: "state set \ state set \ state \ state list \ bool" primrec -"until A B s [] = (s \ B)" +until:: "state set \ state set \ state \ state list \ bool" where +"until A B s [] = (s \ B)" | "until A B s (t#p) = (s \ A \ (s,t) \ M \ until A B t p)" -(*<*)constdefs - eusem :: "state set \ state set \ state set" +(*<*)definition + eusem :: "state set \ state set \ state set" where "eusem A B \ {s. \p. until A B s p}"(*>*) text{*\noindent diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri May 30 17:52:10 2008 +0200 @@ -470,11 +470,10 @@ an auxiliary function:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{consts}\isamarkupfalse% -\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline \isacommand{primrec}\isamarkupfalse% \isanewline -{\isachardoublequoteopen}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline +until{\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +{\isachardoublequoteopen}until\ A\ B\ s\ {\isacharbrackleft}{\isacharbrackright}\ \ \ \ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ B{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbar}\isanewline {\isachardoublequoteopen}until\ A\ B\ s\ {\isacharparenleft}t{\isacharhash}p{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}s\ {\isasymin}\ A\ {\isasymand}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ until\ A\ B\ t\ p{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/Documents/Documents.thy Fri May 30 17:52:10 2008 +0200 @@ -474,11 +474,9 @@ subsection {\ttlbrace}* Basic definitions *{\ttrbrace} - consts - foo :: \dots - bar :: \dots + definition foo :: \dots - defs \dots + definition bar :: \dots subsection {\ttlbrace}* Derived rules *{\ttrbrace} diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Fri May 30 17:52:10 2008 +0200 @@ -523,11 +523,9 @@ subsection {\ttlbrace}* Basic definitions *{\ttrbrace} - consts - foo :: \dots - bar :: \dots + definition foo :: \dots - defs \dots + definition bar :: \dots subsection {\ttlbrace}* Derived rules *{\ttrbrace} diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri May 30 17:52:10 2008 +0200 @@ -225,9 +225,9 @@ For example, given% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{constdefs}\isamarkupfalse% -\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}xor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}% +\isacommand{definition}\isamarkupfalse% +\ xor\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isakeyword{where}\isanewline +{\isachardoublequoteopen}xor\ A\ B\ {\isasymequiv}\ {\isacharparenleft}A\ {\isasymand}\ {\isasymnot}B{\isacharparenright}\ {\isasymor}\ {\isacharparenleft}{\isasymnot}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent we may want to prove% diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Misc/simp.thy --- a/doc-src/TutorialI/Misc/simp.thy Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/Misc/simp.thy Fri May 30 17:52:10 2008 +0200 @@ -161,8 +161,8 @@ For example, given *} -constdefs xor :: "bool \ bool \ bool" - "xor A B \ (A \ \B) \ (\A \ B)" +definition xor :: "bool \ bool \ bool" where +"xor A B \ (A \ \B) \ (\A \ B)" text{*\noindent we may want to prove diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Types/Axioms.thy --- a/doc-src/TutorialI/Types/Axioms.thy Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/Types/Axioms.thy Fri May 30 17:52:10 2008 +0200 @@ -143,7 +143,7 @@ txt{*\noindent @{subgoals[display,show_sorts]} -Assuming @{text"'a :: parord"}, the three axioms of class @{text strord} +Because of @{text"'a :: parord"}, the three axioms of class @{text strord} are easily proved: *} diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Types/Pairs.thy --- a/doc-src/TutorialI/Types/Pairs.thy Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/Types/Pairs.thy Fri May 30 17:52:10 2008 +0200 @@ -1,4 +1,4 @@ -(*<*)theory Pairs imports Main begin(*>*) +(*<*)theory Pairs imports Main begin hide const swap(*>*) section{*Pairs and Tuples*} @@ -57,20 +57,20 @@ lemma "(\(x,y).x) p = fst p" by(simp add: split_def) -text{* This works well if rewriting with @{thm[source]split_def} finishes the +text{* \noindent +This works well if rewriting with @{thm[source]split_def} finishes the proof, as it does above. But if it does not, you end up with exactly what we are trying to avoid: nests of @{term fst} and @{term snd}. Thus this approach is neither elegant nor very practical in large examples, although it can be effective in small ones. If we consider why this lemma presents a problem, -we quickly realize that we need to replace the variable~@{term +we realize that we need to replace variable~@{term p} by some pair @{term"(a,b)"}. Then both sides of the equation would simplify to @{term a} by the simplification rules @{thm split_conv[no_vars]} and @{thm fst_conv[no_vars]}. To reason about tuple patterns requires some way of converting a variable of product type into a pair. - In case of a subterm of the form @{term"split f p"} this is easy: the split rule @{thm[source]split_split} replaces @{term p} by a pair:% \index{*split (method)} @@ -126,9 +126,7 @@ *} (*<*)by(simp split: split_split_asm)(*>*) -consts swap :: "'a \ 'b \ 'b \ 'a" -primrec - "swap (x,y) = (y,x)" +primrec swap :: "'a \ 'b \ 'b \ 'a" where "swap (x,y) = (y,x)" text{*\noindent Note that the above \isacommand{primrec} definition is admissible @@ -138,10 +136,10 @@ lemma "swap(swap p) = p" txt{*\noindent -simplification will do nothing, because the defining equation for @{const swap} -expects a pair. Again, we need to turn @{term p} into a pair first, but this -time there is no @{term split} in sight. In this case the only thing we can do -is to split the term by hand: +simplification will do nothing, because the defining equation for +@{const[source] swap} expects a pair. Again, we need to turn @{term p} +into a pair first, but this time there is no @{term split} in sight. +The only thing we can do is to split the term by hand: *} apply(case_tac p) @@ -154,9 +152,8 @@ appear preferable to the more arcane methods introduced first. However, see the warning about @{text case_tac} in \S\ref{sec:struct-ind-case}. -In case the term to be split is a quantified variable, there are more options. -You can split \emph{all} @{text"\"}-quantified variables in a goal -with the rewrite rule @{thm[source]split_paired_all}: +Alternatively, you can split \emph{all} @{text"\"}-quantified variables +in a goal with the rewrite rule @{thm[source]split_paired_all}: *} (*<*)by simp(*>*) @@ -164,7 +161,7 @@ apply(simp only: split_paired_all) txt{*\noindent -@{subgoals[display,indent=0]} +@{subgoals[display,indent=0,margin=70]} *} apply simp @@ -195,7 +192,7 @@ by simp; text{*\noindent -To turn off this automatic splitting, just disable the +To turn off this automatic splitting, disable the responsible simplification rules: \begin{center} @{thm split_paired_All[no_vars]} diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Types/Typedefs.thy --- a/doc-src/TutorialI/Types/Typedefs.thy Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/Types/Typedefs.thy Fri May 30 17:52:10 2008 +0200 @@ -132,13 +132,9 @@ names: *} -constdefs - A:: three - "A \ Abs_three 0" - B:: three - "B \ Abs_three 1" - C :: three - "C \ Abs_three 2" +definition A :: three where "A \ Abs_three 0" +definition B :: three where "B \ Abs_three 1" +definition C :: three where "C \ Abs_three 2" text{* So far, everything was easy. But it is clear that reasoning about @{typ diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Types/document/Axioms.tex --- a/doc-src/TutorialI/Types/document/Axioms.tex Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/Types/document/Axioms.tex Fri May 30 17:52:10 2008 +0200 @@ -259,7 +259,7 @@ type\ variables{\isacharcolon}\isanewline \isaindent{\ \ }{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord% \end{isabelle} -Assuming \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord} +Because of \isa{{\isacharprime}a\ {\isacharcolon}{\isacharcolon}\ parord}, the three axioms of class \isa{strord} are easily proved:% \end{isamarkuptxt}% \isamarkuptrue% diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Types/document/Pairs.tex --- a/doc-src/TutorialI/Types/document/Pairs.tex Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/Types/document/Pairs.tex Fri May 30 17:52:10 2008 +0200 @@ -95,6 +95,7 @@ \endisadelimproof % \begin{isamarkuptext}% +\noindent This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the proof, as it does above. But if it does not, you end up with exactly what we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this @@ -102,12 +103,11 @@ can be effective in small ones. If we consider why this lemma presents a problem, -we quickly realize that we need to replace the variable~\isa{p} by some pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}. Then both sides of the +we realize that we need to replace variable~\isa{p} by some pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}. Then both sides of the equation would simplify to \isa{a} by the simplification rules \isa{split\ f\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ f\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}. To reason about tuple patterns requires some way of converting a variable of product type into a pair. - In case of a subterm of the form \isa{split\ f\ p} this is easy: the split rule \isa{split{\isacharunderscore}split} replaces \isa{p} by a pair:% \index{*split (method)}% @@ -233,11 +233,8 @@ \isadelimproof % \endisadelimproof -\isacommand{consts}\isamarkupfalse% -\ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequoteclose}\isanewline \isacommand{primrec}\isamarkupfalse% -\isanewline -\ \ {\isachardoublequoteopen}swap\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardoublequoteclose}% +\ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\ {\isachardoublequoteopen}swap\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent Note that the above \isacommand{primrec} definition is admissible @@ -254,10 +251,10 @@ % \begin{isamarkuptxt}% \noindent -simplification will do nothing, because the defining equation for \isa{Pairs{\isachardot}swap} -expects a pair. Again, we need to turn \isa{p} into a pair first, but this -time there is no \isa{split} in sight. In this case the only thing we can do -is to split the term by hand:% +simplification will do nothing, because the defining equation for +\isa{swap} expects a pair. Again, we need to turn \isa{p} +into a pair first, but this time there is no \isa{split} in sight. +The only thing we can do is to split the term by hand:% \end{isamarkuptxt}% \isamarkuptrue% \isacommand{apply}\isamarkupfalse% @@ -265,7 +262,7 @@ \begin{isamarkuptxt}% \noindent \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ Pairs{\isachardot}swap\ {\isacharparenleft}Pairs{\isachardot}swap\ p{\isacharparenright}\ {\isacharequal}\ p% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ swap\ {\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p% \end{isabelle} Again, \methdx{case_tac} is applicable because \isa{{\isasymtimes}} is a datatype. The subgoal is easily proved by \isa{simp}. @@ -274,9 +271,8 @@ appear preferable to the more arcane methods introduced first. However, see the warning about \isa{case{\isacharunderscore}tac} in \S\ref{sec:struct-ind-case}. -In case the term to be split is a quantified variable, there are more options. -You can split \emph{all} \isa{{\isasymAnd}}-quantified variables in a goal -with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:% +Alternatively, you can split \emph{all} \isa{{\isasymAnd}}-quantified variables +in a goal with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:% \end{isamarkuptxt}% \isamarkuptrue% % @@ -299,9 +295,7 @@ \begin{isamarkuptxt}% \noindent \begin{isabelle}% -\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }Pairs{\isachardot}swap\ {\isacharparenleft}Pairs{\isachardot}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}% +\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\ swap\ {\isacharparenleft}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}% \end{isabelle}% \end{isamarkuptxt}% \isamarkuptrue% @@ -368,7 +362,7 @@ % \begin{isamarkuptext}% \noindent -To turn off this automatic splitting, just disable the +To turn off this automatic splitting, disable the responsible simplification rules: \begin{center} \isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}} diff -r 3602b81665b5 -r 63f0b638355c doc-src/TutorialI/Types/document/Typedefs.tex --- a/doc-src/TutorialI/Types/document/Typedefs.tex Fri May 30 17:03:37 2008 +0200 +++ b/doc-src/TutorialI/Types/document/Typedefs.tex Fri May 30 17:52:10 2008 +0200 @@ -177,14 +177,12 @@ names:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{constdefs}\isamarkupfalse% -\isanewline -\ \ A{\isacharcolon}{\isacharcolon}\ three\isanewline -\ {\isachardoublequoteopen}A\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline -\ \ B{\isacharcolon}{\isacharcolon}\ three\isanewline -\ {\isachardoublequoteopen}B\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline -\ \ C\ {\isacharcolon}{\isacharcolon}\ three\isanewline -\ {\isachardoublequoteopen}C\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{2}}{\isachardoublequoteclose}% +\isacommand{definition}\isamarkupfalse% +\ A\ {\isacharcolon}{\isacharcolon}\ three\ \isakeyword{where}\ {\isachardoublequoteopen}A\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline +\isacommand{definition}\isamarkupfalse% +\ B\ {\isacharcolon}{\isacharcolon}\ three\ \isakeyword{where}\ {\isachardoublequoteopen}B\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline +\isacommand{definition}\isamarkupfalse% +\ C\ {\isacharcolon}{\isacharcolon}\ three\ \isakeyword{where}\ {\isachardoublequoteopen}C\ {\isasymequiv}\ Abs{\isacharunderscore}three\ {\isadigit{2}}{\isachardoublequoteclose}% \begin{isamarkuptext}% So far, everything was easy. But it is clear that reasoning about \isa{three} will be hell if we have to go back to \isa{nat} every time. Thus our aim must be to raise our level of abstraction by deriving enough theorems