# HG changeset patch
# User blanchet
# Date 1371158799 14400
# Node ID bae65fd74633c83763d3409264a9f9fb6fc169ee
# Parent  ddb16589b711ec52828010bec5d86038bde88350
store more theorems in data structure

diff -r ddb16589b711 -r bae65fd74633 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Jun 13 16:58:20 2013 -0400
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Jun 13 17:26:39 2013 -0400
@@ -9,12 +9,18 @@
 sig
   type ctr_sugar =
     {ctrs: term list,
+     casex: term,
      discs: term list,
      selss: term list list,
      exhaust: thm,
+     nchotomy: thm,
      injects: thm list,
      distincts: thm list,
      case_thms: thm list,
+     case_cong: thm,
+     weak_case_cong: thm,
+     split: thm,
+     split_asm: thm,
      disc_thmss: thm list list,
      discIs: thm list,
      sel_thmss: thm list list};
@@ -48,25 +54,37 @@
 
 type ctr_sugar =
   {ctrs: term list,
+   casex: term,
    discs: term list,
    selss: term list list,
    exhaust: thm,
+   nchotomy: thm,
    injects: thm list,
    distincts: thm list,
    case_thms: thm list,
+   case_cong: thm,
+   weak_case_cong: thm,
+   split: thm,
+   split_asm: thm,
    disc_thmss: thm list list,
    discIs: thm list,
    sel_thmss: thm list list};
 
-fun morph_ctr_sugar phi {ctrs, discs, selss, exhaust, injects, distincts, case_thms, disc_thmss,
-    discIs, sel_thmss} =
+fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
+    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss} =
   {ctrs = map (Morphism.term phi) ctrs,
+   casex = Morphism.term phi casex,
    discs = map (Morphism.term phi) discs,
    selss = map (map (Morphism.term phi)) selss,
    exhaust = Morphism.thm phi exhaust,
+   nchotomy = Morphism.thm phi nchotomy,
    injects = map (Morphism.thm phi) injects,
    distincts = map (Morphism.thm phi) distincts,
    case_thms = map (Morphism.thm phi) case_thms,
+   case_cong = Morphism.thm phi case_cong,
+   weak_case_cong = Morphism.thm phi weak_case_cong,
+   split = Morphism.thm phi split,
+   split_asm = Morphism.thm phi split_asm,
    disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    discIs = map (Morphism.thm phi) discIs,
    sel_thmss = map (map (Morphism.thm phi)) sel_thmss};
@@ -702,8 +720,10 @@
           [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
       in
-        ({ctrs = ctrs, discs = discs, selss = selss, exhaust = exhaust_thm, injects = inject_thms,
-          distincts = distinct_thms, case_thms = case_thms, disc_thmss = disc_thmss,
+        ({ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
+          nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
+          case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
+          split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
           discIs = discI_thms, sel_thmss = sel_thmss},
          lthy
          |> not rep_compat ?