equal
deleted
inserted
replaced
4 |
4 |
5 |
5 |
6 section {* Sequential Composition of Sets *} |
6 section {* Sequential Composition of Sets *} |
7 |
7 |
8 fun |
8 fun |
9 lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100) |
9 lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
10 where |
10 where |
11 "L1 ; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}" |
11 "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}" |
12 |
12 |
13 |
13 |
14 section {* Kleene Star for Sets *} |
14 section {* Kleene Star for Sets *} |
15 |
15 |
16 inductive_set |
16 inductive_set |
22 |
22 |
23 |
23 |
24 text {* A standard property of Star *} |
24 text {* A standard property of Star *} |
25 |
25 |
26 lemma lang_star_cases: |
26 lemma lang_star_cases: |
27 shows "L\<star> = {[]} \<union> L ; L\<star>" |
27 shows "L\<star> = {[]} \<union> L ;; L\<star>" |
28 by (auto) (metis Star.simps) |
28 by (auto) (metis Star.simps) |
29 |
29 |
30 section {* Regular Expressions *} |
30 section {* Regular Expressions *} |
31 |
31 |
32 datatype rexp = |
32 datatype rexp = |
35 | CHAR char |
35 | CHAR char |
36 | SEQ rexp rexp |
36 | SEQ rexp rexp |
37 | ALT rexp rexp |
37 | ALT rexp rexp |
38 | STAR rexp |
38 | STAR rexp |
39 |
39 |
|
40 types lang = "string set" |
40 |
41 |
41 definition |
42 definition |
|
43 DERIV :: "string \<Rightarrow> lang \<Rightarrow> lang" |
|
44 where |
42 "DERIV s A \<equiv> {s'. s @ s' \<in> A}" |
45 "DERIV s A \<equiv> {s'. s @ s' \<in> A}" |
43 |
46 |
44 definition |
47 definition |
|
48 delta :: "lang \<Rightarrow> lang" |
|
49 where |
45 "delta A = (if [] \<in> A then {[]} else {})" |
50 "delta A = (if [] \<in> A then {[]} else {})" |
46 |
51 |
|
52 lemma |
|
53 "DERIV s (P ; Q) = \<Union>{(delta (DERIV s1 P)) ; (DERIV s2 Q) | s1 s2. s = s1 @ s2}" |
|
54 apply(auto) |
47 |
55 |
|
56 fun |
|
57 D1 :: "string \<Rightarrow> lang \<Rightarrow> lang" |
|
58 where |
|
59 "D1 [] A = A" |
|
60 | "D1 (c # s) A = DERIV [c] (D1 s A)" |
|
61 |
|
62 fun |
|
63 D2 :: "string \<Rightarrow> lang \<Rightarrow> lang" |
|
64 where |
|
65 "D2 [] A = A" |
|
66 | "D2 (c # s) A = DERIV [c] (D1 s A)" |
|
67 |
|
68 function |
|
69 D |
|
70 where |
|
71 "D s P Q = P ;; Q" |
|
72 | "D (c#s) = |
48 |
73 |
49 section {* Semantics of Regular Expressions *} |
74 section {* Semantics of Regular Expressions *} |
50 |
75 |
51 fun |
76 fun |
52 L :: "rexp \<Rightarrow> string set" |
77 L :: "rexp \<Rightarrow> string set" |