
diff -r 8939b8fd8603 -r 069d525f8f1d ProgTutorial/Package/Ind_Code.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Package/Ind_Code.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,589 @@
+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"}
+  
+  applying as many allI and impI as possible
+  
+  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 $i$th @{text "orule"} is 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 "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 "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 {* 
+  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)"},
+                 @{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"}]
+in
+  introductions_tac defs rules preds 1 @{context}
+end *})
+done
+
+ML{*fun introductions rules preds defs lthy = 
+let
+  fun prove_intro (i, goal) =
+    Goal.prove lthy [] [] goal
+      (fn {context, ...} => introductions_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)
+  \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




