src/Pure/Isar/induct_attrib.ML
author wenzelm
Wed Apr 13 18:34:22 2005 +0200 (2005-04-13)
changeset 15703 727ef1b8b3ee
parent 15570 8d8c70b41bab
child 15710 b6b3df30cb0f
permissions -rw-r--r--
*** empty log message ***
     1 (*  Title:      Pure/Isar/induct_attrib.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Declaration of rules for cases and induction.
     6 *)
     7 
     8 signature INDUCT_ATTRIB =
     9 sig
    10   val vars_of: term -> term list
    11   val dest_global_rules: theory ->
    12     {type_cases: (string * thm) list, set_cases: (string * thm) list,
    13       type_induct: (string * thm) list, set_induct: (string * thm) list}
    14   val print_global_rules: theory -> unit
    15   val dest_local_rules: Proof.context ->
    16     {type_cases: (string * thm) list, set_cases: (string * thm) list,
    17       type_induct: (string * thm) list, set_induct: (string * thm) list}
    18   val print_local_rules: Proof.context -> unit
    19   val lookup_casesT : Proof.context -> string -> thm option
    20   val lookup_casesS : Proof.context -> string -> thm option
    21   val lookup_inductT : Proof.context -> string -> thm option
    22   val lookup_inductS : Proof.context -> string -> thm option
    23   val find_casesT: Proof.context -> typ -> thm list
    24   val find_casesS: Proof.context -> thm -> thm list
    25   val find_inductT: Proof.context -> typ -> thm list
    26   val find_inductS: Proof.context -> thm -> thm list
    27   val cases_type_global: string -> theory attribute
    28   val cases_set_global: string -> theory attribute
    29   val cases_type_local: string -> Proof.context attribute
    30   val cases_set_local: string -> Proof.context attribute
    31   val induct_type_global: string -> theory attribute
    32   val induct_set_global: string -> theory attribute
    33   val induct_type_local: string -> Proof.context attribute
    34   val induct_set_local: string -> Proof.context attribute
    35   val casesN: string
    36   val inductN: string
    37   val typeN: string
    38   val setN: string
    39   val setup: (theory -> theory) list
    40 end;
    41 
    42 structure InductAttrib: INDUCT_ATTRIB =
    43 struct
    44 
    45 
    46 (** misc utils **)
    47 
    48 (* encode_type -- for indexing purposes *)
    49 
    50 fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts)
    51   | encode_type (TFree (a, _)) = Free (a, dummyT)
    52   | encode_type (TVar (a, _)) = Var (a, dummyT);
    53 
    54 
    55 (* variables -- ordered left-to-right, preferring right *)
    56 
    57 local
    58 
    59 fun rev_vars_of tm =
    60   Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
    61   |> Library.distinct;
    62 
    63 val mk_var = encode_type o #2 o Term.dest_Var;
    64 
    65 in
    66 
    67 val vars_of = rev o rev_vars_of;
    68 
    69 fun first_var thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
    70   raise THM ("No variables in first premise of rule", 0, [thm]);
    71 
    72 fun last_var thm = mk_var (hd (rev_vars_of (Thm.concl_of thm))) handle Empty =>
    73   raise THM ("No variables in conclusion of rule", 0, [thm]);
    74 
    75 end;
    76 
    77 
    78 
    79 (** global and local induct data **)
    80 
    81 (* rules *)
    82 
    83 type rules = (string * thm) NetRules.T;
    84 
    85 val init_rules =
    86   NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
    87     Drule.eq_thm_prop (th1, th2));
    88 
    89 fun lookup_rule (rs: rules) name = Library.assoc (NetRules.rules rs, name);
    90 
    91 fun print_rules prt kind x rs =
    92   let val thms = map snd (NetRules.rules rs)
    93   in Pretty.writeln (Pretty.big_list kind (map (prt x) thms)) end;
    94 
    95 fun print_all_rules prt x ((casesT, casesS), (inductT, inductS)) =
    96  (print_rules prt "induct type:" x inductT;
    97   print_rules prt "induct set:" x inductS;
    98   print_rules prt "cases type:" x casesT;
    99   print_rules prt "cases set:" x casesS);
   100 
   101 
   102 (* theory data kind 'Isar/induction' *)
   103 
   104 structure GlobalInductArgs =
   105 struct
   106   val name = "Isar/induction";
   107   type T = (rules * rules) * (rules * rules);
   108 
   109   val empty =
   110     ((init_rules (first_var o #2), init_rules (Thm.major_prem_of o #2)),
   111      (init_rules (last_var o #2), init_rules (Thm.major_prem_of o #2)));
   112   val copy = I;
   113   val prep_ext = I;
   114   fun merge (((casesT1, casesS1), (inductT1, inductS1)),
   115       ((casesT2, casesS2), (inductT2, inductS2))) =
   116     ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
   117       (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
   118 
   119   fun print x = print_all_rules Display.pretty_thm_sg x;
   120 
   121   fun dest ((casesT, casesS), (inductT, inductS)) =
   122     {type_cases = NetRules.rules casesT,
   123      set_cases = NetRules.rules casesS,
   124      type_induct = NetRules.rules inductT,
   125      set_induct = NetRules.rules inductS};
   126 end;
   127 
   128 structure GlobalInduct = TheoryDataFun(GlobalInductArgs);
   129 val print_global_rules = GlobalInduct.print;
   130 val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get;
   131 
   132 
   133 (* proof data kind 'Isar/induction' *)
   134 
   135 structure LocalInductArgs =
   136 struct
   137   val name = "Isar/induction";
   138   type T = GlobalInductArgs.T;
   139 
   140   fun init thy = GlobalInduct.get thy;
   141   fun print x = print_all_rules ProofContext.pretty_thm x;
   142 end;
   143 
   144 structure LocalInduct = ProofDataFun(LocalInductArgs);
   145 val print_local_rules = LocalInduct.print;
   146 val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get;
   147 
   148 
   149 (* access rules *)
   150 
   151 val lookup_casesT = lookup_rule o #1 o #1 o LocalInduct.get;
   152 val lookup_casesS = lookup_rule o #2 o #1 o LocalInduct.get;
   153 val lookup_inductT = lookup_rule o #1 o #2 o LocalInduct.get;
   154 val lookup_inductS = lookup_rule o #2 o #2 o LocalInduct.get;
   155 
   156 
   157 fun find_rules which how ctxt x =
   158   map snd (NetRules.retrieve (which (LocalInduct.get ctxt)) (how x));
   159 
   160 val find_casesT = find_rules (#1 o #1) encode_type;
   161 val find_casesS = find_rules (#2 o #1) Thm.concl_of;
   162 val find_inductT = find_rules (#1 o #2) encode_type;
   163 val find_inductS = find_rules (#2 o #2) Thm.concl_of;
   164 
   165 
   166 
   167 (** attributes **)
   168 
   169 local
   170 
   171 fun mk_att f g h name arg =
   172   let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end;
   173 
   174 fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x;
   175 fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x;
   176 fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x;
   177 fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x;
   178 
   179 fun consumes0 x = RuleCases.consumes_default 0 x;
   180 fun consumes1 x = RuleCases.consumes_default 1 x;
   181 
   182 in
   183 
   184 val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0;
   185 val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1;
   186 val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0;
   187 val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1;
   188 
   189 val cases_type_local = mk_att LocalInduct.map add_casesT consumes0;
   190 val cases_set_local = mk_att LocalInduct.map add_casesS consumes1;
   191 val induct_type_local = mk_att LocalInduct.map add_inductT consumes0;
   192 val induct_set_local = mk_att LocalInduct.map add_inductS consumes1;
   193 
   194 end;
   195 
   196 
   197 (** concrete syntax **)
   198 
   199 val casesN = "cases";
   200 val inductN = "induct";
   201 
   202 val typeN = "type";
   203 val setN = "set";
   204 
   205 local
   206 
   207 fun spec k arg =
   208   Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
   209   Scan.lift (Args.$$$ k) >> K "";
   210 
   211 fun attrib tyname const add_type add_set =
   212   Attrib.syntax (spec typeN tyname >> add_type || spec setN const >> add_set);
   213 
   214 in
   215 
   216 val cases_attr =
   217  (attrib Args.global_tyname Args.global_const cases_type_global cases_set_global,
   218   attrib Args.local_tyname Args.local_const cases_type_local cases_set_local);
   219 
   220 val induct_attr =
   221  (attrib Args.global_tyname Args.global_const induct_type_global induct_set_global,
   222   attrib Args.local_tyname Args.local_const induct_type_local induct_set_local);
   223 
   224 end;
   225 
   226 
   227 
   228 (** theory setup **)
   229 
   230 val setup =
   231   [GlobalInduct.init, LocalInduct.init,
   232    Attrib.add_attributes
   233     [(casesN, cases_attr, "declaration of cases rule for type or set"),
   234      (inductN, induct_attr, "declaration of induction rule for type or set")]];
   235 
   236 end;