theory Ind_Code

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

begin

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

text {*

  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.

*}

subsection {* Definitions *}

text {*

  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 [index] define in LocalTheory}. 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, mx), trm) lthy =

let 

  val arg = ((predname, mx), (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 the

  definition has been made. In Line 4, @{ML [index] internalK in Thm} is a flag

  attached to the theorem (others possibile flags are @{ML [index] definitionK in Thm}

  and @{ML [index] 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.\footnote{FIXME: put in the section about theorems.} We

  also use @{ML [index] empty_binding in Attrib} 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. A testcase for this function is

*}

local_setup %gray {* fn lthy =>

let

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

  val (def, lthy') = make_defn arg lthy 

in

  writeln (string_of_thm_no_vars lthy' def); lthy'

end *}

text {*

  which introduces the definition @{thm My_True_def} 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}~@{thm [source] "My_True_def"}\\

  @{text ">"}~@{thm "My_True_def"}

  \end{isabelle}

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

  writeln (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 =>

 (writeln (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 iterate the function

  @{ML defn_aux} over all predicates. The argument @{text "preds"} is again

  the list of predicates as @{ML_type term}s; the argument @{text

  "prednames"} is the list of binding names of the predicates; @{text mxs} 

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

  @{text "arg_tyss"} is the list of argument-type-lists.

*}

ML %linenosgray{*fun defns rules preds prednames mxs 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 ~~ mxs ~~ 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 [index] atomize_term in ObjectLogic} 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 (the theorems are

  registered with the 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_mxs eo_arg_tyss lthy

in

  writeln (string_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 {*

  Recall that the manual proof for the induction principle 

  of @{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 following tactic, called @{text inst_spec_tac}\label{fun:instspectac}.

*}

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

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

  formulae) and the instantiations. The premise is @{text "even n"} in lemma

  @{thm [source] manual_ind_prin_even}; 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}. 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 {*

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

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

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

  the conclusion. 

  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 

  free, but fixed, variables in the local theory @{text "lthy'"}. 

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