# HG changeset patch # User berghofe # Date 1184144019 -7200 # Node ID 3f8ad7418e55a2c91033beca09355eeb46404c55 # Parent f9f89b7cfdc7586a50a0854db7c4ab66e5533fb6 Adapted to new inductive definition package. diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/IsarOverview/Isar/Induction.thy --- a/doc-src/IsarOverview/Isar/Induction.thy Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/IsarOverview/Isar/Induction.thy Wed Jul 11 10:53:39 2007 +0200 @@ -180,11 +180,12 @@ text{* HOL also supports inductively defined sets. See \cite{LNCS2283} for details. As an example we define our own version of the reflexive transitive closure of a relation --- HOL provides a predefined one as well.*} -consts rtc :: "('a \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999) -inductive "r*" -intros -refl: "(x,x) \ r*" -step: "\ (x,y) \ r; (y,z) \ r* \ \ (x,z) \ r*" +inductive_set + rtc :: "('a \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999) + for r :: "('a \ 'a)set" +where + refl: "(x,x) \ r*" +| step: "\ (x,y) \ r; (y,z) \ r* \ \ (x,z) \ r*" text{* \noindent First the constant is declared as a function on binary diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/CTL/CTLind.thy --- a/doc-src/TutorialI/CTL/CTLind.thy Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/CTL/CTLind.thy Wed Jul 11 10:53:39 2007 +0200 @@ -24,10 +24,12 @@ % on the initial segment of M that avoids A. *} -consts Avoid :: "state \ state set \ state set"; -inductive "Avoid s A" -intros "s \ Avoid s A" - "\ t \ Avoid s A; t \ A; (t,u) \ M \ \ u \ Avoid s A"; +inductive_set + Avoid :: "state \ state set \ state set" + for s :: state and A :: "state set" +where + "s \ Avoid s A" + | "\ t \ Avoid s A; t \ A; (t,u) \ M \ \ u \ Avoid s A"; text{* It is easy to see that for any infinite @{term A}-avoiding path @{term f} diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/CTL/document/CTLind.tex --- a/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Wed Jul 11 10:53:39 2007 +0200 @@ -41,12 +41,13 @@ % on the initial segment of M that avoids A.% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{consts}\isamarkupfalse% -\ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequoteclose}\isanewline -\isacommand{inductive}\isamarkupfalse% -\ {\isachardoublequoteopen}Avoid\ s\ A{\isachardoublequoteclose}\isanewline -\isakeyword{intros}\ {\isachardoublequoteopen}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequoteclose}% +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ Avoid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ s\ {\isacharcolon}{\isacharcolon}\ state\ \isakeyword{and}\ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}state\ set{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ \ \ {\isachardoublequoteopen}s\ {\isasymin}\ Avoid\ s\ A{\isachardoublequoteclose}\isanewline +\ \ {\isacharbar}\ {\isachardoublequoteopen}{\isasymlbrakk}\ t\ {\isasymin}\ Avoid\ s\ A{\isacharsemicolon}\ t\ {\isasymnotin}\ A{\isacharsemicolon}\ {\isacharparenleft}t{\isacharcomma}u{\isacharparenright}\ {\isasymin}\ M\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ u\ {\isasymin}\ Avoid\ s\ A{\isachardoublequoteclose}% \begin{isamarkuptext}% It is easy to see that for any infinite \isa{A}-avoiding path \isa{f} with \isa{f\ {\isadigit{0}}\ {\isasymin}\ Avoid\ s\ A} there is an infinite \isa{A}-avoiding path diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/AB.thy --- a/doc-src/TutorialI/Inductive/AB.thy Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Inductive/AB.thy Wed Jul 11 10:53:39 2007 +0200 @@ -34,30 +34,26 @@ text{*\noindent Words over this alphabet are of type @{typ"alfa list"}, and -the three nonterminals are declared as sets of such words: -*} - -consts S :: "alfa list set" - A :: "alfa list set" - B :: "alfa list set" - -text{*\noindent +the three nonterminals are declared as sets of such words. The productions above are recast as a \emph{mutual} inductive definition\index{inductive definition!simultaneous} of @{term S}, @{term A} and~@{term B}: *} -inductive S A B -intros +inductive_set + S :: "alfa list set" + and A :: "alfa list set" + and B :: "alfa list set" +where "[] \ S" - "w \ A \ b#w \ S" - "w \ B \ a#w \ S" +| "w \ A \ b#w \ S" +| "w \ B \ a#w \ S" - "w \ S \ a#w \ A" - "\ v\A; w\A \ \ b#v@w \ A" +| "w \ S \ a#w \ A" +| "\ v\A; w\A \ \ b#v@w \ A" - "w \ S \ b#w \ B" - "\ v \ B; w \ B \ \ a#v@w \ B" +| "w \ S \ b#w \ B" +| "\ v \ B; w \ B \ \ a#v@w \ B" text{*\noindent First we show that all words in @{term S} contain the same number of @{term diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/Advanced.thy --- a/doc-src/TutorialI/Inductive/Advanced.thy Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Inductive/Advanced.thy Wed Jul 11 10:53:39 2007 +0200 @@ -6,9 +6,10 @@ datatype integer_op = Number int | UnaryMinus | Plus; -consts gterms :: "'f set \ 'f gterm set" -inductive "gterms F" -intros +inductive_set + gterms :: "'f set \ 'f gterm set" + for F :: "'f set" +where step[intro!]: "\\t \ set args. t \ gterms F; f \ F\ \ (Apply f args) \ gterms F" @@ -83,17 +84,19 @@ "integer_arity UnaryMinus = 1" "integer_arity Plus = 2" -consts well_formed_gterm :: "('f \ nat) \ 'f gterm set" -inductive "well_formed_gterm arity" -intros +inductive_set + well_formed_gterm :: "('f \ nat) \ 'f gterm set" + for arity :: "'f \ nat" +where step[intro!]: "\\t \ set args. t \ well_formed_gterm arity; length args = arity f\ \ (Apply f args) \ well_formed_gterm arity" -consts well_formed_gterm' :: "('f \ nat) \ 'f gterm set" -inductive "well_formed_gterm' arity" -intros +inductive_set + well_formed_gterm' :: "('f \ nat) \ 'f gterm set" + for arity :: "'f \ nat" +where step[intro!]: "\args \ lists (well_formed_gterm' arity); length args = arity f\ \ (Apply f args) \ well_formed_gterm' arity" @@ -136,26 +139,28 @@ text{* the rest isn't used: too complicated. OK for an exercise though.*} -consts integer_signature :: "(integer_op * (unit list * unit)) set" -inductive "integer_signature" -intros -Number: "(Number n, ([], ())) \ integer_signature" -UnaryMinus: "(UnaryMinus, ([()], ())) \ integer_signature" -Plus: "(Plus, ([(),()], ())) \ integer_signature" +inductive_set + integer_signature :: "(integer_op * (unit list * unit)) set" +where + Number: "(Number n, ([], ())) \ integer_signature" +| UnaryMinus: "(UnaryMinus, ([()], ())) \ integer_signature" +| Plus: "(Plus, ([(),()], ())) \ integer_signature" -consts well_typed_gterm :: "('f \ 't list * 't) \ ('f gterm * 't)set" -inductive "well_typed_gterm sig" -intros +inductive_set + well_typed_gterm :: "('f \ 't list * 't) \ ('f gterm * 't)set" + for sig :: "'f \ 't list * 't" +where step[intro!]: "\\pair \ set args. pair \ well_typed_gterm sig; sig f = (map snd args, rtype)\ \ (Apply f (map fst args), rtype) \ well_typed_gterm sig" -consts well_typed_gterm' :: "('f \ 't list * 't) \ ('f gterm * 't)set" -inductive "well_typed_gterm' sig" -intros +inductive_set + well_typed_gterm' :: "('f \ 't list * 't) \ ('f gterm * 't)set" + for sig :: "'f \ 't list * 't" +where step[intro!]: "\args \ lists(well_typed_gterm' sig); sig f = (map snd args, rtype)\ diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/Even.thy --- a/doc-src/TutorialI/Inductive/Even.thy Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Inductive/Even.thy Wed Jul 11 10:53:39 2007 +0200 @@ -2,11 +2,10 @@ theory Even imports Main begin -consts even :: "nat set" -inductive even -intros -zero[intro!]: "0 \ even" -step[intro!]: "n \ even \ (Suc (Suc n)) \ even" +inductive_set even :: "nat set" +where + zero[intro!]: "0 \ even" +| step[intro!]: "n \ even \ (Suc (Suc n)) \ even" text{*An inductive definition consists of introduction rules. diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/Mutual.thy --- a/doc-src/TutorialI/Inductive/Mutual.thy Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Inductive/Mutual.thy Wed Jul 11 10:53:39 2007 +0200 @@ -8,14 +8,13 @@ natural numbers: *} -consts Even :: "nat set" - Odd :: "nat set" - -inductive Even Odd -intros -zero: "0 \ Even" -EvenI: "n \ Odd \ Suc n \ Even" -OddI: "n \ Even \ Suc n \ Odd" +inductive_set + Even :: "nat set" + and Odd :: "nat set" +where + zero: "0 \ Even" +| EvenI: "n \ Odd \ Suc n \ Even" +| OddI: "n \ Even \ Suc n \ Odd" text{*\noindent The mutually inductive definition of multiple sets is no different from diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/Star.thy --- a/doc-src/TutorialI/Inductive/Star.thy Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Inductive/Star.thy Wed Jul 11 10:53:39 2007 +0200 @@ -14,11 +14,12 @@ available. But now they are: *} -consts rtc :: "('a \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999) -inductive "r*" -intros -rtc_refl[iff]: "(x,x) \ r*" -rtc_step: "\ (x,y) \ r; (y,z) \ r* \ \ (x,z) \ r*" +inductive_set + rtc :: "('a \ 'a)set \ ('a \ 'a)set" ("_*" [1000] 999) + for r :: "('a \ 'a)set" +where + rtc_refl[iff]: "(x,x) \ r*" +| rtc_step: "\ (x,y) \ r; (y,z) \ r* \ \ (x,z) \ r*" text{*\noindent The function @{term rtc} is annotated with concrete syntax: instead of @@ -119,12 +120,13 @@ relation containing @{term r}. The latter is easily formalized *} -consts rtc2 :: "('a \ 'a)set \ ('a \ 'a)set" -inductive "rtc2 r" -intros -"(x,y) \ r \ (x,y) \ rtc2 r" -"(x,x) \ rtc2 r" -"\ (x,y) \ rtc2 r; (y,z) \ rtc2 r \ \ (x,z) \ rtc2 r" +inductive_set + rtc2 :: "('a \ 'a)set \ ('a \ 'a)set" + for r :: "('a \ 'a)set" +where + "(x,y) \ r \ (x,y) \ rtc2 r" +| "(x,x) \ rtc2 r" +| "\ (x,y) \ rtc2 r; (y,z) \ rtc2 r \ \ (x,z) \ rtc2 r" text{*\noindent and the equivalence of the two definitions is easily shown by the obvious rule diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/document/AB.tex --- a/doc-src/TutorialI/Inductive/document/AB.tex Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Inductive/document/AB.tex Wed Jul 11 10:53:39 2007 +0200 @@ -68,32 +68,27 @@ \begin{isamarkuptext}% \noindent Words over this alphabet are of type \isa{alfa\ list}, and -the three nonterminals are declared as sets of such words:% -\end{isamarkuptext}% -\isamarkuptrue% -\isacommand{consts}\isamarkupfalse% -\ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}% -\begin{isamarkuptext}% -\noindent +the three nonterminals are declared as sets of such words. The productions above are recast as a \emph{mutual} inductive definition\index{inductive definition!simultaneous} of \isa{S}, \isa{A} and~\isa{B}:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{inductive}\isamarkupfalse% -\ S\ A\ B\isanewline -\isakeyword{intros}\isanewline +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ S\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{and}\ A\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{and}\ B\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}alfa\ list\ set{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline \ \ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}w\ {\isasymin}\ A\ {\isasymLongrightarrow}\ b{\isacharhash}w\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}w\ {\isasymin}\ B\ {\isasymLongrightarrow}\ a{\isacharhash}w\ {\isasymin}\ S{\isachardoublequoteclose}\isanewline \isanewline -\ \ {\isachardoublequoteopen}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ a{\isacharhash}w\ \ \ {\isasymin}\ A{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}{\isasymlbrakk}\ v{\isasymin}A{\isacharsemicolon}\ w{\isasymin}A\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ b{\isacharhash}v{\isacharat}w\ {\isasymin}\ A{\isachardoublequoteclose}\isanewline \isanewline -\ \ {\isachardoublequoteopen}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequoteclose}\isanewline -\ \ {\isachardoublequoteopen}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequoteclose}% +{\isacharbar}\ {\isachardoublequoteopen}w\ {\isasymin}\ S\ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ b{\isacharhash}w\ \ \ {\isasymin}\ B{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}{\isasymlbrakk}\ v\ {\isasymin}\ B{\isacharsemicolon}\ w\ {\isasymin}\ B\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ a{\isacharhash}v{\isacharat}w\ {\isasymin}\ B{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent First we show that all words in \isa{S} contain the same number of \isa{a}'s and \isa{b}'s. Since the definition of \isa{S} is by mutual diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/document/Advanced.tex --- a/doc-src/TutorialI/Inductive/document/Advanced.tex Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Inductive/document/Advanced.tex Wed Jul 11 10:53:39 2007 +0200 @@ -25,11 +25,11 @@ \isacommand{datatype}\isamarkupfalse% \ integer{\isacharunderscore}op\ {\isacharequal}\ Number\ int\ {\isacharbar}\ UnaryMinus\ {\isacharbar}\ Plus\isanewline \isanewline -\isacommand{consts}\isamarkupfalse% -\ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline -\isacommand{inductive}\isamarkupfalse% -\ {\isachardoublequoteopen}gterms\ F{\isachardoublequoteclose}\isanewline -\isakeyword{intros}\isanewline +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ gterms\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ set\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ F\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ set{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F{\isacharsemicolon}\ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ gterms\ F{\isachardoublequoteclose}\isanewline \isanewline @@ -48,7 +48,8 @@ \begin{isamarkuptxt}% \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasyminter}\ {\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ gterms\ G{\isacharbraceright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G% \end{isabelle}% \end{isamarkuptxt}% @@ -136,7 +137,8 @@ \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ gterms\ F\ {\isasyminter}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ t\ {\isasymin}\ }{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ x\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharbraceright}{\isacharsemicolon}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }f\ {\isasymin}\ F{\isasymrbrakk}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymLongrightarrow}\ }Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}% @@ -191,21 +193,21 @@ {\isachardoublequoteopen}integer{\isacharunderscore}arity\ UnaryMinus\ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline {\isachardoublequoteopen}integer{\isacharunderscore}arity\ Plus\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isadigit{2}}{\isachardoublequoteclose}\isanewline \isanewline -\isacommand{consts}\isamarkupfalse% -\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline -\isacommand{inductive}\isamarkupfalse% -\ {\isachardoublequoteopen}well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequoteclose}\isanewline -\isakeyword{intros}\isanewline +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ well{\isacharunderscore}formed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}t\ {\isasymin}\ set\ args{\isachardot}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharsemicolon}\ \ \isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isachardoublequoteclose}\isanewline \isanewline \isanewline -\isacommand{consts}\isamarkupfalse% -\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline -\isacommand{inductive}\isamarkupfalse% -\ {\isachardoublequoteopen}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequoteclose}\isanewline -\isakeyword{intros}\isanewline +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}f\ gterm\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ arity\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymlbrakk}args\ {\isasymin}\ lists\ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharparenright}{\isacharsemicolon}\ \ \isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ args{\isacharparenright}\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isachardoublequoteclose}\isanewline @@ -236,8 +238,8 @@ \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ }t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasyminter}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}\ \ \ t\ {\isasymin}\ }{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharbraceright}{\isacharsemicolon}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity% \end{isabelle}% @@ -284,7 +286,7 @@ \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymlbrakk}args\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}}{\isasymin}\ lists\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ }{\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\isanewline -\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline +\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ {\isasymlbrakk}{\isasymin}\ \ {\isacharparenleft}}{\isacharbraceleft}a{\isachardot}\ a\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ \ }length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline \isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }{\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity% \end{isabelle}% @@ -312,32 +314,31 @@ the rest isn't used: too complicated. OK for an exercise though.% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{consts}\isamarkupfalse% -\ integer{\isacharunderscore}signature\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}integer{\isacharunderscore}op\ {\isacharasterisk}\ {\isacharparenleft}unit\ list\ {\isacharasterisk}\ unit{\isacharparenright}{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline -\isacommand{inductive}\isamarkupfalse% -\ {\isachardoublequoteopen}integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline -\isakeyword{intros}\isanewline -Number{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}Number\ n{\isacharcomma}\ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline -UnaryMinus{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}UnaryMinus{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline -Plus{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}Plus{\isacharcomma}\ \ \ \ \ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharcomma}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ integer{\isacharunderscore}signature\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}integer{\isacharunderscore}op\ {\isacharasterisk}\ {\isacharparenleft}unit\ list\ {\isacharasterisk}\ unit{\isacharparenright}{\isacharparenright}\ set{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ Number{\isacharcolon}\ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}Number\ n{\isacharcomma}\ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline +{\isacharbar}\ UnaryMinus{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}UnaryMinus{\isacharcomma}\ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline +{\isacharbar}\ Plus{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}Plus{\isacharcomma}\ \ \ \ \ \ \ {\isacharparenleft}{\isacharbrackleft}{\isacharparenleft}{\isacharparenright}{\isacharcomma}{\isacharparenleft}{\isacharparenright}{\isacharbrackright}{\isacharcomma}\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ integer{\isacharunderscore}signature{\isachardoublequoteclose}\isanewline \isanewline \isanewline -\isacommand{consts}\isamarkupfalse% -\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequoteclose}\isanewline -\isacommand{inductive}\isamarkupfalse% -\ {\isachardoublequoteopen}well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequoteclose}\isanewline -\isakeyword{intros}\isanewline +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ well{\isacharunderscore}typed{\isacharunderscore}gterm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ sig\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}{\isasymforall}pair\ {\isasymin}\ set\ args{\isachardot}\ pair\ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isacharsemicolon}\ \isanewline \ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline \ \ \ \ \ {\isasymLongrightarrow}\ {\isacharparenleft}Apply\ f\ {\isacharparenleft}map\ fst\ args{\isacharparenright}{\isacharcomma}\ rtype{\isacharparenright}\ \isanewline \ \ \ \ \ \ \ \ \ {\isasymin}\ well{\isacharunderscore}typed{\isacharunderscore}gterm\ sig{\isachardoublequoteclose}\isanewline \isanewline -\isacommand{consts}\isamarkupfalse% -\ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequoteclose}\isanewline -\isacommand{inductive}\isamarkupfalse% -\ {\isachardoublequoteopen}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isachardoublequoteclose}\isanewline -\isakeyword{intros}\isanewline +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}f\ gterm\ {\isacharasterisk}\ {\isacharprime}t{\isacharparenright}set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ sig\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}f\ {\isasymRightarrow}\ {\isacharprime}t\ list\ {\isacharasterisk}\ {\isacharprime}t{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ \isanewline \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}args\ {\isasymin}\ lists{\isacharparenleft}well{\isacharunderscore}typed{\isacharunderscore}gterm{\isacharprime}\ sig{\isacharparenright}{\isacharsemicolon}\ \isanewline \ \ \ \ \ \ sig\ f\ {\isacharequal}\ {\isacharparenleft}map\ snd\ args{\isacharcomma}\ rtype{\isacharparenright}{\isasymrbrakk}\isanewline diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/document/Even.tex --- a/doc-src/TutorialI/Inductive/document/Even.tex Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Inductive/document/Even.tex Wed Jul 11 10:53:39 2007 +0200 @@ -19,13 +19,11 @@ \endisadelimtheory \isanewline \isanewline -\isacommand{consts}\isamarkupfalse% +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% \ even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline -\isacommand{inductive}\isamarkupfalse% -\ even\isanewline -\isakeyword{intros}\isanewline -zero{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline -step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}% +\isakeyword{where}\isanewline +\ \ zero{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ even{\isachardoublequoteclose}\isanewline +{\isacharbar}\ step{\isacharbrackleft}intro{\isacharbang}{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isasymin}\ even{\isachardoublequoteclose}% \begin{isamarkuptext}% An inductive definition consists of introduction rules. @@ -35,7 +33,7 @@ \rulename{even.step} \begin{isabelle}% -\ \ \ \ \ {\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% +\ \ \ \ \ {\isasymlbrakk}x\ {\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\ x% \end{isabelle} \rulename{even.induct} diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/document/Mutual.tex --- a/doc-src/TutorialI/Inductive/document/Mutual.tex Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Inductive/document/Mutual.tex Wed Jul 11 10:53:39 2007 +0200 @@ -25,16 +25,14 @@ natural numbers:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{consts}\isamarkupfalse% -\ Even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \ Odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% \isanewline -\isacommand{inductive}\isamarkupfalse% -\ Even\ Odd\isanewline -\isakeyword{intros}\isanewline -zero{\isacharcolon}\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline -EvenI{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ Odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline -OddI{\isacharcolon}\ \ {\isachardoublequoteopen}n\ {\isasymin}\ Even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ Odd{\isachardoublequoteclose}% +\ \ Even\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{and}\ Odd\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ set{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ zero{\isacharcolon}\ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline +{\isacharbar}\ EvenI{\isacharcolon}\ {\isachardoublequoteopen}n\ {\isasymin}\ Odd\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ Even{\isachardoublequoteclose}\isanewline +{\isacharbar}\ OddI{\isacharcolon}\ \ {\isachardoublequoteopen}n\ {\isasymin}\ Even\ {\isasymLongrightarrow}\ Suc\ n\ {\isasymin}\ Odd{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent The mutually inductive definition of multiple sets is no different from diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Inductive/document/Star.tex --- a/doc-src/TutorialI/Inductive/document/Star.tex Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Inductive/document/Star.tex Wed Jul 11 10:53:39 2007 +0200 @@ -32,13 +32,13 @@ available. But now they are:% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{consts}\isamarkupfalse% -\ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline -\isacommand{inductive}\isamarkupfalse% -\ {\isachardoublequoteopen}r{\isacharasterisk}{\isachardoublequoteclose}\isanewline -\isakeyword{intros}\isanewline -rtc{\isacharunderscore}refl{\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline -rtc{\isacharunderscore}step{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}% +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ rtc\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharunderscore}{\isacharasterisk}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline +\ \ \isakeyword{for}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ rtc{\isacharunderscore}refl{\isacharbrackleft}iff{\isacharbrackright}{\isacharcolon}\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}\isanewline +{\isacharbar}\ rtc{\isacharunderscore}step{\isacharcolon}\ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent The function \isa{rtc} is annotated with concrete syntax: instead of @@ -87,9 +87,9 @@ To prove transitivity, we need rule induction, i.e.\ theorem \isa{rtc{\isachardot}induct}: \begin{isabelle}% -\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}xb{\isacharcomma}\ {\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline +\ \ \ \ \ {\isasymlbrakk}{\isacharparenleft}{\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}{\isacharcomma}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ x{\isacharsemicolon}\isanewline \isaindent{\ \ \ \ \ \ }{\isasymAnd}x\ y\ z{\isachardot}\ {\isasymlbrakk}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}\ z{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}{\isacharsemicolon}\ {\isacharquery}P\ y\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ x\ z{\isasymrbrakk}\isanewline -\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}xb\ {\isacharquery}xa% +\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ {\isacharquery}P\ {\isacharquery}x{\isadigit{1}}{\isachardot}{\isadigit{0}}\ {\isacharquery}x{\isadigit{2}}{\isachardot}{\isadigit{0}}% \end{isabelle} It says that \isa{{\isacharquery}P} holds for an arbitrary pair \isa{{\isacharparenleft}{\isacharquery}xb{\isacharcomma}{\isacharquery}xa{\isacharparenright}\ {\isasymin}\ {\isacharquery}r{\isacharasterisk}} if \isa{{\isacharquery}P} is preserved by all rules of the inductive definition, i.e.\ if \isa{{\isacharquery}P} holds for the conclusion provided it holds for the @@ -196,14 +196,14 @@ relation containing \isa{r}. The latter is easily formalized% \end{isamarkuptext}% \isamarkuptrue% -\isacommand{consts}\isamarkupfalse% -\ rtc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline -\isacommand{inductive}\isamarkupfalse% -\ {\isachardoublequoteopen}rtc{\isadigit{2}}\ r{\isachardoublequoteclose}\isanewline -\isakeyword{intros}\isanewline -{\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}\isanewline -{\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}\isanewline -{\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}% +\isacommand{inductive{\isacharunderscore}set}\isamarkupfalse% +\isanewline +\ \ rtc{\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline +\ \ \isakeyword{for}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequoteclose}\isanewline +\isakeyword{where}\isanewline +\ \ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}{\isacharparenleft}x{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}\isanewline +{\isacharbar}\ {\isachardoublequoteopen}{\isasymlbrakk}\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isacharsemicolon}\ {\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ rtc{\isadigit{2}}\ r{\isachardoublequoteclose}% \begin{isamarkuptext}% \noindent and the equivalence of the two definitions is easily shown by the obvious rule diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Wed Jul 11 10:53:39 2007 +0200 @@ -66,13 +66,14 @@ (** Inductive definition of all "parts" of a message. **) -consts parts :: "msg set => msg set" -inductive "parts H" - intros +inductive_set + parts :: "msg set => msg set" + for H :: "msg set" + where Inj [intro]: "X \ H ==> X \ parts H" - Fst: "{|X,Y|} \ parts H ==> X \ parts H" - Snd: "{|X,Y|} \ parts H ==> Y \ parts H" - Body: "Crypt K X \ parts H ==> X \ parts H" + | Fst: "{|X,Y|} \ parts H ==> X \ parts H" + | Snd: "{|X,Y|} \ parts H ==> Y \ parts H" + | Body: "Crypt K X \ parts H ==> X \ parts H" (*Monotonicity*) @@ -87,13 +88,14 @@ messages, including keys. A form of downward closure. Pairs can be taken apart; messages decrypted with known keys. **) -consts analz :: "msg set => msg set" -inductive "analz H" - intros +inductive_set + analz :: "msg set => msg set" + for H :: "msg set" + where Inj [intro,simp] : "X \ H ==> X \ analz H" - Fst: "{|X,Y|} \ analz H ==> X \ analz H" - Snd: "{|X,Y|} \ analz H ==> Y \ analz H" - Decrypt [dest]: + | Fst: "{|X,Y|} \ analz H ==> X \ analz H" + | Snd: "{|X,Y|} \ analz H ==> Y \ analz H" + | Decrypt [dest]: "[|Crypt K X \ analz H; Key(invKey K) \ analz H|] ==> X \ analz H" @@ -109,15 +111,16 @@ encrypted with known keys. Agent names are public domain. Numbers can be guessed, but Nonces cannot be. **) -consts synth :: "msg set => msg set" -inductive "synth H" - intros +inductive_set + synth :: "msg set => msg set" + for H :: "msg set" + where Inj [intro]: "X \ H ==> X \ synth H" - Agent [intro]: "Agent agt \ synth H" - Number [intro]: "Number n \ synth H" - Hash [intro]: "X \ synth H ==> Hash X \ synth H" - MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" - Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" + | Agent [intro]: "Agent agt \ synth H" + | Number [intro]: "Number n \ synth H" + | Hash [intro]: "X \ synth H ==> Hash X \ synth H" + | MPair [intro]: "[|X \ synth H; Y \ synth H|] ==> {|X,Y|} \ synth H" + | Crypt [intro]: "[|X \ synth H; Key(K) \ H|] ==> Crypt K X \ synth H" (*Monotonicity*) lemma synth_mono: "G<=H ==> synth(G) <= synth(H)" diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Protocol/Message_lemmas.ML --- a/doc-src/TutorialI/Protocol/Message_lemmas.ML Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Protocol/Message_lemmas.ML Wed Jul 11 10:53:39 2007 +0200 @@ -450,7 +450,7 @@ \ analz (insert (Crypt K X) H) \\ \ \ insert (Crypt K X) (analz (insert X H))"; by (rtac subsetI 1); -by (eres_inst_tac [("xa","x")] analz.induct 1); +by (eres_inst_tac [("x","x")] analz.induct 1); by Auto_tac; val lemma1 = result(); @@ -458,7 +458,7 @@ \ insert (Crypt K X) (analz (insert X H)) \\ \ \ analz (insert (Crypt K X) H)"; by Auto_tac; -by (eres_inst_tac [("xa","x")] analz.induct 1); +by (eres_inst_tac [("x","x")] analz.induct 1); by Auto_tac; by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1); val lemma2 = result(); diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Protocol/NS_Public.thy --- a/doc-src/TutorialI/Protocol/NS_Public.thy Wed Jul 11 10:52:20 2007 +0200 +++ b/doc-src/TutorialI/Protocol/NS_Public.thy Wed Jul 11 10:53:39 2007 +0200 @@ -9,32 +9,31 @@ theory NS_Public imports Public begin -consts ns_public :: "event list set" - -inductive ns_public - intros +inductive_set + ns_public :: "event list set" + where (*Initial trace is empty*) Nil: "[] \ ns_public" (*The spy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1. Common to all similar protocols.*) - Fake: "\evs \ ns_public; X \ synth (analz (knows Spy evs))\ + | Fake: "\evs \ ns_public; X \ synth (analz (knows Spy evs))\ \ Says Spy B X # evs \ ns_public" (*Alice initiates a protocol run, sending a nonce to Bob*) - NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ + | NS1: "\evs1 \ ns_public; Nonce NA \ used evs1\ \ Says A B (Crypt (pubK B) \Nonce NA, Agent A\) # evs1 \ ns_public" (*Bob responds to Alice's message with a further nonce*) - NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; + | NS2: "\evs2 \ ns_public; Nonce NB \ used evs2; Says A' B (Crypt (pubK B) \Nonce NA, Agent A\) \ set evs2\ \ Says B A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) # evs2 \ ns_public" (*Alice proves her existence by sending NB back to Bob.*) - NS3: "\evs3 \ ns_public; + | NS3: "\evs3 \ ns_public; Says A B (Crypt (pubK B) \Nonce NA, Agent A\) \ set evs3; Says B' A (Crypt (pubK A) \Nonce NA, Nonce NB, Agent B\) \ set evs3\