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"
| "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> a\<sharp>Lam b 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"}.


  \begin{center}
  ****************************
  \end{center}
*}


text {*
  For building testcases let us give some shorthands for the definitions of @{text "even/odd"} and
  @{text "fresh"}. (FIXME put in a figure)
*}
  
ML{*val eo_defs = [@{thm even_def}, @{thm odd_def}]
val eo_rules =  
  [@{prop "even 0"},
   @{prop "\<And>n. odd n \<Longrightarrow> even (Suc n)"},
   @{prop "\<And>n. even n \<Longrightarrow> odd (Suc n)"}]
val eo_orules =  
  [@{prop "even 0"},
   @{prop "\<forall>n. odd n \<longrightarrow> even (Suc n)"},
   @{prop "\<forall>n. even n \<longrightarrow> odd (Suc n)"}]
val eo_preds =  [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] 
val eo_prednames = [@{binding "even"}, @{binding "odd"}]
val eo_syns = [NoSyn, NoSyn] 
val eo_arg_tyss = [[@{typ "nat"}],[@{typ "nat"}]] *}


ML{*val fresh_defs = [@{thm fresh_def}]
val fresh_rules =  
  [@{prop "\<And>a b. a\<noteq>b \<Longrightarrow> a\<sharp>Var b"},
   @{prop "\<And>a s t. a\<sharp>t \<Longrightarrow> a\<sharp>s \<Longrightarrow> a\<sharp>App t s"},
   @{prop "\<And>a t. a\<sharp>Lam a t"},
   @{prop "\<And>a b t. a\<noteq>b \<Longrightarrow> a\<sharp>t \<Longrightarrow> a\<sharp>Lam b t"}]
val fresh_orules =  
  [@{prop "\<forall>a b. a\<noteq>b \<longrightarrow> a\<sharp>Var b"},
   @{prop "\<forall>a s t. a\<sharp>t \<longrightarrow> a\<sharp>s \<longrightarrow> a\<sharp>App t s"},
   @{prop "\<forall>a t. a\<sharp>Lam a t"},
   @{prop "\<forall>a b t. a\<noteq>b \<longrightarrow> a\<sharp>t \<longrightarrow> a\<sharp>Lam b t"}]
val fresh_preds =  [@{term "fresh::string\<Rightarrow>trm\<Rightarrow>bool"}] *}


subsection {* Definitions *}

text {*
  First we 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_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. 
  Since we are testing the function inside \isacommand{local\_setup}, i.e., make
  changes to the ambient theory, we can query the definition with the usual
  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"}.


  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 given in @{text "arg_tys"}. 
  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
  "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
  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 pred = @{term "even::nat\<Rightarrow>bool"}
  val arg_tys = [@{typ "nat"}]
  val def = defs_aux lthy eo_orules eo_preds (pred, arg_tys)
in
  warning (Syntax.string_of_term lthy def); lthy
end *}

text {*
  The testcase  calls @{ML defs_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"}

  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
  to @{ML defs_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') = 
    definitions eo_rules eo_preds eo_prednames eo_syns eo_arg_tyss lthy
in
  warning (str_of_thms_no_vars 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}
  @{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}

  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 make again the
  definition, we pollute the name space with two versions of @{text "even"} 
  and @{text "odd"}.

  This completes the code for making the definitions. Next we deal with
  the induction principles. 
*}

subsection {* Introduction Rules *}

text {*
  Recall that the proof of the induction principle 
  for @{text "even"} was:
*}

lemma manual_ind_prin: 
assumes prem: "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 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 tactic:
*}

ML{*fun inst_spec_tac ctrms = 
  EVERY' (map (dtac o inst_spec) ctrms)*}

text {*
  This tactic allows us to instantiate in the following proof 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 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 
  (for example @{text "even n"}) and the instantiations. Compare this with the 
  manual proof given for the lemma @{thm [source] manual_ind_prin}: 
  as you can see there is almost a one-to-one correspondence between the \isacommand{apply}-script 
  and the @{ML induction_tac}. A testcase for this tactic is the function
*}

ML{*fun test_tac prem = 
let
  val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
in 
  induction_tac eo_defs prem insts 
end*}

text {*
  which indeed proves the induction principle: 
*}

lemma automatic_ind_prin:
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(tactic {* test_tac @{thms prem} *})
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] 
  "pred ?zs \<Longrightarrow> rules[preds := ?Ps] \<Longrightarrow> ?P ?zs"}

  where the predicates @{text preds} are replaced in the introduction 
  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. Note 
  that the  @{text "?Ps"}  and @{text "?zs"} need to be
  schematic variables that can be instantiated by the user.

  We generate these goals in two steps. The first function 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 introduction principle;
  @{text "newpred"} is its replacement and @{text "arg_tys"} are the argument
  types of this predicate.
*}

ML %linenosgray{*fun prove_induction 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, ...} => 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 
  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 (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 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 fixed, but free. By exporting this theorem from @{text
  "lthy'"} (which contains the @{text "zs"} as free) 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 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 = 
    prove_induction lthy eo_defs srules cnewpreds ((pred, newpred), arg_tys)
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 
  variable @{text "?z"}. The @{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_induction} over all
  predicates. This is what the second function does: 
*}

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 "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 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 = inductions 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 have been introduced by the pretty-printer and are 
  not significant.

  This completes the code for the induction principles.  
*}

subsection {* Introduction Rules *}

text {*
  Finally we can prove the introduction rules. Their proofs are quite a bit
  more involved. To ease these proofs somewhat 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})*}

text {* 
  To see what these functions do, let us suppose whe have the following three
  theorems. 
*}

lemma all_elims_test:
  fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
  shows "\<forall>x y z. P x y z" sorry

lemma imp_elims_test:
  fixes A B C::"bool"
  shows "A \<longrightarrow> B \<longrightarrow> C" sorry

lemma imp_elims_test':
  fixes A::"bool"
  shows "A" "B" sorry

text {*
  The function @{ML all_elims} takes a list of (certified) terms and instantiates
  theorems of the form @{thm [source] all_elims_test}. For example we can instantiate
  the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows

  @{ML_response_fake [display, gray]
"let
  val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
  val new_thm = all_elims ctrms @{thm all_elims_test}
in
  warning (str_of_thm_no_vars @{context} new_thm)
end"
  "P a b c"}

  Similarly, the function @{ML imp_elims} eliminates preconditions from implications. 
  For example: 

  @{ML_response_fake [display, gray]
"warning (str_of_thm_no_vars @{context} 
            (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))"
  "C"}
*}

ML {* prems_of *}
ML {* Logic.strip_params *}
ML {* Logic.strip_assums_hyp *}

ML {*
fun chop_print (params1, params2) (prems1, prems2) ctxt =
let
  val _ = warning ((commas params1) ^ " | " ^ (commas params2))
  val _ = warning ((commas (map (Syntax.string_of_term ctxt) prems1)) ^ " | " ^
                   (commas (map (Syntax.string_of_term ctxt) prems2)))
in
   ()
end
*}



lemma intro1:
  shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
apply(tactic {* ObjectLogic.rulify_tac 1 *})
apply(tactic {* rewrite_goals_tac [@{thm even_def}, @{thm odd_def}] *})
apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
oops

ML {* fun SUBPROOF_test tac ctxt = (SUBPROOF tac ctxt 1) ORELSE all_tac *}


lemma fresh_App:
  shows "\<And>a t s. \<lbrakk>a\<sharp>t; a\<sharp>s\<rbrakk> \<Longrightarrow> a\<sharp>App t s"
apply(tactic {* ObjectLogic.rulify_tac 1 *})
apply(tactic {* rewrite_goals_tac [@{thm fresh_def}] *})
apply(tactic {* REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1) *})
apply(tactic {* print_tac "" *})
apply(tactic {* SUBPROOF_test (fn {params, prems, ...} =>
   let
     val (prems1, prems2) = chop (length prems - length fresh_rules) prems
     val (params1, params2) = chop (length params - length fresh_preds) params
   in
     no_tac
   end) @{context} *})
oops


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

text {*

*}


ML %linenosgray{*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 
     (* applicateion of the i-ith intro rule *)
     THEN
     EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
   end)*}

text {*
  @{text "params1"} are the variables of the rules; @{text "params2"} is
  the variables corresponding to the @{text "preds"}.

  @{text "prems1"} are the assumption corresponding to the rules;
  @{text "prems2"} are the assumptions coming from the allIs/impIs

  you instantiate the parameters i-th introduction rule with the parameters
  that come from the rule; and you apply it to the goal

  this now generates subgoals corresponding to the premisses of this
  intro rule 
*}

ML{*
fun intros_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]*}

text {*
  A test case
*}

ML{*fun intros_tac_test ctxt i =
  intros_tac eo_defs eo_rules eo_preds i ctxt *}

lemma intro0:
  shows "even 0"
apply(tactic {* intros_tac_test @{context} 0 *})
done

lemma intro1:
  shows "\<And>m. odd m \<Longrightarrow> even (Suc m)"
apply(tactic {* intros_tac_test @{context} 1 *})
done

lemma intro2:
  shows "\<And>m. even m \<Longrightarrow> odd (Suc m)"
apply(tactic {* intros_tac_test @{context} 2 *})
done

ML{*fun introductions rules preds defs lthy = 
let
  fun prove_intro (i, goal) =
    Goal.prove lthy [] [] goal
      (fn {context, ...} => intros_tac defs rules preds i context)
in
  map_index prove_intro rules
end*}

text {* main internal function *}

ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy =
let
  val syns = map snd pred_specs
  val pred_specs' = map fst pred_specs
  val prednames = map fst pred_specs'
  val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'

  val tyss = map (binder_types o fastype_of) preds   
  val (attrs, rules) = split_list rule_specs    

  val (defs, lthy') = definitions rules preds prednames syns tyss lthy      
  val ind_rules = inductions rules defs preds tyss lthy' 	
  val intro_rules = introductions rules preds defs lthy'

  val mut_name = space_implode "_" (map Binding.name_of prednames)
  val case_names = map (Binding.name_of o fst) attrs
in
    lthy' 
    |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
        ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) 
    |-> (fn intross => LocalTheory.note Thm.theoremK
         ((Binding.qualify false mut_name (@{binding "intros"}), []), maps snd intross)) 
    |>> snd 
    ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
         ((Binding.qualify false (Binding.name_of R) (@{binding "induct"}),
          [Attrib.internal (K (RuleCases.case_names case_names)),
           Attrib.internal (K (RuleCases.consumes 1)),
           Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
          (pred_specs ~~ ind_rules)) #>> maps snd) 
    |> snd
end*}

ML{*fun add_inductive_cmd pred_specs rule_specs lthy =
let
  val ((pred_specs', rule_specs'), _) = 
         Specification.read_spec pred_specs rule_specs lthy
in
  add_inductive pred_specs' rule_specs' lthy
end*} 

ML{*val spec_parser = 
   OuterParse.fixes -- 
   Scan.optional 
     (OuterParse.$$$ "where" |--
        OuterParse.!!! 
          (OuterParse.enum1 "|" 
             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}

ML{*val specification =
  spec_parser >>
    (fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*}

ML{*val _ = OuterSyntax.local_theory "simple_inductive" 
              "define inductive predicates"
                 OuterKeyword.thy_decl specification*}

text {*
  Things to include at the end:

  \begin{itemize}
  \item say something about add-inductive-i to return
  the rules
  \item say that the induction principle is weaker (weaker than
  what the standard inductive package generates)
  \item say that no conformity test is done
  \end{itemize}
  
*}

simple_inductive
  Even and Odd
where
  Even0: "Even 0"
| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"
| OddS: "Even n \<Longrightarrow> Odd (Suc n)"

end