--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 11 13:35:27 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Sep 11 13:35:27 2016 +0200
@@ -830,7 +830,6 @@
end;
val cxIns = map2 (mk_cIn ctor) ks xss;
- val cyIns = map2 (mk_cIn (B_ify ctor)) ks yss;
fun mk_set0_thm fp_set_thm ctr_def' cxIn =
Local_Defs.fold lthy [ctr_def']
@@ -877,42 +876,76 @@
|> Conjunction.elim_balanced (length goals)
end;
- fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
- Local_Defs.fold lthy ctr_defs'
- (unfold_thms lthy (pre_rel_def :: abs_inverses @
- (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
- @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
- (infer_instantiate' lthy (map (SOME o Thm.cterm_of lthy) Rs @ [SOME cxIn, SOME cyIn])
- fp_rel_thm))
- |> postproc
- |> singleton (Proof_Context.export names_lthy lthy);
-
- fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
- mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
-
- fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
- mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
- cxIn cyIn;
-
- fun mk_rel_intro_thm m thm =
- uncurry_thm m (thm RS iffD2) handle THM _ => thm;
+ val rel_inject_thms =
+ let
+ fun mk_goal ctrA ctrB xs ys =
+ let
+ val rel = mk_rel live As Bs (rel_of_bnf fp_bnf);
+ val Rrel = list_comb (rel, Rs);
+
+ val lhs = Rrel $ list_comb (ctrA, xs) $ list_comb (ctrB, ys);
+ val conjuncts = map2 (build_rel_app lthy Rs []) xs ys;
+ in
+ HOLogic.mk_Trueprop
+ (if null conjuncts then lhs
+ else HOLogic.mk_eq (lhs, Library.foldr1 HOLogic.mk_conj conjuncts))
+ end;
+
+ val goals = @{map 4} mk_goal ctrAs ctrBs xss yss;
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
+ mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm ctr_defs')
+ |> Thm.close_derivation
+ |> Conjunction.elim_balanced (length goals)
+ end;
+
+ val half_rel_distinct_thmss =
+ let
+ fun mk_goal ((ctrA, xs), (ctrB, ys)) =
+ let
+ val rel = mk_rel live As Bs (rel_of_bnf fp_bnf);
+ val Rrel = list_comb (rel, Rs);
+ in
+ HOLogic.mk_Trueprop (HOLogic.mk_not
+ (Rrel $ list_comb (ctrA, xs) $ list_comb (ctrB, ys)))
+ end;
+
+ val rel_infos = (ctrAs ~~ xss, ctrBs ~~ yss);
+
+ val goalss = map (map mk_goal) (mk_half_pairss rel_infos);
+ val goals = flat goalss;
+ in
+ unflat goalss
+ (if null goals then []
+ else
+ let
+ val goal = Logic.mk_conjunction_balanced goals;
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
+ mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm ctr_defs')
+ |> Thm.close_derivation
+ |> Conjunction.elim_balanced (length goals)
+ end)
+ end;
val rel_flip = rel_flip_of_bnf fp_bnf;
fun mk_other_half_rel_distinct_thm thm =
flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
- val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
-
- val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
- val rel_intro_thms = map2 mk_rel_intro_thm ms rel_inject_thms;
-
- val half_rel_distinct_thmss = map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
val other_half_rel_distinct_thmss =
map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss;
val (rel_distinct_thms, _) =
join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
+ fun mk_rel_intro_thm m thm =
+ uncurry_thm m (thm RS iffD2) handle THM _ => thm;
+
+ val rel_intro_thms = map2 mk_rel_intro_thm ms rel_inject_thms;
+
val rel_code_thms =
map (fn thm => thm RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @
map2 (fn thm => fn 0 => thm RS @{thm eq_True[THEN iffD2]} | _ => thm) rel_inject_thms ms;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 13:35:27 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sun Sep 11 13:35:27 2016 +0200
@@ -10,7 +10,6 @@
sig
val sumprod_thms_set: thm list
val basic_sumprod_thms_set: thm list
- val sumprod_thms_rel: thm list
val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic
val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
@@ -40,6 +39,7 @@
tactic
val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list ->
term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic
+ val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
thm list -> thm list -> tactic
val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
@@ -75,11 +75,11 @@
val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)};
val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
+val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc};
val basic_sumprod_thms_set =
@{thms UN_empty UN_insert UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib
o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set;
-val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc};
fun is_def_looping def =
(case Thm.prop_of def of
@@ -406,13 +406,20 @@
fun mk_map_sel_tac ctxt ct exhaust discs maps sels map_id0s =
TRYALL Goal.conjunction_tac THEN
- ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
- REPEAT_DETERM o hyp_subst_tac ctxt) THEN
- unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
- @{thms not_True_eq_False not_False_eq_True}) THEN
- TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN
- unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN
- ALLGOALS (rtac ctxt refl);
+ ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
+ REPEAT_DETERM o hyp_subst_tac ctxt) THEN
+ unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
+ @{thms not_True_eq_False not_False_eq_True}) THEN
+ TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN
+ unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN
+ ALLGOALS (rtac ctxt refl);
+
+fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel ctr_defs' =
+ TRYALL Goal.conjunction_tac THEN
+ unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ ctr_defs' @ o_apply ::
+ sumprod_thms_rel @ @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]
+ not_False_eq_True}) THEN
+ ALLGOALS (resolve_tac ctxt [TrueI, refl]);
fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs =
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW
@@ -483,16 +490,16 @@
fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
TRYALL Goal.conjunction_tac THEN
- ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
- REPEAT_DETERM o hyp_subst_tac ctxt) THEN
- unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
- @{thms not_True_eq_False not_False_eq_True}) THEN
- TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN
- unfold_thms_tac ctxt (sels @ sets) THEN
- ALLGOALS (REPEAT o (resolve_tac ctxt @{thms UnI1 UnI2 imageI} ORELSE'
- eresolve_tac ctxt @{thms UN_I UN_I[rotated] imageE} ORELSE'
- hyp_subst_tac ctxt) THEN'
- (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt));
+ ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW
+ REPEAT_DETERM o hyp_subst_tac ctxt) THEN
+ unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @
+ @{thms not_True_eq_False not_False_eq_True}) THEN
+ TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN
+ unfold_thms_tac ctxt (sels @ sets) THEN
+ ALLGOALS (REPEAT o (resolve_tac ctxt @{thms UnI1 UnI2 imageI} ORELSE'
+ eresolve_tac ctxt @{thms UN_I UN_I[rotated] imageE} ORELSE'
+ hyp_subst_tac ctxt) THEN'
+ (rtac ctxt @{thm singletonI} ORELSE' assume_tac ctxt));
fun mk_set_cases_tac ctxt ct assms exhaust sets =
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust)