equal
deleted
inserted
replaced
20 |
20 |
21 fun tuple_fun Ts (xi, T) = |
21 fun tuple_fun Ts (xi, T) = |
22 Library.funpow (length Ts) HOLogic.mk_split |
22 Library.funpow (length Ts) HOLogic.mk_split |
23 (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); |
23 (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); |
24 |
24 |
25 val split_all_tuples = |
25 fun split_all_tuples ctxt = |
26 Simplifier.full_simplify (HOL_basic_ss addsimps |
26 Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps |
27 @{thms split_conv split_paired_all unit_all_eq1} @ |
27 @{thms split_conv split_paired_all unit_all_eq1} @ |
28 @{thms fresh_Unit_elim fresh_Pair_elim} @ |
28 @{thms fresh_Unit_elim fresh_Pair_elim} @ |
29 @{thms fresh_star_Unit_elim fresh_star_Pair_elim fresh_star_Un_elim} @ |
29 @{thms fresh_star_Unit_elim fresh_star_Pair_elim fresh_star_Un_elim} @ |
30 @{thms fresh_star_insert_elim fresh_star_empty_elim}) |
30 @{thms fresh_star_insert_elim fresh_star_empty_elim}) |
31 |
31 |
91 |
91 |
92 val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; |
92 val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; |
93 val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs; |
93 val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs; |
94 |
94 |
95 val finish_rule = |
95 val finish_rule = |
96 split_all_tuples |
96 split_all_tuples defs_ctxt |
97 #> rename_params_rule true |
97 #> rename_params_rule true |
98 (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); |
98 (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); |
99 |
99 |
100 fun rule_cases ctxt r = |
100 fun rule_cases ctxt r = |
101 let val r' = if simp then Induct.simplified_rule ctxt r else r |
101 let val r' = if simp then Induct.simplified_rule ctxt r else r |