diff -r 5fed809d0fc1 -r f460d5f75cb5 Myhill_1.thy --- a/Myhill_1.thy Mon Feb 14 11:12:01 2011 +0000 +++ b/Myhill_1.thy Mon Feb 14 23:10:44 2011 +0000 @@ -528,12 +528,17 @@ definition "ardenable ES \ \(X, rhs) \ ES. rhs_nonempty rhs" + text {* @{text "finite_rhs ES"} requires every equation in @{text "rhs"} be finite. *} definition - "finite_rhs ES \ \ X rhs. (X, rhs) \ ES \ finite rhs" + "finite_rhs ES \ \(X, rhs) \ ES. finite rhs" + +lemma finite_rhs_def2: + "finite_rhs ES = (\ X rhs. (X, rhs) \ ES \ finite rhs)" +unfolding finite_rhs_def by auto text {* @{text "classes_of rhs"} returns all variables (or equivalent classes) @@ -548,22 +553,26 @@ equational system @{text "ES"}. *} definition - "lefts_of ES \ {Y | Y yrhs. (Y, yrhs) \ ES}" + "lhss ES \ {Y | Y yrhs. (Y, yrhs) \ ES}" text {* The following @{text "self_contained 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 \ lefts_of ES" + "self_contained ES \ \(X, xrhs) \ ES. classes_of xrhs \ lhss ES" text {* The invariant @{text "invariant(ES)"} is a conjunction of all the previously defined constaints. *} definition - "invariant ES \ valid_eqns ES \ finite ES \ distinct_equas ES \ ardenable ES \ - finite_rhs ES \ self_contained ES" + "invariant ES \ finite ES + \ finite_rhs ES + \ valid_eqns ES + \ distinct_equas ES + \ ardenable ES + \ self_contained ES" lemma invariantI: @@ -645,9 +654,9 @@ shows "classes_of (A \ B) = classes_of A \ classes_of B" by (auto simp add: classes_of_def) -lemma lefts_of_union_distrib: - shows "lefts_of (A \ B) = lefts_of A \ lefts_of B" -by (auto simp add: lefts_of_def) +lemma lhss_union_distrib: + shows "lhss (A \ B) = lhss A \ lhss B" +by (auto simp add: lhss_def) subsubsection {* Intialization *} @@ -760,12 +769,12 @@ unfolding distinct_equas_def Init_def by simp show "ardenable (Init (UNIV // \A))" unfolding ardenable_def Init_def Init_rhs_def rhs_nonempty_def - by auto + by auto 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 lefts_of_def + unfolding self_contained_def Init_def Init_rhs_def classes_of_def lhss_def by auto qed @@ -892,9 +901,9 @@ apply (simp add:Arden_def append_rhs_keeps_cls) by (auto simp:classes_of_def) -lemma lefts_of_keeps_cls: - "lefts_of (Subst_all ES Y yrhs) = lefts_of ES" -by (auto simp:lefts_of_def Subst_all_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 \ @@ -912,10 +921,10 @@ 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' \ lefts_of ?B" + have "classes_of xrhs' \ lhss ?B" proof- - have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def Subst_all_def) - moreover have "classes_of xrhs' \ lefts_of ES" + have "lhss ?B = lhss ES" by (auto simp add:lhss_def Subst_all_def) + moreover have "classes_of xrhs' \ lhss ES" proof- have "classes_of xrhs' \ classes_of xrhs \ classes_of (Arden Y yrhs) - {Y}" @@ -924,12 +933,12 @@ using Arden_removes_cl by simp thus ?thesis using xrhs_xrhs' by (auto simp:Subst_updates_cls) qed - moreover have "classes_of xrhs \ lefts_of ES \ {Y}" using X_in sc - apply (simp only:self_contained_def lefts_of_union_distrib) - by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def) - moreover have "classes_of (Arden Y yrhs) \ lefts_of ES \ {Y}" + moreover have "classes_of xrhs \ lhss ES \ {Y}" using X_in sc + apply (simp only:self_contained_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}" using sc - by (auto simp add:Arden_removes_cl self_contained_def lefts_of_def) + by (auto simp add:Arden_removes_cl self_contained_def lhss_def) ultimately show ?thesis by auto qed ultimately show ?thesis by simp @@ -950,12 +959,16 @@ show "valid_eqns (Subst_all ES Y (Arden Y yrhs))" proof- have "Y = L (Arden Y yrhs)" - using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs - by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+) - thus ?thesis using invariant_ES - by (auto simp add:valid_eqns_def - Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def - simp del:L_rhs.simps) + 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 + apply(auto) + done + thus ?thesis using invariant_ES + unfolding invariant_def finite_rhs_def2 valid_eqns_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) @@ -1015,27 +1028,24 @@ by (auto simp: Subst_all_def) lemma card_noteq_1_has_more: - assumes card:"card S \ 1" - and e_in: "e \ S" - and finite: "finite S" - obtains e' where "e' \ S \ e \ e'" + assumes card:"Cond ES" + and e_in: "(X, xrhs) \ ES" + and finite: "finite ES" + shows "\(Y, yrhs) \ ES. (X, xrhs) \ (Y, yrhs)" proof- - have "card (S - {e}) > 0" - proof - - have "card S > 1" using card e_in finite - by (cases "card S") (auto) - thus ?thesis using finite e_in by auto - qed - hence "S - {e} \ {}" using finite by (rule_tac notI, simp) - thus "(\e'. e' \ S \ e \ e' \ thesis) \ thesis" by auto + have "card ES > 1" using card e_in finite + by (cases "card ES") (auto) + then have "card (ES - {(X, xrhs)}) > 0" + using finite e_in by auto + then have "(ES - {(X, xrhs)}) \ {}" using finite by (rule_tac notI, simp) + then show "\(Y, yrhs) \ ES. (X, xrhs) \ (Y, yrhs)" + by auto qed - - lemma iteration_step_measure: assumes Inv_ES: "invariant ES" and X_in_ES: "(X, xrhs) \ ES" - and not_T: "card ES \ 1" + and not_T: "Cond ES " shows "(Iter X ES, ES) \ measure card" proof - have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) @@ -1043,8 +1053,8 @@ where Y_in_ES: "(Y, yrhs) \ ES" and not_eq: "(X, xrhs) \ (Y, yrhs)" using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) then have "(Y, yrhs) \ ES " "X \ Y" - using X_in_ES Inv_ES - by (auto simp: invariant_def distinct_equas_def) + using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def + by auto then show "(Iter X ES, ES) \ measure card" apply(rule IterI2) apply(rule Remove_in_card_measure) @@ -1055,16 +1065,16 @@ lemma iteration_step_invariant: assumes Inv_ES: "invariant ES" and X_in_ES: "(X, xrhs) \ ES" - and not_T: "card ES \ 1" + and not_T: "Cond ES" shows "invariant (Iter X ES)" proof - have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) then obtain Y yrhs where Y_in_ES: "(Y, yrhs) \ ES" and not_eq: "(X, xrhs) \ (Y, yrhs)" using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) - then have "(Y, yrhs) \ ES " "X \ Y" - using X_in_ES Inv_ES - by (auto simp: invariant_def distinct_equas_def) + then have "(Y, yrhs) \ ES" "X \ Y" + using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def + by auto then show "invariant (Iter X ES)" proof(rule IterI2) fix Y yrhs @@ -1078,7 +1088,7 @@ lemma iteration_step_ex: assumes Inv_ES: "invariant ES" and X_in_ES: "(X, xrhs) \ ES" - and not_T: "card ES \ 1" + and not_T: "Cond ES" shows "\xrhs'. (X, xrhs') \ (Iter X ES)" proof - have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) @@ -1086,8 +1096,8 @@ where Y_in_ES: "(Y, yrhs) \ ES" and not_eq: "(X, xrhs) \ (Y, yrhs)" using not_T X_in_ES by (drule_tac card_noteq_1_has_more) (auto) then have "(Y, yrhs) \ ES " "X \ Y" - using X_in_ES Inv_ES - by (auto simp: invariant_def distinct_equas_def) + using X_in_ES Inv_ES unfolding invariant_def distinct_equas_def + by auto then show "\xrhs'. (X, xrhs') \ (Iter X ES)" apply(rule IterI2) unfolding Remove_def @@ -1100,49 +1110,44 @@ subsubsection {* Conclusion of the proof *} -text {* - From this point until @{text "hard_direction"}, the hard direction is proved - through a simple application of the iteration principle. -*} - - -lemma reduce_x: - assumes inv: "invariant ES" - and contain_x: "(X, xrhs) \ ES" - shows "\ xrhs'. Solve X ES = {(X, xrhs')} \ invariant(Solve X ES)" +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)}" proof - - let ?Inv = "\ ES. (invariant ES \ (\ xrhs. (X, xrhs) \ ES))" - show ?thesis unfolding Solve_def - proof (rule while_rule [where P = ?Inv and r = "measure card"]) - from inv and contain_x show "?Inv ES" by auto - next - show "wf (measure card)" by simp - next - fix ES - assume inv: "?Inv ES" and crd: "card ES \ 1" - then show "(Iter X ES, ES) \ measure card" + def Inv \ "\ES. invariant ES \ (\xrhs. (X, xrhs) \ 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 + { fix ES + assume inv: "Inv ES" and crd: "Cond ES" + then have "Inv (Iter X ES)" + unfolding Inv_def + by (auto simp add: iteration_step_invariant iteration_step_ex) } + moreover + { fix ES + assume "Inv ES" and "\ Cond ES" + then have "\xrhs'. ES = {(X, xrhs')} \ invariant ES" + unfolding Inv_def invariant_def + apply (auto, rule_tac x = xrhs in exI) + apply (auto dest!: card_Suc_Diff1 simp: card_eq_0_iff) + done + then have "\xrhs'. ES = {(X, xrhs')} \ invariant {(X, xrhs')}" + by auto } + moreover + have "wf (measure card)" by simp + moreover + { fix ES + assume inv: "Inv ES" and crd: "Cond ES" + then have "(Iter X ES, ES) \ measure card" + unfolding Inv_def apply(clarify) - apply(rule iteration_step_measure) - apply(auto) - done - next - fix ES - assume inv: "?Inv ES" and crd: "card ES \ 1" - then show "?Inv (Iter X ES)" - apply - - apply(auto) - apply(rule iteration_step_invariant) + apply(rule_tac iteration_step_measure) apply(auto) - apply(rule iteration_step_ex) - apply(auto) - done - next - fix ES - assume "?Inv ES" and "\ card ES \ 1" - thus "\xrhs'. ES = {(X, xrhs')} \ invariant ES" - apply (auto, rule_tac x = xrhs in exI) - by (auto simp: invariant_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) - qed + done } + ultimately + show "\xrhs. Solve X (Init (UNIV // \A)) = {(X, xrhs)} \ invariant {(X, xrhs)}" + unfolding Solve_def by (rule while_rule) qed lemma last_cl_exists_rexp: @@ -1153,7 +1158,7 @@ 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 lefts_of_def + unfolding A_def self_contained_def invariant_def lhss_def by (simp add: Arden_removes_cl) thus ?thesis unfolding A_def classes_of_def apply(auto simp only:) @@ -1190,20 +1195,13 @@ and X_in_CS: "X \ (UNIV // \A)" shows "\r::rexp. L r = X" proof - - def ES \ "Init (UNIV // \A)" - have "invariant ES" using finite_CS unfolding ES_def - by (rule Init_ES_satisfies_invariant) - moreover - from X_in_CS obtain xrhs where "(X, xrhs) \ ES" unfolding ES_def - unfolding Init_def Init_rhs_def by auto - ultimately - obtain xrhs' where "Solve X ES = {(X, xrhs')}" "invariant (Solve X ES)" - using reduce_x by blast + from finite_CS X_in_CS + obtain xrhs where "invariant {(X, xrhs)}" + using Solve by metis then show "\r::rexp. L r = X" - using last_cl_exists_rexp by auto + using last_cl_exists_rexp by auto qed - lemma bchoice_finite_set: assumes a: "\x \ S. \y. x = f y" and b: "finite S"