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+
−