380 "trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}" |
380 "trns_of rhs X \<equiv> {Trn X r | r. Trn X r \<in> rhs}" |
381 |
381 |
382 text {* Transitions between equivalence classes *} |
382 text {* Transitions between equivalence classes *} |
383 |
383 |
384 definition |
384 definition |
385 transition :: "lang \<Rightarrow> rexp \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100) |
385 transition :: "lang \<Rightarrow> char \<Rightarrow> lang \<Rightarrow> bool" ("_ \<Turnstile>_\<Rightarrow>_" [100,100,100] 100) |
386 where |
386 where |
387 "Y \<Turnstile>r\<Rightarrow> X \<equiv> Y ;; (L r) \<subseteq> X" |
387 "Y \<Turnstile>c\<Rightarrow> X \<equiv> Y ;; {[c]} \<subseteq> X" |
388 |
388 |
389 text {* Initial equational system *} |
389 text {* Initial equational system *} |
390 |
390 |
391 definition |
391 definition |
392 "init_rhs CS X \<equiv> |
392 "init_rhs CS X \<equiv> |
393 if ([] \<in> X) then |
393 if ([] \<in> X) then |
394 {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X} |
394 {Lam EMPTY} \<union> {Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} |
395 else |
395 else |
396 {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}" |
396 {Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}" |
397 |
397 |
398 definition |
398 definition |
399 "eqs CS \<equiv> {(X, init_rhs CS X) | X. X \<in> CS}" |
399 "eqs CS \<equiv> {(X, init_rhs CS X) | X. X \<in> CS}" |
400 |
400 |
401 |
401 |
406 The function @{text "attach_rexp r item"} SEQ-composes @{text r} to the |
406 The function @{text "attach_rexp r item"} SEQ-composes @{text r} to the |
407 right of every rhs-item. |
407 right of every rhs-item. |
408 *} |
408 *} |
409 |
409 |
410 fun |
410 fun |
411 attach_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item" |
411 append_rexp :: "rexp \<Rightarrow> rhs_item \<Rightarrow> rhs_item" |
412 where |
412 where |
413 "attach_rexp r (Lam rexp) = Lam (SEQ rexp r)" |
413 "append_rexp r (Lam rexp) = Lam (SEQ rexp r)" |
414 | "attach_rexp r (Trn X rexp) = Trn X (SEQ rexp r)" |
414 | "append_rexp r (Trn X rexp) = Trn X (SEQ rexp r)" |
415 |
415 |
416 |
416 |
417 definition |
417 definition |
418 "append_rhs_rexp rhs rexp \<equiv> (attach_rexp rexp) ` rhs" |
418 "append_rhs_rexp rhs rexp \<equiv> (append_rexp rexp) ` rhs" |
419 |
419 |
420 definition |
420 definition |
421 "arden_op X rhs \<equiv> |
421 "arden_op X rhs \<equiv> |
422 append_rhs_rexp (rhs - trns_of rhs X) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))" |
422 append_rhs_rexp (rhs - trns_of rhs X) (STAR (\<Uplus> {r. Trn X r \<in> rhs}))" |
423 |
423 |
622 have "finite ({r. Lam r \<in> rhs})" using fin by (rule finite_Lam) |
622 have "finite ({r. Lam r \<in> rhs})" using fin by (rule finite_Lam) |
623 then show ?thesis by auto |
623 then show ?thesis by auto |
624 qed |
624 qed |
625 |
625 |
626 lemma [simp]: |
626 lemma [simp]: |
627 "L (attach_rexp r xb) = L xb ;; L r" |
627 "L (append_rexp r xb) = L xb ;; L r" |
628 apply (cases xb, auto simp: Seq_def) |
628 apply (cases xb, auto simp: Seq_def) |
629 apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI) |
629 apply(rule_tac x = "s\<^isub>1 @ s\<^isub>1'" in exI, rule_tac x = "s\<^isub>2'" in exI) |
630 apply(auto simp: Seq_def) |
630 apply(auto simp: Seq_def) |
631 done |
631 done |
632 |
632 |
633 lemma lang_of_append_rhs: |
633 lemma lang_of_append_rhs: |
634 "L (append_rhs_rexp rhs r) = L rhs ;; L r" |
634 "L (append_rhs_rexp rhs r) = L rhs ;; L r" |
635 apply (auto simp:append_rhs_rexp_def image_def) |
635 apply (auto simp:append_rhs_rexp_def image_def) |
636 apply (auto simp:Seq_def) |
636 apply (auto simp:Seq_def) |
637 apply (rule_tac x = "L xb ;; L r" in exI, auto simp add:Seq_def) |
637 apply (rule_tac x = "L xb ;; L r" in exI, auto simp add:Seq_def) |
638 by (rule_tac x = "attach_rexp r xb" in exI, auto simp:Seq_def) |
638 by (rule_tac x = "append_rexp r xb" in exI, auto simp:Seq_def) |
639 |
639 |
640 lemma classes_of_union_distrib: |
640 lemma classes_of_union_distrib: |
641 "classes_of A \<union> classes_of B = classes_of (A \<union> B)" |
641 "classes_of A \<union> classes_of B = classes_of (A \<union> B)" |
642 by (auto simp add:classes_of_def) |
642 by (auto simp add:classes_of_def) |
643 |
643 |
700 where "Y \<in> UNIV // (\<approx>Lang)" |
700 where "Y \<in> UNIV // (\<approx>Lang)" |
701 and "Y ;; {[c]} \<subseteq> X" |
701 and "Y ;; {[c]} \<subseteq> X" |
702 and "clist \<in> Y" |
702 and "clist \<in> Y" |
703 using decom "(1)" every_eqclass_has_transition by blast |
703 using decom "(1)" every_eqclass_has_transition by blast |
704 hence |
704 hence |
705 "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>(CHAR c)\<Rightarrow> X}" |
705 "x \<in> L {Trn Y (CHAR c)| Y c. Y \<in> UNIV // (\<approx>Lang) \<and> Y \<Turnstile>c\<Rightarrow> X}" |
706 unfolding transition_def |
706 unfolding transition_def |
707 using "(1)" decom |
707 using "(1)" decom |
708 by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def) |
708 by (simp, rule_tac x = "Trn Y (CHAR c)" in exI, simp add:Seq_def) |
709 thus ?thesis using X_in_eqs "(1)" |
709 thus ?thesis using X_in_eqs "(1)" |
710 by (simp add: eqs_def init_rhs_def) |
710 by (simp add: eqs_def init_rhs_def) |