theory Ind_Code

imports Ind_General_Scheme "../First_Steps" 

begin

section \<open>The Gory Details\label{sec:code}\<close> 

text \<open>

  As mentioned before the code falls roughly into three parts: the code that deals

  with the definitions, with the induction principles and with the introduction

  rules. In addition there are some administrative functions that string everything 

  together.

\<close>

subsection \<open>Definitions\<close>

text \<open>

  We first have to produce for each predicate the user specifies an appropriate

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

  @{ML_ind define in Local_Theory}. The wrapper takes a predicate name, a syntax

  annotation and a term representing the right-hand side of the definition.

\<close>

ML %linenosgray\<open>fun make_defn ((predname, mx), trm) lthy =

let 

  val arg = ((predname, mx), (Binding.empty_atts, trm))

  val ((_, (_ , thm)), lthy') = Local_Theory.define arg lthy

in 

  (thm, lthy') 

end\<close>

text \<open>

  It returns the definition (as a theorem) and the local theory in which the

  definition has been made. We use @{ML_ind empty_atts in Binding} in Line 3, 

  since the definitions for our inductive predicates are not meant to be seen 

  by the user and therefore do not need to have any theorem attributes. 

  The next two functions construct the right-hand sides of the definitions, 

  which are terms whose general form is:

  @{text [display] "\<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}

  When constructing these terms, the variables \<open>zs\<close> need to be chosen so 

  that they do not occur in the \<open>orules\<close> and also be distinct from the 

  \<open>preds\<close>.

  The first function, named \<open>defn_aux\<close>, constructs the term for one

  particular predicate (the argument \<open>pred\<close> in the code below). The

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

  argument types given in \<open>arg_tys\<close>. The other arguments of the

  function are the \<open>orules\<close> and all the \<open>preds\<close>.

\<close>

ML %linenosgray\<open>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\<close>

text \<open>

  The function \<open>mk_all\<close> in Line 3 is just a helper function for constructing 

  universal quantifications. The code in Lines 5 to 9 produces the fresh \<open>zs\<close>. 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 \<open>orules\<close> (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 \<open>orules\<close> are prefixed (Line 12); in

  Line 13 we quantify over all predicates; and in line 14 we just abstract

  over all the \<open>zs\<close>, i.e., the fresh arguments of the

  predicate. A testcase for this function is

\<close>

local_setup %gray \<open>fn lthy =>

let

  val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys)

in

  pwriteln (pretty_term lthy def); lthy

end\<close>

text \<open>

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

  The testcase calls @{ML defn_aux} for the predicate \<open>even\<close> 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

\<close>

local_setup %gray \<open>fn lthy =>

let

  val arg = (fresh_pred, fresh_arg_tys)

  val def = defn_aux lthy fresh_orules [fresh_pred] arg

in

  pwriteln (pretty_term lthy def); lthy

end\<close>

text \<open>

  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 \<open>defns\<close>, has to iterate the function

  @{ML defn_aux} over all predicates. The argument \<open>preds\<close> is again

  the list of predicates as @{ML_type term}s; the argument \<open>prednames\<close> is the list of binding names of the predicates; \<open>mxs\<close> 

  are the list of syntax, or mixfix, annotations for the predicates; 

  \<open>arg_tyss\<close> is the list of argument-type-lists.

\<close>

ML %linenosgray\<open>fun defns rules preds prednames mxs arg_typss lthy =

let

  val orules = map (Object_Logic.atomize_term lthy) rules

  val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) 

in

  fold_map make_defn (prednames ~~ mxs ~~ defs) lthy

end\<close>

text \<open>

  The user will state the introduction rules using meta-implications and

  into the object logic (since definitions cannot be stated with

  the function is a list of theorems and a local theory (the theorems are

  registered with the local theory). A testcase for this function is

\<close>

local_setup %gray \<open>fn lthy =>

let

  val (defs, lthy') = 

    defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy

in

  pwriteln (pretty_thms_no_vars lthy' defs); lthy

end\<close>

text \<open>

  where we feed into the function all parameters corresponding to

  the \<open>even\<close>/\<open>odd\<close> 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 \<open>lthy\<close> 

  (not the modified \<open>lthy'\<close>). 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 

  \<open>even\<close> and \<open>odd\<close>. We want to avoid this here.

  This completes the code for introducing the definitions. Next we deal with

  the induction principles. 

\<close>

subsection \<open>Induction Principles\<close>

text \<open>

  Recall that the manual proof for the induction principle 

  of \<open>even\<close> was:

\<close>

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

  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. 

\<close>

ML %grayML\<open>fun inst_spec ctrm =

let

  val cty = Thm.ctyp_of_cterm ctrm

in 

  Thm.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec} 

end\<close>

text \<open>

  This helper function uses the function @{ML_ind instantiate' in Thm}

  and instantiates the \<open>?x\<close> in the theorem @{thm spec} with a given

  @{ML_type cterm}. We call this helper function in the following

  tactic.\label{fun:instspectac}.

\<close>

ML %grayML\<open>fun inst_spec_tac ctxt ctrms = 

  EVERY' (map (dresolve_tac ctxt o single o inst_spec) ctrms)\<close>

text \<open>

  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. 

\<close>

lemma 

fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"

shows "\<forall>x y z. P x y z \<Longrightarrow> True"

apply (tactic \<open>

  inst_spec_tac @{context} [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1\<close>)

txt \<open>

  We obtain the goal state

  \begin{minipage}{\textwidth}

  @{subgoals} 

  \end{minipage}\<close>

(*<*)oops(*>*)

text \<open>

  The complete tactic for proving the induction principles can now

  be implemented as follows:

\<close>

ML %linenosgray\<open>fun ind_tac ctxt defs prem insts =

  EVERY1 [Object_Logic.full_atomize_tac ctxt,

          cut_facts_tac prem,

          rewrite_goal_tac ctxt defs,

          inst_spec_tac ctxt insts,

          assume_tac ctxt]\<close>

text \<open>

  We have to give it as arguments the definitions, the premise (a list of

  formulae) and the instantiations. The premise is \<open>even n\<close> in lemma

  @{thm [source] manual_ind_prin_even} shown above; in our code it will always be a list

  consisting of a single formula. Compare this tactic with the manual proof

  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}. We first rewrite the goal to use only object connectives (Line 2),

  "cut in" the premise (Line 3), unfold the definitions (Line 4), instantiate

  the assumptions of the goal (Line 5) and then conclude with @{ML assume_tac}.

  Two testcases for this tactic are:

\<close>

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 \<open>ind_tac @{context} eo_defs @{thms prem} 

                    [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]\<close>)

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 \<open>ind_tac @{context} @{thms fresh_def} @{thms prem} 

                          [@{cterm "P::string\<Rightarrow>trm\<Rightarrow>bool"}]\<close>)

text \<open>

  While the tactic for proving the induction principles is relatively simple,

  it will be a bit more 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}\\

  \<open>> \<close>~@{thm automatic_ind_prin_even}

  \end{isabelle}

  The variables \<open>z\<close>, \<open>P\<close> and \<open>Q\<close> are schematic

  variables (since they are not quantified in the lemma). These 

  variables must be schematic, otherwise they cannot be instantiated 

  by the user. To generate these schematic variables we use a common trick

  in Isabelle programming: we first declare them as \emph{free}, 

  \emph{but fixed}, and then use the infrastructure to turn them into 

  schematic variables.

  In general we have to construct for each predicate \<open>pred\<close> a goal 

  of the form

  @{text [display] 

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

  where the predicates \<open>preds\<close> are replaced in \<open>rules\<close> by new 

  distinct variables \<open>?Ps\<close>. We also need to generate fresh arguments 

  \<open>?zs\<close> for the predicate  \<open>pred\<close> and the \<open>?P\<close> in 

  the conclusion. 

  We generate these goals in two steps. The first function, named \<open>prove_ind\<close>, 

  expects that the introduction rules are already appropriately substituted. The argument

  \<open>srules\<close> stands for these substituted rules; \<open>cnewpreds\<close> are

  the certified terms coresponding to the variables \<open>?Ps\<close>; \<open>pred\<close> is the predicate for which we prove the induction principle;

  \<open>newpred\<close> is its replacement and \<open>arg_tys\<close> are the argument

  types of this predicate.

\<close>

ML %linenosgray\<open>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, context, ...} => ind_tac context defs prems cnewpreds)

  |> singleton (Proof_Context.export lthy' lthy)

end\<close>

text \<open>

  In Line 3 we produce names \<open>zs\<close> for each type in the 

  argument type list. Line 4 makes these names unique and declares them as 

  free, but fixed, variables in the local theory \<open>lthy'\<close>. 

  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 \<open>pred zs\<close> of the induction principle). 

  In Line 8 and 9, we first construct the term  \<open>P zs\<close> 

  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 using the function @{ML_ind 

  prove in Goal}; 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

  \<open>lthy'\<close>, where the variables \<open>zs\<close> are free, but fixed (see

  Line 4). By exporting this theorem from \<open>lthy'\<close> (which contains the

  \<open>zs\<close> as free variables) to \<open>lthy\<close> (which does not), we

  obtain the desired schematic variables \<open>?zs\<close>.  A testcase for this

  function is

\<close>

local_setup %gray \<open>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

  pwriteln (pretty_thm lthy intro); lthy

end\<close>

text \<open>

  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 \<open>lthy'\<close> to \<open>lthy\<close> in Line 13 above 

  has correctly turned the free, but fixed, \<open>z\<close> into a schematic 

  variable \<open>?z\<close>; the variables \<open>P\<close> and \<open>Q\<close> 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 \<open>inds\<close> does. 

\<close>

ML %linenosgray\<open>fun inds rules defs preds arg_tyss lthy  =

let

  val Ps = replicate (length preds) "P"

  val (newprednames, lthy') = Variable.variant_fixes Ps lthy

  val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss

  val newpreds = map Free (newprednames ~~ tyss')

  val cnewpreds = map (Thm.cterm_of lthy') newpreds

  val srules = map (subst_free (preds ~~ newpreds)) rules

in

  map (prove_ind lthy' defs srules cnewpreds) 

        (preds ~~ newpreds ~~ arg_tyss)

          |> Proof_Context.export lthy' lthy

end\<close>

text \<open>

  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 

  \<open>Ps\<close> fresh and declaring them as free, but fixed, in

  the new local theory \<open>lthy'\<close>. In Line 6, we construct the types of these new predicates

  using the given argument types. Next we turn them into terms and subsequently

  certify them (Line 7 and 8). We can now produce the substituted introduction rules 

  (Line 9) using the function @{ML_ind subst_free in Term}. Line 12 and 13 just iterate 

  the proofs for all predicates.

  From this we obtain a list of theorems. Finally we need to export the 

  fixed variables \<open>Ps\<close> to obtain the schematic variables \<open>?Ps\<close> 

  (Line 14).

  A testcase for this function is

\<close>

local_setup %gray \<open>fn lthy =>

let 

  val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy

in

  pwriteln (pretty_thms lthy ind_thms); lthy

end\<close>

text \<open>

  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 \<open>?Ps\<close> and the \<open>?zs\<close>, 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. 

\<close>

subsection \<open>Introduction Rules\<close>

text \<open>

  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

  the introduction rule

  \begin{isabelle}

  @{prop "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"}

  \end{isabelle}

  about freshness for lambdas. In order to ease somewhat 

  our work here, we use the following two helper functions.

\<close>

ML %grayML\<open>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})\<close>

text \<open>

  To see what these functions do, let us suppose we have the following three