equal
deleted
inserted
replaced
176 abbreviation |
176 abbreviation |
177 convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd" |
177 convex_add :: "'a convex_pd \<Rightarrow> 'a convex_pd \<Rightarrow> 'a convex_pd" |
178 (infixl "\<union>\<natural>" 65) where |
178 (infixl "\<union>\<natural>" 65) where |
179 "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys" |
179 "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys" |
180 |
180 |
|
181 nonterminal convex_pd_args |
181 syntax |
182 syntax |
182 "_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>") |
183 "" :: "logic \<Rightarrow> convex_pd_args" ("_") |
183 |
184 "_convex_pd_args" :: "logic \<Rightarrow> convex_pd_args \<Rightarrow> convex_pd_args" ("_,/ _") |
|
185 "_convex_pd" :: "convex_pd_args \<Rightarrow> logic" ("{_}\<natural>") |
184 syntax_consts |
186 syntax_consts |
185 "_convex_pd" == convex_add |
187 "_convex_pd_args" "_convex_pd" == convex_add |
186 |
|
187 translations |
188 translations |
188 "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>" |
189 "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>" |
189 "{x}\<natural>" == "CONST convex_unit\<cdot>x" |
190 "{x}\<natural>" == "CONST convex_unit\<cdot>x" |
190 |
191 |
191 lemma convex_unit_Rep_compact_basis [simp]: |
192 lemma convex_unit_Rep_compact_basis [simp]: |