546 text {* |
551 text {* |
547 @{text "lefts_of ES"} returns all variables defined by an |
552 @{text "lefts_of ES"} returns all variables defined by an |
548 equational system @{text "ES"}. |
553 equational system @{text "ES"}. |
549 *} |
554 *} |
550 definition |
555 definition |
551 "lefts_of ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}" |
556 "lhss ES \<equiv> {Y | Y yrhs. (Y, yrhs) \<in> ES}" |
552 |
557 |
553 text {* |
558 text {* |
554 The following @{text "self_contained ES"} requires that every variable occuring |
559 The following @{text "self_contained ES"} requires that every variable occuring |
555 on the right hand side of equations is already defined by some equation in @{text "ES"}. |
560 on the right hand side of equations is already defined by some equation in @{text "ES"}. |
556 *} |
561 *} |
557 definition |
562 definition |
558 "self_contained ES \<equiv> \<forall>(X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lefts_of ES" |
563 "self_contained ES \<equiv> \<forall>(X, xrhs) \<in> ES. classes_of xrhs \<subseteq> lhss ES" |
559 |
564 |
560 |
565 |
561 text {* |
566 text {* |
562 The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints. |
567 The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints. |
563 *} |
568 *} |
564 definition |
569 definition |
565 "invariant ES \<equiv> valid_eqns ES \<and> finite ES \<and> distinct_equas ES \<and> ardenable ES \<and> |
570 "invariant ES \<equiv> finite ES |
566 finite_rhs ES \<and> self_contained ES" |
571 \<and> finite_rhs ES |
|
572 \<and> valid_eqns ES |
|
573 \<and> distinct_equas ES |
|
574 \<and> ardenable ES |
|
575 \<and> self_contained ES" |
567 |
576 |
568 |
577 |
569 lemma invariantI: |
578 lemma invariantI: |
570 assumes "valid_eqns ES" "finite ES" "distinct_equas ES" "ardenable ES" |
579 assumes "valid_eqns ES" "finite ES" "distinct_equas ES" "ardenable ES" |
571 "finite_rhs ES" "self_contained ES" |
580 "finite_rhs ES" "self_contained ES" |
758 unfolding Init_def by simp |
767 unfolding Init_def by simp |
759 show "distinct_equas (Init (UNIV // \<approx>A))" |
768 show "distinct_equas (Init (UNIV // \<approx>A))" |
760 unfolding distinct_equas_def Init_def by simp |
769 unfolding distinct_equas_def Init_def by simp |
761 show "ardenable (Init (UNIV // \<approx>A))" |
770 show "ardenable (Init (UNIV // \<approx>A))" |
762 unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def |
771 unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def |
763 by auto |
772 by auto |
764 show "finite_rhs (Init (UNIV // \<approx>A))" |
773 show "finite_rhs (Init (UNIV // \<approx>A))" |
765 using finite_Init_rhs[OF finite_CS] |
774 using finite_Init_rhs[OF finite_CS] |
766 unfolding finite_rhs_def Init_def by auto |
775 unfolding finite_rhs_def Init_def by auto |
767 show "self_contained (Init (UNIV // \<approx>A))" |
776 show "self_contained (Init (UNIV // \<approx>A))" |
768 unfolding self_contained_def Init_def Init_rhs_def classes_of_def lefts_of_def |
777 unfolding self_contained_def Init_def Init_rhs_def classes_of_def lhss_def |
769 by auto |
778 by auto |
770 qed |
779 qed |
771 |
780 |
772 subsubsection {* Interation step *} |
781 subsubsection {* Interation step *} |
773 |
782 |
890 lemma Arden_removes_cl: |
899 lemma Arden_removes_cl: |
891 "classes_of (Arden Y yrhs) = classes_of yrhs - {Y}" |
900 "classes_of (Arden Y yrhs) = classes_of yrhs - {Y}" |
892 apply (simp add:Arden_def append_rhs_keeps_cls) |
901 apply (simp add:Arden_def append_rhs_keeps_cls) |
893 by (auto simp:classes_of_def) |
902 by (auto simp:classes_of_def) |
894 |
903 |
895 lemma lefts_of_keeps_cls: |
904 lemma lhss_keeps_cls: |
896 "lefts_of (Subst_all ES Y yrhs) = lefts_of ES" |
905 "lhss (Subst_all ES Y yrhs) = lhss ES" |
897 by (auto simp:lefts_of_def Subst_all_def) |
906 by (auto simp:lhss_def Subst_all_def) |
898 |
907 |
899 lemma Subst_updates_cls: |
908 lemma Subst_updates_cls: |
900 "X \<notin> classes_of xrhs \<Longrightarrow> |
909 "X \<notin> classes_of xrhs \<Longrightarrow> |
901 classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}" |
910 classes_of (Subst rhs X xrhs) = classes_of rhs \<union> classes_of xrhs - {X}" |
902 apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib) |
911 apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib) |
910 { fix X xrhs' |
919 { fix X xrhs' |
911 assume "(X, xrhs') \<in> ?B" |
920 assume "(X, xrhs') \<in> ?B" |
912 then obtain xrhs |
921 then obtain xrhs |
913 where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)" |
922 where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)" |
914 and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast) |
923 and X_in: "(X, xrhs) \<in> ES" by (simp add:Subst_all_def, blast) |
915 have "classes_of xrhs' \<subseteq> lefts_of ?B" |
924 have "classes_of xrhs' \<subseteq> lhss ?B" |
916 proof- |
925 proof- |
917 have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def Subst_all_def) |
926 have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def) |
918 moreover have "classes_of xrhs' \<subseteq> lefts_of ES" |
927 moreover have "classes_of xrhs' \<subseteq> lhss ES" |
919 proof- |
928 proof- |
920 have "classes_of xrhs' \<subseteq> |
929 have "classes_of xrhs' \<subseteq> |
921 classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}" |
930 classes_of xrhs \<union> classes_of (Arden Y yrhs) - {Y}" |
922 proof- |
931 proof- |
923 have "Y \<notin> classes_of (Arden Y yrhs)" |
932 have "Y \<notin> classes_of (Arden Y yrhs)" |
924 using Arden_removes_cl by simp |
933 using Arden_removes_cl by simp |
925 thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls) |
934 thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls) |
926 qed |
935 qed |
927 moreover have "classes_of xrhs \<subseteq> lefts_of ES \<union> {Y}" using X_in sc |
936 moreover have "classes_of xrhs \<subseteq> lhss ES \<union> {Y}" using X_in sc |
928 apply (simp only:self_contained_def lefts_of_union_distrib) |
937 apply (simp only:self_contained_def lhss_union_distrib) |
929 by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def) |
938 by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def) |
930 moreover have "classes_of (Arden Y yrhs) \<subseteq> lefts_of ES \<union> {Y}" |
939 moreover have "classes_of (Arden Y yrhs) \<subseteq> lhss ES \<union> {Y}" |
931 using sc |
940 using sc |
932 by (auto simp add:Arden_removes_cl self_contained_def lefts_of_def) |
941 by (auto simp add:Arden_removes_cl self_contained_def lhss_def) |
933 ultimately show ?thesis by auto |
942 ultimately show ?thesis by auto |
934 qed |
943 qed |
935 ultimately show ?thesis by simp |
944 ultimately show ?thesis by simp |
936 qed |
945 qed |
937 } thus ?thesis by (auto simp only:Subst_all_def self_contained_def) |
946 } thus ?thesis by (auto simp only:Subst_all_def self_contained_def) |
948 have nonempty_yrhs: "rhs_nonempty yrhs" |
957 have nonempty_yrhs: "rhs_nonempty yrhs" |
949 using invariant_ES by (auto simp:invariant_def ardenable_def) |
958 using invariant_ES by (auto simp:invariant_def ardenable_def) |
950 show "valid_eqns (Subst_all ES Y (Arden Y yrhs))" |
959 show "valid_eqns (Subst_all ES Y (Arden Y yrhs))" |
951 proof- |
960 proof- |
952 have "Y = L (Arden Y yrhs)" |
961 have "Y = L (Arden Y yrhs)" |
953 using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs |
962 using Y_eq_yrhs invariant_ES finite_yrhs |
954 by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+) |
963 using finite_Trn[OF finite_yrhs] |
955 thus ?thesis using invariant_ES |
964 apply(rule_tac Arden_keeps_eq) |
956 by (auto simp add:valid_eqns_def |
965 apply(simp_all) |
957 Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def |
966 unfolding invariant_def ardenable_def rhs_nonempty_def |
958 simp del:L_rhs.simps) |
967 apply(auto) |
|
968 done |
|
969 thus ?thesis using invariant_ES |
|
970 unfolding invariant_def finite_rhs_def2 valid_eqns_def Subst_all_def |
|
971 by (auto simp add: Subst_keeps_eq simp del: L_rhs.simps) |
959 qed |
972 qed |
960 show "finite (Subst_all ES Y (Arden Y yrhs))" |
973 show "finite (Subst_all ES Y (Arden Y yrhs))" |
961 using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite) |
974 using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite) |
962 show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" |
975 show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" |
963 using invariant_ES |
976 using invariant_ES |
1013 lemma Subst_all_cls_remains: |
1026 lemma Subst_all_cls_remains: |
1014 "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)" |
1027 "(X, xrhs) \<in> ES \<Longrightarrow> \<exists> xrhs'. (X, xrhs') \<in> (Subst_all ES Y yrhs)" |
1015 by (auto simp: Subst_all_def) |
1028 by (auto simp: Subst_all_def) |
1016 |
1029 |
1017 lemma card_noteq_1_has_more: |
1030 lemma card_noteq_1_has_more: |
1018 assumes card:"card S \<noteq> 1" |
1031 assumes card:"Cond ES" |
1019 and e_in: "e \<in> S" |
1032 and e_in: "(X, xrhs) \<in> ES" |
1020 and finite: "finite S" |
1033 and finite: "finite ES" |
1021 obtains e' where "e' \<in> S \<and> e \<noteq> e'" |
1034 shows "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)" |
1022 proof- |
1035 proof- |
1023 have "card (S - {e}) > 0" |
1036 have "card ES > 1" using card e_in finite |
1024 proof - |
1037 by (cases "card ES") (auto) |
1025 have "card S > 1" using card e_in finite |
1038 then have "card (ES - {(X, xrhs)}) > 0" |
1026 by (cases "card S") (auto) |
1039 using finite e_in by auto |
1027 thus ?thesis using finite e_in by auto |
1040 then have "(ES - {(X, xrhs)}) \<noteq> {}" using finite by (rule_tac notI, simp) |
1028 qed |
1041 then show "\<exists>(Y, yrhs) \<in> ES. (X, xrhs) \<noteq> (Y, yrhs)" |
1029 hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp) |
1042 by auto |
1030 thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto |
1043 qed |
1031 qed |
|
1032 |
|
1033 |
|
1034 |
1044 |
1035 lemma iteration_step_measure: |
1045 lemma iteration_step_measure: |
1036 assumes Inv_ES: "invariant ES" |
1046 assumes Inv_ES: "invariant ES" |
1037 and X_in_ES: "(X, xrhs) \<in> ES" |
1047 and X_in_ES: "(X, xrhs) \<in> ES" |
1038 and not_T: "card ES \<noteq> 1" |
1048 and not_T: "Cond ES " |
1039 shows "(Iter X ES, ES) \<in> measure card" |
1049 shows "(Iter X ES, ES) \<in> measure card" |
1040 proof - |
1050 proof - |
1041 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1051 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1042 then obtain Y yrhs |
1052 then obtain Y yrhs |
1043 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1053 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1044 using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1054 using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1045 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
1055 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
1046 using X_in_ES Inv_ES |
1056 using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def |
1047 by (auto simp: invariant_def distinct_equas_def) |
1057 by auto |
1048 then show "(Iter X ES, ES) \<in> measure card" |
1058 then show "(Iter X ES, ES) \<in> measure card" |
1049 apply(rule IterI2) |
1059 apply(rule IterI2) |
1050 apply(rule Remove_in_card_measure) |
1060 apply(rule Remove_in_card_measure) |
1051 apply(simp_all add: finite_ES) |
1061 apply(simp_all add: finite_ES) |
1052 done |
1062 done |
1053 qed |
1063 qed |
1054 |
1064 |
1055 lemma iteration_step_invariant: |
1065 lemma iteration_step_invariant: |
1056 assumes Inv_ES: "invariant ES" |
1066 assumes Inv_ES: "invariant ES" |
1057 and X_in_ES: "(X, xrhs) \<in> ES" |
1067 and X_in_ES: "(X, xrhs) \<in> ES" |
1058 and not_T: "card ES \<noteq> 1" |
1068 and not_T: "Cond ES" |
1059 shows "invariant (Iter X ES)" |
1069 shows "invariant (Iter X ES)" |
1060 proof - |
1070 proof - |
1061 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1071 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1062 then obtain Y yrhs |
1072 then obtain Y yrhs |
1063 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1073 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1064 using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1074 using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1065 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
1075 then have "(Y, yrhs) \<in> ES" "X \<noteq> Y" |
1066 using X_in_ES Inv_ES |
1076 using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def |
1067 by (auto simp: invariant_def distinct_equas_def) |
1077 by auto |
1068 then show "invariant (Iter X ES)" |
1078 then show "invariant (Iter X ES)" |
1069 proof(rule IterI2) |
1079 proof(rule IterI2) |
1070 fix Y yrhs |
1080 fix Y yrhs |
1071 assume h: "(Y, yrhs) \<in> ES" "X \<noteq> Y" |
1081 assume h: "(Y, yrhs) \<in> ES" "X \<noteq> Y" |
1072 then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto |
1082 then have "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto |
1076 qed |
1086 qed |
1077 |
1087 |
1078 lemma iteration_step_ex: |
1088 lemma iteration_step_ex: |
1079 assumes Inv_ES: "invariant ES" |
1089 assumes Inv_ES: "invariant ES" |
1080 and X_in_ES: "(X, xrhs) \<in> ES" |
1090 and X_in_ES: "(X, xrhs) \<in> ES" |
1081 and not_T: "card ES \<noteq> 1" |
1091 and not_T: "Cond ES" |
1082 shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" |
1092 shows "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" |
1083 proof - |
1093 proof - |
1084 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1094 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1085 then obtain Y yrhs |
1095 then obtain Y yrhs |
1086 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1096 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1087 using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1097 using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) |
1088 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
1098 then have "(Y, yrhs) \<in> ES " "X \<noteq> Y" |
1089 using X_in_ES Inv_ES |
1099 using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def |
1090 by (auto simp: invariant_def distinct_equas_def) |
1100 by auto |
1091 then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" |
1101 then show "\<exists>xrhs'. (X, xrhs') \<in> (Iter X ES)" |
1092 apply(rule IterI2) |
1102 apply(rule IterI2) |
1093 unfolding Remove_def |
1103 unfolding Remove_def |
1094 apply(rule Subst_all_cls_remains) |
1104 apply(rule Subst_all_cls_remains) |
1095 using X_in_ES |
1105 using X_in_ES |
1098 qed |
1108 qed |
1099 |
1109 |
1100 |
1110 |
1101 subsubsection {* Conclusion of the proof *} |
1111 subsubsection {* Conclusion of the proof *} |
1102 |
1112 |
1103 text {* |
1113 lemma Solve: |
1104 From this point until @{text "hard_direction"}, the hard direction is proved |
1114 assumes fin: "finite (UNIV // \<approx>A)" |
1105 through a simple application of the iteration principle. |
1115 and X_in: "X \<in> (UNIV // \<approx>A)" |
1106 *} |
1116 shows "\<exists>xrhs. Solve X (Init (UNIV // \<approx>A)) = {(X, xrhs)} \<and> invariant {(X, xrhs)}" |
1107 |
1117 proof - |
1108 |
1118 def Inv \<equiv> "\<lambda>ES. invariant ES \<and> (\<exists>xrhs. (X, xrhs) \<in> ES)" |
1109 lemma reduce_x: |
1119 have "Inv (Init (UNIV // \<approx>A))" unfolding Inv_def |
1110 assumes inv: "invariant ES" |
1120 using fin X_in by (simp add: Init_ES_satisfies_invariant, simp add: Init_def) |
1111 and contain_x: "(X, xrhs) \<in> ES" |
1121 moreover |
1112 shows "\<exists> xrhs'. Solve X ES = {(X, xrhs')} \<and> invariant(Solve X ES)" |
1122 { fix ES |
1113 proof - |
1123 assume inv: "Inv ES" and crd: "Cond ES" |
1114 let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))" |
1124 then have "Inv (Iter X ES)" |
1115 show ?thesis unfolding Solve_def |
1125 unfolding Inv_def |
1116 proof (rule while_rule [where P = ?Inv and r = "measure card"]) |
1126 by (auto simp add: iteration_step_invariant iteration_step_ex) } |
1117 from inv and contain_x show "?Inv ES" by auto |
1127 moreover |
1118 next |
1128 { fix ES |
1119 show "wf (measure card)" by simp |
1129 assume "Inv ES" and "\<not> Cond ES" |
1120 next |
1130 then have "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES" |
1121 fix ES |
1131 unfolding Inv_def invariant_def |
1122 assume inv: "?Inv ES" and crd: "card ES \<noteq> 1" |
1132 apply (auto, rule_tac x = xrhs in exI) |
1123 then show "(Iter X ES, ES) \<in> measure card" |
1133 apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff) |
|
1134 done |
|
1135 then have "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant {(X, xrhs')}" |
|
1136 by auto } |
|
1137 moreover |
|
1138 have "wf (measure card)" by simp |
|
1139 moreover |
|
1140 { fix ES |
|
1141 assume inv: "Inv ES" and crd: "Cond ES" |
|
1142 then have "(Iter X ES, ES) \<in> measure card" |
|
1143 unfolding Inv_def |
1124 apply(clarify) |
1144 apply(clarify) |
1125 apply(rule iteration_step_measure) |
1145 apply(rule_tac iteration_step_measure) |
1126 apply(auto) |
1146 apply(auto) |
1127 done |
1147 done } |
1128 next |
1148 ultimately |
1129 fix ES |
1149 show "\<exists>xrhs. Solve X (Init (UNIV // \<approx>A)) = {(X, xrhs)} \<and> invariant {(X, xrhs)}" |
1130 assume inv: "?Inv ES" and crd: "card ES \<noteq> 1" |
1150 unfolding Solve_def by (rule while_rule) |
1131 then show "?Inv (Iter X ES)" |
|
1132 apply - |
|
1133 apply(auto) |
|
1134 apply(rule iteration_step_invariant) |
|
1135 apply(auto) |
|
1136 apply(rule iteration_step_ex) |
|
1137 apply(auto) |
|
1138 done |
|
1139 next |
|
1140 fix ES |
|
1141 assume "?Inv ES" and "\<not> card ES \<noteq> 1" |
|
1142 thus "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES" |
|
1143 apply (auto, rule_tac x = xrhs in exI) |
|
1144 by (auto simp: invariant_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) |
|
1145 qed |
|
1146 qed |
1151 qed |
1147 |
1152 |
1148 lemma last_cl_exists_rexp: |
1153 lemma last_cl_exists_rexp: |
1149 assumes Inv_ES: "invariant {(X, xrhs)}" |
1154 assumes Inv_ES: "invariant {(X, xrhs)}" |
1150 shows "\<exists>r::rexp. L r = X" |
1155 shows "\<exists>r::rexp. L r = X" |
1151 proof- |
1156 proof- |
1152 def A \<equiv> "Arden X xrhs" |
1157 def A \<equiv> "Arden X xrhs" |
1153 have eq: "{Lam r | r. Lam r \<in> A} = A" |
1158 have eq: "{Lam r | r. Lam r \<in> A} = A" |
1154 proof - |
1159 proof - |
1155 have "classes_of A = {}" using Inv_ES |
1160 have "classes_of A = {}" using Inv_ES |
1156 unfolding A_def self_contained_def invariant_def lefts_of_def |
1161 unfolding A_def self_contained_def invariant_def lhss_def |
1157 by (simp add: Arden_removes_cl) |
1162 by (simp add: Arden_removes_cl) |
1158 thus ?thesis unfolding A_def classes_of_def |
1163 thus ?thesis unfolding A_def classes_of_def |
1159 apply(auto simp only:) |
1164 apply(auto simp only:) |
1160 apply(case_tac x) |
1165 apply(case_tac x) |
1161 apply(auto) |
1166 apply(auto) |
1188 lemma every_eqcl_has_reg: |
1193 lemma every_eqcl_has_reg: |
1189 assumes finite_CS: "finite (UNIV // \<approx>A)" |
1194 assumes finite_CS: "finite (UNIV // \<approx>A)" |
1190 and X_in_CS: "X \<in> (UNIV // \<approx>A)" |
1195 and X_in_CS: "X \<in> (UNIV // \<approx>A)" |
1191 shows "\<exists>r::rexp. L r = X" |
1196 shows "\<exists>r::rexp. L r = X" |
1192 proof - |
1197 proof - |
1193 def ES \<equiv> "Init (UNIV // \<approx>A)" |
1198 from finite_CS X_in_CS |
1194 have "invariant ES" using finite_CS unfolding ES_def |
1199 obtain xrhs where "invariant {(X, xrhs)}" |
1195 by (rule Init_ES_satisfies_invariant) |
1200 using Solve by metis |
1196 moreover |
|
1197 from X_in_CS obtain xrhs where "(X, xrhs) \<in> ES" unfolding ES_def |
|
1198 unfolding Init_def Init_rhs_def by auto |
|
1199 ultimately |
|
1200 obtain xrhs' where "Solve X ES = {(X, xrhs')}" "invariant (Solve X ES)" |
|
1201 using reduce_x by blast |
|
1202 then show "\<exists>r::rexp. L r = X" |
1201 then show "\<exists>r::rexp. L r = X" |
1203 using last_cl_exists_rexp by auto |
1202 using last_cl_exists_rexp by auto |
1204 qed |
1203 qed |
1205 |
|
1206 |
1204 |
1207 lemma bchoice_finite_set: |
1205 lemma bchoice_finite_set: |
1208 assumes a: "\<forall>x \<in> S. \<exists>y. x = f y" |
1206 assumes a: "\<forall>x \<in> S. \<exists>y. x = f y" |
1209 and b: "finite S" |
1207 and b: "finite S" |
1210 shows "\<exists>ys. (\<Union> S) = \<Union>(f ` ys) \<and> finite ys" |
1208 shows "\<exists>ys. (\<Union> S) = \<Union>(f ` ys) \<and> finite ys" |