--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 30 10:50:28 2014 +0200
@@ -103,6 +103,7 @@
val sel_mapN = "sel_map";
val sel_setN = "sel_set";
val set_emptyN = "set_empty";
+val set_inductN = "set_induct";
structure Data = Generic_Data
(
@@ -112,10 +113,16 @@
fun merge data : T = Symtab.merge (K true) data;
);
-fun choose_relator Rs AB = find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) Rs;
-fun build_the_rel ctxt Rs Ts A B = build_rel ctxt Ts (the o choose_relator Rs) (A, B);
+fun choose_binary_fun fs AB =
+ find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs;
+fun build_binary_fun_app fs a b =
+ Option.map (rapp b o rapp a) (choose_binary_fun fs (fastype_of a, fastype_of b));
+
+fun build_the_rel ctxt Rs Ts A B = build_rel ctxt Ts (the o choose_binary_fun Rs) (A, B);
fun build_rel_app ctxt Rs Ts a b = build_the_rel ctxt Rs Ts (fastype_of a) (fastype_of b) $ a $ b;
+val name_of_set = name_of_const "set";
+
fun fp_sugar_of ctxt =
Symtab.lookup (Data.get (Context.Proof ctxt))
#> Option.map (transfer_fp_sugar ctxt);
@@ -759,6 +766,98 @@
mk_coinduct_attributes fpA_Ts (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss)
end;
+fun derive_set_induct_thms_for_types lthy nn fpTs ctrss setss dtor_set_inducts exhausts
+ set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses =
+ let
+ fun mk_prems A Ps ctr_args t ctxt =
+ (case fastype_of t of
+ Type (type_name, xs) =>
+ (case bnf_of ctxt type_name of
+ NONE => ([], ctxt)
+ | SOME bnf =>
+ let
+ fun seq_assm a set ctxt =
+ let
+ val X = HOLogic.dest_setT (range_type (fastype_of set));
+ val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt;
+ val assm = mk_Trueprop_mem (x, set $ a);
+ in
+ (case build_binary_fun_app Ps x a of
+ NONE =>
+ mk_prems A Ps ctr_args x ctxt'
+ |>> map (Logic.all x o Logic.mk_implies o pair assm)
+ | SOME f =>
+ ([Logic.all x
+ (Logic.mk_implies (assm,
+ Logic.mk_implies (HOLogic.mk_Trueprop f,
+ HOLogic.mk_Trueprop (the (build_binary_fun_app Ps x ctr_args)))))],
+ ctxt'))
+ end;
+ in
+ fold_map (seq_assm t o mk_set xs) (sets_of_bnf bnf) ctxt
+ |>> flat
+ end)
+ | T =>
+ if T = A then ([HOLogic.mk_Trueprop (the (build_binary_fun_app Ps t ctr_args))], ctxt)
+ else ([], ctxt));
+
+ fun mk_prems_for_ctr A Ps ctr ctxt =
+ let
+ val (args, ctxt') = mk_Frees "arg" (binder_types (fastype_of ctr)) ctxt;
+ in
+ fold_map (mk_prems A Ps (list_comb (ctr, args))) args ctxt'
+ |>> map (fold_rev Logic.all args) o flat
+ |>> (fn prems => (prems, mk_names (length prems) (name_of_ctr ctr)))
+ end;
+
+ fun mk_prems_and_concl_for_type A Ps ((fpT, ctrs), set) ctxt =
+ let
+ val ((x, fp), ctxt') = ctxt
+ |> yield_singleton (mk_Frees "x") A
+ ||>> yield_singleton (mk_Frees "a") fpT;
+ val concl = mk_Ball (set $ fp) (Term.absfree (dest_Free x)
+ (the (build_binary_fun_app Ps x fp)));
+ in
+ fold_map (mk_prems_for_ctr A Ps) ctrs ctxt'
+ |>> split_list
+ |>> map_prod flat flat
+ |>> apfst (rpair concl)
+ end;
+
+ fun mk_thm ctxt fpTs ctrss sets =
+ let
+ val A = HOLogic.dest_setT (range_type (fastype_of (hd sets)));
+ val (Ps, ctxt') = mk_Frees "P" (map (fn fpT => A --> fpT --> HOLogic.boolT) fpTs) ctxt;
+ val (((premises, conclusion), case_names), ctxt'') =
+ (fold_map (mk_prems_and_concl_for_type A Ps) (fpTs ~~ ctrss ~~ sets) ctxt')
+ |>> apfst split_list o split_list
+ |>> apfst (apfst flat)
+ |>> apfst (apsnd (Library.foldr1 HOLogic.mk_conj))
+ |>> apsnd flat;
+
+ val thm = Goal.prove_sorry lthy [] premises (HOLogic.mk_Trueprop conclusion)
+ (fn {context = ctxt, prems = prems} =>
+ mk_set_induct0_tac ctxt (map (certify ctxt'') Ps) prems dtor_set_inducts exhausts
+ set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
+ |> singleton (Proof_Context.export ctxt'' ctxt)
+ |> Thm.close_derivation;
+
+ val case_names_attr =
+ Attrib.internal (K (Rule_Cases.case_names (quasi_unambiguous_case_names case_names)));
+ val induct_set_attrs = map (Attrib.internal o K o Induct.induct_pred o name_of_set) sets;
+ in
+ (thm, case_names_attr :: induct_set_attrs)
+ end
+ val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
+ in
+ map (fn Asets =>
+ let
+ fun massage_thm thm = rotate_prems (~1) (thm RS bspec);
+ in
+ mk_thm lthy fpTs ctrss Asets |> nn = 1 ? map_prod massage_thm (cons consumes_attr)
+ end) (transpose setss)
+ end;
+
fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
@@ -1072,7 +1171,7 @@
val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
- xtor_co_rec_thms, rel_xtor_co_induct_thm, ...},
+ xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms, ...},
lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
(map dest_TFree killed_As) fp_eqs no_defs_lthy0
@@ -1143,8 +1242,8 @@
fun massage_simple_notes base =
filter_out (null o #2)
- #> map (fn (thmN, thms, attrs) =>
- ((Binding.qualify true base (Binding.name thmN), attrs), [(thms, [])]));
+ #> map (fn (thmN, thms, f_attrs) =>
+ ((Binding.qualify true base (Binding.name thmN), []), map_index (fn (i, thm) => ([thm], f_attrs i)) thms));
val massage_multi_notes =
maps (fn (thmN, thmss, attrs) =>
@@ -1611,17 +1710,17 @@
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val notes =
- [(disc_map_iffN, disc_map_iff_thms, simp_attrs),
- (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
- (rel_casesN, [rel_cases_thm], rel_cases_attrs),
- (rel_distinctN, rel_distinct_thms, simp_attrs),
- (rel_injectN, rel_inject_thms, simp_attrs),
- (rel_introsN, rel_intro_thms, []),
- (rel_selN, rel_sel_thms, []),
- (setN, set_thms, code_nitpicksimp_attrs @ simp_attrs),
- (sel_mapN, sel_map_thms, []),
- (sel_setN, sel_set_thms, []),
- (set_emptyN, set_empty_thms, [])]
+ [(disc_map_iffN, disc_map_iff_thms, K simp_attrs),
+ (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
+ (rel_casesN, [rel_cases_thm], K rel_cases_attrs),
+ (rel_distinctN, rel_distinct_thms, K simp_attrs),
+ (rel_injectN, rel_inject_thms, K simp_attrs),
+ (rel_introsN, rel_intro_thms, K []),
+ (rel_selN, rel_sel_thms, K []),
+ (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
+ (sel_mapN, sel_map_thms, K []),
+ (sel_setN, sel_set_thms, K []),
+ (set_emptyN, set_empty_thms, K [])]
|> massage_simple_notes fp_b_name;
val (noted, lthy') =
@@ -1692,8 +1791,8 @@
val common_notes =
(if nn > 1 then
- [(inductN, [induct_thm], induct_attrs),
- (rel_inductN, common_rel_induct_thms, common_rel_induct_attrs)]
+ [(inductN, [induct_thm], K induct_attrs),
+ (rel_inductN, common_rel_induct_thms, K common_rel_induct_attrs)]
else
[])
|> massage_simple_notes fp_common_name;
@@ -1765,17 +1864,25 @@
(rel_coinduct_attrs, common_rel_coinduct_attrs))
end;
+ val (set_induct_thms, set_induct_attrss) =
+ derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars)
+ (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_induct_thms
+ (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss)
+ dtor_ctors abs_inverses
+ |> split_list;
+
val simp_thmss =
map6 mk_simp_thms ctr_sugars
(map3 flat_corec_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss)
mapss rel_injectss rel_distinctss setss;
val common_notes =
+ (set_inductN, set_induct_thms, nth set_induct_attrss) ::
(if nn > 1 then
- [(coinductN, [coinduct_thm], common_coinduct_attrs),
- (rel_coinductN, common_rel_coinduct_thms, common_rel_coinduct_attrs),
- (strong_coinductN, [strong_coinduct_thm], common_coinduct_attrs)]
- else [])
+ [(coinductN, [coinduct_thm], K common_coinduct_attrs),
+ (rel_coinductN, common_rel_coinduct_thms, K common_rel_coinduct_attrs),
+ (strong_coinductN, [strong_coinduct_thm], K common_coinduct_attrs)]
+ else [])
|> massage_simple_notes fp_common_name;
val notes =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Jul 30 10:50:28 2014 +0200
@@ -39,6 +39,8 @@
val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
+ val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list ->
+ thm list -> thm list -> thm list -> thm list -> tactic
end;
structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
@@ -257,7 +259,7 @@
HEADGOAL (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
(rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN
- unfold_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
+ unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
@{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
TRYALL (hyp_subst_tac ctxt) THEN
unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
@@ -306,4 +308,28 @@
SOME (thm RS eqFalseI) handle THM _ => NONE) discs) THEN
ALLGOALS (rtac refl ORELSE' etac FalseE);
+fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors
+ Abs_pre_inverses =
+ let
+ val assms_ctor_defs =
+ map (unfold_thms ctxt (@{thm BNF_Comp.id_bnf_comp_def} :: ctor_defs)) assms;
+ val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
+ |> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts;
+ in
+ ALLGOALS (resolve_tac dtor_set_inducts) THEN
+ TRYALL (resolve_tac exhausts' THEN_ALL_NEW
+ (resolve_tac (map (fn ct => refl RS
+ cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
+ THEN' atac THEN' hyp_subst_tac ctxt)) THEN
+ unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
+ @{thms BNF_Comp.id_bnf_comp_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert
+ Un_empty_left Un_empty_right empty_iff singleton_iff}) THEN
+ REPEAT_DETERM (HEADGOAL
+ (TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN'
+ REPEAT_DETERM o eresolve_tac @{thms UN_E UnE singletonE} THEN'
+ fold (curry (op ORELSE')) (map (fn thm =>
+ funpow (length (prems_of thm)) (fn tac => tac THEN' atac) (rtac thm)) assms_ctor_defs)
+ (etac FalseE)))
+ end;
+
end;
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Jul 30 10:50:28 2014 +0200
@@ -463,7 +463,8 @@
xtor_rel_thms = of_fp_res #xtor_rel_thms (*too general types and terms*),
xtor_co_rec_thms = xtor_co_rec_thms,
xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
- rel_xtor_co_induct_thm = rel_xtor_co_induct_thm}
+ rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
+ dtor_set_induct_thms = []}
|> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
in
(fp_res, lthy)
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Jul 30 10:50:28 2014 +0200
@@ -25,7 +25,8 @@
xtor_rel_thms: thm list,
xtor_co_rec_thms: thm list,
xtor_co_rec_o_map_thms: thm list,
- rel_xtor_co_induct_thm: thm}
+ rel_xtor_co_induct_thm: thm,
+ dtor_set_induct_thms: thm list}
val morph_fp_result: morphism -> fp_result -> fp_result
@@ -237,11 +238,12 @@
xtor_rel_thms: thm list,
xtor_co_rec_thms: thm list,
xtor_co_rec_o_map_thms: thm list,
- rel_xtor_co_induct_thm: thm};
+ rel_xtor_co_induct_thm: thm,
+ dtor_set_induct_thms: thm list};
fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
- xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm} =
+ xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms} =
{Ts = map (Morphism.typ phi) Ts,
bnfs = map (morph_bnf phi) bnfs,
ctors = map (Morphism.term phi) ctors,
@@ -257,7 +259,8 @@
xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
- rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
+ rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
+ dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *)
type fp_sugar =
{T: typ,
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Jul 30 10:50:28 2014 +0200
@@ -1659,12 +1659,12 @@
(*register new codatatypes as BNFs*)
val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jset_thmss',
- dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, lthy) =
+ dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, dtor_Jset_induct_thms, lthy) =
if m = 0 then
(timer, replicate n DEADID_bnf,
map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids),
replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs,
- mk_Jrel_DEADID_coinduct_thm (), [], lthy)
+ mk_Jrel_DEADID_coinduct_thm (), [], [], lthy)
else let
val fTs = map2 (curry op -->) passiveAs passiveBs;
val gTs = map2 (curry op -->) passiveBs passiveCs;
@@ -2464,7 +2464,8 @@
bs thmss)
in
(timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jset_thmss',
- dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, lthy)
+ dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, dtor_Jset_induct_thms,
+ lthy)
end;
val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m
@@ -2526,7 +2527,8 @@
ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
- xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm}
+ xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
+ dtor_set_induct_thms = dtor_Jset_induct_thms}
|> morph_fp_result (substitute_noted_thm noted);
in
timer; (fp_res, lthy')
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Jul 30 10:50:28 2014 +0200
@@ -1814,7 +1814,8 @@
ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
- xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm}
+ xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
+ dtor_set_induct_thms = []}
|> morph_fp_result (substitute_noted_thm noted);
in
timer; (fp_res, lthy')
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Wed Jul 30 10:50:28 2014 +0200
@@ -255,12 +255,6 @@
fun mk_disc_or_sel Ts t =
subst_nonatomic_types (snd (Term.dest_Type (domain_type (fastype_of t))) ~~ Ts) t;
-fun name_of_const what t =
- (case head_of t of
- Const (s, _) => s
- | Free (s, _) => s
- | _ => error ("Cannot extract name of " ^ what));
-
val name_of_ctr = name_of_const "constructor";
fun name_of_disc t =
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Wed Jul 30 00:50:41 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Wed Jul 30 10:50:28 2014 +0200
@@ -39,6 +39,8 @@
(string * sort) list * Proof.context
val variant_tfrees: string list -> Proof.context -> typ list * Proof.context
+ val name_of_const: string -> term -> string
+
val typ_subst_nonatomic: (typ * typ) list -> typ -> typ
val subst_nonatomic_types: (typ * typ) list -> term -> term
@@ -177,6 +179,12 @@
apfst (map TFree) o
variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type});
+fun name_of_const what t =
+ (case head_of t of
+ Const (s, _) => s
+ | Free (s, _) => s
+ | _ => error ("Cannot extract name of " ^ what));
+
(*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
fun typ_subst_nonatomic [] = I
| typ_subst_nonatomic inst =