1 (* Title: HOL/Tools/induct_attrib.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Declaration of rules for cases and induction. |
|
7 *) |
|
8 |
|
9 signature INDUCT_ATTRIB = |
|
10 sig |
|
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 get_cases : Proof.context -> (string * thm) NetRules.T * (string * thm) NetRules.T |
|
20 val get_induct : Proof.context -> (string * thm) NetRules.T * (string * thm) NetRules.T |
|
21 val lookup_casesS : Proof.context -> string -> thm option |
|
22 val lookup_casesT : Proof.context -> string -> thm option |
|
23 val lookup_inductS : Proof.context -> string -> thm option |
|
24 val lookup_inductT : Proof.context -> string -> thm option |
|
25 val cases_type_global: string -> theory attribute |
|
26 val cases_set_global: string -> theory attribute |
|
27 val cases_type_local: string -> Proof.context attribute |
|
28 val cases_set_local: string -> Proof.context attribute |
|
29 val induct_type_global: string -> theory attribute |
|
30 val induct_set_global: string -> theory attribute |
|
31 val induct_type_local: string -> Proof.context attribute |
|
32 val induct_set_local: string -> Proof.context attribute |
|
33 val casesN: string |
|
34 val inductN: string |
|
35 val typeN: string |
|
36 val setN: string |
|
37 val setup: (theory -> theory) list |
|
38 end; |
|
39 |
|
40 structure InductAttrib: INDUCT_ATTRIB = |
|
41 struct |
|
42 |
|
43 |
|
44 (** global and local induct data **) |
|
45 |
|
46 (* rules *) |
|
47 |
|
48 type rules = (string * thm) NetRules.T; |
|
49 |
|
50 fun eq_rule ((s1:string, th1), (s2, th2)) = s1 = s2 andalso Thm.eq_thm (th1, th2); |
|
51 |
|
52 val type_rules = NetRules.init eq_rule (Thm.concl_of o #2); |
|
53 val set_rules = NetRules.init eq_rule (Thm.major_prem_of o #2); |
|
54 |
|
55 fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name); |
|
56 |
|
57 fun print_rules kind sg rs = |
|
58 let val thms = map snd (NetRules.rules rs) |
|
59 in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end; |
|
60 |
|
61 |
|
62 (* theory data kind 'HOL/induction' *) |
|
63 |
|
64 structure GlobalInductArgs = |
|
65 struct |
|
66 val name = "HOL/induction"; |
|
67 type T = (rules * rules) * (rules * rules); |
|
68 |
|
69 val empty = ((type_rules, set_rules), (type_rules, set_rules)); |
|
70 val copy = I; |
|
71 val prep_ext = I; |
|
72 fun merge (((casesT1, casesS1), (inductT1, inductS1)), |
|
73 ((casesT2, casesS2), (inductT2, inductS2))) = |
|
74 ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)), |
|
75 (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2))); |
|
76 |
|
77 fun print sg ((casesT, casesS), (inductT, inductS)) = |
|
78 (print_rules "type cases:" sg casesT; |
|
79 print_rules "set cases:" sg casesS; |
|
80 print_rules "type induct:" sg inductT; |
|
81 print_rules "set induct:" sg inductS); |
|
82 |
|
83 fun dest ((casesT, casesS), (inductT, inductS)) = |
|
84 {type_cases = NetRules.rules casesT, |
|
85 set_cases = NetRules.rules casesS, |
|
86 type_induct = NetRules.rules inductT, |
|
87 set_induct = NetRules.rules inductS}; |
|
88 end; |
|
89 |
|
90 structure GlobalInduct = TheoryDataFun(GlobalInductArgs); |
|
91 val print_global_rules = GlobalInduct.print; |
|
92 val dest_global_rules = GlobalInductArgs.dest o GlobalInduct.get; |
|
93 |
|
94 |
|
95 (* proof data kind 'HOL/induction' *) |
|
96 |
|
97 structure LocalInductArgs = |
|
98 struct |
|
99 val name = "HOL/induction"; |
|
100 type T = GlobalInductArgs.T; |
|
101 |
|
102 fun init thy = GlobalInduct.get thy; |
|
103 fun print x = GlobalInductArgs.print (ProofContext.sign_of x); |
|
104 end; |
|
105 |
|
106 structure LocalInduct = ProofDataFun(LocalInductArgs); |
|
107 val print_local_rules = LocalInduct.print; |
|
108 val dest_local_rules = GlobalInductArgs.dest o LocalInduct.get; |
|
109 |
|
110 |
|
111 (* access rules *) |
|
112 |
|
113 val get_cases = #1 o LocalInduct.get; |
|
114 val get_induct = #2 o LocalInduct.get; |
|
115 |
|
116 val lookup_casesT = lookup_rule o #1 o get_cases; |
|
117 val lookup_casesS = lookup_rule o #2 o get_cases; |
|
118 val lookup_inductT = lookup_rule o #1 o get_induct; |
|
119 val lookup_inductS = lookup_rule o #2 o get_induct; |
|
120 |
|
121 |
|
122 |
|
123 (** attributes **) |
|
124 |
|
125 local |
|
126 |
|
127 fun mk_att f g h name arg = |
|
128 let val (x, thm) = h arg in (f (g (name, thm)) x, thm) end; |
|
129 |
|
130 fun add_casesT rule x = apfst (apfst (NetRules.insert rule)) x; |
|
131 fun add_casesS rule x = apfst (apsnd (NetRules.insert rule)) x; |
|
132 fun add_inductT rule x = apsnd (apfst (NetRules.insert rule)) x; |
|
133 fun add_inductS rule x = apsnd (apsnd (NetRules.insert rule)) x; |
|
134 |
|
135 fun consumes0 x = RuleCases.consumes_default 0 x; |
|
136 fun consumes1 x = RuleCases.consumes_default 1 x; |
|
137 |
|
138 in |
|
139 |
|
140 val cases_type_global = mk_att GlobalInduct.map add_casesT consumes0; |
|
141 val cases_set_global = mk_att GlobalInduct.map add_casesS consumes1; |
|
142 val induct_type_global = mk_att GlobalInduct.map add_inductT consumes0; |
|
143 val induct_set_global = mk_att GlobalInduct.map add_inductS consumes1; |
|
144 |
|
145 val cases_type_local = mk_att LocalInduct.map add_casesT consumes0; |
|
146 val cases_set_local = mk_att LocalInduct.map add_casesS consumes1; |
|
147 val induct_type_local = mk_att LocalInduct.map add_inductT consumes0; |
|
148 val induct_set_local = mk_att LocalInduct.map add_inductS consumes1; |
|
149 |
|
150 end; |
|
151 |
|
152 |
|
153 (** concrete syntax **) |
|
154 |
|
155 val casesN = "cases"; |
|
156 val inductN = "induct"; |
|
157 |
|
158 val typeN = "type"; |
|
159 val setN = "set"; |
|
160 |
|
161 local |
|
162 |
|
163 fun spec k = (Args.$$$ k -- Args.colon) |-- Args.!!! Args.name; |
|
164 |
|
165 fun attrib sign_of add_type add_set = Scan.depend (fn x => |
|
166 let val sg = sign_of x in |
|
167 spec typeN >> (add_type o Sign.certify_tycon sg o Sign.intern_tycon sg) || |
|
168 spec setN >> (add_set o Sign.certify_const sg o Sign.intern_const sg) |
|
169 end >> pair x); |
|
170 |
|
171 in |
|
172 |
|
173 val cases_attr = |
|
174 (Attrib.syntax (attrib Theory.sign_of cases_type_global cases_set_global), |
|
175 Attrib.syntax (attrib ProofContext.sign_of cases_type_local cases_set_local)); |
|
176 |
|
177 val induct_attr = |
|
178 (Attrib.syntax (attrib Theory.sign_of induct_type_global induct_set_global), |
|
179 Attrib.syntax (attrib ProofContext.sign_of induct_type_local induct_set_local)); |
|
180 |
|
181 end; |
|
182 |
|
183 |
|
184 |
|
185 (** theory setup **) |
|
186 |
|
187 val setup = |
|
188 [GlobalInduct.init, LocalInduct.init, |
|
189 Attrib.add_attributes |
|
190 [(casesN, cases_attr, "declaration of cases rule for type or set"), |
|
191 (inductN, induct_attr, "declaration of induction rule for type or set")]]; |
|
192 |
|
193 end; |
|