--- 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 \<Rightarrow> state set \<Rightarrow> state \<Rightarrow> state list \<Rightarrow> bool"
primrec
-"until A B s [] = (s \<in> B)"
+until:: "state set \<Rightarrow> state set \<Rightarrow> state \<Rightarrow> state list \<Rightarrow> bool" where
+"until A B s [] = (s \<in> B)" |
"until A B s (t#p) = (s \<in> A \<and> (s,t) \<in> M \<and> until A B t p)"
-(*<*)constdefs
- eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set"
+(*<*)definition
+ eusem :: "state set \<Rightarrow> state set \<Rightarrow> state set" where
"eusem A B \<equiv> {s. \<exists>p. until A B s p}"(*>*)
text{*\noindent
--- 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
--- 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}
--- 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}
--- 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%
--- 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 \<Rightarrow> bool \<Rightarrow> bool"
- "xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
+"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"
text{*\noindent
we may want to prove
--- 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:
*}
--- 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 "(\<lambda>(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 \<times> 'b \<Rightarrow> 'b \<times> 'a"
-primrec
- "swap (x,y) = (y,x)"
+primrec swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> '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"\<And>"}-quantified variables in a goal
-with the rewrite rule @{thm[source]split_paired_all}:
+Alternatively, you can split \emph{all} @{text"\<And>"}-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]}
--- 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 \<equiv> Abs_three 0"
- B:: three
- "B \<equiv> Abs_three 1"
- C :: three
- "C \<equiv> Abs_three 2"
+definition A :: three where "A \<equiv> Abs_three 0"
+definition B :: three where "B \<equiv> Abs_three 1"
+definition C :: three where "C \<equiv> Abs_three 2"
text{*
So far, everything was easy. But it is clear that reasoning about @{typ
--- 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%
--- 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}}
--- 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