10 UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set" |
10 UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set" |
11 |
11 |
12 abbreviation |
12 abbreviation |
13 "EClass x R \<equiv> R `` {x}" |
13 "EClass x R \<equiv> R `` {x}" |
14 |
14 |
15 abbreviation |
15 abbreviation |
16 "append_rexp2 r_itm r \<equiv> append_rexp r r_itm" |
16 "Append_rexp2 r_itm r == Append_rexp r r_itm" |
17 |
|
18 |
17 |
19 notation (latex output) |
18 notation (latex output) |
20 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and |
19 str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and |
21 str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and |
20 str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and |
22 Seq (infixr "\<cdot>" 100) and |
21 Seq (infixr "\<cdot>" 100) and |
30 Lam ("\<lambda>'(_')" [100] 100) and |
29 Lam ("\<lambda>'(_')" [100] 100) and |
31 Trn ("'(_, _')" [100, 100] 100) and |
30 Trn ("'(_, _')" [100, 100] 100) and |
32 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and |
31 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and |
33 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and |
32 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and |
34 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and |
33 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and |
35 append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and |
34 Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and |
36 append_rhs_rexp ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and |
35 Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and |
|
36 |
37 uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and |
37 uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and |
38 tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and |
38 tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and |
39 tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and |
39 tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and |
40 tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and |
40 tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and |
41 tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and |
41 tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and |
492 Overloading the function @{text \<calL>} for the two kinds of terms in the |
492 Overloading the function @{text \<calL>} for the two kinds of terms in the |
493 equational system, we have |
493 equational system, we have |
494 |
494 |
495 \begin{center} |
495 \begin{center} |
496 @{text "\<calL>(Y, r) \<equiv>"} % |
496 @{text "\<calL>(Y, r) \<equiv>"} % |
497 @{thm (rhs) L_rhs_item.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm} |
497 @{thm (rhs) L_rhs_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm} |
498 @{thm L_rhs_item.simps(1)[where r="r", THEN eq_reflection]} |
498 @{thm L_rhs_trm.simps(1)[where r="r", THEN eq_reflection]} |
499 \end{center} |
499 \end{center} |
500 |
500 |
501 \noindent |
501 \noindent |
502 and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations |
502 and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations |
503 % |
503 % |
559 and substitutes @{text X} throughout the rest of the equational system |
559 and substitutes @{text X} throughout the rest of the equational system |
560 adjusting the remaining regular expressions appropriately. To define this adjustment |
560 adjusting the remaining regular expressions appropriately. To define this adjustment |
561 we define the \emph{append-operation} taking a term and a regular expression as argument |
561 we define the \emph{append-operation} taking a term and a regular expression as argument |
562 |
562 |
563 \begin{center} |
563 \begin{center} |
564 @{thm append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm} |
564 @{thm Append_rexp.simps(2)[where X="Y" and r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]}\hspace{10mm} |
565 @{thm append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]} |
565 @{thm Append_rexp.simps(1)[where r="r\<^isub>1" and rexp="r\<^isub>2", THEN eq_reflection]} |
566 \end{center} |
566 \end{center} |
567 |
567 |
568 \noindent |
568 \noindent |
569 We lift this operation to entire right-hand sides of equations, written as |
569 We lift this operation to entire right-hand sides of equations, written as |
570 @{thm (lhs) append_rhs_rexp_def[where rexp="r"]}. With this we can define |
570 @{thm (lhs) Append_rexp_rhs_def[where rexp="r"]}. With this we can define |
571 the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as: |
571 the \emph{arden-operation} for an equation of the form @{text "X = rhs"} as: |
572 % |
572 % |
573 \begin{equation}\label{arden_def} |
573 \begin{equation}\label{arden_def} |
574 \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l} |
574 \mbox{\begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l} |
575 @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\ |
575 @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\ |
710 \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}} |
710 \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}} |
711 @{text "invariant ES"} & @{text "\<equiv>"} & |
711 @{text "invariant ES"} & @{text "\<equiv>"} & |
712 @{term "finite ES"} & @{text "(finiteness)"}\\ |
712 @{term "finite ES"} & @{text "(finiteness)"}\\ |
713 & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\ |
713 & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\ |
714 & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\ |
714 & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\ |
715 & @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\ |
715 & @{text "\<and>"} & @{thm (rhs) distinctness_def}\\ |
716 & & & @{text "(distinctness)"}\\ |
716 & & & @{text "(distinctness)"}\\ |
717 & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\ |
717 & @{text "\<and>"} & @{thm (rhs) ardenable_all_def} & @{text "(ardenable)"}\\ |
718 & @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\ |
718 & @{text "\<and>"} & @{thm (rhs) validity_def} & @{text "(validity)"}\\ |
719 \end{tabular} |
719 \end{tabular} |
720 \end{center} |
720 \end{center} |
721 |
721 |
722 \noindent |
722 \noindent |
723 The first two ensure that the equational system is always finite (number of equations |
723 The first two ensure that the equational system is always finite (number of equations |