--- a/src/Doc/Datatypes/Datatypes.thy Tue Jan 06 22:48:34 2015 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jan 06 22:51:00 2015 +0100
@@ -110,7 +110,7 @@
Functions,'' describes how to specify corecursive functions using the
@{command primcorec} and @{command primcorecursive} commands.
-\item Section \ref{sec:introducing-bounded-natural-functors}, ``Introducing
+\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
Bounded Natural Functors,'' explains how to use the @{command bnf} command
to register arbitrary type constructors as BNFs.
@@ -325,7 +325,7 @@
Type constructors must be registered as BNFs to have live arguments. This is
done automatically for datatypes and codatatypes introduced by the
@{command datatype} and @{command codatatype} commands.
-Section~\ref{sec:introducing-bounded-natural-functors} explains how to
+Section~\ref{sec:registering-bounded-natural-functors} explains how to
register arbitrary type constructors as BNFs.
Here is another example that fails:
@@ -1137,7 +1137,7 @@
datatypes as new-style datatypes. If the goal is to define new-style datatypes
with nested recursion through old-style datatypes, the old-style
datatypes can be registered as a BNF
-(Section~\ref{sec:introducing-bounded-natural-functors}). If the goal is
+(Section~\ref{sec:registering-bounded-natural-functors}). If the goal is
to derive discriminators and selectors, this can be achieved using
@{command free_constructors}
(Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
@@ -2627,8 +2627,8 @@
*)
-section {* Introducing Bounded Natural Functors
- \label{sec:introducing-bounded-natural-functors} *}
+section {* Registering Bounded Natural Functors
+ \label{sec:registering-bounded-natural-functors} *}
text {*
The (co)datatype package can be set up to allow nested recursion through
@@ -2969,9 +2969,9 @@
packages and tools, such as the code generator, Transfer, Lifting, and
Quickcheck. They can be enabled or disabled individually using the
@{syntax plugins} option to the commands @{command datatype},
-@{command codatatype}, @{command free_constructors}, @{command bnf}, and
-@{command bnf_axiomatization}.
-For example:
+@{command primrec}, @{command codatatype}, @{command primcorec},
+@{command primcorecursive}, @{command bnf}, @{command bnf_axiomatization}, and
+@{command free_constructors}. For example:
*}
datatype (plugins del: code "quickcheck") color = Red | Black
@@ -2981,13 +2981,13 @@
\label{ssec:code-generator} *}
text {*
-The \hthm{code} plugin registers (co)datatypes and other freely generated types
-for code generation. No distinction is made between datatypes and codatatypes.
-This means that for target languages with a strict evaluation strategy (e.g.,
-Standard ML), programs that attempt to produce infinite codatatype values will
-not terminate.
-
-The plugin derives the following properties:
+The \hthm{code} plugin registers freely generated types, including
+(co)datatypes, and (co)recursive functions for code generation. No distinction
+is made between datatypes and codatatypes. This means that for target languages
+with a strict evaluation strategy (e.g., Standard ML), programs that attempt to
+produce infinite codatatype values will not terminate.
+
+For types, the plugin derives the following properties:
\begin{indentblock}
\begin{description}
@@ -3007,9 +3007,10 @@
\end{indentblock}
In addition, the plugin sets the @{text "[code]"} attribute on a number of
-properties of (co)datatypes and other freely generated types, as documented in
-Sections \ref{ssec:datatype-generated-theorems} and
-\ref{ssec:codatatype-generated-theorems}.
+properties of freely generated types and of (co)recursive functions, as
+documented in Sections \ref{ssec:datatype-generated-theorems},
+\ref{ssec:primrec-generated-theorems}, \ref{ssec:codatatype-generated-theorems},
+and~\ref{ssec:primcorec-generated-theorems}.
*}
--- a/src/Doc/Datatypes/document/root.tex Tue Jan 06 22:48:34 2015 +0100
+++ b/src/Doc/Datatypes/document/root.tex Tue Jan 06 22:51:00 2015 +0100
@@ -58,7 +58,7 @@
\isadroptag{theory}
\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
-Defining (Co)datatypes in Isabelle/HOL}
+Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL}
\author{Jasmin Christian Blanchette,
Martin Desharnais, \\
Lorenz Panny,
@@ -71,12 +71,17 @@
\maketitle
+\begin{sloppy}
\begin{abstract}
\noindent
-This tutorial describes the definitional package for datatypes and codatatypes
-in Isabelle/HOL. The package provides four main commands: \keyw{datatype},
-\keyw{codatatype}, \keyw{primrec}, and \keyw{primcorec}.
+This tutorial describes the definitional package for datatypes and codatatypes,
+and for primitively recursive and corecursive functions, in Isabelle/HOL. The
+package provides these commands:
+\keyw{datatype}, \keyw{datatype_compat}, \keyw{primrec}, \keyw{codatatype},
+\keyw{primcorec}, \keyw{prim\-co\-recursive}, \keyw{bnf}, \keyw{bnf_axiomatization},
+\keyw{print_bnfs}, and \keyw{free_\allowbreak constructors}.
\end{abstract}
+\end{sloppy}
\tableofcontents
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Jan 06 22:48:34 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Jan 06 22:51:00 2015 +0100
@@ -18,6 +18,7 @@
open Ctr_Sugar_Util
open Ctr_Sugar_Tactics
+open BNF_Util
open BNF_Def
open BNF_FP_Util
open BNF_FP_Def_Sugar
@@ -27,29 +28,27 @@
val transferN = "transfer";
fun mk_lfp_rec_sugar_transfer_tac ctxt def =
- Ctr_Sugar_Tactics.unfold_thms_tac ctxt [def] THEN
- HEADGOAL (Transfer.transfer_prover_tac ctxt);
+ unfold_thms_tac ctxt [def] THEN HEADGOAL (Transfer.transfer_prover_tac ctxt);
-fun mk_gfp_rec_sugar_transfer_tac apply_transfer ctxt f_def corec_def type_definitions
- dtor_corec_transfers rel_pre_defs disc_eq_cases cases case_distribs case_congs =
+fun mk_gfp_rec_sugar_transfer_tac ctxt f_def corec_def type_definitions dtor_corec_transfers
+ rel_pre_defs disc_eq_cases cases case_distribs case_congs =
let
fun instantiate_with_lambda thm =
let
- val prop = Thm.prop_of thm;
- val @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, fT) $ _) $ _) = prop;
+ val prop as @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, fT) $ _) $ _) =
+ Thm.prop_of thm;
val T = range_type fT;
val j = Term.maxidx_of_term prop + 1;
val cond = Var (("x", j), HOLogic.boolT);
val then_branch = Var (("t", j), T);
val else_branch = Var (("e", j), T);
- val lambda = Term.lambda cond (mk_If cond then_branch else_branch);
+ val lam = Term.lambda cond (mk_If cond then_branch else_branch);
in
- cterm_instantiate_pos [SOME (certify ctxt lambda)] thm
+ cterm_instantiate_pos [SOME (certify ctxt lam)] thm
end;
val transfer_rules =
- @{thm Abs_transfer[OF BNF_Composition.type_definition_id_bnf_UNIV
- BNF_Composition.type_definition_id_bnf_UNIV]} ::
+ @{thm Abs_transfer[OF type_definition_id_bnf_UNIV type_definition_id_bnf_UNIV]} ::
map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions @
map (Local_Defs.unfold ctxt rel_pre_defs) dtor_corec_transfers;
val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add;
@@ -57,74 +56,63 @@
val case_distribs = map instantiate_with_lambda case_distribs;
val simps = case_distribs @ disc_eq_cases @ cases @ @{thms if_True if_False};
- val simp_ctxt = put_simpset (simpset_of (ss_only simps ctxt)) ctxt';
+ val ctxt'' = put_simpset (simpset_of (ss_only simps ctxt)) ctxt';
in
unfold_thms_tac ctxt ([f_def, corec_def] @ @{thms split_beta if_conn}) THEN
- HEADGOAL (simp_tac (fold Simplifier.add_cong case_congs simp_ctxt)) THEN
- (if apply_transfer then HEADGOAL (Transfer.transfer_prover_tac ctxt') else all_tac)
+ HEADGOAL (simp_tac (fold Simplifier.add_cong case_congs ctxt'')) THEN
+ HEADGOAL (Transfer.transfer_prover_tac ctxt')
end;
fun massage_simple_notes base =
filter_out (null o #2)
#> map (fn (thmN, thms, f_attrs) =>
((Binding.qualify true base (Binding.name thmN), []),
- map_index (fn (i, thm) => ([thm], f_attrs i)) thms));
+ map_index (fn (kk, thm) => ([thm], f_attrs kk)) thms));
fun fp_sugar_of_bnf ctxt = fp_sugar_of ctxt o (fn Type (s, _) => s) o T_of_bnf;
-fun bnf_depth_first_traverse ctxt f T z =
+fun bnf_depth_first_traverse ctxt f T =
(case T of
- Type (s, innerTs) =>
+ Type (s, Ts) =>
(case bnf_of ctxt s of
- NONE => z
- | SOME bnf => let val z' = f bnf z in
- fold (bnf_depth_first_traverse ctxt f) innerTs z'
- end)
- | _ => z)
-
-fun if_all_bnfs ctxt Ts f g =
- let val bnfs = map_filter (fn Type (s, _) => BNF_Def.bnf_of ctxt s | _ => NONE) Ts in
- if length bnfs = length Ts then f bnfs else g
- end;
+ NONE => I
+ | SOME bnf => fold (bnf_depth_first_traverse ctxt f) Ts o f bnf)
+ | _ => I);
fun mk_goal lthy f =
let
val skematic_Ts = Term.add_tvarsT (fastype_of f) [];
val ((As, Bs), names_lthy) = lthy
- |> Ctr_Sugar_Util.mk_TFrees' (map snd skematic_Ts)
- ||>> Ctr_Sugar_Util.mk_TFrees' (map snd skematic_Ts);
+ |> mk_TFrees' (map snd skematic_Ts)
+ ||>> mk_TFrees' (map snd skematic_Ts);
- val (Rs, names_lthy) =
- Ctr_Sugar_Util.mk_Frees "R" (map2 BNF_Util.mk_pred2T As Bs) names_lthy;
+ val (Rs, names_lthy) = mk_Frees "R" (map2 mk_pred2T As Bs) names_lthy;
val fA = Term.subst_TVars (map fst skematic_Ts ~~ As) f;
val fB = Term.subst_TVars (map fst skematic_Ts ~~ Bs) f;
in
- (BNF_FP_Def_Sugar.mk_parametricity_goal lthy Rs fA fB, names_lthy)
+ (mk_parametricity_goal lthy Rs fA fB, names_lthy)
end;
-fun prove_parametricity_if_bnf prove {transfers, fun_names, funs, fun_defs, fpTs} lthy =
- fold_index (fn (n, (((transfer, f_names), f), def)) => fn lthy =>
- if not transfer then
- lthy
+fun fp_rec_sugar_transfer_interpretation prove {transfers, fun_names, funs, fun_defs, fpTs} =
+ fold_index (fn (kk, (((transfer, fun_name), funx), fun_def)) => fn lthy =>
+ if transfer then
+ (case try (map the) (map (fn Type (s, _) => bnf_of lthy s | _ => NONE) fpTs) of
+ NONE => error "No transfer rule possible"
+ | SOME bnfs =>
+ (case try (prove kk bnfs funx fun_def) lthy of
+ NONE => error "Failed to prove transfer rule"
+ | SOME thm =>
+ let
+ val notes = [(transferN, [thm], K @{attributes [transfer_rule]})]
+ |> massage_simple_notes fun_name;
+ in
+ snd (Local_Theory.notes notes lthy)
+ end))
else
- if_all_bnfs lthy fpTs
- (fn bnfs => fn () => prove n bnfs f_names f def lthy)
- (fn () => error "Function is not parametric" (*FIXME: wording*)) ())
- (transfers ~~ fun_names ~~ funs ~~ fun_defs) lthy;
-
-fun fp_rec_sugar_transfer_interpretation prove =
- prove_parametricity_if_bnf (fn n => fn bnfs => fn f_name => fn f => fn def => fn lthy =>
- (case try (prove n bnfs f def) lthy of
- NONE => error "Failed to prove parametricity"
- | SOME thm =>
- let
- val notes = [(transferN, [thm], K @{attributes [transfer_rule]})]
- |> massage_simple_notes f_name;
- in
- snd (Local_Theory.notes notes lthy)
- end));
+ lthy)
+ (transfers ~~ fun_names ~~ funs ~~ fun_defs);
val lfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
(fn _ => fn _ => fn f => fn def => fn lthy =>
@@ -136,28 +124,26 @@
end);
val gfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation
- (fn n => fn bnfs => fn f => fn def => fn lthy =>
+ (fn kk => fn bnfs => fn f => fn def => fn lthy =>
let
val fp_sugars = map (the o fp_sugar_of_bnf lthy) bnfs;
val (goal, names_lthy) = mk_goal lthy f;
val (disc_eq_cases, case_thms, case_distribs, case_congs) =
- bnf_depth_first_traverse lthy (fn bnf => fn quad =>
- let
- fun add_thms (disc_eq_cases0, case_thms0, case_distribs0, case_congs0)
- {fp_ctr_sugar = {ctr_sugar = {disc_eq_cases, case_thms, case_distribs, case_cong,
- ...}, ...}, ...} =
- (union Thm.eq_thm disc_eq_cases disc_eq_cases0,
- union Thm.eq_thm case_thms case_thms0,
- union Thm.eq_thm case_distribs case_distribs0,
- insert Thm.eq_thm case_cong case_congs0);
- in
- Option.map (add_thms quad) (fp_sugar_of_bnf lthy bnf)
- |> the_default quad
- end) (fastype_of f) ([], [], [], []);
+ bnf_depth_first_traverse lthy (fn bnf =>
+ (case fp_sugar_of_bnf lthy bnf of
+ NONE => I
+ | SOME {fp_ctr_sugar = {ctr_sugar = {disc_eq_cases, case_thms, case_distribs,
+ case_cong, ...}, ...}, ...} =>
+ (fn (disc_eq_cases0, case_thms0, case_distribs0, case_congs0) =>
+ (union Thm.eq_thm disc_eq_cases disc_eq_cases0,
+ union Thm.eq_thm case_thms case_thms0,
+ union Thm.eq_thm case_distribs case_distribs0,
+ insert Thm.eq_thm case_cong case_congs0))))
+ (fastype_of f) ([], [], [], []);
in
Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_gfp_rec_sugar_transfer_tac true ctxt def
- (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars n)))
+ mk_gfp_rec_sugar_transfer_tac ctxt def
+ (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars kk)))
(map (#type_definition o #absT_info) fp_sugars)
(maps (#xtor_co_rec_transfers o #fp_res) fp_sugars)
(map (rel_def_of_bnf o #pre_bnf) fp_sugars)