theory Ind_Code

imports "../Base" "../FirstSteps" Simple_Inductive_Package Ind_Prelims

begin

section {* Code *}

text {*

  @{text [display] "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}

  @{text [display] "orule ::= \<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}

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

  @{text [display] "ind ::= \<And>zs. pred zs \<Longrightarrow> rules[preds::=Ps] \<Longrightarrow> P zs"}

  @{text [display] "oind ::= \<forall>zs. pred zs \<longrightarrow> orules[preds::=Ps] \<longrightarrow> P zs"}

  So we have @{text "pred zs"} and @{text "orules[preds::=Ps]"}; have to show

  @{text "P zs"}. Expanding @{text "pred zs"} gives @{text "\<forall>preds. orules \<longrightarrow> pred zs"}.

  Instantiating the @{text "preds"} with @{text "Ps"} gives

  @{text "orules[preds::=Ps] \<longrightarrow> P zs"}. So we can conclude with @{text "P zs"}.

  We have to show @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"};

  expanding the defs 

  @{text [display]

  "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>* \<longrightarrow>  (\<forall>preds. orules \<longrightarrow> pred ts"}

  so we have @{text "As"}, @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"},

  @{text "orules"}; and have to show @{text "pred ts"}

  the @{text "orules"} are of the form @{text "\<forall>xs. As \<longrightarrow> (\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>* \<longrightarrow> pred ts"}.

  using the @{text "As"} we ????

*}

text {*

  First we have to produce for each predicate its definitions of the form

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

  In order to make definitions, 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_defs ((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 possibilities 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 the definition does 

  not need to have any theorem attributes. A testcase for this function is

*}

local_setup %gray {* fn lthy =>

let

  val arg =  ((Binding.name "MyTrue", NoSyn), @{term True})

  val (def, lthy') = make_defs arg lthy 

in

  warning (str_of_thm lthy' def); lthy'

end *}

text {*

  which makes the definition @{prop "MyTrue \<equiv> True"} and then prints it out. 

  Since we are testing the function inside \isacommand{local\_setup}, i.e.~make

  changes to the ambient theory, we can query the definition using the usual

  command \isacommand{thm}:

  \begin{isabelle}

  \isacommand{thm}~@{text "MyTrue_def"}\\

  @{text "> MyTrue \<equiv> True"}

  \end{isabelle}

  The next two functions construct the terms we need for the definitions for

  our \isacommand{simple\_inductive} command. These 

  terms are of the form 

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

  The variables @{text "\<^raw:$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 constructs the term for one particular predicate, say

  @{text "pred"}; the number of arguments of this predicate is

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

  So it takes these two parameters as arguments. The other arguments are

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

*}

ML %linenosgray{*fun defs_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 in Line 3 is just a helper function for constructing universal

  quantifications. The code in Lines 5 to 9 produces the fresh @{text

  "\<^raw:$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 @{text "orules"} and the predicates;

  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 "\<^raw:$zs$>"}, i.e.~the fresh arguments of the

  predicate.

  A testcase for this function is

*}

local_setup %gray{* fn lthy =>

let

  val orules = [@{prop "even 0"},

                @{prop "\<forall>n::nat. odd n \<longrightarrow> even (Suc n)"},

                @{prop "\<forall>n::nat. even n \<longrightarrow> odd (Suc n)"}] 

  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}, @{term "z::nat"}]

  val pred = @{term "even::nat\<Rightarrow>bool"}

  val arg_tys = [@{typ "nat"}]

  val def = defs_aux lthy orules preds (pred, arg_tys)

in

  warning (Syntax.string_of_term lthy def); lthy

end *}

text {*

  It constructs the left-hand side for the definition of @{text "even"}. So we obtain 

  as printout the term

  @{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 main function for the definitions now has to just iterate the function

  @{ML defs_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 names of the predicates; @{text "arg_tyss"} is

  the list of argument-type-lists for each predicate.

*}

ML %linenosgray{*fun definitions 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 (defs_aux lthy orules preds) (preds ~~ arg_typss) 

in

  fold_map make_defs (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 defs_aux} in Line 5 produces all left-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 rules = [@{prop "even 0"},

               @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},

               @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 

  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]

  val prednames = [Binding.name "even", Binding.name "odd"] 

  val syns = [NoSyn, NoSyn] 

  val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]

  val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy

in

  warning (str_of_thms 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:

  \begin{isabelle}

  \isacommand{thm}~@{text "even_def odd_def"}\\

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

  \end{isabelle}

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

  the induction principles. Recall that the proof of the induction principle 

  for @{text "even"} was:

*}

lemma man_ind_principle: 

assumes prems: "even n"

shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

apply(atomize (full))

apply(cut_tac prems)

apply(unfold even_def)

apply(drule spec[where x=P])

apply(drule spec[where x=Q])

apply(assumption)

done

text {* 

  The code for such induction principles has to accomplish two tasks: 

  constructing the induction principles from the given introduction

  rules and then automatically generating a proof of 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}. Together with the tactic

*}

ML{*fun inst_spec_tac ctrms = 

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

text {*

  we can use @{ML inst_spec} in the following proof 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 {*

  Now the complete tactic for proving the induction principles can 

  be implemented as follows:

*}

ML %linenosgray{*fun induction_tac defs prems insts =

  EVERY1 [ObjectLogic.full_atomize_tac,

          cut_facts_tac prems,

          K (rewrite_goals_tac defs),

          inst_spec_tac insts,

          assume_tac]*}

text {*

  We only have to give it as arguments the definitions, the premise 

  (like @{text "even n"}) 

  and the instantiations. Compare this with the manual proof given for the

  lemma @{thm [source] man_ind_principle}.  

  A testcase for this tactic is the function

*}

ML{*fun test_tac prems = 

let

  val defs = [@{thm even_def}, @{thm odd_def}]

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

in 

  induction_tac defs prems insts 

end*}

text {*

  which indeed proves the induction principle: 

*}

lemma 

assumes prems: "even n"

shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"

apply(tactic {* test_tac @{thms prems} *})

done

text {*

  While the tactic for the induction principle is relatively simple, 

  it is a bit harder to construct the goals from the introduction 

  rules the user provides. In general we have to construct for each predicate 

  @{text "pred"} a goal of the form

  @{text [display] 

  "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$> \<^raw:$zs$>"}

  where the given predicates @{text preds} are replaced in the introduction 

  rules by new distinct variables written @{text "\<^raw:$Ps$>"}. 

  We also need to generate fresh arguments for the predicate @{text "pred"} in

  the premise and the @{text "\<^raw:$P$>"} in the conclusion. We achieve

  that in two steps. 

  The function below 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 "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for

  which we prove the introduction principle; @{text "newpred"} is its

  replacement and @{text "tys"} are the argument types of this predicate.

*}

ML %linenosgray{*fun prove_induction lthy defs srules cnewpreds ((pred, newpred), tys)  =

let

  val zs = replicate (length tys) "z"

  val (newargnames, lthy') = Variable.variant_fixes zs lthy;

  val newargs = map Free (newargnames ~~ 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, ...} => induction_tac defs prems cnewpreds)

  |> singleton (ProofContext.export lthy' lthy)

end *}

text {* 

  In Line 3 we produce names @{text "\<^raw:$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'"}. In 

  Line 5 we just construct the terms corresponding to these variables. 

  The term variables are applied to the predicate in Line 7 (this corresponds

  to the first premise @{text "pred \<^raw:$zs$>"} of the induction principle). 

  In Line 8 and 9, we first construct the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} 

  and then add the (substituded) 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 call the tactic

  for proving the induction principle. This tactic expects definitions, the

  premise and the (certified) predicates with which the introduction rules

  have been substituted. This will return a theorem. However, it is a theorem

  proved inside the local theory @{text "lthy'"}, where the variables @{text

  "\<^raw:$zs$>"} are fixed, but free. By exporting this theorem from @{text

  "lthy'"} (which contains the @{text "\<^raw:$zs$>"} as free) to @{text

  "lthy"} (which does not), we obtain the desired quantifications @{text

  "\<And>\<^raw:$zs$>"}.

  (FIXME testcase)

  Now it is left to produce the new predicates with which the introduction

  rules are substituted. 

*}

ML %linenosgray{*fun inductions 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_induction 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 "\<^raw:$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 calculate the types of these new predicates

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

  certify them. We can now produce the substituted introduction rules 

  (Line 11). 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 "\<^raw:$Ps$>"} to obtain the correct quantification 

  (Line 16).

  A testcase for this function is

*}

local_setup %gray {* fn lthy =>

let 

  val rules = [@{prop "even (0::nat)"},

               @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},

               @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 

  val defs = [@{thm even_def}, @{thm odd_def}]

  val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]

  val tyss = [[@{typ "nat"}], [@{typ "nat"}]]

  val ind_thms = inductions rules defs preds tyss lthy

in

  warning (str_of_thms lthy ind_thms); lthy

end  

*}

text {*

  which prints out

@{text [display]

"> even z \<Longrightarrow> 

>  P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> P z,

> odd z \<Longrightarrow> 

>  P 0 \<Longrightarrow> (\<And>m. Pa m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Pa (Suc m)) \<Longrightarrow> Pa z"}

  This completes the code for the induction principles. Finally we can 

  prove the introduction rules. 

*}

ML {* ObjectLogic.rulify  *}

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

ML{*fun subproof2 prem params2 prems2 =  

 SUBPROOF (fn {prems, ...} =>

   let

     val prem' = prems MRS prem;

     val prem'' = 

       case prop_of prem' of

           _ $ (Const (@{const_name All}, _) $ _) =>

             prem' |> all_elims params2 

                   |> imp_elims prems2

         | _ => prem';

   in 

     rtac prem'' 1 

   end)*}

ML{*fun subproof1 rules preds i = 

 SUBPROOF (fn {params, prems, context = ctxt', ...} =>

   let

     val (prems1, prems2) = chop (length prems - length rules) prems;

     val (params1, params2) = chop (length params - length preds) params;

   in

     rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 

     THEN

     EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)

   end)*}

ML{*

fun introductions_tac defs rules preds i ctxt =

  EVERY1 [ObjectLogic.rulify_tac,

          K (rewrite_goals_tac defs),

          REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),

          subproof1 rules preds i ctxt]*}

lemma evenS: 

  shows "odd m \<Longrightarrow> even (Suc m)"

apply(tactic {* 

let

  val rules = [@{prop "even (0::nat)"},

                 @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},