1065 lemma fresh_conv_MOST: |
1065 lemma fresh_conv_MOST: |
1066 shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)" |
1066 shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)" |
1067 unfolding fresh_def supp_def |
1067 unfolding fresh_def supp_def |
1068 unfolding MOST_iff_cofinite by simp |
1068 unfolding MOST_iff_cofinite by simp |
1069 |
1069 |
|
1070 lemma supp_subset_fresh: |
|
1071 assumes a: "\<And>a. a \<sharp> x \<Longrightarrow> a \<sharp> y" |
|
1072 shows "supp y \<subseteq> supp x" |
|
1073 using a |
|
1074 unfolding fresh_def |
|
1075 by blast |
|
1076 |
1070 lemma fresh_fun_app: |
1077 lemma fresh_fun_app: |
1071 assumes "a \<sharp> f" and "a \<sharp> x" |
1078 assumes "a \<sharp> f" and "a \<sharp> x" |
1072 shows "a \<sharp> f x" |
1079 shows "a \<sharp> f x" |
1073 using assms |
1080 using assms |
1074 unfolding fresh_conv_MOST |
1081 unfolding fresh_conv_MOST |
1075 unfolding permute_fun_app_eq |
1082 unfolding permute_fun_app_eq |
1076 by (elim MOST_rev_mp, simp) |
1083 by (elim MOST_rev_mp, simp) |
1077 |
1084 |
1078 lemma supp_fun_app: |
1085 lemma supp_fun_app: |
1079 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1086 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1080 using fresh_fun_app |
1087 using fresh_fun_app |
1081 unfolding fresh_def |
1088 unfolding fresh_def |
1082 by auto |
1089 by auto |
1083 |
1090 |
|
1091 text {* support of equivariant functions *} |
|
1092 |
1084 lemma supp_fun_eqvt: |
1093 lemma supp_fun_eqvt: |
1085 assumes a: "\<forall>p. p \<bullet> f = f" |
1094 assumes a: "\<And>p. p \<bullet> f = f" |
1086 shows "supp f = {}" |
1095 shows "supp f = {}" |
1087 unfolding supp_def |
1096 unfolding supp_def |
1088 using a by simp |
1097 using a by simp |
1089 |
1098 |
1090 |
|
1091 lemma fresh_fun_eqvt_app: |
1099 lemma fresh_fun_eqvt_app: |
1092 assumes a: "\<forall>p. p \<bullet> f = f" |
1100 assumes a: "\<And>p. p \<bullet> f = f" |
1093 shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1101 shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1094 proof - |
1102 proof - |
1095 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
1103 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
1096 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1104 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1097 unfolding fresh_def |
1105 unfolding fresh_def |
1098 using supp_fun_app |
1106 using supp_fun_app by auto |
1099 by auto |
|
1100 qed |
1107 qed |
1101 |
1108 |
1102 |
1109 |
1103 section {* Concrete atoms types *} |
1110 section {* Concrete atoms types *} |
1104 |
1111 |