|
1 (* @chunk SIMPLE_INDUCTIVE_PACKAGE *) |
|
2 signature SIMPLE_INDUCTIVE_PACKAGE = |
|
3 sig |
|
4 val add_inductive_i: |
|
5 ((Binding.binding * typ) * mixfix) list -> (*{predicates}*) |
|
6 (Binding.binding * typ) list -> (*{parameters}*) |
|
7 (Attrib.binding * term) list -> (*{rules}*) |
|
8 local_theory -> local_theory |
|
9 |
|
10 val add_inductive: |
|
11 (Binding.binding * string option * mixfix) list -> (*{predicates}*) |
|
12 (Binding.binding * string option * mixfix) list -> (*{parameters}*) |
|
13 (Attrib.binding * string) list -> (*{rules}*) |
|
14 local_theory -> local_theory |
|
15 end; |
|
16 (* @end *) |
|
17 |
|
18 structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE = |
|
19 struct |
|
20 |
|
21 (* @chunk make_definitions *) |
|
22 fun make_defs ((binding, syn), trm) lthy = |
|
23 let |
|
24 val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
|
25 val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy |
|
26 in |
|
27 (thm, lthy) |
|
28 end |
|
29 (* @end *) |
|
30 |
|
31 (* @chunk definitions_aux *) |
|
32 fun defs_aux lthy orules preds params (pred, arg_types) = |
|
33 let |
|
34 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P |
|
35 |
|
36 val fresh_args = |
|
37 arg_types |
|
38 |> map (pair "z") |
|
39 |> Variable.variant_frees lthy orules |
|
40 |> map Free |
|
41 in |
|
42 list_comb (pred, fresh_args) |
|
43 |> fold_rev (curry HOLogic.mk_imp) orules |
|
44 |> fold_rev mk_all preds |
|
45 |> fold_rev lambda (params @ fresh_args) |
|
46 end |
|
47 (* @end *) |
|
48 |
|
49 (* @chunk definitions *) |
|
50 fun definitions rules params preds prednames syns arg_typess lthy = |
|
51 let |
|
52 val thy = ProofContext.theory_of lthy |
|
53 val orules = map (ObjectLogic.atomize_term thy) rules |
|
54 val defs = |
|
55 map (defs_aux lthy orules preds params) (preds ~~ arg_typess) |
|
56 in |
|
57 fold_map make_defs (prednames ~~ syns ~~ defs) lthy |
|
58 end |
|
59 (* @end *) |
|
60 |
|
61 fun inst_spec ct = |
|
62 Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}; |
|
63 |
|
64 (* @chunk induction_tac *) |
|
65 fun induction_tac defs prems insts = |
|
66 EVERY1 [ObjectLogic.full_atomize_tac, |
|
67 cut_facts_tac prems, |
|
68 K (rewrite_goals_tac defs), |
|
69 EVERY' (map (dtac o inst_spec) insts), |
|
70 assume_tac] |
|
71 (* @end *) |
|
72 |
|
73 (* @chunk induction_rules *) |
|
74 fun inductions rules defs parnames preds Tss lthy1 = |
|
75 let |
|
76 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
|
77 |
|
78 val Ps = replicate (length preds) "P" |
|
79 val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2 |
|
80 |
|
81 val thy = ProofContext.theory_of lthy3 |
|
82 |
|
83 val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss |
|
84 val newpreds = map Free (newprednames ~~ Tss') |
|
85 val cnewpreds = map (cterm_of thy) newpreds |
|
86 val rules' = map (subst_free (preds ~~ newpreds)) rules |
|
87 |
|
88 fun prove_induction ((pred, newpred), Ts) = |
|
89 let |
|
90 val (newargnames, lthy4) = |
|
91 Variable.variant_fixes (replicate (length Ts) "z") lthy3; |
|
92 val newargs = map Free (newargnames ~~ Ts) |
|
93 |
|
94 val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs)) |
|
95 val goal = Logic.list_implies |
|
96 (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs))) |
|
97 in |
|
98 Goal.prove lthy4 [] [prem] goal |
|
99 (fn {prems, ...} => induction_tac defs prems cnewpreds) |
|
100 |> singleton (ProofContext.export lthy4 lthy1) |
|
101 end |
|
102 in |
|
103 map prove_induction (preds ~~ newpreds ~~ Tss) |
|
104 end |
|
105 (* @end *) |
|
106 |
|
107 val all_elims = fold (fn ct => fn th => th RS inst_spec ct); |
|
108 val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp}); |
|
109 |
|
110 |
|
111 (* @chunk subproof1 *) |
|
112 fun subproof2 prem params2 prems2 = |
|
113 SUBPROOF (fn {prems, ...} => |
|
114 let |
|
115 val prem' = prems MRS prem; |
|
116 val prem'' = |
|
117 case prop_of prem' of |
|
118 _ $ (Const (@{const_name All}, _) $ _) => |
|
119 prem' |> all_elims params2 |
|
120 |> imp_elims prems2 |
|
121 | _ => prem'; |
|
122 in |
|
123 rtac prem'' 1 |
|
124 end) |
|
125 (* @end *) |
|
126 |
|
127 (* @chunk subproof2 *) |
|
128 fun subproof1 rules preds i = |
|
129 SUBPROOF (fn {params, prems, context = ctxt', ...} => |
|
130 let |
|
131 val (prems1, prems2) = chop (length prems - length rules) prems; |
|
132 val (params1, params2) = chop (length params - length preds) params; |
|
133 in |
|
134 rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 |
|
135 THEN |
|
136 EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1) |
|
137 end) |
|
138 (* @end *) |
|
139 |
|
140 fun introductions_tac defs rules preds i ctxt = |
|
141 EVERY1 [ObjectLogic.rulify_tac, |
|
142 K (rewrite_goals_tac defs), |
|
143 REPEAT o (resolve_tac [@{thm allI},@{thm impI}]), |
|
144 subproof1 rules preds i ctxt] |
|
145 |
|
146 |
|
147 (* @chunk intro_rules *) |
|
148 fun introductions rules parnames preds defs lthy1 = |
|
149 let |
|
150 val (_, lthy2) = Variable.add_fixes parnames lthy1 |
|
151 |
|
152 fun prove_intro (i, goal) = |
|
153 Goal.prove lthy2 [] [] goal |
|
154 (fn {context, ...} => introductions_tac defs rules preds i context) |
|
155 |> singleton (ProofContext.export lthy2 lthy1) |
|
156 in |
|
157 map_index prove_intro rules |
|
158 end |
|
159 (* @end *) |
|
160 |
|
161 (* @chunk add_inductive_i *) |
|
162 fun add_inductive_i preds params specs lthy = |
|
163 let |
|
164 val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params; |
|
165 val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds; |
|
166 val Tss = map (binder_types o fastype_of) preds'; |
|
167 val (ass, rules) = split_list specs; (* FIXME: ass not used? *) |
|
168 |
|
169 val prednames = map (fst o fst) preds |
|
170 val syns = map snd preds |
|
171 val parnames = map (Binding.name_of o fst) params |
|
172 |
|
173 val (defs, lthy1) = definitions rules params' preds' prednames syns Tss lthy; |
|
174 |
|
175 val inducts = inductions rules defs parnames preds' Tss lthy1 |
|
176 |
|
177 val intros = introductions rules parnames preds' defs lthy1 |
|
178 |
|
179 val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds); |
|
180 val case_names = map (Binding.name_of o fst o fst) specs |
|
181 in |
|
182 lthy1 |
|
183 |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) => |
|
184 ((Binding.qualify false mut_name a, atts), [([th], [])])) (specs ~~ intros)) |
|
185 |-> (fn intross => LocalTheory.note Thm.theoremK |
|
186 ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) |
|
187 |>> snd |
|
188 ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) => |
|
189 ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"), |
|
190 [Attrib.internal (K (RuleCases.case_names case_names)), |
|
191 Attrib.internal (K (RuleCases.consumes 1)), |
|
192 Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])])) |
|
193 (preds ~~ inducts)) #>> maps snd) |
|
194 |> snd |
|
195 end |
|
196 (* @end *) |
|
197 |
|
198 (* @chunk read_specification *) |
|
199 fun read_specification' vars specs lthy = |
|
200 let |
|
201 val specs' = map (fn (a, s) => (a, [s])) specs |
|
202 val ((varst, specst), _) = |
|
203 Specification.read_specification vars specs' lthy |
|
204 val specst' = map (apsnd the_single) specst |
|
205 in |
|
206 (varst, specst') |
|
207 end |
|
208 (* @end *) |
|
209 |
|
210 (* @chunk add_inductive *) |
|
211 fun add_inductive preds params specs lthy = |
|
212 let |
|
213 val (vars, specs') = read_specification' (preds @ params) specs lthy; |
|
214 val (preds', params') = chop (length preds) vars; |
|
215 val params'' = map fst params' |
|
216 in |
|
217 add_inductive_i preds' params'' specs' lthy |
|
218 end; |
|
219 (* @end *) |
|
220 |
|
221 (* @chunk parser *) |
|
222 val spec_parser = |
|
223 OuterParse.opt_target -- |
|
224 OuterParse.fixes -- |
|
225 OuterParse.for_fixes -- |
|
226 Scan.optional |
|
227 (OuterParse.$$$ "where" |-- |
|
228 OuterParse.!!! |
|
229 (OuterParse.enum1 "|" |
|
230 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) [] |
|
231 (* @end *) |
|
232 |
|
233 (* @chunk syntax *) |
|
234 val specification = |
|
235 spec_parser >> |
|
236 (fn (((loc, preds), params), specs) => |
|
237 Toplevel.local_theory loc (add_inductive preds params specs)) |
|
238 |
|
239 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
|
240 OuterKeyword.thy_decl specification |
|
241 (* @end *) |
|
242 |
|
243 end; |