equal
deleted
inserted
replaced
1146 ultimately |
1146 ultimately |
1147 show "\<exists>rhs. Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)} \<and> invariant {(X, rhs)}" |
1147 show "\<exists>rhs. Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)} \<and> invariant {(X, rhs)}" |
1148 unfolding Solve_def by (rule while_rule) |
1148 unfolding Solve_def by (rule while_rule) |
1149 qed |
1149 qed |
1150 |
1150 |
1151 lemma last_cl_exists_rexp: |
1151 lemma every_eqcl_has_reg: |
1152 assumes Inv_ES: "invariant {(X, xrhs)}" |
1152 assumes finite_CS: "finite (UNIV // \<approx>A)" |
1153 shows "\<exists>r::rexp. L r = X" |
1153 and X_in_CS: "X \<in> (UNIV // \<approx>A)" |
1154 proof- |
1154 shows "\<exists>r::rexp. X = L r" |
|
1155 proof - |
|
1156 from finite_CS X_in_CS |
|
1157 obtain xrhs where Inv_ES: "invariant {(X, xrhs)}" |
|
1158 using Solve by metis |
|
1159 |
1155 def A \<equiv> "Arden X xrhs" |
1160 def A \<equiv> "Arden X xrhs" |
1156 have "rhss xrhs \<subseteq> {X}" using Inv_ES |
1161 have "rhss xrhs \<subseteq> {X}" using Inv_ES |
1157 unfolding valid_eqs_def invariant_def rhss_def lhss_def |
1162 unfolding valid_eqs_def invariant_def rhss_def lhss_def |
1158 by auto |
1163 by auto |
1159 then have "rhss A = {}" unfolding A_def |
1164 then have "rhss A = {}" unfolding A_def |
1170 then have "X = L A" using Inv_ES |
1175 then have "X = L A" using Inv_ES |
1171 unfolding A_def invariant_def ardenable_def finite_rhs_def rhs_nonempty_def |
1176 unfolding A_def invariant_def ardenable_def finite_rhs_def rhs_nonempty_def |
1172 by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn) |
1177 by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn) |
1173 then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp |
1178 then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp |
1174 then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto |
1179 then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto |
1175 then show "\<exists>r::rexp. L r = X" by blast |
1180 then show "\<exists>r::rexp. X = L r" by blast |
1176 qed |
|
1177 |
|
1178 lemma every_eqcl_has_reg: |
|
1179 assumes finite_CS: "finite (UNIV // \<approx>A)" |
|
1180 and X_in_CS: "X \<in> (UNIV // \<approx>A)" |
|
1181 shows "\<exists>r::rexp. L r = X" |
|
1182 proof - |
|
1183 from finite_CS X_in_CS |
|
1184 obtain xrhs where "invariant {(X, xrhs)}" |
|
1185 using Solve by metis |
|
1186 then show "\<exists>r::rexp. L r = X" |
|
1187 using last_cl_exists_rexp by auto |
|
1188 qed |
1181 qed |
1189 |
1182 |
1190 lemma bchoice_finite_set: |
1183 lemma bchoice_finite_set: |
1191 assumes a: "\<forall>x \<in> S. \<exists>y. x = f y" |
1184 assumes a: "\<forall>x \<in> S. \<exists>y. x = f y" |
1192 and b: "finite S" |
1185 and b: "finite S" |