# HG changeset patch
# User blanchet
# Date 1348646460 -7200
# Node ID b859a02c11503e0ddadbbf76052ab7477b339203
# Parent  91b228e263486c9e95fa3dfea74bca359b43abda
fixed "rels" + split them into injectivity and distinctness

diff -r 91b228e26348 -r b859a02c1150 src/HOL/BNF/Tools/bnf_def.ML
--- 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 =
diff -r 91b228e26348 -r b859a02c1150 src/HOL/BNF/Tools/bnf_fp.ML
--- 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
diff -r 91b228e26348 -r b859a02c1150 src/HOL/BNF/Tools/bnf_fp_sugar.ML
--- 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) =>
diff -r 91b228e26348 -r b859a02c1150 src/HOL/BNF/Tools/bnf_gfp.ML
--- 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