(* @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 -> local_theory

  val add_inductive:
    (Binding.binding * string option * mixfix) list ->  (*{predicates}*)
    (Binding.binding * string option * mixfix) list ->  (*{parameters}*)
    (Attrib.binding * string) list ->  (*{rules}*)
    local_theory -> local_theory
end;
(* @end *)

structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
struct

(* @chunk make_definitions *) 
fun make_defs ((binding, syn), trm) lthy =
let 
  val arg = ((binding, syn), ((Binding.suffix_name "_def" binding, []), trm))
  val ((_, (_ , thm)), lthy) = Local_Theory.define arg lthy
in 
  (thm, lthy) 
end
(* @end *)

(* @chunk definitions_aux *) 
fun defs_aux lthy orules preds params (pred, arg_types) =
let 
  fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P 

  val fresh_args = 
        arg_types 
        |> map (pair "z")
        |> Variable.variant_frees lthy orules 
        |> map Free
in
  list_comb (pred, fresh_args)
  |> fold_rev (curry HOLogic.mk_imp) orules
  |> fold_rev mk_all preds
  |> fold_rev lambda (params @ fresh_args) 
end
(* @end *)

(* @chunk definitions *) 
fun definitions rules params preds prednames syns arg_typess lthy =
let
  val thy = Proof_Context.theory_of lthy
  val orules = map (Object_Logic.atomize_term thy) rules
  val defs = 
    map (defs_aux lthy orules preds params) (preds ~~ arg_typess) 
in
  fold_map make_defs (prednames ~~ syns ~~ defs) lthy
end
(* @end *)

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

(* @chunk induction_tac *)
fun induction_tac defs prems insts =
  EVERY1 [Object_Logic.full_atomize_tac,
          cut_facts_tac prems,
          rewrite_goal_tac defs,
          EVERY' (map (dtac o inst_spec) insts),
          assume_tac]
(* @end *)

(* @chunk induction_rules *)
fun inductions rules defs parnames preds Tss lthy1  =
let
  val (_, lthy2) = Variable.add_fixes parnames lthy1
  
  val Ps = replicate (length preds) "P"
  val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2

  val thy = Proof_Context.theory_of lthy3			      

  val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss
  val newpreds = map Free (newprednames ~~ Tss')
  val cnewpreds = map (cterm_of thy) newpreds
  val rules' = map (subst_free (preds ~~ newpreds)) rules

  fun prove_induction ((pred, newpred), Ts)  =
  let
    val (newargnames, lthy4) = 
          Variable.variant_fixes (replicate (length Ts) "z") lthy3;
    val newargs = map Free (newargnames ~~ Ts)

    val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
    val goal = Logic.list_implies 
         (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
  in
    Goal.prove lthy4 [] [prem] goal
      (fn {prems, ...} => induction_tac defs prems cnewpreds)
      |> singleton (Proof_Context.export lthy4 lthy1)
  end 
in
  map prove_induction (preds ~~ newpreds ~~ Tss)
end
(* @end *)

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


(* @chunk subproof1 *) 
fun subproof2 prem params2 prems2 =  
 SUBPROOF (fn {prems, ...} =>
  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)
(* @end *)

(* @chunk subproof2 *) 
fun subproof1 rules preds i = 
 SUBPROOF (fn {params, prems, context = ctxt', ...} =>
  let
    val (prems1, prems2) = chop (length prems - length rules) prems;
    val (params1, params2) = chop (length params - length preds) (map snd params);
  in
    rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 
    THEN
    EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
  end)
(* @end *)

fun introductions_tac defs rules preds i ctxt =
  EVERY1 [Object_Logic.rulify_tac,
          rewrite_goal_tac defs,
          REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
          subproof1 rules preds i ctxt]


(* @chunk intro_rules *) 
fun introductions rules parnames preds defs lthy1 = 
let
  val (_, lthy2) = Variable.add_fixes parnames lthy1

  fun prove_intro (i, goal) =
    Goal.prove lthy2 [] [] goal
       (fn {context, ...} => introductions_tac defs rules preds i context)
       |> singleton (Proof_Context.export lthy2 lthy1)
in
  map_index prove_intro rules
end
(* @end *)

(* @chunk add_inductive_i *)
fun add_inductive_i preds params specs lthy =
let
  val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params;
  val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds;
  val Tss = map (binder_types o fastype_of) preds';   
  val (ass, rules) = split_list specs;  (* FIXME: ass not used? *)  

  val prednames = map (fst o fst) preds
  val syns = map snd preds
  val parnames = map (Binding.name_of o fst) params

  val (defs, lthy1) = definitions rules params' preds' prednames syns Tss lthy;
      
  val inducts = inductions rules defs parnames preds' Tss lthy1 	
  
  val intros = introductions rules parnames preds' defs lthy1

  val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds);
  val case_names = map (Binding.name_of o fst o fst) specs
in
    lthy1 
    |> Local_Theory.notes (map (fn (((a, atts), _), th) =>
        ((Binding.qualify false mut_name a, atts), [([th], [])])) (specs ~~ intros)) 
    |-> (fn intross => Local_Theory.note 
         ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) 
    |>> snd 
    ||>> (Local_Theory.notes (map (fn (((R, _), _), th) =>
         ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),
          [Attrib.internal (K (Rule_Cases.case_names case_names)),
           Attrib.internal (K (Rule_Cases.consumes 1)),
           Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
          (preds ~~ inducts)) #>> maps snd) 
    |> snd
end
(* @end *)

(* @chunk read_specification *)
fun read_specification' vars specs lthy =
let 
  val specs' = map (fn (a, s) => (a, [s])) specs
  val ((varst, specst), _) = 
                   Specification.read_specification vars specs' lthy
  val specst' = map (apsnd the_single) specst
in   
  (varst, specst')
end 
(* @end *)

(* @chunk add_inductive *)
fun add_inductive preds params specs lthy =
let
  val (vars, specs') = read_specification' (preds @ params) specs lthy;
  val (preds', params') = chop (length preds) vars;
  val params'' = map fst params'
in
  add_inductive_i preds' params'' specs' lthy
end;
(* @end *)

(* @chunk parser *)
val spec_parser = 
   Parse.opt_target --
   Parse.fixes -- 
   Parse.for_fixes --
   Scan.optional 
     (Parse.$$$ "where" |--
        Parse.!!! 
          (Parse.enum1 "|" 
             (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []
(* @end *)

(* @chunk syntax *)
val specification =
  spec_parser >>
    (fn (((loc, preds), params), specs) =>
      Toplevel.local_theory loc (add_inductive preds params specs))

val _ = Outer_Syntax.command @{command_spec "simple_inductive"} "define inductive predicates"
          specification
(* @end *)

end;