# HG changeset patch # User blanchet # Date 1348235609 -7200 # Node ID df9b897fb254fac17f0178f941ce24a1bbb3ba36 # Parent dbbde075a42e4a0f00c0ec689d58c7f60708af07 renamed "iter"/"coiter" to "fold"/"unfold" (cf. Wadler) diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_comp.ML --- 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); diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_comp_tactics.ML --- 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)); diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_def.ML --- 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; diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_def_tactics.ML --- 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, diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_fp.ML --- 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 "_"; diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML --- 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")); diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML --- 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; diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_gfp.ML --- 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; diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML --- 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]) diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_lfp.ML --- 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; diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML --- 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 diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_tactics.ML --- 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; diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_util.ML --- 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; diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_wrap.ML --- 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) = diff -r dbbde075a42e -r df9b897fb254 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML --- 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;