theory Ind_Code

imports "../Base" "../FirstSteps" Ind_General_Scheme 

begin

section {* The Gory Details\label{sec:code} *} 

text {*

*}

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

  actual 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, named @{text defn_aux}, constructs the term for one

  particular predicate (the argument @{text "pred"} in the code below). The

  number of arguments of this predicate is determined by the number of

  argument types given in @{text "arg_tys"}. The other arguments of the

  function are the @{text orules} and all the @{text "preds"}.

*}

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 @{text mk_all} 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 variables are applied to the predicate in 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 def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)

in

  warning (Syntax.string_of_term lthy def); lthy

end *}

text {*

  where we use the shorthands defined in Figure~\ref{fig:shorthands}.

  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 with the rules for 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, named @{text defns}, 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 binding names of the predicates; @{text syns} 

  are the list of syntax annotations for the predicates; @{text "arg_tyss"} is

  the list of argument-type-lists.

*}

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 function 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 {*

*}

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

*}

ML{*fun inst_spec_tac ctrms = 

  EVERY' (map (dtac o inst_spec) ctrms)*}

text {*

  This tactic expects a list of @{ML_type cterm}s. It allows us in the 

  proof below to instantiate 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 {*

  The complete tactic for proving the induction principles can now

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

*}

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

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

  @{text [display] 

  "pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}

  where the predicates @{text preds} are replaced in @{text 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 

  We generate these goals in two steps. The first function, named @{text prove_ind}, 

  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 

  That means they are not schematic variables (yet).

  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 preconditions. 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.\footnote{FIXME: check with 

  Stefan...is this so?} 

  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 free, but fixed (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 newpred = @{term "P::nat\<Rightarrow>bool"}

  val srules =  map (subst_free (eo_preds ~~ newpreds)) eo_rules

  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, named @{text inds} 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 free, but fixed, 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 {*

  Constructing the goals for the introduction rules is easy: they

  are just the rules given by the user. However, their proofs are 

  quite a bit more involved than the ones for the induction principles. 

  To explain the general method, our running example will be