equal
deleted
inserted
replaced
18 by (simp_all add: Sequ_def) |
18 by (simp_all add: Sequ_def) |
19 |
19 |
20 lemma Sequ_empty [simp]: |
20 lemma Sequ_empty [simp]: |
21 shows "A ;; {} = {}" |
21 shows "A ;; {} = {}" |
22 and "{} ;; A = {}" |
22 and "{} ;; A = {}" |
23 by (simp_all add: Sequ_def) |
23 by (simp_all add: Sequ_def) |
24 |
24 |
|
25 lemma |
|
26 shows "(A \<union> B) ;; C = (A ;; C) \<union> (B ;; C)" |
|
27 apply(auto simp add: Sequ_def) |
|
28 done |
|
29 |
|
30 lemma |
|
31 shows "(A \<inter> B) ;; C \<subseteq> (A ;; C) \<inter> (B ;; C)" |
|
32 apply(auto simp add: Sequ_def) |
|
33 done |
|
34 |
|
35 lemma |
|
36 shows "(A ;; C) \<inter> (B ;; C) \<subseteq> (A \<inter> B) ;; C" |
|
37 apply(auto simp add: Sequ_def) |
|
38 oops |
25 |
39 |
26 section {* Semantic Derivative (Left Quotient) of Languages *} |
40 section {* Semantic Derivative (Left Quotient) of Languages *} |
27 |
41 |
28 definition |
42 definition |
29 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
43 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |