--- 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"
--- 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: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
@@ -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
--- 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
--- 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\<Colon>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\<Colon>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\<Colon>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\<Colon>nat) \<le> n \<longleftrightarrow> True"
| "Suc m \<le> n \<longleftrightarrow> (case n of 0 \<Rightarrow> False | Suc n \<Rightarrow> m \<le> n)"
@@ -1303,7 +1303,7 @@
funpow == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
begin
-old_primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> '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 \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> '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 *}
--- 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 \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd" where
+primrec sum_map :: "('a \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> 'a + 'b \<Rightarrow> '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 \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
+primrec Suml :: "('a \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
"Suml f (Inl x) = f x"
-old_primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
+primrec Sumr :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a + 'b \<Rightarrow> 'c" where
"Sumr f (Inr x) = f x"
lemma Suml_inject:
--- 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;
--- 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;
--- 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))
--- 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;
--- 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;
--- 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);
--- 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);
--- 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;
--- 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);
--- 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;
--- 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 \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"
begin
-old_primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
+primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
"relpow 0 R = Id"
| "relpow (Suc n) R = (R ^^ n) O R"
-old_primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
+primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where
"relpowp 0 R = HOL.eq"
| "relpowp (Suc n) R = (R ^^ n) OO R"