1820 |
1820 |
1821 text {* for handling of freshness of functions *} |
1821 text {* for handling of freshness of functions *} |
1822 |
1822 |
1823 simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ss => fn ctrm => |
1823 simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ss => fn ctrm => |
1824 let |
1824 let |
1825 val Const(@{const_name fresh}, _) $ _ $ f = term_of ctrm |
1825 val _ $ _ $ f = term_of ctrm |
1826 in |
1826 in |
1827 case (Term.add_frees f [], Term.add_vars f []) of |
1827 case (Term.add_frees f [], Term.add_vars f []) of |
1828 ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]}) |
1828 ([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]}) |
1829 | (x::_, []) => let |
1829 | (x::_, []) => let |
1830 val thy = Proof_Context.theory_of (Simplifier.the_context ss) |
1830 val thy = Proof_Context.theory_of (Simplifier.the_context ss) |
3138 setup {* Sign.add_const_constraint |
3138 setup {* Sign.add_const_constraint |
3139 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
3139 (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *} |
3140 setup {* Sign.add_const_constraint |
3140 setup {* Sign.add_const_constraint |
3141 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |
3141 (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *} |
3142 |
3142 |
|
3143 |
|
3144 |
|
3145 section {* Library functions for the nominal infrastructure *} |
|
3146 |
|
3147 use "nominal_library.ML" |
|
3148 |
|
3149 |
|
3150 |
3143 section {* The freshness lemma according to Andy Pitts *} |
3151 section {* The freshness lemma according to Andy Pitts *} |
3144 |
3152 |
3145 lemma freshness_lemma: |
3153 lemma freshness_lemma: |
3146 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
3154 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
3147 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
3155 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
3224 shows "Fresh h = h a" |
3232 shows "Fresh h = h a" |
3225 apply (rule Fresh_apply) |
3233 apply (rule Fresh_apply) |
3226 apply (auto simp add: fresh_Pair intro: a) |
3234 apply (auto simp add: fresh_Pair intro: a) |
3227 done |
3235 done |
3228 |
3236 |
|
3237 lemma "1 = 1 &&& 2 = 2" |
|
3238 apply(tactic {* ALLGOALS (asm_full_simp_tac @{simpset}) *}) |
|
3239 done |
|
3240 |
|
3241 |
|
3242 simproc_setup Fresh_simproc ("Fresh (h::'a::at \<Rightarrow> 'b::pt)") = {* fn _ => fn ss => fn ctrm => |
|
3243 let |
|
3244 val ctxt = Simplifier.the_context ss |
|
3245 val _ $ h = term_of ctrm |
|
3246 |
|
3247 val cfresh = @{const_name fresh} |
|
3248 val catom = @{const_name atom} |
|
3249 |
|
3250 val atoms = Simplifier.prems_of ss |
|
3251 |> map_filter (fn thm => case Thm.prop_of thm of |
|
3252 _ $ (Const (cfresh, _) $ (Const (catom, _) $ atm) $ _) => SOME (atm) | _ => NONE) |
|
3253 |> distinct (op=) |
|
3254 |
|
3255 fun get_thm atm = |
|
3256 let |
|
3257 val goal1 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) h) |
|
3258 val goal2 = HOLogic.mk_Trueprop (mk_fresh (mk_atom atm) (h $ atm)) |
|
3259 |
|
3260 val thm1 = Goal.prove ctxt [] [] goal1 (K (asm_simp_tac ss 1)) |
|
3261 val thm2 = Goal.prove ctxt [] [] goal2 (K (asm_simp_tac ss 1)) |
|
3262 in |
|
3263 SOME (@{thm Fresh_apply'} OF [thm1, thm2] RS eq_reflection) |
|
3264 end handle ERROR _ => NONE |
|
3265 in |
|
3266 get_first get_thm atoms |
|
3267 end |
|
3268 *} |
|
3269 |
|
3270 |
3229 lemma Fresh_eqvt: |
3271 lemma Fresh_eqvt: |
3230 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
3272 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
3231 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
3273 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
3232 shows "p \<bullet> (Fresh h) = Fresh (p \<bullet> h)" |
3274 shows "p \<bullet> (Fresh h) = Fresh (p \<bullet> h)" |
3233 using a |
3275 proof - |
3234 apply (clarsimp simp add: fresh_Pair) |
3276 from a obtain a::"'a::at" where fr: "atom a \<sharp> h" "atom a \<sharp> h a" |
3235 apply (subst Fresh_apply', assumption+) |
3277 by (metis fresh_Pair) |
3236 apply (drule fresh_permute_iff [where p=p, THEN iffD2]) |
3278 then have fr_p: "atom (p \<bullet> a) \<sharp> (p \<bullet> h)" "atom (p \<bullet> a) \<sharp> (p \<bullet> h) (p \<bullet> a)" |
3237 apply (drule fresh_permute_iff [where p=p, THEN iffD2]) |
3279 by (metis atom_eqvt fresh_permute_iff eqvt_apply)+ |
3238 apply (simp only: atom_eqvt permute_fun_app_eq [where f=h]) |
3280 have "p \<bullet> (Fresh h) = p \<bullet> (h a)" using fr by simp |
3239 apply (erule (1) Fresh_apply' [symmetric]) |
3281 also have "... = (p \<bullet> h) (p \<bullet> a)" by simp |
3240 done |
3282 also have "... = Fresh (p \<bullet> h)" using fr_p by simp |
|
3283 finally show "p \<bullet> (Fresh h) = Fresh (p \<bullet> h)" . |
|
3284 qed |
3241 |
3285 |
3242 lemma Fresh_supports: |
3286 lemma Fresh_supports: |
3243 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
3287 fixes h :: "'a::at \<Rightarrow> 'b::pt" |
3244 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
3288 assumes a: "\<exists>a. atom a \<sharp> (h, h a)" |
3245 shows "(supp h) supports (Fresh h)" |
3289 shows "(supp h) supports (Fresh h)" |
3254 fixes f :: "'b \<Rightarrow> 'c::pure" |
3298 fixes f :: "'b \<Rightarrow> 'c::pure" |
3255 assumes P: "finite (supp P)" |
3299 assumes P: "finite (supp P)" |
3256 shows "(FRESH x. f (P x)) = f (FRESH x. P x)" |
3300 shows "(FRESH x. f (P x)) = f (FRESH x. P x)" |
3257 proof - |
3301 proof - |
3258 obtain a::'a where "atom a \<sharp> P" using P by (rule obtain_fresh') |
3302 obtain a::'a where "atom a \<sharp> P" using P by (rule obtain_fresh') |
3259 show "(FRESH x. f (P x)) = f (FRESH x. P x)" |
3303 then show "(FRESH x. f (P x)) = f (FRESH x. P x)" |
3260 apply (subst Fresh_apply' [where a=a, OF _ pure_fresh]) |
3304 by (simp add: pure_fresh) |
3261 apply (cut_tac `atom a \<sharp> P`) |
|
3262 apply (simp add: fresh_conv_MOST) |
|
3263 apply (elim MOST_rev_mp, rule MOST_I, clarify) |
|
3264 apply (simp add: permute_fun_def permute_pure fun_eq_iff) |
|
3265 apply (subst Fresh_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh]) |
|
3266 apply (rule refl) |
|
3267 done |
|
3268 qed |
3305 qed |
3269 |
3306 |
3270 lemma FRESH_binop_iff: |
3307 lemma FRESH_binop_iff: |
3271 fixes P :: "'a::at \<Rightarrow> 'b::pure" |
3308 fixes P :: "'a::at \<Rightarrow> 'b::pure" |
3272 fixes Q :: "'a::at \<Rightarrow> 'c::pure" |
3309 fixes Q :: "'a::at \<Rightarrow> 'c::pure" |
3275 and Q: "finite (supp Q)" |
3312 and Q: "finite (supp Q)" |
3276 shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)" |
3313 shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)" |
3277 proof - |
3314 proof - |
3278 from assms have "finite (supp (P, Q))" by (simp add: supp_Pair) |
3315 from assms have "finite (supp (P, Q))" by (simp add: supp_Pair) |
3279 then obtain a::'a where "atom a \<sharp> (P, Q)" by (rule obtain_fresh') |
3316 then obtain a::'a where "atom a \<sharp> (P, Q)" by (rule obtain_fresh') |
3280 then have "atom a \<sharp> P" and "atom a \<sharp> Q" by (simp_all add: fresh_Pair) |
3317 then show ?thesis |
3281 show ?thesis |
3318 by (simp add: pure_fresh) |
3282 apply (subst Fresh_apply' [where a=a, OF _ pure_fresh]) |
|
3283 apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`) |
|
3284 apply (simp add: fresh_conv_MOST) |
|
3285 apply (elim MOST_rev_mp, rule MOST_I, clarify) |
|
3286 apply (simp add: permute_fun_def permute_pure fun_eq_iff) |
|
3287 apply (subst Fresh_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh]) |
|
3288 apply (subst Fresh_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh]) |
|
3289 apply (rule refl) |
|
3290 done |
|
3291 qed |
3319 qed |
3292 |
3320 |
3293 lemma FRESH_conj_iff: |
3321 lemma FRESH_conj_iff: |
3294 fixes P Q :: "'a::at \<Rightarrow> bool" |
3322 fixes P Q :: "'a::at \<Rightarrow> bool" |
3295 assumes P: "finite (supp P)" and Q: "finite (supp Q)" |
3323 assumes P: "finite (supp P)" and Q: "finite (supp Q)" |
3300 fixes P Q :: "'a::at \<Rightarrow> bool" |
3328 fixes P Q :: "'a::at \<Rightarrow> bool" |
3301 assumes P: "finite (supp P)" and Q: "finite (supp Q)" |
3329 assumes P: "finite (supp P)" and Q: "finite (supp Q)" |
3302 shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)" |
3330 shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)" |
3303 using P Q by (rule FRESH_binop_iff) |
3331 using P Q by (rule FRESH_binop_iff) |
3304 |
3332 |
3305 |
|
3306 section {* Library functions for the nominal infrastructure *} |
|
3307 |
|
3308 use "nominal_library.ML" |
|
3309 |
|
3310 |
|
3311 section {* Automation for creating concrete atom types *} |
3333 section {* Automation for creating concrete atom types *} |
3312 |
3334 |
3313 text {* at the moment only single-sort concrete atoms are supported *} |
3335 text {* at the moment only single-sort concrete atoms are supported *} |
3314 |
3336 |
3315 use "nominal_atoms.ML" |
3337 use "nominal_atoms.ML" |