--- a/NEWS Wed Apr 23 15:57:06 2014 +0200
+++ b/NEWS Wed Apr 23 17:05:48 2014 +0200
@@ -279,6 +279,10 @@
* New (co)datatype package:
* "primcorec" is fully implemented.
+ * "datatype_new" generates size functions ("size_xxx" and "size") as
+ required by "fun".
+ * BNFs are integrated with the Lifting tool and new-style (co)datatypes
+ with Transfer.
* Renamed commands:
datatype_new_compat ~> datatype_compat
primrec_new ~> primrec
@@ -306,12 +310,13 @@
Option.set ~> set_option
Option.map ~> map_option
option_rel ~> rel_option
- option_rec ~> case_option
+ list_size ~> size_list
+ option_size ~> size_option
Renamed theorems:
set_def ~> set_rec[abs_def]
map_def ~> map_rec[abs_def]
Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
- option.recs ~> option.case
+ option.recs ~> option.rec
list_all2_def ~> list_all2_iff
set.simps ~> set_simps (or the slightly different "list.set")
map.simps ~> list.map
--- a/src/Doc/Datatypes/Datatypes.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Apr 23 17:05:48 2014 +0200
@@ -103,7 +103,7 @@
\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
Functions,'' describes how to specify recursive functions using
-@{command primrec}, \keyw{fun}, and \keyw{function}.
+@{command primrec}.
\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
describes how to specify codatatypes using the @{command codatatype} command.
@@ -570,8 +570,8 @@
*}
-subsubsection {* \keyw{datatype\_new\_compat}
- \label{sssec:datatype-new-compat} *}
+subsubsection {* \keyw{datatype\_compat}
+ \label{sssec:datatype-compat} *}
text {*
\begin{matharray}{rcl}
@@ -593,27 +593,14 @@
text {* \blankline *}
- thm even_nat_odd_nat.size
-
-text {* \blankline *}
-
ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}
text {*
The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.
The command is interesting because the old datatype package provides some
-functionality that is not yet replicated in the new package:
-
-\begin{itemize}
-\setlength{\itemsep}{0pt}
-
-\item It is integrated with \keyw{fun} \cite{isabelle-function},
-Nitpick \cite{isabelle-nitpick}, Quickcheck, and other packages.
-
-\item It is extended by various add-ons, notably to produce instances of the
-@{const size} function.
-\end{itemize}
+functionality that is not yet replicated in the new package, such as the
+integration with Quickcheck.
A few remarks concern nested recursive datatypes:
@@ -630,8 +617,8 @@
no way to register old-style datatypes as new-style datatypes).
\item The recursor produced for types that recurse through functions has a
-different signature than with the old package. This makes it impossible to use
-the old \keyw{primrec} command.
+different signature than with the old package. This might affect the behavior of
+some third-party extensions.
\end{itemize}
An alternative to @{command datatype_compat} is to use the old package's
@@ -661,13 +648,15 @@
& \quad\vdots \\
& @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
Set functions: &
- @{text set1_t}, \ldots, @{text t.setm_t} \\
+ @{text t.set1_t}, \ldots, @{text t.setm_t} \\
Map function: &
@{text t.map_t} \\
Relator: &
@{text t.rel_t} \\
Recursor: &
- @{text t.rec_t}
+ @{text t.rec_t} \\
+Size function: &
+ @{text t.size_t}
\end{tabular}
\medskip
@@ -676,6 +665,9 @@
The case combinator, discriminators, and selectors are collectively called
\emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
names and is normally hidden.
+
+In addition to the above, the @{class size} class is instantiated to overload the
+@{const size} function based on @{text t.size_t}.
*}
@@ -689,15 +681,16 @@
\begin{itemize}
\setlength{\itemsep}{0pt}
-\item The \emph{free constructor theorems} are properties about the constructors
-and destructors that can be derived for any freely generated type. Internally,
-the derivation is performed by @{command free_constructors}.
-
-\item The \emph{functorial theorems} are properties of datatypes related to
-their BNF nature.
-
-\item The \emph{inductive theorems} are properties of datatypes related to
-their inductive nature.
+\item The \emph{free constructor theorems}
+(Section~\ref{sssec:free-constructor-theorems}) are properties of the
+constructors and destructors that can be derived for any freely generated type.
+Internally, the derivation is performed by @{command free_constructors}.
+
+\item The \emph{functorial theorems} (Section~\ref{sssec:functorial-theorems})
+are properties of datatypes related to their BNF nature.
+
+\item The \emph{inductive theorems} (Section~\ref{sssec:inductive-theorems})
+are properties of datatypes related to their inductive nature.
\end{itemize}
@@ -937,6 +930,18 @@
@{thm list.rec(1)[no_vars]} \\
@{thm list.rec(2)[no_vars]}
+\item[@{text "t."}\hthm{rec\_o\_map}\rm:] ~ \\
+@{thm list.rec_o_map[no_vars]}
+
+\item[@{text "t."}\hthm{size} @{text "[simp, code]"}\rm:] ~ \\
+@{thm list.size(1)[no_vars]} \\
+@{thm list.size(2)[no_vars]} \\
+@{thm list.size(3)[no_vars]} \\
+@{thm list.size(4)[no_vars]}
+
+\item[@{text "t."}\hthm{size\_o\_map}\rm:] ~ \\
+@{thm list.size_o_map[no_vars]}
+
\end{description}
\end{indentblock}
@@ -967,12 +972,12 @@
\item \emph{The Standard ML interfaces are different.} Tools and extensions
written to call the old ML interfaces will need to be adapted to the new
-interfaces. Little has been done so far in this direction. Whenever possible, it
-is recommended to use @{command datatype_compat} or \keyw{rep\_datatype}
-to register new-style datatypes as old-style datatypes.
-
-\item \emph{The constants @{text t_case} and @{text t_rec} are now called
-@{text case_t} and @{text rec_t}.}
+interfaces. This concerns Quickcheck in particular. Whenever possible, it is
+recommended to use @{command datatype_compat} to register new-style datatypes
+as old-style datatypes.
+
+\item \emph{The constants @{text t_case}, @{text t_rec}, and @{text t_size} are
+now called @{text case_t}, @{text rec_t}, and @{text size_t}.}
\item \emph{The recursor @{text rec_t} has a different signature for nested
recursive datatypes.} In the old package, nested recursion through non-functions
@@ -980,26 +985,27 @@
type of the recursor, used by \keyw{primrec}. Recursion through functions was
handled specially. In the new package, nested recursion (for functions and
non-functions) is handled in a more modular fashion. The old-style recursor can
-be generated on demand using @{command primrec}, as explained in
-Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
-new-style datatypes.
+be generated on demand using @{command primrec} if the recursion is via
+new-style datatypes, as explained in
+Section~\ref{sssec:primrec-nested-as-mutual-recursion}.
\item \emph{Accordingly, the induction rule is different for nested recursive
datatypes.} Again, the old-style induction rule can be generated on demand using
-@{command primrec}, as explained in
-Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
-new-style datatypes.
+@{command primrec} if the recursion is via new-style datatypes, as explained in
+Section~\ref{sssec:primrec-nested-as-mutual-recursion}.
\item \emph{The internal constructions are completely different.} Proof texts
that unfold the definition of constants introduced by \keyw{datatype} will be
difficult to port.
-\item \emph{Some induction rules have different names.}
+\item \emph{Some theorems have different names.}
For non-mutually recursive datatypes,
the alias @{text t.inducts} for @{text t.induct} is no longer generated.
For $m > 1$ mutually recursive datatypes,
@{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
-@{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, t}"}.
+@{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, t}"}, and similarly the
+collection @{text "t\<^sub>1_\<dots>_t\<^sub>m.size"} has been divided into @{text "t\<^sub>1.size"},
+\ldots, @{text "t\<^sub>m.size"}.
\item \emph{The @{text t.simps} collection has been extended.}
Previously available theorems are available at the same index.
@@ -1129,7 +1135,7 @@
restrictions imposed on primitively recursive functions. The
@{command datatype_compat} command is needed to register new-style datatypes
for use with \keyw{fun} and \keyw{function}
-(Section~\ref{sssec:datatype-new-compat}):
+(Section~\ref{sssec:datatype-compat}):
*}
datatype_compat nat
@@ -1636,13 +1642,13 @@
with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
\ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
-recursor is replaced by a dual concept:
+recursor is replaced by a dual concept and no size function is produced:
\medskip
\begin{tabular}{@ {}ll@ {}}
Corecursor: &
- @{text corec_t}
+ @{text t.corec_t}
\end{tabular}
*}
@@ -1657,20 +1663,20 @@
\begin{itemize}
\setlength{\itemsep}{0pt}
-\item The \emph{free constructor theorems} are properties about the constructors
-and destructors that can be derived for any freely generated type.
-
-\item The \emph{functorial theorems} are properties of datatypes related to
+\item The \emph{free constructor theorems}
+(Section~\ref{sssec:free-constructor-theorems}) are properties of the
+constructors and destructors that can be derived for any freely generated type.
+
+\item The \emph{functorial theorems}
+(Section~\ref{sssec:functorial-theorems}) are properties of datatypes related to
their BNF nature.
-\item The \emph{coinductive theorems} are properties of datatypes related to
-their coinductive nature.
+\item The \emph{coinductive theorems} (Section~\ref{sssec:coinductive-theorems})
+are properties of datatypes related to their coinductive nature.
\end{itemize}
\noindent
-The first two categories are exactly as for datatypes and are described in
-Sections
-\ref{sssec:free-constructor-theorems}~and~\ref{sssec:functorial-theorems}.
+The first two categories are exactly as for datatypes.
*}
@@ -2696,12 +2702,8 @@
*}
text {*
-%* primcorecursive and primcorec is unfinished
-%
%* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
%
-%* issues with HOL-Proofs?
-%
%* partial documentation
%
%* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
@@ -2723,7 +2725,7 @@
Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
(co)datatype package. Andreas Lochbihler provided lots of comments on earlier
-versions of the package, especially for the coinductive part. Brian Huffman
+versions of the package, especially on the coinductive part. Brian Huffman
suggested major simplifications to the internal constructions, many of which
have yet to be implemented. Florian Haftmann and Christian Urban provided
general advice on Isabelle and package writing. Stefan Milius and Lutz
--- a/src/HOL/BNF_Def.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/BNF_Def.thy Wed Apr 23 17:05:48 2014 +0200
@@ -14,19 +14,19 @@
"bnf" :: thy_goal
begin
-lemma collect_comp: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
+lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
by (rule ext) (auto simp only: comp_apply collect_def)
definition convol ("<_ , _>") where
"<f , g> \<equiv> %a. (f a, g a)"
lemma fst_convol:
-"fst o <f , g> = f"
+"fst \<circ> <f , g> = f"
apply(rule ext)
unfolding convol_def by simp
lemma snd_convol:
-"snd o <f , g> = g"
+"snd \<circ> <f , g> = g"
apply(rule ext)
unfolding convol_def by simp
@@ -97,10 +97,10 @@
"csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
-lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
+lemma snd_fst_flip: "snd xy = (fst \<circ> (%(x, y). (y, x))) xy"
by (simp split: prod.split)
-lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy"
+lemma fst_snd_flip: "fst xy = (snd \<circ> (%(x, y). (y, x))) xy"
by (simp split: prod.split)
lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
@@ -134,16 +134,19 @@
lemma If_the_inv_into_f_f:
"\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow>
- ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
+ ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<circ> g) i = id i"
unfolding Func_def by (auto elim: the_inv_into_f_f)
+lemma the_inv_f_o_f_id: "inj f \<Longrightarrow> (the_inv f \<circ> f) z = id z"
+ by (simp add: the_inv_f_f)
+
lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
unfolding vimage2p_def by -
lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
unfolding rel_fun_def vimage2p_def by auto
-lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
+lemma convol_image_vimage2p: "<f \<circ> fst, g \<circ> snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
unfolding vimage2p_def convol_def by auto
lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
--- a/src/HOL/BNF_FP_Base.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy Wed Apr 23 17:05:48 2014 +0200
@@ -89,34 +89,34 @@
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
by blast
-lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
+lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r"
unfolding comp_def fun_eq_iff by auto
-lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2"
+lemma rewriteR_comp_comp2: "\<lbrakk>g \<circ> h = r1 \<circ> r2; f \<circ> r1 = l\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = l \<circ> r2"
unfolding comp_def fun_eq_iff by auto
-lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
+lemma rewriteL_comp_comp: "\<lbrakk>f \<circ> g = l\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l \<circ> h"
unfolding comp_def fun_eq_iff by auto
-lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r"
+lemma rewriteL_comp_comp2: "\<lbrakk>f \<circ> g = l1 \<circ> l2; l2 \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l1 \<circ> r"
unfolding comp_def fun_eq_iff by auto
-lemma convol_o: "<f, g> o h = <f o h, g o h>"
+lemma convol_o: "<f, g> \<circ> h = <f \<circ> h, g \<circ> h>"
unfolding convol_def by auto
-lemma map_prod_o_convol: "map_prod h1 h2 o <f, g> = <h1 o f, h2 o g>"
+lemma map_prod_o_convol: "map_prod h1 h2 \<circ> <f, g> = <h1 \<circ> f, h2 \<circ> g>"
unfolding convol_def by auto
lemma map_prod_o_convol_id: "(map_prod f id \<circ> <id , g>) x = <id \<circ> f , g> x"
unfolding map_prod_o_convol id_comp comp_id ..
-lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)"
+lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)"
unfolding comp_def by (auto split: sum.splits)
-lemma case_sum_o_map_sum: "case_sum f g o map_sum h1 h2 = case_sum (f o h1) (g o h2)"
+lemma case_sum_o_map_sum: "case_sum f g \<circ> map_sum h1 h2 = case_sum (f \<circ> h1) (g \<circ> h2)"
unfolding comp_def by (auto split: sum.splits)
-lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x"
+lemma case_sum_o_map_sum_id: "(case_sum id g \<circ> map_sum f id) x = case_sum (f \<circ> id) g x"
unfolding case_sum_o_map_sum id_comp comp_id ..
lemma rel_fun_def_butlast:
@@ -144,7 +144,7 @@
lemma
assumes "type_definition Rep Abs UNIV"
- shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs o Rep = id"
+ shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs \<circ> Rep = id"
unfolding fun_eq_iff comp_apply id_apply
type_definition.Abs_inverse[OF assms UNIV_I] type_definition.Rep_inverse[OF assms] by simp_all
@@ -152,7 +152,7 @@
assumes "type_definition Rep Abs UNIV"
"type_definition Rep' Abs' UNIV"
"type_definition Rep'' Abs'' UNIV"
- shows "Abs' o M o Rep'' = (Abs' o M1 o Rep) o (Abs o M2 o Rep'') \<Longrightarrow> M1 o M2 = M"
+ shows "Abs' \<circ> M \<circ> Rep'' = (Abs' \<circ> M1 \<circ> Rep) \<circ> (Abs \<circ> M2 \<circ> Rep'') \<Longrightarrow> M1 \<circ> M2 = M"
by (rule sym) (auto simp: fun_eq_iff type_definition.Abs_inject[OF assms(2) UNIV_I UNIV_I]
type_definition.Abs_inverse[OF assms(1) UNIV_I]
type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])
@@ -160,14 +160,60 @@
lemma vimage2p_id: "vimage2p id id R = R"
unfolding vimage2p_def by auto
-lemma vimage2p_comp: "vimage2p (f1 o f2) (g1 o g2) = vimage2p f2 g2 o vimage2p f1 g1"
+lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
unfolding fun_eq_iff vimage2p_def o_apply by simp
+lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
+ by (erule arg_cong)
+
+lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
+ by (rule ext) simp
+
+lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
+ unfolding inj_on_def by simp
+
+lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
+ by (case_tac x) simp
+
+lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
+ by (case_tac x) simp+
+
+lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
+ by (case_tac x) simp+
+
+lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
+ by (simp add: inj_on_def)
+
ML_file "Tools/BNF/bnf_fp_util.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
+ML_file "Tools/BNF/bnf_lfp_size.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
ML_file "Tools/BNF/bnf_fp_n2m.ML"
ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
+ML_file "Tools/Function/size.ML"
+setup Size.setup
+
+lemma size_bool[code]: "size (b\<Colon>bool) = 0"
+ by (cases b) auto
+
+lemma nat_size[simp, code]: "size (n\<Colon>nat) = n"
+ by (induct n) simp_all
+
+declare prod.size[no_atp]
+
+lemma sum_size_o_map: "sum_size g1 g2 \<circ> map_sum f1 f2 = sum_size (g1 \<circ> f1) (g2 \<circ> f2)"
+ by (rule ext) (case_tac x, auto)
+
+lemma prod_size_o_map: "prod_size g1 g2 \<circ> map_prod f1 f2 = prod_size (g1 \<circ> f1) (g2 \<circ> f2)"
+ by (rule ext) auto
+
+setup {*
+BNF_LFP_Size.register_size_global @{type_name sum} @{const_name sum_size} @{thms sum.size}
+ @{thms sum_size_o_map}
+#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name prod_size} @{thms prod.size}
+ @{thms prod_size_o_map}
+*}
+
end
--- a/src/HOL/Fun_Def.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Fun_Def.thy Wed Apr 23 17:05:48 2014 +0200
@@ -111,7 +111,8 @@
#> Function_Fun.setup
*}
-subsection {* Measure Functions *}
+
+subsection {* Measure functions *}
inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
where is_measure_trivial: "is_measure f"
@@ -137,7 +138,7 @@
setup Lexicographic_Order.setup
-subsection {* Congruence Rules *}
+subsection {* Congruence rules *}
lemma let_cong [fundef_cong]:
"M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
@@ -156,22 +157,22 @@
"f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
unfolding o_apply .
+
subsection {* Simp rules for termination proofs *}
-lemma termination_basic_simps[termination_simp]:
- "x < (y::nat) \<Longrightarrow> x < y + z"
- "x < z \<Longrightarrow> x < y + z"
- "x \<le> y \<Longrightarrow> x \<le> y + (z::nat)"
- "x \<le> z \<Longrightarrow> x \<le> y + (z::nat)"
- "x < y \<Longrightarrow> x \<le> (y::nat)"
-by arith+
-
-declare le_imp_less_Suc[termination_simp]
+declare
+ trans_less_add1[termination_simp]
+ trans_less_add2[termination_simp]
+ trans_le_add1[termination_simp]
+ trans_le_add2[termination_simp]
+ less_imp_le_nat[termination_simp]
+ le_imp_less_Suc[termination_simp]
lemma prod_size_simp[termination_simp]:
"prod_size f g p = f (fst p) + g (snd p) + Suc 0"
by (induct p) auto
+
subsection {* Decomposition *}
lemma less_by_empty:
@@ -185,7 +186,7 @@
by (auto simp add: wf_comp_self[of R])
-subsection {* Reduction Pairs *}
+subsection {* Reduction pairs *}
definition
"reduction_pair P = (wf (fst P) \<and> fst P O snd P \<subseteq> fst P)"
--- a/src/HOL/Lazy_Sequence.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Lazy_Sequence.thy Wed Apr 23 17:05:48 2014 +0200
@@ -28,7 +28,7 @@
by (auto intro: lazy_sequence_eqI)
lemma lazy_sequence_size_eq:
- "lazy_sequence_size f xq = Suc (list_size f (list_of_lazy_sequence xq))"
+ "lazy_sequence_size f xq = Suc (size_list f (list_of_lazy_sequence xq))"
by (cases xq) simp
lemma size_lazy_sequence_eq [code]:
--- a/src/HOL/Library/FSet.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Library/FSet.thy Wed Apr 23 17:05:48 2014 +0200
@@ -112,7 +112,7 @@
fix X :: "'a fset set"
{
assume "x \<in> X" "bdd_below X"
- then show "Inf X |\<subseteq>| x" by transfer auto
+ then show "Inf X |\<subseteq>| x" by transfer auto
next
assume "X \<noteq> {}" "(\<And>x. x \<in> X \<Longrightarrow> z |\<subseteq>| x)"
then show "z |\<subseteq>| Inf X" by transfer (clarsimp, blast)
@@ -150,6 +150,8 @@
abbreviation fUNIV :: "'a::finite fset" where "fUNIV \<equiv> top"
abbreviation fuminus :: "'a::finite fset \<Rightarrow> 'a fset" ("|-| _" [81] 80) where "|-| x \<equiv> uminus x"
+declare top_fset.rep_eq[simp]
+
subsection {* Other operations *}
@@ -643,7 +645,7 @@
by (transfer fixing: f) (rule fold_fun_left_comm)
lemma ffold_finsert2:
- "x |\<notin>| A \<Longrightarrow> ffold f z (finsert x A) = ffold f (f x z) A"
+ "x |\<notin>| A \<Longrightarrow> ffold f z (finsert x A) = ffold f (f x z) A"
by (transfer fixing: f) (rule fold_insert2)
lemma ffold_rec:
@@ -672,7 +674,7 @@
begin
lemma ffold_finsert_idem:
- "ffold f z (finsert x A) = f x (ffold f z A)"
+ "ffold f z (finsert x A) = f x (ffold f z A)"
by (transfer fixing: f) (rule fold_insert_idem)
declare ffold_finsert [simp del] ffold_finsert_idem [simp]
@@ -782,7 +784,7 @@
apply (subst bchoice_iff[symmetric])
using R_S[unfolded rel_set_def OO_def] by blast
- obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
+ obtain g where g: "\<forall>z\<in>Z. S (g z) z \<and> (\<exists>x\<in>X. R x (g z))"
apply atomize_elim
apply (subst bchoice_iff[symmetric])
using R_S[unfolded rel_set_def OO_def] by blast
@@ -978,6 +980,36 @@
lemmas [simp] = fset.map_comp fset.map_id fset.set_map
+subsection {* Size setup *}
+
+context includes fset.lifting begin
+lift_definition size_fset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a fset \<Rightarrow> nat" is "\<lambda>f. setsum (Suc \<circ> f)" .
+end
+
+instantiation fset :: (type) size begin
+definition size_fset where
+ size_fset_overloaded_def: "size_fset = FSet.size_fset (\<lambda>_. 0)"
+instance ..
+end
+
+lemmas size_fset_simps[simp] =
+ size_fset_def[THEN meta_eq_to_obj_eq, THEN fun_cong, THEN fun_cong,
+ unfolded map_fun_def comp_def id_apply]
+
+lemmas size_fset_overloaded_simps[simp] =
+ size_fset_simps[of "\<lambda>_. 0", unfolded add_0_left add_0_right,
+ folded size_fset_overloaded_def]
+
+lemma fset_size_o_map: "inj f \<Longrightarrow> size_fset g \<circ> fimage f = size_fset (g \<circ> f)"
+ unfolding size_fset_def fimage_def
+ by (auto simp: Abs_fset_inverse setsum_reindex_cong[OF subset_inj_on[OF _ top_greatest]])
+
+setup {*
+BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset}
+ @{thms size_fset_simps size_fset_overloaded_simps} @{thms fset_size_o_map}
+*}
+
+
subsection {* Advanced relator customization *}
(* Set vs. sum relators: *)
--- a/src/HOL/Library/IArray.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Library/IArray.thy Wed Apr 23 17:05:48 2014 +0200
@@ -59,7 +59,7 @@
by (cases as) simp
lemma [code]:
-"iarray_size f as = Suc (list_size f (IArray.list_of as))"
+"iarray_size f as = Suc (size_list f (IArray.list_of as))"
by (cases as) simp
lemma [code]:
--- a/src/HOL/Library/Multiset.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Library/Multiset.thy Wed Apr 23 17:05:48 2014 +0200
@@ -572,47 +572,65 @@
subsubsection {* Size *}
-instantiation multiset :: (type) size
-begin
-
-definition size_def:
- "size M = setsum (count M) (set_of M)"
-
+definition wcount where "wcount f M = (\<lambda>x. count M x * Suc (f x))"
+
+lemma wcount_union: "wcount f (M + N) a = wcount f M a + wcount f N a"
+ by (auto simp: wcount_def add_mult_distrib)
+
+definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
+ "size_multiset f M = setsum (wcount f M) (set_of M)"
+
+lemmas size_multiset_eq = size_multiset_def[unfolded wcount_def]
+
+instantiation multiset :: (type) size begin
+definition size_multiset where
+ size_multiset_overloaded_def: "size_multiset = Multiset.size_multiset (\<lambda>_. 0)"
instance ..
-
end
+lemmas size_multiset_overloaded_eq =
+ size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified]
+
+lemma size_multiset_empty [simp]: "size_multiset f {#} = 0"
+by (simp add: size_multiset_def)
+
lemma size_empty [simp]: "size {#} = 0"
-by (simp add: size_def)
+by (simp add: size_multiset_overloaded_def)
+
+lemma size_multiset_single [simp]: "size_multiset f {#b#} = Suc (f b)"
+by (simp add: size_multiset_eq)
lemma size_single [simp]: "size {#b#} = 1"
-by (simp add: size_def)
-
-lemma setsum_count_Int:
- "finite A ==> setsum (count N) (A \<inter> set_of N) = setsum (count N) A"
+by (simp add: size_multiset_overloaded_def)
+
+lemma setsum_wcount_Int:
+ "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_of N) = setsum (wcount f N) A"
apply (induct rule: finite_induct)
apply simp
-apply (simp add: Int_insert_left set_of_def)
+apply (simp add: Int_insert_left set_of_def wcount_def)
+done
+
+lemma size_multiset_union [simp]:
+ "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
+apply (simp add: size_multiset_def setsum_Un_nat setsum_addf setsum_wcount_Int wcount_union)
+apply (subst Int_commute)
+apply (simp add: setsum_wcount_Int)
done
lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
-apply (unfold size_def)
-apply (subgoal_tac "count (M + N) = (\<lambda>a. count M a + count N a)")
- prefer 2
- apply (rule ext, simp)
-apply (simp (no_asm_simp) add: setsum_Un_nat setsum_addf setsum_count_Int)
-apply (subst Int_commute)
-apply (simp (no_asm_simp) add: setsum_count_Int)
-done
+by (auto simp add: size_multiset_overloaded_def)
+
+lemma size_multiset_eq_0_iff_empty [iff]: "(size_multiset f M = 0) = (M = {#})"
+by (auto simp add: size_multiset_eq multiset_eq_iff)
lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
-by (auto simp add: size_def multiset_eq_iff)
+by (auto simp add: size_multiset_overloaded_def)
lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
lemma size_eq_Suc_imp_elem: "size M = Suc n ==> \<exists>a. a :# M"
-apply (unfold size_def)
+apply (unfold size_multiset_overloaded_eq)
apply (drule setsum_SucD)
apply auto
done
@@ -1309,7 +1327,7 @@
lemma size_eq_mcard:
"size = mcard"
- by (simp add: fun_eq_iff size_def mcard_unfold_setsum)
+ by (simp add: fun_eq_iff size_multiset_overloaded_eq mcard_unfold_setsum)
lemma mcard_multiset_of:
"mcard (multiset_of xs) = length xs"
@@ -3017,4 +3035,23 @@
theorems rel_multiset_induct[case_names empty add, induct pred: rel_multiset] =
rel_multiset'.induct[unfolded rel_multiset_rel_multiset'[symmetric]]
+
+subsection {* Size setup *}
+
+lemma multiset_size_o_map: "size_multiset g \<circ> mmap f = size_multiset (g \<circ> f)"
+apply (rule ext)
+apply (unfold o_apply)
+apply (induct_tac x)
+apply auto
+done
+
+setup {*
+BNF_LFP_Size.register_size_global @{type_name multiset} @{const_name size_multiset}
+ @{thms size_multiset_empty size_multiset_single size_multiset_union size_empty size_single
+ size_union}
+ @{thms multiset_size_o_map}
+*}
+
+hide_const (open) wcount
+
end
--- a/src/HOL/List.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/List.thy Wed Apr 23 17:05:48 2014 +0200
@@ -3488,8 +3488,8 @@
"x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
by (induct xs) (auto simp add: ac_simps)
-lemma (in monoid_add) list_size_conv_listsum:
- "list_size f xs = listsum (map f xs) + size xs"
+lemma (in monoid_add) size_list_conv_listsum:
+ "size_list f xs = listsum (map f xs) + size xs"
by (induct xs) auto
lemma (in monoid_add) length_concat:
@@ -5945,28 +5945,28 @@
subsection {* Size function *}
-lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
+lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (size_list f)"
by (rule is_measure_trivial)
-lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
+lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (size_option f)"
by (rule is_measure_trivial)
-lemma list_size_estimation[termination_simp]:
- "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
+lemma size_list_estimation[termination_simp]:
+ "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < size_list f xs"
by (induct xs) auto
-lemma list_size_estimation'[termination_simp]:
- "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
+lemma size_list_estimation'[termination_simp]:
+ "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> size_list f xs"
by (induct xs) auto
-lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
+lemma size_list_map[simp]: "size_list f (map g xs) = size_list (f o g) xs"
by (induct xs) auto
-lemma list_size_append[simp]: "list_size f (xs @ ys) = list_size f xs + list_size f ys"
+lemma size_list_append[simp]: "size_list f (xs @ ys) = size_list f xs + size_list f ys"
by (induct xs, auto)
-lemma list_size_pointwise[termination_simp]:
- "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
+lemma size_list_pointwise[termination_simp]:
+ "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> size_list f xs \<le> size_list g xs"
by (induct xs) force+
@@ -6757,7 +6757,7 @@
lemma length_transfer [transfer_rule]:
"(list_all2 A ===> op =) length length"
- unfolding list_size_overloaded_def by transfer_prover
+ unfolding size_list_overloaded_def size_list_def by transfer_prover
lemma rotate1_transfer [transfer_rule]:
"(list_all2 A ===> list_all2 A) rotate1 rotate1"
--- a/src/HOL/Nitpick.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Nitpick.thy Wed Apr 23 17:05:48 2014 +0200
@@ -113,9 +113,8 @@
declare nat.case [nitpick_simp del]
-lemma list_size_simp [nitpick_simp]:
-"list_size f xs = (if xs = [] then 0
- else Suc (f (hd xs) + list_size f (tl xs)))"
+lemma size_list_simp [nitpick_simp]:
+"size_list f xs = (if xs = [] then 0 else Suc (f (hd xs) + size_list f (tl xs)))"
"size xs = (if xs = [] then 0 else Suc (size (tl xs)))"
by (cases xs) auto
@@ -145,8 +144,9 @@
definition Frac :: "int \<times> int \<Rightarrow> bool" where
"Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
-axiomatization Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
- and Rep_Frac :: "'a \<Rightarrow> int \<times> int"
+axiomatization
+ Abs_Frac :: "int \<times> int \<Rightarrow> 'a" and
+ Rep_Frac :: "'a \<Rightarrow> int \<times> int"
definition zero_frac :: 'a where
"zero_frac \<equiv> Abs_Frac (0, 1)"
@@ -244,7 +244,7 @@
hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
prod_def refl'_def wf'_def card'_def setsum'_def
fold_graph'_def The_psimp Eps_psimp case_unit_unfold case_nat_unfold
- list_size_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
+ size_list_simp nat_gcd_def nat_lcm_def int_gcd_def int_lcm_def Frac_def
zero_frac_def one_frac_def num_def denom_def norm_frac_def frac_def
plus_frac_def times_frac_def uminus_frac_def number_of_frac_def
inverse_frac_def less_frac_def less_eq_frac_def of_frac_def wf_wfrec'_def
--- a/src/HOL/Probability/Fin_Map.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Probability/Fin_Map.thy Wed Apr 23 17:05:48 2014 +0200
@@ -267,12 +267,6 @@
definition dist_finmap where
"dist P Q = Max (range (\<lambda>i. dist ((P)\<^sub>F i) ((Q)\<^sub>F i))) + (if domain P = domain Q then 0 else 1)"
-lemma add_eq_zero_iff[simp]:
- fixes a b::real
- assumes "a \<ge> 0" "b \<ge> 0"
- shows "a + b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
-using assms by auto
-
lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^sub>F ` S)"
by (rule finite_subset[of _ "proj P ` (domain P \<inter> S \<union> {x})"]) auto
@@ -406,6 +400,7 @@
by (auto intro: Max_in Max_eqI)
show "dist P Q = 0 \<longleftrightarrow> P = Q"
by (auto simp: finmap_eq_iff dist_finmap_def Max_ge_iff finite_proj_diag Max_eq_iff
+ add_nonneg_eq_0_iff
intro!: Max_eqI image_eqI[where x=undefined])
next
fix P Q R::"'a \<Rightarrow>\<^sub>F 'b"
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Apr 23 17:05:48 2014 +0200
@@ -1286,8 +1286,7 @@
fun is_format_with_defs (THF _) = true
| is_format_with_defs _ = false
-fun make_fact ctxt format type_enc iff_for_eq
- ((name, stature as (_, status)), t) =
+fun make_fact ctxt format type_enc iff_for_eq ((name, stature as (_, status)), t) =
let
val role =
if is_format_with_defs format andalso status = Non_Rec_Def andalso
@@ -1742,8 +1741,7 @@
fun should_specialize_helper type_enc t =
could_specialize_helpers type_enc andalso not (null (Term.hidden_polymorphism t))
-fun add_helper_facts_of_sym ctxt format type_enc completish
- (s, {types, ...} : sym_info) =
+fun add_helper_facts_of_sym ctxt format type_enc completish (s, {types, ...} : sym_info) =
(case unprefix_and_unascii const_prefix s of
SOME mangled_s =>
let
@@ -1785,8 +1783,7 @@
end
| NONE => I)
fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab =
- Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish)
- sym_tab []
+ Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish) sym_tab []
(***************************************************************)
(* Type Classes Present in the Axiom or Conjecture Clauses *)
@@ -2438,24 +2435,31 @@
val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms
in mono_lines @ decl_lines end
-fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _)
- uncurried_aliases sym_tab =
+fun datatypes_of_sym_table ctxt ctrss (DFG Polymorphic) (type_enc as Native _) uncurried_aliases
+ sym_tab =
if is_type_enc_polymorphic type_enc then
let
val thy = Proof_Context.theory_of ctxt
+
fun do_ctr (s, T) =
let
val s' = make_fixed_const (SOME type_enc) s
val ary = ary_of T
- fun mk name = mk_aterm type_enc name (robust_const_type_args thy (s, T)) []
+ fun mk name = SOME (mk_aterm type_enc name (robust_const_type_args thy (s, T)) [])
in
- (case Symtab.lookup sym_tab s' of
- NONE => NONE
- | SOME ({min_ary, ...} : sym_info) =>
- if ary = min_ary then SOME (mk (s', s))
- else if uncurried_aliases then SOME (mk (aliased_uncurried ary (s', s)))
- else NONE)
+ if T = HOLogic.boolT then
+ (case proxify_const s' of
+ SOME proxy_base => mk (proxy_base |>> prefix const_prefix)
+ | NONE => NONE)
+ else
+ (case Symtab.lookup sym_tab s' of
+ NONE => NONE
+ | SOME ({min_ary, ...} : sym_info) =>
+ if ary = min_ary then mk (s', s)
+ else if uncurried_aliases then mk (aliased_uncurried ary (s', s))
+ else NONE)
end
+
fun datatype_of_ctrs (ctrs as (_, T1) :: _) =
let val ctrs' = map do_ctr ctrs in
if forall is_some ctrs' then
@@ -2610,8 +2614,7 @@
| (s, (sym, ty)) => cons (Sym_Decl (sym_decl_prefix ^ s, sym, ty ()))) syms []
in (heading, decls) :: problem end
-fun all_ctrss_of_datatypes ctxt =
- map (map_filter (try dest_Const) o #ctrs) (Ctr_Sugar.ctr_sugars_of ctxt)
+val all_ctrss_of_datatypes = map (map_filter (try dest_Const) o #ctrs) o Ctr_Sugar.ctr_sugars_of
val app_op_and_predicator_threshold = 45
--- a/src/HOL/Tools/BNF/bnf_comp.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Wed Apr 23 17:05:48 2014 +0200
@@ -707,7 +707,7 @@
fun mk_absT thy repT absT repU =
let
- val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) [];
+ val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) [];
in Term.typ_subst_TVars rho absT end
handle Type.TYPE_MATCH => raise Term.TYPE ("mk_absT", [repT, absT, repU], []);
--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 17:05:48 2014 +0200
@@ -53,6 +53,7 @@
val in_cong_of_bnf: bnf -> thm
val in_mono_of_bnf: bnf -> thm
val in_rel_of_bnf: bnf -> thm
+ val inj_map_of_bnf: bnf -> thm
val map_comp0_of_bnf: bnf -> thm
val map_comp_of_bnf: bnf -> thm
val map_cong0_of_bnf: bnf -> thm
@@ -217,6 +218,7 @@
in_cong: thm lazy,
in_mono: thm lazy,
in_rel: thm lazy,
+ inj_map: thm lazy,
map_comp: thm lazy,
map_cong: thm lazy,
map_id: thm lazy,
@@ -233,7 +235,7 @@
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
- map_comp map_cong map_id map_transfer rel_eq rel_flip set_map rel_cong rel_mono
+ inj_map map_comp map_cong map_id map_transfer rel_eq rel_flip set_map rel_cong rel_mono
rel_mono_strong rel_Grp rel_conversep rel_OO = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
@@ -243,6 +245,7 @@
in_cong = in_cong,
in_mono = in_mono,
in_rel = in_rel,
+ inj_map = inj_map,
map_comp = map_comp,
map_cong = map_cong,
map_id = map_id,
@@ -266,6 +269,7 @@
in_cong,
in_mono,
in_rel,
+ inj_map,
map_comp,
map_cong,
map_id,
@@ -287,6 +291,7 @@
in_cong = Lazy.map f in_cong,
in_mono = Lazy.map f in_mono,
in_rel = Lazy.map f in_rel,
+ inj_map = Lazy.map f inj_map,
map_comp = Lazy.map f map_comp,
map_cong = Lazy.map f map_cong,
map_id = Lazy.map f map_id,
@@ -404,6 +409,7 @@
val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf;
val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf;
val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf;
+val inj_map_of_bnf = Lazy.force o #inj_map o #facts o rep_bnf;
val map_def_of_bnf = #map_def o #defs o rep_bnf;
val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf;
val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
@@ -572,6 +578,7 @@
val in_bdN = "in_bd";
val in_monoN = "in_mono";
val in_relN = "in_rel";
+val inj_mapN = "inj_map";
val map_id0N = "map_id0";
val map_idN = "map_id";
val map_comp0N = "map_comp0";
@@ -624,6 +631,7 @@
(in_bdN, [Lazy.force (#in_bd facts)]),
(in_monoN, [Lazy.force (#in_mono facts)]),
(in_relN, [Lazy.force (#in_rel facts)]),
+ (inj_mapN, [Lazy.force (#inj_map facts)]),
(map_comp0N, [#map_comp0 axioms]),
(map_id0N, [#map_id0 axioms]),
(map_transferN, [Lazy.force (#map_transfer facts)]),
@@ -933,8 +941,8 @@
||>> mk_Frees "R" transfer_domRTs
||>> mk_Frees "S" transfer_ranRTs;
- val fs_copy = map2 (retype_free o fastype_of) fs gs;
- val x_copy = retype_free CA' y;
+ val fs_copy = map2 (retype_const_or_free o fastype_of) fs gs;
+ val x_copy = retype_const_or_free CA' y;
val rel = mk_bnf_rel pred2RTs CA' CB';
val relAsAs = mk_bnf_rel self_pred2RTs CA' CA';
@@ -1103,6 +1111,19 @@
val map_cong = Lazy.lazy mk_map_cong;
+ fun mk_inj_map () =
+ let
+ val prems = map (HOLogic.mk_Trueprop o mk_inj) fs;
+ val concl = HOLogic.mk_Trueprop (mk_inj (Term.list_comb (bnf_map_AsBs, fs)));
+ val goal = fold_rev Logic.all fs (Logic.list_implies (prems, concl));
+ in
+ Goal.prove_sorry lthy [] [] goal (fn _ => mk_inj_map_tac live (Lazy.force map_id)
+ (Lazy.force map_comp) (#map_cong0 axioms) (Lazy.force map_cong))
+ |> Thm.close_derivation
+ end;
+
+ val inj_map = Lazy.lazy mk_inj_map;
+
val set_map = map (fn thm => Lazy.lazy (fn () => mk_set_map thm)) (#set_map0 axioms);
val wit_thms =
@@ -1289,7 +1310,7 @@
val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
- in_mono in_rel map_comp map_cong map_id map_transfer rel_eq rel_flip set_map
+ in_mono in_rel inj_map map_comp map_cong map_id map_transfer rel_eq rel_flip set_map
rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
val wits = map2 mk_witness bnf_wits wit_thms;
@@ -1331,7 +1352,7 @@
(*|> Sign.restore_naming thy*)
end;
-val bnf_interpretation = BNF_Interpretation.interpretation o with_repaired_path;
+fun bnf_interpretation f = BNF_Interpretation.interpretation (with_repaired_path f);
fun register_bnf key bnf =
Local_Theory.declaration {syntax = false, pervasive = true}
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Apr 23 17:05:48 2014 +0200
@@ -9,10 +9,11 @@
signature BNF_DEF_TACTICS =
sig
val mk_collect_set_map_tac: thm list -> tactic
+ val mk_in_mono_tac: int -> tactic
+ val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic
val mk_map_id: thm -> thm
val mk_map_comp: thm -> thm
val mk_map_cong_tac: Proof.context -> thm -> tactic
- val mk_in_mono_tac: int -> tactic
val mk_set_map: thm -> thm
val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic
@@ -55,6 +56,16 @@
((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
(etac subset_trans THEN' atac) 1;
+fun mk_inj_map_tac n map_id map_comp map_cong0 map_cong =
+ let
+ val map_cong' = map_cong OF (asm_rl :: replicate n refl);
+ val map_cong0' = map_cong0 OF (replicate n @{thm the_inv_f_o_f_id});
+ in
+ HEADGOAL (rtac @{thm injI} THEN' etac (map_cong' RS box_equals) THEN'
+ REPEAT_DETERM_N 2 o (rtac (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN'
+ REPEAT_DETERM_N n o atac))
+ end;
+
fun mk_collect_set_map_tac set_map0s =
(rtac (@{thm collect_comp} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
EVERY' (map (fn set_map0 =>
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 17:05:48 2014 +0200
@@ -7,34 +7,10 @@
signature BNF_FP_DEF_SUGAR =
sig
- type fp_sugar =
- {T: typ,
- X: typ,
- fp: BNF_Util.fp_kind,
- fp_res_index: int,
- fp_res: BNF_FP_Util.fp_result,
- pre_bnf: BNF_Def.bnf,
- absT_info: BNF_Comp.absT_info,
- nested_bnfs: BNF_Def.bnf list,
- nesting_bnfs: BNF_Def.bnf list,
- ctrXs_Tss: typ list list,
- ctr_defs: thm list,
- ctr_sugar: Ctr_Sugar.ctr_sugar,
- co_rec: term,
- maps: thm list,
- common_co_inducts: thm list,
- co_inducts: thm list,
- co_rec_thms: thm list,
- disc_co_recs: thm list,
- sel_co_recss: thm list list,
- rel_injects: thm list};
-
- val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
- val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
- val fp_sugar_of: Proof.context -> string -> fp_sugar option
- val fp_sugars_of: Proof.context -> fp_sugar list
- val fp_sugar_interpretation: (fp_sugar -> theory -> theory) -> theory -> theory
- val register_fp_sugar: string -> fp_sugar -> local_theory -> local_theory
+ val fp_sugar_of: Proof.context -> string -> BNF_FP_Util.fp_sugar option
+ val fp_sugars_of: Proof.context -> BNF_FP_Util.fp_sugar list
+ val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) -> theory -> theory
+ val register_fp_sugars: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory
val co_induct_of: 'a list -> 'a
val strong_co_induct_of: 'a list -> 'a
@@ -73,7 +49,7 @@
typ list list
* (typ list list list list * typ list list list * typ list list list list * typ list)
val define_rec:
- (typ list list * typ list list list list * term list list * term list list list list) option ->
+ typ list list * typ list list list list * term list list * term list list list list ->
(string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context ->
(term * thm) * Proof.context
val define_corec: 'a * term list * term list list
@@ -118,57 +94,10 @@
open BNF_Def
open BNF_FP_Util
open BNF_FP_Def_Sugar_Tactics
+open BNF_LFP_Size
val EqN = "Eq_";
-type fp_sugar =
- {T: typ,
- X: typ,
- fp: fp_kind,
- fp_res_index: int,
- fp_res: fp_result,
- pre_bnf: bnf,
- absT_info: absT_info,
- nested_bnfs: bnf list,
- nesting_bnfs: bnf list,
- ctrXs_Tss: typ list list,
- ctr_defs: thm list,
- ctr_sugar: Ctr_Sugar.ctr_sugar,
- co_rec: term,
- maps: thm list,
- common_co_inducts: thm list,
- co_inducts: thm list,
- co_rec_thms: thm list,
- disc_co_recs: thm list,
- sel_co_recss: thm list list,
- rel_injects: thm list};
-
-fun morph_fp_sugar phi ({T, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
- nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, maps, common_co_inducts, co_inducts,
- co_rec_thms, disc_co_recs, sel_co_recss, rel_injects} : fp_sugar) =
- {T = Morphism.typ phi T,
- X = Morphism.typ phi X,
- fp = fp,
- fp_res = morph_fp_result phi fp_res,
- fp_res_index = fp_res_index,
- pre_bnf = morph_bnf phi pre_bnf,
- absT_info = morph_absT_info phi absT_info,
- nested_bnfs = map (morph_bnf phi) nested_bnfs,
- nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
- ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
- ctr_defs = map (Morphism.thm phi) ctr_defs,
- ctr_sugar = morph_ctr_sugar phi ctr_sugar,
- co_rec = Morphism.term phi co_rec,
- maps = map (Morphism.thm phi) maps,
- common_co_inducts = map (Morphism.thm phi) common_co_inducts,
- co_inducts = map (Morphism.thm phi) co_inducts,
- co_rec_thms = map (Morphism.thm phi) co_rec_thms,
- disc_co_recs = map (Morphism.thm phi) disc_co_recs,
- sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss,
- rel_injects = map (Morphism.thm phi) rel_injects};
-
-val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
-
structure Data = Generic_Data
(
type T = fp_sugar Symtab.table;
@@ -189,39 +118,45 @@
structure FP_Sugar_Interpretation = Interpretation
(
- type T = fp_sugar;
- val eq: T * T -> bool = op = o pairself #T;
+ type T = fp_sugar list;
+ val eq: T * T -> bool = op = o pairself (map #T);
);
(* FIXME naming *)
-fun with_repaired_path f (fp_sugar as {T, ...} : fp_sugar) thy =
+fun with_repaired_path f (fp_sugars as ({T = Type (s, _), ...} : fp_sugar) :: _) thy =
thy
(*|> Sign.root_path*)
- (*|> Sign.add_path (Long_Name.qualifier (fst (dest_Type T)))*)
- |> (fn thy => f (morph_fp_sugar (Morphism.transfer_morphism thy) fp_sugar) thy)
+ (*|> Sign.add_path (Long_Name.qualifier s)*)
+ |> f fp_sugars
(*|> Sign.restore_naming thy*);
-val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
+fun fp_sugar_interpretation f = FP_Sugar_Interpretation.interpretation (with_repaired_path f);
-fun register_fp_sugar key fp_sugar =
- Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)))
- #> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugar);
+fun register_fp_sugars (fp_sugars as {fp, ...} :: _) =
+ fold (fn fp_sugar as {T = Type (s, _), ...} =>
+ Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
+ fp_sugars
+ #> fp = Least_FP ? generate_lfp_size fp_sugars
+ #> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugars);
-fun register_fp_sugars Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs (fp_res as {Ts, ...})
- ctrXs_Tsss ctr_defss ctr_sugars co_recs mapss common_co_inducts co_inductss co_rec_thmss
- disc_co_recss sel_co_recsss rel_injects lthy =
- (0, lthy)
- |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
- register_fp_sugar s {T = T, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
- pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, nested_bnfs = nested_bnfs,
- nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk,
- ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, maps = nth mapss kk,
- common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk,
- co_rec_thms = nth co_rec_thmss kk, disc_co_recs = nth disc_co_recss kk,
- sel_co_recss = nth sel_co_recsss kk, rel_injects = nth rel_injects kk}
- lthy)) Ts
- |> snd;
+fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
+ ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss common_co_inducts co_inductss
+ co_rec_thmss disc_co_recss sel_co_recsss rel_injectss rel_distinctss =
+ let
+ val fp_sugars =
+ map_index (fn (kk, T) =>
+ {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk,
+ pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, nested_bnfs = nested_bnfs,
+ nesting_bnfs = nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk,
+ ctr_sugar = nth ctr_sugars kk, co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk,
+ maps = nth mapss kk, common_co_inducts = common_co_inducts,
+ co_inducts = nth co_inductss kk, co_rec_thms = nth co_rec_thmss kk,
+ disc_co_recs = nth disc_co_recss kk, sel_co_recss = nth sel_co_recsss kk,
+ rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk}) Ts
+ in
+ register_fp_sugars fp_sugars
+ end;
(* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A",
"x.x_A", "y.A"). *)
@@ -443,18 +378,14 @@
fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =
let
val thy = Proof_Context.theory_of lthy;
- val nn = length fpTs;
val (xtor_co_rec_fun_Ts, xtor_co_recs) =
mk_xtor_co_recs thy fp fpTs Cs xtor_co_recs0 |> `(binder_fun_types o fastype_of o hd);
val ((recs_args_types, corecs_args_types), lthy') =
if fp = Least_FP then
- if nn = 1 andalso forall (forall (forall (not o exists_subtype_in fpTs))) ctr_Tsss then
- ((NONE, NONE), lthy)
- else
- mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
- |>> (rpair NONE o SOME)
+ mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
+ |>> (rpair NONE o SOME)
else
mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
|>> (pair NONE o SOME);
@@ -489,20 +420,19 @@
((cst', def'), lthy')
end;
-fun define_rec NONE _ _ _ _ _ = pair (Term.dummy, refl)
- | define_rec (SOME (_, _, fss, xssss)) mk_binding fpTs Cs reps ctor_rec =
- let
- val nn = length fpTs;
- val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec)
- |>> map domain_type ||> domain_type;
- in
- define_co_rec Least_FP fpT Cs (mk_binding recN)
- (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
- map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
- mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss)
- (map flat_rec_arg_args xsss))
- ctor_rec_absTs reps fss xssss)))
- end;
+fun define_rec (_, _, fss, xssss) mk_binding fpTs Cs reps ctor_rec =
+ let
+ val nn = length fpTs;
+ val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec)
+ |>> map domain_type ||> domain_type;
+ in
+ define_co_rec Least_FP fpT Cs (mk_binding recN)
+ (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
+ map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
+ mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss)
+ (map flat_rec_arg_args xsss))
+ ctor_rec_absTs reps fss xssss)))
+ end;
fun define_corec (_, cs, cpss, ((pgss, cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
let
@@ -662,10 +592,7 @@
map2 (map2 prove) goalss tacss
end;
- val rec_thmss =
- (case rec_args_typess of
- SOME types => mk_rec_thmss types recs rec_defs ctor_rec_thms
- | NONE => replicate nn []);
+ val rec_thmss = mk_rec_thmss (the rec_args_typess) recs rec_defs ctor_rec_thms;
in
((induct_thms, induct_thm, [induct_case_names_attr]),
(rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
@@ -1083,6 +1010,7 @@
val dtors = map (mk_dtor As) dtors0;
val fpTs = map (domain_type o fastype_of) dtors;
+ val fpBTs = map B_ify fpTs;
fun massage_simple_notes base =
filter_out (null o #2)
@@ -1212,7 +1140,7 @@
end;
val cxIns = map2 (mk_cIn ctor) ks xss;
- val cyIns = map2 (mk_cIn (map_types B_ify ctor)) ks yss;
+ val cyIns = map2 (mk_cIn (Term.map_types B_ify ctor)) ks yss;
fun mk_map_thm ctr_def' cxIn =
fold_thms lthy [ctr_def']
@@ -1303,7 +1231,7 @@
(wrap_ctrs
#> derive_maps_sets_rels
##>>
- (if fp = Least_FP then define_rec recs_args_types mk_binding fpTs Cs reps
+ (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps
else define_corec (the corecs_args_types) mk_binding fpTs Cs abss) xtor_co_rec
#> massage_res, lthy')
end;
@@ -1318,7 +1246,7 @@
injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
fun derive_note_induct_recs_thms_for_types
- ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
+ ((((mapss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
(recs, rec_defs)), lthy) =
let
val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
@@ -1328,12 +1256,8 @@
val induct_type_attr = Attrib.internal o K o Induct.induct_type;
- val (recs', rec_thmss') =
- if is_some recs_args_types then (recs, rec_thmss)
- else (map #casex ctr_sugars, map #case_thms ctr_sugars);
-
val simp_thmss =
- map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injects rel_distincts setss;
+ map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injectss rel_distinctss setss;
val common_notes =
(if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
@@ -1346,18 +1270,16 @@
|> massage_multi_notes;
in
lthy
- |> (if is_some recs_args_types then
- Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
- else
- I)
+ |> Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_fp_sugars Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
- ctrXs_Tsss ctr_defss ctr_sugars recs' mapss [induct_thm] (map single induct_thms)
- rec_thmss' (replicate nn []) (replicate nn []) rel_injects
+ |> register_as_fp_sugars fpTs fpBTs Xs Least_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs
+ fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs mapss [induct_thm]
+ (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss
+ rel_distinctss
end;
fun derive_note_coinduct_corecs_thms_for_types
- ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
+ ((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
(corecs, corec_defs)), lthy) =
let
val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
@@ -1378,7 +1300,7 @@
val simp_thmss =
map6 mk_simp_thms ctr_sugars
(map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
- mapss rel_injects rel_distincts setss;
+ mapss rel_injectss rel_distinctss setss;
val common_notes =
(if nn > 1 then
@@ -1404,10 +1326,10 @@
|> fold (curry (Spec_Rules.add Spec_Rules.Equational) corecs)
[flat sel_corec_thmss, flat corec_thmss]
|> Local_Theory.notes (common_notes @ notes) |> snd
- |> register_fp_sugars Xs Greatest_FP pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
- ctrXs_Tsss ctr_defss ctr_sugars corecs mapss [coinduct_thm, strong_coinduct_thm]
- (transpose [coinduct_thms, strong_coinduct_thms]) corec_thmss disc_corec_thmss
- sel_corec_thmsss rel_injects
+ |> register_as_fp_sugars fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos nested_bnfs
+ nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs mapss
+ [coinduct_thm, strong_coinduct_thm] (transpose [coinduct_thms, strong_coinduct_thms])
+ corec_thmss disc_corec_thmss sel_corec_thmsss rel_injectss rel_distinctss
end;
val lthy'' = lthy'
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 23 17:05:48 2014 +0200
@@ -8,7 +8,7 @@
signature BNF_FP_N2M =
sig
val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
- BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list ->
+ BNF_FP_Util.fp_sugar list -> binding list -> (string * sort) list ->
typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
BNF_FP_Util.fp_result * local_theory
end;
@@ -25,7 +25,7 @@
open BNF_FP_N2M_Tactics
fun force_typ ctxt T =
- map_types Type_Infer.paramify_vars
+ Term.map_types Type_Infer.paramify_vars
#> Type.constraint T
#> Syntax.check_term ctxt
#> singleton (Variable.polymorphic ctxt);
@@ -239,7 +239,7 @@
val co_recs = of_fp_res #xtor_co_recs;
val ns = map (length o #Ts o #fp_res) fp_sugars;
- fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
+ fun substT rho (Type (@{type_name fun}, [T, U])) = substT rho T --> substT rho U
| substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
| substT _ T = T;
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Apr 23 17:05:48 2014 +0200
@@ -11,13 +11,13 @@
val dest_map: Proof.context -> string -> term -> term * term list
val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
- term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
- (BNF_FP_Def_Sugar.fp_sugar list
+ term list list list list -> BNF_FP_Util.fp_sugar list -> local_theory ->
+ (BNF_FP_Util.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
* local_theory
val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
- (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
+ (typ list * int list * BNF_FP_Util.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
* local_theory
end;
@@ -247,7 +247,7 @@
val ((co_recs, co_rec_defs), lthy) =
fold_map2 (fn b =>
- if fp = Least_FP then define_rec recs_args_types (mk_binding b) fpTs Cs reps
+ if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps
else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
fp_bs xtor_co_recs lthy
|>> split_list;
@@ -274,20 +274,22 @@
val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
- fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec maps
- co_inducts co_rec_thms disc_corec_thms sel_corec_thmss rel_injects =
- {T = T, X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf,
- absT_info = absT_info, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs,
- ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec,
- maps = maps, common_co_inducts = common_co_inducts, co_inducts = co_inducts,
+ fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
+ co_rec_def maps co_inducts co_rec_thms disc_corec_thms sel_corec_thmss
+ ({rel_injects, rel_distincts, ...} : fp_sugar) =
+ {T = T, BT = Term.dummyT (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res,
+ fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info, nested_bnfs = nested_bnfs,
+ nesting_bnfs = nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs,
+ ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps,
+ common_co_inducts = common_co_inducts, co_inducts = co_inducts,
co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
- sel_co_recss = sel_corec_thmss, rel_injects = rel_injects}
+ sel_co_recss = sel_corec_thmss, rel_injects = rel_injects, rel_distincts = rel_distincts}
|> morph_fp_sugar phi;
val target_fp_sugars =
- map15 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
- co_recs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss sel_corec_thmsss
- (map #rel_injects fp_sugars0);
+ map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
+ co_recs co_rec_defs mapss (transpose co_inductss) co_rec_thmss disc_corec_thmss
+ sel_corec_thmsss fp_sugars0;
val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
in
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Wed Apr 23 17:05:48 2014 +0200
@@ -29,7 +29,7 @@
val exists_strict_subtype_in: typ list -> typ -> bool
val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list
- val retype_free: typ -> term -> term
+ val retype_const_or_free: typ -> term -> term
val drop_all: term -> term
val permute_args: int -> term -> term
@@ -82,8 +82,9 @@
fun tvar_subst thy Ts Us =
Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) [];
-fun retype_free T (Free (s, _)) = Free (s, T)
- | retype_free _ t = raise TERM ("retype_free", [t]);
+fun retype_const_or_free T (Const (s, _)) = Const (s, T)
+ | retype_const_or_free T (Free (s, _)) = Free (s, T)
+ | retype_const_or_free _ t = raise TERM ("retype_const_or_free", [t]);
fun drop_all t =
subst_bounds (strip_qnt_vars @{const_name Pure.all} t |> map Free |> rev,
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Apr 23 17:05:48 2014 +0200
@@ -28,6 +28,34 @@
val morph_fp_result: morphism -> fp_result -> fp_result
+ type fp_sugar =
+ {T: typ,
+ BT: typ,
+ X: typ,
+ fp: BNF_Util.fp_kind,
+ fp_res_index: int,
+ fp_res: fp_result,
+ pre_bnf: BNF_Def.bnf,
+ absT_info: BNF_Comp.absT_info,
+ nested_bnfs: BNF_Def.bnf list,
+ nesting_bnfs: BNF_Def.bnf list,
+ ctrXs_Tss: typ list list,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar,
+ co_rec: term,
+ co_rec_def: thm,
+ maps: thm list,
+ common_co_inducts: thm list,
+ co_inducts: thm list,
+ co_rec_thms: thm list,
+ disc_co_recs: thm list,
+ sel_co_recss: thm list list,
+ rel_injects: thm list,
+ rel_distincts: thm list};
+
+ val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
+ val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
+
val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
@@ -184,6 +212,7 @@
structure BNF_FP_Util : BNF_FP_UTIL =
struct
+open Ctr_Sugar
open BNF_Comp
open BNF_Def
open BNF_Util
@@ -226,6 +255,60 @@
xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
+type fp_sugar =
+ {T: typ,
+ BT: typ,
+ X: typ,
+ fp: fp_kind,
+ fp_res_index: int,
+ fp_res: fp_result,
+ pre_bnf: bnf,
+ absT_info: absT_info,
+ nested_bnfs: bnf list,
+ nesting_bnfs: bnf list,
+ ctrXs_Tss: typ list list,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar,
+ co_rec: term,
+ co_rec_def: thm,
+ maps: thm list,
+ common_co_inducts: thm list,
+ co_inducts: thm list,
+ co_rec_thms: thm list,
+ disc_co_recs: thm list,
+ sel_co_recss: thm list list,
+ rel_injects: thm list,
+ rel_distincts: thm list};
+
+fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
+ nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
+ co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
+ {T = Morphism.typ phi T,
+ BT = Morphism.typ phi BT,
+ X = Morphism.typ phi X,
+ fp = fp,
+ fp_res = morph_fp_result phi fp_res,
+ fp_res_index = fp_res_index,
+ pre_bnf = morph_bnf phi pre_bnf,
+ absT_info = morph_absT_info phi absT_info,
+ nested_bnfs = map (morph_bnf phi) nested_bnfs,
+ nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+ ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
+ ctr_defs = map (Morphism.thm phi) ctr_defs,
+ ctr_sugar = morph_ctr_sugar phi ctr_sugar,
+ co_rec = Morphism.term phi co_rec,
+ co_rec_def = Morphism.thm phi co_rec_def,
+ maps = map (Morphism.thm phi) maps,
+ common_co_inducts = map (Morphism.thm phi) common_co_inducts,
+ co_inducts = map (Morphism.thm phi) co_inducts,
+ co_rec_thms = map (Morphism.thm phi) co_rec_thms,
+ disc_co_recs = map (Morphism.thm phi) disc_co_recs,
+ sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss,
+ rel_injects = map (Morphism.thm phi) rel_injects,
+ rel_distincts = map (Morphism.thm phi) rel_distincts};
+
+val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
+
fun time ctxt timer msg = (if Config.get ctxt bnf_timing
then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
"ms")
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Apr 23 17:05:48 2014 +0200
@@ -3,7 +3,7 @@
Author: Andrei Popescu, TU Muenchen
Copyright 2012
-Datatype construction.
+New-style datatype construction.
*)
signature BNF_LFP =
@@ -906,9 +906,9 @@
||>> mk_Frees "f" fTs
||>> mk_Frees "s" rec_sTs;
- val Izs = map2 retype_free Ts zs;
- val phis = map2 retype_free (map mk_pred1T Ts) init_phis;
- val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis;
+ val Izs = map2 retype_const_or_free Ts zs;
+ val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis;
+ val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis;
fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Apr 23 17:05:48 2014 +0200
@@ -3,7 +3,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2013
-Recursor sugar ("primrec").
+New-style recursor sugar ("primrec").
*)
signature BNF_LFP_REC_SUGAR =
@@ -333,10 +333,11 @@
nth_map arg_idx (K (nth ctr_args ctr_arg_idx)))
no_calls'
|> fold (fn (ctr_arg_idx, (arg_idx, T)) => fn xs =>
- nth_map arg_idx (K (ensure_unique xs (retype_free T (nth ctr_args ctr_arg_idx)))) xs)
+ nth_map arg_idx (K (ensure_unique xs
+ (retype_const_or_free T (nth ctr_args ctr_arg_idx)))) xs)
mutual_calls'
|> fold (fn (ctr_arg_idx, (arg_idx, T)) =>
- nth_map arg_idx (K (retype_free T (nth ctr_args ctr_arg_idx))))
+ nth_map arg_idx (K (retype_const_or_free T (nth ctr_args ctr_arg_idx))))
nested_calls';
val fun_name_ctr_pos_list =
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Wed Apr 23 17:05:48 2014 +0200
@@ -3,7 +3,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2013
-More recursor sugar.
+More new-style recursor sugar.
*)
structure BNF_LFP_Rec_Sugar_More : sig end =
@@ -141,14 +141,14 @@
in
if ctr_pos >= 0 then
if d = SOME ~1 andalso length vs = ctr_pos then
- list_comb (permute_args ctr_pos (snd_const pT), vs)
+ Term.list_comb (permute_args ctr_pos (snd_const pT), vs)
else if length vs > ctr_pos andalso is_some d andalso
d = try (fn Bound n => n) (nth vs ctr_pos) then
- list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs))
+ Term.list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs))
else
raise PRIMREC ("recursive call not directly applied to constructor argument", [t])
else
- list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs)
+ Term.list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs)
end
in
subst (SOME ~1)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 17:05:48 2014 +0200
@@ -0,0 +1,355 @@
+(* Title: HOL/Tools/BNF/bnf_lfp_size.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2014
+
+Generation of size functions for new-style datatypes.
+*)
+
+signature BNF_LFP_SIZE =
+sig
+ val register_size: string -> string -> thm list -> thm list -> local_theory -> local_theory
+ val register_size_global: string -> string -> thm list -> thm list -> theory -> theory
+ val lookup_size: Proof.context -> string -> (string * (thm list * thm list)) option
+ val lookup_size_global: theory -> string -> (string * (thm list * thm list)) option
+ val generate_lfp_size: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory
+end;
+
+structure BNF_LFP_Size : BNF_LFP_SIZE =
+struct
+
+open BNF_Util
+open BNF_Tactics
+open BNF_Def
+open BNF_FP_Util
+
+val size_N = "size_"
+
+val rec_o_mapN = "rec_o_map"
+val sizeN = "size"
+val size_o_mapN = "size_o_map"
+
+val nitpicksimp_attrs = @{attributes [nitpick_simp]};
+val simp_attrs = @{attributes [simp]};
+val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs;
+
+structure Data = Generic_Data
+(
+ type T = (string * (thm list * thm list)) Symtab.table;
+ val empty = Symtab.empty;
+ val extend = I
+ fun merge data = Symtab.merge (K true) data;
+);
+
+fun register_size T_name size_name size_simps size_o_maps =
+ Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps)))));
+
+fun register_size_global T_name size_name size_simps size_o_maps =
+ Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps)))));
+
+val lookup_size = Symtab.lookup o Data.get o Context.Proof;
+val lookup_size_global = Symtab.lookup o Data.get o Context.Theory;
+
+val zero_nat = @{const zero_class.zero (nat)};
+
+fun mk_plus_nat (t1, t2) = Const (@{const_name Groups.plus},
+ HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
+
+fun mk_to_natT T = T --> HOLogic.natT;
+
+fun mk_abs_zero_nat T = Term.absdummy T zero_nat;
+
+fun pointfill ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong);
+
+fun mk_unabs_def_unused_0 n =
+ funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
+
+val rec_o_map_simp_thms =
+ @{thms o_def id_def case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def};
+
+fun mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map =
+ unfold_thms_tac ctxt [rec_def] THEN
+ HEADGOAL (rtac (ctor_rec_o_map RS trans)) THEN
+ PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN
+ HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop abs_inverses @
+ rec_o_map_simp_thms) ctxt));
+
+val size_o_map_simp_thms = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
+
+fun mk_size_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
+ unfold_thms_tac ctxt [size_def] THEN
+ HEADGOAL (rtac (rec_o_map RS trans) THEN'
+ asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt)) THEN
+ IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
+
+fun generate_lfp_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs),
+ fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs,
+ nesting_bnfs, ...} : fp_sugar) :: _) lthy0 =
+ let
+ val data = Data.get (Context.Proof lthy0);
+
+ val Ts = map #T fp_sugars
+ val T_names = map (fst o dest_Type) Ts;
+ val nn = length Ts;
+
+ val B_ify = Term.typ_subst_atomic (As ~~ Bs);
+
+ val recs = map #co_rec fp_sugars;
+ val rec_thmss = map #co_rec_thms fp_sugars;
+ val rec_Ts as rec_T1 :: _ = map fastype_of recs;
+ val rec_arg_Ts = binder_fun_types rec_T1;
+ val Cs = map body_type rec_Ts;
+ val Cs_rho = map (rpair HOLogic.natT) Cs;
+ val substCnatT = Term.subst_atomic_types Cs_rho;
+
+ val f_Ts = map mk_to_natT As;
+ val f_TsB = map mk_to_natT Bs;
+ val num_As = length As;
+
+ fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0);
+
+ val f_names = variant_names num_As "f";
+ val fs = map2 (curry Free) f_names f_Ts;
+ val fsB = map2 (curry Free) f_names f_TsB;
+ val As_fs = As ~~ fs;
+
+ val size_bs =
+ map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o
+ Long_Name.base_name) T_names;
+
+ fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T'
+ | is_pair_C _ _ = false;
+
+ fun mk_size_of_typ (T as TFree _) =
+ pair (case AList.lookup (op =) As_fs T of
+ SOME f => f
+ | NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T)
+ | mk_size_of_typ (T as Type (s, Ts)) =
+ if is_pair_C s Ts then
+ pair (snd_const T)
+ else if exists (exists_subtype_in As) Ts then
+ (case Symtab.lookup data s of
+ SOME (size_name, (_, size_o_maps as _ :: _)) =>
+ let
+ val (args, size_o_mapss') = split_list (map (fn T => mk_size_of_typ T []) Ts);
+ val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T);
+ in
+ fold (union Thm.eq_thm) (size_o_maps :: size_o_mapss')
+ #> pair (Term.list_comb (size_const, args))
+ end
+ | _ => pair (mk_abs_zero_nat T))
+ else
+ pair (mk_abs_zero_nat T);
+
+ fun mk_size_of_arg t =
+ mk_size_of_typ (fastype_of t) #>> (fn s => substCnatT (betapply (s, t)));
+
+ fun mk_size_arg rec_arg_T size_o_maps =
+ let
+ val x_Ts = binder_types rec_arg_T;
+ val m = length x_Ts;
+ val x_names = variant_names m "x";
+ val xs = map2 (curry Free) x_names x_Ts;
+ val (summands, size_o_maps') =
+ fold_map mk_size_of_arg xs size_o_maps
+ |>> remove (op =) zero_nat;
+ val sum =
+ if null summands then HOLogic.zero
+ else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
+ in
+ (fold_rev Term.lambda (map substCnatT xs) sum, size_o_maps')
+ end;
+
+ fun mk_size_rhs recx size_o_maps =
+ let val (args, size_o_maps') = fold_map mk_size_arg rec_arg_Ts size_o_maps in
+ (fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)), size_o_maps')
+ end;
+
+ val maybe_conceal_def_binding = Thm.def_binding
+ #> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
+
+ val (size_rhss, nested_size_o_maps) = fold_map mk_size_rhs recs [];
+ val size_Ts = map fastype_of size_rhss;
+
+ val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0
+ |> apfst split_list o fold_map2 (fn b => fn rhs =>
+ Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd)
+ size_bs size_rhss
+ ||> `Local_Theory.restore;
+
+ val phi = Proof_Context.export_morphism lthy1 lthy1';
+
+ val size_defs = map (Morphism.thm phi) raw_size_defs;
+
+ val size_consts0 = map (Morphism.term phi) raw_size_consts;
+ val size_consts = map2 retype_const_or_free size_Ts size_consts0;
+ val size_constsB = map (Term.map_types B_ify) size_consts;
+
+ val zeros = map mk_abs_zero_nat As;
+
+ val overloaded_size_rhss = map (fn c => Term.list_comb (c, zeros)) size_consts;
+ val overloaded_size_Ts = map fastype_of overloaded_size_rhss;
+ val overloaded_size_consts = map (curry Const @{const_name size}) overloaded_size_Ts;
+ val overloaded_size_def_bs =
+ map (maybe_conceal_def_binding o Binding.suffix_name "_overloaded") size_bs;
+
+ fun define_overloaded_size def_b lhs0 rhs lthy =
+ let
+ val Free (c, _) = Syntax.check_term lthy lhs0;
+ val (thm, lthy') = lthy
+ |> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs))
+ |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
+ val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
+ val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
+ in (thm', lthy') end;
+
+ val (overloaded_size_defs, lthy2) = lthy1
+ |> Local_Theory.background_theory_result
+ (Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size])
+ #> fold_map3 define_overloaded_size overloaded_size_def_bs overloaded_size_consts
+ overloaded_size_rhss
+ ##> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+ ##> Local_Theory.exit_global);
+
+ val size_defs' =
+ map (mk_unabs_def (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs;
+ val size_defs_unused_0 =
+ map (mk_unabs_def_unused_0 (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs;
+ val overloaded_size_defs' =
+ map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs;
+
+ val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps;
+ val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs @ nesting_bnfs);
+
+ fun derive_size_simp size_def' simp0 =
+ (trans OF [size_def', simp0])
+ |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_id snd_o_convol} @
+ all_inj_maps @ nested_size_maps) lthy2)
+ |> fold_thms lthy2 size_defs_unused_0;
+ fun derive_overloaded_size_simp size_def' simp0 =
+ (trans OF [size_def', simp0])
+ |> unfold_thms lthy2 @{thms add_0_left add_0_right}
+ |> fold_thms lthy2 overloaded_size_defs';
+
+ val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
+ val size_simps = flat size_simpss;
+ val overloaded_size_simpss =
+ map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss;
+ val size_thmss = map2 append size_simpss overloaded_size_simpss;
+
+ val ABs = As ~~ Bs;
+ val g_names = variant_names num_As "g";
+ val gs = map2 (curry Free) g_names (map (op -->) ABs);
+
+ val liveness = map (op <>) ABs;
+ val live_gs = AList.find (op =) (gs ~~ liveness) true;
+ val live = length live_gs;
+
+ val maps0 = map map_of_bnf fp_bnfs;
+
+ val (rec_o_map_thmss, size_o_map_thmss) =
+ if live = 0 then
+ `I (replicate nn [])
+ else
+ let
+ val pre_bnfs = map #pre_bnf fp_sugars;
+ val pre_map_defs = map map_def_of_bnf pre_bnfs;
+ val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
+ val rec_defs = map #co_rec_def fp_sugars;
+
+ val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
+
+ val num_rec_args = length rec_arg_Ts;
+ val h_Ts = map B_ify rec_arg_Ts;
+ val h_names = variant_names num_rec_args "h";
+ val hs = map2 (curry Free) h_names h_Ts;
+ val hrecs = map (fn recx => Term.list_comb (Term.map_types B_ify recx, hs)) recs;
+
+ val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) hrecs gmaps;
+
+ val ABgs = ABs ~~ gs;
+
+ fun mk_rec_arg_arg (x as Free (_, T)) =
+ let val U = B_ify T in
+ if T = U then x else build_map lthy2 (the o AList.lookup (op =) ABgs) (T, U) $ x
+ end;
+
+ fun mk_rec_o_map_arg rec_arg_T h =
+ let
+ val x_Ts = binder_types rec_arg_T;
+ val m = length x_Ts;
+ val x_names = variant_names m "x";
+ val xs = map2 (curry Free) x_names x_Ts;
+ val xs' = map mk_rec_arg_arg xs;
+ in
+ fold_rev Term.lambda xs (Term.list_comb (h, xs'))
+ end;
+
+ fun mk_rec_o_map_rhs recx =
+ let val args = map2 mk_rec_o_map_arg rec_arg_Ts hs in
+ Term.list_comb (recx, args)
+ end;
+
+ val rec_o_map_rhss = map mk_rec_o_map_rhs recs;
+
+ val rec_o_map_goals =
+ map2 (fold_rev (fold_rev Logic.all) [gs, hs] o HOLogic.mk_Trueprop oo
+ curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
+ val rec_o_map_thms =
+ map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
+ Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
+ mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map)
+ |> Thm.close_derivation)
+ rec_o_map_goals rec_defs ctor_rec_o_maps;
+
+ val size_o_map_conds =
+ if exists (can Logic.dest_implies o Thm.prop_of) nested_size_o_maps then
+ map (HOLogic.mk_Trueprop o mk_inj) live_gs
+ else
+ [];
+
+ val fsizes = map (fn size_constB => Term.list_comb (size_constB, fsB)) size_constsB;
+ val size_o_map_lhss = map2 (curry HOLogic.mk_comp) fsizes gmaps;
+
+ val fgs = map2 (fn fB => fn g as Free (_, Type (_, [A, B])) =>
+ if A = B then fB else HOLogic.mk_comp (fB, g)) fsB gs;
+ val size_o_map_rhss = map (fn c => Term.list_comb (c, fgs)) size_consts;
+
+ val size_o_map_goals =
+ map2 (fold_rev (fold_rev Logic.all) [fsB, gs] o
+ curry Logic.list_implies size_o_map_conds o HOLogic.mk_Trueprop oo
+ curry HOLogic.mk_eq) size_o_map_lhss size_o_map_rhss;
+ val size_o_map_thms =
+ map3 (fn goal => fn size_def => fn rec_o_map =>
+ Goal.prove lthy2 [] [] goal (fn {context = ctxt, ...} =>
+ mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
+ |> Thm.close_derivation)
+ size_o_map_goals size_defs rec_o_map_thms;
+ in
+ pairself (map single) (rec_o_map_thms, size_o_map_thms)
+ end;
+
+ val massage_multi_notes =
+ maps (fn (thmN, thmss, attrs) =>
+ map2 (fn T_name => fn thms =>
+ ((Binding.qualify true (Long_Name.base_name T_name) (Binding.name thmN), attrs),
+ [(thms, [])]))
+ T_names thmss)
+ #> filter_out (null o fst o hd o snd);
+
+ val notes =
+ [(rec_o_mapN, rec_o_map_thmss, []),
+ (sizeN, size_thmss, code_nitpicksimp_simp_attrs),
+ (size_o_mapN, size_o_map_thmss, [])]
+ |> massage_multi_notes;
+ in
+ lthy2
+ |> Local_Theory.notes notes |> snd
+ |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps)
+ |> Local_Theory.declaration {syntax = false, pervasive = true}
+ (fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) =>
+ Symtab.update (T_name, (size_name,
+ pairself (map (Morphism.thm phi)) (size_simps, flat size_o_map_thmss))))
+ T_names size_consts))
+ end;
+
+end;
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Apr 23 17:05:48 2014 +0200
@@ -3,7 +3,7 @@
Author: Andrei Popescu, TU Muenchen
Copyright 2012
-Tactics for the datatype construction.
+Tactics for the new-style datatype construction.
*)
signature BNF_LFP_TACTICS =
--- a/src/HOL/Tools/BNF/bnf_lfp_util.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_util.ML Wed Apr 23 17:05:48 2014 +0200
@@ -3,7 +3,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2012
-Library for the datatype construction.
+Library for the new-style datatype construction.
*)
signature BNF_LFP_UTIL =
--- a/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 23 17:05:48 2014 +0200
@@ -39,6 +39,10 @@
'o -> 'p) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
+ val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+ 'o -> 'p -> 'q) ->
+ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+ 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
@@ -101,6 +105,7 @@
val mk_rel_fun: term -> term -> term
val mk_image: term -> term
val mk_in: term list -> term list -> typ -> term
+ val mk_inj: term -> term
val mk_leq: term -> term -> term
val mk_ordLeq: term -> term -> term
val mk_rel_comp: term * term -> term
@@ -214,6 +219,12 @@
map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s
| map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+fun map16 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
+ | map16 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+ (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) (x16::x16s) =
+ f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 ::
+ map16 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s
+ | map16 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
fun fold_map4 _ [] [] [] [] acc = ([], acc)
| fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
@@ -470,6 +481,12 @@
else HOLogic.mk_UNIV T
end;
+fun mk_inj t =
+ let val T as Type (@{type_name fun}, [domT, _]) = fastype_of t in
+ Const (@{const_name inj_on}, T --> HOLogic.mk_setT domT --> HOLogic.boolT) $ t
+ $ HOLogic.mk_UNIV domT
+ end;
+
fun mk_leq t1 t2 =
Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Apr 23 17:05:48 2014 +0200
@@ -166,7 +166,7 @@
(*|> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)*)
(*|> Sign.restore_naming thy*);
-val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
+fun ctr_sugar_interpretation f = Ctr_Sugar_Interpretation.interpretation (with_repaired_path f);
fun register_ctr_sugar key ctr_sugar =
Local_Theory.declaration {syntax = false, pervasive = true}
--- a/src/HOL/Tools/Function/size.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/Function/size.ML Wed Apr 23 17:05:48 2014 +0200
@@ -6,23 +6,12 @@
signature SIZE =
sig
- val size_thms: theory -> string -> thm list
val setup: theory -> theory
end;
structure Size: SIZE =
struct
-structure Data = Theory_Data
-(
- type T = (string * thm list) Symtab.table;
- val empty = Symtab.empty;
- val extend = I
- fun merge data = Symtab.merge (K true) data;
-);
-
-val lookup_size = Data.get #> Symtab.lookup;
-
fun plus (t1, t2) = Const (@{const_name Groups.plus},
HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
@@ -35,15 +24,13 @@
map (fn U => U --> HOLogic.natT) Ts @ [T] ---> HOLogic.natT),
map (size_of_type' f g h) Ts))
| NONE => NONE))
- | size_of_type f g h (TFree (s, _)) = h s
+ | size_of_type _ _ h (TFree (s, _)) = h s
and size_of_type' f g h T = (case size_of_type f g h T of
NONE => Abs ("x", T, HOLogic.zero)
| SOME t => t);
fun is_poly thy (Datatype_Aux.DtType (name, dts)) =
- (case lookup_size thy name of
- NONE => false
- | SOME _ => exists (is_poly thy) dts)
+ is_some (BNF_LFP_Size.lookup_size_global thy name) andalso exists (is_poly thy) dts
| is_poly _ _ = true;
fun constrs_of thy name =
@@ -59,165 +46,173 @@
val {descr, rec_names, rec_rewrites, induct, ...} = info;
val l = length new_type_names;
val descr' = List.take (descr, l);
- val (rec_names1, rec_names2) = chop l rec_names;
- val recTs = Datatype_Aux.get_rec_types descr;
- val (recTs1, recTs2) = chop l recTs;
- val (_, (_, paramdts, _)) :: _ = descr;
- val paramTs = map (Datatype_Aux.typ_of_dtyp descr) paramdts;
- val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
- map (fn T as TFree (s, _) =>
- let
- val name = "f" ^ unprefix "'" s;
- val U = T --> HOLogic.natT
- in
- (((s, Free (name, U)), U), name)
- end) |> split_list |>> split_list;
- val param_size = AList.lookup op = param_size_fs;
-
- val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
- map_filter (Option.map snd o lookup_size thy) |> flat;
- val extra_size = Option.map fst o lookup_size thy;
-
- val (((size_names, size_fns), def_names), def_names') =
- recTs1 |> map (fn T as Type (s, _) =>
- let
- val s' = Long_Name.base_name s ^ "_size";
- val s'' = Sign.full_bname thy s';
- in
- (s'',
- (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
- map snd param_size_fs),
- (s' ^ "_def", s' ^ "_overloaded_def")))
- end) |> split_list ||>> split_list ||>> split_list;
- val overloaded_size_fns = map HOLogic.size_const recTs1;
-
- (* instantiation for primrec combinator *)
- fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
- let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
- val k = length (filter Datatype_Aux.is_rec_type cargs);
- val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
- if Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
- else
- (if b andalso is_poly thy dt' then
- case size_of_type (K NONE) extra_size size_ofp T of
- NONE => us | SOME sz => sz $ Bound j :: us
- else us, i, j + 1))
- (cargs ~~ cargs' ~~ Ts) ([], 0, k);
- val t =
- if null ts andalso (not b orelse not (exists (is_poly thy) cargs'))
- then HOLogic.zero
- else foldl1 plus (ts @ [HOLogic.Suc_zero])
- in
- fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
- end;
-
- val fs = maps (fn (_, (name, _, constrs)) =>
- map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr;
- val fs' = maps (fn (n, (name, _, constrs)) =>
- map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr;
- val fTs = map fastype_of fs;
-
- val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) =>
- Const (rec_name, fTs @ [T] ---> HOLogic.natT))
- (recTs ~~ rec_names));
-
- fun define_overloaded (def_name, eq) lthy =
- let
- val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
- val (thm, lthy') = lthy
- |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
- |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
- val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
- val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
- in (thm', lthy') end;
-
- val ((size_def_thms, size_def_thms'), thy') =
+ val tycos = map (#1 o snd) descr';
+ in
+ if forall (fn tyco => can (Sign.arity_sorts thy tyco) [HOLogic.class_size]) tycos then
+ (* nothing to do -- the "size" function is already defined *)
thy
- |> Sign.add_consts (map (fn (s, T) =>
- (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
- (size_names ~~ recTs1))
- |> Global_Theory.add_defs false
- (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
- (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
- ||> Class.instantiation
- (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
- ||>> fold_map define_overloaded
- (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
- ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- ||> Local_Theory.exit_global;
-
- val ctxt = Proof_Context.init_global thy';
-
- val simpset1 =
- put_simpset HOL_basic_ss ctxt addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
- size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
- val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
-
- fun mk_unfolded_size_eq tab size_ofp fs (p as (x, T), r) =
- HOLogic.mk_eq (app fs r $ Free p,
- the (size_of_type tab extra_size size_ofp T) $ Free p);
-
- fun prove_unfolded_size_eqs size_ofp fs =
- if null recTs2 then []
- else Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs []
- (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l @{term True} @
- map (mk_unfolded_size_eq (AList.lookup op =
- (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
- (xs ~~ recTs2 ~~ rec_combs2))))
- (fn _ => (Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
-
- val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
- val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';
-
- (* characteristic equations for size functions *)
- fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
+ else
let
- val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
- val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts);
- val ts = map_filter (fn (sT as (s, T), dt) =>
- Option.map (fn sz => sz $ Free sT)
- (if p dt then size_of_type size_of extra_size size_ofp T
- else NONE)) (tnames ~~ Ts ~~ cargs)
- in
- HOLogic.mk_Trueprop (HOLogic.mk_eq
- (size_const $ list_comb (Const (cname, Ts ---> T),
- map2 (curry Free) tnames Ts),
- if null ts then HOLogic.zero
- else foldl1 plus (ts @ [HOLogic.Suc_zero])))
- end;
+ val recTs = Datatype_Aux.get_rec_types descr;
+ val (recTs1, recTs2) = chop l recTs;
+ val (_, (_, paramdts, _)) :: _ = descr;
+ val paramTs = map (Datatype_Aux.typ_of_dtyp descr) paramdts;
+ val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
+ map (fn T as TFree (s, _) =>
+ let
+ val name = "f" ^ unprefix "'" s;
+ val U = T --> HOLogic.natT
+ in
+ (((s, Free (name, U)), U), name)
+ end) |> split_list |>> split_list;
+ val param_size = AList.lookup op = param_size_fs;
+
+ val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
+ map_filter (Option.map (fst o snd) o BNF_LFP_Size.lookup_size_global thy) |> flat;
+ val extra_size = Option.map fst o BNF_LFP_Size.lookup_size_global thy;
+
+ val (((size_names, size_fns), def_names), def_names') =
+ recTs1 |> map (fn T as Type (s, _) =>
+ let
+ val s' = Long_Name.base_name s ^ "_size";
+ val s'' = Sign.full_bname thy s';
+ in
+ (s'',
+ (list_comb (Const (s'', param_size_fTs @ [T] ---> HOLogic.natT),
+ map snd param_size_fs),
+ (s' ^ "_def", s' ^ "_overloaded_def")))
+ end) |> split_list ||>> split_list ||>> split_list;
+ val overloaded_size_fns = map HOLogic.size_const recTs1;
- val simpset2 =
- put_simpset HOL_basic_ss ctxt
- addsimps (rec_rewrites @ size_def_thms @ unfolded_size_eqs1);
- val simpset3 =
- put_simpset HOL_basic_ss ctxt
- addsimps (rec_rewrites @ size_def_thms' @ unfolded_size_eqs2);
+ (* instantiation for primrec combinator *)
+ fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
+ let
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
+ val k = length (filter Datatype_Aux.is_rec_type cargs);
+ val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
+ if Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
+ else
+ (if b andalso is_poly thy dt' then
+ case size_of_type (K NONE) extra_size size_ofp T of
+ NONE => us | SOME sz => sz $ Bound j :: us
+ else us, i, j + 1))
+ (cargs ~~ cargs' ~~ Ts) ([], 0, k);
+ val t =
+ if null ts andalso (not b orelse not (exists (is_poly thy) cargs'))
+ then HOLogic.zero
+ else foldl1 plus (ts @ [HOLogic.Suc_zero])
+ in
+ fold_rev (fn T => fn t' => Abs ("x", T, t')) (Ts @ replicate k HOLogic.natT) t
+ end;
+
+ val fs = maps (fn (_, (name, _, constrs)) =>
+ map (size_of_constr true param_size) (constrs ~~ constrs_of thy name)) descr;
+ val fs' = maps (fn (n, (name, _, constrs)) =>
+ map (size_of_constr (l <= n) (K NONE)) (constrs ~~ constrs_of thy name)) descr;
+ val fTs = map fastype_of fs;
+
+ val (rec_combs1, rec_combs2) = chop l (map (fn (T, rec_name) =>
+ Const (rec_name, fTs @ [T] ---> HOLogic.natT))
+ (recTs ~~ rec_names));
+
+ fun define_overloaded (def_name, eq) lthy =
+ let
+ val (Free (c, _), rhs) = (Logic.dest_equals o Syntax.check_term lthy) eq;
+ val (thm, lthy') = lthy
+ |> Local_Theory.define ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs))
+ |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
+ val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
+ val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
+ in (thm', lthy') end;
- fun prove_size_eqs p size_fns size_ofp simpset =
- maps (fn (((_, (_, _, constrs)), size_const), T) =>
- map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] []
- (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
- size_ofp size_const T constr)
- (fn _ => simp_tac simpset 1))) constrs)
- (descr' ~~ size_fns ~~ recTs1);
+ val ((size_def_thms, size_def_thms'), thy') =
+ thy
+ |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s),
+ param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
+ (size_names ~~ recTs1))
+ |> Global_Theory.add_defs false
+ (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
+ (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
+ ||> Class.instantiation (tycos, map dest_TFree paramTs, [HOLogic.class_size])
+ ||>> fold_map define_overloaded
+ (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
+ ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+ ||> Local_Theory.exit_global;
+
+ val ctxt = Proof_Context.init_global thy';
- val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
- prove_size_eqs Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
+ val simpset1 =
+ put_simpset HOL_basic_ss ctxt addsimps @{thm Nat.add_0} :: @{thm Nat.add_0_right} ::
+ size_def_thms @ size_def_thms' @ rec_rewrites @ extra_rewrites;
+ val xs = map (fn i => "x" ^ string_of_int i) (1 upto length recTs2);
+
+ fun mk_unfolded_size_eq tab size_ofp fs (p as (_, T), r) =
+ HOLogic.mk_eq (app fs r $ Free p,
+ the (size_of_type tab extra_size size_ofp T) $ Free p);
+
+ fun prove_unfolded_size_eqs size_ofp fs =
+ if null recTs2 then []
+ else Datatype_Aux.split_conj_thm (Goal.prove_sorry ctxt xs []
+ (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l @{term True} @
+ map (mk_unfolded_size_eq (AList.lookup op =
+ (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
+ (xs ~~ recTs2 ~~ rec_combs2))))
+ (fn _ => (Datatype_Aux.ind_tac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1));
+
+ val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs;
+ val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs';
- val ([(_, size_thms)], thy'') = thy'
- |> Global_Theory.note_thmss ""
- [((Binding.name "size",
- [Simplifier.simp_add, Nitpick_Simps.add,
- Thm.declaration_attribute (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
- [(size_eqns, [])])];
+ (* characteristic equations for size functions *)
+ fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
+ let
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr) cargs;
+ val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts);
+ val ts = map_filter (fn (sT as (_, T), dt) =>
+ Option.map (fn sz => sz $ Free sT)
+ (if p dt then size_of_type size_of extra_size size_ofp T
+ else NONE)) (tnames ~~ Ts ~~ cargs)
+ in
+ HOLogic.mk_Trueprop (HOLogic.mk_eq
+ (size_const $ list_comb (Const (cname, Ts ---> T),
+ map2 (curry Free) tnames Ts),
+ if null ts then HOLogic.zero
+ else foldl1 plus (ts @ [HOLogic.Suc_zero])))
+ end;
+
+ val simpset2 =
+ put_simpset HOL_basic_ss ctxt
+ addsimps (rec_rewrites @ size_def_thms @ unfolded_size_eqs1);
+ val simpset3 =
+ put_simpset HOL_basic_ss ctxt
+ addsimps (rec_rewrites @ size_def_thms' @ unfolded_size_eqs2);
- in
- Data.map (fold (Symtab.update_new o apsnd (rpair size_thms))
- (new_type_names ~~ size_names)) thy''
+ fun prove_size_eqs p size_fns size_ofp simpset =
+ maps (fn (((_, (_, _, constrs)), size_const), T) =>
+ map (fn constr => Drule.export_without_context (Goal.prove_sorry ctxt [] []
+ (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
+ size_ofp size_const T constr)
+ (fn _ => simp_tac simpset 1))) constrs)
+ (descr' ~~ size_fns ~~ recTs1);
+
+ val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
+ prove_size_eqs Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
+
+ val ([(_, size_thms)], thy'') = thy'
+ |> Global_Theory.note_thmss ""
+ [((Binding.name "size",
+ [Simplifier.simp_add, Nitpick_Simps.add,
+ Thm.declaration_attribute (fn thm =>
+ Context.mapping (Code.add_default_eqn thm) I)]),
+ [(size_eqns, [])])];
+
+ in
+ fold2 (fn new_type_name => fn size_name =>
+ BNF_LFP_Size.register_size_global new_type_name size_name size_thms [])
+ new_type_names size_names thy''
+ end
end;
-fun add_size_thms config (new_type_names as name :: _) thy =
+fun add_size_thms _ (new_type_names as name :: _) thy =
let
val info as {descr, ...} = Datatype_Data.the_info thy name;
val prefix = space_implode "_" (map Long_Name.base_name new_type_names);
@@ -233,8 +228,6 @@
|> Sign.restore_naming thy
end;
-val size_thms = snd oo (the oo lookup_size);
-
val setup = Datatype_Data.interpretation add_size_thms;
end;
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Apr 23 17:05:48 2014 +0200
@@ -18,6 +18,7 @@
open BNF_Util
open BNF_Def
+open BNF_FP_Util
open BNF_FP_Def_Sugar
(* util functions *)
@@ -64,8 +65,10 @@
fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
-fun fp_sugar_only_type_ctr f fp_sugar =
- if is_Type (T_of_bnf (bnf_of_fp_sugar fp_sugar)) then f fp_sugar else I
+fun fp_sugar_only_type_ctr f fp_sugars =
+ (case filter (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugars of
+ [] => I
+ | fp_sugars' => f fp_sugars')
(* relation constraints - bi_total & co. *)
@@ -344,7 +347,7 @@
snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
end
-val _ = Context.>> (Context.map_theory (fp_sugar_interpretation
- (fp_sugar_only_type_ctr (fn fp_sugar => map_local_theory (transfer_fp_sugar_interpretation fp_sugar)))))
+val _ = Context.>> (Context.map_theory (fp_sugar_interpretation (fp_sugar_only_type_ctr
+ (fn fp_sugars => map_local_theory (fold transfer_fp_sugar_interpretation fp_sugars)))))
end
--- a/src/HOL/Transfer.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Transfer.thy Wed Apr 23 17:05:48 2014 +0200
@@ -6,7 +6,7 @@
header {* Generic theorem transfer using relations *}
theory Transfer
-imports Hilbert_Choice Basic_BNFs BNF_FP_Base Metis Option
+imports Hilbert_Choice BNF_FP_Base Metis Option
begin
(* We include Option here altough it's not needed here.
--- a/src/HOL/Wellfounded.thy Wed Apr 23 15:57:06 2014 +0200
+++ b/src/HOL/Wellfounded.thy Wed Apr 23 17:05:48 2014 +0200
@@ -848,20 +848,6 @@
done
-subsection {* size of a datatype value *}
-
-ML_file "Tools/Function/size.ML"
-setup Size.setup
-
-lemma size_bool [code]:
- "size (b\<Colon>bool) = 0" by (cases b) auto
-
-lemma nat_size [simp, code]: "size (n\<Colon>nat) = n"
- by (induct n) simp_all
-
-declare prod.size [no_atp]
-
-
hide_const (open) acc accp
end