--- a/src/HOL/BNF/Tools/bnf_def.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Sep 26 10:01:00 2012 +0200
@@ -715,7 +715,7 @@
||>> mk_Frees' "r" setRTs
||>> mk_Frees "r" setRTs
||>> mk_Frees "s" setRTsBsCs
- ||>> mk_Frees' "R" QTs;
+ ||>> mk_Frees' "P" QTs;
(*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
val O_Gr =
--- a/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:01:00 2012 +0200
@@ -84,7 +84,8 @@
val nchotomyN: string
val recN: string
val recsN: string
- val relsN: string
+ val rel_injectN: string
+ val rel_distinctN: string
val rvN: string
val sel_corecsN: string
val sel_relsN: string
@@ -270,6 +271,10 @@
val iffsN = "_iffs"
val disc_unfold_iffsN = discN ^ "_" ^ unfoldN ^ iffsN
val disc_corec_iffsN = discN ^ "_" ^ corecN ^ iffsN
+val distinctN = "distinct"
+val rel_distinctN = relN ^ "_" ^ distinctN
+val injectN = "inject"
+val rel_injectN = relN ^ "_" ^ injectN
val relsN = relN ^ "s"
val selN = "sel"
val sel_relsN = selN ^ "_" ^ relsN
--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML Wed Sep 26 10:01:00 2012 +0200
@@ -532,27 +532,29 @@
(cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
|> postproc |> thaw (xs @ ys);
- fun mk_pos_rel_thm (((ctr_def', xs), cxIn), ((_, ys), cyIn)) =
+ fun mk_rel_inject_thm (((ctr_def', xs), cxIn), ((_, ys), cyIn)) =
mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] xs cxIn ys cyIn;
- val pos_rel_thms = map mk_pos_rel_thm (op ~~ rel_infos);
+ val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
- fun mk_half_neg_rel_thm (((xctr_def', xs), cxIn), ((yctr_def', ys), cyIn)) =
+ fun mk_half_rel_distinct_thm (((xctr_def', xs), cxIn), ((yctr_def', ys), cyIn)) =
mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
xs cxIn ys cyIn;
- fun mk_other_half_neg_rel_thm thm =
+ 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 half_neg_rel_thmss = map (map mk_half_neg_rel_thm) (mk_half_pairss rel_infos);
- val other_half_neg_rel_thmss = map (map mk_other_half_neg_rel_thm) half_neg_rel_thmss;
- val (neg_rel_thms, _) = join_halves n half_neg_rel_thmss other_half_neg_rel_thmss;
-
- val rel_thms = pos_rel_thms @ neg_rel_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;
val notes =
[(mapsN, map_thms, code_simp_attrs),
- (relsN, rel_thms, code_simp_attrs),
+ (rel_distinctN, rel_distinct_thms, code_simp_attrs),
+ (rel_injectN, rel_inject_thms, code_simp_attrs),
(setsN, flat set_thmss, code_simp_attrs)]
|> filter_out (null o #2)
|> map (fn (thmN, thms, attrs) =>
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 26 10:01:00 2012 +0200
@@ -1874,7 +1874,7 @@
||>> mk_Frees "f" unfold_fTs
||>> mk_Frees "g" unfold_fTs
||>> mk_Frees "s" corec_sTs
- ||>> mk_Frees "R" (map2 mk_pred2T Ts Ts);
+ ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
fun dtor_bind i = Binding.suffix_name ("_" ^ dtorN) (nth bs (i - 1));
val dtor_name = Binding.name_of o dtor_bind;
@@ -2318,7 +2318,7 @@
||>> mk_Frees "u" uTs
||>> mk_Frees' "b" Ts'
||>> mk_Frees' "b" Ts'
- ||>> mk_Freess "R" (map (fn A => map (mk_pred2T A) Ts) passiveAs)
+ ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs)
||>> mk_Frees "r" JRTs
||>> mk_Frees "P" JphiTs
||>> mk_Frees "B1" B1Ts