170 let |
172 let |
171 val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} |
173 val ss1 = HOL_basic_ss addsimps @{thms supports_def fresh_def[symmetric]} |
172 val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} |
174 val ss2 = HOL_ss addsimps @{thms swap_fresh_fresh fresh_Pair} |
173 in |
175 in |
174 EVERY' [ simp_tac ss1, |
176 EVERY' [ simp_tac ss1, |
175 Nominal_Permeq.eqvt_strict_tac ctxt perm_simps [], |
177 eqvt_tac ctxt (eqvt_strict_config addpres perm_simps), |
176 simp_tac ss2 ] |
178 simp_tac ss2 ] |
177 end |
179 end |
178 |
180 |
179 fun prove_supports_single ctxt perm_simps qtrm = |
181 fun prove_supports_single ctxt perm_simps qtrm = |
180 let |
182 let |
297 |> dest_comb |
299 |> dest_comb |
298 val supp_abs_tac = |
300 val supp_abs_tac = |
299 case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of |
301 case (AList.lookup (op=) (qtrms ~~ bclausess) (head_of arg)) of |
300 SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) |
302 SOME bclauses => EVERY' (mk_supp_abs_tac ctxt bclauses) |
301 | NONE => mk_bn_supp_abs_tac fv_fun |
303 | NONE => mk_bn_supp_abs_tac fv_fun |
|
304 val eqvt_rconfig = eqvt_relaxed_config addpres (perm_simps @ fv_bn_eqvts) |
302 in |
305 in |
303 EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
306 EVERY' [ TRY o asm_full_simp_tac (add_ss (@{thm supp_Pair[symmetric]}::fv_simps)), |
304 TRY o supp_abs_tac, |
307 TRY o supp_abs_tac, |
305 TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), |
308 TRY o simp_tac (add_ss @{thms supp_def supp_rel_def}), |
306 TRY o Nominal_Permeq.eqvt_tac ctxt (perm_simps @ fv_bn_eqvts) [], |
309 TRY o eqvt_tac ctxt eqvt_rconfig, |
307 TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), |
310 TRY o simp_tac (add_ss (@{thms Abs_eq_iff} @ eq_iffs)), |
308 TRY o asm_full_simp_tac (add_ss thms3), |
311 TRY o asm_full_simp_tac (add_ss thms3), |
309 TRY o simp_tac (add_ss thms2), |
312 TRY o simp_tac (add_ss thms2), |
310 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i |
313 TRY o asm_full_simp_tac (add_ss (thms1 @ (symmetric fv_bn_eqvts)))] i |
311 end) |
314 end) |
371 |
374 |
372 val props = map2 mk_goal qbns qperm_bns |
375 val props = map2 mk_goal qbns qperm_bns |
373 val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs |
376 val ss = @{thm id_def}::qperm_bn_simps @ qbn_defs |
374 val ss_tac = |
377 val ss_tac = |
375 EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss), |
378 EVERY' [asm_full_simp_tac (HOL_basic_ss addsimps ss), |
376 TRY o Nominal_Permeq.eqvt_strict_tac ctxt' qbn_eqvts [], |
379 TRY o eqvt_tac ctxt' (eqvt_strict_config addpres qbn_eqvts), |
377 TRY o asm_full_simp_tac HOL_basic_ss] |
380 TRY o asm_full_simp_tac HOL_basic_ss] |
378 in |
381 in |
379 induct_prove qtys props qinduct (K ss_tac) ctxt' |
382 induct_prove qtys props qinduct (K ss_tac) ctxt' |
380 |> ProofContext.export ctxt' ctxt |
383 |> ProofContext.export ctxt' ctxt |
381 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
384 |> map (simplify (HOL_basic_ss addsimps @{thms id_def})) |
517 |
520 |
518 val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] |
521 val tac2 = EVERY' [simp_tac (HOL_basic_ss addsimps ss), TRY o simp_tac HOL_ss] |
519 in |
522 in |
520 [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) |
523 [ Goal.prove ctxt [] [] goal (K (HEADGOAL (tac1 THEN_ALL_NEW tac2))) |
521 |> (if rec_flag |
524 |> (if rec_flag |
522 then Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt [] |
525 then eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt) |
523 else Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) ] |
526 else eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) ] |
524 end |
527 end |
525 |
528 |
526 |
529 |
527 val setify = @{lemma "xs = ys ==> set xs = set ys" by simp} |
530 val setify = @{lemma "xs = ys ==> set xs = set ys" by simp} |
528 |
531 |
554 full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' |
557 full_simp_tac (HOL_basic_ss addsimps @{thms set_append set.simps})])) abs_eq_thms ctxt' |
555 |
558 |
556 val (abs_eqs, peqs) = split_filter is_abs_eq eqs |
559 val (abs_eqs, peqs) = split_filter is_abs_eq eqs |
557 |
560 |
558 val fprops' = |
561 val fprops' = |
559 map (Nominal_Permeq.eqvt_strict_rule ctxt permute_bns []) fprops |
562 map (eqvt_rule ctxt (eqvt_strict_config addpres permute_bns)) fprops |
560 @ map (Nominal_Permeq.eqvt_strict_rule ctxt bn_eqvt []) fprops |
563 @ map (eqvt_rule ctxt (eqvt_strict_config addpres bn_eqvt)) fprops |
561 |
564 |
562 (* for freshness conditions *) |
565 (* for freshness conditions *) |
563 val tac1 = SOLVED' (EVERY' |
566 val tac1 = SOLVED' (EVERY' |
564 [ simp_tac (HOL_basic_ss addsimps peqs), |
567 [ simp_tac (HOL_basic_ss addsimps peqs), |
565 rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), |
568 rewrite_goal_tac (@{thms fresh_star_Un[THEN eq_reflection]}), |