equal
deleted
inserted
replaced
7 |
7 |
8 |
8 |
9 section {* Abstractions *} |
9 section {* Abstractions *} |
10 |
10 |
11 fun |
11 fun |
12 alpha_set |
12 alpha_set |
13 where |
13 where |
14 alpha_set[simp del]: |
14 alpha_set[simp del]: |
15 "alpha_set (bs, x) R f p (cs, y) \<longleftrightarrow> |
15 "alpha_set (bs, x) R f p (cs, y) \<longleftrightarrow> |
16 f x - bs = f y - cs \<and> |
16 f x - bs = f y - cs \<and> |
17 (f x - bs) \<sharp>* p \<and> |
17 (f x - bs) \<sharp>* p \<and> |
1077 by (perm_simp) (rule refl) |
1077 by (perm_simp) (rule refl) |
1078 |
1078 |
1079 lemma prod_fv_supp: |
1079 lemma prod_fv_supp: |
1080 shows "prod_fv supp supp = supp" |
1080 shows "prod_fv supp supp = supp" |
1081 by (rule ext) |
1081 by (rule ext) |
1082 (auto simp add: prod_fv.simps supp_Pair) |
1082 (auto simp add: supp_Pair) |
1083 |
1083 |
1084 lemma prod_alpha_eq: |
1084 lemma prod_alpha_eq: |
1085 shows "prod_alpha (op=) (op=) = (op=)" |
1085 shows "prod_alpha (op=) (op=) = (op=)" |
1086 unfolding prod_alpha_def |
1086 unfolding prod_alpha_def |
1087 by (auto intro!: ext) |
1087 by (auto intro!: ext) |
1088 |
1088 |
1089 |
|
1090 |
|
1091 |
|
1092 |
|
1093 |
|
1094 |
|
1095 end |
1089 end |
1096 |
|