|
1 (* Title: HOL/Tools/Function/induction_schema.ML |
|
2 Author: Alexander Krauss, TU Muenchen |
|
3 |
|
4 A method to prove induction schemas. |
|
5 *) |
|
6 |
|
7 signature INDUCTION_SCHEMA = |
|
8 sig |
|
9 val mk_ind_tac : (int -> tactic) -> (int -> tactic) -> (int -> tactic) |
|
10 -> Proof.context -> thm list -> tactic |
|
11 val induction_schema_tac : Proof.context -> thm list -> tactic |
|
12 val setup : theory -> theory |
|
13 end |
|
14 |
|
15 |
|
16 structure Induction_Schema : INDUCTION_SCHEMA = |
|
17 struct |
|
18 |
|
19 open Function_Lib |
|
20 |
|
21 type rec_call_info = int * (string * typ) list * term list * term list |
|
22 |
|
23 datatype scheme_case = SchemeCase of |
|
24 {bidx : int, |
|
25 qs: (string * typ) list, |
|
26 oqnames: string list, |
|
27 gs: term list, |
|
28 lhs: term list, |
|
29 rs: rec_call_info list} |
|
30 |
|
31 datatype scheme_branch = SchemeBranch of |
|
32 {P : term, |
|
33 xs: (string * typ) list, |
|
34 ws: (string * typ) list, |
|
35 Cs: term list} |
|
36 |
|
37 datatype ind_scheme = IndScheme of |
|
38 {T: typ, (* sum of products *) |
|
39 branches: scheme_branch list, |
|
40 cases: scheme_case list} |
|
41 |
|
42 val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize} |
|
43 val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify} |
|
44 |
|
45 fun meta thm = thm RS eq_reflection |
|
46 |
|
47 val sum_prod_conv = Raw_Simplifier.rewrite true |
|
48 (map meta (@{thm split_conv} :: @{thms sum.cases})) |
|
49 |
|
50 fun term_conv thy cv t = |
|
51 cv (cterm_of thy t) |
|
52 |> prop_of |> Logic.dest_equals |> snd |
|
53 |
|
54 fun mk_relT T = HOLogic.mk_setT (HOLogic.mk_prodT (T, T)) |
|
55 |
|
56 fun dest_hhf ctxt t = |
|
57 let |
|
58 val ((vars, imp), ctxt') = Function_Lib.focus_term t ctxt |
|
59 in |
|
60 (ctxt', vars, Logic.strip_imp_prems imp, Logic.strip_imp_concl imp) |
|
61 end |
|
62 |
|
63 fun mk_scheme' ctxt cases concl = |
|
64 let |
|
65 fun mk_branch concl = |
|
66 let |
|
67 val (_, ws, Cs, _ $ Pxs) = dest_hhf ctxt concl |
|
68 val (P, xs) = strip_comb Pxs |
|
69 in |
|
70 SchemeBranch { P=P, xs=map dest_Free xs, ws=ws, Cs=Cs } |
|
71 end |
|
72 |
|
73 val (branches, cases') = (* correction *) |
|
74 case Logic.dest_conjunctions concl of |
|
75 [conc] => |
|
76 let |
|
77 val _ $ Pxs = Logic.strip_assums_concl conc |
|
78 val (P, _) = strip_comb Pxs |
|
79 val (cases', conds) = |
|
80 take_prefix (Term.exists_subterm (curry op aconv P)) cases |
|
81 val concl' = fold_rev (curry Logic.mk_implies) conds conc |
|
82 in |
|
83 ([mk_branch concl'], cases') |
|
84 end |
|
85 | concls => (map mk_branch concls, cases) |
|
86 |
|
87 fun mk_case premise = |
|
88 let |
|
89 val (ctxt', qs, prems, _ $ Plhs) = dest_hhf ctxt premise |
|
90 val (P, lhs) = strip_comb Plhs |
|
91 |
|
92 fun bidx Q = |
|
93 find_index (fn SchemeBranch {P=P',...} => Q aconv P') branches |
|
94 |
|
95 fun mk_rcinfo pr = |
|
96 let |
|
97 val (_, Gvs, Gas, _ $ Phyp) = dest_hhf ctxt' pr |
|
98 val (P', rcs) = strip_comb Phyp |
|
99 in |
|
100 (bidx P', Gvs, Gas, rcs) |
|
101 end |
|
102 |
|
103 fun is_pred v = exists (fn SchemeBranch {P,...} => v aconv P) branches |
|
104 |
|
105 val (gs, rcprs) = |
|
106 take_prefix (not o Term.exists_subterm is_pred) prems |
|
107 in |
|
108 SchemeCase {bidx=bidx P, qs=qs, oqnames=map fst qs(*FIXME*), |
|
109 gs=gs, lhs=lhs, rs=map mk_rcinfo rcprs} |
|
110 end |
|
111 |
|
112 fun PT_of (SchemeBranch { xs, ...}) = |
|
113 foldr1 HOLogic.mk_prodT (map snd xs) |
|
114 |
|
115 val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) (map PT_of branches) |
|
116 in |
|
117 IndScheme {T=ST, cases=map mk_case cases', branches=branches } |
|
118 end |
|
119 |
|
120 fun mk_completeness ctxt (IndScheme {cases, branches, ...}) bidx = |
|
121 let |
|
122 val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx |
|
123 val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases |
|
124 |
|
125 val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases [] |
|
126 val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs)) |
|
127 val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs |
|
128 |
|
129 fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) = |
|
130 HOLogic.mk_Trueprop Pbool |
|
131 |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l))) |
|
132 (xs' ~~ lhs) |
|
133 |> fold_rev (curry Logic.mk_implies) gs |
|
134 |> fold_rev mk_forall_rename (oqnames ~~ map Free qs) |
|
135 in |
|
136 HOLogic.mk_Trueprop Pbool |
|
137 |> fold_rev (curry Logic.mk_implies o mk_case) relevant_cases |
|
138 |> fold_rev (curry Logic.mk_implies) Cs' |
|
139 |> fold_rev (Logic.all o Free) ws |
|
140 |> fold_rev mk_forall_rename (map fst xs ~~ xs') |
|
141 |> mk_forall_rename ("P", Pbool) |
|
142 end |
|
143 |
|
144 fun mk_wf R (IndScheme {T, ...}) = |
|
145 HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R) |
|
146 |
|
147 fun mk_ineqs R (IndScheme {T, cases, branches}) = |
|
148 let |
|
149 fun inject i ts = |
|
150 SumTree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts) |
|
151 |
|
152 val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *) |
|
153 |
|
154 fun mk_pres bdx args = |
|
155 let |
|
156 val SchemeBranch { xs, ws, Cs, ... } = nth branches bdx |
|
157 fun replace (x, v) t = betapply (lambda (Free x) t, v) |
|
158 val Cs' = map (fold replace (xs ~~ args)) Cs |
|
159 val cse = |
|
160 HOLogic.mk_Trueprop thesis |
|
161 |> fold_rev (curry Logic.mk_implies) Cs' |
|
162 |> fold_rev (Logic.all o Free) ws |
|
163 in |
|
164 Logic.mk_implies (cse, HOLogic.mk_Trueprop thesis) |
|
165 end |
|
166 |
|
167 fun f (SchemeCase {bidx, qs, oqnames, gs, lhs, rs, ...}) = |
|
168 let |
|
169 fun g (bidx', Gvs, Gas, rcarg) = |
|
170 let val export = |
|
171 fold_rev (curry Logic.mk_implies) Gas |
|
172 #> fold_rev (curry Logic.mk_implies) gs |
|
173 #> fold_rev (Logic.all o Free) Gvs |
|
174 #> fold_rev mk_forall_rename (oqnames ~~ map Free qs) |
|
175 in |
|
176 (HOLogic.mk_mem (HOLogic.mk_prod (inject bidx' rcarg, inject bidx lhs), R) |
|
177 |> HOLogic.mk_Trueprop |
|
178 |> export, |
|
179 mk_pres bidx' rcarg |
|
180 |> export |
|
181 |> Logic.all thesis) |
|
182 end |
|
183 in |
|
184 map g rs |
|
185 end |
|
186 in |
|
187 map f cases |
|
188 end |
|
189 |
|
190 |
|
191 fun mk_ind_goal thy branches = |
|
192 let |
|
193 fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) = |
|
194 HOLogic.mk_Trueprop (list_comb (P, map Free xs)) |
|
195 |> fold_rev (curry Logic.mk_implies) Cs |
|
196 |> fold_rev (Logic.all o Free) ws |
|
197 |> term_conv thy ind_atomize |
|
198 |> Object_Logic.drop_judgment thy |
|
199 |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs)) |
|
200 in |
|
201 SumTree.mk_sumcases HOLogic.boolT (map brnch branches) |
|
202 end |
|
203 |
|
204 fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss |
|
205 (IndScheme {T, cases=scases, branches}) = |
|
206 let |
|
207 val n = length branches |
|
208 val scases_idx = map_index I scases |
|
209 |
|
210 fun inject i ts = |
|
211 SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts) |
|
212 val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches) |
|
213 |
|
214 val thy = ProofContext.theory_of ctxt |
|
215 val cert = cterm_of thy |
|
216 |
|
217 val P_comp = mk_ind_goal thy branches |
|
218 |
|
219 (* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
|
220 val ihyp = Term.all T $ Abs ("z", T, |
|
221 Logic.mk_implies |
|
222 (HOLogic.mk_Trueprop ( |
|
223 Const (@{const_name Set.member}, HOLogic.mk_prodT (T, T) --> mk_relT T --> HOLogic.boolT) |
|
224 $ (HOLogic.pair_const T T $ Bound 0 $ x) |
|
225 $ R), |
|
226 HOLogic.mk_Trueprop (P_comp $ Bound 0))) |
|
227 |> cert |
|
228 |
|
229 val aihyp = Thm.assume ihyp |
|
230 |
|
231 (* Rule for case splitting along the sum types *) |
|
232 val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches |
|
233 val pats = map_index (uncurry inject) xss |
|
234 val sum_split_rule = |
|
235 Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats) |
|
236 |
|
237 fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) = |
|
238 let |
|
239 val fxs = map Free xs |
|
240 val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat)))) |
|
241 |
|
242 val C_hyps = map (cert #> Thm.assume) Cs |
|
243 |
|
244 val (relevant_cases, ineqss') = |
|
245 (scases_idx ~~ ineqss) |
|
246 |> filter (fn ((_, SchemeCase {bidx=bidx', ...}), _) => bidx' = bidx) |
|
247 |> split_list |
|
248 |
|
249 fun prove_case (cidx, SchemeCase {qs, gs, lhs, rs, ...}) ineq_press = |
|
250 let |
|
251 val case_hyps = |
|
252 map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs) |
|
253 |
|
254 val cqs = map (cert o Free) qs |
|
255 val ags = map (Thm.assume o cert) gs |
|
256 |
|
257 val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps) |
|
258 val sih = full_simplify replace_x_ss aihyp |
|
259 |
|
260 fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) = |
|
261 let |
|
262 val cGas = map (Thm.assume o cert) Gas |
|
263 val cGvs = map (cert o Free) Gvs |
|
264 val import = fold Thm.forall_elim (cqs @ cGvs) |
|
265 #> fold Thm.elim_implies (ags @ cGas) |
|
266 val ipres = pres |
|
267 |> Thm.forall_elim (cert (list_comb (P_of idx, rcargs))) |
|
268 |> import |
|
269 in |
|
270 sih |
|
271 |> Thm.forall_elim (cert (inject idx rcargs)) |
|
272 |> Thm.elim_implies (import ineq) (* Psum rcargs *) |
|
273 |> Conv.fconv_rule sum_prod_conv |
|
274 |> Conv.fconv_rule ind_rulify |
|
275 |> (fn th => th COMP ipres) (* P rs *) |
|
276 |> fold_rev (Thm.implies_intr o cprop_of) cGas |
|
277 |> fold_rev Thm.forall_intr cGvs |
|
278 end |
|
279 |
|
280 val P_recs = map2 mk_Prec rs ineq_press (* [P rec1, P rec2, ... ] *) |
|
281 |
|
282 val step = HOLogic.mk_Trueprop (list_comb (P, lhs)) |
|
283 |> fold_rev (curry Logic.mk_implies o prop_of) P_recs |
|
284 |> fold_rev (curry Logic.mk_implies) gs |
|
285 |> fold_rev (Logic.all o Free) qs |
|
286 |> cert |
|
287 |
|
288 val Plhs_to_Pxs_conv = |
|
289 foldl1 (uncurry Conv.combination_conv) |
|
290 (Conv.all_conv :: map (fn ch => K (Thm.symmetric (ch RS eq_reflection))) case_hyps) |
|
291 |
|
292 val res = Thm.assume step |
|
293 |> fold Thm.forall_elim cqs |
|
294 |> fold Thm.elim_implies ags |
|
295 |> fold Thm.elim_implies P_recs (* P lhs *) |
|
296 |> Conv.fconv_rule (Conv.arg_conv Plhs_to_Pxs_conv) (* P xs *) |
|
297 |> fold_rev (Thm.implies_intr o cprop_of) (ags @ case_hyps) |
|
298 |> fold_rev Thm.forall_intr cqs (* !!qs. Gas ==> xs = lhss ==> P xs *) |
|
299 in |
|
300 (res, (cidx, step)) |
|
301 end |
|
302 |
|
303 val (cases, steps) = split_list (map2 prove_case relevant_cases ineqss') |
|
304 |
|
305 val bstep = complete_thm |
|
306 |> Thm.forall_elim (cert (list_comb (P, fxs))) |
|
307 |> fold (Thm.forall_elim o cert) (fxs @ map Free ws) |
|
308 |> fold Thm.elim_implies C_hyps |
|
309 |> fold Thm.elim_implies cases (* P xs *) |
|
310 |> fold_rev (Thm.implies_intr o cprop_of) C_hyps |
|
311 |> fold_rev (Thm.forall_intr o cert o Free) ws |
|
312 |
|
313 val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x)) |
|
314 |> Goal.init |
|
315 |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases})) |
|
316 THEN CONVERSION ind_rulify 1) |
|
317 |> Seq.hd |
|
318 |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep) |
|
319 |> Goal.finish ctxt |
|
320 |> Thm.implies_intr (cprop_of branch_hyp) |
|
321 |> fold_rev (Thm.forall_intr o cert) fxs |
|
322 in |
|
323 (Pxs, steps) |
|
324 end |
|
325 |
|
326 val (branches, steps) = |
|
327 map_index prove_branch (branches ~~ (complete_thms ~~ pats)) |
|
328 |> split_list |> apsnd flat |
|
329 |
|
330 val istep = sum_split_rule |
|
331 |> fold (fn b => fn th => Drule.compose_single (b, 1, th)) branches |
|
332 |> Thm.implies_intr ihyp |
|
333 |> Thm.forall_intr (cert x) (* "!!x. (!!y<x. P y) ==> P x" *) |
|
334 |
|
335 val induct_rule = |
|
336 @{thm "wf_induct_rule"} |
|
337 |> (curry op COMP) wf_thm |
|
338 |> (curry op COMP) istep |
|
339 |
|
340 val steps_sorted = map snd (sort (int_ord o pairself fst) steps) |
|
341 in |
|
342 (steps_sorted, induct_rule) |
|
343 end |
|
344 |
|
345 |
|
346 fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts = |
|
347 (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) => |
|
348 let |
|
349 val (ctxt', _, cases, concl) = dest_hhf ctxt t |
|
350 val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl |
|
351 val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' |
|
352 val R = Free (Rn, mk_relT ST) |
|
353 val x = Free (xn, ST) |
|
354 val cert = cterm_of (ProofContext.theory_of ctxt) |
|
355 |
|
356 val ineqss = mk_ineqs R scheme |
|
357 |> map (map (pairself (Thm.assume o cert))) |
|
358 val complete = |
|
359 map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches) |
|
360 val wf_thm = mk_wf R scheme |> cert |> Thm.assume |
|
361 |
|
362 val (descent, pres) = split_list (flat ineqss) |
|
363 val newgoals = complete @ pres @ wf_thm :: descent |
|
364 |
|
365 val (steps, indthm) = |
|
366 mk_induct_rule ctxt'' R x complete wf_thm ineqss scheme |
|
367 |
|
368 fun project (i, SchemeBranch {xs, ...}) = |
|
369 let |
|
370 val inst = (foldr1 HOLogic.mk_prod (map Free xs)) |
|
371 |> SumTree.mk_inj ST (length branches) (i + 1) |
|
372 |> cert |
|
373 in |
|
374 indthm |
|
375 |> Drule.instantiate' [] [SOME inst] |
|
376 |> simplify SumTree.sumcase_split_ss |
|
377 |> Conv.fconv_rule ind_rulify |
|
378 end |
|
379 |
|
380 val res = Conjunction.intr_balanced (map_index project branches) |
|
381 |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps) |
|
382 |> Drule.generalize ([], [Rn]) |
|
383 |
|
384 val nbranches = length branches |
|
385 val npres = length pres |
|
386 in |
|
387 Thm.compose_no_flatten false (res, length newgoals) i |
|
388 THEN term_tac (i + nbranches + npres) |
|
389 THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches)))) |
|
390 THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i))) |
|
391 end)) |
|
392 |
|
393 |
|
394 fun induction_schema_tac ctxt = |
|
395 mk_ind_tac (K all_tac) (assume_tac APPEND' Goal.assume_rule_tac ctxt) (K all_tac) ctxt; |
|
396 |
|
397 val setup = |
|
398 Method.setup @{binding induction_schema} (Scan.succeed (RAW_METHOD o induction_schema_tac)) |
|
399 "proves an induction principle" |
|
400 |
|
401 end |