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

  \underline{Induction proof}

  After ``objectivication'' we have 

   @{text "pred zs"} and @{text "orules[preds::=Ps]"}; and 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"}.

  \underline{Intro proof}

  Assume we want to prove the $i$th intro rule. 

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

  expanding the defs, gives 

  @{text [display]

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

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

  the $i$th @{text "orule"} is of the 

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

*}

text {*

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

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

  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

*}

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

  @{text [quotes] "z"} (Line 7); then generates variants for all these strings

  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

*}

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

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

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

*}

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 "even"}, @{binding "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 {* 

  constructing the induction principles from the given introduction

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

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

*}

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: 

*}

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] 

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

  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

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

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

*}

let

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

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

  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

  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. 

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

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

*}

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 

  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

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

  (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

text {*

  which prints out

@{text [display]