equal
deleted
inserted
replaced
180 lemma [intro]: |
180 lemma [intro]: |
181 "x \<in> A \<Longrightarrow> replicate n x \<in> list n A" |
181 "x \<in> A \<Longrightarrow> replicate n x \<in> list n A" |
182 by (induct n, auto) |
182 by (induct n, auto) |
183 |
183 |
184 lemma lesubstep_type_simple: |
184 lemma lesubstep_type_simple: |
185 "a <=[Product.le (op =) r] b \<Longrightarrow> a \<le>|r| b" |
185 "a <=[Product.le (=) r] b \<Longrightarrow> a \<le>|r| b" |
186 apply (unfold lesubstep_type_def) |
186 apply (unfold lesubstep_type_def) |
187 apply clarify |
187 apply clarify |
188 apply (simp add: set_conv_nth) |
188 apply (simp add: set_conv_nth) |
189 apply clarify |
189 apply clarify |
190 apply (drule le_listD, assumption) |
190 apply (drule le_listD, assumption) |