# HG changeset patch # User blanchet # Date 1348247869 -7200 # Node ID b377da40244bc39f116849d2a5904652910673e2 # Parent c473c8749cd17682976591c96dc9cdd612d32a0d renamed LFP low-level rel property to have ctor not dtor in its name diff -r c473c8749cd1 -r b377da40244b src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp.ML Fri Sep 21 19:17:49 2012 +0200 @@ -33,6 +33,8 @@ val ctor_foldsN: string val ctor_recN: string val ctor_recsN: string + val ctor_relN: string + val ctor_srelN: string val disc_unfold_iffN: string val disc_unfoldsN: string val disc_corec_iffN: string @@ -42,9 +44,10 @@ val dtor_relN: string val dtor_corecN: string val dtor_corecsN: string + val dtor_ctorN: string val dtor_exhaustN: string - val dtor_ctorN: string val dtor_injectN: string + val dtor_srelN: string val dtor_strong_coinductN: string val dtor_unfoldN: string val dtor_unfold_uniqueN: string @@ -74,7 +77,6 @@ val set_set_inclN: string val simpsN: string val srel_coinductN: string - val dtor_srelN: string val srel_strong_coinductN: string val strTN: string val str_initN: string @@ -225,7 +227,9 @@ val rel_coinductN = relN ^ "_" ^ coinductN val srel_coinductN = srelN ^ "_" ^ coinductN val simpN = "_simp"; +val ctor_srelN = ctorN ^ "_" ^ srelN val dtor_srelN = dtorN ^ "_" ^ srelN +val ctor_relN = ctorN ^ "_" ^ relN val dtor_relN = dtorN ^ "_" ^ relN val strongN = "strong_" val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN diff -r c473c8749cd1 -r b377da40244b src/HOL/BNF/Tools/bnf_fp_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML Fri Sep 21 19:17:49 2012 +0200 @@ -499,6 +499,9 @@ ((wrap, define_rec_likes), lthy') end; + 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 pre_map_defs = map map_def_of_bnf pre_bnfs; val pre_set_defss = map set_defs_of_bnf pre_bnfs; val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs; @@ -854,7 +857,6 @@ val notes = [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *) - (unfoldsN, unfold_thmss, []), (corecsN, corec_thmss, []), (disc_unfold_iffN, disc_unfold_iff_thmss, simp_attrs), (disc_unfoldsN, disc_unfold_thmss, simp_attrs), @@ -862,7 +864,8 @@ (disc_corecsN, disc_corec_thmss, simp_attrs), (sel_unfoldsN, sel_unfold_thmss, simp_attrs), (sel_corecsN, sel_corec_thmss, simp_attrs), - (simpsN, simp_thmss, [])] + (simpsN, simp_thmss, []), + (unfoldsN, unfold_thmss, [])] |> maps (fn (thmN, thmss, attrs) => map_filter (fn (_, []) => NONE | (b, thms) => SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs), @@ -871,16 +874,19 @@ lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd end; - fun wrap_types_and_define_rec_likes ((wraps, define_rec_likess), lthy) = - fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list8 + fun derive_pred_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _, ctr_defss, unfold_defs, + corec_defs), lthy) = + lthy; val lthy' = lthy |> 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_rec_likes - |> (if lfp then derive_induct_fold_rec_thms_for_types - else derive_coinduct_unfold_corec_thms_for_types); + |> `(if lfp then derive_induct_fold_rec_thms_for_types + else derive_coinduct_unfold_corec_thms_for_types) + |> swap |>> fst + |> derive_pred_thms_for_types; val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^ (if lfp then "" else "co") ^ "datatype")); diff -r c473c8749cd1 -r b377da40244b src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Fri Sep 21 19:17:49 2012 +0200 @@ -2925,7 +2925,7 @@ in map3 (fn goal => fn srel_def => fn dtor_Jsrel => Skip_Proof.prove lthy [] [] goal - (mk_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel) + (mk_ctor_or_dtor_rel_tac srel_def Jrel_defs Jsrel_defs dtor_Jsrel) |> Thm.close_derivation) goals srel_defs dtor_Jsrel_thms end; diff -r c473c8749cd1 -r b377da40244b src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Fri Sep 21 19:17:49 2012 +0200 @@ -1742,7 +1742,7 @@ val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss; val folded_set_simp_thmss' = transpose folded_set_simp_thmss; - val dtor_Isrel_thms = + val ctor_Isrel_thms = let fun mk_goal xF yF ctor ctor' IsrelR srelR = fold_rev Logic.all (xF :: yF :: IRs) (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (ctor $ xF, ctor' $ yF), IsrelR), @@ -1753,24 +1753,24 @@ fn map_simp => fn set_simps => fn ctor_inject => fn ctor_dtor => fn set_naturals => fn set_incls => fn set_set_inclss => Skip_Proof.prove lthy [] [] goal - (K (mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps + (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject ctor_dtor set_naturals set_incls set_set_inclss)) |> Thm.close_derivation) ks goals in_srels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss' ctor_inject_thms ctor_dtor_thms set_natural'ss set_incl_thmss set_set_incl_thmsss end; - val dtor_Irel_thms = + val ctor_Irel_thms = let fun mk_goal xF yF ctor ctor' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis) (mk_Trueprop_eq (Ipredphi $ (ctor $ xF) $ (ctor' $ yF), predphi $ xF $ yF)); val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis; in - map3 (fn goal => fn srel_def => fn dtor_Isrel => + map3 (fn goal => fn srel_def => fn ctor_Isrel => Skip_Proof.prove lthy [] [] goal - (mk_dtor_rel_tac srel_def Irel_defs Isrel_defs dtor_Isrel) + (mk_ctor_or_dtor_rel_tac srel_def Irel_defs Isrel_defs ctor_Isrel) |> Thm.close_derivation) - goals srel_defs dtor_Isrel_thms + goals srel_defs ctor_Isrel_thms end; val timer = time (timer "additional properties"); @@ -1783,8 +1783,8 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val Ibnf_notes = - [(dtor_relN, map single dtor_Irel_thms), - (dtor_srelN, map single dtor_Isrel_thms), + [(ctor_relN, map single ctor_Irel_thms), + (ctor_srelN, map single ctor_Isrel_thms), (map_simpsN, map single folded_map_simp_thms), (set_inclN, set_incl_thmss), (set_set_inclN, map flat set_set_incl_thmsss)] @ diff -r c473c8749cd1 -r b377da40244b src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Fri Sep 21 19:17:49 2012 +0200 @@ -22,9 +22,9 @@ thm list -> tactic val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic + val mk_ctor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> + thm list -> thm list -> thm list list -> tactic val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic - val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> - thm list -> thm list -> thm list list -> tactic val mk_ex_copy_alg_tac: int -> thm -> thm -> tactic val mk_in_bd_tac: thm -> thm -> thm -> thm -> tactic val mk_incl_min_alg_tac: (int -> tactic) -> thm list list list -> thm list -> thm -> @@ -770,7 +770,7 @@ EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp, REPEAT_DETERM_N n o etac UnE]))))] 1); -fun mk_dtor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject +fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong map_simp set_simps ctor_inject ctor_dtor set_naturals set_incls set_set_inclss = let val m = length set_incls; diff -r c473c8749cd1 -r b377da40244b src/HOL/BNF/Tools/bnf_tactics.ML --- a/src/HOL/BNF/Tools/bnf_tactics.ML Fri Sep 21 18:25:17 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML Fri Sep 21 19:17:49 2012 +0200 @@ -27,8 +27,8 @@ val mk_Abs_inj_thm: thm -> thm val simple_srel_O_Gr_tac: Proof.context -> tactic - val mk_dtor_rel_tac: thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> - tactic + val mk_ctor_or_dtor_rel_tac: + thm -> thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic val mk_map_comp_id_tac: thm -> tactic val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic @@ -101,7 +101,7 @@ fun simple_srel_O_Gr_tac ctxt = unfold_thms_tac ctxt @{thms Collect_fst_snd_mem_eq Collect_pair_mem_eq} THEN rtac refl 1; -fun mk_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} = +fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} = unfold_thms_tac ctxt IJrel_defs THEN subst_tac ctxt [unfold_thms ctxt (IJrel_defs @ IJsrel_defs @ @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel] 1 THEN