equal
deleted
inserted
replaced
1 (* ID: $Id$ |
1 (* Author: Christian Urban and Makarius |
2 Author: Christian Urban and Makarius |
|
3 |
2 |
4 The nominal induct proof method. |
3 The nominal induct proof method. |
5 *) |
4 *) |
6 |
5 |
7 structure NominalInduct: |
6 structure NominalInduct: |
22 Library.funpow (length Ts) HOLogic.mk_split |
21 Library.funpow (length Ts) HOLogic.mk_split |
23 (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); |
22 (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); |
24 |
23 |
25 val split_all_tuples = |
24 val split_all_tuples = |
26 Simplifier.full_simplify (HOL_basic_ss addsimps |
25 Simplifier.full_simplify (HOL_basic_ss addsimps |
27 [split_conv, split_paired_all, unit_all_eq1, thm "fresh_unit_elim", thm "fresh_prod_elim"]); |
26 [split_conv, split_paired_all, unit_all_eq1, @{thm fresh_unit_elim}, @{thm fresh_prod_elim}] @ |
|
27 @{thms fresh_star_unit_elim} @ @{thms fresh_star_prod_elim}); |
28 |
28 |
29 |
29 |
30 (* prepare rule *) |
30 (* prepare rule *) |
31 |
31 |
32 fun inst_mutual_rule ctxt insts avoiding rules = |
32 fun inst_mutual_rule ctxt insts avoiding rules = |