# HG changeset patch # User blanchet # Date 1379973670 -7200 # Node ID b3e2022530e34d219f24d58f446df4a669bc360b # Parent 1045907bbf9ab9d0603c82d29a8454fdc222b51e register codatatypes with Nitpick diff -r 1045907bbf9a -r b3e2022530e3 src/Doc/Nitpick/document/root.tex --- a/src/Doc/Nitpick/document/root.tex Mon Sep 23 23:27:46 2013 +0200 +++ b/src/Doc/Nitpick/document/root.tex Tue Sep 24 00:01:10 2013 +0200 @@ -956,15 +956,7 @@ \subsection{Coinductive Datatypes} \label{coinductive-datatypes} -While Isabelle regrettably lacks a high-level mechanism for defining coinductive -datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's -\textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive -``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick -supports these lazy lists seamlessly and provides a hook, described in -\S\ref{registration-of-coinductive-datatypes}, to register custom coinductive -datatypes. - -(Co)intuitively, a coinductive datatype is similar to an inductive datatype but +A coinductive datatype is similar to an inductive datatype but allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a, \ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0, 1, 2, 3, \ldots]$ can be defined as lazy lists using the @@ -977,6 +969,7 @@ finite lists: \prew +\textbf{codatatype} $'a$ \textit{llist} = \textit{LNil}~$\mid$~\textit{LCons}~$'a$~``$'a\;\textit{llist}$'' \\[2\smallskipamount] \textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs\/}$'' \\ \textbf{nitpick} \\[2\smallskipamount] \slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount] @@ -992,6 +985,8 @@ The next example is more interesting: \prew +\textbf{primcorecursive}~$\textit{iterates}$~\textbf{where} \\ +``$\textit{iterates}~f\>a = \textit{LCons}~a~(\textit{iterates}~f\>(f\>a))$'' \textbf{.} \\[2\smallskipamount] \textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\ \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount] @@ -1072,15 +1067,14 @@ In the first \textbf{nitpick} invocation, the after-the-fact check discovered that the two known elements of type $'a~\textit{llist}$ are bisimilar, prompting -Nitpick to label the example ``quasi genuine.'' +Nitpick to label the example as only ``quasi genuine.'' A compromise between leaving out the bisimilarity predicate from the Kodkod -problem and performing the after-the-fact check is to specify a lower -nonnegative \textit{bisim\_depth} value than the default one provided by -Nitpick. In general, a value of $K$ means that Nitpick will require all lists to -be distinguished from each other by their prefixes of length $K$. Be aware that -setting $K$ to a too low value can overconstrain Nitpick, preventing it from -finding any counterexamples. +problem and performing the after-the-fact check is to specify a low +nonnegative \textit{bisim\_depth} value. In general, a value of $K$ means that +Nitpick will require all lists to be distinguished from each other by their +prefixes of length $K$. However, setting $K$ to a too low value can +overconstrain Nitpick, preventing it from finding any counterexamples. \subsection{Boxing} \label{boxing} diff -r 1045907bbf9a -r b3e2022530e3 src/HOL/BNF/Examples/Stream.thy --- a/src/HOL/BNF/Examples/Stream.thy Mon Sep 23 23:27:46 2013 +0200 +++ b/src/HOL/BNF/Examples/Stream.thy Tue Sep 24 00:01:10 2013 +0200 @@ -15,11 +15,6 @@ codatatype (sset: 'a) stream (map: smap rel: stream_all2) = Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65) -declaration {* - Nitpick_HOL.register_codatatype - @{typ "'a stream"} @{const_name stream_case} [dest_Const @{term Stream}] -*} - code_datatype Stream lemma stream_case_cert: diff -r 1045907bbf9a -r b3e2022530e3 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Sep 23 23:27:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Tue Sep 24 00:01:10 2013 +0200 @@ -132,8 +132,9 @@ val safe_elim_attrs = @{attributes [elim!]}; val iff_attrs = @{attributes [iff]}; val induct_simp_attrs = @{attributes [induct_simp]}; +val nitpick_attrs = @{attributes [nitpick_simp]}; val simp_attrs = @{attributes [simp]}; -val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs; +val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs @ simp_attrs; fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys); @@ -759,7 +760,7 @@ val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name)); val notes = - [(caseN, case_thms, code_simp_attrs), + [(caseN, case_thms, code_nitpick_simp_attrs), (case_congN, [case_cong_thm], []), (case_convN, case_conv_thms, []), (collapseN, safe_collapse_thms, simp_attrs), @@ -772,7 +773,7 @@ (expandN, expand_thms, []), (injectN, inject_thms, iff_attrs @ induct_simp_attrs), (nchotomyN, [nchotomy_thm], []), - (selN, all_sel_thms, code_simp_attrs), + (selN, all_sel_thms, code_nitpick_simp_attrs), (splitN, [split_thm], []), (split_asmN, [split_asm_thm], []), (splitsN, [split_thm, split_asm_thm], []), diff -r 1045907bbf9a -r b3e2022530e3 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Sep 23 23:27:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Sep 24 00:01:10 2013 +0200 @@ -47,8 +47,7 @@ type lfp_sugar_thms = (thm list * thm * Args.src list) - * (thm list list * Args.src list) - * (thm list list * Args.src list) + * (thm list list * thm list list * Args.src list) type gfp_sugar_thms = ((thm list * thm) list * Args.src list) @@ -201,8 +200,9 @@ val id_def = @{thm id_def}; val mp_conj = @{thm mp_conj}; +val nitpick_attrs = @{attributes [nitpick_simp]}; +val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs; val simp_attrs = @{attributes [simp]}; -val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs; fun tvar_subst thy Ts Us = Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) []; @@ -402,8 +402,7 @@ type lfp_sugar_thms = (thm list * thm * Args.src list) - * (thm list list * Args.src list) - * (thm list list * Args.src list); + * (thm list list * thm list list * Args.src list) type gfp_sugar_thms = ((thm list * thm) list * Args.src list) @@ -774,7 +773,7 @@ val rec_thmss = mk_iter_thmss rec_args_types recs rec_defs (map co_rec_of ctor_iter_thmss); in ((induct_thms, induct_thm, [induct_case_names_attr]), - (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs)) + (fold_thmss, rec_thmss, code_nitpick_simp_attrs @ simp_attrs)) end; fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss, @@ -1045,7 +1044,7 @@ coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; in ((coinduct_thms_pairs, coinduct_case_attrs), - (unfold_thmss, corec_thmss, []), + (unfold_thmss, corec_thmss, code_nitpick_simp_attrs), (safe_unfold_thmss, safe_corec_thmss), (disc_unfold_thmss, disc_corec_thmss, []), (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs), @@ -1403,10 +1402,10 @@ join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss; val notes = - [(mapN, map_thms, code_simp_attrs), - (rel_distinctN, rel_distinct_thms, code_simp_attrs), - (rel_injectN, rel_inject_thms, code_simp_attrs), - (setN, flat set_thmss, code_simp_attrs)] + [(mapN, map_thms, code_nitpick_simp_attrs @ simp_attrs), + (rel_distinctN, rel_distinct_thms, code_nitpick_simp_attrs @ simp_attrs), + (rel_injectN, rel_inject_thms, code_nitpick_simp_attrs @ simp_attrs), + (setN, flat set_thmss, code_nitpick_simp_attrs @ simp_attrs)] |> massage_simple_notes fp_b_name; in (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar), @@ -1441,8 +1440,7 @@ ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)), (iterss, iter_defss)), lthy) = let - val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs), - (rec_thmss, rec_attrs)) = + val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, iter_attrs)) = derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss iter_defss lthy; @@ -1457,9 +1455,9 @@ |> massage_simple_notes fp_common_name; val notes = - [(foldN, fold_thmss, K fold_attrs), + [(foldN, fold_thmss, K iter_attrs), (inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]), - (recN, rec_thmss, K rec_attrs), + (recN, rec_thmss, K iter_attrs), (simpsN, simp_thmss, K [])] |> massage_multi_notes; in diff -r 1045907bbf9a -r b3e2022530e3 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Mon Sep 23 23:27:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Tue Sep 24 00:01:10 2013 +0200 @@ -157,7 +157,7 @@ derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss co_iterss co_iter_defss lthy - |> `(fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) => + |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) => ([induct], fold_thmss, rec_thmss, [], [], [], [])) ||> (fn info => (SOME info, NONE)) else diff -r 1045907bbf9a -r b3e2022530e3 src/HOL/BNF/Tools/bnf_lfp_compat.ML --- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML Mon Sep 23 23:27:46 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML Tue Sep 24 00:01:10 2013 +0200 @@ -131,7 +131,7 @@ val all_notes = (case lfp_sugar_thms of NONE => [] - | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, _), (rec_thmss, _)) => + | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) => let val common_notes = (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) diff -r 1045907bbf9a -r b3e2022530e3 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Mon Sep 23 23:27:46 2013 +0200 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Tue Sep 24 00:01:10 2013 +0200 @@ -1,6 +1,6 @@ (* Title: HOL/Nitpick_Examples/Manual_Nits.thy Author: Jasmin Blanchette, TU Muenchen - Copyright 2009-2011 + Copyright 2009-2013 Examples from the Nitpick manual. *) @@ -12,7 +12,7 @@ suite. *) theory Manual_Nits -imports Main "~~/src/HOL/Library/Quotient_Product" Real +imports Main Real "~~/src/HOL/Library/Quotient_Product" "~~/src/HOL/BNF/BNF" begin chapter {* 2. First Steps *} @@ -193,35 +193,10 @@ subsection {* 2.9. Coinductive Datatypes *} -(* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since - we cannot rely on its presence, we expediently provide our own - axiomatization. The examples also work unchanged with Lochbihler's - "Coinductive_List" theory. *) - -(* BEGIN LAZY LIST SETUP *) -definition "llist = (UNIV\('a list + (nat \ 'a)) set)" - -typedef 'a llist = "llist\('a list + (nat \ 'a)) set" -unfolding llist_def by auto +codatatype 'a llist = LNil | LCons 'a "'a llist" -definition LNil where -"LNil = Abs_llist (Inl [])" -definition LCons where -"LCons y ys = Abs_llist (case Rep_llist ys of - Inl ys' \ Inl (y # ys') - | Inr f \ Inr (\n. case n of 0 \ y | Suc m \ f m))" - -axiomatization iterates :: "('a \ 'a) \ 'a \ 'a llist" - -lemma iterates_def [nitpick_simp]: -"iterates f a = LCons a (iterates f (f a))" -sorry - -declaration {* -Nitpick_HOL.register_codatatype @{typ "'a llist"} "" - (map dest_Const [@{term LNil}, @{term LCons}]) -*} -(* END LAZY LIST SETUP *) +primcorecursive iterates where +"iterates f a = LCons a (iterates f (f a))" . lemma "xs \ LCons a xs" nitpick [expect = genuine] diff -r 1045907bbf9a -r b3e2022530e3 src/HOL/ROOT --- a/src/HOL/ROOT Mon Sep 23 23:27:46 2013 +0200 +++ b/src/HOL/ROOT Tue Sep 24 00:01:10 2013 +0200 @@ -239,7 +239,7 @@ Trans_Closure Sets -session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL + +session "HOL-BNF-Nitpick_Examples" in Nitpick_Examples = "HOL-BNF" + description {* Author: Jasmin Blanchette, TU Muenchen Copyright 2009