1097 simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
1097 simp_tac (HOL_basic_ss addsimps @{thms de_Morgan_conj[symmetric]}) THEN_ALL_NEW |
1098 simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW |
1098 simp_tac (HOL_basic_ss addsimps @{thms ex_simps(1,2)[symmetric]}) THEN_ALL_NEW |
1099 simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
1099 simp_tac (HOL_ss addsimps @{thms Collect_const finite.emptyI}) |
1100 *} |
1100 *} |
1101 |
1101 |
1102 end |
1102 (* Given function for buildng a goal for an input, prepares a |
|
1103 one common goals for all the inputs and proves it by induction |
|
1104 together *) |
|
1105 ML {* |
|
1106 fun prove_by_induct tys build_goal ind utac inputs ctxt = |
|
1107 let |
|
1108 val names = Datatype_Prop.make_tnames tys; |
|
1109 val (names', ctxt') = Variable.variant_fixes names ctxt; |
|
1110 val frees = map Free (names' ~~ tys); |
|
1111 val (gls_lists, ctxt'') = fold_map (build_goal (tys ~~ frees)) inputs ctxt'; |
|
1112 val gls = flat gls_lists; |
|
1113 fun trm_gls_map t = filter (exists_subterm (fn s => s = t)) gls; |
|
1114 val trm_gl_lists = map trm_gls_map frees; |
|
1115 val trm_gl_insts = map2 (fn n => fn l => [NONE, if l = [] then NONE else SOME n]) names' trm_gl_lists |
|
1116 val trm_gls = map mk_conjl trm_gl_lists; |
|
1117 val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj trm_gls); |
|
1118 fun tac {context,...} = ((fn _ => print_tac (PolyML.makestring names')) THEN' |
|
1119 InductTacs.induct_rules_tac context [(flat trm_gl_insts)] [ind] |
|
1120 THEN_ALL_NEW split_conjs THEN_ALL_NEW utac) 1 |
|
1121 val th_loc = Goal.prove ctxt'' [] [] gl tac |
|
1122 val ths_loc = HOLogic.conj_elims th_loc |
|
1123 val ths = Variable.export ctxt'' ctxt ths_loc |
|
1124 in |
|
1125 filter (fn x => not (prop_of x = prop_of @{thm TrueI})) ths |
|
1126 end |
|
1127 *} |
|
1128 |
|
1129 ML {* |
|
1130 fun build_eqvt_gl pi frees fnctn ctxt = |
|
1131 let |
|
1132 val typ = domain_type (fastype_of fnctn); |
|
1133 val arg = the (AList.lookup (op=) frees typ); |
|
1134 in |
|
1135 ([HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt) |
|
1136 end |
|
1137 *} |
|
1138 |
|
1139 ML {* |
|
1140 fun prove_eqvt tys ind simps funs ctxt = |
|
1141 let |
|
1142 val ([pi], ctxt') = Variable.variant_fixes ["p"] ctxt; |
|
1143 val pi = Free (pi, @{typ perm}); |
|
1144 val tac = asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: simps @ all_eqvts ctxt')) |
|
1145 val ths_loc = prove_by_induct tys (build_eqvt_gl pi) ind tac funs ctxt' |
|
1146 val ths = Variable.export ctxt' ctxt ths_loc |
|
1147 val add_eqvt = Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add) |
|
1148 in |
|
1149 (ths, snd (Local_Theory.note ((Binding.empty, [add_eqvt]), ths) ctxt)) |
|
1150 end |
|
1151 *} |
|
1152 |
|
1153 end |