--- a/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -32,6 +32,7 @@
val ctor_fold_uniqueN: string
val ctor_foldsN: string
val ctor_mapN: string
+ val ctor_map_uniqueN: string
val ctor_recN: string
val ctor_recsN: string
val ctor_relN: string
@@ -49,6 +50,7 @@
val dtor_ctorN: string
val dtor_exhaustN: string
val dtor_injectN: string
+ val dtor_map_uniqueN: string
val dtor_srelN: string
val dtor_strong_coinductN: string
val dtor_unfoldN: string
@@ -186,6 +188,8 @@
val ctor_mapN = ctorN ^ "_" ^ mapN
val dtor_mapN = dtorN ^ "_" ^ mapN
val map_uniqueN = mapN ^ uniqueN
+val ctor_map_uniqueN = ctorN ^ "_" ^ map_uniqueN
+val dtor_map_uniqueN = dtorN ^ "_" ^ map_uniqueN
val min_algN = "min_alg"
val morN = "mor"
val bisN = "bis"
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -2396,7 +2396,7 @@
|> Thm.close_derivation)
end;
- val map_unique_thm =
+ val dtor_map_unique_thm =
let
fun mk_prem u map dtor dtor' =
mk_Trueprop_eq (HOLogic.mk_comp (dtor', u),
@@ -2408,7 +2408,7 @@
in
Skip_Proof.prove lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (mk_map_unique_tac dtor_unfold_unique_thm map_comps)
+ (mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps)
|> Thm.close_derivation
end;
@@ -2933,7 +2933,7 @@
val ls' = if m = 1 then [0] else ls;
val Jbnf_common_notes =
- [(map_uniqueN, [fold_maps map_unique_thm])] @
+ [(dtor_map_uniqueN, [fold_maps dtor_map_unique_thm])] @
map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_set_induct_thms
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200
@@ -59,7 +59,7 @@
thm list list -> thm list list list -> tactic
val mk_map_id_tac: thm list -> thm -> thm -> tactic
val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
- val mk_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->
thm list -> {prems: 'a, context: Proof.context} -> tactic
@@ -1255,7 +1255,7 @@
rtac conjI, rtac refl, rtac refl]) ks]) 1
end
-fun mk_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
+fun mk_dtor_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
rtac unfold_unique 1 THEN
unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
ALLGOALS (etac sym);
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200
@@ -1409,7 +1409,7 @@
map (fn thm => thm RS @{thm pointfreeE}) maps
end;
- val (map_unique_thms, map_unique_thm) =
+ val (ctor_map_unique_thms, ctor_map_unique_thm) =
let
fun mk_prem u map ctor ctor' =
mk_Trueprop_eq (HOLogic.mk_comp (u, ctor),
@@ -1420,7 +1420,7 @@
(map2 (curry HOLogic.mk_eq) us fs_maps));
val unique = Skip_Proof.prove lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (K (mk_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs))
+ (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_congs))
|> Thm.close_derivation;
in
`split_conj_thm unique
@@ -1659,9 +1659,9 @@
val timer = time (timer "helpers for BNF properties");
- val map_id_tacs = map (K o mk_map_id_tac map_ids) map_unique_thms;
+ val map_id_tacs = map (K o mk_map_id_tac map_ids) ctor_map_unique_thms;
val map_comp_tacs =
- map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) map_unique_thms ks;
+ map2 (K oo mk_map_comp_tac map_comp's ctor_map_thms) ctor_map_unique_thms ks;
val map_cong_tacs = map (mk_map_cong_tac m) map_cong_thms;
val set_nat_tacss = map (map (K o mk_set_natural_tac)) (transpose set_natural_thmss);
val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
@@ -1776,7 +1776,7 @@
val ls' = if m = 1 then [0] else ls
val Ibnf_common_notes =
- [(map_uniqueN, [fold_maps map_unique_thm])]
+ [(ctor_map_uniqueN, [fold_maps ctor_map_unique_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Sun Sep 23 14:52:53 2012 +0200
@@ -42,7 +42,7 @@
val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
val mk_map_id_tac: thm list -> thm -> tactic
val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
- val mk_map_unique_tac: int -> thm -> thm -> thm list -> thm list -> tactic
+ val mk_ctor_map_unique_tac: int -> thm -> thm -> thm list -> thm list -> tactic
val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
@@ -577,7 +577,7 @@
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
rtac sym, rtac o_apply] 1;
-fun mk_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_congs =
+fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_congs =
let
val n = length map_congs;
fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE},