# HG changeset patch # User wenzelm # Date 1393856040 -3600 # Node ID b11b358fec5762373d5bc8af533d59d7fdd19cf5 # Parent 6478b12b7297ee118950100211c3160531f25c54# Parent c871a2e751ec8a6da32d35bc6d8de030dafae615 merged; diff -r c871a2e751ec -r b11b358fec57 NEWS --- 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 diff -r c871a2e751ec -r b11b358fec57 src/Doc/Datatypes/Datatypes.thy --- 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} diff -r c871a2e751ec -r b11b358fec57 src/HOL/BNF_Cardinal_Arithmetic.thy --- 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 \ Cinfinite r2 \ 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: "\Cinfinite r1; Cinfinite r2\ \ Cinfinite (r1 +c r2)" by (erule Cinfinite_csum1) @@ -335,6 +335,9 @@ lemma cprod_mono2: "p2 \o r2 \ q *c p2 \o q *c r2" by (simp only: cprod_def ordLeq_Times_mono2) +lemma cprod_mono: "\p1 \o r1; p2 \o r2\ \ p1 *c p2 \o r1 *c r2" +by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2]) + lemma ordLeq_cprod2: "\Cnotzero p1; Card_order p2\ \ p2 \o p1 *c p2" unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI) @@ -347,6 +350,15 @@ lemma Cinfinite_cprod2: "\Cnotzero r1; Cinfinite r2\ \ Cinfinite (r1 *c r2)" by (blast intro: cinfinite_cprod2 Card_order_cprod) +lemma cprod_cong: "\p1 =o r1; p2 =o r2\ \ p1 *c p2 =o r1 *c r2" +unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono) + +lemma cprod_cong1: "\p1 =o r1\ \ p1 *c p2 =o r1 *c p2" +unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono1) + +lemma cprod_cong2: "p2 =o r2 \ 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 \ 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 \o r2" diff -r c871a2e751ec -r b11b358fec57 src/HOL/BNF_Comp.thy --- 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 \ 'a" where "id_bnf_comp = (\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 \ Card_order r \ p +c p' =o r +c r \ p +c p' =o r" +apply (erule ordIso_transitive) +apply (frule csum_absorb2') +apply (erule ordLeq_refl) +by simp + +lemma cprod_dup: "cinfinite r \ Card_order r \ p *c p' =o r *c r \ 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 diff -r c871a2e751ec -r b11b358fec57 src/HOL/BNF_Examples/Derivation_Trees/DTree.thy --- 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 \ NNode n (the_inv fset as)" definition "cont \ fset o ccont" -definition "unfold rt ct \ unfold_dtree rt (the_inv fset o ct)" +definition "unfold rt ct \ corec_dtree rt (the_inv fset o image (sum_map id Inr) o ct)" definition "corec rt ct \ 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) \ cont (unfold rt ct b) = image (id \ unfold rt ct) (ct b)" -using dtree.sel_unfold[of rt "the_inv fset \ 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) \ cont (corec rt ct b) = image (id \ ([[id, corec rt ct]])) (ct b)" using dtree.sel_corec[of rt "the_inv fset \ ct" b] unfolding corec_def -apply - -apply simp unfolding cont_def comp_def id_def -by simp +by simp_all end diff -r c871a2e751ec -r b11b358fec57 src/HOL/BNF_Examples/Misc_Primcorec.thy --- 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 \ 'a bin_rose_tree mylist" and id_trees2 :: "'a bin_rose_tree mylist \ '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' \ 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 \ MyNil + | MyCons t ts \ 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 \ MyNil + | MyCons t ts \ MyCons (id_tree t) (id_trees2 ts))" primcorec trunc_tree :: "'a bin_rose_tree \ 'a bin_rose_tree" and trunc_trees1 :: "'a bin_rose_tree mylist \ 'a bin_rose_tree mylist" and trunc_trees2 :: "'a bin_rose_tree mylist \ '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' \ BRTree a (trunc_trees1 ts) (trunc_trees2 ts'))" | "trunc_trees1 ts = (case ts of - MyNil => MyNil - | MyCons t _ => MyCons (trunc_tree t) MyNil)" | + MyNil \ MyNil + | MyCons t _ \ MyCons (trunc_tree t) MyNil)" | "trunc_trees2 ts = (case ts of - MyNil => MyNil - | MyCons t ts => MyCons (trunc_tree t) MyNil)" + MyNil \ MyNil + | MyCons t ts \ MyCons (trunc_tree t) MyNil)" primcorec freeze_exp :: "('b \ 'a) \ ('a, 'b) exp \ ('a, 'b) exp" and diff -r c871a2e751ec -r b11b358fec57 src/HOL/BNF_Examples/Stream.thy --- 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 \ 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' \ set2_pre_stream (dtor_stream s)" and prems: "a \ 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 diff -r c871a2e751ec -r b11b358fec57 src/HOL/BNF_FP_Base.thy --- 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 diff -r c871a2e751ec -r b11b358fec57 src/HOL/BNF_LFP.thy --- 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: "\(r, s) \ R; s' = s\ \ (r, s') \ R" - by simp + by (rule ssubst) ML_file "Tools/BNF/bnf_lfp_util.ML" ML_file "Tools/BNF/bnf_lfp_tactics.ML" diff -r c871a2e751ec -r b11b358fec57 src/HOL/Cardinals/Cardinal_Arithmetic.thy --- 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 \ q *c p2 =o q *c r2" -by (simp only: cprod_def ordIso_Times_cong2) lemma ordLeq_cprod1: "\Card_order p1; Cnotzero p2\ \ p1 \o p1 *c p2" unfolding cprod_def by (metis Card_order_Times1 czeroI) -lemma cprod_infinite: "Cinfinite r \ r *c r =o r" -using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast - -lemma cprod_mono: "\p1 \o r1; p2 \o r2\ \ p1 *c p2 \o r1 *c r2" - by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2]) - subsection {* Exponentiation *} diff -r c871a2e751ec -r b11b358fec57 src/HOL/Nitpick_Examples/Refute_Nits.thy --- 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 \ n | Some u \ s u)" nitpick [expect = genuine] oops diff -r c871a2e751ec -r b11b358fec57 src/HOL/Option.thy --- 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 *} diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_comp.ML --- 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') = diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_comp_tactics.ML --- 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; diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_def.ML --- 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 diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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")); diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- 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' diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- 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 diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- 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 diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- 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; diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_fp_util.ML --- 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; diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_gfp.ML --- 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; diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- 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; diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_lfp.ML --- 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; diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- 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) => diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- 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 diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- 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)] diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/BNF/bnf_util.ML --- 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 diff -r c871a2e751ec -r b11b358fec57 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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), []) diff -r c871a2e751ec -r b11b358fec57 src/HOL/ex/Refute_Examples.thy --- 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 \ n | Some u \ s u)" refute [expect = genuine] oops