renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler)
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -242,9 +242,9 @@
rel_converse_of_bnf outer RS sym], outer_rel_Gr],
trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
(map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym)
- |> unfold_defs lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
+ |> unfold_thms lthy (basic_thms @ rel_def_of_bnf outer :: map rel_def_of_bnf inners);
in
- unfold_defs_tac lthy basic_thms THEN rtac thm 1
+ unfold_thms_tac lthy basic_thms THEN rtac thm 1
end;
val tacs = zip_axioms map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
@@ -316,7 +316,7 @@
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
fun map_comp_tac {context, ...} =
- unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+ unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
fun map_cong_tac {context, ...} =
mk_kill_map_cong_tac context n (live - n) (map_cong_of_bnf bnf);
@@ -352,7 +352,7 @@
trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
(replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
replicate (live - n) @{thm Gr_fst_snd})]]] RS sym)
- |> unfold_defs lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
+ |> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv});
in
rtac thm 1
end;
@@ -410,7 +410,7 @@
fun map_id_tac _ = rtac (map_id_of_bnf bnf) 1;
fun map_comp_tac {context, ...} =
- unfold_defs_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
+ unfold_thms_tac context ((map_comp_of_bnf bnf RS sym) :: @{thms o_assoc id_o o_id}) THEN
rtac refl 1;
fun map_cong_tac {context, ...} =
rtac (map_cong_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac context 1);
@@ -615,10 +615,10 @@
set_unfoldss);
val expand_preds = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
pred_unfolds);
- val unfold_maps = fold (unfold_defs lthy o single) map_unfolds;
- val unfold_sets = fold (unfold_defs lthy) set_unfoldss;
- val unfold_preds = unfold_defs lthy pred_unfolds;
- val unfold_rels = unfold_defs lthy rel_unfolds;
+ val unfold_maps = fold (unfold_thms lthy o single) map_unfolds;
+ val unfold_sets = fold (unfold_thms lthy) set_unfoldss;
+ val unfold_preds = unfold_thms lthy pred_unfolds;
+ val unfold_rels = unfold_thms lthy rel_unfolds;
val unfold_all = unfold_sets o unfold_maps o unfold_preds o unfold_rels;
val bnf_map = expand_maps (mk_map_of_bnf Ds As Bs bnf);
val bnf_sets = map (expand_maps o expand_sets)
@@ -665,7 +665,7 @@
(mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
(K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
(mk_tac (map_wpull_of_bnf bnf))
- (mk_tac (unfold_defs lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
+ (mk_tac (unfold_thms lthy [rel_def_of_bnf bnf] (rel_O_Gr_of_bnf bnf)));
val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -64,8 +64,8 @@
(* Composition *)
fun mk_comp_set_alt_tac ctxt collect_set_natural =
- unfold_defs_tac ctxt @{thms sym[OF o_assoc]} THEN
- unfold_defs_tac ctxt [collect_set_natural RS sym] THEN
+ unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN
+ unfold_thms_tac ctxt [collect_set_natural RS sym] THEN
rtac refl 1;
fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps =
@@ -138,9 +138,9 @@
rtac bd;
fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
in
- unfold_defs_tac ctxt [comp_set_alt] THEN
+ unfold_thms_tac ctxt [comp_set_alt] THEN
rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
- unfold_defs_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
+ unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
(rtac ctrans THEN'
WRAP' gen_before gen_after bds (rtac last_bd) THEN'
rtac @{thm ordIso_imp_ordLeq} THEN'
@@ -152,12 +152,12 @@
conj_assoc};
fun mk_comp_in_alt_tac ctxt comp_set_alts =
- unfold_defs_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
- unfold_defs_tac ctxt @{thms set_eq_subset} THEN
+ unfold_thms_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
+ unfold_thms_tac ctxt @{thms set_eq_subset} THEN
rtac conjI 1 THEN
REPEAT_DETERM (
rtac @{thm subsetI} 1 THEN
- unfold_defs_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
+ unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
(REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
REPEAT_DETERM (CHANGED ((
(rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE'
@@ -214,7 +214,7 @@
fun mk_comp_wit_tac ctxt Gwit_thms collect_set_natural Fwit_thms =
ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
- unfold_defs_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
+ unfold_thms_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
REPEAT_DETERM (
atac 1 ORELSE
REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
@@ -408,7 +408,7 @@
TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
fun mk_simple_rel_O_Gr_tac ctxt rel_def rel_O_Gr in_alt_thm =
- rtac (unfold_defs ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym]))
+ rtac (unfold_thms ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym]))
1;
fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Fri Sep 21 15:53:29 2012 +0200
@@ -1180,7 +1180,7 @@
let
val wits_tac =
K (TRYALL Goal.conjunction_tac) THEN' K (TRYALL (rtac TrueI)) THEN'
- mk_unfold_defs_then_tac lthy one_step_defs wit_tac;
+ mk_unfold_thms_then_tac lthy one_step_defs wit_tac;
val wit_goals = map mk_conjunction_balanced' wit_goalss;
val wit_thms =
Skip_Proof.prove lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac
@@ -1189,7 +1189,7 @@
|> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
in
map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
- goals (map (mk_unfold_defs_then_tac lthy one_step_defs) tacs)
+ goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
|> (fn thms => after_qed (map single thms @ wit_thms) lthy)
end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
--- a/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -69,8 +69,8 @@
val n = length set_naturals;
in
if null set_naturals then
- unfold_defs_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
- else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+ unfold_thms_tac ctxt rel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
+ else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac equalityI, rtac subsetI,
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac Pair_eqD,
@@ -105,7 +105,7 @@
end;
fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
- unfold_defs_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
+ unfold_thms_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
subst_tac ctxt [map_id] 1 THEN
(if n = 0 then rtac refl 1
else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
@@ -113,7 +113,7 @@
CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac refl] 1);
fun mk_rel_mono_tac rel_O_Grs in_mono {context = ctxt, prems = _} =
- unfold_defs_tac ctxt rel_O_Grs THEN
+ unfold_thms_tac ctxt rel_O_Grs THEN
EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
@@ -124,8 +124,8 @@
val n = length set_naturals;
in
if null set_naturals then
- unfold_defs_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
- else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+ unfold_thms_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
+ else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac Pair_eqD,
@@ -151,8 +151,8 @@
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
in
- if null set_naturals then unfold_defs_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
- else unfold_defs_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
+ if null set_naturals then unfold_thms_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
+ else unfold_thms_tac ctxt (@{thm Gr_def} :: rel_O_Grs) THEN
EVERY' [rtac equalityI, rtac @{thm subrelI},
REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
REPEAT_DETERM o dtac Pair_eqD,
@@ -197,7 +197,7 @@
let
val ls' = replicate (Int.max (1, m)) ();
in
- unfold_defs_tac ctxt (rel_O_Grs @
+ unfold_thms_tac ctxt (rel_O_Grs @
@{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
--- a/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -18,32 +18,30 @@
val caseN: string
val coN: string
val coinductN: string
- val coiterN: string
- val coitersN: string
val corecN: string
val corecsN: string
val ctorN: string
val ctor_dtorN: string
- val ctor_dtor_coitersN: string
+ val ctor_dtor_unfoldsN: string
val ctor_dtor_corecsN: string
val ctor_exhaustN: string
val ctor_induct2N: string
val ctor_inductN: string
val ctor_injectN: string
- val ctor_iterN: string
- val ctor_iter_uniqueN: string
- val ctor_itersN: string
+ val ctor_foldN: string
+ val ctor_fold_uniqueN: string
+ val ctor_foldsN: string
val ctor_recN: string
val ctor_recsN: string
- val disc_coiter_iffN: string
- val disc_coitersN: string
+ val disc_unfold_iffN: string
+ val disc_unfoldsN: string
val disc_corec_iffN: string
val disc_corecsN: string
val dtorN: string
val dtor_coinductN: string
- val dtor_coiterN: string
- val dtor_coiter_uniqueN: string
- val dtor_coitersN: string
+ val dtor_unfoldN: string
+ val dtor_unfold_uniqueN: string
+ val dtor_unfoldsN: string
val dtor_corecN: string
val dtor_corecsN: string
val dtor_exhaustN: string
@@ -51,13 +49,13 @@
val dtor_injectN: string
val dtor_strong_coinductN: string
val exhaustN: string
+ val foldN: string
+ val foldsN: string
val hsetN: string
val hset_recN: string
val inductN: string
val injectN: string
val isNodeN: string
- val iterN: string
- val itersN: string
val lsbisN: string
val map_simpsN: string
val map_uniqueN: string
@@ -73,7 +71,7 @@
val rel_simpN: string
val rel_strong_coinductN: string
val rvN: string
- val sel_coitersN: string
+ val sel_unfoldsN: string
val sel_corecsN: string
val set_inclN: string
val set_set_inclN: string
@@ -83,6 +81,8 @@
val strongN: string
val sum_bdN: string
val sum_bdTN: string
+ val unfoldN: string
+ val unfoldsN: string
val uniqueN: string
val mk_exhaustN: string -> string
@@ -158,23 +158,24 @@
val rawN = "raw_"
val coN = "co"
+val unN = "un"
val algN = "alg"
val IITN = "IITN"
-val iterN = "iter"
-val itersN = iterN ^ "s"
-val coiterN = coN ^ iterN
-val coitersN = coiterN ^ "s"
+val foldN = "fold"
+val foldsN = foldN ^ "s"
+val unfoldN = unN ^ foldN
+val unfoldsN = unfoldN ^ "s"
val uniqueN = "_unique"
val simpsN = "simps"
val ctorN = "ctor"
val dtorN = "dtor"
-val ctor_iterN = ctorN ^ "_" ^ iterN
-val ctor_itersN = ctor_iterN ^ "s"
-val dtor_coiterN = dtorN ^ "_" ^ coiterN
-val dtor_coitersN = dtor_coiterN ^ "s"
-val ctor_iter_uniqueN = ctor_iterN ^ uniqueN
-val dtor_coiter_uniqueN = dtor_coiterN ^ uniqueN
-val ctor_dtor_coitersN = ctorN ^ "_" ^ dtor_coiterN ^ "s"
+val ctor_foldN = ctorN ^ "_" ^ foldN
+val ctor_foldsN = ctor_foldN ^ "s"
+val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
+val dtor_unfoldsN = dtor_unfoldN ^ "s"
+val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
+val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
+val ctor_dtor_unfoldsN = ctorN ^ "_" ^ dtor_unfoldN ^ "s"
val map_simpsN = mapN ^ "_" ^ simpsN
val map_uniqueN = mapN ^ uniqueN
val min_algN = "min_alg"
@@ -237,13 +238,13 @@
val caseN = "case"
val discN = "disc"
-val disc_coitersN = discN ^ "_" ^ coitersN
+val disc_unfoldsN = discN ^ "_" ^ unfoldsN
val disc_corecsN = discN ^ "_" ^ corecsN
val iffN = "_iff"
-val disc_coiter_iffN = discN ^ "_" ^ coiterN ^ iffN
+val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
val selN = "sel"
-val sel_coitersN = selN ^ "_" ^ coitersN
+val sel_unfoldsN = selN ^ "_" ^ unfoldsN
val sel_corecsN = selN ^ "_" ^ corecsN
val mk_common_name = space_implode "_";
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Fri Sep 21 15:53:29 2012 +0200
@@ -169,8 +169,8 @@
val fp_eqs =
map dest_TFree Bs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsBs;
- val (pre_bnfs, ((dtors0, ctors0, fp_iters0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
- ctor_injects, fp_iter_thms, fp_rec_thms), lthy)) =
+ val (pre_bnfs, ((dtors0, ctors0, fp_folds0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
+ ctor_injects, fp_fold_thms, fp_rec_thms), lthy)) =
fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
fun add_nesty_bnf_names Us =
@@ -211,7 +211,7 @@
val mss = map (map length) ctr_Tsss;
val Css = map2 replicate ns Cs;
- fun mk_iter_like Ts Us t =
+ fun mk_rec_like Ts Us t =
let
val (bindings, body) = strip_type (fastype_of t);
val (f_Us, prebody) = split_last bindings;
@@ -221,20 +221,20 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
- val fp_iters as fp_iter1 :: _ = map (mk_iter_like As Cs) fp_iters0;
- val fp_recs as fp_rec1 :: _ = map (mk_iter_like As Cs) fp_recs0;
+ val fp_folds as fp_fold1 :: _ = map (mk_rec_like As Cs) fp_folds0;
+ val fp_recs as fp_rec1 :: _ = map (mk_rec_like As Cs) fp_recs0;
- val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1)));
+ val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of fp_fold1)));
val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
- val (((iter_only as (gss, _, _), rec_only as (hss, _, _)),
- (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
+ val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
+ (zs, cs, cpss, unfold_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
names_lthy) =
if lfp then
let
val y_Tsss =
map3 (fn n => fn ms => map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type)
- ns mss fp_iter_fun_Ts;
+ ns mss fp_fold_fun_Ts;
val g_Tss = map2 (map2 (curry (op --->))) y_Tsss Css;
val ((gss, ysss), lthy) =
@@ -287,7 +287,7 @@
val pf_Tss = map3 zip_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
in (q_Tssss, f_sum_prod_Ts, f_Tssss, pf_Tss) end;
- val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_iter_fun_Ts;
+ val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_fold_fun_Ts;
val ((((Free (z, _), cs), pss), gssss), lthy) =
lthy
@@ -329,7 +329,7 @@
(mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy)
end;
- fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), ctor), dtor), fp_iter), fp_rec),
+ fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), ctor), dtor), fp_fold), fp_rec),
ctor_dtor), dtor_ctor), ctor_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
let
@@ -391,7 +391,7 @@
end;
val sumEN_thm' =
- unfold_defs lthy @{thms all_unit_eq}
+ unfold_thms lthy @{thms all_unit_eq}
(Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
(mk_sumEN_balanced n))
|> Morphism.thm phi;
@@ -413,25 +413,25 @@
val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
- fun define_iter_rec (wrap_res, no_defs_lthy) =
+ fun define_fold_rec (wrap_res, no_defs_lthy) =
let
val fpT_to_C = fpT --> C;
- fun generate_iter_like (suf, fp_iter_like, (fss, f_Tss, xssss)) =
+ fun generate_rec_like (suf, fp_rec_like, (fss, f_Tss, xssss)) =
let
val res_T = fold_rev (curry (op --->)) f_Tss fpT_to_C;
val binding = Binding.suffix_name ("_" ^ suf) fp_b;
val spec =
mk_Trueprop_eq (lists_bmoc fss (Free (Binding.name_of binding, res_T)),
- Term.list_comb (fp_iter_like,
+ Term.list_comb (fp_rec_like,
map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss));
in (binding, spec) end;
- val iter_like_infos =
- [(iterN, fp_iter, iter_only),
+ val rec_like_infos =
+ [(foldN, fp_fold, fold_only),
(recN, fp_rec, rec_only)];
- val (bindings, specs) = map generate_iter_like iter_like_infos |> split_list;
+ val (bindings, specs) = map generate_rec_like rec_like_infos |> split_list;
val ((csts, defs), (lthy', lthy)) = no_defs_lthy
|> apfst split_list o fold_map2 (fn b => fn spec =>
@@ -441,14 +441,14 @@
val phi = Proof_Context.export_morphism lthy lthy';
- val [iter_def, rec_def] = map (Morphism.thm phi) defs;
+ val [fold_def, rec_def] = map (Morphism.thm phi) defs;
- val [iterx, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
+ val [foldx, recx] = map (mk_rec_like As Cs o Morphism.term phi) csts;
in
- ((wrap_res, ctrs, iterx, recx, xss, ctr_defs, iter_def, rec_def), lthy)
+ ((wrap_res, ctrs, foldx, recx, xss, ctr_defs, fold_def, rec_def), lthy)
end;
- fun define_coiter_corec (wrap_res, no_defs_lthy) =
+ fun define_unfold_corec (wrap_res, no_defs_lthy) =
let
val B_to_fpT = C --> fpT;
@@ -456,22 +456,22 @@
Term.lambda c (mk_IfN sum_prod_T cps
(map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)));
- fun generate_coiter_like (suf, fp_iter_like, ((pfss, cqfsss), (f_sum_prod_Ts,
+ fun generate_corec_like (suf, fp_rec_like, ((pfss, cqfsss), (f_sum_prod_Ts,
pf_Tss))) =
let
val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
val binding = Binding.suffix_name ("_" ^ suf) fp_b;
val spec =
mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binding, res_T)),
- Term.list_comb (fp_iter_like,
+ Term.list_comb (fp_rec_like,
map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss));
in (binding, spec) end;
- val coiter_like_infos =
- [(coiterN, fp_iter, coiter_only),
+ val corec_like_infos =
+ [(unfoldN, fp_fold, unfold_only),
(corecN, fp_rec, corec_only)];
- val (bindings, specs) = map generate_coiter_like coiter_like_infos |> split_list;
+ val (bindings, specs) = map generate_corec_like corec_like_infos |> split_list;
val ((csts, defs), (lthy', lthy)) = no_defs_lthy
|> apfst split_list o fold_map2 (fn b => fn spec =>
@@ -481,11 +481,11 @@
val phi = Proof_Context.export_morphism lthy lthy';
- val [coiter_def, corec_def] = map (Morphism.thm phi) defs;
+ val [unfold_def, corec_def] = map (Morphism.thm phi) defs;
- val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
+ val [unfold, corec] = map (mk_rec_like As Cs o Morphism.term phi) csts;
in
- ((wrap_res, ctrs, coiter, corec, xss, ctr_defs, coiter_def, corec_def), lthy)
+ ((wrap_res, ctrs, unfold, corec, xss, ctr_defs, unfold_def, corec_def), lthy)
end;
fun wrap lthy =
@@ -494,9 +494,9 @@
sel_defaultss))) lthy
end;
- val define_iter_likes = if lfp then define_iter_rec else define_coiter_corec;
+ val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
in
- ((wrap, define_iter_likes), lthy')
+ ((wrap, define_rec_likes), lthy')
end;
val pre_map_defs = map map_def_of_bnf pre_bnfs;
@@ -521,11 +521,11 @@
in Term.list_comb (mapx, args) end;
val mk_simp_thmss =
- map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn iter_likes =>
- injects @ distincts @ cases @ rec_likes @ iter_likes);
+ map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn rec_likes =>
+ injects @ distincts @ cases @ rec_likes @ rec_likes);
- fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss,
- iter_defs, rec_defs), lthy) =
+ fun derive_induct_fold_rec_thms_for_types ((wrap_ress, ctrss, folds, recs, xsss, ctr_defss,
+ fold_defs, rec_defs), lthy) =
let
val (((phis, phis'), us'), names_lthy) =
lthy
@@ -615,55 +615,55 @@
(* TODO: Generate nicer names in case of clashes *)
val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
- val (iter_thmss, rec_thmss) =
+ val (fold_thmss, rec_thmss) =
let
val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
- val giters = map (lists_bmoc gss) iters;
+ val gfolds = map (lists_bmoc gss) folds;
val hrecs = map (lists_bmoc hss) recs;
- fun mk_goal fss fiter_like xctr f xs fxs =
+ fun mk_goal fss frec_like xctr f xs fxs =
fold_rev (fold_rev Logic.all) (xs :: fss)
- (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
+ (mk_Trueprop_eq (frec_like $ xctr, Term.list_comb (f, fxs)));
- fun build_call fiter_likes maybe_tick (T, U) =
+ fun build_call frec_likes maybe_tick (T, U) =
if T = U then
id_const T
else
(case find_index (curry (op =) T) fpTs of
- ~1 => build_map (build_call fiter_likes maybe_tick) T U
- | j => maybe_tick (nth us j) (nth fiter_likes j));
+ ~1 => build_map (build_call frec_likes maybe_tick) T U
+ | j => maybe_tick (nth us j) (nth frec_likes j));
fun mk_U maybe_mk_prodT =
typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
- fun intr_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
+ fun intr_calls frec_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
if member (op =) fpTs T then
- maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x]
+ maybe_cons x [build_call frec_likes (K I) (T, mk_U (K I) T) $ x]
else if exists_fp_subtype T then
- [build_call fiter_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
+ [build_call frec_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
else
[x];
- val gxsss = map (map (maps (intr_calls giters (K I) (K I) (K I)))) xsss;
+ val gxsss = map (map (maps (intr_calls gfolds (K I) (K I) (K I)))) xsss;
val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
- val iter_goalss = map5 (map4 o mk_goal gss) giters xctrss gss xsss gxsss;
+ val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
- val iter_tacss =
- map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids iter_defs) fp_iter_thms
+ val fold_tacss =
+ map2 (map o mk_rec_like_tac pre_map_defs nesting_map_ids fold_defs) fp_fold_thms
ctr_defss;
val rec_tacss =
- map2 (map o mk_iter_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
+ map2 (map o mk_rec_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
ctr_defss;
fun prove goal tac = Skip_Proof.prove lthy [] [] goal (tac o #context);
in
- (map2 (map2 prove) iter_goalss iter_tacss,
+ (map2 (map2 prove) fold_goalss fold_tacss,
map2 (map2 prove) rec_goalss rec_tacss)
end;
- val simp_thmss = mk_simp_thmss wrap_ress rec_thmss iter_thmss;
+ val simp_thmss = mk_simp_thmss wrap_ress rec_thmss fold_thmss;
val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
@@ -678,7 +678,7 @@
val notes =
[(inductN, map single induct_thms,
fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
- (itersN, iter_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
+ (foldsN, fold_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
(recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
(simpsN, simp_thmss, K [])]
|> maps (fn (thmN, thmss, attrs) =>
@@ -689,8 +689,8 @@
lthy |> Local_Theory.notes (common_notes @ notes) |> snd
end;
- fun derive_coinduct_coiter_corec_thms_for_types ((wrap_ress, ctrss, coiters, corecs, _,
- ctr_defss, coiter_defs, corec_defs), lthy) =
+ fun derive_coinduct_unfold_corec_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _,
+ ctr_defss, unfold_defs, corec_defs), lthy) =
let
val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
val selsss = map #2 wrap_ress;
@@ -714,79 +714,79 @@
fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
val z = the_single zs;
- val gcoiters = map (lists_bmoc pgss) coiters;
+ val gunfolds = map (lists_bmoc pgss) unfolds;
val hcorecs = map (lists_bmoc phss) corecs;
- val (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss) =
+ val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) =
let
- fun mk_goal pfss c cps fcoiter_like n k ctr m cfs' =
+ fun mk_goal pfss c cps fcorec_like n k ctr m cfs' =
fold_rev (fold_rev Logic.all) ([c] :: pfss)
(Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
- mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, take m cfs'))));
+ mk_Trueprop_eq (fcorec_like $ c, Term.list_comb (ctr, take m cfs'))));
- fun build_call fiter_likes maybe_tack (T, U) =
+ fun build_call frec_likes maybe_tack (T, U) =
if T = U then
id_const T
else
(case find_index (curry (op =) U) fpTs of
- ~1 => build_map (build_call fiter_likes maybe_tack) T U
- | j => maybe_tack (nth cs j, nth us j) (nth fiter_likes j));
+ ~1 => build_map (build_call frec_likes maybe_tack) T U
+ | j => maybe_tack (nth cs j, nth us j) (nth frec_likes j));
fun mk_U maybe_mk_sumT =
typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
- fun intr_calls fiter_likes maybe_mk_sumT maybe_tack cqf =
+ fun intr_calls frec_likes maybe_mk_sumT maybe_tack cqf =
let val T = fastype_of cqf in
if exists_subtype (member (op =) Cs) T then
- build_call fiter_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
+ build_call frec_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
else
cqf
end;
- val crgsss' = map (map (map (intr_calls gcoiters (K I) (K I)))) crgsss;
+ val crgsss' = map (map (map (intr_calls gunfolds (K I) (K I)))) crgsss;
val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss;
- val coiter_goalss =
- map8 (map4 oooo mk_goal pgss) cs cpss gcoiters ns kss ctrss mss crgsss';
+ 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 coiter_tacss =
- map3 (map oo mk_coiter_like_tac coiter_defs nesting_map_ids) fp_iter_thms pre_map_defs
+ val unfold_tacss =
+ map3 (map oo mk_corec_like_tac unfold_defs nesting_map_ids) fp_fold_thms pre_map_defs
ctr_defss;
val corec_tacss =
- map3 (map oo mk_coiter_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
+ map3 (map oo mk_corec_like_tac corec_defs nesting_map_ids) fp_rec_thms pre_map_defs
ctr_defss;
fun prove goal tac =
Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation;
- val coiter_thmss = map2 (map2 prove) coiter_goalss coiter_tacss;
+ val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
val corec_thmss =
map2 (map2 prove) corec_goalss corec_tacss
- |> map (map (unfold_defs lthy @{thms sum_case_if}));
+ |> map (map (unfold_thms lthy @{thms sum_case_if}));
- val coiter_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss;
+ val unfold_safesss = map2 (map2 (map2 (curry (op =)))) crgsss' crgsss;
val corec_safesss = map2 (map2 (map2 (curry (op =)))) cshsss' cshsss;
val filter_safesss =
map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo
curry (op ~~));
- val safe_coiter_thmss = filter_safesss coiter_safesss coiter_thmss;
+ val safe_unfold_thmss = filter_safesss unfold_safesss unfold_thmss;
val safe_corec_thmss = filter_safesss corec_safesss corec_thmss;
in
- (coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss)
+ (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss)
end;
- val (disc_coiter_iff_thmss, disc_corec_iff_thmss) =
+ val (disc_unfold_iff_thmss, disc_corec_iff_thmss) =
let
- fun mk_goal c cps fcoiter_like n k disc =
- mk_Trueprop_eq (disc $ (fcoiter_like $ c),
+ fun mk_goal c cps fcorec_like n k disc =
+ mk_Trueprop_eq (disc $ (fcorec_like $ c),
if n = 1 then @{const True}
else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
- val coiter_goalss = map6 (map2 oooo mk_goal) cs cpss gcoiters ns kss discss;
+ 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;
fun mk_case_split' cp =
@@ -794,10 +794,10 @@
val case_splitss' = map (map mk_case_split') cpss;
- val coiter_tacss =
- map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' coiter_thmss disc_thmsss;
+ val unfold_tacss =
+ map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' unfold_thmss disc_thmsss;
val corec_tacss =
- map3 (map oo mk_disc_coiter_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
+ map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
fun prove goal tac =
Skip_Proof.prove lthy [] [] goal (tac o #context)
@@ -807,17 +807,17 @@
fun proves [_] [_] = []
| proves goals tacs = map2 prove goals tacs;
in
- (map2 proves coiter_goalss coiter_tacss,
+ (map2 proves unfold_goalss unfold_tacss,
map2 proves corec_goalss corec_tacss)
end;
- fun mk_disc_coiter_like_thms coiter_likes discIs =
- map (op RS) (filter_out (is_triv_implies o snd) (coiter_likes ~~ discIs));
+ fun mk_disc_corec_like_thms corec_likes discIs =
+ map (op RS) (filter_out (is_triv_implies o snd) (corec_likes ~~ discIs));
- val disc_coiter_thmss = map2 mk_disc_coiter_like_thms coiter_thmss discIss;
- val disc_corec_thmss = map2 mk_disc_coiter_like_thms corec_thmss discIss;
+ val disc_unfold_thmss = map2 mk_disc_corec_like_thms unfold_thmss discIss;
+ val disc_corec_thmss = map2 mk_disc_corec_like_thms corec_thmss discIss;
- fun mk_sel_coiter_like_thm coiter_like_thm sel sel_thm =
+ fun mk_sel_corec_like_thm corec_like_thm sel sel_thm =
let
val (domT, ranT) = dest_funT (fastype_of sel);
val arg_cong' =
@@ -826,25 +826,25 @@
|> Thm.varifyT_global;
val sel_thm' = sel_thm RSN (2, trans);
in
- coiter_like_thm RS arg_cong' RS sel_thm'
+ corec_like_thm RS arg_cong' RS sel_thm'
end;
- fun mk_sel_coiter_like_thms coiter_likess =
- map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_likess selsss sel_thmsss |> map flat;
+ fun mk_sel_corec_like_thms corec_likess =
+ map3 (map3 (map2 o mk_sel_corec_like_thm)) corec_likess selsss sel_thmsss |> map flat;
- val sel_coiter_thmss = mk_sel_coiter_like_thms coiter_thmss;
- val sel_corec_thmss = mk_sel_coiter_like_thms corec_thmss;
+ val sel_unfold_thmss = mk_sel_corec_like_thms unfold_thmss;
+ val sel_corec_thmss = mk_sel_corec_like_thms corec_thmss;
- fun zip_coiter_like_thms coiter_likes disc_coiter_likes sel_coiter_likes =
- coiter_likes @ disc_coiter_likes @ sel_coiter_likes;
+ fun zip_corec_like_thms corec_likes disc_corec_likes sel_corec_likes =
+ corec_likes @ disc_corec_likes @ sel_corec_likes;
val simp_thmss =
mk_simp_thmss wrap_ress
- (map3 zip_coiter_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
- (map3 zip_coiter_like_thms safe_coiter_thmss disc_coiter_thmss sel_coiter_thmss);
+ (map3 zip_corec_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss)
+ (map3 zip_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss);
val anonymous_notes =
- [(flat safe_coiter_thmss @ flat safe_corec_thmss, simp_attrs)]
+ [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val common_notes =
@@ -854,13 +854,13 @@
val notes =
[(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
- (coitersN, coiter_thmss, []),
+ (unfoldsN, unfold_thmss, []),
(corecsN, corec_thmss, []),
- (disc_coiter_iffN, disc_coiter_iff_thmss, simp_attrs),
- (disc_coitersN, disc_coiter_thmss, simp_attrs),
+ (disc_unfold_iffN, disc_unfold_iff_thmss, simp_attrs),
+ (disc_unfoldsN, disc_unfold_thmss, simp_attrs),
(disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
(disc_corecsN, disc_corec_thmss, simp_attrs),
- (sel_coitersN, sel_coiter_thmss, simp_attrs),
+ (sel_unfoldsN, sel_unfold_thmss, simp_attrs),
(sel_corecsN, sel_corec_thmss, simp_attrs),
(simpsN, simp_thmss, [])]
|> maps (fn (thmN, thmss, attrs) =>
@@ -871,16 +871,16 @@
lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
end;
- fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
- fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list8
+ fun wrap_types_and_define_rec_likes ((wraps, define_rec_likess), lthy) =
+ fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list8
val lthy' = lthy
- |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_iters ~~
+ |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_folds ~~
fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
- |>> split_list |> wrap_types_and_define_iter_likes
- |> (if lfp then derive_induct_iter_rec_thms_for_types
- else derive_coinduct_coiter_corec_thms_for_types);
+ |>> split_list |> wrap_types_and_define_rec_likes
+ |> (if lfp then derive_induct_fold_rec_thms_for_types
+ else derive_coinduct_unfold_corec_thms_for_types);
val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
(if lfp then "" else "co") ^ "datatype"));
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -8,16 +8,16 @@
signature BNF_FP_SUGAR_TACTICS =
sig
val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
- val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
+ val mk_corec_like_tac: thm list -> thm list -> 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_like_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+ val mk_disc_corec_like_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 list -> tactic
val mk_induct_tac: Proof.context -> int list -> int list list -> int list list list -> thm list ->
thm -> thm list -> thm list list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> tactic
- val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
+ val mk_rec_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
end;
structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
@@ -44,14 +44,14 @@
val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
fun mk_case_tac ctxt n k m case_def ctr_def dtor_ctor =
- unfold_defs_tac ctxt [case_def, ctr_def, dtor_ctor] THEN
+ unfold_thms_tac ctxt [case_def, ctr_def, dtor_ctor] THEN
(rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN'
rtac refl) 1;
fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
- unfold_defs_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN rtac sumEN' 1 THEN
- unfold_defs_tac ctxt @{thms all_prod_eq} THEN
+ unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN rtac sumEN' 1 THEN
+ unfold_thms_tac ctxt @{thms all_prod_eq} THEN
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)) 1;
@@ -59,41 +59,41 @@
(rtac iffI THEN'
EVERY' (map3 (fn cTs => fn cx => fn th =>
dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
- SELECT_GOAL (unfold_defs_tac ctxt [th]) THEN'
+ SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor])) 1;
fun mk_half_distinct_tac ctxt ctor_inject ctr_defs =
- unfold_defs_tac ctxt (ctor_inject :: @{thms sum.inject} @ ctr_defs) THEN
+ unfold_thms_tac ctxt (ctor_inject :: @{thms sum.inject} @ ctr_defs) THEN
rtac @{thm sum.distinct(1)} 1;
fun mk_inject_tac ctxt ctr_def ctor_inject =
- unfold_defs_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
- unfold_defs_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
+ unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
+ unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
-val iter_like_unfold_thms =
+val rec_like_unfold_thms =
@{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
split_conv};
-fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs ctor_iter_like ctr_def ctxt =
- unfold_defs_tac ctxt (ctr_def :: ctor_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
- iter_like_unfold_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1;
+fun mk_rec_like_tac pre_map_defs map_ids rec_like_defs ctor_rec_like ctr_def ctxt =
+ unfold_thms_tac ctxt (ctr_def :: ctor_rec_like :: rec_like_defs @ pre_map_defs @ map_ids @
+ rec_like_unfold_thms) THEN unfold_thms_tac ctxt @{thms id_def} THEN rtac refl 1;
-val coiter_like_ss = ss_only @{thms if_True if_False};
-val coiter_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
+val corec_like_ss = ss_only @{thms if_True if_False};
+val corec_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
-fun mk_coiter_like_tac coiter_like_defs map_ids ctor_dtor_coiter_like pre_map_def ctr_def ctxt =
- unfold_defs_tac ctxt (ctr_def :: coiter_like_defs) THEN
- subst_tac ctxt [ctor_dtor_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
- unfold_defs_tac ctxt (pre_map_def :: coiter_like_unfold_thms @ map_ids) THEN
- unfold_defs_tac ctxt @{thms id_def} THEN
+fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt =
+ unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN
+ subst_tac ctxt [ctor_dtor_corec_like] 1 THEN asm_simp_tac corec_like_ss 1 THEN
+ unfold_thms_tac ctxt (pre_map_def :: corec_like_unfold_thms @ map_ids) THEN
+ unfold_thms_tac ctxt @{thms id_def} THEN
TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
-fun mk_disc_coiter_like_iff_tac case_splits' coiter_likes discs ctxt =
- EVERY (map3 (fn case_split_tac => fn coiter_like_thm => fn disc =>
- case_split_tac 1 THEN unfold_defs_tac ctxt [coiter_like_thm] THEN
+fun mk_disc_corec_like_iff_tac case_splits' corec_likes discs ctxt =
+ EVERY (map3 (fn case_split_tac => fn corec_like_thm => fn disc =>
+ case_split_tac 1 THEN unfold_thms_tac ctxt [corec_like_thm] THEN
asm_simp_tac (ss_only @{thms simp_thms(7,8,12,14,22,24)}) 1 THEN
(if is_refl disc then all_tac else rtac disc 1))
- (map rtac case_splits' @ [K all_tac]) coiter_likes discs);
+ (map rtac case_splits' @ [K all_tac]) corec_likes discs);
val solve_prem_prem_tac =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
@@ -107,7 +107,7 @@
fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
- SELECT_GOAL (unfold_defs_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
+ SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
solve_prem_prem_tac]) (rev kks)) 1;
fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
@@ -125,7 +125,7 @@
val nn = length ns;
val n = Integer.sum ns;
in
- unfold_defs_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
+ unfold_thms_tac ctxt ctr_defs THEN rtac ctor_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
pre_set_defss mss (unflat mss (1 upto n)) kkss)
end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -1060,9 +1060,9 @@
val sum_card_order = mk_sum_card_order bd_card_orders;
- val sbd_ordIso = fold_defs lthy [sbd_def]
+ val sbd_ordIso = fold_thms lthy [sbd_def]
(@{thm dir_image} OF [Abs_sbdT_inj, sum_Card_order]);
- val sbd_card_order = fold_defs lthy [sbd_def]
+ val sbd_card_order = fold_thms lthy [sbd_def]
(@{thm card_order_dir_image} OF [Abs_sbdT_bij, sum_card_order]);
val sbd_Cinfinite = @{thm Cinfinite_cong} OF [sbd_ordIso, sum_Cinfinite];
val sbd_Cnotzero = sbd_Cinfinite RS @{thm Cinfinite_Cnotzero};
@@ -1854,14 +1854,14 @@
val sndsTs = map snd_const prodTs;
val dtorTs = map2 (curry (op -->)) Ts FTs;
val ctorTs = map2 (curry (op -->)) FTs Ts;
- val coiter_fTs = map2 (curry op -->) activeAs Ts;
+ val unfold_fTs = map2 (curry op -->) activeAs Ts;
val corec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) sum_sTs;
val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls;
val corec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls_rev;
val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls;
val (((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jzs1), Jzs2), Jpairs),
- FJzs), TRs), coiter_fs), coiter_fs_copy), corec_ss), phis), names_lthy) = names_lthy
+ FJzs), TRs), unfold_fs), unfold_fs_copy), corec_ss), phis), names_lthy) = names_lthy
|> mk_Frees' "z" Ts
||>> mk_Frees' "z" Ts'
||>> mk_Frees "z" Ts
@@ -1870,8 +1870,8 @@
||>> mk_Frees "j" (map2 (curry HOLogic.mk_prodT) Ts Ts')
||>> mk_Frees "x" prodFTs
||>> mk_Frees "R" (map (mk_relT o `I) Ts)
- ||>> mk_Frees "f" coiter_fTs
- ||>> mk_Frees "g" coiter_fTs
+ ||>> mk_Frees "f" unfold_fTs
+ ||>> mk_Frees "g" unfold_fTs
||>> mk_Frees "s" corec_sTs
||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
@@ -1927,38 +1927,38 @@
val timer = time (timer "dtor definitions & thms");
- fun coiter_bind i = Binding.suffix_name ("_" ^ dtor_coiterN) (nth bs (i - 1));
- val coiter_name = Binding.name_of o coiter_bind;
- val coiter_def_bind = rpair [] o Thm.def_binding o coiter_bind;
-
- fun coiter_spec i T AT abs f z z' =
+ fun unfold_bind i = Binding.suffix_name ("_" ^ dtor_unfoldN) (nth bs (i - 1));
+ val unfold_name = Binding.name_of o unfold_bind;
+ val unfold_def_bind = rpair [] o Thm.def_binding o unfold_bind;
+
+ fun unfold_spec i T AT abs f z z' =
let
- val coiterT = Library.foldr (op -->) (sTs, AT --> T);
-
- val lhs = Term.list_comb (Free (coiter_name i, coiterT), ss);
+ val unfoldT = Library.foldr (op -->) (sTs, AT --> T);
+
+ val lhs = Term.list_comb (Free (unfold_name i, unfoldT), ss);
val rhs = Term.absfree z' (abs $ (f $ z));
in
mk_Trueprop_eq (lhs, rhs)
end;
- val ((coiter_frees, (_, coiter_def_frees)), (lthy, lthy_old)) =
+ val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
lthy
|> fold_map7 (fn i => fn T => fn AT => fn abs => fn f => fn z => fn z' =>
Specification.definition
- (SOME (coiter_bind i, NONE, NoSyn), (coiter_def_bind i, coiter_spec i T AT abs f z z')))
+ (SOME (unfold_bind i, NONE, NoSyn), (unfold_def_bind i, unfold_spec i T AT abs f z z')))
ks Ts activeAs Abs_Ts (map (fn i => HOLogic.mk_comp
(mk_proj (mk_LSBIS passive_UNIVs i), mk_beh ss i)) ks) zs zs'
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val coiters = map (Morphism.term phi) coiter_frees;
- val coiter_names = map (fst o dest_Const) coiters;
- fun mk_coiter Ts ss i = Term.list_comb (Const (nth coiter_names (i - 1), Library.foldr (op -->)
+ val unfolds = map (Morphism.term phi) unfold_frees;
+ val unfold_names = map (fst o dest_Const) unfolds;
+ fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
- val coiter_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) coiter_def_frees;
-
- val mor_coiter_thm =
+ val unfold_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unfold_def_frees;
+
+ val mor_unfold_thm =
let
val Abs_inverses' = map2 (curry op RS) in_car_final_thms Abs_inverses;
val morEs' = map (fn thm =>
@@ -1966,12 +1966,12 @@
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all ss
- (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_coiter Ts ss) ks))))
- (K (mk_mor_coiter_tac m mor_UNIV_thm dtor_defs coiter_defs Abs_inverses' morEs'
+ (HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors (map (mk_unfold Ts ss) ks))))
+ (K (mk_mor_unfold_tac m mor_UNIV_thm dtor_defs unfold_defs Abs_inverses' morEs'
map_comp_id_thms map_congs))
|> Thm.close_derivation
end;
- val coiter_thms = map (fn thm => (thm OF [mor_coiter_thm, UNIV_I]) RS sym) morE_thms;
+ val dtor_unfold_thms = map (fn thm => (thm OF [mor_unfold_thm, UNIV_I]) RS sym) morE_thms;
val (raw_coind_thms, raw_coind_thm) =
let
@@ -1990,15 +1990,15 @@
val unique_mor_thms =
let
val prems = [HOLogic.mk_Trueprop (mk_coalg passive_UNIVs Bs ss), HOLogic.mk_Trueprop
- (HOLogic.mk_conj (mk_mor Bs ss UNIVs dtors coiter_fs,
- mk_mor Bs ss UNIVs dtors coiter_fs_copy))];
+ (HOLogic.mk_conj (mk_mor Bs ss UNIVs dtors unfold_fs,
+ mk_mor Bs ss UNIVs dtors unfold_fs_copy))];
fun mk_fun_eq B f g z = HOLogic.mk_imp
(HOLogic.mk_mem (z, B), HOLogic.mk_eq (f $ z, g $ z));
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map4 mk_fun_eq Bs coiter_fs coiter_fs_copy zs));
+ (map4 mk_fun_eq Bs unfold_fs unfold_fs_copy zs));
val unique_mor = Skip_Proof.prove lthy [] []
- (fold_rev Logic.all (Bs @ ss @ coiter_fs @ coiter_fs_copy @ zs)
+ (fold_rev Logic.all (Bs @ ss @ unfold_fs @ unfold_fs_copy @ zs)
(Logic.list_implies (prems, unique)))
(K (mk_unique_mor_tac raw_coind_thms bis_image2_thm))
|> Thm.close_derivation;
@@ -2006,38 +2006,38 @@
map (fn thm => conjI RSN (2, thm RS mp)) (split_conj_thm unique_mor)
end;
- val (coiter_unique_mor_thms, coiter_unique_mor_thm) =
+ val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
let
- val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors coiter_fs);
- fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_coiter Ts ss i);
+ val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors unfold_fs);
+ fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_unfold Ts ss i);
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map2 mk_fun_eq coiter_fs ks));
+ (map2 mk_fun_eq unfold_fs ks));
val bis_thm = tcoalg_thm RSN (2, tcoalg_thm RS bis_image2_thm);
val mor_thm = mor_comp_thm OF [tcoalg_thm RS mor_final_thm, mor_Abs_thm];
val unique_mor = Skip_Proof.prove lthy [] []
- (fold_rev Logic.all (ss @ coiter_fs) (Logic.mk_implies (prem, unique)))
- (K (mk_coiter_unique_mor_tac raw_coind_thms bis_thm mor_thm coiter_defs))
+ (fold_rev Logic.all (ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
+ (K (mk_unfold_unique_mor_tac raw_coind_thms bis_thm mor_thm unfold_defs))
|> Thm.close_derivation;
in
`split_conj_thm unique_mor
end;
- val (coiter_unique_thms, coiter_unique_thm) = `split_conj_thm (split_conj_prems n
- (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS coiter_unique_mor_thm));
-
- val coiter_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) coiter_unique_mor_thms;
-
- val coiter_o_dtor_thms =
+ val (dtor_unfold_unique_thms, dtor_unfold_unique_thm) = `split_conj_thm (split_conj_prems n
+ (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS unfold_unique_mor_thm));
+
+ val unfold_dtor_thms = map (fn thm => mor_id_thm RS thm RS sym) unfold_unique_mor_thms;
+
+ val unfold_o_dtor_thms =
let
- val mor = mor_comp_thm OF [mor_str_thm, mor_coiter_thm];
+ val mor = mor_comp_thm OF [mor_str_thm, mor_unfold_thm];
in
- map2 (fn unique => fn coiter_ctor =>
- trans OF [mor RS unique, coiter_ctor]) coiter_unique_mor_thms coiter_dtor_thms
+ map2 (fn unique => fn unfold_ctor =>
+ trans OF [mor RS unique, unfold_ctor]) unfold_unique_mor_thms unfold_dtor_thms
end;
- val timer = time (timer "coiter definitions & thms");
+ val timer = time (timer "unfold definitions & thms");
val map_dtors = map2 (fn Ds => fn bnf =>
Term.list_comb (mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ FTs) bnf,
@@ -2050,7 +2050,7 @@
fun ctor_spec i ctorT =
let
val lhs = Free (ctor_name i, ctorT);
- val rhs = mk_coiter Ts map_dtors i;
+ val rhs = mk_unfold Ts map_dtors i;
in
mk_Trueprop_eq (lhs, rhs)
end;
@@ -2070,7 +2070,7 @@
val ctors = mk_ctors params';
val ctor_defs = map (Morphism.thm phi) ctor_def_frees;
- val ctor_o_dtor_thms = map2 (fold_defs lthy o single) ctor_defs coiter_o_dtor_thms;
+ val ctor_o_dtor_thms = map2 (fold_thms lthy o single) ctor_defs unfold_o_dtor_thms;
val dtor_o_ctor_thms =
let
@@ -2078,11 +2078,11 @@
mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
val goals = map3 mk_goal dtors ctors FTs;
in
- map5 (fn goal => fn ctor_def => fn coiter => fn map_comp_id => fn map_congL =>
+ map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_congL =>
Skip_Proof.prove lthy [] [] goal
- (mk_dtor_o_ctor_tac ctor_def coiter map_comp_id map_congL coiter_o_dtor_thms)
+ (mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtor_thms)
|> Thm.close_derivation)
- goals ctor_defs coiter_thms map_comp_id_thms map_congL_thms
+ goals ctor_defs dtor_unfold_thms map_comp_id_thms map_congL_thms
end;
val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
@@ -2104,20 +2104,20 @@
val ctor_inject_thms = map (fn thm => thm RS @{thm inj_eq}) inj_ctor_thms;
val ctor_exhaust_thms = map (fn thm => thm RS exE) ctor_nchotomy_thms;
- fun mk_ctor_dtor_coiter_like_thm dtor_inject dtor_ctor coiter =
- iffD1 OF [dtor_inject, trans OF [coiter, dtor_ctor RS sym]];
-
- val ctor_coiter_thms =
- map3 mk_ctor_dtor_coiter_like_thm dtor_inject_thms dtor_ctor_thms coiter_thms;
+ fun mk_ctor_dtor_unfold_like_thm dtor_inject dtor_ctor unfold =
+ iffD1 OF [dtor_inject, trans OF [unfold, dtor_ctor RS sym]];
+
+ val ctor_dtor_unfold_thms =
+ map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_unfold_thms;
val timer = time (timer "ctor definitions & thms");
val corec_Inl_sum_thms =
let
- val mor = mor_comp_thm OF [mor_sum_case_thm, mor_coiter_thm];
+ val mor = mor_comp_thm OF [mor_sum_case_thm, mor_unfold_thm];
in
- map2 (fn unique => fn coiter_dtor =>
- trans OF [mor RS unique, coiter_dtor]) coiter_unique_mor_thms coiter_dtor_thms
+ map2 (fn unique => fn unfold_dtor =>
+ trans OF [mor RS unique, unfold_dtor]) unfold_unique_mor_thms unfold_dtor_thms
end;
fun corec_bind i = Binding.suffix_name ("_" ^ dtor_corecN) (nth bs (i - 1));
@@ -2132,7 +2132,7 @@
dtors corec_ss corec_maps;
val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
- val rhs = HOLogic.mk_comp (mk_coiter Ts maps i, Inr_const T AT);
+ val rhs = HOLogic.mk_comp (mk_unfold Ts maps i, Inr_const T AT);
in
mk_Trueprop_eq (lhs, rhs)
end;
@@ -2155,7 +2155,7 @@
val sum_cases =
map2 (fn T => fn i => mk_sum_case (HOLogic.id_const T, mk_corec corec_ss i)) Ts ks;
- val corec_thms =
+ val dtor_corec_thms =
let
fun mk_goal i corec_s corec_map dtor z =
let
@@ -2166,15 +2166,15 @@
end;
val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
in
- map3 (fn goal => fn coiter => fn map_cong =>
+ map3 (fn goal => fn unfold => fn map_cong =>
Skip_Proof.prove lthy [] [] goal
- (mk_corec_tac m corec_defs coiter map_cong corec_Inl_sum_thms)
+ (mk_corec_tac m corec_defs unfold map_cong corec_Inl_sum_thms)
|> Thm.close_derivation)
- goals coiter_thms map_congs
+ goals dtor_unfold_thms map_congs
end;
- val ctor_corec_thms =
- map3 mk_ctor_dtor_coiter_like_thm dtor_inject_thms dtor_ctor_thms corec_thms;
+ val ctor_dtor_corec_thms =
+ map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms;
val timer = time (timer "corec definitions & thms");
@@ -2216,7 +2216,7 @@
val rel_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (rel_prems, concl));
val coinduct_params = rev (Term.add_tfrees rel_coinduct_goal []);
- val rel_coinduct = unfold_defs lthy @{thms diag_UNIV}
+ val rel_coinduct = unfold_thms lthy @{thms diag_UNIV}
(Skip_Proof.prove lthy [] [] rel_coinduct_goal
(K (mk_rel_coinduct_tac ks raw_coind_thm bis_rel_thm))
|> Thm.close_derivation);
@@ -2272,8 +2272,8 @@
val pred_of_rel_thms =
rel_defs @ @{thms Id_def' mem_Collect_eq fst_conv snd_conv split_conv};
- val pred_coinduct = unfold_defs lthy pred_of_rel_thms rel_coinduct;
- val pred_strong_coinduct = unfold_defs lthy pred_of_rel_thms rel_strong_coinduct;
+ val pred_coinduct = unfold_thms lthy pred_of_rel_thms rel_coinduct;
+ val pred_strong_coinduct = unfold_thms lthy pred_of_rel_thms rel_strong_coinduct;
in
(dtor_coinduct, rev (Term.add_tfrees dtor_coinduct_goal []), rel_coinduct, pred_coinduct,
dtor_strong_coinduct, rel_strong_coinduct, pred_strong_coinduct)
@@ -2332,7 +2332,7 @@
map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ map mk_T Ts)) Dss bnfs;
fun mk_Fmap mk_const fs Ts Fmap = Term.list_comb (Fmap, fs @ map mk_const Ts);
fun mk_map mk_const mk_T Ts fs Ts' dtors mk_maps =
- mk_coiter Ts' (map2 (fn dtor => fn Fmap =>
+ mk_unfold Ts' (map2 (fn dtor => fn Fmap =>
HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, dtor)) dtors (mk_maps Ts mk_T));
val mk_map_id = mk_map HOLogic.id_const I;
val mk_mapsAB = mk_maps passiveAs passiveBs;
@@ -2374,11 +2374,11 @@
val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's;
val cTs = map (SOME o certifyT lthy) FTs';
val maps =
- map5 (fn goal => fn cT => fn coiter => fn map_comp' => fn map_cong =>
+ map5 (fn goal => fn cT => fn unfold => fn map_comp' => fn map_cong =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_map_tac m n cT coiter map_comp' map_cong))
+ (K (mk_map_tac m n cT unfold map_comp' map_cong))
|> Thm.close_derivation)
- goals cTs coiter_thms map_comp's map_congs;
+ goals cTs dtor_unfold_thms map_comp's map_congs;
in
map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps
end;
@@ -2392,7 +2392,7 @@
fs_maps gs_maps fgs_maps)))
in
split_conj_thm (Skip_Proof.prove lthy [] [] goal
- (K (mk_map_comp_tac m n map_thms map_comps map_congs coiter_unique_thm))
+ (K (mk_map_comp_tac m n map_thms map_comps map_congs dtor_unfold_unique_thm))
|> Thm.close_derivation)
end;
@@ -2408,7 +2408,7 @@
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (mk_map_unique_tac coiter_unique_thm map_comps)
+ (mk_map_unique_tac dtor_unfold_unique_thm map_comps)
|> Thm.close_derivation
end;
@@ -2566,7 +2566,7 @@
(map2 (curry (op $)) dtors Jzs) (map2 (curry (op $)) dtor's Jz's);
val pickF_ss = map3 (fn pickF => fn z => fn z' =>
HOLogic.mk_split (Term.absfree z (Term.absfree z' pickF))) pickFs Jzs' Jz's';
- val picks = map (mk_coiter XTs pickF_ss) ks;
+ val picks = map (mk_unfold XTs pickF_ss) ks;
val wpull_prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s));
@@ -2613,7 +2613,7 @@
map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
Skip_Proof.prove lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms
map_comp's pickWP_assms_tacs) |> Thm.close_derivation,
- Skip_Proof.prove lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def coiter_thms
+ Skip_Proof.prove lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms
map_comp's) |> Thm.close_derivation)
end;
@@ -2637,8 +2637,8 @@
val thms =
map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
singleton (Proof_Context.export names_lthy lthy) (Skip_Proof.prove lthy [] [] goal
- (mk_pick_col_tac m j cts rec_0s rec_Sucs coiter_thms set_natural'ss map_wpull_thms
- pickWP_assms_tacs))
+ (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_natural'ss
+ map_wpull_thms pickWP_assms_tacs))
|> Thm.close_derivation)
ls goals ctss hset_rec_0ss' hset_rec_Sucss';
in
@@ -2647,7 +2647,8 @@
val timer = time (timer "helpers for BNF properties");
- val map_id_tacs = map2 (K oo mk_map_id_tac map_thms) coiter_unique_thms coiter_dtor_thms;
+ val map_id_tacs =
+ map2 (K oo mk_map_id_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
val map_comp_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp_thms;
val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
val set_nat_tacss =
@@ -2716,7 +2717,7 @@
map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
((set_minimal
|> Drule.instantiate' [] (mk_induct_tinst phis jsets y y')
- |> unfold_defs lthy incls) OF
+ |> unfold_thms lthy incls) OF
(replicate n ballI @
maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
|> singleton (Proof_Context.export names_lthy lthy)
@@ -2806,7 +2807,7 @@
end;
fun mk_coind_wits ((I, dummys), (args, thms)) =
- ((I, dummys), (map (fn i => mk_coiter Ts args i $ HOLogic.unit) ks, thms));
+ ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms));
val coind_witss =
maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
@@ -2830,7 +2831,7 @@
in
map2 (fn goal => fn induct =>
Skip_Proof.prove lthy [] [] goal
- (mk_coind_wit_tac induct coiter_thms (flat set_natural'ss) wit_thms)
+ (mk_coind_wit_tac induct dtor_unfold_thms (flat set_natural'ss) wit_thms)
|> Thm.close_derivation)
goals hset_induct_thms
|> map split_conj_thm
@@ -2867,10 +2868,10 @@
|> register_bnf (Local_Theory.full_name lthy b))
tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
- val fold_maps = fold_defs lthy (map (fn bnf =>
+ val fold_maps = fold_thms lthy (map (fn bnf =>
mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Jbnfs);
- val fold_sets = fold_defs lthy (maps (fn bnf =>
+ val fold_sets = fold_thms lthy (maps (fn bnf =>
map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Jbnfs);
val timer = time (timer "registered new codatatypes as BNFs");
@@ -2965,25 +2966,25 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
val notes =
- [(dtor_coitersN, coiter_thms),
- (dtor_coiter_uniqueN, coiter_unique_thms),
- (dtor_corecsN, corec_thms),
+ [(ctor_dtorN, ctor_dtor_thms),
+ (ctor_dtor_unfoldsN, ctor_dtor_unfold_thms),
+ (ctor_dtor_corecsN, ctor_dtor_corec_thms),
+ (ctor_exhaustN, ctor_exhaust_thms),
+ (ctor_injectN, ctor_inject_thms),
+ (dtor_corecsN, dtor_corec_thms),
(dtor_ctorN, dtor_ctor_thms),
- (ctor_dtorN, ctor_dtor_thms),
+ (dtor_exhaustN, dtor_exhaust_thms),
(dtor_injectN, dtor_inject_thms),
- (dtor_exhaustN, dtor_exhaust_thms),
- (ctor_injectN, ctor_inject_thms),
- (ctor_exhaustN, ctor_exhaust_thms),
- (ctor_dtor_coitersN, ctor_coiter_thms),
- (ctor_dtor_corecsN, ctor_corec_thms)]
+ (dtor_unfold_uniqueN, dtor_unfold_unique_thms),
+ (dtor_unfoldsN, dtor_unfold_thms)]
|> map (apsnd (map single))
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ((dtors, ctors, coiters, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
- ctor_inject_thms, ctor_coiter_thms, ctor_corec_thms),
+ ((dtors, ctors, unfolds, corecs, dtor_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
+ ctor_inject_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -30,7 +30,6 @@
{prems: 'a, context: Proof.context} -> tactic
val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
- val mk_coiter_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
thm list list -> tactic
val mk_col_natural_tac: cterm option list -> thm list -> thm list -> thm list -> thm list list ->
@@ -69,8 +68,6 @@
thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list ->
thm list list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
- val mk_mor_coiter_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
- thm list -> tactic
val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic
val mk_mor_elim_tac: thm -> tactic
val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list ->
@@ -85,6 +82,8 @@
{prems: thm list, context: Proof.context} -> tactic
val mk_mor_thePull_pick_tac: thm -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
+ val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
+ thm list -> tactic
val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic
val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
@@ -115,6 +114,7 @@
val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
thm list list -> thm list list -> thm -> thm list list -> tactic
+ val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
val mk_unique_mor_tac: thm list -> thm -> tactic
val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
@@ -345,7 +345,7 @@
fun mk_bis_Gr_tac bis_rel rel_Grs mor_images morEs coalg_ins
{context = ctxt, prems = _} =
- unfold_defs_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
+ unfold_thms_tac ctxt (bis_rel :: @{thm diag_Gr} :: rel_Grs) THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn thm => rtac (@{thm Gr_incl} RS ssubst) THEN' etac thm) mor_images,
CONJ_WRAP' (fn (coalg_in, morE) =>
@@ -358,7 +358,7 @@
val n = length in_monos;
val ks = 1 upto n;
in
- unfold_defs_tac ctxt [bis_def] THEN
+ unfold_thms_tac ctxt [bis_def] THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn i =>
EVERY' [rtac @{thm UN_least}, dtac bspec, atac,
@@ -421,7 +421,7 @@
rtac conjI, etac @{thm Shift_prefCl},
rtac conjI, rtac ballI,
rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1,
- SELECT_GOAL (unfold_defs_tac ctxt @{thms Succ_Shift shift_def}),
+ SELECT_GOAL (unfold_thms_tac ctxt @{thms Succ_Shift shift_def}),
etac bspec, etac @{thm ShiftD},
CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD},
dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i),
@@ -445,7 +445,7 @@
rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift},
rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
in
- unfold_defs_tac ctxt defs THEN
+ unfold_thms_tac ctxt defs THEN
CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1
end;
@@ -598,7 +598,7 @@
val m = length strT_hsets;
in
if m = 0 then atac 1
- else (unfold_defs_tac ctxt [isNode_def] THEN
+ else (unfold_thms_tac ctxt [isNode_def] THEN
EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
rtac exI, rtac conjI, atac,
CONJ_WRAP' (fn (thm, i) => if i > m then atac
@@ -987,7 +987,7 @@
(K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
if n = 1 then K all_tac
else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
- SELECT_GOAL (unfold_defs_tac ctxt [from_to_sbd]), rtac refl,
+ SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl,
rtac refl])
ks to_sbd_injs from_to_sbds)];
in
@@ -1044,7 +1044,7 @@
fun mk_mor_Rep_tac m defs Reps Abs_inverses coalg_final_setss map_comp_ids map_congLs
{context = ctxt, prems = _} =
- unfold_defs_tac ctxt defs THEN
+ unfold_thms_tac ctxt defs THEN
EVERY' [rtac conjI,
CONJ_WRAP' (fn thm => rtac ballI THEN' rtac thm) Reps,
CONJ_WRAP' (fn (Rep, ((map_comp_id, map_congL), coalg_final_sets)) =>
@@ -1056,21 +1056,21 @@
(Reps ~~ ((map_comp_ids ~~ map_congLs) ~~ coalg_final_setss))] 1;
fun mk_mor_Abs_tac defs Abs_inverses {context = ctxt, prems = _} =
- unfold_defs_tac ctxt defs THEN
+ unfold_thms_tac ctxt defs THEN
EVERY' [rtac conjI,
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) Abs_inverses,
CONJ_WRAP' (fn thm => rtac ballI THEN' etac (thm RS arg_cong RS sym)) Abs_inverses] 1;
-fun mk_mor_coiter_tac m mor_UNIV dtor_defs coiter_defs Abs_inverses morEs map_comp_ids map_congs =
+fun mk_mor_unfold_tac m mor_UNIV dtor_defs unfold_defs Abs_inverses morEs map_comp_ids map_congs =
EVERY' [rtac iffD2, rtac mor_UNIV,
- CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, coiter_def), (map_comp_id, map_cong))) =>
+ CONJ_WRAP' (fn ((Abs_inverse, morE), ((dtor_def, unfold_def), (map_comp_id, map_cong))) =>
EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (dtor_def RS trans),
- rtac (coiter_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
+ rtac (unfold_def RS arg_cong RS trans), rtac (Abs_inverse RS arg_cong RS trans),
rtac (morE RS arg_cong RS trans), rtac (map_comp_id RS trans),
rtac (o_apply RS trans RS sym), rtac map_cong,
REPEAT_DETERM_N m o rtac refl,
- EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) coiter_defs)])
- ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ coiter_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
+ EVERY' (map (fn thm => rtac (thm RS trans) THEN' rtac (o_apply RS sym)) unfold_defs)])
+ ((Abs_inverses ~~ morEs) ~~ ((dtor_defs ~~ unfold_defs) ~~ (map_comp_ids ~~ map_congs)))] 1;
fun mk_raw_coind_tac bis_def bis_cong bis_O bis_converse bis_Gr tcoalg coalgT mor_T_final
sbis_lsbis lsbis_incls incl_lsbiss equiv_LSBISs mor_Rep Rep_injects =
@@ -1103,23 +1103,23 @@
etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac])
raw_coinds 1;
-fun mk_coiter_unique_mor_tac raw_coinds bis mor coiter_defs =
- CONJ_WRAP' (fn (raw_coind, coiter_def) =>
+fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
+ CONJ_WRAP' (fn (raw_coind, unfold_def) =>
EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
- rtac @{thm image2_eqI}, rtac refl, rtac (coiter_def RS arg_cong RS trans),
- rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ coiter_defs) 1;
+ rtac @{thm image2_eqI}, rtac refl, rtac (unfold_def RS arg_cong RS trans),
+ rtac (o_apply RS sym), rtac UNIV_I]) (raw_coinds ~~ unfold_defs) 1;
-fun mk_dtor_o_ctor_tac ctor_def coiter map_comp_id map_congL coiter_o_dtors
+fun mk_dtor_o_ctor_tac ctor_def unfold map_comp_id map_congL unfold_o_dtors
{context = ctxt, prems = _} =
- unfold_defs_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
- rtac trans, rtac coiter, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
+ unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
+ rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
EVERY' (map (fn thm =>
- rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) coiter_o_dtors),
+ rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) unfold_o_dtors),
rtac sym, rtac @{thm id_apply}] 1;
-fun mk_corec_tac m corec_defs coiter map_cong corec_Inls {context = ctxt, prems = _} =
- unfold_defs_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
- rtac trans, rtac coiter, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
+fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
+ rtac trans, rtac unfold, fo_rtac (@{thm sum.cases(2)} RS arg_cong RS trans) ctxt, rtac map_cong,
REPEAT_DETERM_N m o rtac refl,
EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
@@ -1179,9 +1179,9 @@
rtac impI, REPEAT_DETERM o etac conjE,
CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) ks] 1;
-fun mk_map_tac m n cT coiter map_comp' map_cong =
+fun mk_map_tac m n cT unfold map_comp' map_cong =
EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
- rtac (coiter RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
+ rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp' RS box_equals)), rtac map_cong,
REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong),
rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
@@ -1201,12 +1201,12 @@
REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
-fun mk_map_id_tac maps coiter_unique coiter_dtor =
- EVERY' [rtac (coiter_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
- rtac coiter_dtor] 1;
+fun mk_map_id_tac maps unfold_unique unfold_dtor =
+ EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
+ rtac unfold_dtor] 1;
-fun mk_map_comp_tac m n maps map_comps map_congs coiter_unique =
- EVERY' [rtac coiter_unique,
+fun mk_map_comp_tac m n maps map_comps map_congs unfold_unique =
+ EVERY' [rtac unfold_unique,
EVERY' (map3 (fn map_thm => fn map_comp => fn map_cong =>
EVERY' (map rtac
([@{thm o_assoc} RS trans,
@@ -1255,9 +1255,9 @@
rtac conjI, rtac refl, rtac refl]) ks]) 1
end
-fun mk_map_unique_tac coiter_unique map_comps {context = ctxt, prems = _} =
- rtac coiter_unique 1 THEN
- unfold_defs_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
+fun mk_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
+ rtac unfold_unique 1 THEN
+ unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
ALLGOALS (etac sym);
fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss
@@ -1266,11 +1266,11 @@
val n = length map_simps;
in
EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
- REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_defs_tac ctxt rec_0s),
+ REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
REPEAT_DETERM o rtac allI,
CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY'
- [SELECT_GOAL (unfold_defs_tac ctxt
+ [SELECT_GOAL (unfold_thms_tac ctxt
(rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
rtac @{thm Un_cong}, rtac refl,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
@@ -1367,14 +1367,14 @@
fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs
{context = ctxt, prems = _} =
- unfold_defs_tac ctxt [coalg_def] THEN
+ unfold_thms_tac ctxt [coalg_def] THEN
CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) =>
EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
pickWP_assms_tac,
- SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}), rtac impI,
+ SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac CollectI,
REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
@@ -1389,16 +1389,16 @@
let
val n = length map_comps;
in
- unfold_defs_tac ctxt [mor_def] THEN
+ unfold_thms_tac ctxt [mor_def] THEN
EVERY' [rtac conjI,
CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
hyp_subst_tac,
- SELECT_GOAL (unfold_defs_tac ctxt @{thms o_apply prod.cases}),
+ SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
rtac (map_comp RS trans),
- SELECT_GOAL (unfold_defs_tac ctxt (conv :: @{thms o_id id_o})),
+ SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
pickWP_assms_tac])
(map_wpulls ~~ (pickWP_assms_tacs ~~ map_comps))] 1
@@ -1407,17 +1407,17 @@
val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
-fun mk_mor_thePull_pick_tac mor_def coiters map_comps {context = ctxt, prems = _} =
- unfold_defs_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
- CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) coiters 1 THEN
- CONJ_WRAP' (fn (coiter, map_comp) =>
+fun mk_mor_thePull_pick_tac mor_def unfolds map_comps {context = ctxt, prems = _} =
+ unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
+ CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
+ CONJ_WRAP' (fn (unfold, map_comp) =>
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
hyp_subst_tac,
- SELECT_GOAL (unfold_defs_tac ctxt (coiter :: map_comp :: @{thms comp_def id_def})),
+ SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
rtac refl])
- (coiters ~~ map_comps) 1;
+ (unfolds ~~ map_comps) 1;
-fun mk_pick_col_tac m j cts rec_0s rec_Sucs coiters set_naturalss map_wpulls pickWP_assms_tacs
+fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_naturalss map_wpulls pickWP_assms_tacs
{context = ctxt, prems = _} =
let
val n = length rec_0s;
@@ -1428,7 +1428,7 @@
CONJ_WRAP' (fn thm => EVERY'
[rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
REPEAT_DETERM o rtac allI,
- CONJ_WRAP' (fn (rec_Suc, ((coiter, set_naturals), (map_wpull, pickWP_assms_tac))) =>
+ CONJ_WRAP' (fn (rec_Suc, ((unfold, set_naturals), (map_wpull, pickWP_assms_tac))) =>
EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
@@ -1437,16 +1437,16 @@
rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
rtac ord_eq_le_trans, rtac rec_Suc,
rtac @{thm Un_least},
- SELECT_GOAL (unfold_defs_tac ctxt [coiter, nth set_naturals (j - 1),
+ SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_naturals (j - 1),
@{thm prod.cases}]),
etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) =>
EVERY' [rtac @{thm UN_least},
- SELECT_GOAL (unfold_defs_tac ctxt [coiter, set_natural, @{thm prod.cases}]),
+ SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_natural, @{thm prod.cases}]),
etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
(ks ~~ rev (drop m set_naturals))])
- (rec_Sucs ~~ ((coiters ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
+ (rec_Sucs ~~ ((unfolds ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
end;
fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
@@ -1477,7 +1477,7 @@
ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
REPEAT_DETERM (atac 1 ORELSE
EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
- K (unfold_defs_tac ctxt dtor_ctors),
+ K (unfold_thms_tac ctxt dtor_ctors),
REPEAT_DETERM_N n o etac UnE,
REPEAT_DETERM o
(TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
@@ -1485,11 +1485,11 @@
(dresolve_tac wit THEN'
(etac FalseE ORELSE'
EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
- K (unfold_defs_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
+ K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
-fun mk_coind_wit_tac induct coiters set_nats wits {context = ctxt, prems = _} =
+fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
- unfold_defs_tac ctxt (coiters @ set_nats @ @{thms image_id id_apply}) THEN
+ unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
ALLGOALS (TRY o
FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Fri Sep 21 15:53:29 2012 +0200
@@ -973,20 +973,20 @@
val map_FT_inits = map2 (fn Ds =>
mk_map_of_bnf Ds (passiveAs @ Ts) (passiveAs @ active_initTs)) Dss bnfs;
val fTs = map2 (curry op -->) Ts activeAs;
- val iterT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs);
+ val foldT = Library.foldr1 HOLogic.mk_prodT (map2 (curry op -->) Ts activeAs);
val rec_sTs = map (Term.typ_subst_atomic (activeBs ~~ Ts)) prod_sTs;
val rec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts;
val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
- (iter_f, iter_f')), fs), rec_ss), names_lthy) = names_lthy
+ (fold_f, fold_f')), fs), rec_ss), names_lthy) = names_lthy
|> mk_Frees' "z1" Ts
||>> mk_Frees' "z2" Ts'
||>> mk_Frees' "x" FTs
||>> mk_Frees "y" FTs'
||>> mk_Freess' "z" setFTss
- ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") iterT
+ ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT
||>> mk_Frees "f" fTs
||>> mk_Frees "s" rec_sTs;
@@ -1049,90 +1049,90 @@
val timer = time (timer "ctor definitions & thms");
- val iter_fun = Term.absfree iter_f'
- (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n iter_f) ks));
- val iterx = HOLogic.choice_const iterT $ iter_fun;
+ val fold_fun = Term.absfree fold_f'
+ (mk_mor UNIVs ctors active_UNIVs ss (map (mk_nthN n fold_f) ks));
+ val foldx = HOLogic.choice_const foldT $ fold_fun;
- fun iter_bind i = Binding.suffix_name ("_" ^ ctor_iterN) (nth bs (i - 1));
- val iter_name = Binding.name_of o iter_bind;
- val iter_def_bind = rpair [] o Thm.def_binding o iter_bind;
+ fun fold_bind i = Binding.suffix_name ("_" ^ ctor_foldN) (nth bs (i - 1));
+ val fold_name = Binding.name_of o fold_bind;
+ val fold_def_bind = rpair [] o Thm.def_binding o fold_bind;
- fun iter_spec i T AT =
+ fun fold_spec i T AT =
let
- val iterT = Library.foldr (op -->) (sTs, T --> AT);
+ val foldT = Library.foldr (op -->) (sTs, T --> AT);
- val lhs = Term.list_comb (Free (iter_name i, iterT), ss);
- val rhs = mk_nthN n iterx i;
+ val lhs = Term.list_comb (Free (fold_name i, foldT), ss);
+ val rhs = mk_nthN n foldx i;
in
mk_Trueprop_eq (lhs, rhs)
end;
- val ((iter_frees, (_, iter_def_frees)), (lthy, lthy_old)) =
+ val ((fold_frees, (_, fold_def_frees)), (lthy, lthy_old)) =
lthy
|> fold_map3 (fn i => fn T => fn AT =>
Specification.definition
- (SOME (iter_bind i, NONE, NoSyn), (iter_def_bind i, iter_spec i T AT)))
+ (SOME (fold_bind i, NONE, NoSyn), (fold_def_bind i, fold_spec i T AT)))
ks Ts activeAs
|>> apsnd split_list o split_list
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
- val iters = map (Morphism.term phi) iter_frees;
- val iter_names = map (fst o dest_Const) iters;
- fun mk_iter Ts ss i = Term.list_comb (Const (nth iter_names (i - 1), Library.foldr (op -->)
+ val folds = map (Morphism.term phi) fold_frees;
+ val fold_names = map (fst o dest_Const) folds;
+ fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
(map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
- val iter_defs = map (Morphism.thm phi) iter_def_frees;
+ val fold_defs = map (Morphism.thm phi) fold_def_frees;
- val mor_iter_thm =
+ val mor_fold_thm =
let
val ex_mor = talg_thm RS init_ex_mor_thm;
val mor_cong = mor_cong_thm OF (map (mk_nth_conv n) ks);
val mor_comp = mor_Rep_thm RS mor_comp_thm;
- val cT = certifyT lthy iterT;
- val ct = certify lthy iter_fun
+ val cT = certifyT lthy foldT;
+ val ct = certify lthy fold_fun
in
singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] []
- (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_iter Ts ss) ks)))
- (K (mk_mor_iter_tac cT ct iter_defs ex_mor (mor_comp RS mor_cong))))
+ (HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss (map (mk_fold Ts ss) ks)))
+ (K (mk_mor_fold_tac cT ct fold_defs ex_mor (mor_comp RS mor_cong))))
|> Thm.close_derivation
end;
- val iter_thms = map (fn morE => rule_by_tactic lthy
+ val ctor_fold_thms = map (fn morE => rule_by_tactic lthy
((rtac CollectI THEN' CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto m + n)) 1)
- (mor_iter_thm RS morE)) morE_thms;
+ (mor_fold_thm RS morE)) morE_thms;
- val (iter_unique_mor_thms, iter_unique_mor_thm) =
+ val (fold_unique_mor_thms, fold_unique_mor_thm) =
let
val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors active_UNIVs ss fs);
- fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_iter Ts ss i);
+ fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_fold Ts ss i);
val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
val unique_mor = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (ss @ fs) (Logic.mk_implies (prem, unique)))
- (K (mk_iter_unique_mor_tac type_defs init_unique_mor_thms Reps
- mor_comp_thm mor_Abs_thm mor_iter_thm))
+ (K (mk_fold_unique_mor_tac type_defs init_unique_mor_thms Reps
+ mor_comp_thm mor_Abs_thm mor_fold_thm))
|> Thm.close_derivation;
in
`split_conj_thm unique_mor
end;
- val iter_unique_thms =
+ val ctor_fold_unique_thms =
split_conj_thm (mk_conjIN n RS
- (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS iter_unique_mor_thm))
+ (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS fold_unique_mor_thm))
- val iter_ctor_thms =
+ val fold_ctor_thms =
map (fn thm => (mor_incl_thm OF replicate n @{thm subset_UNIV}) RS thm RS sym)
- iter_unique_mor_thms;
+ fold_unique_mor_thms;
- val ctor_o_iter_thms =
+ val ctor_o_fold_thms =
let
- val mor = mor_comp_thm OF [mor_iter_thm, mor_str_thm];
+ val mor = mor_comp_thm OF [mor_fold_thm, mor_str_thm];
in
- map2 (fn unique => fn iter_ctor =>
- trans OF [mor RS unique, iter_ctor]) iter_unique_mor_thms iter_ctor_thms
+ map2 (fn unique => fn fold_ctor =>
+ trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
end;
- val timer = time (timer "iter definitions & thms");
+ val timer = time (timer "fold definitions & thms");
val map_ctors = map2 (fn Ds => fn bnf =>
Term.list_comb (mk_map_of_bnf Ds (passiveAs @ FTs) (passiveAs @ Ts) bnf,
@@ -1147,7 +1147,7 @@
val dtorT = T --> FT;
val lhs = Free (dtor_name i, dtorT);
- val rhs = mk_iter Ts map_ctors i;
+ val rhs = mk_fold Ts map_ctors i;
in
mk_Trueprop_eq (lhs, rhs)
end;
@@ -1167,7 +1167,7 @@
val dtors = mk_dtors params';
val dtor_defs = map (Morphism.thm phi) dtor_def_frees;
- val ctor_o_dtor_thms = map2 (fold_defs lthy o single) dtor_defs ctor_o_iter_thms;
+ val ctor_o_dtor_thms = map2 (fold_thms lthy o single) dtor_defs ctor_o_fold_thms;
val dtor_o_ctor_thms =
let
@@ -1175,11 +1175,11 @@
mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
val goals = map3 mk_goal dtors ctors FTs;
in
- map5 (fn goal => fn dtor_def => fn iterx => fn map_comp_id => fn map_congL =>
+ map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_congL =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_dtor_o_ctor_tac dtor_def iterx map_comp_id map_congL ctor_o_iter_thms))
+ (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_fold_thms))
|> Thm.close_derivation)
- goals dtor_defs iter_thms map_comp_id_thms map_congL_thms
+ goals dtor_defs ctor_fold_thms map_comp_id_thms map_congL_thms
end;
val dtor_ctor_thms = map (fn thm => thm RS @{thm pointfree_idE}) dtor_o_ctor_thms;
@@ -1205,10 +1205,10 @@
val fst_rec_pair_thms =
let
- val mor = mor_comp_thm OF [mor_iter_thm, mor_convol_thm];
+ val mor = mor_comp_thm OF [mor_fold_thm, mor_convol_thm];
in
- map2 (fn unique => fn iter_ctor =>
- trans OF [mor RS unique, iter_ctor]) iter_unique_mor_thms iter_ctor_thms
+ map2 (fn unique => fn fold_ctor =>
+ trans OF [mor RS unique, fold_ctor]) fold_unique_mor_thms fold_ctor_thms
end;
fun rec_bind i = Binding.suffix_name ("_" ^ ctor_recN) (nth bs (i - 1));
@@ -1223,7 +1223,7 @@
ctors rec_ss rec_maps;
val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss);
- val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_iter Ts maps i);
+ val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts maps i);
in
mk_Trueprop_eq (lhs, rhs)
end;
@@ -1245,7 +1245,7 @@
val rec_defs = map (Morphism.thm phi) rec_def_frees;
val convols = map2 (fn T => fn i => mk_convol (HOLogic.id_const T, mk_rec rec_ss i)) Ts ks;
- val rec_thms =
+ val ctor_rec_thms =
let
fun mk_goal i rec_s rec_map ctor x =
let
@@ -1256,10 +1256,10 @@
end;
val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
in
- map2 (fn goal => fn iterx =>
- Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs iterx fst_rec_pair_thms)
+ map2 (fn goal => fn foldx =>
+ Skip_Proof.prove lthy [] [] goal (mk_rec_tac rec_defs foldx fst_rec_pair_thms)
|> Thm.close_derivation)
- goals iter_thms
+ goals ctor_fold_thms
end;
val timer = time (timer "rec definitions & thms");
@@ -1381,10 +1381,10 @@
mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
fun mk_passive_maps ATs BTs Ts =
map2 (fn Ds => mk_map_of_bnf Ds (ATs @ Ts) (BTs @ Ts)) Dss bnfs;
- fun mk_map_iter_arg fs Ts ctor fmap =
+ fun mk_map_fold_arg fs Ts ctor fmap =
HOLogic.mk_comp (ctor, Term.list_comb (fmap, fs @ map HOLogic.id_const Ts));
fun mk_map Ts fs Ts' ctors mk_maps =
- mk_iter Ts (map2 (mk_map_iter_arg fs Ts') ctors (mk_maps Ts'));
+ mk_fold Ts (map2 (mk_map_fold_arg fs Ts') ctors (mk_maps Ts'));
val pmapsABT' = mk_passive_maps passiveAs passiveBs;
val fs_maps = map (mk_map Ts fs Ts' ctor's pmapsABT') ks;
val fs_copy_maps = map (mk_map Ts fs_copy Ts' ctor's pmapsABT') ks;
@@ -1401,10 +1401,10 @@
HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps))));
val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's;
val maps =
- map4 (fn goal => fn iterx => fn map_comp_id => fn map_cong =>
- Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n iterx map_comp_id map_cong))
+ map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong =>
+ Skip_Proof.prove lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong))
|> Thm.close_derivation)
- goals iter_thms map_comp_id_thms map_congs;
+ goals ctor_fold_thms map_comp_id_thms map_congs;
in
map (fn thm => thm RS @{thm pointfreeE}) maps
end;
@@ -1420,7 +1420,7 @@
(map2 (curry HOLogic.mk_eq) us fs_maps));
val unique = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (K (mk_map_unique_tac m mor_def iter_unique_mor_thm map_comp_id_thms map_congs))
+ (K (mk_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs))
|> Thm.close_derivation;
in
`split_conj_thm unique
@@ -1451,7 +1451,7 @@
end;
val colss = map5 (fn l => fn T => map3 (mk_col l T)) ls passiveAs AFss AFss' setsss;
- val setss_by_range = map (fn cols => map (mk_iter Ts cols) ks) colss;
+ val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss;
val setss_by_bnf = transpose setss_by_range;
val set_simp_thmss =
@@ -1461,9 +1461,9 @@
HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
val goalss =
map3 (fn sets => map4 (mk_goal sets) ctors sets) setss_by_range colss map_setss;
- val setss = map (map2 (fn iterx => fn goal =>
- Skip_Proof.prove lthy [] [] goal (K (mk_set_tac iterx)) |> Thm.close_derivation)
- iter_thms) goalss;
+ val setss = map (map2 (fn foldx => fn goal =>
+ Skip_Proof.prove lthy [] [] goal (K (mk_set_tac foldx)) |> Thm.close_derivation)
+ ctor_fold_thms) goalss;
fun mk_simp_goal pas_set act_sets sets ctor z set =
Logic.all z (mk_Trueprop_eq (set $ (ctor $ z),
@@ -1712,11 +1712,11 @@
|> register_bnf (Local_Theory.full_name lthy b))
tacss bs fs_maps setss_by_bnf Ts ctor_witss lthy;
- val fold_maps = fold_defs lthy (map (fn bnf =>
+ val fold_maps = fold_thms lthy (map (fn bnf =>
mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Ibnfs);
- val fold_sets = fold_defs lthy (maps (fn bnf =>
- map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs);
+ val fold_sets = fold_thms lthy (maps (fn bnf =>
+ map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs);
val timer = time (timer "registered new datatypes as BNFs");
@@ -1806,10 +1806,10 @@
val notes =
[(ctor_dtorN, ctor_dtor_thms),
(ctor_exhaustN, ctor_exhaust_thms),
+ (ctor_fold_uniqueN, ctor_fold_unique_thms),
+ (ctor_foldsN, ctor_fold_thms),
(ctor_injectN, ctor_inject_thms),
- (ctor_iter_uniqueN, iter_unique_thms),
- (ctor_itersN, iter_thms),
- (ctor_recsN, rec_thms),
+ (ctor_recsN, ctor_rec_thms),
(dtor_ctorN, dtor_ctor_thms),
(dtor_exhaustN, dtor_exhaust_thms),
(dtor_injectN, dtor_inject_thms)]
@@ -1819,8 +1819,8 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ((dtors, ctors, iters, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms,
- iter_thms, rec_thms),
+ ((dtors, ctors, folds, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms,
+ ctor_fold_thms, ctor_rec_thms),
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -32,7 +32,7 @@
val mk_init_unique_mor_tac: int -> thm -> thm -> thm list -> thm list -> thm list -> thm list ->
thm list -> tactic
val mk_iso_alt_tac: thm list -> thm -> tactic
- val mk_iter_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
+ val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
val mk_least_min_alg_tac: thm -> thm -> tactic
val mk_lfp_map_wpull_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list list ->
thm list list list -> thm list -> tactic
@@ -56,7 +56,7 @@
val mk_mor_elim_tac: thm -> tactic
val mk_mor_incl_tac: thm -> thm list -> tactic
val mk_mor_inv_tac: thm -> thm -> thm list list -> thm list -> thm list -> thm list -> tactic
- val mk_mor_iter_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic
+ val mk_mor_fold_tac: ctyp -> cterm -> thm list -> thm -> thm -> tactic
val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
thm list -> tactic
val mk_mor_str_tac: 'a list -> thm -> tactic
@@ -386,7 +386,7 @@
fun mk_alg_select_tac Abs_inverse {context = ctxt, prems = _} =
EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac] 1 THEN
- unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
+ unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs) THEN atac 1;
fun mk_mor_select_tac mor_def mor_cong mor_comp mor_incl_min_alg alg_def alg_select
alg_sets set_natural's str_init_defs =
@@ -431,7 +431,7 @@
rtac mor_select THEN' atac THEN' rtac CollectI THEN'
REPEAT_DETERM o rtac exI THEN'
rtac conjI THEN' rtac refl THEN' atac THEN'
- K (unfold_defs_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
+ K (unfold_thms_tac ctxt (Abs_inverse :: fst_snd_convs)) THEN'
etac mor_comp THEN' etac mor_incl_min_alg) 1
end;
@@ -486,7 +486,7 @@
end;
fun mk_mor_Rep_tac ctor_defs copy bijs inver_Abss inver_Reps {context = ctxt, prems = _} =
- (K (unfold_defs_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
+ (K (unfold_thms_tac ctxt ctor_defs) THEN' rtac conjunct1 THEN' rtac copy THEN'
EVERY' (map (fn bij => EVERY' [rtac bij, atac, etac bexI, rtac UNIV_I]) bijs) THEN'
EVERY' (map rtac inver_Abss) THEN'
EVERY' (map rtac inver_Reps)) 1;
@@ -497,34 +497,34 @@
EVERY' [rtac conjI, rtac subset_UNIV, rtac conjI, rtac inver_Rep, rtac inver_Abs])
inver_Abss inver_Reps)) 1;
-fun mk_mor_iter_tac cT ct iter_defs ex_mor mor =
- (EVERY' (map stac iter_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN'
- REPEAT_DETERM_N (length iter_defs) o etac exE THEN'
+fun mk_mor_fold_tac cT ct fold_defs ex_mor mor =
+ (EVERY' (map stac fold_defs) THEN' EVERY' [rtac rev_mp, rtac ex_mor, rtac impI] THEN'
+ REPEAT_DETERM_N (length fold_defs) o etac exE THEN'
rtac (Drule.instantiate' [SOME cT] [SOME ct] @{thm someI}) THEN' etac mor) 1;
-fun mk_iter_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_iter =
+fun mk_fold_unique_mor_tac type_defs init_unique_mors Reps mor_comp mor_Abs mor_fold =
let
fun mk_unique type_def =
EVERY' [rtac @{thm surj_fun_eq}, rtac (type_def RS @{thm type_definition.Abs_image}),
rtac ballI, resolve_tac init_unique_mors,
EVERY' (map (fn thm => atac ORELSE' rtac thm) Reps),
rtac mor_comp, rtac mor_Abs, atac,
- rtac mor_comp, rtac mor_Abs, rtac mor_iter];
+ rtac mor_comp, rtac mor_Abs, rtac mor_fold];
in
CONJ_WRAP' mk_unique type_defs 1
end;
-fun mk_dtor_o_ctor_tac dtor_def iterx map_comp_id map_congL ctor_o_iters =
- EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iterx,
+fun mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_congL ctor_o_folds =
+ EVERY' [stac dtor_def, rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx,
rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
EVERY' (map (fn thm => rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply]))
- ctor_o_iters),
+ ctor_o_folds),
rtac sym, rtac id_apply] 1;
-fun mk_rec_tac rec_defs iterx fst_recs {context = ctxt, prems = _}=
- unfold_defs_tac ctxt
+fun mk_rec_tac rec_defs foldx fst_recs {context = ctxt, prems = _}=
+ unfold_thms_tac ctxt
(rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd}) fst_recs) THEN
- EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (iterx RS @{thm arg_cong[of _ _ snd]}),
+ EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (foldx RS @{thm arg_cong[of _ _ snd]}),
rtac @{thm snd_convol'}] 1;
fun mk_ctor_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
@@ -570,14 +570,14 @@
CONJ_WRAP' (K atac) ks] 1
end;
-fun mk_map_tac m n iterx map_comp_id map_cong =
- EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac iterx, rtac trans, rtac o_apply,
+fun mk_map_tac m n foldx map_comp_id map_cong =
+ EVERY' [rtac ext, rtac trans, rtac o_apply, rtac trans, rtac foldx, rtac trans, rtac o_apply,
rtac trans, rtac (map_comp_id RS arg_cong), rtac trans, rtac (map_cong RS arg_cong),
REPEAT_DETERM_N m o rtac refl,
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
rtac sym, rtac o_apply] 1;
-fun mk_map_unique_tac m mor_def iter_unique_mor map_comp_ids map_congs =
+fun mk_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_congs =
let
val n = length map_congs;
fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},
@@ -586,13 +586,13 @@
REPEAT_DETERM_N m o rtac refl,
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply]))];
in
- EVERY' [rtac iter_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
+ EVERY' [rtac fold_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_congs,
CONJ_WRAP' mk_mor (map_comp_ids ~~ map_congs)] 1
end;
-fun mk_set_tac iterx = EVERY' [rtac ext, rtac trans, rtac o_apply,
- rtac trans, rtac iterx, rtac sym, rtac o_apply] 1;
+fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
+ rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
fun mk_set_simp_tac set set_natural' set_natural's =
let
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -16,8 +16,8 @@
val subst_asm_tac: Proof.context -> thm list -> int -> tactic
val subst_tac: Proof.context -> thm list -> int -> tactic
val substs_tac: Proof.context -> thm list -> int -> tactic
- val unfold_defs_tac: Proof.context -> thm list -> tactic
- val mk_unfold_defs_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
+ val unfold_thms_tac: Proof.context -> thm list -> tactic
+ val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
@@ -57,11 +57,11 @@
rtac (Drule.instantiate_normalize insts thm) 1
end);
-fun unfold_defs_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
+fun unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
-fun mk_unfold_defs_then_tac lthy defs tac x = unfold_defs_tac lthy defs THEN tac x;
+fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
-(*unlike "unfold_defs_tac", succeeds when the RHS contains schematic variables not in the LHS*)
+(*unlike "unfold_thms_tac", succeeds when the RHS contains schematic variables not in the LHS*)
fun subst_asm_tac ctxt = EqSubst.eqsubst_asm_tac ctxt [0];
fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt [0];
fun substs_tac ctxt = REPEAT_DETERM oo subst_tac ctxt;
@@ -99,13 +99,13 @@
end;
fun simple_rel_O_Gr_tac ctxt =
- unfold_defs_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
+ unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1;
fun mk_pred_simp_tac rel_def IJpred_defs IJrel_defs rel_simp {context = ctxt, prems = _} =
- unfold_defs_tac ctxt IJpred_defs THEN
- subst_tac ctxt [unfold_defs ctxt (IJpred_defs @ IJrel_defs @
+ unfold_thms_tac ctxt IJpred_defs THEN
+ subst_tac ctxt [unfold_thms ctxt (IJpred_defs @ IJrel_defs @
@{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) rel_simp] 1 THEN
- unfold_defs_tac ctxt (rel_def ::
+ unfold_thms_tac ctxt (rel_def ::
@{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
split_conv}) THEN
rtac refl 1;
--- a/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML Fri Sep 21 15:53:29 2012 +0200
@@ -134,8 +134,8 @@
val no_refl: thm list -> thm list
val no_reflexive: thm list -> thm list
- val fold_defs: Proof.context -> thm list -> thm -> thm
- val unfold_defs: Proof.context -> thm list -> thm -> thm
+ val fold_thms: Proof.context -> thm list -> thm -> thm
+ val unfold_thms: Proof.context -> thm list -> thm -> thm
val mk_permute: ''a list -> ''a list -> 'b list -> 'b list
val find_indices: ''a list -> ''a list -> int list
@@ -613,7 +613,7 @@
val no_refl = filter_out is_refl;
val no_reflexive = filter_out Thm.is_reflexive;
-fun fold_defs ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
-fun unfold_defs ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
+fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
+fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
end;
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Fri Sep 21 15:53:29 2012 +0200
@@ -443,7 +443,7 @@
disc_defs';
val not_discI_thms =
map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
- (unfold_defs lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
+ (unfold_thms lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
ms disc_defs';
val (disc_thmss', disc_thmss) =
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Fri Sep 21 15:53:29 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Fri Sep 21 15:53:29 2012 +0200
@@ -42,7 +42,7 @@
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
- hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
+ hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
rtac distinct, rtac uexhaust] @
(([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
|> k = 1 ? swap |> op @)) 1;
@@ -63,7 +63,7 @@
atac
else
REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
- SELECT_GOAL (unfold_defs_tac ctxt sels) THEN' rtac refl)) 1;
+ SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
disc_excludesss' =
@@ -98,7 +98,7 @@
fun mk_case_eq_tac ctxt n uexhaust cases discss' selss =
(rtac uexhaust THEN'
EVERY' (map3 (fn casex => fn if_discs => fn sels =>
- EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_defs_tac ctxt (if_discs @ sels)), rtac casex])
+ EVERY' [hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex])
cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)) 1;
fun mk_case_cong_tac uexhaust cases =
@@ -117,6 +117,6 @@
val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
fun mk_split_asm_tac ctxt split =
- rtac (split RS trans) 1 THEN unfold_defs_tac ctxt split_asm_thms THEN rtac refl 1;
+ rtac (split RS trans) 1 THEN unfold_thms_tac ctxt split_asm_thms THEN rtac refl 1;
end;