--- 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}
--- 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:
--- 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], []),
--- 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
--- 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
--- 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 [])
--- 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\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
-
-typedef 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> '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' \<Rightarrow> Inl (y # ys')
- | Inr f \<Rightarrow> Inr (\<lambda>n. case n of 0 \<Rightarrow> y | Suc m \<Rightarrow> f m))"
-
-axiomatization iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> '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 \<noteq> LCons a xs"
nitpick [expect = genuine]
--- 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