equal
deleted
inserted
replaced
2021 lemma fresh_PairD: |
2021 lemma fresh_PairD: |
2022 shows "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> x" |
2022 shows "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> x" |
2023 and "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> y" |
2023 and "a \<sharp> (x, y) \<Longrightarrow> a \<sharp> y" |
2024 by (simp_all add: fresh_Pair) |
2024 by (simp_all add: fresh_Pair) |
2025 |
2025 |
2026 ML {* |
|
2027 val mksimps_pairs = (@{const_name Nominal2_Base.fresh}, @{thms fresh_PairD}) :: mksimps_pairs; |
|
2028 *} |
|
2029 |
|
2030 declaration {* fn _ => |
2026 declaration {* fn _ => |
2031 Simplifier.map_ss (fn ss => ss setmksimps (mksimps mksimps_pairs)) |
2027 let |
|
2028 val mksimps_pairs = (@{const_name Nominal2_Base.fresh}, @{thms fresh_PairD}) :: mksimps_pairs |
|
2029 in |
|
2030 Simplifier.map_ss (fn ss => Simplifier.set_mksimps (mksimps mksimps_pairs) ss) |
|
2031 end |
2032 *} |
2032 *} |
2033 |
2033 |
2034 text {* The fresh-star generalisation of fresh is used in strong |
2034 text {* The fresh-star generalisation of fresh is used in strong |
2035 induction principles. *} |
2035 induction principles. *} |
2036 |
2036 |