src/Tools/induct.ML
changeset 30722 623d4831c8cf
parent 30560 0cc3b7f03ade
child 32032 a6a6e8031c14
     1.1 --- a/src/Tools/induct.ML	Wed Mar 25 21:35:49 2009 +0100
     1.2 +++ b/src/Tools/induct.ML	Thu Mar 26 14:14:02 2009 +0100
     1.3 @@ -259,16 +259,15 @@
     1.4    spec setN Args.const >> add_pred ||
     1.5    Scan.lift Args.del >> K del;
     1.6  
     1.7 -val cases_att = attrib cases_type cases_pred cases_del;
     1.8 -val induct_att = attrib induct_type induct_pred induct_del;
     1.9 -val coinduct_att = attrib coinduct_type coinduct_pred coinduct_del;
    1.10 -
    1.11  in
    1.12  
    1.13  val attrib_setup =
    1.14 -  Attrib.setup @{binding cases} cases_att "declaration of cases rule" #>
    1.15 -  Attrib.setup @{binding induct} induct_att "declaration of induction rule" #>
    1.16 -  Attrib.setup @{binding coinduct} coinduct_att "declaration of coinduction rule";
    1.17 +  Attrib.setup @{binding cases} (attrib cases_type cases_pred cases_del)
    1.18 +    "declaration of cases rule" #>
    1.19 +  Attrib.setup @{binding induct} (attrib induct_type induct_pred induct_del)
    1.20 +    "declaration of induction rule" #>
    1.21 +  Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del)
    1.22 +    "declaration of coinduction rule";
    1.23  
    1.24  end;
    1.25  
    1.26 @@ -735,23 +734,29 @@
    1.27  
    1.28  in
    1.29  
    1.30 -val cases_meth =
    1.31 -  P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
    1.32 -  (fn (insts, opt_rule) => fn ctxt =>
    1.33 -    METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts))));
    1.34 +val cases_setup =
    1.35 +  Method.setup @{binding cases}
    1.36 +    (P.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule >>
    1.37 +      (fn (insts, opt_rule) => fn ctxt =>
    1.38 +        METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL (cases_tac ctxt insts opt_rule facts)))))
    1.39 +    "case analysis on types or predicates/sets";
    1.40  
    1.41 -val induct_meth =
    1.42 -  P.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.43 -    (arbitrary -- taking -- Scan.option induct_rule) >>
    1.44 -  (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
    1.45 -    RAW_METHOD_CASES (fn facts =>
    1.46 -      Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts))));
    1.47 +val induct_setup =
    1.48 +  Method.setup @{binding induct}
    1.49 +    (P.and_list' (Scan.repeat (unless_more_args def_inst)) --
    1.50 +      (arbitrary -- taking -- Scan.option induct_rule) >>
    1.51 +      (fn (insts, ((arbitrary, taking), opt_rule)) => fn ctxt =>
    1.52 +        RAW_METHOD_CASES (fn facts =>
    1.53 +          Seq.DETERM (HEADGOAL (induct_tac ctxt insts arbitrary taking opt_rule facts)))))
    1.54 +    "induction on types or predicates/sets";
    1.55  
    1.56 -val coinduct_meth =
    1.57 -  Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
    1.58 -  (fn ((insts, taking), opt_rule) => fn ctxt =>
    1.59 -    RAW_METHOD_CASES (fn facts =>
    1.60 -      Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))));
    1.61 +val coinduct_setup =
    1.62 +  Method.setup @{binding coinduct}
    1.63 +    (Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
    1.64 +      (fn ((insts, taking), opt_rule) => fn ctxt =>
    1.65 +        RAW_METHOD_CASES (fn facts =>
    1.66 +          Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))))
    1.67 +    "coinduction on types or predicates/sets";
    1.68  
    1.69  end;
    1.70  
    1.71 @@ -759,10 +764,6 @@
    1.72  
    1.73  (** theory setup **)
    1.74  
    1.75 -val setup =
    1.76 -  attrib_setup #>
    1.77 -  Method.setup @{binding cases} cases_meth "case analysis on types or predicates/sets" #>
    1.78 -  Method.setup @{binding induct} induct_meth "induction on types or predicates/sets" #>
    1.79 -  Method.setup @{binding coinduct} coinduct_meth "coinduction on types or predicates/sets";
    1.80 +val setup = attrib_setup #> cases_setup  #> induct_setup #> coinduct_setup;
    1.81  
    1.82  end;