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