equal
deleted
inserted
replaced
41 lemma in_nlists_Suc_iff: "(xs \<in> nlists (Suc n) A) = (\<exists>y\<in>A. \<exists>ys \<in> nlists n A. xs = y#ys)" |
41 lemma in_nlists_Suc_iff: "(xs \<in> nlists (Suc n) A) = (\<exists>y\<in>A. \<exists>ys \<in> nlists n A. xs = y#ys)" |
42 unfolding nlists_def by (cases "xs") auto |
42 unfolding nlists_def by (cases "xs") auto |
43 |
43 |
44 lemma Cons_in_nlists_Suc [iff]: "(x#xs \<in> nlists (Suc n) A) \<longleftrightarrow> (x\<in>A \<and> xs \<in> nlists n A)" |
44 lemma Cons_in_nlists_Suc [iff]: "(x#xs \<in> nlists (Suc n) A) \<longleftrightarrow> (x\<in>A \<and> xs \<in> nlists n A)" |
45 unfolding nlists_def by (auto) |
45 unfolding nlists_def by (auto) |
|
46 |
|
47 lemma nlists_Suc: "nlists (Suc n) A = (\<Union>a\<in>A. (#) a ` nlists n A)" |
|
48 by(auto simp: set_eq_iff image_iff in_nlists_Suc_iff) |
46 |
49 |
47 lemma nlists_not_empty: "A\<noteq>{} \<Longrightarrow> \<exists>xs. xs \<in> nlists n A" |
50 lemma nlists_not_empty: "A\<noteq>{} \<Longrightarrow> \<exists>xs. xs \<in> nlists n A" |
48 by (induct "n") (auto simp: in_nlists_Suc_iff) |
51 by (induct "n") (auto simp: in_nlists_Suc_iff) |
49 |
52 |
50 |
53 |