src/Tools/induct.ML

 (*  Title:      Tools/induct.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Proof by cases and induction.
+Proof by cases, induction, and coinduction.
 *)
 
 signature INDUCT_DATA =
 sig
   val cases_default: thm

   val inner_atomize_tac: int -> tactic
   val rulified_term: thm -> theory * term
   val rulify_tac: int -> tactic
   val internalize: int -> thm -> thm
   val guess_instance: thm -> int -> thm -> thm Seq.seq
-  val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
+  val cases_tac: Proof.context -> term option list list -> thm option ->
     thm list -> int -> cases_tactic
-  val induct_tac: Proof.context -> bool -> (string option * term) option list list ->
-    (string * typ) list list -> term option list -> thm list option -> thm list -> int ->
-    cases_tactic
-  val coinduct_tac: Proof.context -> bool -> term option list -> term option list ->
-    thm option -> thm list -> int -> cases_tactic
+  val induct_tac: Proof.context -> (string option * term) 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 setup: theory -> theory
 end;
 
 functor InductFun(Data: INDUCT_DATA): INDUCT =
 struct

 
 fun trace_rules _ kind [] = error ("Unable to figure out " ^ kind ^ " rule")
   | trace_rules ctxt _ rules = Method.trace ctxt rules;
 
 
-(* make_cases *)
-
-fun make_cases is_open rule =
-  RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
-
-fun warn_open true =
-      legacy_feature ("Open rule cases in proof method" ^ Position.str_of (Position.thread_data ()))
-  | warn_open false = ();
-
-
 
 (** cases method **)
 
 (*
   rule selection scheme:

 fun get_casesP ctxt (fact :: _) = find_casesP ctxt (Thm.concl_of fact)
   | get_casesP _ _ = [];
 
 in
 
-fun cases_tac ctxt is_open insts opt_rule facts =
-  let
-    val _ = warn_open is_open;
+fun cases_tac ctxt insts opt_rule facts =
+  let
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
     fun inst_rule r =
       if null insts then `RuleCases.get r

   in
     fn i => fn st =>
       ruleq
       |> Seq.maps (RuleCases.consume [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
-        CASES (make_cases is_open rule cases)
+        CASES (RuleCases.make_common false (thy, Thm.prop_of rule) cases)
           (Method.insert_tac more_facts i THEN Tactic.rtac rule i) st)
   end;
 
 end;
 

 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];
 
 in
 
-fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
-  let
-    val _ = warn_open is_open;
+fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
+  let
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
     val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
     val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;

           |> map_filter (RuleCases.mutual_rule ctxt)
           |> tap (trace_rules ctxt inductN o map #2)
           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
 
     fun rule_cases rule =
-      RuleCases.make_nested is_open (Thm.prop_of rule) (rulified_term rule);
+      RuleCases.make_nested false (Thm.prop_of rule) (rulified_term rule);
   in
     (fn i => fn st =>
       ruleq
       |> Seq.maps (RuleCases.consume (flat defs) facts)
       |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>

 fun main_prop_of th =
   if RuleCases.get_consumes th > 0 then Thm.major_prem_of th else Thm.concl_of th;
 
 in
 
-fun coinduct_tac ctxt is_open inst taking opt_rule facts =
-  let
-    val _ = warn_open is_open;
+fun coinduct_tac ctxt inst taking opt_rule facts =
+  let
     val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
 
     fun inst_rule r =
       if null inst then `RuleCases.get r

       |> Seq.maps (RuleCases.consume [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
         guess_instance rule i st
         |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
         |> Seq.maps (fn rule' =>
-          CASES (make_cases is_open rule' cases)
+          CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
             (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
   end;
 
 end;
 
 
 
 (** concrete syntax **)
 
-val openN = "open";
 val arbitraryN = "arbitrary";
 val takingN = "taking";
 val ruleN = "rule";
 
 local

   Scan.repeat1 (unless_more_args inst)) [];
 
 in
 
 fun cases_meth src =
-  Method.syntax (Args.mode openN --
-    (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule)) src
-  #> (fn ((is_open, (insts, opt_rule)), ctxt) =>
+  Method.syntax (Args.and_list (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) src
+  #> (fn ((insts, opt_rule), ctxt) =>
     Method.METHOD_CASES (fn facts =>
-      Seq.DETERM (HEADGOAL (cases_tac ctxt is_open insts opt_rule facts))));
+      Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
 
 fun induct_meth src =
-  Method.syntax (Args.mode openN --
-    (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
-    (arbitrary -- taking -- Scan.option induct_rule))) src
-  #> (fn ((is_open, (insts, ((arbitrary, taking), opt_rule))), ctxt) =>
+  Method.syntax (Args.and_list (Scan.repeat (unless_more_args def_inst)) --
+    (arbitrary -- taking -- Scan.option induct_rule)) src
+  #> (fn ((insts, ((arbitrary, taking), opt_rule)), ctxt) =>
     Method.RAW_METHOD_CASES (fn facts =>
-      Seq.DETERM (HEADGOAL (induct_tac ctxt is_open insts arbitrary taking opt_rule facts))));
+      Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
 
 fun coinduct_meth src =
-  Method.syntax (Args.mode openN --
-    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule)) src
-  #> (fn ((is_open, ((insts, taking), opt_rule)), ctxt) =>
+  Method.syntax (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule) src
+  #> (fn (((insts, taking), opt_rule), ctxt) =>
     Method.RAW_METHOD_CASES (fn facts =>
-      Seq.DETERM (HEADGOAL (coinduct_tac ctxt is_open insts taking opt_rule facts))));
+      Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
 
 end;