src/Tools/induct.ML
changeset 59940 087d81f5213e
parent 59936 b8ffc3dc9e24
child 59970 e9f73d87d904
     1.1 --- a/src/Tools/induct.ML	Mon Apr 06 22:11:01 2015 +0200
     1.2 +++ b/src/Tools/induct.ML	Mon Apr 06 23:14:05 2015 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4     (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     1.5      (string * typ) list list -> term option list -> thm list option ->
     1.6      thm list -> int -> cases_tactic) ->
     1.7 -   theory -> theory
     1.8 +   local_theory -> local_theory
     1.9  end;
    1.10  
    1.11  functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
    1.12 @@ -363,14 +363,14 @@
    1.13  in
    1.14  
    1.15  val _ =
    1.16 -  Theory.setup
    1.17 -   (Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
    1.18 +  Theory.local_setup
    1.19 +   (Attrib.local_setup @{binding cases} (attrib cases_type cases_pred cases_del)
    1.20        "declaration of cases rule" #>
    1.21 -    Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
    1.22 +    Attrib.local_setup @{binding induct} (attrib induct_type induct_pred induct_del)
    1.23        "declaration of induction rule" #>
    1.24 -    Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
    1.25 +    Attrib.local_setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
    1.26        "declaration of coinduction rule" #>
    1.27 -    Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
    1.28 +    Attrib.local_setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
    1.29        "declaration of rules for simplifying induction or cases rules");
    1.30  
    1.31  end;
    1.32 @@ -737,10 +737,10 @@
    1.33    SUBGOAL_CASES (fn (_, i, st) =>
    1.34      let
    1.35        val thy = Proof_Context.theory_of ctxt;
    1.36 -  
    1.37 +
    1.38        val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
    1.39        val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
    1.40 -  
    1.41 +
    1.42        fun inst_rule (concls, r) =
    1.43          (if null insts then `Rule_Cases.get r
    1.44           else (align_left "Rule has fewer conclusions than arguments given"
    1.45 @@ -749,7 +749,7 @@
    1.46            |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
    1.47          |> mod_cases thy
    1.48          |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
    1.49 -  
    1.50 +
    1.51        val ruleq =
    1.52          (case opt_rule of
    1.53            SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
    1.54 @@ -759,7 +759,7 @@
    1.55              |> map_filter (Rule_Cases.mutual_rule ctxt)
    1.56              |> tap (trace_rules ctxt inductN o map #2)
    1.57              |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
    1.58 -  
    1.59 +
    1.60        fun rule_cases ctxt rule cases =
    1.61          let
    1.62            val rule' = Rule_Cases.internalize_params rule;
    1.63 @@ -910,18 +910,8 @@
    1.64  
    1.65  in
    1.66  
    1.67 -val _ =
    1.68 -  Theory.setup
    1.69 -    (Method.setup @{binding cases}
    1.70 -      (Scan.lift (Args.mode no_simpN) --
    1.71 -        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
    1.72 -        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
    1.73 -          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
    1.74 -            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
    1.75 -      "case analysis on types or predicates/sets");
    1.76 -
    1.77  fun gen_induct_setup binding tac =
    1.78 -  Method.setup binding
    1.79 +  Method.local_setup binding
    1.80      (Scan.lift (Args.mode no_simpN) --
    1.81        (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.82          (arbitrary -- taking -- Scan.option induct_rule)) >>
    1.83 @@ -929,11 +919,17 @@
    1.84          Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
    1.85      "induction on types or predicates/sets";
    1.86  
    1.87 -val _ = Theory.setup (gen_induct_setup @{binding induct} induct_tac);
    1.88 -
    1.89  val _ =
    1.90 -  Theory.setup
    1.91 -    (Method.setup @{binding coinduct}
    1.92 +  Theory.local_setup
    1.93 +    (Method.local_setup @{binding cases}
    1.94 +      (Scan.lift (Args.mode no_simpN) --
    1.95 +        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
    1.96 +        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
    1.97 +          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
    1.98 +            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
    1.99 +      "case analysis on types or predicates/sets" #>
   1.100 +    gen_induct_setup @{binding induct} induct_tac #>
   1.101 +     Method.local_setup @{binding coinduct}
   1.102        (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
   1.103          (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
   1.104            Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))