removed obsolete option open;
authorwenzelm
Fri May 16 21:53:30 2008 +0200 (2008-05-16)
changeset 26924485213276a2a
parent 26923 54dce7c7c76f
child 26925 ce964f0df281
removed obsolete option open;
tuned comments;
src/Tools/induct.ML
     1.1 --- a/src/Tools/induct.ML	Fri May 16 21:53:29 2008 +0200
     1.2 +++ b/src/Tools/induct.ML	Fri May 16 21:53:30 2008 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Proof by cases and induction.
     1.8 +Proof by cases, induction, and coinduction.
     1.9  *)
    1.10  
    1.11  signature INDUCT_DATA =
    1.12 @@ -57,13 +57,13 @@
    1.13    val rulify_tac: int -> tactic
    1.14    val internalize: int -> thm -> thm
    1.15    val guess_instance: thm -> int -> thm -> thm Seq.seq
    1.16 -  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
    1.17 +  val cases_tac: Proof.context -> term option list list -> thm option ->
    1.18      thm list -> int -> cases_tactic
    1.19 -  val induct_tac: Proof.context -> bool -> (string option * term) option list list ->
    1.20 -    (string * typ) list list -> term option list -> thm list option -> thm list -> int ->
    1.21 -    cases_tactic
    1.22 -  val coinduct_tac: Proof.context -> bool -> term option list -> term option list ->
    1.23 -    thm option -> thm list -> int -> cases_tactic
    1.24 +  val induct_tac: Proof.context -> (string option * term) option list list ->
    1.25 +    (string * typ) list list -> term option list -> thm list option ->
    1.26 +    thm list -> int -> cases_tactic
    1.27 +  val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
    1.28 +    thm list -> int -> cases_tactic
    1.29    val setup: theory -> theory
    1.30  end;
    1.31  
    1.32 @@ -304,16 +304,6 @@
    1.33    | trace_rules ctxt _ rules = Method.trace ctxt rules;
    1.34  
    1.35  
    1.36 -(* make_cases *)
    1.37 -
    1.38 -fun make_cases is_open rule =
    1.39 -  RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
    1.40 -
    1.41 -fun warn_open true =
    1.42 -      legacy_feature ("Open rule cases in proof method" ^ Position.str_of (Position.thread_data ()))
    1.43 -  | warn_open false = ();
    1.44 -
    1.45 -
    1.46  
    1.47  (** cases method **)
    1.48  
    1.49 @@ -335,9 +325,8 @@
    1.50  
    1.51  in
    1.52  
    1.53 -fun cases_tac ctxt is_open insts opt_rule facts =
    1.54 +fun cases_tac ctxt insts opt_rule facts =
    1.55    let
    1.56 -    val _ = warn_open is_open;
    1.57      val thy = ProofContext.theory_of ctxt;
    1.58      val cert = Thm.cterm_of thy;
    1.59  
    1.60 @@ -359,7 +348,7 @@
    1.61        ruleq
    1.62        |> Seq.maps (RuleCases.consume [] facts)
    1.63        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
    1.64 -        CASES (make_cases is_open rule cases)
    1.65 +        CASES (RuleCases.make_common false (thy, Thm.prop_of rule) cases)
    1.66            (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
    1.67    end;
    1.68  
    1.69 @@ -575,9 +564,8 @@
    1.70  
    1.71  in
    1.72  
    1.73 -fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
    1.74 +fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
    1.75    let
    1.76 -    val _ = warn_open is_open;
    1.77      val thy = ProofContext.theory_of ctxt;
    1.78      val cert = Thm.cterm_of thy;
    1.79  
    1.80 @@ -603,7 +591,7 @@
    1.81            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
    1.82  
    1.83      fun rule_cases rule =
    1.84 -      RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule);
    1.85 +      RuleCases.make_nested false (Thm.prop_of rule) (rulified_term rule);
    1.86    in
    1.87      (fn i => fn st =>
    1.88        ruleq
    1.89 @@ -651,9 +639,8 @@
    1.90  
    1.91  in
    1.92  
    1.93 -fun coinduct_tac ctxt is_open inst taking opt_rule facts =
    1.94 +fun coinduct_tac ctxt inst taking opt_rule facts =
    1.95    let
    1.96 -    val _ = warn_open is_open;
    1.97      val thy = ProofContext.theory_of ctxt;
    1.98      val cert = Thm.cterm_of thy;
    1.99  
   1.100 @@ -677,7 +664,7 @@
   1.101          guess_instance rule i st
   1.102          |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
   1.103          |> Seq.maps (fn rule' =>
   1.104 -          CASES (make_cases is_open rule' cases)
   1.105 +          CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
   1.106              (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
   1.107    end;
   1.108  
   1.109 @@ -687,7 +674,6 @@
   1.110  
   1.111  (** concrete syntax **)
   1.112  
   1.113 -val openN = "open";
   1.114  val arbitraryN = "arbitrary";
   1.115  val takingN = "taking";
   1.116  val ruleN = "rule";
   1.117 @@ -736,26 +722,23 @@
   1.118  in
   1.119  
   1.120  fun cases_meth src =
   1.121 -  Method.syntax (Args.mode openN --
   1.122 -    (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src
   1.123 -  #> (fn ((is_open, (insts, opt_rule)), ctxt) =>
   1.124 +  Method.syntax (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
   1.125 +  #> (fn ((insts, opt_rule), ctxt) =>
   1.126      Method.METHOD_CASES (fn facts =>
   1.127 -      Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts))));
   1.128 +      Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
   1.129  
   1.130  fun induct_meth src =
   1.131 -  Method.syntax (Args.mode openN --
   1.132 -    (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
   1.133 -    (arbitrary -- taking -- Scan.option induct_rule))) src
   1.134 -  #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) =>
   1.135 +  Method.syntax (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
   1.136 +    (arbitrary -- taking -- Scan.option induct_rule)) src
   1.137 +  #> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) =>
   1.138      Method.RAW_METHOD_CASES (fn facts =>
   1.139 -      Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts))));
   1.140 +      Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
   1.141  
   1.142  fun coinduct_meth src =
   1.143 -  Method.syntax (Args.mode openN --
   1.144 -    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src
   1.145 -  #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) =>
   1.146 +  Method.syntax (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule) src
   1.147 +  #> (fn (((insts, taking), opt_rule), ctxt) =>
   1.148      Method.RAW_METHOD_CASES (fn facts =>
   1.149 -      Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts))));
   1.150 +      Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
   1.151  
   1.152  end;
   1.153