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 {* Induction Principles *}+
−
+
−
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} 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*})+
−
txt {* \begin{minipage}{\textwidth}+
−
       @{subgoals} +
−
       \end{minipage}*}+
−
(*<*)oops(*>*)+
−
+
−
+
−
lemma +
−
  assumes "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(atomize (full))+
−
apply(cut_tac prems)+
−
apply(unfold even_def)+
−
apply(drule spec[where x=P])+
−
apply(drule spec[where x=Q])+
−
apply(assumption)+
−
done+
−
+
−
text {*+
−
  The tactic for proving the induction rules: +
−
*}+
−
+
−
ML{*fun induction_tac defs prems insts =+
−
  EVERY1 [K (print_tac "start"),+
−
          ObjectLogic.full_atomize_tac,+
−
          cut_facts_tac prems,+
−
          K (rewrite_goals_tac defs),+
−
          EVERY' (map (dtac o inst_spec) insts),+
−
          assume_tac]*}+
−
+
−
lemma +
−
  assumes "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 {* +
−
  let+
−
     val defs = [@{thm even_def}, @{thm odd_def}]+
−
     val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]+
−
  in +
−
    induction_tac defs @{thms prems} insts +
−
  end *})+
−
done+
−
+
−
text {*+
−
  While the generic proof is relatively simple, it is a bit harder to+
−
  set up the goals for the induction principles. +
−
*}+
−
+
−
+
−
ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =+
−
let+
−
  val Ps = replicate (length preds) "P"+
−
  val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1+
−
  +
−
  val thy = ProofContext.theory_of lthy2+
−
+
−
  val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss+
−
  val newpreds = map Free (newprednames ~~ tyss')+
−
  val cnewpreds = map (cterm_of thy) newpreds+
−
  val rules' = map (subst_free (preds ~~ newpreds)) rules+
−
+
−
  fun prove_induction ((pred, newpred), tys)  =+
−
  let+
−
    val zs = replicate (length tys) "z"+
−
    val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;+
−
    val newargs = map Free (newargnames ~~ tys)+
−
+
−
    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 ~~ tyss)+
−
end*}+
−
+
−
(*+
−
ML {*+
−
  let +
−
    val rules = [@{term "even 0"},+
−
                 @{term "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},+
−
                 @{term "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] +
−
    val defs = [@{thm even_def}, @{thm odd_def}]+
−
    val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]+
−
    val tyss = [[@{typ "nat"}],[@{typ "nat"}]]+
−
  in+
−
    inductions rules defs preds tyss @{context}+
−
  end+
−
*}+
−
*)+
−
+
−
subsection {* Introduction Rules *}+
−
+
−
ML{*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})*}+
−
+
−
ML{*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)*}+
−
+
−
ML{*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) params;+
−
   in+
−
     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 +
−
     THEN+
−
     EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)+
−
   end)*}+
−
+
−
ML{*+
−
fun introductions_tac defs rules preds i ctxt =+
−
  EVERY1 [ObjectLogic.rulify_tac,+
−
          K (rewrite_goals_tac defs),+
−
          REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),+
−
          subproof1 rules preds i ctxt]*}+
−
+
−
ML{*fun introductions rules preds defs lthy = +
−
let+
−
  fun prove_intro (i, goal) =+
−
    Goal.prove lthy [] [] goal+
−
      (fn {context, ...} => introductions_tac defs rules preds i context)+
−
in+
−
  map_index prove_intro rules+
−
end*}+
−
+
−
ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy =+
−
let+
−
  val syns = map snd pred_specs+
−
  val pred_specs' = map fst pred_specs+
−
  val prednames = map fst pred_specs'+
−
  val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'+
−
+
−
  val tyss = map (binder_types o fastype_of) preds   +
−
  val (attrs, rules) = split_list rule_specs    +
−
+
−
  val (defs, lthy') = definitions rules preds prednames syns tyss lthy      +
−
  val ind_rules = inductions rules defs preds tyss lthy' 	+
−
  val intro_rules = introductions rules preds defs lthy'+
−
+
−
  val mut_name = space_implode "_" (map Binding.name_of prednames)+
−
  val case_names = map (Binding.name_of o fst) attrs+
−
in+
−
    lthy' +
−
    |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>+
−
        ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) +
−
    |-> (fn intross => LocalTheory.note Thm.theoremK+
−
         ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) +
−
    |>> snd +
−
    ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>+
−
         ((Binding.qualify false (Binding.name_of 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], [])]))+
−
          (pred_specs ~~ ind_rules)) #>> maps snd) +
−
    |> snd+
−
end*}+
−
+
−
+
−
ML{*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*}+
−
+
−
ML{*fun add_inductive pred_specs rule_specs lthy =+
−
let+
−
  val (pred_specs', rule_specs') = +
−
    read_specification' pred_specs rule_specs lthy+
−
in+
−
  add_inductive_i pred_specs' rule_specs' lthy+
−
end*} +
−
+
−
ML{*val spec_parser = +
−
   OuterParse.opt_target --+
−
   OuterParse.fixes -- +
−
   Scan.optional +
−
     (OuterParse.$$$ "where" |--+
−
        OuterParse.!!! +
−
          (OuterParse.enum1 "|" +
−
             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}+
−
+
−
ML{*val specification =+
−
  spec_parser >>+
−
    (fn ((loc, pred_specs), rule_specs) =>+
−
      Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*}+
−
+
−
ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"+
−
          OuterKeyword.thy_decl specification*}+
−
+
−
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}+
−
  +
−
*}+
−
+
−
simple_inductive+
−
  Even and Odd+
−
where+
−
  Even0: "Even 0"+
−
| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"+
−
| OddS: "Even n \<Longrightarrow> Odd (Suc n)"+
−
+
−
end+
−