# HG changeset patch # User blanchet # Date 1459279519 -7200 # Node ID f65ef4723acae54ac05e5e1da9dd4f05b2a551bb # Parent 4384baae875335f36c82c7d6357de7494b33d577 more 'corec' docs diff -r 4384baae8753 -r f65ef4723aca src/Doc/Corec/Corec.thy --- a/src/Doc/Corec/Corec.thy Tue Mar 29 19:17:05 2016 +0200 +++ b/src/Doc/Corec/Corec.thy Tue Mar 29 21:25:19 2016 +0200 @@ -21,7 +21,7 @@ text \ ... -\cite{isabelle-datatypes} +@{cite "isabelle-datatypes"} * friend * up to @@ -31,6 +31,8 @@ BNF link to papers + +* plugins (code) \ @@ -45,15 +47,13 @@ \label{ssec:simple-corecursion}\ text \ -The case studies by Rutten~\cite{rutten05} and Hinze~\cite{hinze10} on stream +The case studies by Rutten~@{cite rutten05} and Hinze~@{cite hinze10} on stream calculi serve as our starting point. Streams can be defined as follows (cf. @{file "~~/src/HOL/Library/Stream.thy"}): \ - codatatype (sset: 'a) stream = + codatatype 'a stream = SCons (shd: 'a) (stl: "'a stream") - for - map: smap text \ The @{command corec} command makes it possible to define functions where the @@ -92,8 +92,8 @@ text \ \noindent -The command emits two proof goals. The first one corresponds to the equation we -specified and is trivial to discharge. The second one is a parametricity goal +The command emits two subgoals. The first one corresponds to the equation we +specified and is trivial to discharge. The second one is a parametricity subgoal and can usually be discharged using the @{text transfer_prover} proof method. After registering @{const ssum} as a friend, we can use it in the corecursive @@ -126,7 +126,7 @@ text \ \noindent -The parametricity proof goal is given to @{text transfer_prover}. +The parametricity subgoal is given to @{text transfer_prover}. The @{const sprod} and @{const sexp} functions provide shuffle product and exponentiation on streams. We can use them to define the stream of factorial @@ -196,6 +196,43 @@ "ttimes t u = Node (lab t * lab u) (map (\(t', u'). tplus (ttimes t u') (ttimes t' u)) (zip (sub t) (sub u)))" +text \ +All the syntactic convenience provided by \keyw{primcorec} is also supported by +@{command corec}, @{command corecursive}, and @{command friend_of_corec}. In +particular, nesting through the function type can be expressed using +@{text \}-abstractions and function applications rather than through composition +(@{term "op \"}, the map function for @{text \}). For example: +\ + + codatatype 'a language = + Lang (\: bool) (\
: "'a \ 'a language") + +text \\blankline\ + + corec (friend) Plus :: "'a language \ 'a language \ 'a language" where + "Plus r s = Lang (\ r \ \ s) (\a. Plus (\
r a) (\
s a))" + +text \\blankline\ + + corec (friend) Times :: "'a language \ 'a language \ 'a language" where + "Times r s = Lang (\ r \ \ s) + (\a. if \ r then Plus (Times (\
r a) s) (\
s a) else Times (\
r a) s)" + +text \\blankline\ + + corec (friend) Star :: "'a language \ 'a language" where + "Star r = Lang True (\a. Times (\
r a) (Star r))" + +text \\blankline\ + + corec (friend) Inter :: "'a language \ 'a language \ 'a language" where + "Inter r s = Lang (\ r \ \ s) (\a. Inter (\
r a) (\
s a))" + +text \\blankline\ + + corec (friend) PLUS :: "'a language list \ 'a language" where + "PLUS xs = Lang (\x \ set xs. \ x) (\a. PLUS (map (\r. \
r a) xs))" + subsection \Mixed Recursion--Corecursion \label{ssec:mixed-recursion-corecursion}\ @@ -209,7 +246,7 @@ Intuitively, the unguarded recursive call can be unfolded to arbitrary finite depth, ultimately yielding a purely corecursive definition. An example is the @{term primes} function from Di Gianantonio and Miculan -\cite{di-gianantonio-miculan-2003}: +@{cite "di-gianantonio-miculan-2003"}: \ corecursive primes :: "nat \ nat \ nat stream" where @@ -241,10 +278,11 @@ most finitely often before taking the then branch and producing one constructor. There is a slight complication when @{term "m = 0 \ n > 1"}: Without the first disjunct in the @{text "if"} condition, the function could stall. (This corner -case was overlooked in the original example \cite{di-gianantonio-miculan-2003}.) +case was overlooked in the original example +@{cite "di-gianantonio-miculan-2003"}.) -In the following example, which defines the stream of Catalan numbers, -termination is discharged automatically using @{text lexicographic_order}: +In the following examples, termination is discharged automatically by +@{command corec} by invoking @{method lexicographic_order}: \ corec catalan :: "nat \ nat stream" where @@ -252,6 +290,10 @@ (if n > 0 then ssum (catalan (n - 1)) (SCons 0 (catalan (n + 1))) else SCons 1 (catalan 1))" + corec collatz :: "nat \ nat stream" where + "collatz n = (if even n \ n > 0 then collatz (n div 2) + else SCons n (collatz (3 * n + 1)))" + text \ A more elaborate case study, revolving around the filter function on lazy lists, is presented in @{file "~~/src/HOL/Corec_Examples/LFilter.thy"}. @@ -292,7 +334,9 @@ The structural coinduction principle for @{typ "'a stream"}, called @{thm [source] stream.coinduct}, is as follows: % -\[@{thm stream.coinduct[no_vars]}\] +\begin{indentblock} +@{thm stream.coinduct[no_vars]} +\end{indentblock} % Coinduction allows us to prove an equality @{text "l = r"} on streams by providing a relation @{text R} that relates @{text l} and @{text r} (first @@ -301,10 +345,12 @@ the selectors @{const shd} and @{const stl}); hence they must be equal. The coinduction up-to principle after registering @{const sskew} as friendly is -available as @{thm [source] sskew.coinduct} or -@{thm [source] stream.coinduct_upto(2)}: +available as @{thm [source] sskew.coinduct} and as one of the components of +the collection @{thm [source] stream.coinduct_upto}: % -\[@{thm sfsup.coinduct[no_vars]}\] +\begin{indentblock} +@{thm sfsup.coinduct[no_vars]} +\end{indentblock} % This rule is almost identical to structural coinduction, except that the corecursive application of @{term R} is replaced by @@ -366,12 +412,9 @@ command. Consider the following definitions: \ - codatatype (tset: 'a, 'b) tllist = - TNil (terminal : 'b) - | TCons (thd : 'a) (ttl : "('a, 'b) tllist") - for - map: tmap - rel: tllist_all2 + codatatype ('a, 'b) tllist = + TNil (terminal: 'b) + | TCons (thd: 'a) (ttl: "('a, 'b) tllist") corec (friend) square_elems :: "(nat, 'b) tllist \ (nat, 'b) tllist" where "square_elems xs = @@ -411,9 +454,11 @@ coinduction_upto nat_int_tllist: "(nat, int) tllist" text \ +\noindent This produces the theorems @{thm [source] nat_int_tllist.coinduct_upto} and @{thm [source] nat_int_tllist.cong_intros} (as well as the individually named -introduction rules), and extends @{thm [source] tllist.coinduct_upto}. +introduction rules) and extends @{thm [source] tllist.coinduct_upto} and +@{thm [source] tllist.cong_intros}. \ @@ -421,26 +466,99 @@ \label{ssec:uniqueness-reasoning}\ text \ -t is sometimes possible to achieve better automation by using a more specialized -proof method than coinduction. Uniqueness principles maintain a good balance -between expressiveness and automation. They exploit the property that a +It is sometimes possible to achieve better automation by using a more +specialized proof method than coinduction. Uniqueness principles maintain a good +balance between expressiveness and automation. They exploit the property that a corecursive specification is the unique solution to a fixpoint equation. + +The @{command corec}, @{command corecursive}, and @{command friend_of_corec} +commands generate a property @{text f.unique} about the function of interest +@{term f} that can be used to prove that any function that satisfies +@{term f}'s corecursive specification must be equal to @{term f}. For example: +\[@{thm ssum.unique[no_vars]}\] + +The uniqueness principles are not restricted to functions defined using +@{command corec} or @{command corecursive} or registered with +@{command friend_of_corec}. Suppose @{term "t x"} is an arbitrary term +depending on @{term x}. The @{method corec_unique} proof method, provided by our +tool, transforms subgoals of the form +\[@{term "(\x. f x = H x f) \ f x = t x"}\] +into +\[@{term "\x. t x = H x t"}\] +The higher-order functional @{term H} must be such that the equation +@{term "f x = H x f"} would be a valid @{command corec} specification---but +without nested self-calls or unguarded calls. Thus, @{method corec_unique} +proves uniqueness of @{term t} with respect to the given fixpoint equation +regardless of how @{term t} was defined. For example: \ + lemma + fixes f :: "nat stream \ nat stream \ nat stream" + assumes "\xs ys. f xs ys = + SCons (shd ys * shd xs) (ssum (f xs (stl ys)) (f (stl xs) ys))" + shows "f = sprod" + using assms + proof corec_unique + show "sprod = (\xs ys :: nat stream. + SCons (shd ys * shd xs) (ssum (sprod xs (stl ys)) (sprod (stl xs) ys)))" + apply (rule ext)+ + apply (subst sprod.code) + by simp + qed + section \Command Syntax \label{sec:command-syntax}\ -text \ -... -\ - - subsection \\keyw{corec} and \keyw{corecursive} \label{ssec:corec-and-corecursive}\ text \ -... +\begin{matharray}{rcl} + @{command_def "corec"} & : & @{text "local_theory \ local_theory"} \\ + @{command_def "corecursive"} & : & @{text "local_theory \ proof(prove)"} +\end{matharray} + +@{rail \ + (@@{command corec} | @@{command corecursive}) target? \ + @{syntax cr_options}? fix @'where' prop + ; + @{syntax_def cr_options}: '(' ((@{syntax plugins} | 'friend' | 'transfer') + ',') ')' +\} + +\medskip + +\noindent +The @{command corec} and @{command corecursive} commands introduce a corecursive +function over a codatatype. + +The syntactic entity \synt{target} can be used to specify a local context, +\synt{fix} denotes name with an optional type signature, and \synt{prop} denotes +a HOL proposition @{cite "isabelle-isar-ref"}. + +The optional target is optionally followed by a combination of the following +options: + +\begin{itemize} +\setlength{\itemsep}{0pt} + +\item +The @{text plugins} option indicates which plugins should be enabled +(@{text only}) or disabled (@{text del}). By default, all plugins are enabled. + +\item +The @{text friend} option indicates that the defined function should be +registered as a friend. This gives rise to additional proof obligations. + +\item +The @{text transfer} option indicates that an unconditional transfer rule +should be generated and proved @{text "by transfer_prover"}. The +@{text "[transfer_rule]"} attribute is set on the generated theorem. +\end{itemize} + +The @{command corec} command is an abbreviation for @{command corecursive} with +@{text "apply transfer_prover"} or @{text "apply lexicographic_order"} to +discharge any emerging proof obligations. \ @@ -448,7 +566,42 @@ \label{ssec:friend-of-corec}\ text \ -... +\begin{matharray}{rcl} + @{command_def "friend_of_corec"} & : & @{text "local_theory \ proof(prove)"} +\end{matharray} + +@{rail \ + @@{command friend_of_corec} target? \ + @{syntax foc_options}? fix @'where' prop + ; + @{syntax_def foc_options}: '(' ((@{syntax plugins} | 'transfer') + ',') ')' +\} + +\medskip + +\noindent +The @{command friend_of_corec} command registers a corecursive function as +friendly. + +The syntactic entity \synt{target} can be used to specify a local context, +\synt{fix} denotes name with an optional type signature, and \synt{prop} denotes +a HOL proposition @{cite "isabelle-isar-ref"}. + +The optional target is optionally followed by a combination of the following +options: + +\begin{itemize} +\setlength{\itemsep}{0pt} + +\item +The @{text plugins} option indicates which plugins should be enabled +(@{text only}) or disabled (@{text del}). By default, all plugins are enabled. + +\item +The @{text transfer} option indicates that an unconditional transfer rule +should be generated and proved @{text "by transfer_prover"}. The +@{text "[transfer_rule]"} attribute is set on the generated theorem. +\end{itemize} \ @@ -456,7 +609,23 @@ \label{ssec:coinduction-upto}\ text \ -... +\begin{matharray}{rcl} + @{command_def "coinduction_upto"} & : & @{text "local_theory \ local_theory"} +\end{matharray} + +@{rail \ + @@{command coinduction_upto} target? name ':' type +\} + +\medskip + +\noindent +The @{command coinduction_upto} generates a coinduction up-to rule for a given +instance of a (possibly polymorphic) codatatype and notes the result with the +specified prefix. + +The syntactic entity \synt{name} denotes an identifier and \synt{type} denotes a +type @{cite "isabelle-isar-ref"}. \ @@ -526,6 +695,7 @@ * unfinished tactics * polymorphism of corecUU_transfer * alternative views + * plugins \end{enumerate} \ diff -r 4384baae8753 -r f65ef4723aca src/Doc/Corec/document/root.tex --- a/src/Doc/Corec/document/root.tex Tue Mar 29 19:17:05 2016 +0200 +++ b/src/Doc/Corec/document/root.tex Tue Mar 29 21:25:19 2016 +0200 @@ -1,6 +1,7 @@ \documentclass[12pt,a4paper]{article} % fleqn \usepackage{lmodern} \usepackage[T1]{fontenc} +\usepackage{amsfonts} \usepackage{amsmath} \usepackage{cite} \usepackage{enumitem} diff -r 4384baae8753 -r f65ef4723aca src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Mar 29 19:17:05 2016 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Mar 29 21:25:19 2016 +0200 @@ -3094,8 +3094,9 @@ The syntactic entity \synt{target} can be used to specify a local context, \synt{name} denotes an identifier, \synt{typefree} denotes fixed type variable -(@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix} denotes the usual -parenthesized mixfix notation @{cite "isabelle-isar-ref"}. +(@{typ 'a}, @{typ 'b}, \ldots), \synt{mixfix} denotes the usual parenthesized +mixfix notation, and \synt{types} denotes a space-separated list of types +@{cite "isabelle-isar-ref"}. The @{syntax plugins} option indicates which plugins should be enabled (@{text only}) or disabled (@{text del}). By default, all plugins are enabled. diff -r 4384baae8753 -r f65ef4723aca src/Doc/Datatypes/document/root.tex --- a/src/Doc/Datatypes/document/root.tex Tue Mar 29 19:17:05 2016 +0200 +++ b/src/Doc/Datatypes/document/root.tex Tue Mar 29 21:25:19 2016 +0200 @@ -1,6 +1,7 @@ \documentclass[12pt,a4paper]{article} % fleqn \usepackage{lmodern} \usepackage[T1]{fontenc} +\usepackage{amsfonts} \usepackage{amsmath} \usepackage{cite} \usepackage{enumitem}