510 |
510 |
511 definition |
511 definition |
512 "sound_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs" |
512 "sound_eqs ES \<equiv> \<forall>(X, rhs) \<in> ES. X = L rhs" |
513 |
513 |
514 text {* |
514 text {* |
515 @{text "rhs_nonempty rhs"} requires regular expressions occuring in |
515 @{text "ardenable rhs"} requires regular expressions occuring in |
516 transitional items of @{text "rhs"} do not contain empty string. This is |
516 transitional items of @{text "rhs"} do not contain empty string. This is |
517 necessary for the application of Arden's transformation to @{text "rhs"}. |
517 necessary for the application of Arden's transformation to @{text "rhs"}. |
518 *} |
518 *} |
519 |
519 |
520 definition |
520 definition |
521 "rhs_nonempty rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)" |
521 "ardenable rhs \<equiv> (\<forall> Y r. Trn Y r \<in> rhs \<longrightarrow> [] \<notin> L r)" |
522 |
522 |
523 text {* |
523 text {* |
524 The following @{text "ardenable ES"} requires that Arden's transformation |
524 The following @{text "ardenable_all ES"} requires that Arden's transformation |
525 is applicable to every equation of equational system @{text "ES"}. |
525 is applicable to every equation of equational system @{text "ES"}. |
526 *} |
526 *} |
527 |
527 |
528 definition |
528 definition |
529 "ardenable ES \<equiv> \<forall>(X, rhs) \<in> ES. rhs_nonempty rhs" |
529 "ardenable_all ES \<equiv> \<forall>(X, rhs) \<in> ES. ardenable rhs" |
530 |
530 |
531 |
531 |
532 text {* |
532 text {* |
533 @{text "finite_rhs ES"} requires every equation in @{text "rhs"} |
533 @{text "finite_rhs ES"} requires every equation in @{text "rhs"} |
534 be finite. |
534 be finite. |
763 using l_eq_r_in_eqs by auto |
763 using l_eq_r_in_eqs by auto |
764 show "finite (Init (UNIV // \<approx>A))" using finite_CS |
764 show "finite (Init (UNIV // \<approx>A))" using finite_CS |
765 unfolding Init_def by simp |
765 unfolding Init_def by simp |
766 show "distinct_equas (Init (UNIV // \<approx>A))" |
766 show "distinct_equas (Init (UNIV // \<approx>A))" |
767 unfolding distinct_equas_def Init_def by simp |
767 unfolding distinct_equas_def Init_def by simp |
768 show "ardenable (Init (UNIV // \<approx>A))" |
768 show "ardenable_all (Init (UNIV // \<approx>A))" |
769 unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def |
769 unfolding ardenable_all_def Init_def Init_rhs_def ardenable_def |
770 by auto |
770 by auto |
771 show "finite_rhs (Init (UNIV // \<approx>A))" |
771 show "finite_rhs (Init (UNIV // \<approx>A))" |
772 using finite_Init_rhs[OF finite_CS] |
772 using finite_Init_rhs[OF finite_CS] |
773 unfolding finite_rhs_def Init_def by auto |
773 unfolding finite_rhs_def Init_def by auto |
774 show "valid_eqs (Init (UNIV // \<approx>A))" |
774 show "valid_eqs (Init (UNIV // \<approx>A))" |
783 the correctness of the iteration step @{text "Iter X ES"} is proved. |
783 the correctness of the iteration step @{text "Iter X ES"} is proved. |
784 *} |
784 *} |
785 |
785 |
786 lemma Arden_keeps_eq: |
786 lemma Arden_keeps_eq: |
787 assumes l_eq_r: "X = L rhs" |
787 assumes l_eq_r: "X = L rhs" |
788 and not_empty: "[] \<notin> L (\<Uplus>{r. Trn X r \<in> rhs})" |
788 and not_empty: "ardenable rhs" |
789 and finite: "finite rhs" |
789 and finite: "finite rhs" |
790 shows "X = L (Arden X rhs)" |
790 shows "X = L (Arden X rhs)" |
791 proof - |
791 proof - |
792 def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})" |
792 def A \<equiv> "L (\<Uplus>{r. Trn X r \<in> rhs})" |
793 def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}" |
793 def b \<equiv> "rhs - {Trn X r | r. Trn X r \<in> rhs}" |
797 have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def) |
797 have "L rhs = L({Trn X r | r. Trn X r \<in> rhs} \<union> b)" by (auto simp: b_def) |
798 also have "\<dots> = X ;; A \<union> B" |
798 also have "\<dots> = X ;; A \<union> B" |
799 unfolding L_rhs_union_distrib[symmetric] |
799 unfolding L_rhs_union_distrib[symmetric] |
800 by (simp only: lang_of_rexp_of finite B_def A_def) |
800 by (simp only: lang_of_rexp_of finite B_def A_def) |
801 finally show ?thesis |
801 finally show ?thesis |
802 using l_eq_r not_empty |
|
803 apply(rule_tac arden[THEN iffD1]) |
802 apply(rule_tac arden[THEN iffD1]) |
804 apply(simp add: A_def) |
803 apply(simp (no_asm) add: A_def) |
|
804 using finite_Trn[OF finite] not_empty |
|
805 apply(simp add: ardenable_def) |
|
806 using l_eq_r |
805 apply(simp) |
807 apply(simp) |
806 done |
808 done |
807 qed |
809 qed |
808 moreover have "L (Arden X rhs) = B ;; A\<star>" |
810 moreover have "L (Arden X rhs) = B ;; A\<star>" |
809 by (simp only:Arden_def L_rhs_union_distrib lang_of_append_rhs |
811 by (simp only:Arden_def L_rhs_union_distrib lang_of_append_rhs |
818 lemma Arden_keeps_finite: |
820 lemma Arden_keeps_finite: |
819 "finite rhs \<Longrightarrow> finite (Arden X rhs)" |
821 "finite rhs \<Longrightarrow> finite (Arden X rhs)" |
820 by (auto simp:Arden_def append_keeps_finite) |
822 by (auto simp:Arden_def append_keeps_finite) |
821 |
823 |
822 lemma append_keeps_nonempty: |
824 lemma append_keeps_nonempty: |
823 "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (append_rhs_rexp rhs r)" |
825 "ardenable rhs \<Longrightarrow> ardenable (append_rhs_rexp rhs r)" |
824 apply (auto simp:rhs_nonempty_def append_rhs_rexp_def) |
826 apply (auto simp:ardenable_def append_rhs_rexp_def) |
825 by (case_tac x, auto simp:Seq_def) |
827 by (case_tac x, auto simp:Seq_def) |
826 |
828 |
827 lemma nonempty_set_sub: |
829 lemma nonempty_set_sub: |
828 "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (rhs - A)" |
830 "ardenable rhs \<Longrightarrow> ardenable (rhs - A)" |
829 by (auto simp:rhs_nonempty_def) |
831 by (auto simp:ardenable_def) |
830 |
832 |
831 lemma nonempty_set_union: |
833 lemma nonempty_set_union: |
832 "\<lbrakk>rhs_nonempty rhs; rhs_nonempty rhs'\<rbrakk> \<Longrightarrow> rhs_nonempty (rhs \<union> rhs')" |
834 "\<lbrakk>ardenable rhs; ardenable rhs'\<rbrakk> \<Longrightarrow> ardenable (rhs \<union> rhs')" |
833 by (auto simp:rhs_nonempty_def) |
835 by (auto simp:ardenable_def) |
834 |
836 |
835 lemma Arden_keeps_nonempty: |
837 lemma Arden_keeps_nonempty: |
836 "rhs_nonempty rhs \<Longrightarrow> rhs_nonempty (Arden X rhs)" |
838 "ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)" |
837 by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub) |
839 by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub) |
838 |
840 |
839 |
841 |
840 lemma Subst_keeps_nonempty: |
842 lemma Subst_keeps_nonempty: |
841 "\<lbrakk>rhs_nonempty rhs; rhs_nonempty xrhs\<rbrakk> \<Longrightarrow> rhs_nonempty (Subst rhs X xrhs)" |
843 "\<lbrakk>ardenable rhs; ardenable xrhs\<rbrakk> \<Longrightarrow> ardenable (Subst rhs X xrhs)" |
842 by (simp only:Subst_def append_keeps_nonempty nonempty_set_union nonempty_set_sub) |
844 by (simp only:Subst_def append_keeps_nonempty nonempty_set_union nonempty_set_sub) |
843 |
845 |
844 lemma Subst_keeps_eq: |
846 lemma Subst_keeps_eq: |
845 assumes substor: "X = L xrhs" |
847 assumes substor: "X = L xrhs" |
846 and finite: "finite rhs" |
848 and finite: "finite rhs" |
867 lemma Subst_keeps_finite_rhs: |
869 lemma Subst_keeps_finite_rhs: |
868 "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)" |
870 "\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)" |
869 by (auto simp:Subst_def append_keeps_finite) |
871 by (auto simp:Subst_def append_keeps_finite) |
870 |
872 |
871 lemma Subst_all_keeps_finite: |
873 lemma Subst_all_keeps_finite: |
872 assumes finite:"finite (ES:: (string set \<times> rhs_item set) set)" |
874 assumes finite: "finite ES" |
873 shows "finite (Subst_all ES Y yrhs)" |
875 shows "finite (Subst_all ES Y yrhs)" |
874 proof - |
876 proof - |
875 have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \<in> ES}" |
877 def eqns \<equiv> "{(X::lang, rhs) |X rhs. (X, rhs) \<in> ES}" |
876 (is "finite ?A") |
878 def h \<equiv> "\<lambda>(X::lang, rhs). (X, Subst rhs Y yrhs)" |
877 proof- |
879 have "finite (h ` eqns)" using finite h_def eqns_def by auto |
878 def eqns' \<equiv> "{(Ya::lang, yrhsa) | Ya yrhsa. (Ya, yrhsa) \<in> ES}" |
880 moreover |
879 def h \<equiv> "\<lambda>(Ya::lang, yrhsa). (Ya, Subst yrhsa Y yrhs)" |
881 have "Subst_all ES Y yrhs = h ` eqns" unfolding h_def eqns_def Subst_all_def by auto |
880 have "finite (h ` eqns')" using finite h_def eqns'_def by auto |
882 ultimately |
881 moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def) |
883 show "finite (Subst_all ES Y yrhs)" by simp |
882 ultimately show ?thesis by auto |
|
883 qed |
|
884 thus ?thesis by (simp add:Subst_all_def) |
|
885 qed |
884 qed |
886 |
885 |
887 lemma Subst_all_keeps_finite_rhs: |
886 lemma Subst_all_keeps_finite_rhs: |
888 "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)" |
887 "\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)" |
889 by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def) |
888 by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def) |
908 rhss (Subst rhs X xrhs) = rhss rhs \<union> rhss xrhs - {X}" |
907 rhss (Subst rhs X xrhs) = rhss rhs \<union> rhss xrhs - {X}" |
909 apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib) |
908 apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib) |
910 by (auto simp:rhss_def) |
909 by (auto simp:rhss_def) |
911 |
910 |
912 lemma Subst_all_keeps_valid_eqs: |
911 lemma Subst_all_keeps_valid_eqs: |
913 assumes sc: "valid_eqs (ES \<union> {(Y, yrhs)})" (is "valid_eqs ?A") |
912 assumes sc: "valid_eqs (ES \<union> {(Y, yrhs)})" (is "valid_eqs ?A") |
914 shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))" |
913 shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))" (is "valid_eqs ?B") |
915 (is "valid_eqs ?B") |
914 proof - |
916 proof- |
|
917 { fix X xrhs' |
915 { fix X xrhs' |
918 assume "(X, xrhs') \<in> ?B" |
916 assume "(X, xrhs') \<in> ?B" |
919 then obtain xrhs |
917 then obtain xrhs |
920 where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)" |
918 where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)" |
921 and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast) |
919 and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast) |
922 have "rhss xrhs' \<subseteq> lhss ?B" |
920 have "rhss xrhs' \<subseteq> lhss ?B" |
923 proof- |
921 proof- |
924 have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def) |
922 have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def) |
925 moreover have "rhss xrhs' \<subseteq> lhss ES" |
923 moreover have "rhss xrhs' \<subseteq> lhss ES" |
926 proof- |
924 proof- |
927 have "rhss xrhs' \<subseteq> |
925 have "rhss xrhs' \<subseteq> rhss xrhs \<union> rhss (Arden Y yrhs) - {Y}" |
928 rhss xrhs \<union> rhss (Arden Y yrhs) - {Y}" |
|
929 proof- |
926 proof- |
930 have "Y \<notin> rhss (Arden Y yrhs)" |
927 have "Y \<notin> rhss (Arden Y yrhs)" |
931 using Arden_removes_cl by simp |
928 using Arden_removes_cl by simp |
932 thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls) |
929 thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls) |
933 qed |
930 qed |
950 proof (rule invariantI) |
947 proof (rule invariantI) |
951 have Y_eq_yrhs: "Y = L yrhs" |
948 have Y_eq_yrhs: "Y = L yrhs" |
952 using invariant_ES by (simp only:invariant_def sound_eqs_def, blast) |
949 using invariant_ES by (simp only:invariant_def sound_eqs_def, blast) |
953 have finite_yrhs: "finite yrhs" |
950 have finite_yrhs: "finite yrhs" |
954 using invariant_ES by (auto simp:invariant_def finite_rhs_def) |
951 using invariant_ES by (auto simp:invariant_def finite_rhs_def) |
955 have nonempty_yrhs: "rhs_nonempty yrhs" |
952 have nonempty_yrhs: "ardenable yrhs" |
956 using invariant_ES by (auto simp:invariant_def ardenable_def) |
953 using invariant_ES by (auto simp:invariant_def ardenable_all_def) |
957 show "sound_eqs (Subst_all ES Y (Arden Y yrhs))" |
954 show "sound_eqs (Subst_all ES Y (Arden Y yrhs))" |
958 proof- |
955 proof - |
959 have "Y = L (Arden Y yrhs)" |
956 have "Y = L (Arden Y yrhs)" |
960 using Y_eq_yrhs invariant_ES finite_yrhs |
957 using Y_eq_yrhs invariant_ES finite_yrhs |
961 using finite_Trn[OF finite_yrhs] |
958 using finite_Trn[OF finite_yrhs] |
962 apply(rule_tac Arden_keeps_eq) |
959 apply(rule_tac Arden_keeps_eq) |
963 apply(simp_all) |
960 apply(simp_all) |
964 unfolding invariant_def ardenable_def rhs_nonempty_def |
961 unfolding invariant_def ardenable_all_def ardenable_def |
965 apply(auto) |
962 apply(auto) |
966 done |
963 done |
967 thus ?thesis using invariant_ES |
964 thus ?thesis using invariant_ES |
968 unfolding invariant_def finite_rhs_def2 sound_eqs_def Subst_all_def |
965 unfolding invariant_def finite_rhs_def2 sound_eqs_def Subst_all_def |
969 by (auto simp add: Subst_keeps_eq simp del: L_rhs.simps) |
966 by (auto simp add: Subst_keeps_eq simp del: L_rhs.simps) |
970 qed |
967 qed |
971 show "finite (Subst_all ES Y (Arden Y yrhs))" |
968 show "finite (Subst_all ES Y (Arden Y yrhs))" |
972 using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite) |
969 using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite) |
973 show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" |
970 show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" |
974 using invariant_ES |
971 using invariant_ES |
975 by (auto simp:distinct_equas_def Subst_all_def invariant_def) |
972 unfolding distinct_equas_def Subst_all_def invariant_def by auto |
976 show "ardenable (Subst_all ES Y (Arden Y yrhs))" |
973 show "ardenable_all (Subst_all ES Y (Arden Y yrhs))" |
977 proof - |
974 proof - |
978 { fix X rhs |
975 { fix X rhs |
979 assume "(X, rhs) \<in> ES" |
976 assume "(X, rhs) \<in> ES" |
980 hence "rhs_nonempty rhs" using prems invariant_ES |
977 hence "ardenable rhs" using prems invariant_ES |
981 by (auto simp add:invariant_def ardenable_def) |
978 by (auto simp add:invariant_def ardenable_all_def) |
982 with nonempty_yrhs |
979 with nonempty_yrhs |
983 have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))" |
980 have "ardenable (Subst rhs Y (Arden Y yrhs))" |
984 by (simp add:nonempty_yrhs |
981 by (simp add:nonempty_yrhs |
985 Subst_keeps_nonempty Arden_keeps_nonempty) |
982 Subst_keeps_nonempty Arden_keeps_nonempty) |
986 } thus ?thesis by (auto simp add:ardenable_def Subst_all_def) |
983 } thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def) |
987 qed |
984 qed |
988 show "finite_rhs (Subst_all ES Y (Arden Y yrhs))" |
985 show "finite_rhs (Subst_all ES Y (Arden Y yrhs))" |
989 proof- |
986 proof- |
990 have "finite_rhs ES" using invariant_ES |
987 have "finite_rhs ES" using invariant_ES |
991 by (simp add:invariant_def finite_rhs_def) |
988 by (simp add:invariant_def finite_rhs_def) |
1077 proof(rule IterI2) |
1074 proof(rule IterI2) |
1078 fix Y yrhs |
1075 fix Y yrhs |
1079 assume h: "(Y, yrhs) \<in> ES" "X \<noteq> Y" |
1076 assume h: "(Y, yrhs) \<in> ES" "X \<noteq> Y" |
1080 then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto |
1077 then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto |
1081 then show "invariant (Remove ES Y yrhs)" unfolding Remove_def |
1078 then show "invariant (Remove ES Y yrhs)" unfolding Remove_def |
1082 using Inv_ES by (rule_tac Subst_all_satisfies_invariant) (simp) |
1079 using Inv_ES |
|
1080 thm Subst_all_satisfies_invariant |
|
1081 by (rule_tac Subst_all_satisfies_invariant) (simp) |
1083 qed |
1082 qed |
1084 qed |
1083 qed |
1085 |
1084 |
1086 lemma iteration_step_ex: |
1085 lemma iteration_step_ex: |
1087 assumes Inv_ES: "invariant ES" |
1086 assumes Inv_ES: "invariant ES" |
1122 then have "Inv (Iter X ES)" |
1121 then have "Inv (Iter X ES)" |
1123 unfolding Inv_def |
1122 unfolding Inv_def |
1124 by (auto simp add: iteration_step_invariant iteration_step_ex) } |
1123 by (auto simp add: iteration_step_invariant iteration_step_ex) } |
1125 moreover |
1124 moreover |
1126 { fix ES |
1125 { fix ES |
1127 assume "Inv ES" and "\<not> Cond ES" |
1126 assume inv: "Inv ES" and not_crd: "\<not>Cond ES" |
1128 then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant ES" |
1127 from inv obtain rhs where "(X, rhs) \<in> ES" unfolding Inv_def by auto |
1129 unfolding Inv_def invariant_def |
1128 moreover |
1130 apply (auto, rule_tac x = rhs in exI) |
1129 from not_crd have "card ES = 1" by simp |
1131 apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff) |
1130 ultimately |
1132 done |
1131 have "ES = {(X, rhs)}" by (auto simp add: card_Suc_eq) |
1133 then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant {(X, rhs')}" |
1132 then have "\<exists>rhs'. ES = {(X, rhs')} \<and> invariant {(X, rhs')}" using inv |
1134 by auto } |
1133 unfolding Inv_def by auto } |
1135 moreover |
1134 moreover |
1136 have "wf (measure card)" by simp |
1135 have "wf (measure card)" by simp |
1137 moreover |
1136 moreover |
1138 { fix ES |
1137 { fix ES |
1139 assume inv: "Inv ES" and crd: "Cond ES" |
1138 assume inv: "Inv ES" and crd: "Cond ES" |
1171 then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam) |
1170 then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam) |
1172 |
1171 |
1173 have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def |
1172 have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def |
1174 by simp |
1173 by simp |
1175 then have "X = L A" using Inv_ES |
1174 then have "X = L A" using Inv_ES |
1176 unfolding A_def invariant_def ardenable_def finite_rhs_def rhs_nonempty_def |
1175 unfolding A_def invariant_def ardenable_all_def finite_rhs_def |
1177 by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn) |
1176 by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn) |
1178 then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp |
1177 then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp |
1179 then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto |
1178 then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto |
1180 then show "\<exists>r::rexp. X = L r" by blast |
1179 then show "\<exists>r::rexp. X = L r" by blast |
1181 qed |
1180 qed |