diff -r 5fed809d0fc1 -r f460d5f75cb5 Matcher.thy --- a/Matcher.thy Mon Feb 14 11:12:01 2011 +0000 +++ b/Matcher.thy Mon Feb 14 23:10:44 2011 +0000 @@ -6,9 +6,9 @@ section {* Sequential Composition of Sets *} fun - lang_seq :: "string set \ string set \ string set" ("_ ; _" [100,100] 100) + lang_seq :: "string set \ string set \ string set" ("_ ;; _" [100,100] 100) where - "L1 ; L2 = {s1 @ s2 | s1 s2. s1 \ L1 \ s2 \ L2}" + "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \ L1 \ s2 \ L2}" section {* Kleene Star for Sets *} @@ -24,7 +24,7 @@ text {* A standard property of Star *} lemma lang_star_cases: - shows "L\ = {[]} \ L ; L\" + shows "L\ = {[]} \ L ;; L\" by (auto) (metis Star.simps) section {* Regular Expressions *} @@ -37,14 +37,39 @@ | ALT rexp rexp | STAR rexp +types lang = "string set" definition + DERIV :: "string \ lang \ lang" +where "DERIV s A \ {s'. s @ s' \ A}" definition + delta :: "lang \ lang" +where "delta A = (if [] \ A then {[]} else {})" +lemma + "DERIV s (P ; Q) = \{(delta (DERIV s1 P)) ; (DERIV s2 Q) | s1 s2. s = s1 @ s2}" +apply(auto) +fun + D1 :: "string \ lang \ lang" +where + "D1 [] A = A" +| "D1 (c # s) A = DERIV [c] (D1 s A)" + +fun + D2 :: "string \ lang \ lang" +where + "D2 [] A = A" +| "D2 (c # s) A = DERIV [c] (D1 s A)" + +function + D +where + "D s P Q = P ;; Q" +| "D (c#s) = section {* Semantics of Regular Expressions *}