equal
deleted
inserted
replaced
60 lemma Der_char [simp]: |
60 lemma Der_char [simp]: |
61 shows "Der c {[d]} = (if c = d then {[]} else {})" |
61 shows "Der c {[d]} = (if c = d then {[]} else {})" |
62 unfolding Der_def |
62 unfolding Der_def |
63 by auto |
63 by auto |
64 |
64 |
|
65 lemma Der_Sequ [simp]: |
|
66 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
|
67 unfolding Der_def Sequ_def |
|
68 by (auto simp add: Cons_eq_append_conv) |
|
69 |
65 lemma Der_union [simp]: |
70 lemma Der_union [simp]: |
66 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
71 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
67 unfolding Der_def |
72 unfolding Der_def |
68 by auto |
73 by auto |
69 |
|
70 lemma Der_Sequ [simp]: |
|
71 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
|
72 unfolding Der_def Sequ_def |
|
73 by (auto simp add: Cons_eq_append_conv) |
|
74 |
74 |
75 lemma Der_UNION: |
75 lemma Der_UNION: |
76 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
76 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
77 by (auto simp add: Der_def) |
77 by (auto simp add: Der_def) |
78 |
78 |