theory Ind_Code

begin

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.

*}

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 

  These flags just classify theorems and have no significant meaning, except 

  for tools that, for example, find theorems in the theorem database. We also

*}

local_setup %gray {* fn lthy =>

let

  val arg = ((@{binding "MyTrue"}, NoSyn), @{term True})

in

  warning (str_of_thm_no_vars lthy' def); lthy'

end *}

text {*

  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"}.

  determined by the number of argument types given in @{text "arg_tys"}. 

  The other arguments are all the @{text "preds"} and the @{text "orules"}.

*}

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"}]

in

  warning (Syntax.string_of_term lthy def); lthy

end *}

text {*

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

  The second function for the definitions has to just iterate the function

  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.

*}

let

  val thy = ProofContext.theory_of lthy

  val orules = map (ObjectLogic.atomize_term thy) rules

in

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

  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') = 

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:

  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

  and @{text "odd"}.

  the induction principles. 

*}

text {*

  Recall that the proof of the induction principle 

  for @{text "even"} was:

*}

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:

*}

  EVERY1 [ObjectLogic.full_atomize_tac,

          cut_facts_tac prem,

          K (rewrite_goals_tac defs),

          inst_spec_tac insts,

          assume_tac]*}

text {*

*}

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"

text {*

  \begin{isabelle}

  \end{isabelle}

  @{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

  @{text "newpred"} is its replacement and @{text "arg_tys"} are the argument

  types of this predicate.

*}

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

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

  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 does not), we obtain the desired schematic variables @{text "?zs"}.

  A testcase for this function is

*}

local_setup %gray{* fn lthy =>

let

  val cnewpreds = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]

  val newpred = @{term "P::nat\<Rightarrow>bool"}

  val intro = 

in

  warning (str_of_thm lthy intro); lthy

text {*

  @{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"}

  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

  predicates. This is what the second function does: 

*}

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

        (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 

in

  warning (str_of_thms lthy ind_thms); lthy

end *}

text {*

  which prints out

@{text [display]

  Note that now both, the @{text "?Ps"} and the @{text "?zs"}, are schematic

*}

subsection {* Introduction Rules *}

text {*

  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: