theory Ind_Code

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

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.

*}

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

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

*}

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

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

  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

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

*}

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

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

*}

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

  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

*}

ML{*fun inst_spec_tac ctrms = 

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

text {*

*}

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

  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

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

text {*

  \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

  @{text [display] 

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

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

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

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

*}

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 

  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})*}