equal
deleted
inserted
replaced
20 assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b" |
20 assumes atom_eq_iff [simp]: "atom a = atom b \<longleftrightarrow> a = b" |
21 assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)" |
21 assumes atom_eqvt: "p \<bullet> (atom a) = atom (p \<bullet> a)" |
22 |
22 |
23 class at = at_base + |
23 class at = at_base + |
24 assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" |
24 assumes sort_of_atom_eq [simp]: "sort_of (atom a) = sort_of (atom b)" |
25 |
|
26 instance at < at_base .. |
|
27 |
25 |
28 lemma supp_at_base: |
26 lemma supp_at_base: |
29 fixes a::"'a::at_base" |
27 fixes a::"'a::at_base" |
30 shows "supp a = {atom a}" |
28 shows "supp a = {atom a}" |
31 by (simp add: supp_atom [symmetric] supp_def atom_eqvt) |
29 by (simp add: supp_atom [symmetric] supp_def atom_eqvt) |
144 using assms |
142 using assms |
145 by (simp add: flip_def swap_fresh_fresh) |
143 by (simp add: flip_def swap_fresh_fresh) |
146 |
144 |
147 subsection {* Syntax for coercing at-elements to the atom-type *} |
145 subsection {* Syntax for coercing at-elements to the atom-type *} |
148 |
146 |
149 (* |
|
150 syntax |
147 syntax |
151 "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3) |
148 "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3) |
152 |
149 |
153 translations |
150 translations |
154 "_atom_constrain a t" => "atom (_constrain a t)" |
151 "_atom_constrain a t" => "CONST atom (_constrain a t)" |
155 *) |
152 |
156 |
153 |
157 subsection {* A lemma for proving instances of class @{text at}. *} |
154 subsection {* A lemma for proving instances of class @{text at}. *} |
158 |
155 |
159 setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *} |
156 setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *} |
160 setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *} |
157 setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *} |