# HG changeset patch
# User blanchet
# Date 1367505184 -7200
# Node ID 9761deff11bc50b3b706c6c08b38112af94c225e
# Parent  d77cf35c27ac522bc6d7a71b96e1cf97199ef8ad
store (co)induction rules in data structure

diff -r d77cf35c27ac -r 9761deff11bc src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 16:14:14 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 16:33:04 2013 +0200
@@ -16,6 +16,8 @@
      ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
      un_folds: term list,
      co_recs: term list,
+     co_induct: thm,
+     strong_co_induct: thm,
      un_fold_thmss: thm list list,
      co_rec_thmss: thm list list};
 
@@ -83,6 +85,8 @@
    ctr_sugars: ctr_sugar list,
    un_folds: term list,
    co_recs: term list,
+   co_induct: thm,
+   strong_co_induct: thm,
    un_fold_thmss: thm list list,
    co_rec_thmss: thm list list};
 
@@ -90,11 +94,12 @@
     {T = T2, lfp = lfp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
   T1 = T2 andalso lfp1 = lfp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
 
-fun morph_fp_sugar phi {T, lfp, index, pre_bnfs, fp_res, ctr_sugars, un_folds, co_recs,
-    un_fold_thmss, co_rec_thmss} =
+fun morph_fp_sugar phi {T, lfp, index, pre_bnfs, fp_res, ctr_sugars, un_folds, co_recs, co_induct,
+    strong_co_induct, un_fold_thmss, co_rec_thmss} =
   {T = Morphism.typ phi T, lfp = lfp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
    fp_res = morph_fp_result phi fp_res, ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
    un_folds = map (Morphism.term phi) un_folds, co_recs = map (Morphism.term phi) co_recs,
+   co_induct = Morphism.thm phi co_induct, strong_co_induct = Morphism.thm phi strong_co_induct,
    un_fold_thmss = map (map (Morphism.thm phi)) un_fold_thmss,
    co_rec_thmss = map (map (Morphism.thm phi)) co_rec_thmss};
 
@@ -112,13 +117,14 @@
   Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar)));
 
-fun register_fp_sugars lfp pre_bnfs (fp_res as {Ts, ...}) ctr_sugars un_folds co_recs
-    un_fold_thmss co_rec_thmss lthy =
+fun register_fp_sugars lfp pre_bnfs (fp_res as {Ts, ...}) ctr_sugars un_folds co_recs co_induct
+    strong_co_induct un_fold_thmss co_rec_thmss lthy =
   (0, lthy)
   |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
     register_fp_sugar s {T = T, lfp = lfp, index = kk, pre_bnfs = pre_bnfs, fp_res = fp_res,
-      ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs,
-      un_fold_thmss = un_fold_thmss, co_rec_thmss = co_rec_thmss} lthy)) Ts
+      ctr_sugars = ctr_sugars, un_folds = un_folds, co_recs = co_recs, co_induct = co_induct,
+      strong_co_induct = strong_co_induct, un_fold_thmss = un_fold_thmss,
+      co_rec_thmss = co_rec_thmss} lthy)) Ts
   |> snd;
 
 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
@@ -1314,7 +1320,8 @@
       in
         lthy
         |> Local_Theory.notes (common_notes @ notes) |> snd
-        |> register_fp_sugars true pre_bnfs fp_res ctr_sugars folds recs fold_thmss rec_thmss
+        |> register_fp_sugars true pre_bnfs fp_res ctr_sugars folds recs induct_thm induct_thm
+          fold_thmss rec_thmss
       end;
 
     fun derive_and_note_coinduct_unfold_corec_thms_for_types
@@ -1372,8 +1379,8 @@
       in
         lthy
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
-        |> register_fp_sugars false pre_bnfs fp_res ctr_sugars unfolds corecs unfold_thmss
-          corec_thmss
+        |> register_fp_sugars false pre_bnfs fp_res ctr_sugars unfolds corecs coinduct_thm
+          strong_coinduct_thm unfold_thmss corec_thmss
       end;
 
     val lthy' = lthy