# HG changeset patch
# User nipkow
# Date 1316490431 -7200
# Node ID 0e847655b2d87c33aa05e033ba82a4dc862b0949
# Parent  8b74cfea913ac21121b98a996c99e107cb4a9b87
New proof method "induction" that gives induction hypotheses the name IH.

diff -r 8b74cfea913a -r 0e847655b2d8 NEWS
--- a/NEWS	Tue Sep 20 01:32:04 2011 +0200
+++ b/NEWS	Tue Sep 20 05:47:11 2011 +0200
@@ -76,6 +76,11 @@
 
 *** HOL ***
 
+* New proof method "induction" that gives induction hypotheses the name IH,
+thus distinguishing them from further hypotheses that come from rule
+induction.  The latter are still called "hyps".  Method "induction" is a thin
+wrapper around "induct" and follows the same syntax.
+
 * Class bot and top require underlying partial order rather than
 preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
 
diff -r 8b74cfea913a -r 0e847655b2d8 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Tue Sep 20 01:32:04 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Tue Sep 20 05:47:11 2011 +0200
@@ -1259,10 +1259,12 @@
   \begin{matharray}{rcl}
     @{method_def cases} & : & @{text method} \\
     @{method_def induct} & : & @{text method} \\
+    @{method_def induction} & : & @{text method} \\
     @{method_def coinduct} & : & @{text method} \\
   \end{matharray}
 
-  The @{method cases}, @{method induct}, and @{method coinduct}
+  The @{method cases}, @{method induct}, @{method induction},
+  and @{method coinduct}
   methods provide a uniform interface to common proof techniques over
   datatypes, inductive predicates (or sets), recursive functions etc.
   The corresponding rules may be specified and instantiated in a
@@ -1277,11 +1279,15 @@
   and parameters separately).  This avoids cumbersome encoding of
   ``strengthened'' inductive statements within the object-logic.
 
+  Method @{method induction} differs from @{method induct} only in
+  the names of the facts in the local context invoked by the @{command "case"}
+  command.
+
   @{rail "
     @@{method cases} ('(' 'no_simp' ')')? \\
       (@{syntax insts} * @'and') rule?
     ;
-    @@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
+    (@@{method induct} | @@{method induction}) ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
     ;
     @@{method coinduct} @{syntax insts} taking rule?
     ;
@@ -1325,8 +1331,9 @@
   "(no_simp)"} option can be used to disable pre-simplification of
   cases (see the description of @{method induct} below for details).
 
-  \item @{method induct}~@{text "insts R"} is analogous to the
-  @{method cases} method, but refers to induction rules, which are
+  \item @{method induct}~@{text "insts R"} and
+  @{method induction}~@{text "insts R"} are analogous to the
+  @{method cases} method, but refer to induction rules, which are
   determined as follows:
 
   \medskip
@@ -1437,13 +1444,20 @@
   and definitions effectively participate in the inductive rephrasing
   of the original statement.
 
-  In induction proofs, local assumptions introduced by cases are split
+  In @{method induct} proofs, local assumptions introduced by cases are split
   into two different kinds: @{text hyps} stemming from the rule and
   @{text prems} from the goal statement.  This is reflected in the
   extracted cases accordingly, so invoking ``@{command "case"}~@{text
   c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
   as well as fact @{text c} to hold the all-inclusive list.
 
+  In @{method induction} proofs, local assumptions introduced by cases are
+  split into three different kinds: @{text IH}, the induction hypotheses,
+  @{text hyps}, the remaining hypotheses stemming from the rule, and
+  @{text prems}, the assumptions from the goal statement. The names are
+  @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above.
+
+
   \medskip Facts presented to either method are consumed according to
   the number of ``major premises'' of the rule involved, which is
   usually 0 for plain cases and induction rules of datatypes etc.\ and
diff -r 8b74cfea913a -r 0e847655b2d8 doc-src/IsarRef/Thy/document/Proof.tex
--- a/doc-src/IsarRef/Thy/document/Proof.tex	Tue Sep 20 01:32:04 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex	Tue Sep 20 05:47:11 2011 +0200
@@ -1700,10 +1700,12 @@
 \begin{matharray}{rcl}
     \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isa{method} \\
     \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isa{method} \\
+    \indexdef{}{method}{induction}\hypertarget{method.induction}{\hyperlink{method.induction}{\mbox{\isa{induction}}}} & : & \isa{method} \\
     \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{method} \\
   \end{matharray}
 
-  The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
+  The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, \hyperlink{method.induction}{\mbox{\isa{induction}}},
+  and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
   methods provide a uniform interface to common proof techniques over
   datatypes, inductive predicates (or sets), recursive functions etc.
   The corresponding rules may be specified and instantiated in a
@@ -1718,6 +1720,10 @@
   and parameters separately).  This avoids cumbersome encoding of
   ``strengthened'' inductive statements within the object-logic.
 
+  Method \hyperlink{method.induction}{\mbox{\isa{induction}}} differs from \hyperlink{method.induct}{\mbox{\isa{induct}}} only in
+  the names of the facts in the local context invoked by the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}
+  command.
+
   \begin{railoutput}
 \rail@begin{6}{}
 \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
@@ -1742,7 +1748,11 @@
 \rail@endbar
 \rail@end
 \rail@begin{6}{}
+\rail@bar
 \rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{method.induction}{\mbox{\isa{induction}}}}[]
+\rail@endbar
 \rail@bar
 \rail@nextbar{1}
 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
@@ -1872,8 +1882,9 @@
   last premise (it is usually the same for all cases).  The \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}no{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} option can be used to disable pre-simplification of
   cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
 
-  \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} is analogous to the
-  \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
+  \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} and
+  \hyperlink{method.induction}{\mbox{\isa{induction}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} are analogous to the
+  \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refer to induction rules, which are
   determined as follows:
 
   \medskip
@@ -1979,12 +1990,19 @@
   and definitions effectively participate in the inductive rephrasing
   of the original statement.
 
-  In induction proofs, local assumptions introduced by cases are split
+  In \hyperlink{method.induct}{\mbox{\isa{induct}}} proofs, local assumptions introduced by cases are split
   into two different kinds: \isa{hyps} stemming from the rule and
   \isa{prems} from the goal statement.  This is reflected in the
   extracted cases accordingly, so invoking ``\hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}~\isa{c}'' will provide separate facts \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems},
   as well as fact \isa{c} to hold the all-inclusive list.
 
+  In \hyperlink{method.induction}{\mbox{\isa{induction}}} proofs, local assumptions introduced by cases are
+  split into three different kinds: \isa{IH}, the induction hypotheses,
+  \isa{hyps}, the remaining hypotheses stemming from the rule, and
+  \isa{prems}, the assumptions from the goal statement. The names are
+  \isa{c{\isaliteral{2E}{\isachardot}}IH}, \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems}, as above.
+
+
   \medskip Facts presented to either method are consumed according to
   the number of ``major premises'' of the rule involved, which is
   usually 0 for plain cases and induction rules of datatypes etc.\ and
diff -r 8b74cfea913a -r 0e847655b2d8 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Sep 20 01:32:04 2011 +0200
+++ b/src/HOL/HOL.thy	Tue Sep 20 05:47:11 2011 +0200
@@ -26,6 +26,7 @@
   ("Tools/simpdata.ML")
   "~~/src/Tools/atomize_elim.ML"
   "~~/src/Tools/induct.ML"
+  ("~~/src/Tools/induction.ML")
   ("~~/src/Tools/induct_tacs.ML")
   ("Tools/recfun_codegen.ML")
   ("Tools/cnf_funcs.ML")
@@ -1490,8 +1491,10 @@
 )
 *}
 
+use "~~/src/Tools/induction.ML"
+
 setup {*
-  Induct.setup #>
+  Induct.setup #> Induction.setup #>
   Context.theory_map (Induct.map_simpset (fn ss => ss
     setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
       map (Simplifier.rewrite_rule (map Thm.symmetric
diff -r 8b74cfea913a -r 0e847655b2d8 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Sep 20 01:32:04 2011 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 20 05:47:11 2011 +0200
@@ -145,6 +145,7 @@
   $(SRC)/Tools/eqsubst.ML \
   $(SRC)/Tools/induct.ML \
   $(SRC)/Tools/induct_tacs.ML \
+  $(SRC)/Tools/induction.ML \
   $(SRC)/Tools/intuitionistic.ML \
   $(SRC)/Tools/misc_legacy.ML \
   $(SRC)/Tools/nbe.ML \
diff -r 8b74cfea913a -r 0e847655b2d8 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Sep 20 01:32:04 2011 +0200
+++ b/src/Tools/induct.ML	Tue Sep 20 05:47:11 2011 +0200
@@ -74,11 +74,21 @@
   val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
     thm list -> int -> cases_tactic
   val get_inductT: Proof.context -> term option list list -> thm list list
+  type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
+  val gen_induct_tac: (theory -> case_data * thm -> case_data * thm) ->
+    Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+    (string * typ) list list -> term option list -> thm list option ->
+    thm list -> int -> cases_tactic
   val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic
   val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
     thm list -> int -> cases_tactic
+  val gen_induct_setup: binding ->
+   (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+    (string * typ) list list -> term option list -> thm list option ->
+    thm list -> int -> cases_tactic) ->
+   theory -> theory
   val setup: theory -> theory
 end;
 
@@ -721,7 +731,9 @@
 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];
 
-fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts =
+type case_data = (((string * string list) * string list) list * int)
+
+fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
   let
     val thy = Proof_Context.theory_of ctxt;
 
@@ -734,6 +746,7 @@
           (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
         |> maps (prep_inst ctxt align_right (atomize_term thy))
         |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
+      |> mod_cases thy
       |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
 
     val ruleq =
@@ -791,7 +804,7 @@
        THEN_ALL_NEW rulify_tac)
   end;
 
-
+val induct_tac = gen_induct_tac (K I);
 
 (** coinduct method **)
 
@@ -910,16 +923,18 @@
           (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
     "case analysis on types or predicates/sets";
 
-val induct_setup =
-  Method.setup @{binding induct}
+fun gen_induct_setup binding itac =
+  Method.setup binding
     (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
       (arbitrary -- taking -- Scan.option induct_rule)) >>
       (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
         RAW_METHOD_CASES (fn facts =>
           Seq.DETERM
-            (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
+            (HEADGOAL (itac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
     "induction on types or predicates/sets";
 
+val induct_setup = gen_induct_setup @{binding induct} induct_tac;
+
 val coinduct_setup =
   Method.setup @{binding coinduct}
     (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
diff -r 8b74cfea913a -r 0e847655b2d8 src/Tools/induction.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/induction.ML	Tue Sep 20 05:47:11 2011 +0200
@@ -0,0 +1,43 @@
+signature INDUCTION =
+sig
+  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+    (string * typ) list list -> term option list -> thm list option ->
+    thm list -> int -> cases_tactic
+  val setup: theory -> theory
+end
+
+structure Induction: INDUCTION =
+struct
+
+val ind_hypsN = "IH";
+
+fun preds_of t =
+ (case strip_comb t of
+    (p as Var _, _) => [p]
+  | (p as Free _, _) => [p]
+  | (_, ts) => flat(map preds_of ts))
+
+fun name_hyps thy (arg as ((cases,consumes),th)) =
+  if not(forall (null o #2 o #1) cases) then arg
+  else
+    let
+      val (prems, concl) = Logic.strip_horn (prop_of th);
+      val prems' = drop consumes prems;
+      val ps = preds_of concl;
+
+      fun hname_of t =
+        if exists_subterm (member (op =) ps) t
+        then ind_hypsN else Rule_Cases.case_hypsN
+
+      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
+      val n = Int.min (length hnamess, length cases) 
+      val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
+        (take n cases ~~ take n hnamess)
+    in ((cases',consumes),th) end
+
+val induction_tac = Induct.gen_induct_tac name_hyps
+
+val setup = Induct.gen_induct_setup @{binding induction} induction_tac
+
+end
+