12 where "nlists n A = {xs. size xs = n \<and> set xs \<subseteq> A}" |
12 where "nlists n A = {xs. size xs = n \<and> set xs \<subseteq> A}" |
13 |
13 |
14 lemma nlistsI: "\<lbrakk> size xs = n; set xs \<subseteq> A \<rbrakk> \<Longrightarrow> xs \<in> nlists n A" |
14 lemma nlistsI: "\<lbrakk> size xs = n; set xs \<subseteq> A \<rbrakk> \<Longrightarrow> xs \<in> nlists n A" |
15 by (simp add: nlists_def) |
15 by (simp add: nlists_def) |
16 |
16 |
17 lemma nlistsE_length [simp](*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> size xs = n" |
17 lemma nlistsE_length (*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> size xs = n" |
18 by (simp add: nlists_def) |
18 by (simp add: nlists_def) |
19 |
19 |
20 lemma less_lengthI: "\<lbrakk> xs \<in> nlists n A; p < n \<rbrakk> \<Longrightarrow> p < size xs" |
20 lemma less_lengthI: "\<lbrakk> xs \<in> nlists n A; p < n \<rbrakk> \<Longrightarrow> p < size xs" |
21 by (simp) |
21 by (simp add: nlistsE_length) |
22 |
22 |
23 lemma nlistsE_set[simp](*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> set xs \<subseteq> A" |
23 lemma nlistsE_set[simp](*rm simp del*): "xs \<in> nlists n A \<Longrightarrow> set xs \<subseteq> A" |
24 unfolding nlists_def by (simp) |
24 unfolding nlists_def by (simp) |
25 |
25 |
26 lemma nlists_mono: |
26 lemma nlists_mono: |
27 assumes "A \<subseteq> B" shows "nlists n A \<subseteq> nlists n B" |
27 assumes "A \<subseteq> B" shows "nlists n A \<subseteq> nlists n B" |
28 proof |
28 proof |
29 fix xs assume "xs \<in> nlists n A" |
29 fix xs assume "xs \<in> nlists n A" |
30 then obtain size: "size xs = n" and inA: "set xs \<subseteq> A" by simp |
30 then obtain size: "size xs = n" and inA: "set xs \<subseteq> A" by (simp add:nlistsE_length) |
31 with assms have "set xs \<subseteq> B" by simp |
31 with assms have "set xs \<subseteq> B" by simp |
32 with size show "xs \<in> nlists n B" by(clarsimp intro!: nlistsI) |
32 with size show "xs \<in> nlists n B" by(clarsimp intro!: nlistsI) |
33 qed |
33 qed |
34 |
34 |
35 lemma nlists_n_0 [simp]: "nlists 0 A = {[]}" |
35 lemma nlists_n_0 [simp]: "nlists 0 A = {[]}" |