register codatatypes with Nitpick
authorblanchet
Tue Sep 24 00:01:10 2013 +0200 (2013-09-24)
changeset 53808b3e2022530e3
parent 53807 1045907bbf9a
child 53809 2c0e45bb2f05
register codatatypes with Nitpick
src/Doc/Nitpick/document/root.tex
src/HOL/BNF/Examples/Stream.thy
src/HOL/BNF/Tools/bnf_ctr_sugar.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
src/HOL/BNF/Tools/bnf_lfp_compat.ML
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/ROOT
     1.1 --- a/src/Doc/Nitpick/document/root.tex	Mon Sep 23 23:27:46 2013 +0200
     1.2 +++ b/src/Doc/Nitpick/document/root.tex	Tue Sep 24 00:01:10 2013 +0200
     1.3 @@ -956,15 +956,7 @@
     1.4  \subsection{Coinductive Datatypes}
     1.5  \label{coinductive-datatypes}
     1.6  
     1.7 -While Isabelle regrettably lacks a high-level mechanism for defining coinductive
     1.8 -datatypes, the \textit{Coinductive\_List} theory from Andreas Lochbihler's
     1.9 -\textit{Coinductive} AFP entry \cite{lochbihler-2010} provides a coinductive
    1.10 -``lazy list'' datatype, $'a~\textit{llist}$, defined the hard way. Nitpick
    1.11 -supports these lazy lists seamlessly and provides a hook, described in
    1.12 -\S\ref{registration-of-coinductive-datatypes}, to register custom coinductive
    1.13 -datatypes.
    1.14 -
    1.15 -(Co)intuitively, a coinductive datatype is similar to an inductive datatype but
    1.16 +A coinductive datatype is similar to an inductive datatype but
    1.17  allows infinite objects. Thus, the infinite lists $\textit{ps}$ $=$ $[a, a, a,
    1.18  \ldots]$, $\textit{qs}$ $=$ $[a, b, a, b, \ldots]$, and $\textit{rs}$ $=$ $[0,
    1.19  1, 2, 3, \ldots]$ can be defined as lazy lists using the
    1.20 @@ -977,6 +969,7 @@
    1.21  finite lists:
    1.22  
    1.23  \prew
    1.24 +\textbf{codatatype} $'a$ \textit{llist} = \textit{LNil}~$\mid$~\textit{LCons}~$'a$~``$'a\;\textit{llist}$'' \\[2\smallskipamount]
    1.25  \textbf{lemma} ``$\textit{xs} \not= \textit{LCons}~a~\textit{xs\/}$'' \\
    1.26  \textbf{nitpick} \\[2\smallskipamount]
    1.27  \slshape Nitpick found a counterexample for {\itshape card}~$'a$ = 1: \\[2\smallskipamount]
    1.28 @@ -992,6 +985,8 @@
    1.29  The next example is more interesting:
    1.30  
    1.31  \prew
    1.32 +\textbf{primcorecursive}~$\textit{iterates}$~\textbf{where} \\
    1.33 +``$\textit{iterates}~f\>a = \textit{LCons}~a~(\textit{iterates}~f\>(f\>a))$'' \textbf{.} \\[2\smallskipamount]
    1.34  \textbf{lemma}~``$\lbrakk\textit{xs} = \textit{LCons}~a~\textit{xs};\>\,
    1.35  \textit{ys} = \textit{iterates}~(\lambda b.\> a)~b\rbrakk \,\Longrightarrow\, \textit{xs} = \textit{ys\/}$'' \\
    1.36  \textbf{nitpick} [\textit{verbose}] \\[2\smallskipamount]
    1.37 @@ -1072,15 +1067,14 @@
    1.38  
    1.39  In the first \textbf{nitpick} invocation, the after-the-fact check discovered
    1.40  that the two known elements of type $'a~\textit{llist}$ are bisimilar, prompting
    1.41 -Nitpick to label the example ``quasi genuine.''
    1.42 +Nitpick to label the example as only ``quasi genuine.''
    1.43  
    1.44  A compromise between leaving out the bisimilarity predicate from the Kodkod
    1.45 -problem and performing the after-the-fact check is to specify a lower
    1.46 -nonnegative \textit{bisim\_depth} value than the default one provided by
    1.47 -Nitpick. In general, a value of $K$ means that Nitpick will require all lists to
    1.48 -be distinguished from each other by their prefixes of length $K$. Be aware that
    1.49 -setting $K$ to a too low value can overconstrain Nitpick, preventing it from
    1.50 -finding any counterexamples.
    1.51 +problem and performing the after-the-fact check is to specify a low
    1.52 +nonnegative \textit{bisim\_depth} value. In general, a value of $K$ means that
    1.53 +Nitpick will require all lists to be distinguished from each other by their
    1.54 +prefixes of length $K$. However, setting $K$ to a too low value can
    1.55 +overconstrain Nitpick, preventing it from finding any counterexamples.
    1.56  
    1.57  \subsection{Boxing}
    1.58  \label{boxing}
     2.1 --- a/src/HOL/BNF/Examples/Stream.thy	Mon Sep 23 23:27:46 2013 +0200
     2.2 +++ b/src/HOL/BNF/Examples/Stream.thy	Tue Sep 24 00:01:10 2013 +0200
     2.3 @@ -15,11 +15,6 @@
     2.4  codatatype (sset: 'a) stream (map: smap rel: stream_all2) =
     2.5    Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65)
     2.6  
     2.7 -declaration {*
     2.8 -  Nitpick_HOL.register_codatatype
     2.9 -    @{typ "'a stream"} @{const_name stream_case} [dest_Const @{term Stream}]
    2.10 -*}
    2.11 -
    2.12  code_datatype Stream
    2.13  
    2.14  lemma stream_case_cert:
     3.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Sep 23 23:27:46 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Tue Sep 24 00:01:10 2013 +0200
     3.3 @@ -132,8 +132,9 @@
     3.4  val safe_elim_attrs = @{attributes [elim!]};
     3.5  val iff_attrs = @{attributes [iff]};
     3.6  val induct_simp_attrs = @{attributes [induct_simp]};
     3.7 +val nitpick_attrs = @{attributes [nitpick_simp]};
     3.8  val simp_attrs = @{attributes [simp]};
     3.9 -val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
    3.10 +val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs @ simp_attrs;
    3.11  
    3.12  fun unflat_lookup eq xs ys = map (fn xs' => permute_like eq xs xs' ys);
    3.13  
    3.14 @@ -759,7 +760,7 @@
    3.15          val cases_type_attr = Attrib.internal (K (Induct.cases_type dataT_name));
    3.16  
    3.17          val notes =
    3.18 -          [(caseN, case_thms, code_simp_attrs),
    3.19 +          [(caseN, case_thms, code_nitpick_simp_attrs),
    3.20             (case_congN, [case_cong_thm], []),
    3.21             (case_convN, case_conv_thms, []),
    3.22             (collapseN, safe_collapse_thms, simp_attrs),
    3.23 @@ -772,7 +773,7 @@
    3.24             (expandN, expand_thms, []),
    3.25             (injectN, inject_thms, iff_attrs @ induct_simp_attrs),
    3.26             (nchotomyN, [nchotomy_thm], []),
    3.27 -           (selN, all_sel_thms, code_simp_attrs),
    3.28 +           (selN, all_sel_thms, code_nitpick_simp_attrs),
    3.29             (splitN, [split_thm], []),
    3.30             (split_asmN, [split_asm_thm], []),
    3.31             (splitsN, [split_thm, split_asm_thm], []),
     4.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Sep 23 23:27:46 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Sep 24 00:01:10 2013 +0200
     4.3 @@ -47,8 +47,7 @@
     4.4  
     4.5    type lfp_sugar_thms =
     4.6      (thm list * thm * Args.src list)
     4.7 -    * (thm list list * Args.src list)
     4.8 -    * (thm list list * Args.src list)
     4.9 +    * (thm list list * thm list list * Args.src list)
    4.10  
    4.11    type gfp_sugar_thms =
    4.12      ((thm list * thm) list * Args.src list)
    4.13 @@ -201,8 +200,9 @@
    4.14  val id_def = @{thm id_def};
    4.15  val mp_conj = @{thm mp_conj};
    4.16  
    4.17 +val nitpick_attrs = @{attributes [nitpick_simp]};
    4.18 +val code_nitpick_simp_attrs = Code.add_default_eqn_attrib :: nitpick_attrs;
    4.19  val simp_attrs = @{attributes [simp]};
    4.20 -val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
    4.21  
    4.22  fun tvar_subst thy Ts Us =
    4.23    Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) [];
    4.24 @@ -402,8 +402,7 @@
    4.25  
    4.26  type lfp_sugar_thms =
    4.27    (thm list * thm * Args.src list)
    4.28 -  * (thm list list * Args.src list)
    4.29 -  * (thm list list * Args.src list);
    4.30 +  * (thm list list * thm list list * Args.src list)
    4.31  
    4.32  type gfp_sugar_thms =
    4.33    ((thm list * thm) list * Args.src list)
    4.34 @@ -774,7 +773,7 @@
    4.35      val rec_thmss = mk_iter_thmss rec_args_types recs rec_defs (map co_rec_of ctor_iter_thmss);
    4.36    in
    4.37      ((induct_thms, induct_thm, [induct_case_names_attr]),
    4.38 -     (fold_thmss, code_simp_attrs), (rec_thmss, code_simp_attrs))
    4.39 +     (fold_thmss, rec_thmss, code_nitpick_simp_attrs @ simp_attrs))
    4.40    end;
    4.41  
    4.42  fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
    4.43 @@ -1045,7 +1044,7 @@
    4.44        coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
    4.45    in
    4.46      ((coinduct_thms_pairs, coinduct_case_attrs),
    4.47 -     (unfold_thmss, corec_thmss, []),
    4.48 +     (unfold_thmss, corec_thmss, code_nitpick_simp_attrs),
    4.49       (safe_unfold_thmss, safe_corec_thmss),
    4.50       (disc_unfold_thmss, disc_corec_thmss, []),
    4.51       (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
    4.52 @@ -1403,10 +1402,10 @@
    4.53                  join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
    4.54  
    4.55                val notes =
    4.56 -                [(mapN, map_thms, code_simp_attrs),
    4.57 -                 (rel_distinctN, rel_distinct_thms, code_simp_attrs),
    4.58 -                 (rel_injectN, rel_inject_thms, code_simp_attrs),
    4.59 -                 (setN, flat set_thmss, code_simp_attrs)]
    4.60 +                [(mapN, map_thms, code_nitpick_simp_attrs @ simp_attrs),
    4.61 +                 (rel_distinctN, rel_distinct_thms, code_nitpick_simp_attrs @ simp_attrs),
    4.62 +                 (rel_injectN, rel_inject_thms, code_nitpick_simp_attrs @ simp_attrs),
    4.63 +                 (setN, flat set_thmss, code_nitpick_simp_attrs @ simp_attrs)]
    4.64                  |> massage_simple_notes fp_b_name;
    4.65              in
    4.66                (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_sugar),
    4.67 @@ -1441,8 +1440,7 @@
    4.68          ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
    4.69            (iterss, iter_defss)), lthy) =
    4.70        let
    4.71 -        val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs),
    4.72 -             (rec_thmss, rec_attrs)) =
    4.73 +        val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, iter_attrs)) =
    4.74            derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
    4.75              xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss iterss
    4.76              iter_defss lthy;
    4.77 @@ -1457,9 +1455,9 @@
    4.78            |> massage_simple_notes fp_common_name;
    4.79  
    4.80          val notes =
    4.81 -          [(foldN, fold_thmss, K fold_attrs),
    4.82 +          [(foldN, fold_thmss, K iter_attrs),
    4.83             (inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
    4.84 -           (recN, rec_thmss, K rec_attrs),
    4.85 +           (recN, rec_thmss, K iter_attrs),
    4.86             (simpsN, simp_thmss, K [])]
    4.87            |> massage_multi_notes;
    4.88        in
     5.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Sep 23 23:27:46 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Sep 24 00:01:10 2013 +0200
     5.3 @@ -157,7 +157,7 @@
     5.4            derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
     5.5              xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
     5.6              co_iterss co_iter_defss lthy
     5.7 -          |> `(fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
     5.8 +          |> `(fn ((_, induct, _), (fold_thmss, rec_thmss, _)) =>
     5.9              ([induct], fold_thmss, rec_thmss, [], [], [], []))
    5.10            ||> (fn info => (SOME info, NONE))
    5.11          else
     6.1 --- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Mon Sep 23 23:27:46 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML	Tue Sep 24 00:01:10 2013 +0200
     6.3 @@ -131,7 +131,7 @@
     6.4      val all_notes =
     6.5        (case lfp_sugar_thms of
     6.6          NONE => []
     6.7 -      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, _), (rec_thmss, _)) =>
     6.8 +      | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) =>
     6.9          let
    6.10            val common_notes =
    6.11              (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
     7.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Sep 23 23:27:46 2013 +0200
     7.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Tue Sep 24 00:01:10 2013 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4  (*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     7.5      Author:     Jasmin Blanchette, TU Muenchen
     7.6 -    Copyright   2009-2011
     7.7 +    Copyright   2009-2013
     7.8  
     7.9  Examples from the Nitpick manual.
    7.10  *)
    7.11 @@ -12,7 +12,7 @@
    7.12     suite. *)
    7.13  
    7.14  theory Manual_Nits
    7.15 -imports Main "~~/src/HOL/Library/Quotient_Product" Real
    7.16 +imports Main Real "~~/src/HOL/Library/Quotient_Product" "~~/src/HOL/BNF/BNF"
    7.17  begin
    7.18  
    7.19  chapter {* 2. First Steps *}
    7.20 @@ -193,35 +193,10 @@
    7.21  
    7.22  subsection {* 2.9. Coinductive Datatypes *}
    7.23  
    7.24 -(* Lazy lists are defined in Andreas Lochbihler's "Coinductive" AFP entry. Since
    7.25 -   we cannot rely on its presence, we expediently provide our own
    7.26 -   axiomatization. The examples also work unchanged with Lochbihler's
    7.27 -   "Coinductive_List" theory. *)
    7.28 -
    7.29 -(* BEGIN LAZY LIST SETUP *)
    7.30 -definition "llist = (UNIV\<Colon>('a list + (nat \<Rightarrow> 'a)) set)"
    7.31 -
    7.32 -typedef 'a llist = "llist\<Colon>('a list + (nat \<Rightarrow> 'a)) set"
    7.33 -unfolding llist_def by auto
    7.34 +codatatype 'a llist = LNil | LCons 'a "'a llist"
    7.35  
    7.36 -definition LNil where
    7.37 -"LNil = Abs_llist (Inl [])"
    7.38 -definition LCons where
    7.39 -"LCons y ys = Abs_llist (case Rep_llist ys of
    7.40 -                           Inl ys' \<Rightarrow> Inl (y # ys')
    7.41 -                         | Inr f \<Rightarrow> Inr (\<lambda>n. case n of 0 \<Rightarrow> y | Suc m \<Rightarrow> f m))"
    7.42 -
    7.43 -axiomatization iterates :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist"
    7.44 -
    7.45 -lemma iterates_def [nitpick_simp]:
    7.46 -"iterates f a = LCons a (iterates f (f a))"
    7.47 -sorry
    7.48 -
    7.49 -declaration {*
    7.50 -Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
    7.51 -    (map dest_Const [@{term LNil}, @{term LCons}])
    7.52 -*}
    7.53 -(* END LAZY LIST SETUP *)
    7.54 +primcorecursive iterates where
    7.55 +"iterates f a = LCons a (iterates f (f a))" .
    7.56  
    7.57  lemma "xs \<noteq> LCons a xs"
    7.58  nitpick [expect = genuine]
     8.1 --- a/src/HOL/ROOT	Mon Sep 23 23:27:46 2013 +0200
     8.2 +++ b/src/HOL/ROOT	Tue Sep 24 00:01:10 2013 +0200
     8.3 @@ -239,7 +239,7 @@
     8.4      Trans_Closure
     8.5      Sets
     8.6  
     8.7 -session "HOL-Nitpick_Examples" in Nitpick_Examples = HOL +
     8.8 +session "HOL-BNF-Nitpick_Examples" in Nitpick_Examples = "HOL-BNF" +
     8.9    description {*
    8.10      Author:     Jasmin Blanchette, TU Muenchen
    8.11      Copyright   2009