13 "der_syn r c \<equiv> der c r" |
13 "der_syn r c \<equiv> der c r" |
14 |
14 |
15 abbreviation |
15 abbreviation |
16 "ders_syn r s \<equiv> ders s r" |
16 "ders_syn r s \<equiv> ders s r" |
17 |
17 |
|
18 (* |
18 notation (latex output) |
19 notation (latex output) |
19 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and |
20 If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) |
|
21 *) |
|
22 (* |
|
23 notation (latex output) |
20 Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and |
24 Cons ("_\<^raw:\mbox{$\,$}>::\<^raw:\mbox{$\,$}>_" [75,73] 73) and |
21 |
25 *) |
|
26 |
|
27 (* |
|
28 notation (latex output) |
22 ZERO ("\<^bold>0" 78) and |
29 ZERO ("\<^bold>0" 78) and |
23 ONE ("\<^bold>1" 78) and |
30 ONE ("\<^bold>1" 78) and |
24 CHAR ("_" [1000] 80) and |
31 CH ("_" [1000] 80) and |
25 ALT ("_ + _" [77,77] 78) and |
32 ALT ("_ + _" [77,77] 78) and |
26 SEQ ("_ \<cdot> _" [77,77] 78) and |
33 SEQ ("_ \<cdot> _" [77,77] 78) and |
27 STAR ("_\<^sup>\<star>" [1000] 78) and |
34 STAR ("_\<^sup>\<star>" [1000] 78) and |
28 |
35 |
29 val.Void ("'(')" 1000) and |
36 val.Void ("'(')" 1000) and |
53 F_SEQ2 ("F\<^bsub>Seq2\<^esub> _ _") and |
60 F_SEQ2 ("F\<^bsub>Seq2\<^esub> _ _") and |
54 F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and |
61 F_SEQ ("F\<^bsub>Seq\<^esub> _ _") and |
55 simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and |
62 simp_SEQ ("simp\<^bsub>Seq\<^esub> _ _" [1000, 1000] 1) and |
56 simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and |
63 simp_ALT ("simp\<^bsub>Alt\<^esub> _ _" [1000, 1000] 1) and |
57 slexer ("lexer\<^sup>+" 1000) and |
64 slexer ("lexer\<^sup>+" 1000) and |
58 |
65 *) |
|
66 |
|
67 (* |
|
68 notation (latex output) |
59 ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and |
69 ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and |
60 ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77) |
70 ValOrdEq ("_ \<ge>\<^bsub>_\<^esub> _" [77,77,77] 77) |
|
71 *) |
61 |
72 |
62 definition |
73 definition |
63 "match r s \<equiv> nullable (ders s r)" |
74 "match r s \<equiv> nullable (ders s r)" |
64 |
75 |
65 (* |
76 (* |
403 @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[4mm] |
414 @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[4mm] |
404 @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad |
415 @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad |
405 @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[4mm] |
416 @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[4mm] |
406 @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[4mm] |
417 @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[4mm] |
407 @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad |
418 @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad |
408 @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]} |
419 %%@ { thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]} |
409 \end{tabular} |
420 \end{tabular} |
410 \end{center} |
421 \end{center} |
411 |
422 |
412 \noindent Note that no values are associated with the regular expression |
423 \noindent Note that no values are associated with the regular expression |
413 @{term ZERO}, and that the only value associated with the regular |
424 @{term ZERO}, and that the only value associated with the regular |
1022 Their central definition is an ``ordering relation'' defined by the |
1033 Their central definition is an ``ordering relation'' defined by the |
1023 rules (slightly adapted to fit our notation): |
1034 rules (slightly adapted to fit our notation): |
1024 |
1035 |
1025 \begin{center} |
1036 \begin{center} |
1026 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
1037 \begin{tabular}{@ {}c@ {\hspace{4mm}}c@ {}} |
1027 @{thm[mode=Rule] C2[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>1\<iota>" "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>"]}\,(C2) & |
1038 ??? & |
1028 @{thm[mode=Rule] C1[of "v\<^sub>2" "r\<^sub>2" "v\<^sub>2\<iota>" "v\<^sub>1" "r\<^sub>1"]}\,(C1)\smallskip\\ |
1039 ??? \smallskip\\ |
1029 |
1040 |
1030 @{thm[mode=Rule] A1[of "v\<^sub>1" "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\,(A1) & |
|
1031 @{thm[mode=Rule] A2[of "v\<^sub>2" "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]}\,(A2)\smallskip\\ |
|
1032 |
|
1033 @{thm[mode=Rule] A3[of "v\<^sub>1" "r\<^sub>2" "v\<^sub>2" "r\<^sub>1"]}\,(A3) & |
|
1034 @{thm[mode=Rule] A4[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\,(A4)\smallskip\\ |
|
1035 |
|
1036 @{thm[mode=Rule] K1[of "v" "vs" "r"]}\,(K1) & |
|
1037 @{thm[mode=Rule] K2[of "v" "vs" "r"]}\,(K2)\smallskip\\ |
|
1038 |
|
1039 @{thm[mode=Rule] K3[of "v\<^sub>1" "r" "v\<^sub>2" "vs\<^sub>1" "vs\<^sub>2"]}\,(K3) & |
|
1040 @{thm[mode=Rule] K4[of "vs\<^sub>1" "r" "vs\<^sub>2" "v"]}\,(K4) |
|
1041 \end{tabular} |
1041 \end{tabular} |
1042 \end{center} |
1042 \end{center} |
1043 |
1043 |
1044 \noindent The idea behind the rules (A1) and (A2), for example, is that a |
1044 \noindent The idea behind the rules (A1) and (A2), for example, is that a |
1045 @{text Left}-value is bigger than a @{text Right}-value, if the underlying |
1045 @{text Left}-value is bigger than a @{text Right}-value, if the underlying |
1060 string is. This seems to be only a very minor difference, but it has |
1060 string is. This seems to be only a very minor difference, but it has |
1061 drastic consequences in terms of what properties both orderings enjoy. |
1061 drastic consequences in terms of what properties both orderings enjoy. |
1062 What is interesting for our purposes is that the properties reflexivity, |
1062 What is interesting for our purposes is that the properties reflexivity, |
1063 totality and transitivity for this GREEDY ordering can be proved |
1063 totality and transitivity for this GREEDY ordering can be proved |
1064 relatively easily by induction. |
1064 relatively easily by induction. |
1065 |
1065 *} |
|
1066 |
|
1067 (* |
1066 These properties of GREEDY, however, do not transfer to the POSIX |
1068 These properties of GREEDY, however, do not transfer to the POSIX |
1067 ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. |
1069 ``ordering'' by Sulzmann and Lu, which they define as @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"}. |
1068 To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is |
1070 To start with, @{text "v\<^sub>1 \<ge>\<^sub>r v\<^sub>2"} is |
1069 not defined inductively, but as $($@{term "v\<^sub>1 = v\<^sub>2"}$)$ $\vee$ $($@{term "(v\<^sub>1 >r |
1071 not defined inductively, but as $($@{term "v\<^sub>1 = v\<^sub>2"}$)$ $\vee$ $($@{term "(v\<^sub>1 >r |
1070 v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}$)$. This means that @{term "v\<^sub>1 |
1072 v\<^sub>2) \<and> (flat v\<^sub>1 = flat (v\<^sub>2::val))"}$)$. This means that @{term "v\<^sub>1 |
1071 >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp) |
1073 >(r::rexp) (v\<^sub>2::val)"} does not necessarily imply @{term "v\<^sub>1 \<ge>(r::rexp) |
1072 (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual'' |
1074 (v\<^sub>2::val)"}. Moreover, transitivity does not hold in the ``usual'' |
1073 formulation, for example: |
1075 formulation, for example: |
1074 |
1076 *) |
|
1077 |
|
1078 text {* |
1075 \begin{falsehood} |
1079 \begin{falsehood} |
1076 Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}. |
1080 Suppose @{term "\<turnstile> v\<^sub>1 : r"}, @{term "\<turnstile> v\<^sub>2 : r"} and @{term "\<turnstile> v\<^sub>3 : r"}. |
1077 If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"} |
1081 If @{term "v\<^sub>1 >(r::rexp) (v\<^sub>2::val)"} and @{term "v\<^sub>2 >(r::rexp) (v\<^sub>3::val)"} |
1078 then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}. |
1082 then @{term "v\<^sub>1 >(r::rexp) (v\<^sub>3::val)"}. |
1079 \end{falsehood} |
1083 \end{falsehood} |