theory Ind_Code

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

begin

datatype trm =

  Var "string"

| App "trm" "trm"

| Lam "string" "trm"

simple_inductive 

  fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" ("_ \<sharp> _" [100,100] 100)

where

  "a\<noteq>b \<Longrightarrow> a\<sharp>Var b"

| "\<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"

| "a\<sharp>Lam a t"

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

  By applying as many allI and impI as possible, 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 $i$th @{text "orule"} is of the 

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

  So we apply the $i$th @{text "orule"}, but we have to show the @{text "As"} (by assumption)

  and all @{text "(\<forall>ys. Bs \<longrightarrow> pred ss)\<^isup>*"}. For the latter we use the assumptions

  @{text "(\<forall>ys. Bs \<longrightarrow> (\<forall>preds. orules \<longrightarrow> pred ss))\<^isup>*"} and @{text "orules"}.

*}

text {*

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

  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_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_no_vars lthy' def); lthy'

end *}

text {*

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

  command \isacommand{thm}:

  \begin{isabelle}

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

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

  \end{isabelle}

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

  The first function constructs the term for one particular predicate, say

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

*}

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

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

  predicate. A testcase for this function is

*}

local_setup %gray{* fn lthy =>

let

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

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

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

  The second function for the definitions 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

  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

in

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}

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

  for @{text "even"} was:

*}

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

*}

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:

*}

  EVERY1 [ObjectLogic.full_atomize_tac,

          K (rewrite_goals_tac defs),

          inst_spec_tac insts,

          assume_tac]*}

text {*

*}

let

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

in 

end*}

text {*

  which indeed proves the induction principle: 

*}

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] 

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

  that the  @{text "?Ps"}  and @{text "?zs"} need to be

*}

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, ...} => induction_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'"}. In 

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

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

  "zs"} are fixed, but free. By exporting this theorem from @{text

  "lthy'"} (which contains the @{text "zs"} as free) to @{text

*}

local_setup %gray{* fn lthy =>

let

  val srules = [@{prop "P (0::nat)"},

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

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

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

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

  val newpred = @{term "P::nat\<Rightarrow>bool"}

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

  val intro = 

in

  warning (str_of_thm lthy intro); lthy

end *} 

text {*

  This prints out:

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

  Note that the export from @{text lthy'} to @{text lthy} in Line 13 above 

  has turned the free, but fixed, @{text "z"} into a schematic 

  We still have to produce the new predicates with which the introduction

  rules are substituted and iterate @{ML prove_induction} over all

*}

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)