--- 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
--- 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"));
--- 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;
--- 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)] @
--- 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;
--- 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