theory Ind_Code
imports "../Base" Simple_Inductive_Package Ind_Prelims
begin

section {* Code *}

subsection {* Definitions *}

text {*
  If we give it a term and a constant name, it will define the 
  constant as the term. 
*}

ML{*fun make_defs ((binding, syn), trm) lthy =
let 
  val arg = ((binding, syn), (Attrib.empty_binding, trm))
  val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy
in 
  (thm, lthy) 
end*}

text {*
  Returns the definition and the local theory in which this definition has 
  been made. What is @{ML Thm.internalK}?
*}

ML {*let
  val lthy = TheoryTarget.init NONE @{theory}
in
  make_defs ((Binding.name "MyTrue", NoSyn), @{term "True"}) lthy
end*}

text {*
  Why is the output of MyTrue blue?
*}

text {*
  Constructs the term for the definition: the main arguments are a predicate
  and the types of the arguments, it also expects orules which are the 
  intro rules in the object logic; preds which are all predicates. returns the
  term.
*}

ML %linenosgray{*fun defs_aux lthy orules preds (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 fresh_args 
end*}

text {*
  The lines 5-9 produce fresh arguments with which the predicate can be applied.
  For this it pairs every type with a string @{text [quotes] "z"} (Line 7); then 
  generates variants for all these strings (names) so that they are unique w.r.t.~to 
  the intro rules; in Line 9 it generates the corresponding variable terms for these 
  unique names.

  The unique free variables are applied to the predicate (Line 11); then
  the intro rules are attached as preconditions (Line 12); in Line 13 we
  quantify over all predicates; and in line 14 we just abstract over all
  the (fresh) arguments of the predicate.
*}

text {*
  The arguments of the main function for the definitions are 
  the intro rules; the predicates and their names, their syntax 
  annotations and the argument types of each predicate. It  
  returns a theorem list (the definitions) and a local
  theory where the definitions are made
*}

ML %linenosgray{*fun definitions rules preds prednames syns arg_typss lthy =
let
  val thy = ProofContext.theory_of lthy
  val orules = map (ObjectLogic.atomize_term thy) rules
  val defs = map (defs_aux lthy orules preds) (preds ~~ arg_typss) 
in
  fold_map make_defs (prednames ~~ syns ~~ defs) lthy
end*}

text {*
  In line 4 we generate the intro rules in the object logic; for this we have to 
  obtain the theory behind the local theory (Line 3); with this we can
  call @{ML defs_aux} to generate the terms for the left-hand sides.
  The actual definitions are made in Line 7.  
*}

subsection {* Introduction Rules *}

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

text {*
  Instantiates the @{text "x"} in @{thm spec[no_vars]} with a @{ML_type cterm}.
*}

text {*
  Instantiates universal qantifications in the premises
*}

lemma "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \<Longrightarrow> True"
apply (tactic {* EVERY' (map (dtac o inst_spec) 
          [@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*})
(*<*)oops(*>*)

text {*
  The tactic for proving the induction rules: 
*}

ML{*fun induction_tac defs prems insts =
  EVERY1 [ObjectLogic.full_atomize_tac,
          cut_facts_tac prems,
          K (rewrite_goals_tac defs),
          EVERY' (map (dtac o inst_spec) insts),
          assume_tac]*}

lemma 
  assumes asm: "even n"
  shows "P 0 \<Longrightarrow> 
           (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
apply(tactic {* induction_tac [@{thm even_def}, @{thm odd_def}] [@{thm asm}] 
  [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})
done

ML %linenosgray{*fun inductions rules defs preds Tss lthy1  =
let
  val Ps = replicate (length preds) "P"
  val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1
  
  val thy = ProofContext.theory_of lthy2

  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 zs = replicate (length Ts) "z"
    val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;
    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 lthy3 [] [prem] goal
      (fn {prems, ...} => induction_tac defs prems cnewpreds)
      |> singleton (ProofContext.export lthy3 lthy1)
  end 
in
  map prove_induction (preds ~~ newpreds ~~ Tss)
end*}

ML {* Goal.prove  *}
ML {* singleton *}
ML {* ProofContext.export *}

text {*

*}

text {*
  @{ML_chunk [display,gray] subproof1}

  @{ML_chunk [display,gray] subproof2}

  @{ML_chunk [display,gray] intro_rules}


*}

text {*
  Things to include at the end:

  \begin{itemize}
  \item say something about add-inductive-i to return
  the rules
  \item say that the induction principle is weaker (weaker than
  what the standard inductive package generates)
  \end{itemize}
  
*}


end