# HG changeset patch # User blanchet # Date 1392795273 -3600 # Node ID a5e33e18fb5c06f2d9c03e170d7f2ab73d65ed7b # Parent 4a940ebceef8997d936b2eb65203776d86c3dd85 moved 'primrec' up (for real this time) and removed temporary 'old_primrec' diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/BNF_FP_Base.thy Wed Feb 19 08:34:33 2014 +0100 @@ -149,7 +149,6 @@ unfolding Grp_def by rule auto ML_file "Tools/BNF/bnf_fp_util.ML" -ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML" ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" ML_file "Tools/BNF/bnf_fp_def_sugar.ML" ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML" diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/BNF_LFP.thy --- a/src/HOL/BNF_LFP.thy Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/BNF_LFP.thy Wed Feb 19 08:34:33 2014 +0100 @@ -13,8 +13,7 @@ imports BNF_FP_Base keywords "datatype_new" :: thy_decl and - "datatype_compat" :: thy_decl and - "primrec" :: thy_decl + "datatype_compat" :: thy_decl begin lemma subset_emptyI: "(\x. x \ A \ False) \ A \ {}" @@ -241,7 +240,6 @@ ML_file "Tools/BNF/bnf_lfp_tactics.ML" ML_file "Tools/BNF/bnf_lfp.ML" ML_file "Tools/BNF/bnf_lfp_compat.ML" -ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML" ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" hide_fact (open) id_transfer diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Inductive.thy Wed Feb 19 08:34:33 2014 +0100 @@ -11,7 +11,7 @@ "inductive_cases" "inductive_simps" :: thy_script and "monos" and "print_inductives" :: diag and "rep_datatype" :: thy_goal and - "old_primrec" :: thy_decl + "primrec" :: thy_decl begin subsection {* Least and greatest fixed points *} @@ -277,6 +277,9 @@ ML_file "Tools/Datatype/datatype_codegen.ML" ML_file "Tools/Datatype/primrec.ML" +ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML" +ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML" + text{* Lambda-abstractions with pattern matching: *} syntax diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Nat.thy Wed Feb 19 08:34:33 2014 +0100 @@ -187,7 +187,7 @@ instantiation nat :: comm_monoid_diff begin -old_primrec plus_nat where +primrec plus_nat where add_0: "0 + n = (n\nat)" | add_Suc: "Suc m + n = Suc (m + n)" @@ -202,7 +202,7 @@ lemma add_Suc_shift [code]: "Suc m + n = m + Suc n" by simp -old_primrec minus_nat where +primrec minus_nat where diff_0 [code]: "m - 0 = (m\nat)" | diff_Suc: "m - Suc n = (case m - n of 0 => 0 | Suc k => k)" @@ -235,7 +235,7 @@ definition One_nat_def [simp]: "1 = Suc 0" -old_primrec times_nat where +primrec times_nat where mult_0: "0 * n = (0\nat)" | mult_Suc: "Suc m * n = n + (m * n)" @@ -414,7 +414,7 @@ instantiation nat :: linorder begin -old_primrec less_eq_nat where +primrec less_eq_nat where "(0\nat) \ n \ True" | "Suc m \ n \ (case n of 0 \ False | Suc n \ m \ n)" @@ -1303,7 +1303,7 @@ funpow == "compow :: nat \ ('a \ 'a) \ ('a \ 'a)" begin -old_primrec funpow :: "nat \ ('a \ 'a) \ 'a \ 'a" where +primrec funpow :: "nat \ ('a \ 'a) \ 'a \ 'a" where "funpow 0 f = id" | "funpow (Suc n) f = f o funpow n f" @@ -1410,7 +1410,7 @@ lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n" by (induct m) (simp_all add: add_ac distrib_right) -old_primrec of_nat_aux :: "('a \ 'a) \ nat \ 'a \ 'a" where +primrec of_nat_aux :: "('a \ 'a) \ nat \ 'a \ 'a" where "of_nat_aux inc 0 i = i" | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- {* tail recursive *} diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Sum_Type.thy Wed Feb 19 08:34:33 2014 +0100 @@ -120,7 +120,7 @@ setup {* Sign.parent_path *} -old_primrec sum_map :: "('a \ 'c) \ ('b \ 'd) \ 'a + 'b \ 'c + 'd" where +primrec sum_map :: "('a \ 'c) \ ('b \ 'd) \ 'a + 'b \ 'c + 'd" where "sum_map f1 f2 (Inl a) = Inl (f1 a)" | "sum_map f1 f2 (Inr a) = Inr (f2 a)" @@ -177,10 +177,10 @@ qed qed -old_primrec Suml :: "('a \ 'c) \ 'a + 'b \ 'c" where +primrec Suml :: "('a \ 'c) \ 'a + 'b \ 'c" where "Suml f (Inl x) = f x" -old_primrec Sumr :: "('b \ 'c) \ 'a + 'b \ 'c" where +primrec Sumr :: "('b \ 'c) \ 'a + 'b \ 'c" where "Sumr f (Inr x) = f x" lemma Suml_inject: diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 19 08:34:33 2014 +0100 @@ -9,7 +9,7 @@ sig type fp_sugar = {T: typ, - fp: BNF_FP_Util.fp_kind, + fp: BNF_Util.fp_kind, fp_res_index: int, fp_res: BNF_FP_Util.fp_result, pre_bnf: BNF_Def.bnf, @@ -53,7 +53,7 @@ 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_FP_Util.fp_kind -> typ list list list -> typ list -> typ list -> + val mk_co_iters_prelims: BNF_Util.fp_kind -> typ list list 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 @@ -89,12 +89,12 @@ ((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) * ((binding, binding * typ, term) Ctr_Sugar.ctr_spec * mixfix) list - val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list -> + val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list -> binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) -> (bool * bool) * co_datatype_spec list -> local_theory -> local_theory - val parse_co_datatype_cmd: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list -> + val parse_co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list -> binding list list -> binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory) -> (local_theory -> local_theory) parser @@ -259,6 +259,11 @@ 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]; + fun unzip_corecT (Type (@{type_name sum}, _)) T = [T] | unzip_corecT _ (Type (@{type_name sum}, Ts)) = Ts | unzip_corecT _ T = [T]; @@ -339,6 +344,8 @@ val transfer_gfp_sugar_thms = morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of; +fun mk_iter_fun_arg_types n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type; + fun mk_iters_args_types ctr_Tsss Cs ns mss ctor_iter_fun_Tss lthy = let val Css = map2 replicate ns Cs; diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Tools/BNF/bnf_fp_n2m.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Feb 19 08:34:33 2014 +0100 @@ -7,7 +7,7 @@ signature BNF_FP_N2M = sig - val construct_mutualized_fp: BNF_FP_Util.fp_kind -> typ list -> BNF_FP_Def_Sugar.fp_sugar list -> + val construct_mutualized_fp: BNF_Util.fp_kind -> typ list -> BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> BNF_FP_Util.fp_result * local_theory end; diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 19 08:34:33 2014 +0100 @@ -10,12 +10,12 @@ val unfold_lets_splits: term -> term val dest_map: Proof.context -> string -> term -> term * term list - val mutualize_fp_sugars: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) -> + val mutualize_fp_sugars: BNF_Util.fp_kind -> binding list -> typ list -> (term -> int list) -> term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory -> (BNF_FP_Def_Sugar.fp_sugar list * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) * local_theory - val nested_to_mutual_fps: BNF_FP_Util.fp_kind -> binding list -> typ list -> (term -> int list) -> + val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> (term -> int list) -> (term * term list list) list list -> local_theory -> (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list * (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option)) diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Wed Feb 19 08:34:33 2014 +0100 @@ -7,7 +7,7 @@ signature BNF_FP_N2M_TACTICS = sig - val mk_rel_xtor_co_induct_tactic: BNF_FP_Util.fp_kind -> thm list -> thm list -> thm list -> + val mk_rel_xtor_co_induct_tactic: BNF_Util.fp_kind -> thm list -> thm list -> thm list -> {prems: thm list, context: Proof.context} -> tactic end; diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Wed Feb 19 08:34:33 2014 +0100 @@ -8,31 +8,56 @@ signature BNF_FP_REC_SUGAR_UTIL = sig + datatype fp_kind = Least_FP | Greatest_FP + + val fp_case: fp_kind -> 'a -> 'a -> 'a + + val flat_rec_arg_args: 'a list list -> 'a list + val indexed: 'a list -> int -> int list * int val indexedd: 'a list list -> int -> int list list * int val indexeddd: 'a list list list -> int -> int list list list * int val indexedddd: 'a list list list list -> int -> int list list list list * int val find_index_eq: ''a list -> ''a -> int val finds: ('a * 'b -> bool) -> 'a list -> 'b list -> ('a * 'b list) list * 'b list + val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list + val mk_common_name: string list -> string + + val num_binder_types: typ -> int + val exists_subtype_in: typ list -> typ -> bool + val exists_strict_subtype_in: typ list -> typ -> bool val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list + val retype_free: typ -> term -> term val drop_all: term -> term + 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 get_free_indices: ((binding * typ) * 'a) list -> term -> int list + val mk_co_iter: theory -> fp_kind -> typ -> typ list -> term -> term - (* needed here for bootstrapping; would be more at home in "bnf_fp_def_sugar.ML" (FIXME) *) - val unzip_recT: typ -> typ -> typ list - val mk_iter_fun_arg_types: int -> int list -> typ -> typ list list - val flat_rec_arg_args: 'a list list -> 'a list - val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term + val mk_conjunctN: int -> int -> thm + val conj_dests: int -> thm -> thm list end; structure BNF_FP_Rec_Sugar_Util : BNF_FP_REC_SUGAR_UTIL = struct -open BNF_Util -open BNF_FP_Util +datatype fp_kind = Least_FP | Greatest_FP; + +fun fp_case Least_FP l _ = l + | fp_case Greatest_FP _ g = g; + +fun flat_rec_arg_args xss = + (* FIXME (once the old datatype package is phased out): The first line below gives the preferred + order. The second line is for compatibility with the old datatype package. *) + (* flat xss *) + map hd xss @ maps tl xss; fun indexe _ h = (h, h + 1); fun indexed xs = fold_map indexe xs; @@ -44,32 +69,53 @@ fun finds eq = fold_map (fn x => List.partition (curry eq x) #>> pair x); +fun find_indices eq xs ys = + map_filter I (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys); + +val mk_common_name = space_implode "_"; + +(*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*) +fun num_binder_types (Type (@{type_name fun}, [_, T])) = 1 + num_binder_types T + | num_binder_types _ = 0; + +val exists_subtype_in = Term.exists_subtype o member (op =); +fun exists_strict_subtype_in Ts T = exists_subtype_in (filter_out (curry (op =) T) Ts) T; + fun tvar_subst thy Ts Us = Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) []; +fun retype_free T (Free (s, _)) = Free (s, T) + | retype_free _ t = raise TERM ("retype_free", [t]); + fun drop_all t = subst_bounds (strip_qnt_vars @{const_name all} t |> map Free |> rev, strip_qnt_body @{const_name all} t); +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_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; + +fun mk_compN n bound_Ts (g, f) = + let val typof = curry fastype_of1 bound_Ts in + mk_partial_compN n (typof f) g $ f + end; + +val mk_comp = mk_compN 1; + fun get_free_indices fixes t = map (fst #>> Binding.name_of #> Free) fixes |> map_index (fn (i, v) => if exists_subterm (equal v) t then SOME i else NONE) |> map_filter I; -fun unzip_recT (Type (@{type_name prod}, _)) T = [T] - | unzip_recT _ (Type (@{type_name prod}, Ts)) = Ts - | unzip_recT _ T = [T]; - -fun mk_iter_fun_arg_types n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type; - -fun flat_rec_arg_args xss = - (* FIXME (once the old datatype package is phased out): The first line below gives the preferred - order. The second line is for compatibility with the old datatype package. *) - (* flat xss *) - map hd xss @ maps tl xss; - fun mk_co_iter thy fp fpT Cs t = let - val (f_Cs, Type (_, [prebody, body])) = strip_fun_type (fastype_of t); + val ((f_Cs, prebody), body) = strip_type (fastype_of t) |>> split_last; val fpT0 = fp_case fp prebody body; val Cs0 = distinct (op =) (map (fp_case fp body_type domain_type) f_Cs); val rho = tvar_subst thy (fpT0 :: Cs0) (fpT :: Cs); @@ -77,4 +123,11 @@ Term.subst_TVars rho t end; +fun mk_conjunctN 1 1 = @{thm TrueE[OF TrueI]} + | mk_conjunctN _ 1 = conjunct1 + | mk_conjunctN 2 2 = conjunct2 + | mk_conjunctN n m = conjunct2 RS (mk_conjunctN (n - 1) (m - 1)); + +fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n); + end; diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Feb 19 08:34:33 2014 +0100 @@ -8,9 +8,6 @@ signature BNF_FP_UTIL = sig - datatype fp_kind = Least_FP | Greatest_FP - val fp_case: fp_kind -> 'a -> 'a -> 'a - type fp_result = {Ts: typ list, bnfs: BNF_Def.bnf list, @@ -126,10 +123,9 @@ val mk_dtor_set_inductN: int -> string val mk_set_inductN: int -> string - val co_prefix: fp_kind -> string + val co_prefix: BNF_Util.fp_kind -> string val base_name_of_typ: typ -> string - val mk_common_name: string list -> string val split_conj_thm: thm -> thm list val split_conj_prems: int -> thm -> thm @@ -139,11 +135,6 @@ val mk_proj: typ -> int -> int -> 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_convol: term * term -> term val Inl_const: typ -> typ -> term @@ -162,9 +153,6 @@ val dest_sumTN_balanced: int -> typ -> typ list val dest_tupleT: int -> typ -> typ list - val exists_subtype_in: typ list -> typ -> bool - val exists_strict_subtype_in: typ list -> typ -> bool - val If_const: typ -> term val mk_Field: term -> term @@ -179,13 +167,13 @@ val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list - val mk_rel_xtor_co_induct_thm: fp_kind -> term list -> term list -> term list -> term list -> - term list -> term list -> term list -> term list -> + 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 -> ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm - val mk_un_fold_transfer_thms: fp_kind -> term list -> term list -> term list -> term list -> - term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> + val mk_un_fold_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list -> + term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list - val mk_xtor_un_fold_o_map_thms: fp_kind -> bool -> int -> thm -> thm list -> thm list -> + val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list val mk_strong_coinduct_thm: thm -> thm list -> thm list -> Proof.context -> thm @@ -203,11 +191,6 @@ open BNF_Def open BNF_Util -datatype fp_kind = Least_FP | Greatest_FP; - -fun fp_case Least_FP l _ = l - | fp_case Greatest_FP _ g = g; - type fp_result = {Ts: typ list, bnfs: BNF_Def.bnf list, @@ -362,8 +345,6 @@ fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []); -val mk_common_name = space_implode "_"; - fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T'); fun dest_sumTN 1 T = [T] @@ -379,33 +360,11 @@ val mk_sumTN = Library.foldr1 mk_sumT; val mk_sumTN_balanced = Balanced_Tree.make mk_sumT; -val exists_subtype_in = Term.exists_subtype o member (op =); - -fun exists_strict_subtype_in Ts T = exists_subtype_in (filter_out (curry (op =) T) Ts) T; - fun mk_proj T n k = let val (binders, _) = strip_typeN n T in fold_rev (fn T => fn t => Abs (Name.uu, T, t)) binders (Bound (n - k - 1)) end; -fun mk_partial_comp gT fT g = - let val T = domain_type fT --> range_type gT in - Const (@{const_name Fun.comp}, gT --> fT --> T) $ g - end; - -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; - -fun mk_compN n bound_Ts (g, f) = - let val typof = curry fastype_of1 bound_Ts in - mk_partial_compN n (typof f) g $ f - end; - -val mk_comp = mk_compN 1; - fun mk_convol (f, g) = let val (fU, fTU) = `range_type (fastype_of f); diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Feb 19 08:34:33 2014 +0100 @@ -19,12 +19,15 @@ rec_thms: thm list}; type lfp_rec_extension = - {is_new_datatype: Proof.context -> string -> bool, + {nested_simps: thm list, + is_new_datatype: Proof.context -> string -> bool, get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) -> (term * term list list) list list -> local_theory -> typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory, - massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> - typ list -> term -> term -> term -> term}; + rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list -> term -> + term -> term -> term}; + + exception PRIMREC of string * term list; val register_lfp_rec_extension: lfp_rec_extension -> theory -> theory @@ -45,11 +48,13 @@ struct open Ctr_Sugar +open Ctr_Sugar_Util open Ctr_Sugar_General_Tactics -open BNF_Util -open BNF_FP_Util open BNF_FP_Rec_Sugar_Util +val inductN = "induct" +val simpsN = "simps" + val nitpicksimp_attrs = @{attributes [nitpick_simp]}; val simp_attrs = @{attributes [simp]}; val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs; @@ -57,10 +62,6 @@ exception OLD_PRIMREC of unit; exception PRIMREC of string * term list; -fun primrec_error str = raise PRIMREC (str, []); -fun primrec_error_eqn str eqn = raise PRIMREC (str, [eqn]); -fun primrec_error_eqns str eqns = raise PRIMREC (str, eqns); - datatype rec_call = No_Rec of int * typ | Mutual_Rec of (int * typ) * (int * typ) | @@ -89,12 +90,13 @@ rec_thms: thm list}; type lfp_rec_extension = - {is_new_datatype: Proof.context -> string -> bool, + {nested_simps: thm list, + is_new_datatype: Proof.context -> string -> bool, get_basic_lfp_sugars: binding list -> typ list -> (term -> int list) -> (term * term list list) list list -> local_theory -> typ list * int list * basic_lfp_sugar list * thm list * thm list * thm * bool * local_theory, - massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> - typ list -> term -> term -> term -> term}; + rewrite_nested_rec_call: Proof.context -> (term -> bool) -> (string -> int) -> typ list -> term -> + term -> term -> term}; structure Data = Theory_Data ( @@ -106,6 +108,11 @@ val register_lfp_rec_extension = Data.put o SOME; +fun nested_simps ctxt = + (case Data.get (Proof_Context.theory_of ctxt) of + SOME {nested_simps, ...} => nested_simps + | NONE => []); + fun is_new_datatype ctxt = (case Data.get (Proof_Context.theory_of ctxt) of SOME {is_new_datatype, ...} => is_new_datatype ctxt @@ -116,9 +123,9 @@ SOME {get_basic_lfp_sugars, ...} => get_basic_lfp_sugars bs arg_Ts get_indices callssss lthy | NONE => error "Not implemented yet"); -fun massage_nested_rec_call ctxt = +fun rewrite_nested_rec_call ctxt = (case Data.get (Proof_Context.theory_of ctxt) of - SOME {massage_nested_rec_call, ...} => massage_nested_rec_call ctxt); + SOME {rewrite_nested_rec_call, ...} => rewrite_nested_rec_call ctxt); fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy0 = let @@ -193,9 +200,6 @@ val undef_const = Const (@{const_name undefined}, dummyT); -fun permute_args n t = - list_comb (t, map Bound (0 :: (n downto 1))) |> fold (K (Term.abs (Name.uu, dummyT))) (0 upto n); - type eqn_data = { fun_name: string, rec_type: typ, @@ -212,30 +216,30 @@ let val eqn = drop_all eqn' |> HOLogic.dest_Trueprop handle TERM _ => - primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn'; + raise PRIMREC ("malformed function equation (expected \"lhs = rhs\")", [eqn']); val (lhs, rhs) = HOLogic.dest_eq eqn handle TERM _ => - primrec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn'; + raise PRIMREC ("malformed function equation (expected \"lhs = rhs\")", [eqn']); val (fun_name, args) = strip_comb lhs |>> (fn x => if is_Free x then fst (dest_Free x) - else primrec_error_eqn "malformed function equation (does not start with free)" eqn); + else raise PRIMREC ("malformed function equation (does not start with free)", [eqn])); val (left_args, rest) = take_prefix is_Free args; val (nonfrees, right_args) = take_suffix is_Free rest; val num_nonfrees = length nonfrees; val _ = num_nonfrees = 1 orelse if num_nonfrees = 0 then - primrec_error_eqn "constructor pattern missing in left-hand side" eqn else - primrec_error_eqn "more than one non-variable argument in left-hand side" eqn; + raise PRIMREC ("constructor pattern missing in left-hand side", [eqn]) else + raise PRIMREC ("more than one non-variable argument in left-hand side", [eqn]); val _ = member (op =) fun_names fun_name orelse - primrec_error_eqn "malformed function equation (does not start with function name)" eqn + raise PRIMREC ("malformed function equation (does not start with function name)", [eqn]); val (ctr, ctr_args) = strip_comb (the_single nonfrees); val _ = try (num_binder_types o fastype_of) ctr = SOME (length ctr_args) orelse - primrec_error_eqn "partially applied constructor in pattern" eqn; + raise PRIMREC ("partially applied constructor in pattern", [eqn]); val _ = let val d = duplicates (op =) (left_args @ ctr_args @ right_args) in null d orelse - primrec_error_eqn ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^ - "\" in left-hand side") eqn end; + raise PRIMREC ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^ + "\" in left-hand side", [eqn]) end; val _ = forall is_Free ctr_args orelse - primrec_error_eqn "non-primitive pattern in left-hand side" eqn; + raise PRIMREC ("non-primitive pattern in left-hand side", [eqn]); val _ = let val b = fold_aterms (fn x as Free (v, _) => if (not (member (op =) (left_args @ ctr_args @ right_args) x) andalso @@ -243,8 +247,8 @@ not (Variable.is_fixed lthy v)) then cons x else I | _ => I) rhs [] in null b orelse - primrec_error_eqn ("extra variable(s) in right-hand side: " ^ - commas (map (Syntax.string_of_term lthy) b)) eqn + raise PRIMREC ("extra variable(s) in right-hand side: " ^ + commas (map (Syntax.string_of_term lthy) b), [eqn]) end; in {fun_name = fun_name, @@ -258,39 +262,11 @@ user_eqn = eqn'} end; -fun rewrite_map_arg get_ctr_pos rec_type res_type = - let - val pT = HOLogic.mk_prodT (rec_type, res_type); - - fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const pT) - | subst d (Abs (v, T, b)) = - Abs (v, if d = SOME ~1 then pT else T, subst (Option.map (Integer.add 1) d) b) - | subst d t = - let - val (u, vs) = strip_comb t; - val ctr_pos = try (get_ctr_pos o fst o dest_Free) u |> the_default ~1; - in - if ctr_pos >= 0 then - if d = SOME ~1 andalso length vs = ctr_pos then - list_comb (permute_args ctr_pos (snd_const pT), vs) - else if length vs > ctr_pos andalso is_some d - andalso d = try (fn Bound n => n) (nth vs ctr_pos) then - list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs)) - else - primrec_error_eqn ("recursive call not directly applied to constructor argument") t - else - list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs) - end - in - subst (SOME ~1) - end; - fun subst_rec_calls lthy get_ctr_pos has_call ctr_args mutual_calls nested_calls = let fun try_nested_rec bound_Ts y t = AList.lookup (op =) nested_calls y - |> Option.map (fn y' => - massage_nested_rec_call lthy has_call (rewrite_map_arg get_ctr_pos) bound_Ts y y' t); + |> Option.map (fn y' => rewrite_nested_rec_call lthy has_call get_ctr_pos bound_Ts y y' t); fun subst bound_Ts (t as g' $ y) = let @@ -307,7 +283,7 @@ (case try (get_ctr_pos o fst o dest_Free) g of SOME ctr_pos => (length g_args >= ctr_pos orelse - primrec_error_eqn "too few arguments in recursive call" t; + raise PRIMREC ("too few arguments in recursive call", [t]); (case AList.lookup (op =) mutual_calls y of SOME y' => list_comb (y', g_args) | NONE => subst_rec ())) @@ -320,7 +296,7 @@ fun subst' t = if has_call t then (* FIXME detect this case earlier? *) - primrec_error_eqn "recursive call not directly applied to constructor argument" t + raise PRIMREC ("recursive call not directly applied to constructor argument", [t]) else try_nested_rec [] (head_of t) t |> the_default t in @@ -378,9 +354,9 @@ (take n_funs rec_specs |> map #ctr_specs) ~~ funs_data |> maps (uncurry (finds (fn (x, y) => #ctr x = #ctr y)) ##> (fn x => null x orelse - primrec_error_eqns "excess equations in definition" (map #rhs_term x)) #> fst); + raise PRIMREC ("excess equations in definition", map #rhs_term x)) #> fst); val _ = ctr_spec_eqn_data_list' |> map (fn (_, x) => length x <= 1 orelse - primrec_error_eqns ("multiple equations for constructor") (map #user_eqn x)); + raise PRIMREC ("multiple equations for constructor", map #user_eqn x)); val ctr_spec_eqn_data_list = ctr_spec_eqn_data_list' @ (drop n_funs rec_specs |> maps #ctr_specs |> map (rpair [])); @@ -391,8 +367,8 @@ |> map (uncurry (build_rec_arg lthy funs_data has_call) o apsnd (try the_single)); val ctr_poss = map (fn x => if length (distinct ((op =) o pairself (length o #left_args)) x) <> 1 then - primrec_error ("inconstant constructor pattern position for function " ^ - quote (#fun_name (hd x))) + raise PRIMREC ("inconstant constructor pattern position for function " ^ + quote (#fun_name (hd x)), []) else hd x |> #left_args |> length) funs_data; in @@ -435,8 +411,7 @@ fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx = unfold_thms_tac ctxt fun_defs THEN HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN - unfold_thms_tac ctxt (@{thms id_def split comp_def fst_conv snd_conv} @ map_comps @ - map_idents) THEN + unfold_thms_tac ctxt (nested_simps ctxt @ map_comps @ map_idents) THEN HEADGOAL (rtac refl); fun prepare_primrec fixes specs lthy0 = @@ -450,7 +425,7 @@ |> partition_eq ((op =) o pairself #fun_name) |> finds (fn (x, y) => x = #fun_name (hd y)) fun_names |> fst |> map (fn (x, y) => the_single y - handle List.Empty => primrec_error ("missing equations for function " ^ quote x)); + handle List.Empty => raise PRIMREC ("missing equations for function " ^ quote x, [])); val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =)); val arg_Ts = map (#rec_type o hd) funs_data; @@ -466,7 +441,7 @@ val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else (); val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ res_Ts) of [] => () - | (b, _) :: _ => primrec_error ("type of " ^ Binding.print b ^ " contains top sort")); + | (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", [])); val ((n2m, rec_specs, _, induct_thm, induct_thms), lthy) = rec_specs_of bs arg_Ts res_Ts (get_free_indices fixes) callssss lthy0; @@ -476,8 +451,8 @@ val ctrs = maps (map #ctr o #ctr_specs) rec_specs; val _ = map (fn {ctr, user_eqn, ...} => member (op =) ctrs ctr orelse - primrec_error_eqn ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^ - " is not a constructor in left-hand side") user_eqn) eqns_data; + raise PRIMREC ("argument " ^ quote (Syntax.string_of_term lthy ctr) ^ + " is not a constructor in left-hand side", [user_eqn])) eqns_data; val defs = build_defs lthy bs mxs funs_data rec_specs has_call; @@ -508,8 +483,8 @@ val notes = (if n2m then - map2 (fn name => fn thm => - (name, inductN, [thm], [])) fun_names (take actual_nn induct_thms) + map2 (fn name => fn thm => (name, inductN, [thm], [])) fun_names + (take actual_nn induct_thms) else []) |> map (fn (prefix, thmN, thms, attrs) => @@ -531,7 +506,7 @@ fun add_primrec_simple fixes ts lthy = let val (((names, defs), prove), lthy') = prepare_primrec fixes ts lthy - handle ERROR str => primrec_error str; + handle ERROR str => raise PRIMREC (str, []); in lthy' |> fold_map Local_Theory.define defs @@ -548,7 +523,7 @@ lthy = let val d = duplicates (op =) (map (Binding.name_of o #1) raw_fixes) - val _ = null d orelse primrec_error ("duplicate function name(s): " ^ commas d); + val _ = null d orelse raise PRIMREC ("duplicate function name(s): " ^ commas d, []); val (fixes, specs) = fst (prep_spec raw_fixes raw_spec lthy); diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Wed Feb 19 08:34:33 2014 +0100 @@ -16,6 +16,8 @@ open BNF_FP_N2M_Sugar open BNF_LFP_Rec_Sugar +val nested_simps = @{thms id_def split comp_def fst_conv snd_conv}; + fun is_new_datatype ctxt s = (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false); @@ -125,8 +127,38 @@ massage_call end; +fun rewrite_map_arg get_ctr_pos rec_type res_type = + let + val pT = HOLogic.mk_prodT (rec_type, res_type); + + fun subst d (t as Bound d') = t |> d = SOME d' ? curry (op $) (fst_const pT) + | subst d (Abs (v, T, b)) = + Abs (v, if d = SOME ~1 then pT else T, subst (Option.map (Integer.add 1) d) b) + | subst d t = + let + val (u, vs) = strip_comb t; + val ctr_pos = try (get_ctr_pos o fst o dest_Free) u |> the_default ~1; + in + if ctr_pos >= 0 then + if d = SOME ~1 andalso length vs = ctr_pos then + list_comb (permute_args ctr_pos (snd_const pT), vs) + else if length vs > ctr_pos andalso is_some d andalso + d = try (fn Bound n => n) (nth vs ctr_pos) then + list_comb (snd_const pT $ nth vs ctr_pos, map (subst d) (nth_drop ctr_pos vs)) + else + raise PRIMREC ("recursive call not directly applied to constructor argument", [t]) + else + list_comb (u, map (subst (d |> d = SOME ~1 ? K NONE)) vs) + end + in + subst (SOME ~1) + end; + +fun rewrite_nested_rec_call ctxt has_call get_ctr_pos = + massage_nested_rec_call ctxt has_call (rewrite_map_arg get_ctr_pos); + val _ = Theory.setup (register_lfp_rec_extension - {is_new_datatype = is_new_datatype, get_basic_lfp_sugars = get_basic_lfp_sugars, - massage_nested_rec_call = massage_nested_rec_call}); + {nested_simps = nested_simps, is_new_datatype = is_new_datatype, + get_basic_lfp_sugars = get_basic_lfp_sugars, rewrite_nested_rec_call = rewrite_nested_rec_call}); end; diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Feb 19 08:34:33 2014 +0100 @@ -8,6 +8,7 @@ signature BNF_UTIL = sig include CTR_SUGAR_UTIL + include BNF_FP_REC_SUGAR_UTIL val map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list @@ -50,7 +51,6 @@ 'i list -> 'j -> 'k list * 'j val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list - val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context val mk_Freesss: string -> typ list list list -> Proof.context -> @@ -58,11 +58,9 @@ val mk_Freessss: string -> typ list list list list -> Proof.context -> term list list list list * Proof.context val nonzero_string_of_int: int -> string - val retype_free: typ -> term -> term val binder_fun_types: typ -> typ list val body_fun_type: typ -> typ - val num_binder_types: typ -> int val strip_fun_type: typ -> typ list * typ val strip_typeN: int -> typ -> typ list * typ @@ -110,8 +108,6 @@ (*parameterized thms*) val mk_Un_upper: int -> int -> thm val mk_conjIN: int -> thm - val mk_conjunctN: int -> int -> thm - val conj_dests: int -> thm -> thm list val mk_nthI: int -> int -> thm val mk_nth_conv: int -> int -> thm val mk_ordLeq_csum: int -> int -> thm -> thm @@ -148,6 +144,7 @@ struct open Ctr_Sugar_Util +open BNF_FP_Rec_Sugar_Util (* Library proper *) @@ -319,16 +316,9 @@ fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss; fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss; -fun retype_free T (Free (s, _)) = Free (s, T) - | retype_free _ t = raise TERM ("retype_free", [t]); - (** Types **) -(*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*) -fun num_binder_types (Type (@{type_name fun}, [_, T])) = 1 + num_binder_types T - | num_binder_types _ = 0; - (*maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T)*) fun strip_typeN 0 T = ([], T) | strip_typeN n (Type (@{type_name fun}, [T, T'])) = strip_typeN (n - 1) T' |>> cons T @@ -485,9 +475,6 @@ let val T = (case xs of [] => defT | (x::_) => fastype_of x); in Const (@{const_name collect}, HOLogic.mk_setT T --> T) $ (HOLogic.mk_set T xs) end; -fun find_indices eq xs ys = map_filter I - (map_index (fn (i, y) => if member eq xs y then SOME i else NONE) ys); - fun mk_trans thm1 thm2 = trans OF [thm1, thm2]; fun mk_sym thm = thm RS sym; @@ -522,13 +509,6 @@ | mk_nthI n m = fold (curry op RS) (replicate (m - 1) @{thm sndI}) (if m = n then @{thm TrueE[OF TrueI]} else @{thm fstI}); -fun mk_conjunctN 1 1 = @{thm TrueE[OF TrueI]} - | mk_conjunctN _ 1 = conjunct1 - | mk_conjunctN 2 2 = conjunct2 - | mk_conjunctN n m = conjunct2 RS (mk_conjunctN (n - 1) (m - 1)); - -fun conj_dests n thm = map (fn k => thm RS mk_conjunctN n k) (1 upto n); - fun mk_conjIN 1 = @{thm TrueE[OF TrueI]} | mk_conjIN n = mk_conjIN (n - 1) RSN (2, conjI); diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Tools/Datatype/primrec.ML --- a/src/HOL/Tools/Datatype/primrec.ML Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Tools/Datatype/primrec.ML Wed Feb 19 08:34:33 2014 +0100 @@ -308,13 +308,4 @@ val simps' = Proof_Context.export lthy' lthy simps; in ((ts, simps'), Local_Theory.exit_global lthy') end; - -(* outer syntax *) - -val _ = - Outer_Syntax.local_theory @{command_spec "old_primrec"} - "define primitive recursive functions on datatypes" - (Parse.fixes -- Parse_Spec.where_alt_specs - >> (fn (fixes, specs) => add_primrec_cmd fixes specs #> snd)); - end; diff -r 4a940ebceef8 -r a5e33e18fb5c src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Wed Feb 19 08:34:32 2014 +0100 +++ b/src/HOL/Transitive_Closure.thy Wed Feb 19 08:34:33 2014 +0100 @@ -716,11 +716,11 @@ relpowp == "compow :: nat \ ('a \ 'a \ bool) \ ('a \ 'a \ bool)" begin -old_primrec relpow :: "nat \ ('a \ 'a) set \ ('a \ 'a) set" where +primrec relpow :: "nat \ ('a \ 'a) set \ ('a \ 'a) set" where "relpow 0 R = Id" | "relpow (Suc n) R = (R ^^ n) O R" -old_primrec relpowp :: "nat \ ('a \ 'a \ bool) \ ('a \ 'a \ bool)" where +primrec relpowp :: "nat \ ('a \ 'a \ bool) \ ('a \ 'a \ bool)" where "relpowp 0 R = HOL.eq" | "relpowp (Suc n) R = (R ^^ n) OO R"