equal
deleted
inserted
replaced
69 |
69 |
70 text {* Custom syntax for concrete atoms of type at *} |
70 text {* Custom syntax for concrete atoms of type at *} |
71 |
71 |
72 term "a:::name" |
72 term "a:::name" |
73 |
73 |
74 text {* |
|
75 a:::name stands for (atom a) with a being of concrete atom |
|
76 type name. The above lemma can therefore also be stated as |
|
77 |
|
78 "sort_of (a:::name) = Sort ''name'' []" |
|
79 |
|
80 This does not work for multi-sorted atoms. |
|
81 *} |
|
82 |
|
83 (* fixme |
|
84 lemma supp_of_finite_name_set: |
|
85 fixes S::"name set" |
|
86 assumes "infinte S" "infinite (UNIV - S)" |
|
87 shows "supp S = UNIV" |
|
88 proof - |
|
89 { fix a |
|
90 have "a \<in> supp S" |
|
91 proof (cases "a \<in> atom ` S") |
|
92 assume "a \<in> atom ` S" |
|
93 then have "\<forall>b \<in> UNIV - S. (a \<rightleftharpoons> atom b) \<bullet> S \<noteq> S" |
|
94 apply(clarify) |
|
95 |
|
96 show "a \<in> supp S" |
|
97 } |
|
98 then show "supp S = UNIV" by auto |
|
99 qed |
|
100 *) |
|
101 |
|
102 |
74 |
103 section {* Automatic instantiation of class @{text at}. *} |
75 section {* Automatic instantiation of class @{text at}. *} |
104 |
76 |
105 atom_decl name2 |
77 atom_decl name2 |
106 |
78 |