10 val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term |
10 val comb_binders: Proof.context -> bmode -> term list -> (term option * int) list -> term |
11 |
11 |
12 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> |
12 val define_raw_alpha: string list -> typ list -> cns_info list -> bn_info list -> |
13 bclause list list list -> term list -> Proof.context -> |
13 bclause list list list -> term list -> Proof.context -> |
14 term list * term list * thm list * thm list * thm * local_theory |
14 term list * term list * thm list * thm list * thm * local_theory |
15 |
|
16 val raw_prove_alpha_distincts: Proof.context -> thm list -> thm list -> |
|
17 term list -> string list -> thm list |
|
18 |
|
19 val raw_prove_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
|
20 thm list -> thm list |
|
21 |
15 |
22 val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> |
16 val induct_prove: typ list -> (typ * (term -> term)) list -> thm -> |
23 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
17 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
24 |
18 |
25 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
19 val alpha_prove: term list -> (term * ((term * term) -> term)) list -> thm -> |
26 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
20 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
27 |
21 |
|
22 val raw_prove_alpha_distincts: Proof.context -> thm list -> thm list -> |
|
23 term list -> string list -> thm list |
|
24 |
|
25 val raw_prove_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> |
|
26 thm list -> thm list |
|
27 |
28 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
28 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
29 val raw_prove_sym: term list -> thm list -> thm -> thm list -> Proof.context -> thm list |
29 val raw_prove_sym: term list -> thm list -> thm -> thm list -> Proof.context -> thm list |
30 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> thm list -> |
30 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> thm list -> |
31 Proof.context -> thm list |
31 Proof.context -> thm list |
32 val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> |
32 val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> |
274 in |
275 in |
275 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
276 (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy') |
276 end |
277 end |
277 |
278 |
278 |
279 |
279 |
280 (** induction proofs **) |
280 (** produces the distinctness theorems **) |
281 |
281 |
282 |
282 (* transforms the distinctness theorems of the constructors |
283 (* proof by structural induction over data types *) |
283 into "not-alphas" of the constructors *) |
|
284 fun mk_distinct_goal ty_trm_assoc neq = |
|
285 let |
|
286 val (Const (@{const_name "HOL.eq"}, ty_eq) $ lhs $ rhs) = |
|
287 HOLogic.dest_not (HOLogic.dest_Trueprop neq) |
|
288 val ty_str = fst (dest_Type (domain_type ty_eq)) |
|
289 in |
|
290 Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs |
|
291 |> HOLogic.mk_not |
|
292 |> HOLogic.mk_Trueprop |
|
293 end |
|
294 |
|
295 fun distinct_tac cases_thms distinct_thms = |
|
296 rtac notI THEN' eresolve_tac cases_thms |
|
297 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
|
298 |
|
299 |
|
300 fun raw_prove_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str = |
|
301 let |
|
302 val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms) |
|
303 |
|
304 fun mk_alpha_distinct distinct_trm = |
|
305 let |
|
306 val goal = mk_distinct_goal ty_trm_assoc distinct_trm |
|
307 in |
|
308 Goal.prove ctxt [] [] goal |
|
309 (K (distinct_tac cases_thms distinct_thms 1)) |
|
310 end |
|
311 in |
|
312 map (mk_alpha_distinct o prop_of) distinct_thms |
|
313 end |
|
314 |
|
315 |
|
316 |
|
317 (** produces the alpha_eq_iff simplification rules **) |
|
318 |
|
319 (* in case a theorem is of the form (Rel Const Const), it will be |
|
320 rewritten to ((Rel Const = Const) = True) |
|
321 *) |
|
322 fun mk_simp_rule thm = |
|
323 case (prop_of thm) of |
|
324 @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} |
|
325 | _ => thm |
|
326 |
|
327 fun alpha_eq_iff_tac dist_inj intros elims = |
|
328 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE' |
|
329 (rtac @{thm iffI} THEN' |
|
330 RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj), |
|
331 asm_full_simp_tac (HOL_ss addsimps intros)]) |
|
332 |
|
333 fun mk_alpha_eq_iff_goal thm = |
|
334 let |
|
335 val prop = prop_of thm; |
|
336 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); |
|
337 val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); |
|
338 fun list_conj l = foldr1 HOLogic.mk_conj l; |
|
339 in |
|
340 if hyps = [] then HOLogic.mk_Trueprop concl |
|
341 else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) |
|
342 end; |
|
343 |
|
344 fun raw_prove_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims = |
|
345 let |
|
346 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
|
347 val goals = map mk_alpha_eq_iff_goal thms_imp; |
|
348 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
|
349 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
|
350 in |
|
351 Variable.export ctxt' ctxt thms |
|
352 |> map mk_simp_rule |
|
353 end |
|
354 |
|
355 |
|
356 (** proof by induction over types **) |
|
357 |
284 |
358 fun induct_prove tys props induct_thm cases_tac ctxt = |
285 fun induct_prove tys props induct_thm cases_tac ctxt = |
359 let |
286 let |
360 val (arg_names, ctxt') = |
287 val (arg_names, ctxt') = |
361 Variable.variant_fixes (replicate (length tys) "x") ctxt |
288 Variable.variant_fixes (replicate (length tys) "x") ctxt |
433 |> map (fn th => th RS mp) |
359 |> map (fn th => th RS mp) |
434 |> map Datatype_Aux.split_conj_thm |
360 |> map Datatype_Aux.split_conj_thm |
435 |> flat |
361 |> flat |
436 |> filter_out (is_true o concl_of) |
362 |> filter_out (is_true o concl_of) |
437 |> map zero_var_indexes |
363 |> map zero_var_indexes |
|
364 end |
|
365 |
|
366 |
|
367 |
|
368 (** produces the distinctness theorems **) |
|
369 |
|
370 |
|
371 (* transforms the distinctness theorems of the constructors |
|
372 into "not-alphas" of the constructors *) |
|
373 fun mk_distinct_goal ty_trm_assoc neq = |
|
374 let |
|
375 val (Const (@{const_name "HOL.eq"}, ty_eq) $ lhs $ rhs) = |
|
376 HOLogic.dest_not (HOLogic.dest_Trueprop neq) |
|
377 val ty_str = fst (dest_Type (domain_type ty_eq)) |
|
378 in |
|
379 Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs |
|
380 |> HOLogic.mk_not |
|
381 |> HOLogic.mk_Trueprop |
|
382 end |
|
383 |
|
384 fun distinct_tac cases_thms distinct_thms = |
|
385 rtac notI THEN' eresolve_tac cases_thms |
|
386 THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms) |
|
387 |
|
388 fun raw_prove_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str = |
|
389 let |
|
390 val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms) |
|
391 |
|
392 fun mk_alpha_distinct distinct_trm = |
|
393 let |
|
394 val goal = mk_distinct_goal ty_trm_assoc distinct_trm |
|
395 in |
|
396 Goal.prove ctxt [] [] goal |
|
397 (K (distinct_tac cases_thms distinct_thms 1)) |
|
398 end |
|
399 in |
|
400 map (mk_alpha_distinct o prop_of) distinct_thms |
|
401 end |
|
402 |
|
403 |
|
404 |
|
405 (** produces the alpha_eq_iff simplification rules **) |
|
406 |
|
407 (* in case a theorem is of the form (Rel Const Const), it will be |
|
408 rewritten to ((Rel Const = Const) = True) |
|
409 *) |
|
410 fun mk_simp_rule thm = |
|
411 case (prop_of thm) of |
|
412 @{term "Trueprop"} $ (_ $ Const _ $ Const _) => thm RS @{thm eqTrueI} |
|
413 | _ => thm |
|
414 |
|
415 fun alpha_eq_iff_tac dist_inj intros elims = |
|
416 SOLVED' (asm_full_simp_tac (HOL_ss addsimps intros)) ORELSE' |
|
417 (rtac @{thm iffI} THEN' |
|
418 RANGE [eresolve_tac elims THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps dist_inj), |
|
419 asm_full_simp_tac (HOL_ss addsimps intros)]) |
|
420 |
|
421 fun mk_alpha_eq_iff_goal thm = |
|
422 let |
|
423 val prop = prop_of thm; |
|
424 val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop); |
|
425 val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop); |
|
426 fun list_conj l = foldr1 HOLogic.mk_conj l; |
|
427 in |
|
428 if hyps = [] then HOLogic.mk_Trueprop concl |
|
429 else HOLogic.mk_Trueprop (HOLogic.mk_eq (concl, list_conj hyps)) |
|
430 end; |
|
431 |
|
432 fun raw_prove_alpha_eq_iff ctxt alpha_intros distinct_thms inject_thms alpha_elims = |
|
433 let |
|
434 val ((_, thms_imp), ctxt') = Variable.import false alpha_intros ctxt; |
|
435 val goals = map mk_alpha_eq_iff_goal thms_imp; |
|
436 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
|
437 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
|
438 in |
|
439 Variable.export ctxt' ctxt thms |
|
440 |> map mk_simp_rule |
438 end |
441 end |
439 |
442 |
440 |
443 |
441 (** reflexivity proof for the alphas **) |
444 (** reflexivity proof for the alphas **) |
442 |
445 |