imports "../Base" Simple_Inductive_Package Ind_Prelims

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.

*}

  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 *}

  @{ML_chunk [display,gray] subproof1}

  @{ML_chunk [display,gray] subproof2}