--- a/Myhill_1.thy Tue Feb 08 15:50:26 2011 +0000
+++ b/Myhill_1.thy Tue Feb 08 15:59:47 2011 +0000
@@ -528,13 +528,6 @@
definition
"rexp_of rhs X \<equiv> \<Uplus> {r. Trn X r \<in> rhs}"
-text {*
- The following @{text "lam_of rhs"} returns all pure regular expression trns in @{text "rhs"}.
-*}
-
-definition
- "lam_of rhs \<equiv> {Lam r | r. Lam r \<in> rhs}"
-
text {*
The following @{text "rexp_of_lam rhs"} combines pure regular expression items in @{text "rhs"}
using @{text "ALT"} to form a single regular expression.
@@ -1253,8 +1246,6 @@
def A \<equiv> "arden_variate X xrhs"
have "?P (rexp_of_lam A)"
proof -
- thm lam_of_def
- thm rexp_of_lam_def
have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})"
proof(rule rexp_of_lam_eq_lam_set)
show "finite A"
@@ -1265,7 +1256,7 @@
qed
also have "\<dots> = L A"
proof-
- have "lam_of A = A"
+ have "{Lam r | r. Lam r \<in> A} = A"
proof-
have "classes_of A = {}" using Inv_ES ES_single
unfolding A_def
@@ -1273,9 +1264,9 @@
self_contained_def Inv_def lefts_of_def)
thus ?thesis
unfolding A_def
- by (auto simp only:lam_of_def classes_of_def, case_tac x, auto)
+ by (auto simp only: classes_of_def, case_tac x, auto)
qed
- thus ?thesis unfolding lam_of_def by simp
+ thus ?thesis by simp
qed
also have "\<dots> = X"
unfolding A_def