more uniform treatment of codatatype vs. datatype map and rel theorem generation (towards nonuniform codatatypes)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Oct 27 12:54:55 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Oct 27 14:14:48 2016 +0200
@@ -742,7 +742,7 @@
let
val argA_Ts = binder_types (fastype_of ctrA);
val argB_Ts = binder_types (fastype_of ctrB);
- val ((argAs, argBs), names_ctxt) = ctxt
+ val ((argAs, argBs), names_ctxt) = ctxt
|> mk_Frees "x" argA_Ts
||>> mk_Frees "y" argB_Ts;
val ctrA_args = list_comb (ctrA, argAs);
@@ -810,6 +810,32 @@
val selAss = map (map (mk_disc_or_sel As)) selss;
val selBss = map (map (mk_disc_or_sel Bs)) selss;
+ val map_ctor_thm =
+ if fp = Least_FP then
+ fp_map_thm
+ else
+ let
+ val ctorA = mk_ctor As ctor;
+ val ctorB = mk_ctor Bs ctor;
+ val ctor_cong =
+ infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctorB)] arg_cong;
+
+ val y_T = domain_type (fastype_of ctorA);
+ val (y as Free (y_s, _), _) = lthy
+ |> yield_singleton (mk_Frees "y") y_T;
+
+ val ctor_cong =
+ infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctorB)] arg_cong;
+ val fp_map_thm' = fp_map_thm
+ |> infer_instantiate' lthy (replicate live NONE @
+ [SOME (Thm.cterm_of lthy (ctorA $ y))])
+ |> unfold_thms lthy [dtor_ctor];
+
+ val map_ctor_thm0 = fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans);
+ in
+ Thm.generalize ([], [y_s]) (Thm.maxidx_of map_ctor_thm0 + 1) map_ctor_thm0
+ end;
+
val map_thms =
let
fun mk_goal ctrA ctrB xs ys =
@@ -828,22 +854,10 @@
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 [];
-
- val fp_map_thm' =
- if fp = Least_FP then
- fp_map_thm
- else
- let
- val ctor' = mk_ctor Bs ctor;
- val ctor_cong =
- infer_instantiate' lthy [NONE, NONE, SOME (Thm.cterm_of lthy ctor')] arg_cong;
- in
- fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans)
- end;
in
Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
- mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map_thm'
- live_nesting_map_id0s ctr_defs' extra_unfolds_map)
+ mk_map_tac ctxt abs_inverses pre_map_def map_ctor_thm live_nesting_map_id0s ctr_defs'
+ extra_unfolds_map)
|> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
end;
@@ -880,6 +894,28 @@
val set_thms = set0_thms
|> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left Un_insert_left});
+ val rel_ctor_thm =
+ if fp = Least_FP then
+ fp_rel_thm
+ else
+ let
+ val ctorA = mk_ctor As ctor;
+ val ctorB = mk_ctor Bs ctor;
+
+ val y_T = domain_type (fastype_of ctorA);
+ val z_T = domain_type (fastype_of ctorB);
+ val ((y as Free (y_s, _), z as Free (z_s, _)), _) = lthy
+ |> yield_singleton (mk_Frees "y") y_T
+ ||>> yield_singleton (mk_Frees "z") z_T;
+
+ val rel_ctor_thm0 = fp_rel_thm
+ |> infer_instantiate' lthy (replicate live NONE @
+ [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
+ |> unfold_thms lthy [dtor_ctor];
+ in
+ Thm.generalize ([], [y_s, z_s]) (Thm.maxidx_of rel_ctor_thm0 + 1) rel_ctor_thm0
+ end;
+
val rel_inject_thms =
let
fun mk_goal ctrA ctrB xs ys =
@@ -897,8 +933,8 @@
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 live_nesting_rel_eqs
- ctr_defs' extra_unfolds_rel)
+ mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor_thm live_nesting_rel_eqs ctr_defs'
+ extra_unfolds_rel)
|> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
end;
@@ -923,8 +959,8 @@
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
- live_nesting_rel_eqs ctr_defs' extra_unfolds_rel)
+ mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor_thm live_nesting_rel_eqs
+ ctr_defs' extra_unfolds_rel)
|> Thm.close_derivation
|> Conjunction.elim_balanced (length goals)
end)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Oct 27 12:54:55 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Oct 27 14:14:48 2016 +0200
@@ -30,8 +30,8 @@
val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
- val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list ->
- thm list -> tactic
+ val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm list -> thm list -> thm list ->
+ tactic
val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list ->
thm list -> tactic
@@ -39,8 +39,8 @@
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 -> thm list ->
- thm list -> tactic
+ val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm list -> thm list -> 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 ->
@@ -392,11 +392,11 @@
(1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
selsss));
-fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' live_nesting_map_id0s ctr_defs'
+fun mk_map_tac ctxt abs_inverses pre_map_def map_ctor live_nesting_map_id0s ctr_defs'
extra_unfolds =
TRYALL Goal.conjunction_tac THEN
- unfold_thms_tac ctxt (pre_map_def :: dtor_ctor :: fp_map' :: abs_inverses @
- live_nesting_map_id0s @ ctr_defs' @ extra_unfolds @ sumprod_thms_map @
+ unfold_thms_tac ctxt (pre_map_def :: map_ctor :: abs_inverses @ live_nesting_map_id0s @
+ ctr_defs' @ extra_unfolds @ sumprod_thms_map @
@{thms o_apply id_apply id_o o_id}) THEN
ALLGOALS (rtac ctxt refl);
@@ -419,11 +419,10 @@
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 live_nesting_rel_eqs ctr_defs'
- extra_unfolds =
+fun mk_rel_tac ctxt abs_inverses pre_rel_def rel_ctor live_nesting_rel_eqs ctr_defs' extra_unfolds =
TRYALL Goal.conjunction_tac THEN
- unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ live_nesting_rel_eqs @
- ctr_defs' @ extra_unfolds @ sumprod_thms_rel @ @{thms vimage2p_def o_apply sum.inject
+ unfold_thms_tac ctxt (pre_rel_def :: rel_ctor :: abs_inverses @ live_nesting_rel_eqs @ ctr_defs' @
+ extra_unfolds @ sumprod_thms_rel @ @{thms vimage2p_def o_apply sum.inject
sum.distinct(1)[THEN eq_False[THEN iffD2]] not_False_eq_True}) THEN
ALLGOALS (resolve_tac ctxt [TrueI, refl]);