--- a/NEWS Mon Mar 03 13:54:47 2014 +0100
+++ b/NEWS Mon Mar 03 15:14:00 2014 +0100
@@ -112,8 +112,7 @@
* Moved new (co)datatype package and its dependencies from "HOL-BNF" to "HOL".
The "bnf", "wrap_free_constructors", "datatype_new", "codatatype",
- "primrec_new", "primcorec", and "primcorecursive" command are now part of
- "Main".
+ "primcorec", and "primcorecursive" commands are now part of "Main".
Theory renamings:
FunDef.thy ~> Fun_Def.thy (and Fun_Def_Base.thy)
Library/Wfrec.thy ~> Wfrec.thy
@@ -146,18 +145,26 @@
Discontinued theories:
BNF/BNF.thy
BNF/Equiv_Relations_More.thy
- Renamed commands:
- datatype_new_compat ~> datatype_compat
- primrec_new ~> primrec
- wrap_free_constructors ~> free_constructors
INCOMPATIBILITY.
+* New datatype package:
+ * "primcorec" is fully implemented.
+ * Renamed commands:
+ datatype_new_compat ~> datatype_compat
+ primrec_new ~> primrec
+ wrap_free_constructors ~> free_constructors
+ INCOMPATIBILITY.
+ * The generated constants "xxx_case" and "xxx_rec" have been renamed
+ "case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
+ INCOMPATIBILITY.
+ * The constant "xxx_(un)fold" and related theorems are no longer generated.
+ Use "xxx_(co)rec" or define "xxx_(un)fold" manually using "prim(co)rec".
+ INCOMPATIBILITY.
+
* Old datatype package:
* The generated theorems "xxx.cases" and "xxx.recs" have been renamed
"xxx.case" and "xxx.rec" (e.g., "sum.cases" -> "sum.case").
INCOMPATIBILITY.
-
-* Old and new (co)datatype packages:
* The generated constants "xxx_case" and "xxx_rec" have been renamed
"case_xxx" and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
INCOMPATIBILITY.
@@ -169,10 +176,12 @@
Option.set ~> set_option
Option.map ~> map_option
option_rel ~> rel_option
+ option_rec ~> case_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
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 Mon Mar 03 13:54:47 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Mar 03 15:14:00 2014 +0100
@@ -619,9 +619,9 @@
\begin{itemize}
\setlength{\itemsep}{0pt}
-\item The old-style, nested-as-mutual induction rule, iterator theorems, and
-recursor theorems are generated under their usual names but with ``@{text
-"compat_"}'' prefixed (e.g., @{text compat_tree.induct}).
+\item The old-style, nested-as-mutual induction rule and recursor theorems are
+generated under their usual names but with ``@{text "compat_"}'' prefixed
+(e.g., @{text compat_tree.induct}).
\item All types through which recursion takes place must be new-style datatypes
or the function type. In principle, it should be possible to support old-style
@@ -665,8 +665,6 @@
@{text t.map_t} \\
Relator: &
@{text t.rel_t} \\
-Iterator: &
- @{text t.fold_t} \\
Recursor: &
@{text t.rec_t}
\end{tabular}
@@ -934,10 +932,6 @@
Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
prove $m$ properties simultaneously.
-\item[@{text "t."}\hthm{fold} @{text "[simp, code]"}\rm:] ~ \\
-@{thm list.fold(1)[no_vars]} \\
-@{thm list.fold(2)[no_vars]}
-
\item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
@{thm list.rec(1)[no_vars]} \\
@{thm list.rec(2)[no_vars]}
@@ -951,7 +945,7 @@
\begin{indentblock}
\begin{description}
-\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\
+\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.map} @{text t.rel_inject}] ~ \\
@{text t.rel_distinct} @{text t.set}
\end{description}
@@ -1402,7 +1396,7 @@
% * induct
% * mutualized
% * without some needless induction hypotheses if not used
-% * fold, rec
+% * rec
% * mutualized
*}
*)
@@ -1627,13 +1621,11 @@
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
-iterator and the recursor are replaced by dual concepts:
+recursor is replaced by a dual concept:
\medskip
\begin{tabular}{@ {}ll@ {}}
-Coiterator: &
- @{text unfold_t} \\
Corecursor: &
@{text corec_t}
\end{tabular}
@@ -1696,34 +1688,18 @@
Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
used to prove $m$ properties simultaneously.
-\item[@{text "t."}\hthm{unfold}\rm:] ~ \\
-@{thm llist.unfold(1)[no_vars]} \\
-@{thm llist.unfold(2)[no_vars]}
-
\item[@{text "t."}\hthm{corec}\rm:] ~ \\
@{thm llist.corec(1)[no_vars]} \\
@{thm llist.corec(2)[no_vars]}
-\item[@{text "t."}\hthm{disc\_unfold}\rm:] ~ \\
-@{thm llist.disc_unfold(1)[no_vars]} \\
-@{thm llist.disc_unfold(2)[no_vars]}
-
\item[@{text "t."}\hthm{disc\_corec}\rm:] ~ \\
@{thm llist.disc_corec(1)[no_vars]} \\
@{thm llist.disc_corec(2)[no_vars]}
-\item[@{text "t."}\hthm{disc\_unfold\_iff} @{text "[simp]"}\rm:] ~ \\
-@{thm llist.disc_unfold_iff(1)[no_vars]} \\
-@{thm llist.disc_unfold_iff(2)[no_vars]}
-
\item[@{text "t."}\hthm{disc\_corec\_iff} @{text "[simp]"}\rm:] ~ \\
@{thm llist.disc_corec_iff(1)[no_vars]} \\
@{thm llist.disc_corec_iff(2)[no_vars]}
-\item[@{text "t."}\hthm{sel\_unfold} @{text "[simp]"}\rm:] ~ \\
-@{thm llist.sel_unfold(1)[no_vars]} \\
-@{thm llist.sel_unfold(2)[no_vars]}
-
\item[@{text "t."}\hthm{sel\_corec} @{text "[simp]"}\rm:] ~ \\
@{thm llist.sel_corec(1)[no_vars]} \\
@{thm llist.sel_corec(2)[no_vars]}
@@ -1738,8 +1714,7 @@
\begin{description}
\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.disc_corec} @{text t.disc_corec_iff}] ~ \\
-@{text t.sel_corec} @{text t.disc_unfold} @{text t.disc_unfold_iff} @{text t.sel_unfold} @{text t.map} \\
-@{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
+@{text t.sel_corec} @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
\end{description}
\end{indentblock}
--- a/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_Cardinal_Arithmetic.thy Mon Mar 03 15:14:00 2014 +0100
@@ -199,7 +199,7 @@
"Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)"
unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of)
-lemma Cinfinite_csum_strong:
+lemma Cinfinite_csum_weak:
"\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)"
by (erule Cinfinite_csum1)
@@ -335,6 +335,9 @@
lemma cprod_mono2: "p2 \<le>o r2 \<Longrightarrow> q *c p2 \<le>o q *c r2"
by (simp only: cprod_def ordLeq_Times_mono2)
+lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
+by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
+
lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2"
unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI)
@@ -347,6 +350,15 @@
lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)"
by (blast intro: cinfinite_cprod2 Card_order_cprod)
+lemma cprod_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c r2"
+unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono)
+
+lemma cprod_cong1: "\<lbrakk>p1 =o r1\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c p2"
+unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono1)
+
+lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
+unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono2)
+
lemma cprod_com: "p1 *c p2 =o p2 *c p1"
by (simp only: cprod_def card_of_Times_commute)
@@ -514,6 +526,9 @@
unfolding cinfinite_def cprod_def
by (rule Card_order_Times_infinite[THEN conjunct1]) (blast intro: czeroI)+
+lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
+using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
+
lemma cexp_cprod_ordLeq:
assumes r1: "Card_order r1" and r2: "Cinfinite r2"
and r3: "Cnotzero r3" "r3 \<le>o r2"
--- a/src/HOL/BNF_Comp.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_Comp.thy Mon Mar 03 15:14:00 2014 +0100
@@ -128,7 +128,26 @@
end
+definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp = (\<lambda>x. x)"
+
+lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
+ unfolding id_bnf_comp_def by unfold_locales auto
+
+lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
+apply (erule ordIso_transitive)
+apply (frule csum_absorb2')
+apply (erule ordLeq_refl)
+by simp
+
+lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
+apply (erule ordIso_transitive)
+apply (rule cprod_infinite)
+by simp
+
ML_file "Tools/BNF/bnf_comp_tactics.ML"
ML_file "Tools/BNF/bnf_comp.ML"
+hide_const (open) id_bnf_comp
+hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
+
end
--- a/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_Examples/Derivation_Trees/DTree.thy Mon Mar 03 15:14:00 2014 +0100
@@ -20,7 +20,7 @@
definition "Node n as \<equiv> NNode n (the_inv fset as)"
definition "cont \<equiv> fset o ccont"
-definition "unfold rt ct \<equiv> unfold_dtree rt (the_inv fset o ct)"
+definition "unfold rt ct \<equiv> corec_dtree rt (the_inv fset o image (sum_map id Inr) o ct)"
definition "corec rt ct \<equiv> corec_dtree rt (the_inv fset o ct)"
lemma finite_cont[simp]: "finite (cont tr)"
@@ -75,18 +75,16 @@
lemma unfold:
"root (unfold rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
-using dtree.sel_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def
-apply - apply metis
+using dtree.sel_corec[of rt "the_inv fset o image (sum_map id Inr) o ct" b] unfolding unfold_def
+apply blast
unfolding cont_def comp_def
-by simp
+by (simp add: case_sum_o_inj sum_map.compositionality image_image)
lemma corec:
"root (corec rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
using dtree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
-apply -
-apply simp
unfolding cont_def comp_def id_def
-by simp
+by simp_all
end
--- a/src/HOL/BNF_Examples/Misc_Primcorec.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_Examples/Misc_Primcorec.thy Mon Mar 03 15:14:00 2014 +0100
@@ -88,26 +88,26 @@
id_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
id_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
where
- "id_tree t = (case t of BRTree a ts ts' => BRTree a (id_trees1 ts) (id_trees2 ts'))" |
+ "id_tree t = (case t of BRTree a ts ts' \<Rightarrow> BRTree a (id_trees1 ts) (id_trees2 ts'))" |
"id_trees1 ts = (case ts of
- MyNil => MyNil
- | MyCons t ts => MyCons (id_tree t) (id_trees1 ts))" |
+ MyNil \<Rightarrow> MyNil
+ | MyCons t ts \<Rightarrow> MyCons (id_tree t) (id_trees1 ts))" |
"id_trees2 ts = (case ts of
- MyNil => MyNil
- | MyCons t ts => MyCons (id_tree t) (id_trees2 ts))"
+ MyNil \<Rightarrow> MyNil
+ | MyCons t ts \<Rightarrow> MyCons (id_tree t) (id_trees2 ts))"
primcorec
trunc_tree :: "'a bin_rose_tree \<Rightarrow> 'a bin_rose_tree" and
trunc_trees1 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist" and
trunc_trees2 :: "'a bin_rose_tree mylist \<Rightarrow> 'a bin_rose_tree mylist"
where
- "trunc_tree t = (case t of BRTree a ts ts' => BRTree a (trunc_trees1 ts) (trunc_trees2 ts'))" |
+ "trunc_tree t = (case t of BRTree a ts ts' \<Rightarrow> BRTree a (trunc_trees1 ts) (trunc_trees2 ts'))" |
"trunc_trees1 ts = (case ts of
- MyNil => MyNil
- | MyCons t _ => MyCons (trunc_tree t) MyNil)" |
+ MyNil \<Rightarrow> MyNil
+ | MyCons t _ \<Rightarrow> MyCons (trunc_tree t) MyNil)" |
"trunc_trees2 ts = (case ts of
- MyNil => MyNil
- | MyCons t ts => MyCons (trunc_tree t) MyNil)"
+ MyNil \<Rightarrow> MyNil
+ | MyCons t ts \<Rightarrow> MyCons (trunc_tree t) MyNil)"
primcorec
freeze_exp :: "('b \<Rightarrow> 'a) \<Rightarrow> ('a, 'b) exp \<Rightarrow> ('a, 'b) exp" and
--- a/src/HOL/BNF_Examples/Stream.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_Examples/Stream.thy Mon Mar 03 15:14:00 2014 +0100
@@ -33,16 +33,16 @@
assume "a \<in> set1_pre_stream (dtor_stream s)"
then have "a = shd s"
by (cases "dtor_stream s")
- (auto simp: shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def
- Abs_stream_pre_stream_inverse Abs_stream_pre_stream_inject split: stream.splits)
+ (auto simp: BNF_Comp.id_bnf_comp_def shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def
+ split: stream.splits)
with Base show "P a s" by simp
next
fix a :: 'a and s' :: "'a stream" and s :: "'a stream"
assume "s' \<in> set2_pre_stream (dtor_stream s)" and prems: "a \<in> sset s'" "P a s'"
then have "s' = stl s"
by (cases "dtor_stream s")
- (auto simp: stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def
- Abs_stream_pre_stream_inverse Abs_stream_pre_stream_inject split: stream.splits)
+ (auto simp: BNF_Comp.id_bnf_comp_def stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def
+ split: stream.splits)
with Step prems show "P a s" by simp
qed
--- a/src/HOL/BNF_FP_Base.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_FP_Base.thy Mon Mar 03 15:14:00 2014 +0100
@@ -177,6 +177,9 @@
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])
+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"
unfolding fun_eq_iff vimage2p_def o_apply by simp
--- a/src/HOL/BNF_LFP.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Mon Mar 03 15:14:00 2014 +0100
@@ -251,10 +251,10 @@
unfolding vimage2p_def by auto
lemma id_transfer: "fun_rel A A id id"
-unfolding fun_rel_def by simp
+ unfolding fun_rel_def by simp
lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
- by simp
+ by (rule ssubst)
ML_file "Tools/BNF/bnf_lfp_util.ML"
ML_file "Tools/BNF/bnf_lfp_tactics.ML"
--- a/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Cardinals/Cardinal_Arithmetic.thy Mon Mar 03 15:14:00 2014 +0100
@@ -66,18 +66,10 @@
unfolding cprod_def cone_def Field_card_of
by (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton])
-lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
-by (simp only: cprod_def ordIso_Times_cong2)
lemma ordLeq_cprod1: "\<lbrakk>Card_order p1; Cnotzero p2\<rbrakk> \<Longrightarrow> p1 \<le>o p1 *c p2"
unfolding cprod_def by (metis Card_order_Times1 czeroI)
-lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r"
-using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast
-
-lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2"
- by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2])
-
subsection {* Exponentiation *}
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy Mon Mar 03 15:14:00 2014 +0100
@@ -585,20 +585,6 @@
nitpick [expect = genuine]
oops
-lemma "rec_option n s None = n"
-nitpick [expect = none]
-apply simp
-done
-
-lemma "rec_option n s (Some x) = s x"
-nitpick [expect = none]
-apply simp
-done
-
-lemma "P (rec_option n s x)"
-nitpick [expect = genuine]
-oops
-
lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
nitpick [expect = genuine]
oops
--- a/src/HOL/Option.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Option.thy Mon Mar 03 15:14:00 2014 +0100
@@ -28,7 +28,6 @@
setup {* Sign.mandatory_path "option" *}
lemmas inducts = option.induct
-lemmas recs = option.rec
lemmas cases = option.case
setup {* Sign.parent_path *}
--- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 03 15:14:00 2014 +0100
@@ -6,6 +6,8 @@
Composition of bounded natural functors.
*)
+val inline_ref = Unsynchronized.ref true;
+
signature BNF_COMP =
sig
val ID_bnf: BNF_Def.bnf
@@ -19,7 +21,7 @@
exception BAD_DEAD of typ * typ
- val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
+ val bnf_of_typ: BNF_Def.inline_policy -> (binding -> binding) ->
((string * sort) list list -> (string * sort) list) -> (string * sort) list ->
(string * sort) list -> typ -> (comp_cache * unfold_set) * Proof.context ->
(BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * Proof.context)
@@ -95,6 +97,10 @@
val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
in Envir.expand_term get end;
+fun is_sum_prod_natLeq (Const (@{const_name csum}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
+ | is_sum_prod_natLeq (Const (@{const_name cprod}, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
+ | is_sum_prod_natLeq t = t aconv @{term natLeq};
+
fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) =
let
val olive = live_of_bnf outer;
@@ -170,6 +176,20 @@
(*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd;
+ val (bd', bd_ordIso_natLeq_thm_opt) =
+ if is_sum_prod_natLeq bd then
+ let
+ val bd' = @{term natLeq};
+ val bd_bd' = HOLogic.mk_prod (bd, bd');
+ val ordIso = Const (@{const_name ordIso}, HOLogic.mk_setT (fastype_of bd_bd'));
+ val goal = HOLogic.mk_Trueprop (HOLogic.mk_mem (bd_bd', ordIso));
+ in
+ (bd', SOME (Goal.prove_sorry lthy [] [] goal (K bd_ordIso_natLeq_tac)
+ |> Thm.close_derivation))
+ end
+ else
+ (bd, NONE);
+
fun map_id0_tac _ =
mk_comp_map_id0_tac (map_id0_of_bnf outer) (map_cong0_of_bnf outer)
(map map_id0_of_bnf inners);
@@ -220,7 +240,7 @@
map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
in
map2 (fn set_alt => fn single_set_bds => fn ctxt =>
- mk_comp_set_bd_tac ctxt set_alt single_set_bds)
+ mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_thm_opt set_alt single_set_bds)
set_alt_thms single_set_bd_thmss
end;
@@ -278,7 +298,7 @@
val (bnf', lthy') =
bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
- Binding.empty [] ((((((b, CCA), mapx), sets), bd), wits), SOME rel) lthy;
+ Binding.empty [] ((((((b, CCA), mapx), sets), bd'), wits), SOME rel) lthy;
in
(bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
end;
@@ -610,18 +630,44 @@
let val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) [];
in Term.typ_subst_TVars rho absT end;
-fun mk_repT (t as Type (C, Ts)) repT (u as Type (C', Us)) =
- if C = C' andalso length Ts = length Us then Term.typ_subst_atomic (Ts ~~ Us) repT
- else raise Term.TYPE ("mk_repT", [t, repT, u], [])
- | mk_repT t repT u = raise Term.TYPE ("mk_repT", [t, repT, u], []);
+fun mk_repT absT repT absU =
+ if absT = repT then absU
+ else
+ (case (absT, absU) of
+ (Type (C, Ts), Type (C', Us)) =>
+ if C = C' then Term.typ_subst_atomic (Ts ~~ Us) repT
+ else raise Term.TYPE ("mk_repT", [absT, repT, absT], [])
+ | _ => raise Term.TYPE ("mk_repT", [absT, repT, absT], []));
-fun mk_abs_or_rep getT (Type (_, Us)) abs =
- let val Ts = snd (dest_Type (getT (fastype_of abs)))
- in Term.subst_atomic_types (Ts ~~ Us) abs end;
+fun mk_abs_or_rep _ absU (Const (@{const_name id_bnf_comp}, _)) =
+ Const (@{const_name id_bnf_comp}, absU --> absU)
+ | mk_abs_or_rep getT (Type (_, Us)) abs =
+ let val Ts = snd (dest_Type (getT (fastype_of abs)))
+ in Term.subst_atomic_types (Ts ~~ Us) abs end;
val mk_abs = mk_abs_or_rep range_type;
val mk_rep = mk_abs_or_rep domain_type;
+val smart_max_inline_type_size = 5; (*FUDGE*)
+
+fun maybe_typedef (b, As, mx) set opt_morphs tac =
+ let
+ val repT = HOLogic.dest_setT (fastype_of set);
+ val inline = Term.size_of_typ repT <= smart_max_inline_type_size;
+ in
+ if inline then
+ pair (repT,
+ (@{const_name id_bnf_comp}, @{const_name id_bnf_comp},
+ @{thm type_definition_id_bnf_comp_UNIV},
+ @{thm type_definition.Abs_inverse[OF type_definition_id_bnf_comp_UNIV]},
+ @{thm type_definition.Abs_inject[OF type_definition_id_bnf_comp_UNIV]}))
+ else
+ typedef (b, As, mx) set opt_morphs tac
+ #>> (fn (T_name, ({Rep_name, Abs_name, ...},
+ {type_definition, Abs_inverse, Abs_inject, ...}) : Typedef.info) =>
+ (Type (T_name, map TFree As), (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject)))
+ end;
+
fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy =
let
val live = live_of_bnf bnf;
@@ -652,25 +698,23 @@
fun unfold_all ctxt = unfold_sets ctxt o unfold_maps ctxt o unfold_rels ctxt;
val repTA = mk_T_of_bnf Ds As bnf;
- val repTB = mk_T_of_bnf Ds Bs bnf;
val T_bind = qualify b;
val TA_params = Term.add_tfreesT repTA [];
- val TB_params = Term.add_tfreesT repTB [];
- val ((T_name, (T_glob_info, T_loc_info)), lthy) =
- typedef (T_bind, TA_params, NoSyn)
+ val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject)), lthy) =
+ maybe_typedef (T_bind, TA_params, NoSyn)
(HOLogic.mk_UNIV repTA) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
- val TA = Type (T_name, map TFree TA_params);
- val TB = Type (T_name, map TFree TB_params);
- val RepA = Const (#Rep_name T_glob_info, TA --> repTA);
- val RepB = Const (#Rep_name T_glob_info, TB --> repTB);
- val AbsA = Const (#Abs_name T_glob_info, repTA --> TA);
- val AbsB = Const (#Abs_name T_glob_info, repTB --> TB);
- val typedef_thm = #type_definition T_loc_info;
- val Abs_inject' = #Abs_inject T_loc_info OF @{thms UNIV_I UNIV_I};
- val Abs_inverse' = #Abs_inverse T_loc_info OF @{thms UNIV_I};
+
+ val repTB = mk_T_of_bnf Ds Bs bnf;
+ val TB = Term.typ_subst_atomic (As ~~ Bs) TA;
+ val RepA = Const (Rep_name, TA --> repTA);
+ val RepB = Const (Rep_name, TB --> repTB);
+ val AbsA = Const (Abs_name, repTA --> TA);
+ val AbsB = Const (Abs_name, repTB --> TB);
+ val Abs_inject' = Abs_inject OF @{thms UNIV_I UNIV_I};
+ val Abs_inverse' = Abs_inverse OF @{thms UNIV_I};
val absT_info = {absT = TA, repT = repTA, abs = AbsA, rep = RepA, abs_inject = Abs_inject',
- abs_inverse = Abs_inverse', type_definition = typedef_thm};
+ abs_inverse = Abs_inverse', type_definition = type_definition};
val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB,
Term.list_comb (expand_maps (mk_map_of_bnf Ds As Bs bnf), fs)), RepA));
@@ -704,15 +748,16 @@
(@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1;
fun map_id0_tac ctxt =
- rtac (@{thm type_copy_map_id0} OF [typedef_thm, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1;
+ rtac (@{thm type_copy_map_id0} OF [type_definition, unfold_maps ctxt (map_id0_of_bnf bnf)]) 1;
fun map_comp0_tac ctxt =
- rtac (@{thm type_copy_map_comp0} OF [typedef_thm, unfold_maps ctxt (map_comp0_of_bnf bnf)]) 1;
+ rtac (@{thm type_copy_map_comp0} OF
+ [type_definition, unfold_maps ctxt (map_comp0_of_bnf bnf)]) 1;
fun map_cong0_tac ctxt =
EVERY' (rtac @{thm type_copy_map_cong0} :: rtac (unfold_all ctxt (map_cong0_of_bnf bnf)) ::
map (fn i => EVERY' [select_prem_tac live (dtac meta_spec) i, etac meta_mp,
etac (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1;
fun set_map0_tac thm ctxt =
- rtac (@{thm type_copy_set_map0} OF [typedef_thm, unfold_all ctxt thm]) 1;
+ rtac (@{thm type_copy_set_map0} OF [type_definition, unfold_all ctxt thm]) 1;
val set_bd_tacs = map (fn thm => fn ctxt => rtac (@{thm ordLeq_ordIso_trans} OF
[unfold_sets ctxt thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1)
(set_bd_of_bnf bnf);
@@ -720,8 +765,9 @@
rtac (unfold_rels ctxt (le_rel_OO_of_bnf bnf) RS @{thm vimage2p_relcompp_mono}) 1;
fun rel_OO_Grp_tac ctxt =
(rtac (unfold_all ctxt (rel_OO_Grp_of_bnf bnf) RS @{thm vimage2p_cong} RS trans) THEN'
- SELECT_GOAL (unfold_thms_tac ctxt [o_apply, typedef_thm RS @{thm type_copy_vimage2p_Grp_Rep},
- typedef_thm RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1;
+ SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
+ type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
+ type_definition RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1;
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac
(map set_map0_tac (set_map0_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1))
@@ -732,7 +778,7 @@
(AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1))))
(mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
- fun wit_tac ctxt = ALLGOALS (dtac (typedef_thm RS @{thm type_copy_wit})) THEN
+ fun wit_tac ctxt = ALLGOALS (dtac (type_definition RS @{thm type_copy_wit})) THEN
mk_simple_wit_tac (map (unfold_all ctxt) (wit_thms_of_bnf bnf));
val (bnf', lthy') =
--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML Mon Mar 03 15:14:00 2014 +0100
@@ -15,7 +15,7 @@
val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
- val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
+ val mk_comp_set_bd_tac: Proof.context -> thm option -> thm -> thm list -> tactic
val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic
val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
@@ -31,6 +31,7 @@
val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic
val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
val mk_simple_wit_tac: thm list -> tactic
+ val bd_ordIso_natLeq_tac: tactic
end;
structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
@@ -45,7 +46,6 @@
val trans_o_apply = @{thm trans[OF o_apply]};
-
(* Composition *)
fun mk_comp_set_alt_tac ctxt collect_set_map =
@@ -101,6 +101,7 @@
end;
fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order =
+ rtac @{thm natLeq_card_order} 1 ORELSE
let
val (card_orders, last_card_order) = split_last Fbd_card_orders;
fun gen_before thm = rtac @{thm card_order_csum} THEN' rtac thm;
@@ -111,14 +112,15 @@
end;
fun mk_comp_bd_cinfinite_tac Fbd_cinfinite Gbd_cinfinite =
- (rtac @{thm cinfinite_cprod} THEN'
+ (rtac @{thm natLeq_cinfinite} ORELSE'
+ rtac @{thm cinfinite_cprod} THEN'
((K (TRY ((rtac @{thm cinfinite_csum} THEN' rtac disjI1) 1)) THEN'
((rtac @{thm cinfinite_csum} THEN' rtac disjI1 THEN' rtac Fbd_cinfinite) ORELSE'
rtac Fbd_cinfinite)) ORELSE'
rtac Fbd_cinfinite) THEN'
rtac Gbd_cinfinite) 1;
-fun mk_comp_set_bd_tac ctxt comp_set_alt Gset_Fset_bds =
+fun mk_comp_set_bd_tac ctxt bd_ordIso_natLeq_opt comp_set_alt Gset_Fset_bds =
let
val (bds, last_bd) = split_last Gset_Fset_bds;
fun gen_before bd =
@@ -127,6 +129,9 @@
rtac bd;
fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
in
+ (case bd_ordIso_natLeq_opt of
+ SOME thm => rtac (thm RS rotate_prems 1 @{thm ordLeq_ordIso_trans}) 1
+ | NONE => all_tac) THEN
unfold_thms_tac ctxt [comp_set_alt] THEN
rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
@@ -168,7 +173,6 @@
(etac FalseE ORELSE' atac))) 1);
-
(* Kill operation *)
fun mk_kill_map_cong0_tac ctxt n m map_cong0 =
@@ -187,7 +191,6 @@
REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1));
-
(* Lift operation *)
val empty_natural_tac = rtac @{thm empty_natural} 1;
@@ -206,7 +209,6 @@
REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1));
-
(* Permute operation *)
fun mk_permute_in_alt_tac src dest =
@@ -214,6 +216,9 @@
mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
dest src) 1;
+
+(* Miscellaneous *)
+
fun mk_le_rel_OO_tac outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
EVERY' (map rtac (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1;
@@ -222,4 +227,13 @@
fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
+val csum_thms =
+ @{thms csum_cong1 csum_cong2 csum_cong csum_dup[OF natLeq_cinfinite natLeq_Card_order]};
+val cprod_thms =
+ @{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]};
+
+val bd_ordIso_natLeq_tac =
+ HEADGOAL (REPEAT_DETERM o resolve_tac
+ (@{thm ordIso_refl[OF natLeq_Card_order]} :: csum_thms @ cprod_thms));
+
end;
--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Mar 03 15:14:00 2014 +0100
@@ -90,7 +90,7 @@
val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
- datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
+ datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
datatype fact_policy = Dont_Note | Note_Some | Note_All
val bnf_note_all: bool Config.T
@@ -100,7 +100,7 @@
Proof.context
val print_bnfs: Proof.context -> unit
- val prepare_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
+ val prepare_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
(Proof.context -> 'a -> typ) -> (Proof.context -> 'b -> term) -> typ list option ->
binding -> binding -> binding list ->
(((((binding * 'a) * 'b) * 'b list) * 'b) * 'b list) * 'b option -> Proof.context ->
@@ -109,7 +109,7 @@
((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
local_theory * thm list
- val define_bnf_consts: const_policy -> fact_policy -> typ list option ->
+ val define_bnf_consts: inline_policy -> fact_policy -> typ list option ->
binding -> binding -> binding list ->
(((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
((typ list * typ list * typ list * typ) *
@@ -121,7 +121,7 @@
(typ list -> typ list -> typ list -> term) *
(typ list -> typ list -> typ list -> term))) * local_theory
- val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
+ val bnf_def: inline_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
(Proof.context -> tactic) list ->
(Proof.context -> tactic) -> typ list option -> binding ->
binding -> binding list ->
@@ -583,7 +583,7 @@
val rel_comppN = "rel_compp";
val rel_compp_GrpN = "rel_compp_Grp";
-datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
+datatype inline_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
datatype fact_policy = Dont_Note | Note_Some | Note_All;
@@ -592,7 +592,7 @@
fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
-val smart_max_inline_size = 25; (*FUDGE*)
+val smart_max_inline_term_size = 25; (*FUDGE*)
fun note_bnf_thms fact_policy qualify' bnf_b bnf =
let
@@ -676,7 +676,7 @@
(case const_policy of
Dont_Inline => false
| Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
- | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_size
+ | Smart_Inline => Term.size_of_term rhs <= smart_max_inline_term_size
| Do_Inline => true)
in
if inline then
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 03 15:14:00 2014 +0100
@@ -20,13 +20,13 @@
ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
- co_iters: term list,
+ co_rec: term,
maps: thm list,
common_co_inducts: thm list,
co_inducts: thm list,
- co_iter_thmss: thm list list,
- disc_co_iterss: thm list list,
- sel_co_itersss: thm list list list};
+ co_rec_thms: thm list,
+ disc_co_recs: thm list,
+ sel_co_recss: thm list list};
val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
@@ -41,55 +41,52 @@
val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
type lfp_sugar_thms =
- (thm list * thm * Args.src list) * (thm list list * thm list list * Args.src list)
+ (thm list * thm * Args.src list) * (thm list list * Args.src list)
val morph_lfp_sugar_thms: morphism -> lfp_sugar_thms -> lfp_sugar_thms
val transfer_lfp_sugar_thms: Proof.context -> lfp_sugar_thms -> lfp_sugar_thms
type gfp_sugar_thms =
((thm list * thm) list * Args.src list)
- * (thm list list * thm list list * Args.src list)
- * (thm list list * thm list list * Args.src list)
- * (thm list list * thm list list * Args.src list)
- * (thm list list list * thm list list list * Args.src list)
+ * (thm list list * Args.src list)
+ * (thm list list * Args.src list)
+ * (thm list list * Args.src list)
+ * (thm list list list * Args.src list)
val morph_gfp_sugar_thms: morphism -> gfp_sugar_thms -> gfp_sugar_thms
val transfer_gfp_sugar_thms: Proof.context -> gfp_sugar_thms -> gfp_sugar_thms
- val mk_co_iters_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
- typ list -> typ list -> int list -> int list list -> term list list -> Proof.context ->
- (term list list
- * (typ list list * typ list list list list * term list list
- * term list list list list) list option
- * (string * term list * term list list
- * ((term list list * term list list list) * typ list) list) option)
- * Proof.context
+ val mk_co_recs_prelims: BNF_Util.fp_kind -> typ list list list -> typ list -> typ list ->
+ typ list -> typ list -> int list -> int list list -> term list -> Proof.context ->
+ (term list
+ * (typ list list * typ list list list list * term list list * term list list list list) option
+ * (string * term list * term list list
+ * ((term list list * term list list list) * typ list)) option)
+ * Proof.context
val repair_nullary_single_ctr: typ list list -> typ list list
- val mk_coiter_p_pred_types: typ list -> int list -> typ list list
- val mk_coiter_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list ->
+ val mk_corec_p_pred_types: typ list -> int list -> typ list list
+ val mk_corec_fun_arg_types: typ list list list -> typ list -> typ list -> typ list -> int list ->
int list list -> term ->
typ list list
* (typ list list list list * typ list list list * typ list list list list * typ list)
- val define_iters: string list ->
- (typ list list * typ list list list list * term list list * term list list list list) list ->
- (string -> binding) -> typ list -> typ list -> term list -> term list -> Proof.context ->
- (term list * thm list) * Proof.context
- val define_coiters: string list -> string * term list * term list list
- * ((term list list * term list list list) * typ list) list ->
- (string -> binding) -> typ list -> typ list -> term list -> term list -> Proof.context ->
- (term list * thm list) * Proof.context
- val derive_induct_iters_thms_for_types: BNF_Def.bnf list ->
- (typ list list * typ list list list list * term list list * term list list list list) list ->
- thm -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
- typ list -> typ list list list -> thm list -> thm list -> thm list -> term list list ->
- thm list list -> term list list -> thm list list -> local_theory -> lfp_sugar_thms
- val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
- string * term list * term list list * ((term list list * term list list list)
- * typ list) list ->
- thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
+ val define_rec:
+ (typ list list * typ list list list list * term list list * term list list list list) option ->
+ (string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context ->
+ (term * thm) * Proof.context
+ val define_corec: 'a * term list * term list list
+ * ((term list list * term list list list) * typ list) -> (string -> binding) -> 'b list ->
+ typ list -> term list -> term -> Proof.context -> (term * thm) * local_theory
+ val derive_induct_recs_thms_for_types: BNF_Def.bnf list ->
+ ('a * typ list list list list * term list list * 'b) option -> thm -> thm list ->
+ BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list -> typ list ->
+ typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list ->
+ term list -> thm list -> Proof.context -> lfp_sugar_thms
+ val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list ->
+ string * term list * term list list * ((term list list * term list list list) * typ list) ->
+ thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list ->
typ list -> typ list list list -> int list list -> int list list -> int list -> thm list ->
- thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list list ->
- thm list list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
+ thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list ->
+ thm list -> (thm list -> thm list) -> local_theory -> gfp_sugar_thms
type co_datatype_spec =
((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
@@ -134,17 +131,17 @@
ctrXs_Tss: typ list list,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
- co_iters: term list,
+ co_rec: term,
maps: thm list,
common_co_inducts: thm list,
co_inducts: thm list,
- co_iter_thmss: thm list list,
- disc_co_iterss: thm list list,
- sel_co_itersss: thm list list list};
+ co_rec_thms: thm list,
+ disc_co_recs: thm list,
+ sel_co_recss: thm list 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_iters, maps, common_co_inducts, co_inducts,
- co_iter_thmss, disc_co_iterss, sel_co_itersss} : fp_sugar) =
+ 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} : fp_sugar) =
{T = Morphism.typ phi T,
X = Morphism.typ phi X,
fp = fp,
@@ -157,13 +154,13 @@
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_iters = map (Morphism.term phi) co_iters,
+ 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_iter_thmss = map (map (Morphism.thm phi)) co_iter_thmss,
- disc_co_iterss = map (map (Morphism.thm phi)) disc_co_iterss,
- sel_co_itersss = map (map (map (Morphism.thm phi))) sel_co_itersss};
+ 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};
val transfer_fp_sugar =
morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
@@ -193,17 +190,17 @@
(fn phi => Data.map (Symtab.update (key, morph_fp_sugar phi fp_sugar)));
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_iterss mapss common_co_inducts co_inductss co_iter_thmsss
- disc_co_itersss sel_co_iterssss lthy =
+ ctrXs_Tsss ctr_defss ctr_sugars co_recs mapss common_co_inducts co_inductss co_rec_thmss
+ disc_co_recss sel_co_recsss 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_iters = nth co_iterss kk, maps = nth mapss 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_iter_thmss = nth co_iter_thmsss kk, disc_co_iterss = nth disc_co_itersss kk,
- sel_co_itersss = nth sel_co_iterssss 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}
lthy)) Ts
|> snd;
@@ -231,11 +228,11 @@
val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs));
-fun flat_corec_predss_getterss qss fss = maps (op @) (qss ~~ fss);
+fun flat_corec_predss_getterss qss gss = maps (op @) (qss ~~ gss);
-fun flat_corec_preds_predsss_gettersss [] [qss] [fss] = flat_corec_predss_getterss qss fss
- | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
- p :: flat_corec_predss_getterss qss fss @ flat_corec_preds_predsss_gettersss ps qsss fsss;
+fun flat_corec_preds_predsss_gettersss [] [qss] [gss] = flat_corec_predss_getterss qss gss
+ | flat_corec_preds_predsss_gettersss (p :: ps) (qss :: qsss) (gss :: gsss) =
+ p :: flat_corec_predss_getterss qss gss @ flat_corec_preds_predsss_gettersss ps qsss gsss;
fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1));
@@ -257,7 +254,7 @@
val mk_ctor = mk_ctor_or_dtor range_type;
val mk_dtor = mk_ctor_or_dtor domain_type;
-fun mk_co_iters thy fp fpTs Cs ts0 =
+fun mk_xtor_co_recs thy fp fpTs Cs ts0 =
let
val nn = length fpTs;
val (fpTs0, Cs0) =
@@ -268,7 +265,6 @@
map (Term.subst_TVars rho) ts0
end;
-
fun unzip_recT (Type (@{type_name prod}, _)) T = [T]
| unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts
| unzip_recT _ T = [T];
@@ -320,11 +316,11 @@
fun indexify proj xs f p = f (find_index (curry (op =) (proj p)) xs) p;
type lfp_sugar_thms =
- (thm list * thm * Args.src list) * (thm list list * thm list list * Args.src list)
+ (thm list * thm * Args.src list) * (thm list list * Args.src list);
-fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (foldss, recss, iter_attrs)) =
+fun morph_lfp_sugar_thms phi ((inducts, induct, induct_attrs), (recss, rec_attrs)) =
((map (Morphism.thm phi) inducts, Morphism.thm phi induct, induct_attrs),
- (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs))
+ (map (map (Morphism.thm phi)) recss, rec_attrs))
: lfp_sugar_thms;
val transfer_lfp_sugar_thms =
@@ -332,233 +328,177 @@
type gfp_sugar_thms =
((thm list * thm) list * Args.src list)
- * (thm list list * thm list list * Args.src list)
- * (thm list list * thm list list * Args.src list)
- * (thm list list * thm list list * Args.src list)
- * (thm list list list * thm list list list * Args.src list);
+ * (thm list list * Args.src list)
+ * (thm list list * Args.src list)
+ * (thm list list * Args.src list)
+ * (thm list list list * Args.src list);
fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs),
- (unfoldss, corecss, coiter_attrs), (disc_unfoldss, disc_corecss, disc_iter_attrs),
- (disc_unfold_iffss, disc_corec_iffss, disc_iter_iff_attrs),
- (sel_unfoldsss, sel_corecsss, sel_iter_attrs)) =
+ (corecss, corec_attrs), (disc_corecss, disc_corec_attrs),
+ (disc_corec_iffss, disc_corec_iff_attrs), (sel_corecsss, sel_corec_attrs)) =
((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
coinduct_attrs),
- (map (map (Morphism.thm phi)) unfoldss, map (map (Morphism.thm phi)) corecss, coiter_attrs),
- (map (map (Morphism.thm phi)) disc_unfoldss, map (map (Morphism.thm phi)) disc_corecss,
- disc_iter_attrs),
- (map (map (Morphism.thm phi)) disc_unfold_iffss, map (map (Morphism.thm phi)) disc_corec_iffss,
- disc_iter_iff_attrs),
- (map (map (map (Morphism.thm phi))) sel_unfoldsss,
- map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs)) : gfp_sugar_thms;
+ (map (map (Morphism.thm phi)) corecss, corec_attrs),
+ (map (map (Morphism.thm phi)) disc_corecss, disc_corec_attrs),
+ (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs),
+ (map (map (map (Morphism.thm phi))) sel_corecsss, sel_corec_attrs)) : gfp_sugar_thms;
val transfer_gfp_sugar_thms =
morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
-fun mk_iters_args_types ctr_Tsss Cs absTs repTs ns mss ctor_iter_fun_Tss lthy =
+fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy =
let
val Css = map2 replicate ns Cs;
- val y_Tsss = map5 (fn absT => fn repT => fn n => fn ms =>
- dest_absumprodT absT repT n ms o domain_type)
- absTs repTs ns mss (map un_fold_of ctor_iter_fun_Tss);
- val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
-
- val ((gss, ysss), lthy) =
- lthy
- |> mk_Freess "f" g_Tss
- ||>> mk_Freesss "x" y_Tsss;
-
- val y_Tssss = map (map (map single)) y_Tsss;
- val yssss = map (map (map single)) ysss;
+ val x_Tssss =
+ map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T =>
+ map2 (map2 unzip_recT)
+ ctr_Tss (dest_absumprodT absT repT n ms (domain_type ctor_rec_fun_T)))
+ absTs repTs ns mss ctr_Tsss ctor_rec_fun_Ts;
- val z_Tssss =
- map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_iter_fun_Ts =>
- map2 (map2 unzip_recT)
- ctr_Tss (dest_absumprodT absT repT n ms (domain_type (co_rec_of ctor_iter_fun_Ts))))
- absTs repTs ns mss ctr_Tsss ctor_iter_fun_Tss;
-
- val z_Tsss' = map (map flat_rec_arg_args) z_Tssss;
- val h_Tss = map2 (map2 (curry (op --->))) z_Tsss' Css;
+ val x_Tsss' = map (map flat_rec_arg_args) x_Tssss;
+ val f_Tss = map2 (map2 (curry (op --->))) x_Tsss' Css;
- val hss = map2 (map2 retype_free) h_Tss gss;
- val zssss_hd = map2 (map2 (map2 (retype_free o hd))) z_Tssss ysss;
- val (zssss_tl, lthy) =
+ val ((fss, xssss), lthy) =
lthy
- |> mk_Freessss "y" (map (map (map tl)) z_Tssss);
- val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl;
+ |> mk_Freess "f" f_Tss
+ ||>> mk_Freessss "x" x_Tssss;
in
- ([(g_Tss, y_Tssss, gss, yssss), (h_Tss, z_Tssss, hss, zssss)], lthy)
+ ((f_Tss, x_Tssss, fss, xssss), lthy)
end;
-(*avoid "'a itself" arguments in coiterators*)
+(*avoid "'a itself" arguments in corecursors*)
fun repair_nullary_single_ctr [[]] = [[@{typ unit}]]
| repair_nullary_single_ctr Tss = Tss;
-fun mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts =
+fun mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts =
let
val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss;
- val f_absTs = map range_type fun_Ts;
- val f_Tsss = map repair_nullary_single_ctr (map5 dest_absumprodT absTs repTs ns mss f_absTs);
- val f_Tssss = map3 (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
- Cs ctr_Tsss' f_Tsss;
- val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) f_Tssss;
+ val g_absTs = map range_type fun_Ts;
+ val g_Tsss = map repair_nullary_single_ctr (map5 dest_absumprodT absTs repTs ns mss g_absTs);
+ val g_Tssss = map3 (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
+ Cs ctr_Tsss' g_Tsss;
+ val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) g_Tssss;
in
- (q_Tssss, f_Tsss, f_Tssss, f_absTs)
+ (q_Tssss, g_Tsss, g_Tssss, g_absTs)
end;
-fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
+fun mk_corec_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
-fun mk_coiter_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_coiter =
- (mk_coiter_p_pred_types Cs ns,
- mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss
- (binder_fun_types (fastype_of dtor_coiter)));
-
-fun mk_coiters_args_types ctr_Tsss Cs absTs repTs ns mss dtor_coiter_fun_Tss lthy =
- let
- val p_Tss = mk_coiter_p_pred_types Cs ns;
+fun mk_corec_fun_arg_types ctr_Tsss Cs absTs repTs ns mss dtor_corec =
+ (mk_corec_p_pred_types Cs ns,
+ mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss
+ (binder_fun_types (fastype_of dtor_corec)));
- fun mk_types get_Ts =
- let
- val fun_Ts = map get_Ts dtor_coiter_fun_Tss;
- val (q_Tssss, f_Tsss, f_Tssss, f_repTs) =
- mk_coiter_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts;
- in
- (q_Tssss, f_Tsss, f_Tssss, f_repTs)
- end;
+fun mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts lthy =
+ let
+ val p_Tss = mk_corec_p_pred_types Cs ns;
- val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types un_fold_of;
- val (s_Tssss, h_Tsss, h_Tssss, corec_types) = mk_types co_rec_of;
+ val (q_Tssss, g_Tsss, g_Tssss, corec_types) =
+ mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss dtor_corec_fun_Ts;
- val ((((Free (z, _), cs), pss), gssss), lthy) =
+ val (((((Free (x, _), cs), pss), qssss), gssss), lthy) =
lthy
- |> yield_singleton (mk_Frees "z") dummyT
+ |> yield_singleton (mk_Frees "x") dummyT
||>> mk_Frees "a" Cs
||>> mk_Freess "p" p_Tss
+ ||>> mk_Freessss "q" q_Tssss
||>> mk_Freessss "g" g_Tssss;
- val rssss = map (map (map (fn [] => []))) r_Tssss;
-
- val hssss_hd = map2 (map2 (map2 (fn T :: _ => fn [g] => retype_free T g))) h_Tssss gssss;
- val ((sssss, hssss_tl), lthy) =
- lthy
- |> mk_Freessss "q" s_Tssss
- ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss);
- val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl;
val cpss = map2 (map o rapp) cs pss;
fun build_sum_inj mk_inj = build_map lthy (uncurry mk_inj o dest_sumT o snd);
- fun build_dtor_coiter_arg _ [] [cf] = cf
- | build_dtor_coiter_arg T [cq] [cf, cf'] =
- mk_If cq (build_sum_inj Inl_const (fastype_of cf, T) $ cf)
- (build_sum_inj Inr_const (fastype_of cf', T) $ cf');
+ fun build_dtor_corec_arg _ [] [cg] = cg
+ | build_dtor_corec_arg T [cq] [cg, cg'] =
+ mk_If cq (build_sum_inj Inl_const (fastype_of cg, T) $ cg)
+ (build_sum_inj Inr_const (fastype_of cg', T) $ cg');
- fun mk_args qssss fssss f_Tsss =
- let
- val pfss = map3 flat_corec_preds_predsss_gettersss pss qssss fssss;
- val cqssss = map2 (map o map o map o rapp) cs qssss;
- val cfssss = map2 (map o map o map o rapp) cs fssss;
- val cqfsss = map3 (map3 (map3 build_dtor_coiter_arg)) f_Tsss cqssss cfssss;
- in (pfss, cqfsss) end;
-
- val unfold_args = mk_args rssss gssss g_Tsss;
- val corec_args = mk_args sssss hssss h_Tsss;
+ val pgss = map3 flat_corec_preds_predsss_gettersss pss qssss gssss;
+ val cqssss = map2 (map o map o map o rapp) cs qssss;
+ val cgssss = map2 (map o map o map o rapp) cs gssss;
+ val cqgsss = map3 (map3 (map3 build_dtor_corec_arg)) g_Tsss cqssss cgssss;
in
- ((z, cs, cpss, [(unfold_args, unfold_types), (corec_args, corec_types)]), lthy)
+ ((x, cs, cpss, ((pgss, cqgsss), corec_types)), lthy)
end;
-fun mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy =
+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_iter_fun_Tss, xtor_co_iterss) =
- map (mk_co_iters thy fp fpTs Cs #> `(binder_fun_types o fastype_of o hd))
- (transpose xtor_co_iterss0)
- |> apsnd transpose o apfst transpose o split_list;
+ 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 ((iters_args_types, coiters_args_types), lthy') =
+ val ((recs_args_types, corecs_args_types), lthy') =
if fp = Least_FP then
- mk_iters_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_iter_fun_Tss lthy
- |>> (rpair NONE o SOME)
+ 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)
else
- mk_coiters_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_iter_fun_Tss lthy
+ mk_corecs_args_types ctr_Tsss Cs absTs repTs ns mss xtor_co_rec_fun_Ts lthy
|>> (pair NONE o SOME);
in
- ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy')
+ ((xtor_co_recs, recs_args_types, corecs_args_types), lthy')
end;
-fun mk_preds_getterss_join c cps absT abs cqfss =
+fun mk_preds_getterss_join c cps absT abs cqgss =
let
- val n = length cqfss;
- val ts = map2 (mk_absumprod absT abs n) (1 upto n) cqfss;
+ val n = length cqgss;
+ val ts = map2 (mk_absumprod absT abs n) (1 upto n) cqgss;
in
Term.lambda c (mk_IfN absT cps ts)
end;
-fun define_co_iters fp fpT Cs binding_specs lthy0 =
+fun define_co_rec fp fpT Cs b rhs lthy0 =
let
val thy = Proof_Context.theory_of lthy0;
val maybe_conceal_def_binding = Thm.def_binding
#> Config.get lthy0 bnf_note_all = false ? Binding.conceal;
- val ((csts, defs), (lthy', lthy)) = lthy0
- |> apfst split_list o fold_map (fn (b, rhs) =>
- Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
- #>> apsnd snd) binding_specs
+ val ((cst, (_, def)), (lthy', lthy)) = lthy0
+ |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy lthy';
- val csts' = map (mk_co_iter thy fp fpT Cs o Morphism.term phi) csts;
- val defs' = map (Morphism.thm phi) defs;
+ val cst' = mk_co_rec thy fp fpT Cs (Morphism.term phi cst);
+ val def' = Morphism.thm phi def;
in
- ((csts', defs'), lthy')
- end;
-
-fun define_iters iterNs iter_args_typess' mk_binding fpTs Cs reps ctor_iters lthy =
- let
- val nn = length fpTs;
- val fpT = domain_type (snd (strip_typeN nn (fastype_of (un_fold_of ctor_iters))));
-
- fun generate_iter pre (_, _, fss, xssss) ctor_iter =
- let val ctor_iter_absTs = map domain_type (fst (strip_typeN nn (fastype_of ctor_iter))) in
- (mk_binding pre,
- fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_iter,
- map4 (fn ctor_iter_absT => fn rep => fn fs => fn xsss =>
- mk_case_absumprod ctor_iter_absT rep fs
- (map (HOLogic.mk_tuple o map HOLogic.mk_tuple) xsss) (map flat_rec_arg_args xsss))
- ctor_iter_absTs reps fss xssss)))
- end;
- in
- define_co_iters Least_FP fpT Cs (map3 generate_iter iterNs iter_args_typess' ctor_iters) lthy
+ ((cst', def'), lthy')
end;
-fun define_coiters coiterNs (_, cs, cpss, coiter_args_typess') mk_binding fpTs Cs abss dtor_coiters
- lthy =
+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 (HOLogic.mk_tuple o 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
val nn = length fpTs;
-
- val Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
-
- fun generate_coiter pre ((pfss, cqfsss), f_absTs) dtor_coiter =
- (mk_binding pre,
- fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_coiter,
- map5 mk_preds_getterss_join cs cpss f_absTs abss cqfsss)));
+ val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
in
- define_co_iters Greatest_FP fpT Cs
- (map3 generate_coiter coiterNs coiter_args_typess' dtor_coiters) lthy
+ define_co_rec Greatest_FP fpT Cs (mk_binding corecN)
+ (fold_rev (fold_rev Term.lambda) pgss (Term.list_comb (dtor_corec,
+ map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
end;
-fun derive_induct_iters_thms_for_types pre_bnfs [fold_args_types, rec_args_types] ctor_induct
- ctor_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
- fp_type_definitions abs_inverses ctrss ctr_defss iterss iter_defss lthy =
+fun derive_induct_recs_thms_for_types pre_bnfs rec_args_typess ctor_induct ctor_rec_thms
+ nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses fp_type_definitions abs_inverses
+ ctrss ctr_defss recs rec_defs lthy =
let
- val iterss' = transpose iterss;
- val iter_defss' = transpose iter_defss;
-
- val [folds, recs] = iterss';
- val [fold_defs, rec_defs] = iter_defss';
-
val ctr_Tsss = map (map (binder_types o fastype_of)) ctrss;
val nn = length pre_bnfs;
@@ -668,13 +608,13 @@
val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
- fun mk_iter_thmss (_, x_Tssss, fss, _) iters iter_defs ctor_iter_thms =
+ fun mk_rec_thmss (_, x_Tssss, fss, _) recs rec_defs ctor_rec_thms =
let
- val fiters = map (lists_bmoc fss) iters;
+ val frecs = map (lists_bmoc fss) recs;
- fun mk_goal fss fiter xctr f xs fxs =
+ fun mk_goal frec xctr f xs fxs =
fold_rev (fold_rev Logic.all) (xs :: fss)
- (mk_Trueprop_eq (fiter $ xctr, Term.list_comb (f, fxs)));
+ (mk_Trueprop_eq (frec $ xctr, Term.list_comb (f, fxs)));
fun maybe_tick (T, U) u f =
if try (fst o HOLogic.dest_prodT) U = SOME T then
@@ -682,20 +622,19 @@
else
f;
- fun build_iter (x as Free (_, T)) U =
+ fun build_rec (x as Free (_, T)) U =
if T = U then
x
else
build_map lthy (indexify (perhaps (try (snd o HOLogic.dest_prodT)) o snd) Cs
- (fn kk => fn TU => maybe_tick TU (nth us kk) (nth fiters kk))) (T, U) $ x;
+ (fn kk => fn TU => maybe_tick TU (nth us kk) (nth frecs kk))) (T, U) $ x;
- val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_iter))) xsss x_Tssss;
-
- val goalss = map5 (map4 o mk_goal fss) fiters xctrss fss xsss fxsss;
+ val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
+ val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss;
val tacss =
- map4 (map ooo mk_iter_tac pre_map_defs (nested_map_idents @ nesting_map_idents) iter_defs)
- ctor_iter_thms fp_abs_inverses abs_inverses ctr_defss;
+ map4 (map ooo mk_rec_tac pre_map_defs (nested_map_idents @ nesting_map_idents) rec_defs)
+ ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
fun prove goal tac =
Goal.prove_sorry lthy [] [] goal (tac o #context)
@@ -704,29 +643,24 @@
map2 (map2 prove) goalss tacss
end;
- val fold_thmss = mk_iter_thmss fold_args_types folds fold_defs (map un_fold_of ctor_iter_thmss);
- val rec_thmss = mk_iter_thmss rec_args_types recs rec_defs (map co_rec_of ctor_iter_thmss);
+ val rec_thmss =
+ (case rec_args_typess of
+ SOME types => mk_rec_thmss types recs rec_defs ctor_rec_thms
+ | NONE => replicate nn []);
in
((induct_thms, induct_thm, [induct_case_names_attr]),
- (fold_thmss, rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
+ (rec_thmss, code_nitpicksimp_attrs @ simp_attrs))
end;
-fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss,
- coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)])
- dtor_coinduct dtor_injects dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
+fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
+ dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
- coiterss coiter_defss export_args lthy =
+ corecs corec_defs export_args lthy =
let
- fun mk_ctor_dtor_coiter_thm dtor_inject dtor_ctor coiter =
- iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
+ fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
+ iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]];
- val ctor_dtor_coiter_thmss =
- map3 (map oo mk_ctor_dtor_coiter_thm) dtor_injects dtor_ctors dtor_coiter_thmss;
-
- val coiterss' = transpose coiterss;
- val coiter_defss' = transpose coiter_defss;
-
- val [unfold_defs, corec_defs] = coiter_defss';
+ val ctor_dtor_corec_thms = map3 mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms;
val nn = length pre_bnfs;
@@ -840,79 +774,62 @@
fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
- val fcoiterss' as [gunfolds, hcorecs] =
- map2 (fn (pfss, _) => map (lists_bmoc pfss)) (map fst coiters_args_types) coiterss';
+ val gcorecs = map (lists_bmoc pgss) corecs;
- val (unfold_thmss, corec_thmss) =
+ val corec_thmss =
let
- fun mk_goal pfss c cps fcoiter n k ctr m cfs' =
- fold_rev (fold_rev Logic.all) ([c] :: pfss)
+ fun mk_goal c cps gcorec n k ctr m cfs' =
+ fold_rev (fold_rev Logic.all) ([c] :: pgss)
(Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
- mk_Trueprop_eq (fcoiter $ c, Term.list_comb (ctr, take m cfs'))));
+ mk_Trueprop_eq (gcorec $ c, Term.list_comb (ctr, take m cfs'))));
+
+ val mk_U = typ_subst_nonatomic (map2 (fn C => fn fpT => (mk_sumT (fpT, C), fpT)) Cs fpTs);
- fun mk_U maybe_mk_sumT =
- typ_subst_nonatomic (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
-
- fun tack z_name (c, u) f =
- let val z = Free (z_name, mk_sumT (fastype_of u, fastype_of c)) in
- Term.lambda z (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ z)
+ fun tack (c, u) f =
+ let val x' = Free (x, mk_sumT (fastype_of u, fastype_of c)) in
+ Term.lambda x' (mk_case_sum (Term.lambda u u, Term.lambda c (f $ c)) $ x')
end;
- fun build_coiter fcoiters maybe_mk_sumT maybe_tack cqf =
- let val T = fastype_of cqf in
+ fun build_corec cqg =
+ let val T = fastype_of cqg in
if exists_subtype_in Cs T then
- let val U = mk_U maybe_mk_sumT T in
- build_map lthy (indexify fst (map2 maybe_mk_sumT fpTs Cs) (fn kk => fn _ =>
- maybe_tack (nth cs kk, nth us kk) (nth fcoiters kk))) (T, U) $ cqf
+ let val U = mk_U T in
+ build_map lthy (indexify fst (map2 (curry mk_sumT) fpTs Cs) (fn kk => fn _ =>
+ tack (nth cs kk, nth us kk) (nth gcorecs kk))) (T, U) $ cqg
end
else
- cqf
+ cqg
end;
- val crgsss' = map (map (map (build_coiter (un_fold_of fcoiterss') (K I) (K I)))) crgsss;
- val cshsss' = map (map (map (build_coiter (co_rec_of fcoiterss') (curry mk_sumT) (tack z))))
- cshsss;
-
- val unfold_goalss = map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss';
- val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss';
+ val cqgsss' = map (map (map build_corec)) cqgsss;
+ val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss';
- val unfold_tacss =
- map4 (map ooo mk_coiter_tac unfold_defs nesting_map_idents)
- (map un_fold_of ctor_dtor_coiter_thmss) pre_map_defs abs_inverses ctr_defss;
- val corec_tacss =
- map4 (map ooo mk_coiter_tac corec_defs nesting_map_idents)
- (map co_rec_of ctor_dtor_coiter_thmss) pre_map_defs abs_inverses ctr_defss;
+ val tacss =
+ map4 (map ooo mk_corec_tac corec_defs nesting_map_idents)
+ ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss;
fun prove goal tac =
Goal.prove_sorry lthy [] [] goal (tac o #context)
|> Thm.close_derivation;
-
- val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
- val corec_thmss =
- map2 (map2 prove) corec_goalss corec_tacss
- |> map (map (unfold_thms lthy @{thms case_sum_if}));
in
- (unfold_thmss, corec_thmss)
+ map2 (map2 prove) goalss tacss
+ |> map (map (unfold_thms lthy @{thms case_sum_if}))
end;
- val (disc_unfold_iff_thmss, disc_corec_iff_thmss) =
+ val disc_corec_iff_thmss =
let
- fun mk_goal c cps fcoiter n k disc =
- mk_Trueprop_eq (disc $ (fcoiter $ c),
+ fun mk_goal c cps gcorec n k disc =
+ mk_Trueprop_eq (disc $ (gcorec $ c),
if n = 1 then @{const True}
else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
- val unfold_goalss = map6 (map2 oooo mk_goal) cs cpss gunfolds ns kss discss;
- val corec_goalss = map6 (map2 oooo mk_goal) cs cpss hcorecs ns kss discss;
+ val goalss = map6 (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
fun mk_case_split' cp = Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
val case_splitss' = map (map mk_case_split') cpss;
- val unfold_tacss =
- map3 (map oo mk_disc_coiter_iff_tac) case_splitss' unfold_thmss disc_thmsss;
- val corec_tacss =
- map3 (map oo mk_disc_coiter_iff_tac) case_splitss' corec_thmss disc_thmsss;
+ val tacss = map3 (map oo mk_disc_corec_iff_tac) case_splitss' corec_thmss disc_thmsss;
fun prove goal tac =
Goal.prove_sorry lthy [] [] goal (tac o #context)
@@ -923,15 +840,14 @@
fun proves [_] [_] = []
| proves goals tacs = map2 prove goals tacs;
in
- (map2 proves unfold_goalss unfold_tacss, map2 proves corec_goalss corec_tacss)
+ map2 proves goalss tacss
end;
- fun mk_disc_coiter_thms coiters discIs = map (op RS) (coiters ~~ discIs);
+ fun mk_disc_corec_thms corecs discIs = map (op RS) (corecs ~~ discIs);
- val disc_unfold_thmss = map2 mk_disc_coiter_thms unfold_thmss discIss;
- val disc_corec_thmss = map2 mk_disc_coiter_thms corec_thmss discIss;
+ val disc_corec_thmss = map2 mk_disc_corec_thms corec_thmss discIss;
- fun mk_sel_coiter_thm coiter_thm sel sel_thm =
+ fun mk_sel_corec_thm corec_thm sel sel_thm =
let
val (domT, ranT) = dest_funT (fastype_of sel);
val arg_cong' =
@@ -940,14 +856,13 @@
|> Thm.varifyT_global;
val sel_thm' = sel_thm RSN (2, trans);
in
- coiter_thm RS arg_cong' RS sel_thm'
+ corec_thm RS arg_cong' RS sel_thm'
end;
- fun mk_sel_coiter_thms coiter_thmss =
- map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss;
+ fun mk_sel_corec_thms corec_thmss =
+ map3 (map3 (map2 o mk_sel_corec_thm)) corec_thmss selsss sel_thmsss;
- val sel_unfold_thmsss = mk_sel_coiter_thms unfold_thmss;
- val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss;
+ val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
@@ -959,10 +874,10 @@
coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs;
in
((coinduct_thms_pairs, coinduct_case_attrs),
- (unfold_thmss, corec_thmss, code_nitpicksimp_attrs),
- (disc_unfold_thmss, disc_corec_thmss, []),
- (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
- (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
+ (corec_thmss, code_nitpicksimp_attrs),
+ (disc_corec_thmss, []),
+ (disc_corec_iff_thmss, simp_attrs),
+ (sel_corec_thmsss, simp_attrs))
end;
fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
@@ -1080,9 +995,9 @@
(unsorted_As ~~ transpose set_boss);
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
- dtors = dtors0, xtor_co_iterss = xtor_co_iterss0, xtor_co_induct, dtor_ctors,
+ dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_iter_thmss, ...},
+ xtor_co_rec_thms, ...},
lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
(map dest_TFree killed_As) fp_eqs no_defs_lthy0
@@ -1167,11 +1082,11 @@
val kss = map (fn n => 1 upto n) ns;
val mss = map (map length) ctr_Tsss;
- val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') =
- mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy;
+ val ((xtor_co_recs, recs_args_types, corecs_args_types), lthy') =
+ mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
fun define_ctrs_dtrs_for_type (((((((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor),
- xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
+ xtor_co_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), abs),
abs_inject), abs_inverse), type_definition), ctr_bindings), ctr_mixfixes), ctr_Tss),
disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
@@ -1362,17 +1277,14 @@
fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
- fun massage_res (((maps_sets_rels, ctr_sugar), co_iter_res), lthy) =
- (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_iter_res), lthy);
+ fun massage_res (((maps_sets_rels, ctr_sugar), co_rec_res), lthy) =
+ (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_rec_res), lthy);
in
(wrap_ctrs
#> derive_maps_sets_rels
##>>
- (if fp = Least_FP then
- define_iters [foldN, recN] (the iters_args_types) mk_binding fpTs Cs reps xtor_co_iters
- else
- define_coiters [unfoldN, corecN] (the coiters_args_types) mk_binding fpTs Cs abss
- xtor_co_iters)
+ (if fp = Least_FP then define_rec 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;
@@ -1381,71 +1293,71 @@
|>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list)
o split_list;
- fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) un_folds co_recs
- mapsx rel_injects rel_distincts setss =
- injects @ distincts @ case_thms @ co_recs @ un_folds @ mapsx @ rel_injects @ rel_distincts
- @ flat setss;
+ fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs mapsx rel_injects
+ rel_distincts setss =
+ injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
- fun derive_note_induct_iters_thms_for_types
+ fun derive_note_induct_recs_thms_for_types
((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)),
- (iterss, iter_defss)), lthy) =
+ (recs, rec_defs)), lthy) =
let
- val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, iter_attrs)) =
- derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
- xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
- type_definitions abs_inverses ctrss ctr_defss iterss iter_defss lthy;
+ val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
+ derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct xtor_co_rec_thms
+ nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses type_definitions
+ abs_inverses ctrss ctr_defss recs rec_defs lthy;
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 =
- map7 mk_simp_thms ctr_sugars fold_thmss rec_thmss mapss rel_injects rel_distincts setss;
+ map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injects rel_distincts setss;
val common_notes =
(if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
|> massage_simple_notes fp_common_name;
val notes =
- [(foldN, fold_thmss, K iter_attrs),
- (inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
- (recN, rec_thmss, K iter_attrs),
+ [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
+ (recN, rec_thmss, K rec_attrs),
(simpsN, simp_thmss, K [])]
|> massage_multi_notes;
in
lthy
- |> Spec_Rules.add Spec_Rules.Equational (map un_fold_of iterss, flat fold_thmss)
- |> Spec_Rules.add Spec_Rules.Equational (map co_rec_of iterss, flat rec_thmss)
+ |> (if is_some recs_args_types then
+ Spec_Rules.add Spec_Rules.Equational (recs, flat rec_thmss)
+ else
+ I)
|> 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 iterss mapss [induct_thm] (map single induct_thms)
- (transpose [fold_thmss, rec_thmss]) (replicate nn []) (replicate nn [])
+ ctrXs_Tsss ctr_defss ctr_sugars recs' mapss [induct_thm] (map single induct_thms)
+ rec_thmss' (replicate nn []) (replicate nn [])
end;
- fun derive_note_coinduct_coiters_thms_for_types
+ fun derive_note_coinduct_corecs_thms_for_types
((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)),
- (coiterss, coiter_defss)), lthy) =
+ (corecs, corec_defs)), lthy) =
let
val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
coinduct_attrs),
- (unfold_thmss, corec_thmss, coiter_attrs),
- (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
- (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
- (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) =
- derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
- dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
- abs_inverses abs_inverses I ctr_defss ctr_sugars coiterss coiter_defss
+ (corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs),
+ (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
+ derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
+ dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
+ abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
(Proof_Context.export lthy' no_defs_lthy) lthy;
- val sel_unfold_thmss = map flat sel_unfold_thmsss;
val sel_corec_thmss = map flat sel_corec_thmsss;
val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
- val flat_coiter_thms = append oo append;
+ val flat_corec_thms = append oo append;
val simp_thmss =
- map7 mk_simp_thms ctr_sugars
- (map3 flat_coiter_thms disc_unfold_thmss disc_unfold_iff_thmss sel_unfold_thmss)
- (map3 flat_coiter_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_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;
val common_notes =
@@ -1459,44 +1371,34 @@
val notes =
[(coinductN, map single coinduct_thms,
fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
- (corecN, corec_thmss, K coiter_attrs),
- (disc_corecN, disc_corec_thmss, K disc_coiter_attrs),
- (disc_corec_iffN, disc_corec_iff_thmss, K disc_coiter_iff_attrs),
- (disc_unfoldN, disc_unfold_thmss, K disc_coiter_attrs),
- (disc_unfold_iffN, disc_unfold_iff_thmss, K disc_coiter_iff_attrs),
- (sel_corecN, sel_corec_thmss, K sel_coiter_attrs),
- (sel_unfoldN, sel_unfold_thmss, K sel_coiter_attrs),
+ (corecN, corec_thmss, K corec_attrs),
+ (disc_corecN, disc_corec_thmss, K disc_corec_attrs),
+ (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),
+ (sel_corecN, sel_corec_thmss, K sel_corec_attrs),
(simpsN, simp_thmss, K []),
- (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
- (unfoldN, unfold_thmss, K coiter_attrs)]
+ (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs)]
|> massage_multi_notes;
-
- (* TODO: code theorems *)
- fun add_spec_rules coiter_of sel_thmss ctr_thmss =
- fold (curry (Spec_Rules.add Spec_Rules.Equational) (map coiter_of coiterss))
- [flat sel_thmss, flat ctr_thmss]
in
lthy
- |> add_spec_rules un_fold_of sel_unfold_thmss unfold_thmss
- |> add_spec_rules co_rec_of sel_corec_thmss corec_thmss
+ (* TODO: code theorems *)
+ |> 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 coiterss mapss [coinduct_thm, strong_coinduct_thm]
- (transpose [coinduct_thms, strong_coinduct_thms])
- (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
- (transpose [sel_unfold_thmsss, sel_corec_thmsss])
+ 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
end;
val lthy'' = lthy'
|> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~
- xtor_co_iterss ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
- pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~
- kss ~~ mss ~~ abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~
- ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
- raw_sel_defaultsss)
+ xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~
+ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~
+ abss ~~ abs_injects ~~ abs_inverses ~~ type_definitions ~~ ctr_bindingss ~~ ctr_mixfixess ~~
+ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
|> wrap_types_etc
- |> fp_case fp derive_note_induct_iters_thms_for_types
- derive_note_coinduct_coiters_thms_for_types;
+ |> fp_case fp derive_note_induct_recs_thms_for_types
+ derive_note_coinduct_corecs_thms_for_types;
val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
co_prefix fp ^ "datatype"));
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Mar 03 15:14:00 2014 +0100
@@ -14,16 +14,16 @@
val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
thm list list list -> tactic
- val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
+ val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
- val mk_disc_coiter_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+ val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
- val mk_iter_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
+ val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
tactic
end;
@@ -66,7 +66,6 @@
fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN
- unfold_thms_tac ctxt @{thms split_paired_all} THEN
HEADGOAL (EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k,
REPEAT_DETERM o dtac meta_spec, etac meta_mp, atac]) (1 upto n)));
@@ -87,32 +86,32 @@
unfold_thms_tac ctxt (abs_inject :: @{thms sum.inject Pair_eq conj_assoc}) THEN
HEADGOAL (rtac refl);
-val iter_unfold_thms =
+val rec_unfold_thms =
@{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
case_unit_Unity} @ sum_prod_thms_map;
-fun mk_iter_tac pre_map_defs map_idents iter_defs ctor_iter fp_abs_inverse abs_inverse ctr_def ctxt =
- unfold_thms_tac ctxt (ctr_def :: ctor_iter :: fp_abs_inverse :: abs_inverse :: iter_defs @
- pre_map_defs @ map_idents @ iter_unfold_thms) THEN HEADGOAL (rtac refl);
+fun mk_rec_tac pre_map_defs map_idents rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
+ unfold_thms_tac ctxt (ctr_def :: ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
+ pre_map_defs @ map_idents @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
-val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
+val corec_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
-fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def abs_inverse ctr_def ctxt =
+fun mk_corec_tac corec_defs map_idents ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
let
- val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ coiter_unfold_thms @
+ val ss = ss_only (pre_map_def :: abs_inverse :: map_idents @ corec_unfold_thms @
@{thms o_apply vimage2p_def if_True if_False}) ctxt;
in
- unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
- HEADGOAL (rtac (ctor_dtor_coiter RS trans) THEN' asm_simp_tac ss) THEN_MAYBE
+ unfold_thms_tac ctxt (ctr_def :: corec_defs) THEN
+ HEADGOAL (rtac (ctor_dtor_corec RS trans) THEN' asm_simp_tac ss) THEN_MAYBE
HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))
end;
-fun mk_disc_coiter_iff_tac case_splits' coiters discs ctxt =
- EVERY (map3 (fn case_split_tac => fn coiter_thm => fn disc =>
- HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [coiter_thm] THEN
+fun mk_disc_corec_iff_tac case_splits' corecs discs ctxt =
+ EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc =>
+ HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN
HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN
(if is_refl disc then all_tac else HEADGOAL (rtac disc)))
- (map rtac case_splits' @ [K all_tac]) coiters discs);
+ (map rtac case_splits' @ [K all_tac]) corecs discs);
fun solve_prem_prem_tac ctxt =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Mar 03 15:14:00 2014 +0100
@@ -207,7 +207,7 @@
|> unfold_thms lthy (@{thms eq_le_Grp_id_iff all_simps(1,2)[symmetric]} @ rel_eqs)
|> funpow n (fn thm => thm RS spec)
|> unfold_thms lthy (@{thm eq_alt} :: map rel_Grp_of_bnf bnfs @ map_id0s)
- |> unfold_thms lthy (@{thms vimage2p_comp comp_apply comp_id
+ |> unfold_thms lthy (@{thms vimage2p_id vimage2p_comp comp_apply comp_id
Grp_id_mono_subst eqTrueI[OF subset_UNIV] simp_thms(22)} @
maps mk_fp_type_copy_thms fp_type_definitions @
maps mk_type_copy_thms type_definitions)
@@ -236,7 +236,8 @@
|> mk_Frees' "s" fold_strTs
||>> mk_Frees' "s" rec_strTs;
- val co_iters = of_fp_res #xtor_co_iterss;
+ val co_folds = of_fp_res #xtor_co_folds;
+ 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
@@ -245,11 +246,11 @@
val typ_subst_nonatomic_sorted = fold_rev (typ_subst_nonatomic o single);
- fun force_iter is_rec i TU TU_rec raw_iters =
+ fun force_iter is_rec i TU TU_rec raw_fold raw_rec =
let
val thy = Proof_Context.theory_of lthy;
- val approx_fold = un_fold_of raw_iters
+ val approx_fold = raw_fold
|> force_typ names_lthy
(replicate (nth ns i) dummyT ---> (if is_rec then TU_rec else TU));
val subst = Term.typ_subst_atomic fold_thetaAs;
@@ -269,9 +270,8 @@
val js = find_indices Type.could_unify TUs cands;
val Tpats = map (fn j => mk_co_algT (nth fold_pre_deads_only_Ts j) (nth Xs j)) js;
- val iter = raw_iters |> (if is_rec then co_rec_of else un_fold_of);
in
- force_typ names_lthy (Tpats ---> TU) iter
+ force_typ names_lthy (Tpats ---> TU) (if is_rec then raw_rec else raw_fold)
end;
fun mk_co_comp_abs_rep fp_absT absT fp_abs fp_rep abs rep t =
@@ -286,10 +286,11 @@
val i = find_index (fn T => x = T) Xs;
val TUiter =
(case find_first (fn f => body_fun_type (fastype_of f) = TU) iters of
- NONE => nth co_iters i
- |> force_iter is_rec i
+ NONE =>
+ force_iter is_rec i
(TU |> (is_none b_opt andalso not is_rec) ? substT (fpTs ~~ Xs))
- (TU |> (is_none b_opt) ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
+ (TU |> is_none b_opt ? substT (map2 mk_co_productT fpTs Xs ~~ Xs))
+ (nth co_folds i) (nth co_recs i)
| SOME f => f);
val TUs = binder_fun_types (fastype_of TUiter);
@@ -373,6 +374,9 @@
val un_folds = map (Morphism.term phi) raw_un_folds;
val co_recs = map (Morphism.term phi) raw_co_recs;
+ val fp_fold_o_maps = of_fp_res #xtor_co_fold_o_map_thms;
+ val fp_rec_o_maps = of_fp_res #xtor_co_rec_o_map_thms;
+
val (xtor_un_fold_thms, xtor_co_rec_thms) =
let
val folds = map (fn f => Term.list_comb (f, fold_strs)) raw_un_folds;
@@ -419,13 +423,9 @@
val unfold_map = map (unfold_thms lthy (id_apply :: pre_map_defs));
- val fp_xtor_co_iterss = of_fp_res #xtor_co_iter_thmss;
- val fp_xtor_un_folds = map (mk_pointfree lthy o un_fold_of) fp_xtor_co_iterss;
- val fp_xtor_co_recs = map (mk_pointfree lthy o co_rec_of) fp_xtor_co_iterss;
+ val fp_xtor_un_folds = map (mk_pointfree lthy) (of_fp_res #xtor_co_fold_thms);
+ val fp_xtor_co_recs = map (mk_pointfree lthy) (of_fp_res #xtor_co_rec_thms);
- val fp_co_iter_o_mapss = of_fp_res #xtor_co_iter_o_map_thmss;
- val fp_fold_o_maps = map un_fold_of fp_co_iter_o_mapss;
- val fp_rec_o_maps = map co_rec_of fp_co_iter_o_mapss;
val fold_thms = fp_case fp @{thm comp_assoc} @{thm comp_assoc[symmetric]} ::
map (fn thm => thm RS rewrite_comp_comp) @{thms map_pair.comp sum_map.comp} @
@{thms id_apply comp_id id_comp map_pair.comp map_pair.id sum_map.comp sum_map.id};
@@ -464,12 +464,8 @@
(* These results are half broken. This is deliberate. We care only about those fields that are
used by "primrec", "primcorecursive", and "datatype_compat". *)
val fp_res =
- ({Ts = fpTs,
- bnfs = of_fp_res #bnfs,
- dtors = dtors,
- ctors = ctors,
- xtor_co_iterss = transpose [un_folds, co_recs],
- xtor_co_induct = xtor_co_induct_thm,
+ ({Ts = fpTs, bnfs = of_fp_res #bnfs, dtors = dtors, ctors = ctors, xtor_co_folds = un_folds,
+ xtor_co_recs = co_recs, xtor_co_induct = xtor_co_induct_thm,
dtor_ctors = of_fp_res #dtor_ctors (*too general types*),
ctor_dtors = of_fp_res #ctor_dtors (*too general types*),
ctor_injects = of_fp_res #ctor_injects (*too general types*),
@@ -477,9 +473,10 @@
xtor_map_thms = of_fp_res #xtor_map_thms (*too general types and terms*),
xtor_set_thmss = of_fp_res #xtor_set_thmss (*too general types and terms*),
xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
- xtor_co_iter_thmss = transpose [xtor_un_fold_thms, xtor_co_rec_thms],
- xtor_co_iter_o_map_thmss = of_fp_res #xtor_co_iter_o_map_thmss
- (*theorem about old constant*),
+ xtor_co_fold_thms = xtor_un_fold_thms,
+ xtor_co_rec_thms = xtor_co_rec_thms,
+ xtor_co_fold_o_map_thms = fp_fold_o_maps (*theorems about old constants*),
+ xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Mar 03 15:14:00 2014 +0100
@@ -223,8 +223,8 @@
val fp_absT_infos = map #absT_info fp_sugars0;
- val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_iterss = xtor_co_iterss0, xtor_co_induct,
- dtor_injects, dtor_ctors, xtor_co_iter_thmss, ...}, lthy)) =
+ val ((pre_bnfs, absT_infos), (fp_res as {xtor_co_recs = xtor_co_recs0, xtor_co_induct,
+ dtor_injects, dtor_ctors, xtor_co_rec_thms, ...}, lthy)) =
fp_bnf (construct_mutualized_fp fp fpTs fp_sugars0) fp_bs As' killed_As' fp_eqs
no_defs_lthy0;
@@ -240,61 +240,53 @@
val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;
val nested_bnfs = nesty_bnfs lthy ctrXs_Tsss Xs;
- val ((xtor_co_iterss, iters_args_types, coiters_args_types), _) =
- mk_co_iters_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_iterss0 lthy;
+ val ((xtor_co_recs, recs_args_types, corecs_args_types), _) =
+ mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy;
fun mk_binding b suf = Binding.suffix_name ("_" ^ suf) b;
- val ((co_iterss, co_iter_defss), lthy) =
+ val ((co_recs, co_rec_defs), lthy) =
fold_map2 (fn b =>
- if fp = Least_FP then
- define_iters [foldN, recN] (the iters_args_types) (mk_binding b) fpTs Cs reps
- else
- define_coiters [unfoldN, corecN] (the coiters_args_types) (mk_binding b) fpTs Cs abss)
- fp_bs xtor_co_iterss lthy
+ if fp = Least_FP then define_rec 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;
- val ((common_co_inducts, co_inductss, un_fold_thmss, co_rec_thmss, disc_unfold_thmss,
- disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss), fp_sugar_thms) =
+ val ((common_co_inducts, co_inductss, co_rec_thmss, disc_corec_thmss, sel_corec_thmsss),
+ fp_sugar_thms) =
if fp = Least_FP then
- derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
- xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
- fp_type_definitions abs_inverses ctrss ctr_defss co_iterss co_iter_defss lthy
- |> `(fn ((inducts, induct, _), (fold_thmss, rec_thmss, _)) =>
- ([induct], [inducts], fold_thmss, rec_thmss, replicate nn [],
- replicate nn [], replicate nn [], replicate nn []))
+ derive_induct_recs_thms_for_types pre_bnfs recs_args_types xtor_co_induct
+ xtor_co_rec_thms nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss fp_abs_inverses
+ fp_type_definitions abs_inverses ctrss ctr_defss co_recs co_rec_defs lthy
+ |> `(fn ((inducts, induct, _), (rec_thmss, _)) =>
+ ([induct], [inducts], rec_thmss, replicate nn [], replicate nn []))
||> (fn info => (SOME info, NONE))
else
- derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
- dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
- ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
- ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
- |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _),
- (disc_unfold_thmss, disc_corec_thmss, _), _,
- (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
- (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, unfold_thmss,
- corec_thmss, disc_unfold_thmss, disc_corec_thmss, sel_unfold_thmsss,
- sel_corec_thmsss))
+ derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
+ dtor_injects dtor_ctors xtor_co_rec_thms nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns
+ fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
+ ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
+ |> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _,
+ (sel_corec_thmsss, _)) =>
+ (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
+ disc_corec_thmss, sel_corec_thmsss))
||> (fn info => (NONE, SOME info));
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_iters maps
- co_inducts un_fold_thms co_rec_thms disc_unfold_thms disc_corec_thms sel_unfold_thmss
- sel_corec_thmss =
+ 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 =
{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_iters = co_iters,
+ 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,
- co_iter_thmss = [un_fold_thms, co_rec_thms],
- disc_co_iterss = [disc_unfold_thms, disc_corec_thms],
- sel_co_itersss = [sel_unfold_thmss, sel_corec_thmss]}
+ co_rec_thms = co_rec_thms, disc_co_recs = disc_corec_thms,
+ sel_co_recss = sel_corec_thmss}
|> morph_fp_sugar phi;
val target_fp_sugars =
- map17 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
- co_iterss mapss (transpose co_inductss) un_fold_thmss co_rec_thmss disc_unfold_thmss
- disc_corec_thmss sel_unfold_thmsss sel_corec_thmsss;
+ map14 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;
val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
in
--- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Mon Mar 03 15:14:00 2014 +0100
@@ -34,11 +34,10 @@
val permute_args: int -> term -> term
val mk_partial_compN: int -> typ -> term -> term
- val mk_partial_comp: typ -> typ -> term -> term
val mk_compN: int -> typ list -> term * term -> term
val mk_comp: typ list -> term * term -> term
- val mk_co_iter: theory -> fp_kind -> typ -> typ list -> term -> term
+ val mk_co_rec: theory -> fp_kind -> typ -> typ list -> term -> term
val mk_conjunctN: int -> int -> thm
val conj_dests: int -> thm -> thm list
@@ -93,13 +92,10 @@
fun permute_args n t =
list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n);
-fun mk_partial_comp gT fT g = fst (Term.dest_comb (HOLogic.mk_comp (g, Free (Name.uu, fT))));
+fun mk_partial_comp fT g = fst (Term.dest_comb (HOLogic.mk_comp (g, Free (Name.uu, fT))));
fun mk_partial_compN 0 _ g = g
- | mk_partial_compN n fT g =
- let val g' = mk_partial_compN (n - 1) (range_type fT) g in
- mk_partial_comp (fastype_of g') fT g'
- end;
+ | mk_partial_compN n fT g = mk_partial_comp fT (mk_partial_compN (n - 1) (range_type fT) g);
fun mk_compN n bound_Ts (g, f) =
let val typof = curry fastype_of1 bound_Ts in
@@ -108,7 +104,7 @@
val mk_comp = mk_compN 1;
-fun mk_co_iter thy fp fpT Cs t =
+fun mk_co_rec thy fp fpT Cs t =
let
val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last;
val fpT0 = fp_case fp prebody body;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 03 15:14:00 2014 +0100
@@ -13,7 +13,8 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
- xtor_co_iterss: term list list,
+ xtor_co_folds: term list,
+ xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
ctor_dtors: thm list,
@@ -22,16 +23,18 @@
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
- xtor_co_iter_thmss: thm list list,
- xtor_co_iter_o_map_thmss: thm list list,
+ xtor_co_fold_thms: thm list,
+ xtor_co_rec_thms: thm list,
+ xtor_co_fold_o_map_thms: thm list,
+ xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm}
val morph_fp_result: morphism -> fp_result -> fp_result
- val un_fold_of: 'a list -> 'a
- val co_rec_of: 'a list -> 'a
val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
+ val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
+
val IITN: string
val LevN: string
val algN: string
@@ -60,8 +63,6 @@
val ctor_relN: string
val ctor_set_inclN: string
val ctor_set_set_inclN: string
- val disc_unfoldN: string
- val disc_unfold_iffN: string
val disc_corecN: string
val disc_corec_iffN: string
val dtorN: string
@@ -85,7 +86,6 @@
val dtor_unfold_transferN: string
val dtor_unfold_uniqueN: string
val exhaustN: string
- val foldN: string
val hsetN: string
val hset_recN: string
val inductN: string
@@ -106,7 +106,6 @@
val sel_corecN: string
val set_inclN: string
val set_set_inclN: string
- val sel_unfoldN: string
val setN: string
val simpsN: string
val strTN: string
@@ -114,7 +113,6 @@
val strong_coinductN: string
val sum_bdN: string
val sum_bdTN: string
- val unfoldN: string
val uniqueN: string
(* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *)
@@ -164,7 +162,8 @@
val mk_sum_caseN: int -> int -> thm
val mk_sum_caseN_balanced: int -> int -> thm
- val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
+ val mk_sum_Cinfinite: thm list -> thm
+ val mk_sum_card_order: thm list -> thm
val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
term list -> term list -> term list -> term list -> term list ->
@@ -195,7 +194,8 @@
bnfs: BNF_Def.bnf list,
ctors: term list,
dtors: term list,
- xtor_co_iterss: term list list,
+ xtor_co_folds: term list,
+ xtor_co_recs: term list,
xtor_co_induct: thm,
dtor_ctors: thm list,
ctor_dtors: thm list,
@@ -204,18 +204,22 @@
xtor_map_thms: thm list,
xtor_set_thmss: thm list list,
xtor_rel_thms: thm list,
- xtor_co_iter_thmss: thm list list,
- xtor_co_iter_o_map_thmss: thm list list,
+ xtor_co_fold_thms: thm list,
+ xtor_co_rec_thms: thm list,
+ xtor_co_fold_o_map_thms: thm list,
+ xtor_co_rec_o_map_thms: thm list,
rel_xtor_co_induct_thm: thm};
-fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct, dtor_ctors,
- ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_iter_thmss, xtor_co_iter_o_map_thmss, rel_xtor_co_induct_thm} =
+fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_folds, xtor_co_recs, xtor_co_induct,
+ dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
+ xtor_rel_thms, xtor_co_fold_thms, xtor_co_rec_thms, xtor_co_fold_o_map_thms,
+ xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
dtors = map (Morphism.term phi) dtors,
- xtor_co_iterss = map (map (Morphism.term phi)) xtor_co_iterss,
+ xtor_co_folds = map (Morphism.term phi) xtor_co_folds,
+ xtor_co_recs = map (Morphism.term phi) xtor_co_recs,
xtor_co_induct = Morphism.thm phi xtor_co_induct,
dtor_ctors = map (Morphism.thm phi) dtor_ctors,
ctor_dtors = map (Morphism.thm phi) ctor_dtors,
@@ -224,13 +228,12 @@
xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
- xtor_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss,
- xtor_co_iter_o_map_thmss = map (map (Morphism.thm phi)) xtor_co_iter_o_map_thmss,
+ xtor_co_fold_thms = map (Morphism.thm phi) xtor_co_fold_thms,
+ xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
+ xtor_co_fold_o_map_thms = map (Morphism.thm phi) xtor_co_fold_o_map_thms,
+ 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};
-fun un_fold_of [f, _] = f;
-fun co_rec_of [_, r] = r;
-
fun time ctxt timer msg = (if Config.get ctxt bnf_timing
then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
"ms")
@@ -322,10 +325,8 @@
val caseN = "case"
val discN = "disc"
-val disc_unfoldN = discN ^ "_" ^ unfoldN
val disc_corecN = discN ^ "_" ^ corecN
val iffN = "_iff"
-val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
val distinctN = "distinct"
val rel_distinctN = relN ^ "_" ^ distinctN
@@ -334,7 +335,6 @@
val rel_coinductN = relN ^ "_" ^ coinductN
val rel_inductN = relN ^ "_" ^ inductN
val selN = "sel"
-val sel_unfoldN = selN ^ "_" ^ unfoldN
val sel_corecN = selN ^ "_" ^ corecN
fun co_prefix fp = (if fp = Greatest_FP then "co" else "");
@@ -474,6 +474,12 @@
Balanced_Tree.access {left = mk_sum_step @{thm sum.case(1)} @{thm case_sum_step(1)},
right = mk_sum_step @{thm sum.case(2)} @{thm case_sum_step(2)}, init = refl} n k;
+fun mk_sum_Cinfinite [thm] = thm
+ | mk_sum_Cinfinite (thm :: thms) = @{thm Cinfinite_csum_weak} OF [thm, mk_sum_Cinfinite thms];
+
+fun mk_sum_card_order [thm] = thm
+ | mk_sum_card_order (thm :: thms) = @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
+
fun mk_rel_xtor_co_induct_thm fp pre_rels pre_phis rels phis xs ys xtors xtor's tac lthy =
let
val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 03 15:14:00 2014 +0100
@@ -953,17 +953,8 @@
val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
- fun mk_sum_Cinfinite [thm] = thm
- | mk_sum_Cinfinite (thm :: thms) =
- @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
-
val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
val sum_Card_order = sum_Cinfinite RS conjunct2;
-
- fun mk_sum_card_order [thm] = thm
- | mk_sum_card_order (thm :: thms) =
- @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
-
val sum_card_order = mk_sum_card_order bd_card_orders;
val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
@@ -2609,16 +2600,13 @@
val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
in
timer;
- ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors,
- xtor_co_iterss = transpose [unfolds, corecs],
- xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
- ctor_dtors = ctor_dtor_thms,
- ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
+ ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_co_folds = unfolds,
+ xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
+ ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
- xtor_rel_thms = dtor_Jrel_thms,
- xtor_co_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms],
- xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_Jmap_thms, dtor_corec_o_Jmap_thms],
- rel_xtor_co_induct_thm = Jrel_coinduct_thm},
+ xtor_rel_thms = dtor_Jrel_thms, xtor_co_fold_thms = dtor_unfold_thms,
+ xtor_co_rec_thms = dtor_corec_thms, xtor_co_fold_o_map_thms = dtor_unfold_o_Jmap_thms,
+ xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm},
lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)) |> snd)
end;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Mar 03 15:14:00 2014 +0100
@@ -94,7 +94,7 @@
fun unexpected_corec_call ctxt t =
error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
-fun order_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs)
+fun sort_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs);
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
@@ -374,9 +374,8 @@
let
val thy = Proof_Context.theory_of lthy0;
- val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, co_iters = coiter1 :: _,
- common_co_inducts = common_coinduct_thms, ...} :: _,
- (_, gfp_sugar_thms)), lthy) =
+ val ((missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs,
+ common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
@@ -394,7 +393,7 @@
val perm_Ts = map #T perm_fp_sugars;
val perm_Xs = map #X perm_fp_sugars;
- val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o #co_iters) perm_fp_sugars;
+ val perm_Cs = map (domain_type o body_fun_type o fastype_of o #co_rec) perm_fp_sugars;
val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
@@ -403,7 +402,7 @@
SOME (T, C) => [T, C]
| NONE => [U]);
- val perm_p_Tss = mk_coiter_p_pred_types perm_Cs perm_ns';
+ val perm_p_Tss = mk_corec_p_pred_types perm_Cs perm_ns';
val perm_f_Tssss =
map2 (fn C => map (map (map (curry (op -->) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss';
val perm_q_Tssss =
@@ -454,27 +453,22 @@
end;
fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...}
- : ctr_sugar) p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss sel_coitersss =
- let
- val p_ios = map SOME p_is @ [NONE];
- val corec_thms = co_rec_of coiter_thmss;
- val disc_corecs = co_rec_of disc_coiterss;
- val sel_corecss = co_rec_of sel_coitersss;
- in
+ : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms disc_corecs sel_corecss =
+ let val p_ios = map SOME p_is @ [NONE] in
map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
disc_excludesss collapses corec_thms disc_corecs sel_corecss
end;
- fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_iters = coiters,
- co_iter_thmss = coiter_thmss, disc_co_iterss = disc_coiterss,
- sel_co_itersss = sel_coitersss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
- {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of coiters),
+ fun mk_spec ({T, ctr_sugar as {disc_exhausts, ...}, co_rec = corec,
+ co_rec_thms = corec_thms, disc_co_recs = disc_corecs,
+ sel_co_recss = sel_corecss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
+ {corec = mk_co_rec thy Greatest_FP (substAT T) perm_Cs' corec,
disc_exhausts = disc_exhausts,
nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs,
nested_map_idents = map (unfold_thms lthy @{thms id_def} o map_id0_of_bnf) nested_bnfs,
nested_map_comps = map map_comp_of_bnf nested_bnfs,
- ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss coiter_thmss disc_coiterss
- sel_coitersss};
+ ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms disc_corecs
+ sel_corecss};
in
((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
@@ -929,8 +923,8 @@
val frees = map (fst #>> Binding.name_of #> Free) fixes;
val has_call = exists_subterm (member (op =) frees);
val eqns_data =
- fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (tag_list 0 (map snd specs))
- of_specs_opt []
+ fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss)
+ (tag_list 0 (map snd specs)) of_specs_opt []
|> flat o fst;
val callssss =
@@ -1270,14 +1264,14 @@
val disc_alistss = map3 (map oo prove_disc) corec_specs excludessss disc_eqnss;
val disc_alists = map (map snd o flat) disc_alistss;
val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss;
- val disc_thmss = map (map snd o order_list_duplicates o flat) disc_alistss;
+ val disc_thmss = map (map snd o sort_list_duplicates o flat) disc_alistss;
val disc_thmsss' = map (map (map (snd o snd))) disc_alistss;
- val sel_thmss = map (map snd o order_list_duplicates) sel_alists;
+ val sel_thmss = map (map snd o sort_list_duplicates) sel_alists;
fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
(({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
- if null exhaust_thms orelse null (tl ctr_specs) then
+ if null exhaust_thms orelse null disc_thms then
[]
else
let
@@ -1291,7 +1285,7 @@
(the_single exhaust_thms) disc_thms disc_thmss' (flat disc_excludess)
|> K |> Goal.prove_sorry lthy [] [] goal
|> Thm.close_derivation
- |> fold (fn rule => perhaps (try (fn thm => thm RS rule)))
+ |> fold (fn rule => perhaps (try (fn thm => Meson.first_order_resolve thm rule)))
@{thms eqTrueE eq_False[THEN iffD1] notnotD}
|> pair eqn_pos
|> single
@@ -1299,10 +1293,10 @@
val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss
- |> map order_list_duplicates;
+ |> map sort_list_duplicates;
- val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists) disc_eqnss
- sel_eqnss ctr_specss;
+ val ctr_alists = map5 (maps oooo prove_ctr) disc_alists (map (map snd) sel_alists)
+ disc_eqnss sel_eqnss ctr_specss;
val ctr_thmss' = map (map snd) ctr_alists;
val ctr_thmss = map (map snd o order_list) ctr_alists;
@@ -1315,11 +1309,15 @@
val common_name = mk_common_name fun_names;
+ val anonymous_notes =
+ [(flat disc_iff_or_disc_thmss, simp_attrs)]
+ |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
val notes =
[(coinductN, map (if n2m then single else K []) coinduct_thms, []),
(codeN, code_thmss, code_nitpicksimp_attrs),
(ctrN, ctr_thmss, []),
- (discN, disc_thmss, simp_attrs),
+ (discN, disc_thmss, []),
(disc_iffN, disc_iff_thmss, []),
(excludeN, exclude_thmss, []),
(exhaustN, nontriv_exhaust_thmss, []),
@@ -1343,7 +1341,7 @@
|> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat sel_thmss)
|> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat ctr_thmss)
|> Spec_Rules.add Spec_Rules.Equational (map fst def_infos, flat code_thmss)
- |> Local_Theory.notes (notes @ common_notes)
+ |> Local_Theory.notes (anonymous_notes @ notes @ common_notes)
|> snd
end;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 03 15:14:00 2014 +0100
@@ -587,17 +587,8 @@
val Abs_sbdT_inj = mk_Abs_inj_thm (#Abs_inject sbdT_loc_info);
val Abs_sbdT_bij = mk_Abs_bij_thm lthy Abs_sbdT_inj (#Abs_cases sbdT_loc_info);
- fun mk_sum_Cinfinite [thm] = thm
- | mk_sum_Cinfinite (thm :: thms) =
- @{thm Cinfinite_csum_strong} OF [thm, mk_sum_Cinfinite thms];
-
val sum_Cinfinite = mk_sum_Cinfinite bd_Cinfinites;
val sum_Card_order = sum_Cinfinite RS conjunct2;
-
- fun mk_sum_card_order [thm] = thm
- | mk_sum_card_order (thm :: thms) =
- @{thm card_order_csum} OF [thm, mk_sum_card_order thms];
-
val sum_card_order = mk_sum_card_order bd_card_orders;
val sbd_ordIso = @{thm ssubst_Pair_rhs} OF
@@ -1863,14 +1854,13 @@
val maybe_conceal_notes = note_all = false ? map (apfst (apfst Binding.conceal));
in
timer;
- ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs],
- xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
- ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
+ ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_folds = folds,
+ xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
+ ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
- xtor_rel_thms = ctor_Irel_thms,
- xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms],
- xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_Imap_thms, ctor_rec_o_Imap_thms],
- rel_xtor_co_induct_thm = Irel_induct_thm},
+ xtor_rel_thms = ctor_Irel_thms, xtor_co_fold_thms = ctor_fold_thms,
+ xtor_co_rec_thms = ctor_rec_thms, xtor_co_fold_o_map_thms = ctor_fold_o_Imap_thms,
+ xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm},
lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd)
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Mar 03 15:14:00 2014 +0100
@@ -146,8 +146,8 @@
(kk, (T_name, map (mk_dtyp (map snd (take 1 parents))) Ts, map2 (mk_ctr_descr Ts) kksss ctrs0));
val descr = map3 mk_typ_descr kkssss Tparentss ctrss0;
- val recs = map (fst o dest_Const o co_rec_of o #co_iters) fp_sugars;
- val rec_thms = maps (co_rec_of o #co_iter_thmss) fp_sugars;
+ val recs = map (fst o dest_Const o #co_rec) fp_sugars;
+ val rec_thms = maps #co_rec_thms fp_sugars;
fun mk_info (kk, {T = Type (T_name0, _), ctr_sugar = {casex, exhaust, nchotomy, injects,
distincts, case_thms, case_cong, weak_case_cong, split, split_asm, ...}, ...} : fp_sugar) =
@@ -163,7 +163,7 @@
val all_notes =
(case lfp_sugar_thms of
NONE => []
- | SOME ((induct_thms, induct_thm, induct_attrs), (fold_thmss, rec_thmss, _)) =>
+ | SOME ((induct_thms, induct_thm, induct_attrs), (rec_thmss, _)) =>
let
val common_notes =
(if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else [])
@@ -172,8 +172,7 @@
((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));
val notes =
- [(foldN, fold_thmss, []),
- (inductN, map single induct_thms, induct_attrs),
+ [(inductN, map single induct_thms, induct_attrs),
(recN, rec_thmss, code_nitpicksimp_simp_attrs)]
|> filter_out (null o #2)
|> maps (fn (thmN, thmss, attrs) =>
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Mar 03 15:14:00 2014 +0100
@@ -190,7 +190,7 @@
fun mk_spec ctr_offset
({T, fp_res_index, ctr_sugar = {ctrs, ...}, recx, rec_thms, ...} : basic_lfp_sugar) =
- {recx = mk_co_iter thy Least_FP (substAT T) perm_Cs' recx,
+ {recx = mk_co_rec thy Least_FP (substAT T) perm_Cs' recx,
nested_map_idents = nested_map_idents, nested_map_comps = nested_map_comps,
ctr_specs = mk_ctr_specs fp_res_index ctr_offset ctrs rec_thms};
in
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Mon Mar 03 15:14:00 2014 +0100
@@ -21,10 +21,10 @@
fun is_new_datatype ctxt s =
(case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false);
-fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_iters = iters,
- co_iter_thmss = iter_thmss, ...} : fp_sugar) =
+fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_defs, ctr_sugar, co_rec = recx,
+ co_rec_thms = rec_thms, ...} : fp_sugar) =
{T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_defs = ctr_defs,
- ctr_sugar = ctr_sugar, recx = co_rec_of iters, rec_thms = co_rec_of iter_thmss};
+ ctr_sugar = ctr_sugar, recx = recx, rec_thms = rec_thms};
fun get_basic_lfp_sugars bs arg_Ts callers callssss0 lthy0 =
let
@@ -35,7 +35,7 @@
val Ts = map #T fp_sugars;
val Xs = map #X fp_sugars;
- val Cs = map (body_type o fastype_of o co_rec_of o #co_iters) fp_sugars;
+ val Cs = map (body_type o fastype_of o #co_rec) fp_sugars;
val Xs_TCs = Xs ~~ (Ts ~~ Cs);
fun zip_recT (Type (s, Us)) = [Type (s, map (HOLogic.mk_tupleT o zip_recT) Us)]
--- a/src/HOL/Tools/BNF/bnf_util.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Mar 03 15:14:00 2014 +0100
@@ -35,19 +35,6 @@
'o) ->
'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
- val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
- '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 map17: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
- 'o -> 'p -> 'q -> 'r) ->
- '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 -> 'r 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) ->
@@ -216,29 +203,6 @@
map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s
| map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-fun map15 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
- | map15 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) =
- f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ::
- 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 map17 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
- | map17 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) (x17::x17s) =
- f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 ::
- map17 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s x17s
- | map17 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
fun fold_map4 _ [] [] [] [] acc = ([], acc)
| fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
let
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Mar 03 15:14:00 2014 +0100
@@ -1775,17 +1775,24 @@
raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
\(\"" ^ s ^ "\")")
else if is_quot_abs_fun ctxt x then
- let
- val rep_T = domain_type T
- val abs_T = range_type T
- in
- (Abs (Name.uu, rep_T,
- Const (@{const_name Quot}, rep_T --> abs_T)
- $ (Const (quot_normal_name_for_type ctxt abs_T,
- rep_T --> rep_T) $ Bound 0)), ts)
- end
+ case T of
+ Type (@{type_name fun}, [rep_T, abs_T as Type (abs_s, _)]) =>
+ if is_basic_datatype thy [(NONE, true)] abs_s then
+ raise NOT_SUPPORTED ("abstraction function on " ^
+ quote abs_s)
+ else
+ (Abs (Name.uu, rep_T,
+ Const (@{const_name Quot}, rep_T --> abs_T)
+ $ (Const (quot_normal_name_for_type ctxt abs_T,
+ rep_T --> rep_T) $ Bound 0)), ts)
else if is_quot_rep_fun ctxt x then
- quot_rep_of depth Ts (domain_type T) (range_type T) ts
+ case T of
+ Type (@{type_name fun}, [abs_T as Type (abs_s, _), rep_T]) =>
+ if is_basic_datatype thy [(NONE, true)] abs_s then
+ raise NOT_SUPPORTED ("representation function on " ^
+ quote abs_s)
+ else
+ quot_rep_of depth Ts abs_T rep_T ts
else if is_record_get thy x then
case length ts of
0 => (do_term depth Ts (eta_expand Ts t 1), [])
--- a/src/HOL/ex/Refute_Examples.thy Mon Mar 03 13:54:47 2014 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Mon Mar 03 15:14:00 2014 +0100
@@ -547,18 +547,6 @@
refute [expect = genuine]
oops
-lemma "rec_option n s None = n"
-refute [expect = none]
-by simp
-
-lemma "rec_option n s (Some x) = s x"
-refute [maxsize = 4, expect = none]
-by simp
-
-lemma "P (rec_option n s x)"
-refute [expect = genuine]
-oops
-
lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
refute [expect = genuine]
oops