525 It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}. |
525 It will be used later to implement @{text "arden_variate"} and @{text "rhs_subst"}. |
526 *} |
526 *} |
527 |
527 |
528 definition |
528 definition |
529 "rexp_of rhs X \<equiv> \<Uplus> {r. Trn X r \<in> rhs}" |
529 "rexp_of rhs X \<equiv> \<Uplus> {r. Trn X r \<in> rhs}" |
530 |
|
531 text {* |
|
532 The following @{text "lam_of rhs"} returns all pure regular expression trns in @{text "rhs"}. |
|
533 *} |
|
534 |
|
535 definition |
|
536 "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}" |
|
537 |
530 |
538 text {* |
531 text {* |
539 The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"} |
532 The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"} |
540 using @{text "ALT"} to form a single regular expression. |
533 using @{text "ALT"} to form a single regular expression. |
541 When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"} |
534 When all variables inside @{text "rhs"} are eliminated, @{text "rexp_of_lam rhs"} |
1251 shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r") |
1244 shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r") |
1252 proof- |
1245 proof- |
1253 def A \<equiv> "arden_variate X xrhs" |
1246 def A \<equiv> "arden_variate X xrhs" |
1254 have "?P (rexp_of_lam A)" |
1247 have "?P (rexp_of_lam A)" |
1255 proof - |
1248 proof - |
1256 thm lam_of_def |
|
1257 thm rexp_of_lam_def |
|
1258 have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})" |
1249 have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})" |
1259 proof(rule rexp_of_lam_eq_lam_set) |
1250 proof(rule rexp_of_lam_eq_lam_set) |
1260 show "finite A" |
1251 show "finite A" |
1261 unfolding A_def |
1252 unfolding A_def |
1262 using Inv_ES ES_single |
1253 using Inv_ES ES_single |
1263 by (rule_tac arden_variate_keeps_finite) |
1254 by (rule_tac arden_variate_keeps_finite) |
1264 (auto simp add: Inv_def finite_rhs_def) |
1255 (auto simp add: Inv_def finite_rhs_def) |
1265 qed |
1256 qed |
1266 also have "\<dots> = L A" |
1257 also have "\<dots> = L A" |
1267 proof- |
1258 proof- |
1268 have "lam_of A = A" |
1259 have "{Lam r | r. Lam r \<in> A} = A" |
1269 proof- |
1260 proof- |
1270 have "classes_of A = {}" using Inv_ES ES_single |
1261 have "classes_of A = {}" using Inv_ES ES_single |
1271 unfolding A_def |
1262 unfolding A_def |
1272 by (simp add:arden_variate_removes_cl |
1263 by (simp add:arden_variate_removes_cl |
1273 self_contained_def Inv_def lefts_of_def) |
1264 self_contained_def Inv_def lefts_of_def) |
1274 thus ?thesis |
1265 thus ?thesis |
1275 unfolding A_def |
1266 unfolding A_def |
1276 by (auto simp only:lam_of_def classes_of_def, case_tac x, auto) |
1267 by (auto simp only: classes_of_def, case_tac x, auto) |
1277 qed |
1268 qed |
1278 thus ?thesis unfolding lam_of_def by simp |
1269 thus ?thesis by simp |
1279 qed |
1270 qed |
1280 also have "\<dots> = X" |
1271 also have "\<dots> = X" |
1281 unfolding A_def |
1272 unfolding A_def |
1282 proof(rule arden_variate_keeps_eq [THEN sym]) |
1273 proof(rule arden_variate_keeps_eq [THEN sym]) |
1283 show "X = L xrhs" using Inv_ES ES_single |
1274 show "X = L xrhs" using Inv_ES ES_single |