equal
deleted
inserted
replaced
1079 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1079 shows "supp (f x) \<subseteq> (supp f) \<union> (supp x)" |
1080 using fresh_fun_app |
1080 using fresh_fun_app |
1081 unfolding fresh_def |
1081 unfolding fresh_def |
1082 by auto |
1082 by auto |
1083 |
1083 |
|
1084 lemma supp_fun_eqvt: |
|
1085 assumes a: "\<forall>p. p \<bullet> f = f" |
|
1086 shows "supp f = {}" |
|
1087 unfolding supp_def |
|
1088 using a by simp |
|
1089 |
|
1090 |
1084 lemma fresh_fun_eqvt_app: |
1091 lemma fresh_fun_eqvt_app: |
1085 assumes a: "\<forall>p. p \<bullet> f = f" |
1092 assumes a: "\<forall>p. p \<bullet> f = f" |
1086 shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1093 shows "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1087 proof - |
1094 proof - |
1088 from a have "supp f = {}" |
1095 from a have "supp f = {}" by (simp add: supp_fun_eqvt) |
1089 unfolding supp_def by simp |
|
1090 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1096 then show "a \<sharp> x \<Longrightarrow> a \<sharp> f x" |
1091 unfolding fresh_def |
1097 unfolding fresh_def |
1092 using supp_fun_app |
1098 using supp_fun_app |
1093 by auto |
1099 by auto |
1094 qed |
1100 qed |