theory Ind_Code+
−
imports "../Base" "../FirstSteps" Ind_General_Scheme +
−
begin+
−
+
−
section {* The Gory Details *} +
−
+
−
subsection {* Definitions *}+
−
+
−
text {*+
−
  We first have to produce for each predicate the definition, whose general form is+
−
+
−
  @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}+
−
+
−
  and then ``register'' the definition inside a local theory. +
−
  To do the latter, we use the following wrapper for +
−
  @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax+
−
  annotation and a term representing the right-hand side of the definition.+
−
*}+
−
+
−
ML %linenosgray{*fun make_defn ((predname, syn), trm) lthy =+
−
let +
−
  val arg = ((predname, syn), (Attrib.empty_binding, trm))+
−
  val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy+
−
in +
−
  (thm, lthy') +
−
end*}+
−
+
−
text {*+
−
  It returns the definition (as a theorem) and the local theory in which this definition has +
−
  been made. In Line 4, @{ML internalK in Thm} is a flag attached to the +
−
  theorem (others possibile flags are @{ML definitionK in Thm} and @{ML axiomK in Thm}). +
−
  These flags just classify theorems and have no significant meaning, except +
−
  for tools that, for example, find theorems in the theorem database. We also+
−
  use @{ML empty_binding in Attrib} in Line 3, since for our inductive predicates +
−
  the definitions do not need to have any theorem attributes. A testcase for this +
−
  function is+
−
*}+
−
+
−
local_setup %gray {* fn lthy =>+
−
let+
−
  val arg = ((@{binding "MyTrue"}, NoSyn), @{term True})+
−
  val (def, lthy') = make_defn arg lthy +
−
in+
−
  warning (str_of_thm_no_vars lthy' def); lthy'+
−
end *}+
−
+
−
text {*+
−
  which introduces the definition @{prop "MyTrue \<equiv> True"} and then prints it out. +
−
  Since we are testing the function inside \isacommand{local\_setup}, i.e., make+
−
  changes to the ambient theory, we can query the definition with the usual+
−
  command \isacommand{thm}:+
−
+
−
  \begin{isabelle}+
−
  \isacommand{thm}~@{text "MyTrue_def"}\\+
−
  @{text "> MyTrue \<equiv> True"}+
−
  \end{isabelle}+
−
+
−
  The next two functions construct the right-hand sides of the definitions, +
−
  which are terms of the form+
−
+
−
  @{text [display] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}+
−
+
−
  When constructing them, the variables @{text "zs"} need to be chosen so that+
−
  they do not occur in the @{text orules} and also be distinct from the @{text+
−
  "preds"}.+
−
+
−
+
−
  The first function constructs the term for one particular predicate (the+
−
  argument @{text "pred"} in the code belo). The number of arguments of this predicate is+
−
  determined by the number of argument types given in @{text "arg_tys"}. +
−
  The other arguments are all the @{text "preds"} and the @{text "orules"}.+
−
*}+
−
+
−
ML %linenosgray{*fun defn_aux lthy orules preds (pred, arg_tys) =+
−
let +
−
  fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P+
−
+
−
  val fresh_args = +
−
        arg_tys +
−
        |> map (pair "z")+
−
        |> Variable.variant_frees lthy (preds @ 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 function in Line 3 is just a helper function for constructing universal+
−
  quantifications. The code in Lines 5 to 9 produces the fresh @{text+
−
  "zs"}. For this it pairs every argument type with the string+
−
  @{text [quotes] "z"} (Line 7); then generates variants for all these strings+
−
  so that they are unique w.r.t.~to the predicates and @{text "orules"} (Line 8);+
−
  in Line 9 it generates the corresponding variable terms for the unique+
−
  strings.+
−
+
−
  The unique free variables are applied to the predicate (Line 11) using the+
−
  function @{ML list_comb}; then the @{text orules} are prefixed (Line 12); in+
−
  Line 13 we quantify over all predicates; and in line 14 we just abstract+
−
  over all the @{text "zs"}, i.e., the fresh arguments of the+
−
  predicate. A testcase for this function is+
−
*}+
−
+
−
local_setup %gray{* fn lthy =>+
−
let+
−
  val pred = @{term "even::nat\<Rightarrow>bool"}+
−
  val arg_tys = [@{typ "nat"}]+
−
  val def = defn_aux lthy eo_orules eo_preds (pred, arg_tys)+
−
in+
−
  warning (Syntax.string_of_term lthy def); lthy+
−
end *}+
−
+
−
text {*+
−
  The testcase  calls @{ML defn_aux} for the predicate @{text "even"} and prints+
−
  out the generated definition. So we obtain as printout +
−
+
−
  @{text [display] +
−
"\<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) +
−
                         \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z"}+
−
+
−
  If we try out the function for the definition of freshness+
−
*}+
−
+
−
local_setup %gray{* fn lthy =>+
−
 (warning (Syntax.string_of_term lthy+
−
    (defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys)));+
−
  lthy) *}+
−
+
−
text {*+
−
  we obtain+
−
+
−
  @{term [display] +
−
"\<lambda>z za. \<forall>fresh. (\<forall>a b. \<not> a = b \<longrightarrow> fresh a (Var b)) \<longrightarrow>+
−
               (\<forall>a s t. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>+
−
                (\<forall>a t. fresh a (Lam a t)) \<longrightarrow>+
−
                (\<forall>a b t. \<not> a = b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh z za"}+
−
+
−
+
−
  The second function for the definitions has to just iterate the function+
−
  @{ML defn_aux} over all predicates. The argument @{text "preds"} is again+
−
  the the list of predicates as @{ML_type term}s; the argument @{text+
−
  "prednames"} is the list of names of the predicates; @{text syns} are the+
−
  syntax annotations for each predicate; @{text "arg_tyss"} is+
−
  the list of argument-type-lists for each predicate.+
−
*}+
−
+
−
ML %linenosgray{*fun defns 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 (defn_aux lthy orules preds) (preds ~~ arg_typss) +
−
in+
−
  fold_map make_defn (prednames ~~ syns ~~ defs) lthy+
−
end*}+
−
+
−
text {*+
−
  The user will state the introduction rules using meta-implications and+
−
  meta-quanti\-fications. In Line 4, we transform these introduction rules into+
−
  the object logic (since definitions cannot be stated with+
−
  meta-connectives). To do this transformation we have to obtain the theory+
−
  behind the local theory (Line 3); with this theory we can use the function+
−
  @{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call+
−
  to @{ML defn_aux} in Line 5 produces all right-hand sides of the+
−
  definitions. The actual definitions are then made in Line 7.  The result+
−
  of the function is a list of theorems and a local theory. A testcase for +
−
  this function is +
−
*}+
−
+
−
local_setup %gray {* fn lthy =>+
−
let+
−
  val (defs, lthy') = +
−
    defns eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy+
−
in+
−
  warning (str_of_thms_no_vars lthy' defs); lthy+
−
end *}+
−
+
−
text {*+
−
  where we feed into the functions all parameters corresponding to+
−
  the @{text even}-@{text odd} example. The definitions we obtain+
−
  are:+
−
+
−
  @{text [display, break]+
−
"even \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n))  +
−
                                \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> even z,+
−
odd \<equiv> \<lambda>z. \<forall>even odd. (even 0) \<longrightarrow> (\<forall>n. odd n \<longrightarrow> even (Suc n)) +
−
                               \<longrightarrow> (\<forall>n. even n \<longrightarrow> odd (Suc n)) \<longrightarrow> odd z"}+
−
+
−
  Note that in the testcase we return the local theory @{text lthy} +
−
  (not the modified @{text lthy'}). As a result the test case has no effect+
−
  on the ambient theory. The reason is that if we introduce the+
−
  definition again, we pollute the name space with two versions of @{text "even"} +
−
  and @{text "odd"}.+
−
+
−
  This completes the code for introducing the definitions. Next we deal with+
−
  the induction principles. +
−
*}+
−
+
−
subsection {* Induction Principles *}+
−
+
−
text {*+
−
  Recall that the proof of the induction principle +
−
  for @{text "even"} was:+
−
*}+
−
+
−
lemma manual_ind_prin_even: +
−
assumes prem: "even z"+
−
shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"+
−
apply(atomize (full))+
−
apply(cut_tac prem)+
−
apply(unfold even_def)+
−
apply(drule spec[where x=P])+
−
apply(drule spec[where x=Q])+
−
apply(assumption)+
−
done+
−
+
−
text {* +
−
  The code for automating such induction principles has to accomplish two tasks: +
−
  constructing the induction principles from the given introduction+
−
  rules and then automatically generating proofs for them using a tactic. +
−
  +
−
  The tactic will use the following helper function for instantiating universal +
−
  quantifiers. +
−
*}+
−
+
−
ML{*fun inst_spec ctrm = +
−
 Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] @{thm spec}*}+
−
+
−
text {*+
−
  This helper function instantiates the @{text "?x"} in the theorem +
−
  @{thm spec} with a given @{ML_type cterm}. We call this helper function+
−
  in the tactic:+
−
*}+
−
+
−
ML{*fun inst_spec_tac ctrms = +
−
  EVERY' (map (dtac o inst_spec) ctrms)*}+
−
+
−
text {*+
−
  This tactic allows us to instantiate in the following proof the +
−
  three quantifiers in the assumption. +
−
*}+
−
+
−
lemma +
−
  fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"+
−
  shows "\<forall>x y z. P x y z \<Longrightarrow> True"+
−
apply (tactic {* +
−
  inst_spec_tac  [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})+
−
txt {* +
−
  We obtain the goal state+
−
+
−
  \begin{minipage}{\textwidth}+
−
  @{subgoals} +
−
  \end{minipage}*}+
−
(*<*)oops(*>*)+
−
+
−
text {*+
−
  Now the complete tactic for proving the induction principles can +
−
  be implemented as follows:+
−
*}+
−
+
−
ML %linenosgray{*fun ind_tac defs prem insts =+
−
  EVERY1 [ObjectLogic.full_atomize_tac,+
−
          cut_facts_tac prem,+
−
          K (rewrite_goals_tac defs),+
−
          inst_spec_tac insts,+
−
          assume_tac]*}+
−
+
−
text {*+
−
  We have to give it as arguments the definitions, the premise (this premise+
−
  is @{text "even n"} in lemma @{thm [source] manual_ind_prin_even}) and the+
−
  instantiations. Compare this tactic with the manual for the lemma @{thm+
−
  [source] manual_ind_prin_even}: as you can see there is almost a one-to-one+
−
  correspondence between the \isacommand{apply}-script and the @{ML+
−
  ind_tac}. Two testcases for this tactic are:+
−
*}+
−
+
−
lemma automatic_ind_prin_even:+
−
assumes prem: "even z"+
−
shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"+
−
by (tactic {* ind_tac eo_defs @{thms prem} +
−
                    [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})+
−
+
−
lemma automatic_ind_prin_fresh:+
−
assumes prem: "fresh z za" +
−
shows "(\<And>a b. a \<noteq> b \<Longrightarrow> P a (Var b)) \<Longrightarrow> +
−
        (\<And>a t s. \<lbrakk>P a t; P a s\<rbrakk> \<Longrightarrow> P a (App t s)) \<Longrightarrow>+
−
        (\<And>a t. P a (Lam a t)) \<Longrightarrow> +
−
        (\<And>a b t. \<lbrakk>a \<noteq> b; P a t\<rbrakk> \<Longrightarrow> P a (Lam b t)) \<Longrightarrow> P z za"+
−
by (tactic {* ind_tac @{thms fresh_def} @{thms prem} +
−
                    [@{cterm "P::string\<Rightarrow>trm\<Rightarrow>bool"}] *})+
−
+
−
+
−
text {*+
−
  Let us have a closer look at the first proved theorem:+
−
+
−
  \begin{isabelle}+
−
  \isacommand{thm}~@{thm [source] automatic_ind_prin_even}\\+
−
  @{text "> "}~@{thm automatic_ind_prin_even}+
−
  \end{isabelle}+
−
+
−
  The variables @{text "z"}, @{text "P"} and @{text "Q"} are schematic+
−
  variables (since they are not quantified in the lemma). These schematic+
−
  variables are needed so that they can be instantiated by the user later+
−
  on. We have to take care to also generate these schematic variables when+
−
  generating the goals for the induction principles. While the tactic for+
−
  proving the induction principles is relatively simple, it will be a bit+
−
  of work to construct the goals from the introduction rules the user+
−
  provides. In general we have to construct for each predicate @{text "pred"}+
−
  a goal of the form+
−
+
−
  @{text [display] +
−
  "pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}+
−
+
−
  where the predicates @{text preds} are replaced in the introduction +
−
  rules by new distinct variables @{text "?Ps"}.+
−
  We also need to generate fresh arguments @{text "?zs"} for the predicate +
−
  @{text "pred"} and the @{text "?P"} in the conclusion. Note +
−
  that the  @{text "?Ps"}  and @{text "?zs"} need to be+
−
  schematic variables that can be instantiated by the user.+
−
+
−
  We generate these goals in two steps. The first function expects that the+
−
  introduction rules are already appropriately substituted. The argument+
−
  @{text "srules"} stands for these substituted rules; @{text cnewpreds} are+
−
  the certified terms coresponding to the variables @{text "?Ps"}; @{text+
−
  "pred"} is the predicate for which we prove the induction principle;+
−
  @{text "newpred"} is its replacement and @{text "arg_tys"} are the argument+
−
  types of this predicate.+
−
*}+
−
+
−
ML %linenosgray{*fun prove_ind lthy defs srules cnewpreds ((pred, newpred), arg_tys) =+
−
let+
−
  val zs = replicate (length arg_tys) "z"+
−
  val (newargnames, lthy') = Variable.variant_fixes zs lthy;+
−
  val newargs = map Free (newargnames ~~ arg_tys)+
−
  +
−
  val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))+
−
  val goal = Logic.list_implies +
−
         (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))+
−
in+
−
  Goal.prove lthy' [] [prem] goal+
−
      (fn {prems, ...} => ind_tac defs prems cnewpreds)+
−
  |> singleton (ProofContext.export lthy' lthy)+
−
end *}+
−
+
−
text {* +
−
  In Line 3 we produce names @{text "zs"} for each type in the +
−
  argument type list. Line 4 makes these names unique and declares them as +
−
  \emph{free} (but fixed) variables in the local theory @{text "lthy'"}. +
−
  That means they are not (yet) schematic variables.+
−
  In Line 5 we construct the terms corresponding to these variables. +
−
  The variables are applied to the predicate in Line 7 (this corresponds+
−
  to the first premise @{text "pred zs"} of the induction principle). +
−
  In Line 8 and 9, we first construct the term  @{text "P zs"} +
−
  and then add the (substituted) introduction rules as premises. In case that+
−
  no introduction rules are given, the conclusion of this implication needs+
−
  to be wrapped inside a @{term Trueprop}, otherwise the Isabelle's goal+
−
  mechanism will fail. +
−
+
−
  In Line 11 we set up the goal to be proved; in the next line we call the+
−
  tactic for proving the induction principle. As mentioned before, this tactic+
−
  expects the definitions, the premise and the (certified) predicates with+
−
  which the introduction rules have been substituted. The code in these two+
−
  lines will return a theorem. However, it is a theorem+
−
  proved inside the local theory @{text "lthy'"}, where the variables @{text+
−
  "zs"} are fixed, but free (see Line 4). By exporting this theorem from @{text+
−
  "lthy'"} (which contains the @{text "zs"} as free variables) to @{text+
−
  "lthy"} (which does not), we obtain the desired schematic variables @{text "?zs"}.+
−
  A testcase for this function is+
−
*}+
−
+
−
local_setup %gray{* fn lthy =>+
−
let+
−
  val newpreds = [@{term "P::nat\<Rightarrow>bool"}, @{term "Q::nat\<Rightarrow>bool"}]+
−
  val cnewpreds = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]+
−
  val srules =  map (subst_free (eo_preds ~~ newpreds)) eo_rules+
−
  val newpred = @{term "P::nat\<Rightarrow>bool"}+
−
  val intro = +
−
       prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys)+
−
in+
−
  warning (str_of_thm lthy intro); lthy+
−
end *}+
−
+
−
text {*+
−
  This prints out the theorem:+
−
+
−
  @{text [display]+
−
  " \<lbrakk>even ?z; P 0; \<And>n. Q n \<Longrightarrow> P (Suc n); \<And>n. P n \<Longrightarrow> Q (Suc n)\<rbrakk> \<Longrightarrow> P ?z"}+
−
+
−
  The export from @{text lthy'} to @{text lthy} in Line 13 above +
−
  has correctly turned the free, but fixed, @{text "z"} into a schematic +
−
  variable @{text "?z"}; the variables @{text "P"} and @{text "Q"} are not yet+
−
  schematic. +
−
+
−
  We still have to produce the new predicates with which the introduction+
−
  rules are substituted and iterate @{ML prove_ind} over all+
−
  predicates. This is what the second function does: +
−
*}+
−
+
−
ML %linenosgray{*fun inds rules defs preds arg_tyss lthy  =+
−
let+
−
  val Ps = replicate (length preds) "P"+
−
  val (newprednames, lthy') = Variable.variant_fixes Ps lthy+
−
  +
−
  val thy = ProofContext.theory_of lthy'+
−
+
−
  val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss+
−
  val newpreds = map Free (newprednames ~~ tyss')+
−
  val cnewpreds = map (cterm_of thy) newpreds+
−
  val srules = map (subst_free (preds ~~ newpreds)) rules+
−
+
−
in+
−
  map (prove_ind lthy' defs srules cnewpreds) +
−
        (preds ~~ newpreds ~~ arg_tyss)+
−
          |> ProofContext.export lthy' lthy+
−
end*}+
−
+
−
text {*+
−
  In Line 3, we generate a string @{text [quotes] "P"} for each predicate. +
−
  In Line 4, we use the same trick as in the previous function, that is making the +
−
  @{text "Ps"} fresh and declaring them as fixed, but free, in+
−
  the new local theory @{text "lthy'"}. From the local theory we extract+
−
  the ambient theory in Line 6. We need this theory in order to certify +
−
  the new predicates. In Line 8, we construct the types of these new predicates+
−
  using the given argument types. Next we turn them into terms and subsequently+
−
  certify them (Line 9 and 10). We can now produce the substituted introduction rules +
−
  (Line 11) using the function @{ML subst_free}. Line 14 and 15 just iterate +
−
  the proofs for all predicates.+
−
  From this we obtain a list of theorems. Finally we need to export the +
−
  fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"} +
−
  (Line 16).+
−
+
−
  A testcase for this function is+
−
*}+
−
+
−
local_setup %gray {* fn lthy =>+
−
let +
−
  val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy+
−
in+
−
  warning (str_of_thms lthy ind_thms); lthy+
−
end *}+
−
+
−
+
−
text {*+
−
  which prints out+
−
+
−
@{text [display]+
−
"even ?z \<Longrightarrow> ?P1 0 \<Longrightarrow> +
−
 (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?P1 ?z,+
−
odd ?z \<Longrightarrow> ?P1 0 \<Longrightarrow>+
−
 (\<And>m. ?Pa1 m \<Longrightarrow> ?P1 (Suc m)) \<Longrightarrow> (\<And>m. ?P1 m \<Longrightarrow> ?Pa1 (Suc m)) \<Longrightarrow> ?Pa1 ?z"}+
−
+
−
  Note that now both, the @{text "?Ps"} and the @{text "?zs"}, are schematic+
−
  variables. The numbers attached to these variables have been introduced by +
−
  the pretty-printer and are \emph{not} important for the user. +
−
+
−
  This completes the code for the induction principles. The final peice+
−
  of reasoning infrastructure we need are the introduction rules. +
−
*}+
−
+
−
subsection {* Introduction Rules *}+
−
+
−
text {*+
−
  The proofs of the introduction rules are quite a bit+
−
  more involved than the ones for the induction principles. +
−
  To ease somewhat our work here, we use the following two helper+
−
  functions.+
−
+
−
*}+
−
+
−
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})*}+
−
+
−
text {* +
−
  To see what these functions do, let us suppose whe have the following three+
−
  theorems. +
−
*}+
−
+
−
lemma all_elims_test:+
−
  fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"+
−
  shows "\<forall>x y z. P x y z" sorry+
−
+
−
lemma imp_elims_test:+
−
  shows "A \<longrightarrow> B \<longrightarrow> C" sorry+
−
+
−
lemma imp_elims_test':+
−
  shows "A" "B" sorry+
−
+
−
text {*+
−
  The function @{ML all_elims} takes a list of (certified) terms and instantiates+
−
  theorems of the form @{thm [source] all_elims_test}. For example we can instantiate+
−
  the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:+
−
+
−
  @{ML_response_fake [display, gray]+
−
"let+
−
  val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]+
−
  val new_thm = all_elims ctrms @{thm all_elims_test}+
−
in+
−
  warning (str_of_thm_no_vars @{context} new_thm)+
−
end"+
−
  "P a b c"}+
−
+
−
  Similarly, the function @{ML imp_elims} eliminates preconditions from implications. +
−
  For example we can eliminate the preconditions @{text "A"} and @{text "B"} from+
−
  @{thm [source] imp_elims_test}:+
−
+
−
  @{ML_response_fake [display, gray]+
−
"warning (str_of_thm_no_vars @{context} +
−
            (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"+
−
  "C"}+
−
+
−
  To explain the proof for the introduction rule, our running example will be+
−
  the rule:+
−
+
−
  \begin{isabelle}+
−
  @{prop "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}+
−
  \end{isabelle}+
−
  +
−
  for freshness of applications. We set up the proof as follows:+
−
*}+
−
+
−
lemma fresh_App:+
−
  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"+
−
(*<*)oops(*>*)+
−
+
−
text {*+
−
  The first step will be to expand the definitions of freshness+
−
  and then introduce quantifiers and implications. For this we+
−
  will use the tactic+
−
*}+
−
+
−
ML{*fun expand_tac defs =+
−
  ObjectLogic.rulify_tac 1+
−
  THEN rewrite_goals_tac defs+
−
  THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}+
−
+
−
text {*+
−
  The first step of ``rulifying'' the lemma will turn out important+
−
  later on. Applying this tactic +
−
*}+
−
+
−
(*<*)+
−
lemma fresh_App:+
−
  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"+
−
(*>*)+
−
apply(tactic {* expand_tac @{thms fresh_def} *})+
−
+
−
txt {*+
−
  we end up in the goal state+
−
+
−
  \begin{isabelle}+
−
  @{subgoals [display]}+
−
  \end{isabelle}+
−
+
−
  As you can see, there are parameters (namely @{text "a"}, @{text "b"} +
−
  and @{text "t"}) which come from the introduction rule and parameters+
−
  (in the case above only @{text "fresh"}) which come from the universal+
−
  quantification in the definition @{term "fresh a (App t s)"}.+
−
  Similarly, there are preconditions+
−
  that come from the premises of the rule and premises from the+
−
  definition. We need to treat these +
−
  parameters and preconditions differently. In the code below+
−
  we will therefore separate them into @{text "params1"} and @{text params2},+
−
  respectively @{text "prems1"} and @{text "prems2"}. To do this +
−
  separation, it is best to open a subproof with the tactic +
−
  @{ML SUBPROOF}, since this tactic provides us+
−
  with the parameters (as list of @{ML_type cterm}s) and the premises+
−
  (as list of @{ML_type thm}s). The problem we have to overcome +
−
  with @{ML SUBPROOF} is that this tactic always expects us to completely +
−
  discharge with the goal (see Section ???). This is inconvenient for+
−
  our gradual explanation of the proof. To circumvent this inconvenience+
−
  we use the following modified tactic: +
−
*}+
−
(*<*)oops(*>*)+
−
ML{*fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac*}+
−
+
−
text {*+
−
  If the tactic inside @{ML SUBPROOF} fails, then the overall tactic will+
−
  still succeed. With this testing tactic, we can gradually implement+
−
  all necessary proof steps.+
−
*}+
−
+
−
text_raw {*+
−
\begin{figure}[t]+
−
\begin{minipage}{\textwidth}+
−
\begin{isabelle}+
−
*}+
−
ML{*fun chop_print params1 params2 prems1 prems2 ctxt =+
−
let +
−
  val s = ["Params1 from the rule:", str_of_cterms ctxt params1] +
−
        @ ["Params2 from the predicate:", str_of_cterms ctxt params2] +
−
        @ ["Prems1 from the rule:"] @ (map (str_of_thm ctxt) prems1) +
−
        @ ["Prems2 from the predicate:"] @ (map (str_of_thm ctxt) prems2) +
−
in +
−
  s |> separate "\n"+
−
    |> implode+
−
    |> warning+
−
end*}+
−
text_raw{*+
−
\end{isabelle}+
−
\end{minipage}+
−
\caption{FIXME\label{fig:chopprint}}+
−
\end{figure}+
−
*}+
−
+
−
text {*+
−
  First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}+
−
  from @{text "params"} and @{text "prems"}, respectively. To see what is+
−
  going in our example, we will print out the values using the printing+
−
  function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will+
−
  supply us the @{text "params"} and @{text "prems"} as lists, we can +
−
  separate them using the function @{ML chop}. +
−
*}+
−
+
−
ML{*fun chop_test_tac preds rules =+
−
  SUBPROOF_test (fn {params, prems, context, ...} =>+
−
  let+
−
    val (params1, params2) = chop (length params - length preds) params+
−
    val (prems1, prems2) = chop (length prems - length rules) prems+
−
  in+
−
    chop_print params1 params2 prems1 prems2 context; no_tac+
−
  end) *}+
−
+
−
text {* +
−
  For the separation we can rely on that Isabelle deterministically +
−
  produces parameter and premises in a goal state. The last parameters+
−
  that were introduced, come from the quantifications in the definitions.+
−
  Therefore we only have to subtract the number of predicates (in this+
−
  case only @{text "1"} from the lenghts of all parameters. Similarly+
−
  with the @{text "prems"}. The last premises in the goal state must+
−
  come from unfolding of the conclusion. So we can just subtract+
−
  the number of rules from the number of all premises. Applying+
−
  this tactic in our example +
−
*}+
−
+
−
(*<*)+
−
lemma fresh_App:+
−
  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"+
−
apply(tactic {* expand_tac @{thms fresh_def} *})+
−
(*>*)+
−
apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} *})+
−
(*<*)oops(*>*)+
−
+
−
text {*+
−
  gives+
−
+
−
  \begin{isabelle}+
−
  @{text "Params1 from the rule:"}\\+
−
  @{text "a, b, t"}\\+
−
  @{text "Params2 from the predicate:"}\\+
−
  @{text "fresh"}\\+
−
  @{text "Prems1 from the rule:"}\\+
−
  @{term "a \<noteq> b"}\\+
−
  @{text [break]+
−
"\<forall>fresh.+
−
      (\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>+
−
      (\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>+
−
      (\<forall>a t. fresh a (Lam a t)) \<longrightarrow> +
−
      (\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}\\+
−
   @{text "Prems2 from the predicate:"}\\+
−
   @{term "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}\\+
−
   @{term "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}\\+
−
   @{term "\<forall>a t. fresh a (Lam a t)"}\\+
−
   @{term "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)"}+
−
  \end{isabelle}+
−
+
−
+
−
  We now have to select from @{text prems2} the premise +
−
  that corresponds to the introduction rule we prove, namely:+
−
+
−
  @{term [display] "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}+
−
+
−
  To use this premise with @{ML rtac}, we need to instantiate its +
−
  quantifiers (with @{text params1}) and transform it into a +
−
  introduction rule (using @{ML "ObjectLogic.rulify"}. +
−
  So we can modify the subproof as follows:+
−
*}+
−
+
−
ML{*fun apply_prem_tac i preds rules =+
−
  SUBPROOF_test (fn {params, prems, context, ...} =>+
−
  let+
−
    val (params1, params2) = chop (length params - length preds) params+
−
    val (prems1, prems2) = chop (length prems - length rules) prems+
−
  in+
−
    rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1+
−
    THEN print_tac ""+
−
    THEN no_tac+
−
  end) *}+
−
+
−
text {* and apply it with *}+
−
+
−
(*<*)+
−
lemma fresh_App:+
−
  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"+
−
apply(tactic {* expand_tac @{thms fresh_def} *})+
−
(*>*)+
−
apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} *})+
−
(*<*)oops(*>*)+
−
+
−
text {*+
−
  Since we print out the goal state after the @{ML rtac} we can see+
−
  the goal state has the two subgoals+
−
+
−
  \begin{isabelle}+
−
  @{text "1."}~@{prop "a \<noteq> b"}\\+
−
  @{text "2."}~@{prop "fresh a t"}+
−
  \end{isabelle}+
−
+
−
  where the first comes from a non-recursive precondition of the rule+
−
  and the second comes from a recursive precondition. The first kind+
−
  can be solved immediately by @{text "prems1"}. The second kind+
−
  needs more work. It can be solved with the other premise in @{text "prems1"},+
−
  namely+
−
+
−
  @{term [break,display]+
−
  "\<forall>fresh.+
−
      (\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>+
−
      (\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>+
−
      (\<forall>a t. fresh a (Lam a t)) \<longrightarrow> +
−
      (\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}+
−
+
−
  but we have to instantiate it appropriately. These instantiations+
−
  come from @{text "params1"} and @{text "prems2"}. We can determine+
−
  whether we are in the simple or complicated case by checking whether+
−
  the topmost connective is @{text "\<forall>"}. The premises in the simple+
−
  case cannot have such a quantification, since in the first step +
−
  of @{ML "expand_tac"} was the ``rulification'' of the lemma. So +
−
  we can implement the following function+
−
*}+
−
+
−
ML{*fun prepare_prem params2 prems2 prem =  +
−
  rtac (case prop_of prem of+
−
           _ $ (Const (@{const_name All}, _) $ _) =>+
−
                 prem |> all_elims params2 +
−
                      |> imp_elims prems2+
−
         | _ => prem) *}+
−
+
−
text {* +
−
  which either applies the premise outright or if it had an+
−
  outermost universial quantification, instantiates it first with +
−
  @{text "params1"} and then @{text "prems1"}. The following tactic +
−
  will therefore prove the lemma.+
−
*}+
−
+
−
ML{*fun prove_intro_tac i preds rules =+
−
  SUBPROOF (fn {params, prems, context, ...} =>+
−
  let+
−
    val (params1, params2) = chop (length params - length preds) params+
−
    val (prems1, prems2) = chop (length prems - length rules) prems+
−
  in+
−
    rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1+
−
    THEN EVERY1 (map (prepare_prem params2 prems2) prems1)+
−
  end) *}+
−
+
−
text {*+
−
  We can complete the proof of the introduction rule now as follows:+
−
*}+
−
+
−
(*<*)+
−
lemma fresh_App:+
−
  shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"+
−
apply(tactic {* expand_tac @{thms fresh_def} *})+
−
(*>*)+
−
apply(tactic {* prove_intro_tac 3 [fresh_pred] fresh_rules @{context} 1 *})+
−
done+
−
+
−
text {* +
−
  Unfortunately, not everything is done yet.+
−
*}+
−
+
−
lemma accpartI:+
−
  shows "\<And>x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"+
−
apply(tactic {* expand_tac @{thms accpart_def} *})+
−
apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} *})+
−
apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} *})+
−
+
−
txt {*+
−
  +
−
  @{subgoals [display]}+
−
+
−
  \begin{isabelle}+
−
  @{text "Params1 from the rule:"}\\+
−
  @{text "x"}\\+
−
  @{text "Params2 from the predicate:"}\\+
−
  @{text "P"}\\+
−
  @{text "Prems1 from the rule:"}\\+
−
  @{text "R ?y x \<Longrightarrow> \<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P ?y"}\\+
−
  @{text "Prems2 from the predicate:"}\\+
−
  @{term "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x"}\\+
−
  \end{isabelle}+
−
+
−
*}+
−
(*<*)oops(*>*)+
−
+
−
+
−
ML{*fun prepare_prem params2 prems2 ctxt prem =  +
−
  SUBPROOF (fn {prems, ...} =>+
−
  let+
−
    val prem' = prems MRS prem+
−
  in +
−
    rtac (case prop_of prem' of+
−
           _ $ (Const (@{const_name All}, _) $ _) =>+
−
                 prem' |> all_elims params2 +
−
                       |> imp_elims prems2+
−
         | _ => prem') 1+
−
  end) ctxt *}+
−
+
−
ML{*fun prove_intro_tac i preds rules =+
−
  SUBPROOF (fn {params, prems, context, ...} =>+
−
  let+
−
    val (params1, params2) = chop (length params - length preds) params+
−
    val (prems1, prems2) = chop (length prems - length rules) prems+
−
  in+
−
    rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1+
−
    THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1)+
−
  end) *}+
−
+
−
lemma accpartI:+
−
  shows "\<And>x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"+
−
apply(tactic {* expand_tac @{thms accpart_def} *})+
−
apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *})+
−
done+
−
+
−
+
−
+
−
text {*+
−
+
−
*}+
−
+
−
ML{*+
−
fun intros_tac defs rules preds i ctxt =+
−
  EVERY1 [ObjectLogic.rulify_tac,+
−
          K (rewrite_goals_tac defs),+
−
          REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),+
−
          prove_intro_tac i preds rules ctxt]*}+
−
+
−
text {*+
−
  A test case+
−
*}+
−
+
−
ML{*fun intros_tac_test ctxt i =+
−
  intros_tac eo_defs eo_rules eo_preds i ctxt *}+
−
+
−
lemma intro0:+
−
  shows "even 0"+
−
apply(tactic {* intros_tac_test @{context} 0 *})+
−
done+
−
+
−
lemma intro1:+
−
  shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"+
−
apply(tactic {* intros_tac_test @{context} 1 *})+
−
done+
−
+
−
lemma intro2:+
−
  shows "\<And>m. even m \<Longrightarrow> odd (Suc m)"+
−
apply(tactic {* intros_tac_test @{context} 2 *})+
−
done+
−
+
−
ML{*fun intros rules preds defs lthy = +
−
let+
−
  fun prove_intro (i, goal) =+
−
    Goal.prove lthy [] [] goal+
−
      (fn {context, ...} => intros_tac defs rules preds i context)+
−
in+
−
  map_index prove_intro rules+
−
end*}+
−
+
−
text {* main internal function *}+
−
+
−
ML %linenosgray{*fun add_inductive 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') = defns rules preds prednames syns tyss lthy      +
−
  val ind_rules = inds rules defs preds tyss lthy' 	+
−
  val intro_rules = intros 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 "intros"}), []), maps snd intross)) +
−
    |>> snd +
−
    ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>+
−
         ((Binding.qualify false (Binding.name_of R) (@{binding "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 add_inductive_cmd pred_specs rule_specs lthy =+
−
let+
−
  val ((pred_specs', rule_specs'), _) = +
−
         Specification.read_spec pred_specs rule_specs lthy+
−
in+
−
  add_inductive pred_specs' rule_specs' lthy+
−
end*} +
−
+
−
ML{*val spec_parser = +
−
   OuterParse.fixes -- +
−
   Scan.optional +
−
     (OuterParse.$$$ "where" |--+
−
        OuterParse.!!! +
−
          (OuterParse.enum1 "|" +
−
             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}+
−
+
−
ML{*val specification =+
−
  spec_parser >>+
−
    (fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*}+
−
+
−
ML{*val _ = OuterSyntax.local_theory "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)+
−
  \item say that no conformity test is done+
−
  \item exercise about strong induction principles+
−
  \item exercise about the test for the intro rules+
−
  \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+
−