equal
deleted
inserted
replaced
50 flat ("|_|" [75] 74) and |
50 flat ("|_|" [75] 74) and |
51 Sequ ("_ @ _" [78,77] 63) and |
51 Sequ ("_ @ _" [78,77] 63) and |
52 injval ("inj _ _ _" [79,77,79] 76) and |
52 injval ("inj _ _ _" [79,77,79] 76) and |
53 mkeps ("mkeps _" [79] 76) and |
53 mkeps ("mkeps _" [79] 76) and |
54 length ("len _" [73] 73) and |
54 length ("len _" [73] 73) and |
|
55 intlen ("len _" [73] 73) and |
55 |
56 |
56 Prf ("_ : _" [75,75] 75) and |
57 Prf ("_ : _" [75,75] 75) and |
57 Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and |
58 Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and |
58 |
59 |
59 lexer ("lexer _ _" [78,78] 77) and |
60 lexer ("lexer _ _" [78,78] 77) and |
69 |
70 |
70 at ("_\<^raw:\mbox{$\downharpoonleft$}>\<^bsub>_\<^esub>") and |
71 at ("_\<^raw:\mbox{$\downharpoonleft$}>\<^bsub>_\<^esub>") and |
71 lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and |
72 lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and |
72 PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and |
73 PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and |
73 PosOrd_ex ("_ \<prec> _" [77,77] 77) and |
74 PosOrd_ex ("_ \<prec> _" [77,77] 77) and |
74 PosOrd_ex1 ("_ \<^raw:\mbox{$\preccurlyeq$}> _" [77,77] 77) and |
75 PosOrd_ex_eq ("_ \<^raw:\mbox{$\preccurlyeq$}> _" [77,77] 77) and |
75 pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and |
76 pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and |
76 nprec ("_ \<^raw:\mbox{$\not\prec$}> _" [77,77] 77) |
77 nprec ("_ \<^raw:\mbox{$\not\prec$}> _" [77,77] 77) |
77 |
78 |
78 (* |
79 (* |
79 ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and |
80 ValOrd ("_ >\<^bsub>_\<^esub> _" [77,77,77] 77) and |
428 \\[-8mm] |
429 \\[-8mm] |
429 @{thm[mode=Axiom] Prf.intros(4)} \qquad |
430 @{thm[mode=Axiom] Prf.intros(4)} \qquad |
430 @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[4mm] |
431 @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[4mm] |
431 @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad |
432 @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad |
432 @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[4mm] |
433 @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[4mm] |
433 @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[4mm] |
434 @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]} \qquad |
434 @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad |
435 @{thm[mode=Rule] Prf.intros(6)[of "vs"]} |
435 @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]} |
|
436 \end{tabular} |
436 \end{tabular} |
437 \end{center} |
437 \end{center} |
438 |
438 |
439 \noindent Note that no values are associated with the regular expression |
439 \noindent Note that no values are associated with the regular expression |
440 @{term ZERO}, and that the only value associated with the regular |
440 @{term ZERO}, and that the only value associated with the regular |
1096 \end{tabular} |
1096 \end{tabular} |
1097 \end{center} |
1097 \end{center} |
1098 |
1098 |
1099 @{thm PosOrd_ex_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} |
1099 @{thm PosOrd_ex_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} |
1100 |
1100 |
1101 @{thm PosOrd_ex1_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} |
1101 @{thm PosOrd_ex_eq_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} |
1102 |
1102 |
1103 Lemma 1 |
1103 Lemma 1 |
1104 |
1104 |
1105 @{thm [mode=IfThen] PosOrd_shorterE[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} |
1105 @{thm [mode=IfThen] PosOrd_shorterE[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]} |
1106 |
1106 |