wenzelm@11658: (*  Title:      Pure/Isar/induct_attrib.ML
wenzelm@11656:     ID:         $Id$
wenzelm@11656:     Author:     Markus Wenzel, TU Muenchen
wenzelm@11656: 
wenzelm@11656: Declaration of rules for cases and induction.
wenzelm@11656: *)
wenzelm@11656: 
wenzelm@11656: signature INDUCT_ATTRIB =
wenzelm@11656: sig
wenzelm@11730:   val vars_of: term -> term list
wenzelm@21506:   val dest_rules: Proof.context ->
wenzelm@11656:     {type_cases: (string * thm) list, set_cases: (string * thm) list,
wenzelm@18210:       type_induct: (string * thm) list, set_induct: (string * thm) list,
wenzelm@18210:       type_coinduct: (string * thm) list, set_coinduct: (string * thm) list}
wenzelm@21506:   val print_rules: Proof.context -> unit
wenzelm@11730:   val lookup_casesT : Proof.context -> string -> thm option
wenzelm@11656:   val lookup_casesS : Proof.context -> string -> thm option
wenzelm@11730:   val lookup_inductT : Proof.context -> string -> thm option
wenzelm@11656:   val lookup_inductS : Proof.context -> string -> thm option
wenzelm@18210:   val lookup_coinductT : Proof.context -> string -> thm option
wenzelm@18210:   val lookup_coinductS : Proof.context -> string -> thm option
wenzelm@11730:   val find_casesT: Proof.context -> typ -> thm list
wenzelm@18226:   val find_casesS: Proof.context -> term -> thm list
wenzelm@11730:   val find_inductT: Proof.context -> typ -> thm list
wenzelm@18226:   val find_inductS: Proof.context -> term -> thm list
wenzelm@18210:   val find_coinductT: Proof.context -> typ -> thm list
wenzelm@18226:   val find_coinductS: Proof.context -> term -> thm list
wenzelm@18728:   val cases_type: string -> attribute
wenzelm@18728:   val cases_set: string -> attribute
wenzelm@18728:   val induct_type: string -> attribute
wenzelm@18728:   val induct_set: string -> attribute
wenzelm@18728:   val coinduct_type: string -> attribute
wenzelm@18728:   val coinduct_set: string -> attribute
wenzelm@11656:   val casesN: string
wenzelm@11656:   val inductN: string
wenzelm@18210:   val coinductN: string
wenzelm@11656:   val typeN: string
wenzelm@11656:   val setN: string
wenzelm@11656: end;
wenzelm@11656: 
wenzelm@11656: structure InductAttrib: INDUCT_ATTRIB =
wenzelm@11656: struct
wenzelm@11656: 
wenzelm@11656: 
wenzelm@11730: (** misc utils **)
wenzelm@11730: 
wenzelm@11730: (* encode_type -- for indexing purposes *)
wenzelm@11730: 
wenzelm@11730: fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
wenzelm@11730:   | encode_type (TFree (a, _)) = Free (a, dummyT)
wenzelm@11730:   | encode_type (TVar (a, _)) = Var (a, dummyT);
wenzelm@11730: 
wenzelm@11730: 
wenzelm@11730: (* variables -- ordered left-to-right, preferring right *)
wenzelm@11730: 
wenzelm@18210: fun vars_of tm =
wenzelm@19046:   rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
wenzelm@11730: 
wenzelm@18210: local
wenzelm@11730: 
wenzelm@11730: val mk_var = encode_type o #2 o Term.dest_Var;
wenzelm@11730: 
wenzelm@18210: fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
wenzelm@18210:   raise THM ("No variables in conclusion of rule", 0, [thm]);
wenzelm@18210: 
wenzelm@11730: in
wenzelm@11730: 
wenzelm@18210: fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
wenzelm@18210:   raise THM ("No variables in major premise of rule", 0, [thm]);
wenzelm@11730: 
wenzelm@18210: val left_var_concl = concl_var hd;
wenzelm@18210: val right_var_concl = concl_var List.last;
wenzelm@11730: 
wenzelm@11730: end;
wenzelm@11730: 
wenzelm@11730: 
wenzelm@11730: 
wenzelm@18637: (** induct data **)
wenzelm@11656: 
wenzelm@11656: (* rules *)
wenzelm@11656: 
wenzelm@11656: type rules = (string * thm) NetRules.T;
wenzelm@11656: 
wenzelm@12381: val init_rules =
wenzelm@13105:   NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
wenzelm@22360:     Thm.eq_thm_prop (th1, th2));
wenzelm@11656: 
wenzelm@17184: fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs);
wenzelm@11656: 
wenzelm@18637: fun pretty_rules ctxt kind rs =
wenzelm@11656:   let val thms = map snd (NetRules.rules rs)
wenzelm@18637:   in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end;
wenzelm@11656: 
wenzelm@11656: 
wenzelm@18637: (* context data *)
wenzelm@11656: 
wenzelm@18637: structure Induct = GenericDataFun
wenzelm@18637: (
wenzelm@18210:   type T = (rules * rules) * (rules * rules) * (rules * rules);
wenzelm@11730:   val empty =
wenzelm@18210:     ((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)),
wenzelm@18210:      (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
wenzelm@18210:      (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
wenzelm@16424:   val extend = I;
wenzelm@18210:   fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)),
wenzelm@18210:       ((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) =
wenzelm@11656:     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
wenzelm@18210:       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)),
wenzelm@18210:       (NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2)));
wenzelm@18637: );
wenzelm@11656: 
wenzelm@22846: val get_local = Induct.get o Context.Proof;
wenzelm@11656: 
wenzelm@22846: fun dest_rules ctxt =
wenzelm@22846:   let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
wenzelm@22846:     {type_cases = NetRules.rules casesT,
wenzelm@22846:      set_cases = NetRules.rules casesS,
wenzelm@22846:      type_induct = NetRules.rules inductT,
wenzelm@22846:      set_induct = NetRules.rules inductS,
wenzelm@22846:      type_coinduct = NetRules.rules coinductT,
wenzelm@22846:      set_coinduct = NetRules.rules coinductS}
wenzelm@22846:   end;
wenzelm@22846: 
wenzelm@22846: fun print_rules ctxt =
wenzelm@22846:   let val ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = get_local ctxt in
wenzelm@22846:    [pretty_rules ctxt "coinduct type:" coinductT,
wenzelm@22846:     pretty_rules ctxt "coinduct set:" coinductS,
wenzelm@22846:     pretty_rules ctxt "induct type:" inductT,
wenzelm@22846:     pretty_rules ctxt "induct set:" inductS,
wenzelm@22846:     pretty_rules ctxt "cases type:" casesT,
wenzelm@22846:     pretty_rules ctxt "cases set:" casesS]
wenzelm@22846:     |> Pretty.chunks |> Pretty.writeln
wenzelm@22846:   end;
wenzelm@11656: 
wenzelm@11656: 
wenzelm@11656: (* access rules *)
wenzelm@11656: 
wenzelm@18637: val lookup_casesT = lookup_rule o #1 o #1 o get_local;
wenzelm@18637: val lookup_casesS = lookup_rule o #2 o #1 o get_local;
wenzelm@18637: val lookup_inductT = lookup_rule o #1 o #2 o get_local;
wenzelm@18637: val lookup_inductS = lookup_rule o #2 o #2 o get_local;
wenzelm@18637: val lookup_coinductT = lookup_rule o #1 o #3 o get_local;
wenzelm@18637: val lookup_coinductS = lookup_rule o #2 o #3 o get_local;
wenzelm@11730: 
wenzelm@11656: 
wenzelm@11730: fun find_rules which how ctxt x =
wenzelm@18637:   map snd (NetRules.retrieve (which (get_local ctxt)) (how x));
wenzelm@11730: 
wenzelm@11730: val find_casesT = find_rules (#1 o #1) encode_type;
wenzelm@18226: val find_casesS = find_rules (#2 o #1) I;
wenzelm@11730: val find_inductT = find_rules (#1 o #2) encode_type;
wenzelm@18226: val find_inductS = find_rules (#2 o #2) I;
wenzelm@18210: val find_coinductT = find_rules (#1 o #3) encode_type;
wenzelm@18226: val find_coinductS = find_rules (#2 o #3) I;
wenzelm@11656: 
wenzelm@11656: 
wenzelm@11656: 
wenzelm@11656: (** attributes **)
wenzelm@11656: 
wenzelm@11656: local
wenzelm@11656: 
wenzelm@18637: fun mk_att f g name arg =
wenzelm@18637:   let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end;
wenzelm@11656: 
wenzelm@18210: fun map1 f (x, y, z) = (f x, y, z);
wenzelm@18210: fun map2 f (x, y, z) = (x, f y, z);
wenzelm@18210: fun map3 f (x, y, z) = (x, y, f z);
wenzelm@18210: 
wenzelm@18210: fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x;
wenzelm@18210: fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x;
wenzelm@18210: fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x;
wenzelm@18210: fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x;
wenzelm@18210: fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x;
wenzelm@18210: fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x;
wenzelm@11656: 
wenzelm@11656: fun consumes0 x = RuleCases.consumes_default 0 x;
wenzelm@11656: fun consumes1 x = RuleCases.consumes_default 1 x;
wenzelm@11656: 
wenzelm@11656: in
wenzelm@11656: 
wenzelm@18637: val cases_type = mk_att add_casesT consumes0;
wenzelm@18637: val cases_set = mk_att add_casesS consumes1;
wenzelm@18637: val induct_type = mk_att add_inductT consumes0;
wenzelm@18637: val induct_set = mk_att add_inductS consumes1;
wenzelm@18637: val coinduct_type = mk_att add_coinductT consumes0;
wenzelm@18637: val coinduct_set = mk_att add_coinductS consumes1;
wenzelm@11656: 
wenzelm@11656: end;
wenzelm@11656: 
wenzelm@11656: 
wenzelm@18637: 
wenzelm@11656: (** concrete syntax **)
wenzelm@11656: 
wenzelm@11656: val casesN = "cases";
wenzelm@11656: val inductN = "induct";
wenzelm@18210: val coinductN = "coinduct";
wenzelm@11656: 
wenzelm@11656: val typeN = "type";
wenzelm@11656: val setN = "set";
wenzelm@11656: 
wenzelm@11656: local
wenzelm@11656: 
wenzelm@15703: fun spec k arg =
wenzelm@15703:   Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
wenzelm@15703:   Scan.lift (Args.$$$ k) >> K "";
wenzelm@11656: 
wenzelm@18637: fun attrib add_type add_set =
wenzelm@18637:   Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set);
wenzelm@11656: 
wenzelm@11656: in
wenzelm@11656: 
wenzelm@18637: val cases_att = attrib cases_type cases_set;
wenzelm@18637: val induct_att = attrib induct_type induct_set;
wenzelm@18637: val coinduct_att = attrib coinduct_type coinduct_set;
wenzelm@18210: 
wenzelm@11656: end;
wenzelm@11656: 
wenzelm@15801: val _ = Context.add_setup
wenzelm@18708:  (Attrib.add_attributes
wenzelm@18728:   [(casesN, cases_att, "declaration of cases rule for type or set"),
wenzelm@18728:    (inductN, induct_att, "declaration of induction rule for type or set"),
wenzelm@18728:    (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]);
wenzelm@11656: 
wenzelm@11656: end;