# HG changeset patch
# User blanchet
# Date 1346319107 -7200
# Node ID fc3b9b49c92dd3286578aa5ddbd4817d415aa1fa
# Parent  72dcf53c1ee44c3d48258424d5180a511f3ea935
added discriminator theorems

diff -r 72dcf53c1ee4 -r fc3b9b49c92d src/HOL/Codatatype/Tools/bnf_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 11:31:20 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Thu Aug 30 11:31:47 2012 +0200
@@ -21,13 +21,19 @@
 val casesN = "cases"
 val ctr_selsN = "ctr_sels"
 val disc_disjointN = "disc_disjoint"
+val disc_exhaustN = "disc_exhaust"
+val discsN = "discs"
 val distinctN = "distinct"
-val disc_exhaustN = "disc_exhaust"
 val selsN = "sels"
 val splitN = "split"
 val split_asmN = "split_asm"
 val weak_case_cong_thmsN = "weak_case_cong"
 
+fun index_of_triangle_row _ 0 = 0
+  | index_of_triangle_row n j = index_of_triangle_row n (j - 1) + n - j;
+
+fun index_of_triangle_cell n j k = index_of_triangle_row n j + k - (j + 1);
+
 fun prepare_sugar prep_term (((raw_ctrs, raw_caseof), disc_names), sel_namess) no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
@@ -194,7 +200,20 @@
             flat (map6 mk_thms ks xss goal_cases case_thms selss sel_defss)
           end;
 
-        val disc_thms = [];
+        val disc_thms =
+          let
+            fun get_distinct_thm k k' =
+              if k > k' then nth half_distinct_thms (index_of_triangle_cell n (k' - 1) (k - 1))
+              else nth other_half_distinct_thms (index_of_triangle_cell n (k' - 1) (k' - 1))
+            fun mk_thm ((k, m), disc_def) k' =
+              if k = k' then
+                refl RS (funpow m (fn thm => exI RS thm) (disc_def RS iffD2))
+              else
+                get_distinct_thm k k' RS (funpow m (fn thm => allI RS thm)
+                  (Local_Defs.unfold lthy @{thms not_ex} (disc_def RS @{thm ssubst[of _ _ Not]})));
+          in
+            map_product mk_thm (ks ~~ map length ctr_Tss ~~ disc_defs) ks
+          end;
 
         val disc_disjoint_thms = [];
 
@@ -223,6 +242,7 @@
         |> note case_discsN case_disc_thms
         |> note casesN case_thms
         |> note ctr_selsN ctr_sel_thms
+        |> note discsN disc_thms
         |> note disc_disjointN disc_disjoint_thms
         |> note disc_exhaustN disc_exhaust_thms
         |> note distinctN (half_distinct_thms @ other_half_distinct_thms)