equal
deleted
inserted
replaced
33 |
33 |
34 val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list |
34 val prove_bns_finite: typ list -> term list -> thm -> thm list -> Proof.context -> thm list |
35 |
35 |
36 val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> |
36 val prove_perm_bn_alpha_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> |
37 thm list -> Proof.context -> thm list |
37 thm list -> Proof.context -> thm list |
38 |
38 |
|
39 val prove_permute_bn_thms: typ list -> term list -> term list -> thm -> thm list -> thm list -> |
|
40 thm list -> Proof.context -> thm list |
39 end |
41 end |
40 |
42 |
41 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
43 structure Nominal_Dt_Quot: NOMINAL_DT_QUOT = |
42 struct |
44 struct |
43 |
45 |
321 @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) |
323 @{thms set.simps set_append finite_insert finite.emptyI finite_Un})) |
322 in |
324 in |
323 induct_prove qtys props qinduct (K ss_tac) ctxt |
325 induct_prove qtys props qinduct (K ss_tac) ctxt |
324 end |
326 end |
325 |
327 |
|
328 |
326 fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt = |
329 fun prove_perm_bn_alpha_thms qtys qperm_bns alpha_bns qinduct qperm_bn_simps qeq_iffs qalpha_refls ctxt = |
327 let |
330 let |
328 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
331 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
329 val p = Free (p, @{typ perm}) |
332 val p = Free (p, @{typ perm}) |
330 |
333 |
342 induct_prove qtys props qinduct (K ss_tac) ctxt' |
345 induct_prove qtys props qinduct (K ss_tac) ctxt' |
343 |> ProofContext.export ctxt' ctxt |
346 |> ProofContext.export ctxt' ctxt |
344 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
347 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
345 end |
348 end |
346 |
349 |
347 |
350 fun prove_permute_bn_thms qtys qbns qperm_bns qinduct qperm_bn_simps qbn_defs qbn_eqvts ctxt = |
|
351 let |
|
352 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
|
353 val p = Free (p, @{typ perm}) |
|
354 |
|
355 fun mk_goal qbn qperm_bn = |
|
356 let |
|
357 val arg_ty = domain_type (fastype_of qbn) |
|
358 in |
|
359 (arg_ty, fn x => |
|
360 (mk_id (Abs ("", arg_ty, |
|
361 HOLogic.mk_eq (mk_perm p (qbn $ Bound 0), qbn $ (qperm_bn $ p $ Bound 0)))) $ x)) |
|
362 end |
|
363 |
|
364 val props = map2 mk_goal qbns qperm_bns |
|
365 val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs |
|
366 val ss_tac = |
|
367 EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss), |
|
368 TRY o Nominal_Permeq.eqvt_strict_tac ctxt' qbn_eqvts [], |
|
369 TRY o asm_full_simp_tac HOL_basic_ss] |
|
370 in |
|
371 induct_prove qtys props qinduct (K ss_tac) ctxt' |
|
372 |> ProofContext.export ctxt' ctxt |
|
373 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
|
374 end |
348 |
375 |
349 end (* structure *) |
376 end (* structure *) |
350 |
377 |