(* @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}*)
    (Attrib.binding * string list) list list ->  (*{rules}*)
    local_theory -> local_theory
end;
(* @end *)

structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
struct

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

fun inst_spec ct = Drule.instantiate'
      [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};

val all_elims = fold (fn ct => fn th => th RS inst_spec ct);
val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp});

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 *)
fun add_inductive preds params specs lthy =
 let
    val ((vars, specs'), _) = Specification.read_specification (preds @ params) specs lthy;
    val (preds', params') = chop (length preds) vars;
    val specs'' = map (apsnd the_single) specs'
    val params'' = map fst params'
 in
    snd (add_inductive_i preds' params'' specs'' lthy) 
 end;
(* @end *)


(* outer syntax *)
(* @chunk syntax *)
val parser = 
   OuterParse.opt_target --
   OuterParse.fixes -- 
   OuterParse.for_fixes --
   Scan.optional 
       (OuterParse.$$$ "where" |--
          OuterParse.!!! 
            (OuterParse.enum1 "|" 
               ((SpecParse.opt_thm_name ":" -- 
                   (OuterParse.prop >> single)) >> single))) []


val ind_decl =
    parser >>
    (fn (((loc, preds), params), specs) =>
      Toplevel.local_theory loc (add_inductive preds params specs));

val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
  OuterKeyword.thy_decl ind_decl;
(* @end *)

end;