relator induction for datatypes

--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Wed May 08 11:57:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Wed May 08 13:33:04 2013 +0200
@@ -93,6 +93,8 @@
   val morN: string
   val nchotomyN: string
   val recN: string
+  val rel_coinductN: string
+  val rel_inductN: string
   val rel_injectN: string
   val rel_distinctN: string
   val rvN: string
@@ -310,6 +312,8 @@
 val rel_distinctN = relN ^ "_" ^ distinctN
 val injectN = "inject"
 val rel_injectN = relN ^ "_" ^ injectN
+val rel_coinductN = relN ^ "_" ^ coinductN
+val rel_inductN = relN ^ "_" ^ inductN
 val selN = "sel"
 val sel_unfoldN = selN ^ "_" ^ unfoldN
 val sel_corecN = selN ^ "_" ^ corecN

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed May 08 11:57:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed May 08 13:33:04 2013 +0200
@@ -1366,6 +1366,13 @@
     fun mk_ctor_Irel_DEADID_thm ctor_inject bnf =
       trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
 
+    val IphiTs = map2 mk_pred2T passiveAs passiveBs;
+    val activeIphiTs = map2 mk_pred2T Ts Ts';
+    val ((Iphis, activeIphis), names_lthy) = names_lthy
+      |> mk_Frees "R" IphiTs
+      ||>> mk_Frees "IR" activeIphiTs;
+    val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
+
     (*register new datatypes as BNFs*)
     val (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) =
       if m = 0 then
@@ -1383,10 +1390,9 @@
         val AXTs = map HOLogic.mk_setT passiveXs;
         val XTs = mk_Ts passiveXs;
         val YTs = mk_Ts passiveYs;
-        val IphiTs = map2 mk_pred2T passiveAs passiveBs;
 
-        val ((((((((((((((fs, fs'), fs_copy), us),
-          B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')), Iphis),
+        val (((((((((((((fs, fs'), fs_copy), us),
+          B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')),
           names_lthy) = names_lthy
           |> mk_Frees' "f" fTs
           ||>> mk_Frees "f" fTs
@@ -1399,8 +1405,7 @@
           ||>> mk_Frees "f2" f2Ts
           ||>> mk_Frees "p1" p1Ts
           ||>> mk_Frees "p2" p2Ts
-          ||>> mk_Frees' "y" passiveAs
-          ||>> mk_Frees "R" IphiTs;
+          ||>> mk_Frees' "y" passiveAs;
 
         val map_FTFT's = map2 (fn Ds =>
           mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
@@ -1746,7 +1751,6 @@
 
         val timer = time (timer "registered new datatypes as BNFs");
 
-        val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
         val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
 
         val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels;
@@ -1803,9 +1807,33 @@
           lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
       end;
 
+      val Irel_induct_thm =
+        let
+          val relphis = map (fn rel => Term.list_comb (rel, Iphis @ activeIphis)) rels;
+          fun mk_prem relphi phi x y ctor ctor' =
+            fold_rev Logic.all [x, y] (Logic.mk_implies (HOLogic.mk_Trueprop (relphi $ x $ y),
+              HOLogic.mk_Trueprop (phi $ (ctor $ x) $ (ctor' $ y))));
+          val prems = map6 mk_prem relphis activeIphis xFs yFs ctors ctor's;
+
+          val Irels = if m = 0 then map HOLogic.eq_const Ts
+            else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
+          val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels;
+          val concl =
+            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq Irelphis activeIphis));
+        in
+          Goal.prove_sorry lthy [] []
+            (fold_rev Logic.all (Iphis @ activeIphis) (Logic.list_implies (prems, concl)))
+            (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms
+               (map rel_mono_strong_of_bnf bnfs))
+          |> Thm.close_derivation
+        end;
+
+      val timer = time (timer "relator induction");
+
       val common_notes =
         [(ctor_inductN, [ctor_induct_thm]),
-        (ctor_induct2N, [ctor_induct2_thm])]
+        (ctor_induct2N, [ctor_induct2_thm]),
+        (rel_inductN, [Irel_induct_thm])]
         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 

--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed May 08 11:57:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed May 08 13:33:04 2013 +0200
@@ -64,6 +64,8 @@
   val mk_mor_select_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list list ->
     thm list -> tactic
   val mk_mor_str_tac: 'a list -> thm -> tactic
+  val mk_rel_induct_tac: int -> thm -> int list -> thm list -> thm list ->
+    {prems: 'a, context: Proof.context} -> tactic
   val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
   val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
     tactic
@@ -844,4 +846,19 @@
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   end;
 
+fun mk_rel_induct_tac m ctor_induct2 ks ctor_rels rel_mono_strongs {context = ctxt, prems = _} =
+  let val n = length ks;
+  in
+    unfold_tac @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} ctxt THEN
+    EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
+      EVERY' (map3 (fn i => fn ctor_rel => fn rel_mono_strong =>
+        EVERY' [rtac impI, dtac (ctor_rel RS iffD1), select_prem_tac n (dtac @{thm meta_spec2}) i,
+          etac meta_mp, etac rel_mono_strong,
+          REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]},
+          EVERY' (map (fn j =>
+            EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]},
+              Goal.assume_rule_tac ctxt]) ks)])
+      ks ctor_rels rel_mono_strongs)] 1
+  end;
+
 end;