216 case cprems_of psimp of |
216 case cprems_of psimp of |
217 [] => ([], psimp, I) |
217 [] => ([], psimp, I) |
218 | [cond] => ([Thm.assume cond], Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) |
218 | [cond] => ([Thm.assume cond], Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond) |
219 | _ => raise General.Fail "Too many conditions" |
219 | _ => raise General.Fail "Too many conditions" |
220 |
220 |
221 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
221 val ([p], ctxt') = ctxt |
|
222 |> fold Variable.declare_term args |
|
223 |> Variable.variant_fixes ["p"] |
222 val p = Free (p, @{typ perm}) |
224 val p = Free (p, @{typ perm}) |
|
225 |
223 val ss = HOL_basic_ss addsimps |
226 val ss = HOL_basic_ss addsimps |
224 @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @ |
227 @{thms permute_sum.simps[symmetric] Pair_eqvt[symmetric]} @ |
225 @{thms Projr.simps Projl.simps} @ |
228 @{thms Projr.simps Projl.simps} @ |
226 [(cond MRS eqvt_thm) RS @{thm sym}] @ |
229 [(cond MRS eqvt_thm) RS @{thm sym}] @ |
227 [inl_perm, inr_perm, simp] |
230 [inl_perm, inr_perm, simp] |
348 end |
351 end |
349 |
352 |
350 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
353 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = |
351 let |
354 let |
352 val result = inner_cont proof |
355 val result = inner_cont proof |
|
356 |
353 val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], |
357 val NominalFunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], |
354 termination, domintros, eqvts=[eqvt],...} = result |
358 termination, domintros, eqvts=[eqvt],...} = result |
355 |
359 |
356 val (all_f_defs, fs) = |
360 val (all_f_defs, fs) = |
357 map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |
361 map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} => |