New proof method "induction" that gives induction hypotheses the name IH.
authornipkow
Tue Sep 20 05:47:11 2011 +0200 (2011-09-20)
changeset 450140e847655b2d8
parent 45008 8b74cfea913a
child 45015 fdac1e9880eb
New proof method "induction" that gives induction hypotheses the name IH.
NEWS
doc-src/IsarRef/Thy/Proof.thy
doc-src/IsarRef/Thy/document/Proof.tex
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/Tools/induct.ML
src/Tools/induction.ML
     1.1 --- a/NEWS	Tue Sep 20 01:32:04 2011 +0200
     1.2 +++ b/NEWS	Tue Sep 20 05:47:11 2011 +0200
     1.3 @@ -76,6 +76,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New proof method "induction" that gives induction hypotheses the name IH,
     1.8 +thus distinguishing them from further hypotheses that come from rule
     1.9 +induction.  The latter are still called "hyps".  Method "induction" is a thin
    1.10 +wrapper around "induct" and follows the same syntax.
    1.11 +
    1.12  * Class bot and top require underlying partial order rather than
    1.13  preorder: uniqueness of bot and top is guaranteed.  INCOMPATIBILITY.
    1.14  
     2.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Tue Sep 20 01:32:04 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Tue Sep 20 05:47:11 2011 +0200
     2.3 @@ -1259,10 +1259,12 @@
     2.4    \begin{matharray}{rcl}
     2.5      @{method_def cases} & : & @{text method} \\
     2.6      @{method_def induct} & : & @{text method} \\
     2.7 +    @{method_def induction} & : & @{text method} \\
     2.8      @{method_def coinduct} & : & @{text method} \\
     2.9    \end{matharray}
    2.10  
    2.11 -  The @{method cases}, @{method induct}, and @{method coinduct}
    2.12 +  The @{method cases}, @{method induct}, @{method induction},
    2.13 +  and @{method coinduct}
    2.14    methods provide a uniform interface to common proof techniques over
    2.15    datatypes, inductive predicates (or sets), recursive functions etc.
    2.16    The corresponding rules may be specified and instantiated in a
    2.17 @@ -1277,11 +1279,15 @@
    2.18    and parameters separately).  This avoids cumbersome encoding of
    2.19    ``strengthened'' inductive statements within the object-logic.
    2.20  
    2.21 +  Method @{method induction} differs from @{method induct} only in
    2.22 +  the names of the facts in the local context invoked by the @{command "case"}
    2.23 +  command.
    2.24 +
    2.25    @{rail "
    2.26      @@{method cases} ('(' 'no_simp' ')')? \\
    2.27        (@{syntax insts} * @'and') rule?
    2.28      ;
    2.29 -    @@{method induct} ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
    2.30 +    (@@{method induct} | @@{method induction}) ('(' 'no_simp' ')')? (definsts * @'and') \\ arbitrary? taking? rule?
    2.31      ;
    2.32      @@{method coinduct} @{syntax insts} taking rule?
    2.33      ;
    2.34 @@ -1325,8 +1331,9 @@
    2.35    "(no_simp)"} option can be used to disable pre-simplification of
    2.36    cases (see the description of @{method induct} below for details).
    2.37  
    2.38 -  \item @{method induct}~@{text "insts R"} is analogous to the
    2.39 -  @{method cases} method, but refers to induction rules, which are
    2.40 +  \item @{method induct}~@{text "insts R"} and
    2.41 +  @{method induction}~@{text "insts R"} are analogous to the
    2.42 +  @{method cases} method, but refer to induction rules, which are
    2.43    determined as follows:
    2.44  
    2.45    \medskip
    2.46 @@ -1437,13 +1444,20 @@
    2.47    and definitions effectively participate in the inductive rephrasing
    2.48    of the original statement.
    2.49  
    2.50 -  In induction proofs, local assumptions introduced by cases are split
    2.51 +  In @{method induct} proofs, local assumptions introduced by cases are split
    2.52    into two different kinds: @{text hyps} stemming from the rule and
    2.53    @{text prems} from the goal statement.  This is reflected in the
    2.54    extracted cases accordingly, so invoking ``@{command "case"}~@{text
    2.55    c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
    2.56    as well as fact @{text c} to hold the all-inclusive list.
    2.57  
    2.58 +  In @{method induction} proofs, local assumptions introduced by cases are
    2.59 +  split into three different kinds: @{text IH}, the induction hypotheses,
    2.60 +  @{text hyps}, the remaining hypotheses stemming from the rule, and
    2.61 +  @{text prems}, the assumptions from the goal statement. The names are
    2.62 +  @{text c.IH}, @{text c.hyps} and @{text c.prems}, as above.
    2.63 +
    2.64 +
    2.65    \medskip Facts presented to either method are consumed according to
    2.66    the number of ``major premises'' of the rule involved, which is
    2.67    usually 0 for plain cases and induction rules of datatypes etc.\ and
     3.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Tue Sep 20 01:32:04 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Tue Sep 20 05:47:11 2011 +0200
     3.3 @@ -1700,10 +1700,12 @@
     3.4  \begin{matharray}{rcl}
     3.5      \indexdef{}{method}{cases}\hypertarget{method.cases}{\hyperlink{method.cases}{\mbox{\isa{cases}}}} & : & \isa{method} \\
     3.6      \indexdef{}{method}{induct}\hypertarget{method.induct}{\hyperlink{method.induct}{\mbox{\isa{induct}}}} & : & \isa{method} \\
     3.7 +    \indexdef{}{method}{induction}\hypertarget{method.induction}{\hyperlink{method.induction}{\mbox{\isa{induction}}}} & : & \isa{method} \\
     3.8      \indexdef{}{method}{coinduct}\hypertarget{method.coinduct}{\hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}} & : & \isa{method} \\
     3.9    \end{matharray}
    3.10  
    3.11 -  The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
    3.12 +  The \hyperlink{method.cases}{\mbox{\isa{cases}}}, \hyperlink{method.induct}{\mbox{\isa{induct}}}, \hyperlink{method.induction}{\mbox{\isa{induction}}},
    3.13 +  and \hyperlink{method.coinduct}{\mbox{\isa{coinduct}}}
    3.14    methods provide a uniform interface to common proof techniques over
    3.15    datatypes, inductive predicates (or sets), recursive functions etc.
    3.16    The corresponding rules may be specified and instantiated in a
    3.17 @@ -1718,6 +1720,10 @@
    3.18    and parameters separately).  This avoids cumbersome encoding of
    3.19    ``strengthened'' inductive statements within the object-logic.
    3.20  
    3.21 +  Method \hyperlink{method.induction}{\mbox{\isa{induction}}} differs from \hyperlink{method.induct}{\mbox{\isa{induct}}} only in
    3.22 +  the names of the facts in the local context invoked by the \hyperlink{command.case}{\mbox{\isa{\isacommand{case}}}}
    3.23 +  command.
    3.24 +
    3.25    \begin{railoutput}
    3.26  \rail@begin{6}{}
    3.27  \rail@term{\hyperlink{method.cases}{\mbox{\isa{cases}}}}[]
    3.28 @@ -1742,7 +1748,11 @@
    3.29  \rail@endbar
    3.30  \rail@end
    3.31  \rail@begin{6}{}
    3.32 +\rail@bar
    3.33  \rail@term{\hyperlink{method.induct}{\mbox{\isa{induct}}}}[]
    3.34 +\rail@nextbar{1}
    3.35 +\rail@term{\hyperlink{method.induction}{\mbox{\isa{induction}}}}[]
    3.36 +\rail@endbar
    3.37  \rail@bar
    3.38  \rail@nextbar{1}
    3.39  \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
    3.40 @@ -1872,8 +1882,9 @@
    3.41    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
    3.42    cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details).
    3.43  
    3.44 -  \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} is analogous to the
    3.45 -  \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are
    3.46 +  \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} and
    3.47 +  \hyperlink{method.induction}{\mbox{\isa{induction}}}~\isa{{\isaliteral{22}{\isachardoublequote}}insts\ R{\isaliteral{22}{\isachardoublequote}}} are analogous to the
    3.48 +  \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refer to induction rules, which are
    3.49    determined as follows:
    3.50  
    3.51    \medskip
    3.52 @@ -1979,12 +1990,19 @@
    3.53    and definitions effectively participate in the inductive rephrasing
    3.54    of the original statement.
    3.55  
    3.56 -  In induction proofs, local assumptions introduced by cases are split
    3.57 +  In \hyperlink{method.induct}{\mbox{\isa{induct}}} proofs, local assumptions introduced by cases are split
    3.58    into two different kinds: \isa{hyps} stemming from the rule and
    3.59    \isa{prems} from the goal statement.  This is reflected in the
    3.60    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},
    3.61    as well as fact \isa{c} to hold the all-inclusive list.
    3.62  
    3.63 +  In \hyperlink{method.induction}{\mbox{\isa{induction}}} proofs, local assumptions introduced by cases are
    3.64 +  split into three different kinds: \isa{IH}, the induction hypotheses,
    3.65 +  \isa{hyps}, the remaining hypotheses stemming from the rule, and
    3.66 +  \isa{prems}, the assumptions from the goal statement. The names are
    3.67 +  \isa{c{\isaliteral{2E}{\isachardot}}IH}, \isa{c{\isaliteral{2E}{\isachardot}}hyps} and \isa{c{\isaliteral{2E}{\isachardot}}prems}, as above.
    3.68 +
    3.69 +
    3.70    \medskip Facts presented to either method are consumed according to
    3.71    the number of ``major premises'' of the rule involved, which is
    3.72    usually 0 for plain cases and induction rules of datatypes etc.\ and
     4.1 --- a/src/HOL/HOL.thy	Tue Sep 20 01:32:04 2011 +0200
     4.2 +++ b/src/HOL/HOL.thy	Tue Sep 20 05:47:11 2011 +0200
     4.3 @@ -26,6 +26,7 @@
     4.4    ("Tools/simpdata.ML")
     4.5    "~~/src/Tools/atomize_elim.ML"
     4.6    "~~/src/Tools/induct.ML"
     4.7 +  ("~~/src/Tools/induction.ML")
     4.8    ("~~/src/Tools/induct_tacs.ML")
     4.9    ("Tools/recfun_codegen.ML")
    4.10    ("Tools/cnf_funcs.ML")
    4.11 @@ -1490,8 +1491,10 @@
    4.12  )
    4.13  *}
    4.14  
    4.15 +use "~~/src/Tools/induction.ML"
    4.16 +
    4.17  setup {*
    4.18 -  Induct.setup #>
    4.19 +  Induct.setup #> Induction.setup #>
    4.20    Context.theory_map (Induct.map_simpset (fn ss => ss
    4.21      setmksimps (fn ss => Simpdata.mksimps Simpdata.mksimps_pairs ss #>
    4.22        map (Simplifier.rewrite_rule (map Thm.symmetric
     5.1 --- a/src/HOL/IsaMakefile	Tue Sep 20 01:32:04 2011 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Tue Sep 20 05:47:11 2011 +0200
     5.3 @@ -145,6 +145,7 @@
     5.4    $(SRC)/Tools/eqsubst.ML \
     5.5    $(SRC)/Tools/induct.ML \
     5.6    $(SRC)/Tools/induct_tacs.ML \
     5.7 +  $(SRC)/Tools/induction.ML \
     5.8    $(SRC)/Tools/intuitionistic.ML \
     5.9    $(SRC)/Tools/misc_legacy.ML \
    5.10    $(SRC)/Tools/nbe.ML \
     6.1 --- a/src/Tools/induct.ML	Tue Sep 20 01:32:04 2011 +0200
     6.2 +++ b/src/Tools/induct.ML	Tue Sep 20 05:47:11 2011 +0200
     6.3 @@ -74,11 +74,21 @@
     6.4    val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
     6.5      thm list -> int -> cases_tactic
     6.6    val get_inductT: Proof.context -> term option list list -> thm list list
     6.7 +  type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
     6.8 +  val gen_induct_tac: (theory -> case_data * thm -> case_data * thm) ->
     6.9 +    Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    6.10 +    (string * typ) list list -> term option list -> thm list option ->
    6.11 +    thm list -> int -> cases_tactic
    6.12    val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    6.13      (string * typ) list list -> term option list -> thm list option ->
    6.14      thm list -> int -> cases_tactic
    6.15    val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
    6.16      thm list -> int -> cases_tactic
    6.17 +  val gen_induct_setup: binding ->
    6.18 +   (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
    6.19 +    (string * typ) list list -> term option list -> thm list option ->
    6.20 +    thm list -> int -> cases_tactic) ->
    6.21 +   theory -> theory
    6.22    val setup: theory -> theory
    6.23  end;
    6.24  
    6.25 @@ -721,7 +731,9 @@
    6.26  fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
    6.27    | get_inductP _ _ = [];
    6.28  
    6.29 -fun induct_tac ctxt simp def_insts arbitrary taking opt_rule facts =
    6.30 +type case_data = (((string * string list) * string list) list * int)
    6.31 +
    6.32 +fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
    6.33    let
    6.34      val thy = Proof_Context.theory_of ctxt;
    6.35  
    6.36 @@ -734,6 +746,7 @@
    6.37            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
    6.38          |> maps (prep_inst ctxt align_right (atomize_term thy))
    6.39          |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
    6.40 +      |> mod_cases thy
    6.41        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    6.42  
    6.43      val ruleq =
    6.44 @@ -791,7 +804,7 @@
    6.45         THEN_ALL_NEW rulify_tac)
    6.46    end;
    6.47  
    6.48 -
    6.49 +val induct_tac = gen_induct_tac (K I);
    6.50  
    6.51  (** coinduct method **)
    6.52  
    6.53 @@ -910,16 +923,18 @@
    6.54            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
    6.55      "case analysis on types or predicates/sets";
    6.56  
    6.57 -val induct_setup =
    6.58 -  Method.setup @{binding induct}
    6.59 +fun gen_induct_setup binding itac =
    6.60 +  Method.setup binding
    6.61      (Args.mode no_simpN -- (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
    6.62        (arbitrary -- taking -- Scan.option induct_rule)) >>
    6.63        (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
    6.64          RAW_METHOD_CASES (fn facts =>
    6.65            Seq.DETERM
    6.66 -            (HEADGOAL (induct_tac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
    6.67 +            (HEADGOAL (itac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
    6.68      "induction on types or predicates/sets";
    6.69  
    6.70 +val induct_setup = gen_induct_setup @{binding induct} induct_tac;
    6.71 +
    6.72  val coinduct_setup =
    6.73    Method.setup @{binding coinduct}
    6.74      (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/induction.ML	Tue Sep 20 05:47:11 2011 +0200
     7.3 @@ -0,0 +1,43 @@
     7.4 +signature INDUCTION =
     7.5 +sig
     7.6 +  val induction_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     7.7 +    (string * typ) list list -> term option list -> thm list option ->
     7.8 +    thm list -> int -> cases_tactic
     7.9 +  val setup: theory -> theory
    7.10 +end
    7.11 +
    7.12 +structure Induction: INDUCTION =
    7.13 +struct
    7.14 +
    7.15 +val ind_hypsN = "IH";
    7.16 +
    7.17 +fun preds_of t =
    7.18 + (case strip_comb t of
    7.19 +    (p as Var _, _) => [p]
    7.20 +  | (p as Free _, _) => [p]
    7.21 +  | (_, ts) => flat(map preds_of ts))
    7.22 +
    7.23 +fun name_hyps thy (arg as ((cases,consumes),th)) =
    7.24 +  if not(forall (null o #2 o #1) cases) then arg
    7.25 +  else
    7.26 +    let
    7.27 +      val (prems, concl) = Logic.strip_horn (prop_of th);
    7.28 +      val prems' = drop consumes prems;
    7.29 +      val ps = preds_of concl;
    7.30 +
    7.31 +      fun hname_of t =
    7.32 +        if exists_subterm (member (op =) ps) t
    7.33 +        then ind_hypsN else Rule_Cases.case_hypsN
    7.34 +
    7.35 +      val hnamess = map (map hname_of o Logic.strip_assums_hyp) prems'
    7.36 +      val n = Int.min (length hnamess, length cases) 
    7.37 +      val cases' = map (fn (((cn,_),concls),hns) => ((cn,hns),concls))
    7.38 +        (take n cases ~~ take n hnamess)
    7.39 +    in ((cases',consumes),th) end
    7.40 +
    7.41 +val induction_tac = Induct.gen_induct_tac name_hyps
    7.42 +
    7.43 +val setup = Induct.gen_induct_setup @{binding induction} induction_tac
    7.44 +
    7.45 +end
    7.46 +