diff -r f460d5f75cb5 -r 5bd73aa805a7 Myhill_1.thy --- a/Myhill_1.thy Mon Feb 14 23:10:44 2011 +0000 +++ b/Myhill_1.thy Tue Feb 15 08:08:04 2011 +0000 @@ -509,7 +509,7 @@ *} definition - "valid_eqns ES \ \(X, rhs) \ ES. X = L rhs" + "sound_eqs ES \ \(X, rhs) \ ES. X = L rhs" text {* @{text "rhs_nonempty rhs"} requires regular expressions occuring in @@ -546,7 +546,7 @@ *} definition - "classes_of rhs \ {X | X r. Trn X r \ rhs}" + "rhss rhs \ {X | X r. Trn X r \ rhs}" text {* @{text "lefts_of ES"} returns all variables defined by an @@ -556,11 +556,11 @@ "lhss ES \ {Y | Y yrhs. (Y, yrhs) \ ES}" text {* - The following @{text "self_contained ES"} requires that every variable occuring + The following @{text "valid_eqs ES"} requires that every variable occuring on the right hand side of equations is already defined by some equation in @{text "ES"}. *} definition - "self_contained ES \ \(X, xrhs) \ ES. classes_of xrhs \ lhss ES" + "valid_eqs ES \ \(X, rhs) \ ES. rhss rhs \ lhss ES" text {* @@ -569,15 +569,15 @@ definition "invariant ES \ finite ES \ finite_rhs ES - \ valid_eqns ES + \ sound_eqs ES \ distinct_equas ES \ ardenable ES - \ self_contained ES" + \ valid_eqs ES" lemma invariantI: - assumes "valid_eqns ES" "finite ES" "distinct_equas ES" "ardenable ES" - "finite_rhs ES" "self_contained ES" + assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable ES" + "finite_rhs ES" "valid_eqs ES" shows "invariant ES" using assms by (simp add: invariant_def) @@ -650,9 +650,9 @@ unfolding append_rhs_rexp_def by (auto simp add: Seq_def lang_of_append) -lemma classes_of_union_distrib: - shows "classes_of (A \ B) = classes_of A \ classes_of B" -by (auto simp add: classes_of_def) +lemma rhss_union_distrib: + shows "rhss (A \ B) = rhss A \ rhss B" +by (auto simp add: rhss_def) lemma lhss_union_distrib: shows "lhss (A \ B) = lhss A \ lhss B" @@ -760,8 +760,8 @@ assumes finite_CS: "finite (UNIV // \A)" shows "invariant (Init (UNIV // \A))" proof (rule invariantI) - show "valid_eqns (Init (UNIV // \A))" - unfolding valid_eqns_def + show "sound_eqs (Init (UNIV // \A))" + unfolding sound_eqs_def using l_eq_r_in_eqs by auto show "finite (Init (UNIV // \A))" using finite_CS unfolding Init_def by simp @@ -773,8 +773,8 @@ show "finite_rhs (Init (UNIV // \A))" using finite_Init_rhs[OF finite_CS] unfolding finite_rhs_def Init_def by auto - show "self_contained (Init (UNIV // \A))" - unfolding self_contained_def Init_def Init_rhs_def classes_of_def lhss_def + show "valid_eqs (Init (UNIV // \A))" + unfolding valid_eqs_def Init_def Init_rhs_def rhss_def lhss_def by auto qed @@ -891,59 +891,59 @@ by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def) lemma append_rhs_keeps_cls: - "classes_of (append_rhs_rexp rhs r) = classes_of rhs" -apply (auto simp:classes_of_def append_rhs_rexp_def) + "rhss (append_rhs_rexp rhs r) = rhss rhs" +apply (auto simp:rhss_def append_rhs_rexp_def) apply (case_tac xa, auto simp:image_def) by (rule_tac x = "SEQ ra r" in exI, rule_tac x = "Trn x ra" in bexI, simp+) lemma Arden_removes_cl: - "classes_of (Arden Y yrhs) = classes_of yrhs - {Y}" + "rhss (Arden Y yrhs) = rhss yrhs - {Y}" apply (simp add:Arden_def append_rhs_keeps_cls) -by (auto simp:classes_of_def) +by (auto simp:rhss_def) lemma lhss_keeps_cls: "lhss (Subst_all ES Y yrhs) = lhss ES" by (auto simp:lhss_def Subst_all_def) lemma Subst_updates_cls: - "X \ classes_of xrhs \ - classes_of (Subst rhs X xrhs) = classes_of rhs \ classes_of xrhs - {X}" -apply (simp only:Subst_def append_rhs_keeps_cls classes_of_union_distrib) -by (auto simp:classes_of_def) + "X \ rhss xrhs \ + rhss (Subst rhs X xrhs) = rhss rhs \ rhss xrhs - {X}" +apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib) +by (auto simp:rhss_def) -lemma Subst_all_keeps_self_contained: - assumes sc: "self_contained (ES \ {(Y, yrhs)})" (is "self_contained ?A") - shows "self_contained (Subst_all ES Y (Arden Y yrhs))" - (is "self_contained ?B") +lemma Subst_all_keeps_valid_eqs: + assumes sc: "valid_eqs (ES \ {(Y, yrhs)})" (is "valid_eqs ?A") + shows "valid_eqs (Subst_all ES Y (Arden Y yrhs))" + (is "valid_eqs ?B") proof- { fix X xrhs' assume "(X, xrhs') \ ?B" then obtain xrhs where xrhs_xrhs': "xrhs' = Subst xrhs Y (Arden Y yrhs)" and X_in: "(X, xrhs) \ ES" by (simp add:Subst_all_def, blast) - have "classes_of xrhs' \ lhss ?B" + have "rhss xrhs' \ lhss ?B" proof- have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def) - moreover have "classes_of xrhs' \ lhss ES" + moreover have "rhss xrhs' \ lhss ES" proof- - have "classes_of xrhs' \ - classes_of xrhs \ classes_of (Arden Y yrhs) - {Y}" + have "rhss xrhs' \ + rhss xrhs \ rhss (Arden Y yrhs) - {Y}" proof- - have "Y \ classes_of (Arden Y yrhs)" + have "Y \ rhss (Arden Y yrhs)" using Arden_removes_cl by simp thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls) qed - moreover have "classes_of xrhs \ lhss ES \ {Y}" using X_in sc - apply (simp only:self_contained_def lhss_union_distrib) + moreover have "rhss xrhs \ lhss ES \ {Y}" using X_in sc + apply (simp only:valid_eqs_def lhss_union_distrib) by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lhss_def) - moreover have "classes_of (Arden Y yrhs) \ lhss ES \ {Y}" + moreover have "rhss (Arden Y yrhs) \ lhss ES \ {Y}" using sc - by (auto simp add:Arden_removes_cl self_contained_def lhss_def) + by (auto simp add:Arden_removes_cl valid_eqs_def lhss_def) ultimately show ?thesis by auto qed ultimately show ?thesis by simp qed - } thus ?thesis by (auto simp only:Subst_all_def self_contained_def) + } thus ?thesis by (auto simp only:Subst_all_def valid_eqs_def) qed lemma Subst_all_satisfies_invariant: @@ -951,12 +951,12 @@ shows "invariant (Subst_all ES Y (Arden Y yrhs))" proof (rule invariantI) have Y_eq_yrhs: "Y = L yrhs" - using invariant_ES by (simp only:invariant_def valid_eqns_def, blast) + using invariant_ES by (simp only:invariant_def sound_eqs_def, blast) have finite_yrhs: "finite yrhs" using invariant_ES by (auto simp:invariant_def finite_rhs_def) have nonempty_yrhs: "rhs_nonempty yrhs" using invariant_ES by (auto simp:invariant_def ardenable_def) - show "valid_eqns (Subst_all ES Y (Arden Y yrhs))" + show "sound_eqs (Subst_all ES Y (Arden Y yrhs))" proof- have "Y = L (Arden Y yrhs)" using Y_eq_yrhs invariant_ES finite_yrhs @@ -967,7 +967,7 @@ apply(auto) done thus ?thesis using invariant_ES - unfolding invariant_def finite_rhs_def2 valid_eqns_def Subst_all_def + unfolding invariant_def finite_rhs_def2 sound_eqs_def Subst_all_def by (auto simp add: Subst_keeps_eq simp del: L_rhs.simps) qed show "finite (Subst_all ES Y (Arden Y yrhs))" @@ -1000,8 +1000,8 @@ ultimately show ?thesis by (simp add:Subst_all_keeps_finite_rhs) qed - show "self_contained (Subst_all ES Y (Arden Y yrhs))" - using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def) + show "valid_eqs (Subst_all ES Y (Arden Y yrhs))" + using invariant_ES Subst_all_keeps_valid_eqs by (simp add:invariant_def) qed lemma Remove_in_card_measure: @@ -1113,9 +1113,9 @@ lemma Solve: assumes fin: "finite (UNIV // \A)" and X_in: "X \ (UNIV // \A)" - shows "\xrhs. Solve X (Init (UNIV // \A)) = {(X, xrhs)} \ invariant {(X, xrhs)}" + shows "\rhs. Solve X (Init (UNIV // \A)) = {(X, rhs)} \ invariant {(X, rhs)}" proof - - def Inv \ "\ES. invariant ES \ (\xrhs. (X, xrhs) \ ES)" + def Inv \ "\ES. invariant ES \ (\rhs. (X, rhs) \ ES)" have "Inv (Init (UNIV // \A))" unfolding Inv_def using fin X_in by (simp add: Init_ES_satisfies_invariant, simp add: Init_def) moreover @@ -1127,12 +1127,12 @@ moreover { fix ES assume "Inv ES" and "\ Cond ES" - then have "\xrhs'. ES = {(X, xrhs')} \ invariant ES" + then have "\rhs'. ES = {(X, rhs')} \ invariant ES" unfolding Inv_def invariant_def - apply (auto, rule_tac x = xrhs in exI) + apply (auto, rule_tac x = rhs in exI) apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff) done - then have "\xrhs'. ES = {(X, xrhs')} \ invariant {(X, xrhs')}" + then have "\rhs'. ES = {(X, rhs')} \ invariant {(X, rhs')}" by auto } moreover have "wf (measure card)" by simp @@ -1146,7 +1146,7 @@ apply(auto) done } ultimately - show "\xrhs. Solve X (Init (UNIV // \A)) = {(X, xrhs)} \ invariant {(X, xrhs)}" + show "\rhs. Solve X (Init (UNIV // \A)) = {(X, rhs)} \ invariant {(X, rhs)}" unfolding Solve_def by (rule while_rule) qed @@ -1157,10 +1157,10 @@ def A \ "Arden X xrhs" have eq: "{Lam r | r. Lam r \ A} = A" proof - - have "classes_of A = {}" using Inv_ES - unfolding A_def self_contained_def invariant_def lhss_def + have "rhss A = {}" using Inv_ES + unfolding A_def valid_eqs_def invariant_def lhss_def by (simp add: Arden_removes_cl) - thus ?thesis unfolding A_def classes_of_def + thus ?thesis unfolding A_def rhss_def apply(auto simp only:) apply(case_tac x) apply(auto) @@ -1174,7 +1174,7 @@ also have "\ = L A" by (simp add: eq) also have "\ = X" proof - - have "X = L xrhs" using Inv_ES unfolding invariant_def valid_eqns_def + have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def by auto moreover from Inv_ES have "[] \ L (\{r. Trn X r \ xrhs})"