2184 val mksimps_pairs = (@{const_name Nominal2_Base.fresh}, @{thms fresh_PairD}) :: mksimps_pairs |
2184 val mksimps_pairs = (@{const_name Nominal2_Base.fresh}, @{thms fresh_PairD}) :: mksimps_pairs |
2185 in |
2185 in |
2186 Simplifier.map_ss (fn ss => Simplifier.set_mksimps (mksimps mksimps_pairs) ss) |
2186 Simplifier.map_ss (fn ss => Simplifier.set_mksimps (mksimps mksimps_pairs) ss) |
2187 end |
2187 end |
2188 *} |
2188 *} |
|
2189 |
2189 |
2190 |
2190 text {* The fresh-star generalisation of fresh is used in strong |
2191 text {* The fresh-star generalisation of fresh is used in strong |
2191 induction principles. *} |
2192 induction principles. *} |
2192 |
2193 |
2193 definition |
2194 definition |
2808 lemma fresh_star_atom_at_base: |
2809 lemma fresh_star_atom_at_base: |
2809 fixes b::"'a::at_base" |
2810 fixes b::"'a::at_base" |
2810 shows "as \<sharp>* atom b \<longleftrightarrow> as \<sharp>* b" |
2811 shows "as \<sharp>* atom b \<longleftrightarrow> as \<sharp>* b" |
2811 by (simp add: fresh_star_def fresh_atom_at_base) |
2812 by (simp add: fresh_star_def fresh_atom_at_base) |
2812 |
2813 |
|
2814 lemma if_fresh_at_base [simp]: |
|
2815 shows "atom a \<sharp> x \<Longrightarrow> P (if a = x then t else s) = P s" |
|
2816 and "atom a \<sharp> x \<Longrightarrow> P (if x = a then t else s) = P s" |
|
2817 by (simp_all add: fresh_at_base) |
|
2818 |
|
2819 simproc_setup fresh_ineq ("x \<noteq> (y::'a::at_base)") = {* fn _ => fn ss => fn ctrm => |
|
2820 let |
|
2821 fun first_is_neg lhs rhs [] = NONE |
|
2822 | first_is_neg lhs rhs (thm::thms) = |
|
2823 (case Thm.prop_of thm of |
|
2824 _ $ (@{term "HOL.Not"} $ (Const ("HOL.eq", _) $ l $ r)) => |
|
2825 (if l = lhs andalso r = rhs then SOME(thm) |
|
2826 else if r = lhs andalso l = rhs then SOME(thm RS @{thm not_sym}) |
|
2827 else NONE) |
|
2828 | _ => first_is_neg lhs rhs thms) |
|
2829 |
|
2830 val simp_thms = @{thms fresh_Pair fresh_at_base atom_eq_iff} |
|
2831 val prems = Simplifier.prems_of ss |
|
2832 |> filter (fn thm => case Thm.prop_of thm of |
|
2833 _ $ (Const (@{const_name fresh}, _) $ _ $ _) => true | _ => false) |
|
2834 |> map (simplify (HOL_basic_ss addsimps simp_thms)) |
|
2835 |> map HOLogic.conj_elims |
|
2836 |> flat |
|
2837 in |
|
2838 case term_of ctrm of |
|
2839 @{term "HOL.Not"} $ (Const ("HOL.eq", _) $ lhs $ rhs) => |
|
2840 (case first_is_neg lhs rhs prems of |
|
2841 SOME(thm) => SOME(thm RS @{thm Eq_TrueI}) |
|
2842 | NONE => NONE) |
|
2843 | _ => NONE |
|
2844 end |
|
2845 *} |
|
2846 |
|
2847 |
2813 instance at_base < fs |
2848 instance at_base < fs |
2814 proof qed (simp add: supp_at_base) |
2849 proof qed (simp add: supp_at_base) |
2815 |
2850 |
2816 lemma at_base_infinite [simp]: |
2851 lemma at_base_infinite [simp]: |
2817 shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") |
2852 shows "infinite (UNIV :: 'a::at_base set)" (is "infinite ?U") |
3121 by (rule freshness_lemma) |
3156 by (rule freshness_lemma) |
3122 next |
3157 next |
3123 fix x y |
3158 fix x y |
3124 assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
3159 assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" |
3125 assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y" |
3160 assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y" |
3126 from a x y show "x = y" |
3161 from a x y show "x = y" |
3127 by (auto simp add: fresh_Pair) |
3162 by (auto simp add: fresh_Pair) |
3128 qed |
3163 qed |
3129 |
3164 |
3130 text {* packaging the freshness lemma into a function *} |
3165 text {* packaging the freshness lemma into a function *} |
3131 |
3166 |