equal
deleted
inserted
replaced
845 using `a \<in> S` `b \<notin> S` `sort_of a = sort_of b` |
845 using `a \<in> S` `b \<notin> S` `sort_of a = sort_of b` |
846 by (rule a3) |
846 by (rule a3) |
847 ultimately show "False" by simp |
847 ultimately show "False" by simp |
848 qed |
848 qed |
849 qed |
849 qed |
|
850 |
|
851 section {* Support w.r.t. relations *} |
|
852 |
|
853 text {* |
|
854 This definition is used for unquotient types, where |
|
855 alpha-equivalence does not coincide with equality. |
|
856 *} |
|
857 |
|
858 definition |
|
859 "supp_rel R x = {a. infinite {b. \<not>(R ((a \<rightleftharpoons> b) \<bullet> x) x)}}" |
|
860 |
|
861 |
850 |
862 |
851 section {* Finitely-supported types *} |
863 section {* Finitely-supported types *} |
852 |
864 |
853 class fs = pt + |
865 class fs = pt + |
854 assumes finite_supp: "finite (supp x)" |
866 assumes finite_supp: "finite (supp x)" |