nominal2: comparison Nominal/Nominal2

equal deleted inserted replaced

-:c25e4c9481f2
+:a331468b2f5a
 lemma finite_eqvt [eqvt]:
 shows "p \<bullet> finite A = finite (p \<bullet> A)"
 unfolding finite_def
 by (perm_simp) (rule refl)
-lemma Let_eqvt [eqvt]:
-"p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
-unfolding Let_def permute_fun_app_eq ..
 subsubsection {* Equivariance for product operations *}
 lemma fst_eqvt [eqvt]:
 shows "p \<bullet> (fst x) = fst (p \<bullet> x)"
 using a
 unfolding eqvt_def
 unfolding supp_def
 by simp
+lemma fresh_fun_eqvt:
+assumes a: "eqvt f"
+shows "a \<sharp> f"
+using a
+unfolding fresh_def
+by (simp add: supp_fun_eqvt)
 lemma fresh_fun_eqvt_app:
 assumes a: "eqvt f"
 shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x"
 proof -
 from a have "supp f = {}" by (simp add: supp_fun_eqvt)
 using fresh
 unfolding fresh_def
 using supp_eqvt_at[OF asm fin]
 by auto
+text {* for handling of freshness of functions *}
+simproc_setup fresh_fun_simproc ("a \<sharp> (f::'a::pt \<Rightarrow>'b::pt)") = {* fn _ => fn ss => fn ctrm =>
+let
+val Const(@{const_name fresh}, _) $ _ $ f = term_of ctrm
+in
+case (Term.add_frees f [], Term.add_vars f []) of
+([], []) => SOME(@{thm fresh_fun_eqvt[simplified eqvt_def, THEN Eq_TrueI]})
+| (x::_, []) => let
+val thy = Proof_Context.theory_of (Simplifier.the_context ss)
+val argx = Free x
+val absf = absfree x f
+val cty_inst = [SOME (ctyp_of thy (fastype_of argx)), SOME (ctyp_of thy (fastype_of f))]
+val ctrm_inst = [NONE, SOME (cterm_of thy absf), SOME (cterm_of thy argx)]
+val thm = Drule.instantiate' cty_inst ctrm_inst @{thm fresh_fun_app}
+in
+SOME(thm RS @{thm Eq_TrueI})
+end
+| (_, _) => NONE
+end
+*}
 subsection {* helper functions for nominal_functions *}
 lemma THE_defaultI2:
 assumes "\<exists>!x. P x" "\<And>x. P x \<Longrightarrow> Q x"
 qed
 text {* packaging the freshness lemma into a function *}
 definition
-fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"
+Fresh :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"
 where
-"fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"
+"Fresh h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"
-lemma fresh_fun_apply:
+lemma Fresh_apply:
 fixes h :: "'a::at \<Rightarrow> 'b::pt"
 assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
 assumes b: "atom a \<sharp> h"
-shows "fresh_fun h = h a"
+shows "Fresh h = h a"
-unfolding fresh_fun_def
+unfolding Fresh_def
 proof (rule the_equality)
 show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"
 proof (intro strip)
 fix a':: 'a
 assume c: "atom a' \<sharp> h"
 fix fr :: 'b
 assume "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = fr"
 with b show "fr = h a" by auto
 qed
-lemma fresh_fun_apply':
+lemma Fresh_apply':
 fixes h :: "'a::at \<Rightarrow> 'b::pt"
 assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"
-shows "fresh_fun h = h a"
+shows "Fresh h = h a"
-apply (rule fresh_fun_apply)
+apply (rule Fresh_apply)
 apply (auto simp add: fresh_Pair intro: a)
 done
-lemma fresh_fun_eqvt:
+lemma Fresh_eqvt:
 fixes h :: "'a::at \<Rightarrow> 'b::pt"
 assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
-shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"
+shows "p \<bullet> (Fresh h) = Fresh (p \<bullet> h)"
 using a
 apply (clarsimp simp add: fresh_Pair)
-apply (subst fresh_fun_apply', assumption+)
+apply (subst Fresh_apply', assumption+)
 apply (drule fresh_permute_iff [where p=p, THEN iffD2])
 apply (drule fresh_permute_iff [where p=p, THEN iffD2])
 apply (simp only: atom_eqvt permute_fun_app_eq [where f=h])
-apply (erule (1) fresh_fun_apply' [symmetric])
+apply (erule (1) Fresh_apply' [symmetric])
 done
-lemma fresh_fun_supports:
+lemma Fresh_supports:
 fixes h :: "'a::at \<Rightarrow> 'b::pt"
 assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
-shows "(supp h) supports (fresh_fun h)"
+shows "(supp h) supports (Fresh h)"
 apply (simp add: supports_def fresh_def [symmetric])
-apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)
+apply (simp add: Fresh_eqvt [OF a] swap_fresh_fresh)
 done
-notation fresh_fun (binder "FRESH " 10)
+notation Fresh (binder "FRESH " 10)
 lemma FRESH_f_iff:
 fixes P :: "'a::at \<Rightarrow> 'b::pure"
 fixes f :: "'b \<Rightarrow> 'c::pure"
 assumes P: "finite (supp P)"
 shows "(FRESH x. f (P x)) = f (FRESH x. P x)"
 proof -
 obtain a::'a where "atom a \<sharp> P" using P by (rule obtain_fresh')
 show "(FRESH x. f (P x)) = f (FRESH x. P x)"
-apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh])
+apply (subst Fresh_apply' [where a=a, OF _ pure_fresh])
 apply (cut_tac `atom a \<sharp> P`)
 apply (simp add: fresh_conv_MOST)
 apply (elim MOST_rev_mp, rule MOST_I, clarify)
 apply (simp add: permute_fun_def permute_pure fun_eq_iff)
-apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
+apply (subst Fresh_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
 apply (rule refl)
 done
 qed
 lemma FRESH_binop_iff:
 proof -
 from assms have "finite (supp (P, Q))" by (simp add: supp_Pair)
 then obtain a::'a where "atom a \<sharp> (P, Q)" by (rule obtain_fresh')
 then have "atom a \<sharp> P" and "atom a \<sharp> Q" by (simp_all add: fresh_Pair)
 show ?thesis
-apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh])
+apply (subst Fresh_apply' [where a=a, OF _ pure_fresh])
 apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)
 apply (simp add: fresh_conv_MOST)
 apply (elim MOST_rev_mp, rule MOST_I, clarify)
 apply (simp add: permute_fun_def permute_pure fun_eq_iff)
-apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
+apply (subst Fresh_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
-apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
+apply (subst Fresh_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
 apply (rule refl)
 done
 qed
 lemma FRESH_conj_iff:

changeset 3178	a331468b2f5a
parent 3176	31372760c2fb
child 3180	7b5db6c23753