--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon May 19 09:35:35 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu May 15 16:15:44 2014 +0200
@@ -98,6 +98,7 @@
val EqN = "Eq_";
val set_emptyN = "set_empty";
+val disc_map_iffN = "disc_map_iff";
structure Data = Generic_Data
(
@@ -1176,6 +1177,48 @@
end;
val sets = map mk_set (sets_of_bnf fp_bnf);
+
+ val disc_map_iff_thms =
+ let
+ val (((Ds, As), Bs), names_lthy) = lthy
+ |> mk_TFrees (dead_of_bnf fp_bnf)
+ ||>> mk_TFrees (live_of_bnf fp_bnf)
+ ||>> mk_TFrees (live_of_bnf fp_bnf);
+ val fTs = map2 (curry op -->) As Bs;
+ val T1 = mk_T_of_bnf Ds As fp_bnf;
+ val T2 = mk_T_of_bnf Ds Bs fp_bnf;
+ val ((fs, t), names_lthy) = names_lthy
+ |> mk_Frees "f" fTs
+ ||>> yield_singleton (mk_Frees "a") T1;
+ val map_term = mk_map_of_bnf Ds As Bs fp_bnf;
+ fun mk_discs T = map (fn disc =>
+ subst_nonatomic_types [(domain_type (fastype_of disc), T)] disc);
+ val discs1 = mk_discs T1 discs;
+ val discs2 = mk_discs T2 discs;
+ val discs1_t = map (fn disc1 => Term.betapply (disc1, t)) discs1;
+ fun mk_goal (disc1_t, disc2) =
+ let
+ val (head, tail) = Term.strip_comb disc1_t;
+ val is_t_eq_t = head aconv HOLogic.eq_const T1 andalso
+ forall (fn u => u = t) tail;
+ in
+ if head aconv @{const Not} orelse is_t_eq_t then NONE
+ else
+ SOME (mk_Trueprop_eq
+ (betapply (disc2, (Term.list_comb (map_term, fs) $ t)), disc1_t))
+ end;
+ val goals = map_filter mk_goal (discs1_t ~~ discs2);
+ in
+ if null goals then []
+ else
+ Goal.prove_sorry names_lthy [] [] (Logic.mk_conjunction_balanced goals)
+ (fn {context = ctxt, prems = _} =>
+ mk_disc_map_iff_tac ctxt (certify ctxt t) exhaust (flat disc_thmss)
+ map_thms)
+ |> Conjunction.elim_balanced (length goals)
+ |> Proof_Context.export names_lthy lthy
+ end;
+
val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
binder_types o fastype_of) ctrs;
val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
@@ -1238,7 +1281,8 @@
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val notes =
- [(mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
+ [(disc_map_iffN, disc_map_iff_thms, simp_attrs),
+ (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
(rel_distinctN, rel_distinct_thms, simp_attrs),
(rel_injectN, rel_inject_thms, simp_attrs),
(setN, set_thms, code_nitpicksimp_attrs @ simp_attrs),
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon May 19 09:35:35 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu May 15 16:15:44 2014 +0200
@@ -18,6 +18,7 @@
val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+ val mk_disc_map_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
@@ -31,6 +32,7 @@
structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
struct
+open Ctr_Sugar_Util
open BNF_Tactics
open BNF_Util
open BNF_FP_Util
@@ -113,6 +115,15 @@
(if is_refl disc then all_tac else HEADGOAL (rtac disc)))
(map rtac case_splits' @ [K all_tac]) corecs discs);
+fun mk_disc_map_iff_tac ctxt ct exhaust discs maps =
+ TRYALL Goal.conjunction_tac THEN
+ ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+ REPEAT_DETERM o hyp_subst_tac ctxt) THEN
+ unfold_thms_tac ctxt maps THEN
+ unfold_thms_tac ctxt (map (fn thm => thm RS @{thm iffD2[OF eq_False]}
+ handle THM _ => thm RS @{thm iffD2[OF eq_True]}) discs) THEN
+ ALLGOALS (rtac refl ORELSE' rtac TrueI);
+
fun solve_prem_prem_tac ctxt =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
@@ -194,10 +205,10 @@
fun mk_set_empty_tac ctxt ct exhaust sets discs =
TRYALL Goal.conjunction_tac THEN
- ALLGOALS(rtac (Ctr_Sugar_Util.cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+ ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
REPEAT_DETERM o hyp_subst_tac ctxt) THEN
unfold_thms_tac ctxt (sets @ map_filter (fn thm =>
SOME (thm RS @{thm iffD2[OF eq_False]}) handle THM _ => NONE) discs) THEN
- ALLGOALS(rtac refl ORELSE' etac FalseE);
+ ALLGOALS (rtac refl ORELSE' etac FalseE);
end;