diff -r 79b37ef9505f -r e500cab16be4 Myhill_1.thy --- a/Myhill_1.thy Wed Feb 16 12:25:53 2011 +0000 +++ b/Myhill_1.thy Thu Feb 17 11:42:16 2011 +0000 @@ -512,21 +512,21 @@ "sound_eqs ES \ \(X, rhs) \ ES. X = L rhs" text {* - @{text "rhs_nonempty rhs"} requires regular expressions occuring in + @{text "ardenable rhs"} requires regular expressions occuring in transitional items of @{text "rhs"} do not contain empty string. This is necessary for the application of Arden's transformation to @{text "rhs"}. *} definition - "rhs_nonempty rhs \ (\ Y r. Trn Y r \ rhs \ [] \ L r)" + "ardenable rhs \ (\ Y r. Trn Y r \ rhs \ [] \ L r)" text {* - The following @{text "ardenable ES"} requires that Arden's transformation + The following @{text "ardenable_all ES"} requires that Arden's transformation is applicable to every equation of equational system @{text "ES"}. *} definition - "ardenable ES \ \(X, rhs) \ ES. rhs_nonempty rhs" + "ardenable_all ES \ \(X, rhs) \ ES. ardenable rhs" text {* @@ -571,12 +571,12 @@ \ finite_rhs ES \ sound_eqs ES \ distinct_equas ES - \ ardenable ES + \ ardenable_all ES \ valid_eqs ES" lemma invariantI: - assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable ES" + assumes "sound_eqs ES" "finite ES" "distinct_equas ES" "ardenable_all ES" "finite_rhs ES" "valid_eqs ES" shows "invariant ES" using assms by (simp add: invariant_def) @@ -619,9 +619,9 @@ lemma rexp_of_empty: assumes finite: "finite rhs" - and nonempty: "rhs_nonempty rhs" + and nonempty: "ardenable rhs" shows "[] \ L (\ {r. Trn X r \ rhs})" -using finite nonempty rhs_nonempty_def +using finite nonempty ardenable_def using finite_Trn[OF finite] by auto @@ -765,8 +765,8 @@ unfolding Init_def by simp show "distinct_equas (Init (UNIV // \A))" unfolding distinct_equas_def Init_def by simp - show "ardenable (Init (UNIV // \A))" - unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def + show "ardenable_all (Init (UNIV // \A))" + unfolding ardenable_all_def Init_def Init_rhs_def ardenable_def by auto show "finite_rhs (Init (UNIV // \A))" using finite_Init_rhs[OF finite_CS] @@ -785,7 +785,7 @@ lemma Arden_keeps_eq: assumes l_eq_r: "X = L rhs" - and not_empty: "[] \ L (\{r. Trn X r \ rhs})" + and not_empty: "ardenable rhs" and finite: "finite rhs" shows "X = L (Arden X rhs)" proof - @@ -799,9 +799,11 @@ unfolding L_rhs_union_distrib[symmetric] by (simp only: lang_of_rexp_of finite B_def A_def) finally show ?thesis - using l_eq_r not_empty apply(rule_tac arden[THEN iffD1]) - apply(simp add: A_def) + apply(simp (no_asm) add: A_def) + using finite_Trn[OF finite] not_empty + apply(simp add: ardenable_def) + using l_eq_r apply(simp) done qed @@ -820,25 +822,25 @@ by (auto simp:Arden_def append_keeps_finite) lemma append_keeps_nonempty: - "rhs_nonempty rhs \ rhs_nonempty (append_rhs_rexp rhs r)" -apply (auto simp:rhs_nonempty_def append_rhs_rexp_def) + "ardenable rhs \ ardenable (append_rhs_rexp rhs r)" +apply (auto simp:ardenable_def append_rhs_rexp_def) by (case_tac x, auto simp:Seq_def) lemma nonempty_set_sub: - "rhs_nonempty rhs \ rhs_nonempty (rhs - A)" -by (auto simp:rhs_nonempty_def) + "ardenable rhs \ ardenable (rhs - A)" +by (auto simp:ardenable_def) lemma nonempty_set_union: - "\rhs_nonempty rhs; rhs_nonempty rhs'\ \ rhs_nonempty (rhs \ rhs')" -by (auto simp:rhs_nonempty_def) + "\ardenable rhs; ardenable rhs'\ \ ardenable (rhs \ rhs')" +by (auto simp:ardenable_def) lemma Arden_keeps_nonempty: - "rhs_nonempty rhs \ rhs_nonempty (Arden X rhs)" + "ardenable rhs \ ardenable (Arden X rhs)" by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub) lemma Subst_keeps_nonempty: - "\rhs_nonempty rhs; rhs_nonempty xrhs\ \ rhs_nonempty (Subst rhs X xrhs)" + "\ardenable rhs; ardenable xrhs\ \ ardenable (Subst rhs X xrhs)" by (simp only:Subst_def append_keeps_nonempty nonempty_set_union nonempty_set_sub) lemma Subst_keeps_eq: @@ -869,19 +871,16 @@ by (auto simp:Subst_def append_keeps_finite) lemma Subst_all_keeps_finite: - assumes finite:"finite (ES:: (string set \ rhs_item set) set)" + assumes finite: "finite ES" shows "finite (Subst_all ES Y yrhs)" proof - - have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \ ES}" - (is "finite ?A") - proof- - def eqns' \ "{(Ya::lang, yrhsa) | Ya yrhsa. (Ya, yrhsa) \ ES}" - def h \ "\(Ya::lang, yrhsa). (Ya, Subst yrhsa Y yrhs)" - have "finite (h ` eqns')" using finite h_def eqns'_def by auto - moreover have "?A = h ` eqns'" by (auto simp:h_def eqns'_def) - ultimately show ?thesis by auto - qed - thus ?thesis by (simp add:Subst_all_def) + def eqns \ "{(X::lang, rhs) |X rhs. (X, rhs) \ ES}" + def h \ "\(X::lang, rhs). (X, Subst rhs Y yrhs)" + have "finite (h ` eqns)" using finite h_def eqns_def by auto + moreover + have "Subst_all ES Y yrhs = h ` eqns" unfolding h_def eqns_def Subst_all_def by auto + ultimately + show "finite (Subst_all ES Y yrhs)" by simp qed lemma Subst_all_keeps_finite_rhs: @@ -910,10 +909,9 @@ by (auto simp:rhss_def) 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- + 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 @@ -924,8 +922,7 @@ have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def) moreover have "rhss xrhs' \ lhss ES" proof- - have "rhss xrhs' \ - rhss xrhs \ rhss (Arden Y yrhs) - {Y}" + have "rhss xrhs' \ rhss xrhs \ rhss (Arden Y yrhs) - {Y}" proof- have "Y \ rhss (Arden Y yrhs)" using Arden_removes_cl by simp @@ -952,38 +949,38 @@ 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) + have nonempty_yrhs: "ardenable yrhs" + using invariant_ES by (auto simp:invariant_def ardenable_all_def) show "sound_eqs (Subst_all ES Y (Arden Y yrhs))" - proof- + proof - have "Y = L (Arden Y yrhs)" using Y_eq_yrhs invariant_ES finite_yrhs using finite_Trn[OF finite_yrhs] apply(rule_tac Arden_keeps_eq) apply(simp_all) - unfolding invariant_def ardenable_def rhs_nonempty_def + unfolding invariant_def ardenable_all_def ardenable_def apply(auto) done thus ?thesis using invariant_ES - unfolding invariant_def finite_rhs_def2 sound_eqs_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))" using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite) show "distinct_equas (Subst_all ES Y (Arden Y yrhs))" - using invariant_ES - by (auto simp:distinct_equas_def Subst_all_def invariant_def) - show "ardenable (Subst_all ES Y (Arden Y yrhs))" + using invariant_ES + unfolding distinct_equas_def Subst_all_def invariant_def by auto + show "ardenable_all (Subst_all ES Y (Arden Y yrhs))" proof - { fix X rhs assume "(X, rhs) \ ES" - hence "rhs_nonempty rhs" using prems invariant_ES - by (auto simp add:invariant_def ardenable_def) + hence "ardenable rhs" using prems invariant_ES + by (auto simp add:invariant_def ardenable_all_def) with nonempty_yrhs - have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))" + have "ardenable (Subst rhs Y (Arden Y yrhs))" by (simp add:nonempty_yrhs Subst_keeps_nonempty Arden_keeps_nonempty) - } thus ?thesis by (auto simp add:ardenable_def Subst_all_def) + } thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def) qed show "finite_rhs (Subst_all ES Y (Arden Y yrhs))" proof- @@ -1079,7 +1076,9 @@ assume h: "(Y, yrhs) \ ES" "X \ Y" then have "ES - {(Y, yrhs)} \ {(Y, yrhs)} = ES" by auto then show "invariant (Remove ES Y yrhs)" unfolding Remove_def - using Inv_ES by (rule_tac Subst_all_satisfies_invariant) (simp) + using Inv_ES + thm Subst_all_satisfies_invariant + by (rule_tac Subst_all_satisfies_invariant) (simp) qed qed @@ -1124,14 +1123,14 @@ by (auto simp add: iteration_step_invariant iteration_step_ex) } moreover { fix ES - assume "Inv ES" and "\ Cond ES" - then have "\rhs'. ES = {(X, rhs')} \ invariant ES" - unfolding Inv_def invariant_def - apply (auto, rule_tac x = rhs in exI) - apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff) - done - then have "\rhs'. ES = {(X, rhs')} \ invariant {(X, rhs')}" - by auto } + assume inv: "Inv ES" and not_crd: "\Cond ES" + from inv obtain rhs where "(X, rhs) \ ES" unfolding Inv_def by auto + moreover + from not_crd have "card ES = 1" by simp + ultimately + have "ES = {(X, rhs)}" by (auto simp add: card_Suc_eq) + then have "\rhs'. ES = {(X, rhs')} \ invariant {(X, rhs')}" using inv + unfolding Inv_def by auto } moreover have "wf (measure card)" by simp moreover @@ -1173,7 +1172,7 @@ have "X = L xrhs" using Inv_ES unfolding invariant_def sound_eqs_def by simp then have "X = L A" using Inv_ES - unfolding A_def invariant_def ardenable_def finite_rhs_def rhs_nonempty_def + unfolding A_def invariant_def ardenable_all_def finite_rhs_def by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn) then have "X = L {Lam r | r. Lam r \ A}" using eq by simp then have "X = L (\{r. Lam r \ A})" using fin by auto