(* @chunk SIMPLE_INDUCTIVE_PACKAGE *)

signature SIMPLE_INDUCTIVE_PACKAGE =

sig

  val add_inductive_i:

    ((Binding.binding * typ) * mixfix) list ->  (*{predicates}*)

    (Binding.binding * typ) list ->  (*{parameters}*)

    (Attrib.binding * term) list ->  (*{rules}*)

    local_theory -> (thm list * thm list) * local_theory

  val add_inductive:

    (Binding.binding * string option * mixfix) list ->  (*{predicates}*)

    (Binding.binding * string option * mixfix) list ->  (*{parameters}*)

end;

(* @end *)

structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =

struct

fun add_inductive_i preds_syn params intrs lthy =

  let

    val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;

    val preds = map (fn ((R, T), _) =>

      list_comb (Free (Binding.base_name R, T), params')) preds_syn;

    val Tss = map (binder_types o fastype_of) preds;

    (* making the definition *)

    val intrs' = map

      (ObjectLogic.atomize_term (ProofContext.theory_of lthy) o snd) intrs;

    val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) =>

      let val zs = map Free (Variable.variant_frees lthy intrs'

        (map (pair "z") Ts))

      in

        LocalTheory.define Thm.internalK

          ((R, syn), (Attrib.empty_binding, fold_rev lambda (params' @ zs)

            (fold_rev mk_all preds (fold_rev (curry HOLogic.mk_imp)

               intrs' (list_comb (pred, zs)))))) #>> snd #>> snd

       end) (preds_syn ~~ preds ~~ Tss) lthy;

    val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;

    (* proving the induction rules *)

    (* @chunk induction_rules *)

    val (Pnames, lthy3) =

      Variable.variant_fixes (replicate (length preds) "P") lthy2;

    val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT))

      (Pnames ~~ Tss);

    val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps;

    val intrs'' = map (subst_free (preds ~~ Ps) o snd) intrs;

    fun prove_indrule ((R, P), Ts) =

      let

        val (znames, lthy4) =

          Variable.variant_fixes (replicate (length Ts) "z") lthy3;

        val zs = map Free (znames ~~ Ts)

      in

        Goal.prove lthy4 []

          [HOLogic.mk_Trueprop (list_comb (R, zs))]

          (Logic.list_implies (intrs'',

             HOLogic.mk_Trueprop (list_comb (P, zs))))

          (fn {prems, ...} => EVERY

             ([ObjectLogic.full_atomize_tac 1,

               cut_facts_tac prems 1,

               rewrite_goals_tac defs] @

              map (fn ct => dtac (inst_spec ct) 1) cPs @

              [assume_tac 1])) |>

        singleton (ProofContext.export lthy4 lthy1)

      end;

    val indrules = map prove_indrule (preds ~~ Ps ~~ Tss);

    (* @end *)

    (* proving the introduction rules *)

    (* @chunk intro_rules *) 

    fun prove_intr (i, (_, r)) =

      Goal.prove lthy2 [] [] r

        (fn {prems, context = ctxt} => EVERY

           [ObjectLogic.rulify_tac 1,

            rewrite_goals_tac defs,

            REPEAT (resolve_tac [allI, impI] 1),

            SUBPROOF (fn {params, prems, context = ctxt', ...} =>

              let

                val (prems1, prems2) =

                  chop (length prems - length intrs) prems;

                val (params1, params2) =

                  chop (length params - length preds) params

              in

                rtac (ObjectLogic.rulify

                  (all_elims params1 (nth prems2 i))) 1 THEN

                EVERY (map (fn prem =>

                  SUBPROOF (fn {prems = prems', concl, ...} =>

                    let

                      val prem' = prems' MRS prem;

                      val prem'' = case prop_of prem' of

                          _ $ (Const (@{const_name All}, _) $ _) =>

                            prem' |> all_elims params2 |>

                            imp_elims prems2

                        | _ => prem'

                    in rtac prem'' 1 end) ctxt' 1) prems1)

              end) ctxt 1]) |>

      singleton (ProofContext.export lthy2 lthy1);

    val intr_ths = map_index prove_intr intrs;

    (* @end *)

    (* storing the theorems *)

    (* @chunk storing *)

    val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds_syn);

    val case_names = map (Binding.base_name o fst o fst) intrs

    (* @end *)

  in

    lthy1 |>

    LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>

      ((Binding.qualify mut_name a, atts), [([th], [])]))

        (intrs ~~ intr_ths)) |->

    (fn intr_thss => LocalTheory.note Thm.theoremK

       ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intr_thss)) |>>

    snd ||>>

    (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>

       ((Binding.qualify (Binding.base_name R) (Binding.name "induct"),

         [Attrib.internal (K (RuleCases.case_names case_names)),

          Attrib.internal (K (RuleCases.consumes 1)),

          Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))

         (preds_syn ~~ indrules)) #>> maps snd)

  end;

(* @chunk add_inductive *)

(* @end *)

(* outer syntax *)

val ind_decl =

val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"

(* @end *)

end;