src/Tools/induct.ML
changeset 58826 2ed2eaabe3df
parent 58002 0ed1e999a0fb
child 58838 59203adfc33f
     1.1 --- a/src/Tools/induct.ML	Wed Oct 29 17:01:44 2014 +0100
     1.2 +++ b/src/Tools/induct.ML	Wed Oct 29 19:01:49 2014 +0100
     1.3 @@ -89,7 +89,6 @@
     1.4      (string * typ) list list -> term option list -> thm list option ->
     1.5      thm list -> int -> cases_tactic) ->
     1.6     theory -> theory
     1.7 -  val setup: theory -> theory
     1.8  end;
     1.9  
    1.10  functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
    1.11 @@ -368,15 +367,16 @@
    1.12  
    1.13  in
    1.14  
    1.15 -val attrib_setup =
    1.16 -  Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
    1.17 -    "declaration of cases rule" #>
    1.18 -  Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
    1.19 -    "declaration of induction rule" #>
    1.20 -  Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
    1.21 -    "declaration of coinduction rule" #>
    1.22 -  Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
    1.23 -    "declaration of rules for simplifying induction or cases rules";
    1.24 +val _ =
    1.25 +  Theory.setup
    1.26 +   (Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
    1.27 +      "declaration of cases rule" #>
    1.28 +    Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
    1.29 +      "declaration of induction rule" #>
    1.30 +    Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
    1.31 +      "declaration of coinduction rule" #>
    1.32 +    Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del)
    1.33 +      "declaration of rules for simplifying induction or cases rules");
    1.34  
    1.35  end;
    1.36  
    1.37 @@ -923,14 +923,15 @@
    1.38  
    1.39  in
    1.40  
    1.41 -val cases_setup =
    1.42 -  Method.setup @{binding cases}
    1.43 -    (Scan.lift (Args.mode no_simpN) --
    1.44 -      (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
    1.45 -      (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
    1.46 -        METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
    1.47 -          (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
    1.48 -    "case analysis on types or predicates/sets";
    1.49 +val _ =
    1.50 +  Theory.setup
    1.51 +    (Method.setup @{binding cases}
    1.52 +      (Scan.lift (Args.mode no_simpN) --
    1.53 +        (Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
    1.54 +        (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
    1.55 +          METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
    1.56 +            (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
    1.57 +      "case analysis on types or predicates/sets");
    1.58  
    1.59  fun gen_induct_setup binding tac =
    1.60    Method.setup binding
    1.61 @@ -941,21 +942,16 @@
    1.62          Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
    1.63      "induction on types or predicates/sets";
    1.64  
    1.65 -val induct_setup = gen_induct_setup @{binding induct} induct_tac;
    1.66 +val _ = Theory.setup (gen_induct_setup @{binding induct} induct_tac);
    1.67  
    1.68 -val coinduct_setup =
    1.69 -  Method.setup @{binding coinduct}
    1.70 -    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
    1.71 -      (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
    1.72 -        Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
    1.73 -    "coinduction on types or predicates/sets";
    1.74 +val _ =
    1.75 +  Theory.setup
    1.76 +    (Method.setup @{binding coinduct}
    1.77 +      (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
    1.78 +        (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
    1.79 +          Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
    1.80 +      "coinduction on types or predicates/sets");
    1.81  
    1.82  end;
    1.83  
    1.84 -
    1.85 -
    1.86 -(** theory setup **)
    1.87 -
    1.88 -val setup = attrib_setup #> cases_setup  #> induct_setup #> coinduct_setup;
    1.89 -
    1.90  end;