(* @chunk SIMPLE_INDUCTIVE_PACKAGE *)

signature SIMPLE_INDUCTIVE_PACKAGE =

sig

  val add_inductive_i:

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

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

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

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

  val add_inductive:

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

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

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

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

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 (Name.name_of p, T)) params;

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

      list_comb (Free (Name.name_of 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;

    fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P;

    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.no_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 (Name.name_of o fst) params) lthy1;

    (* proving the 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 inst_spec ct = Drule.instantiate'

      [SOME (ctyp_of_term ct)] [NONE, SOME ct] spec;

    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);

    (* proving the introduction rules *)

    val all_elims = fold (fn ct => fn th => th RS inst_spec ct);

    val imp_elims = fold (fn th => fn th' => [th', th] MRS mp);

    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;

    (* storing the theorems *)

    val mut_name = space_implode "_" (map (Name.name_of o fst o fst) preds_syn);

    val case_names = map (Name.name_of o fst o fst) intrs

  in

    lthy1 |>

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

      ((Name.qualified mut_name a, atts), [([th], [])]))

        (intrs ~~ intr_ths)) |->

    (fn intr_thss => LocalTheory.note Thm.theoremK

       ((Name.qualified mut_name (Name.binding "intros"), []), maps snd intr_thss)) |>>

    snd ||>>

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

       ((Name.qualified (Name.name_of R) (Name.binding "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 *)

fun add_inductive preds_syn params_syn intro_srcs lthy =

  let

    val ((vars, specs), _) = Specification.read_specification

      (preds_syn @ params_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs)

      lthy;

    val (preds_syn', params_syn') = chop (length preds_syn) vars;

    val intrs = map (apsnd the_single) specs

  in

    add_inductive_i preds_syn' (map fst params_syn') intrs lthy

  end;

(* @end *)

(* outer syntax *)

(* @chunk syntax *)

local structure P = OuterParse and K = OuterKeyword in

val ind_decl =

  P.opt_target --

  P.fixes -- P.for_fixes --

  Scan.optional (P.$$$ "where" |--

    P.!!! (P.enum1 "|" (SpecParse.opt_thm_name ":" -- P.prop))) [] >>

  (fn (((loc, preds), params), specs) =>

    Toplevel.local_theory loc (add_inductive preds params specs #> snd));

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

  K.thy_decl ind_decl;

end;

(* @end *)

end;