diff -r c6ebfe052109 -r edacc141060f Myhill_1.thy --- a/Myhill_1.thy Thu Jul 28 11:56:25 2011 +0000 +++ b/Myhill_1.thy Thu Jul 28 14:22:10 2011 +0000 @@ -5,7 +5,7 @@ section {* Direction @{text "finite partition \ regular language"} *} -lemma Pair_Collect[simp]: +lemma Pair_Collect [simp]: shows "(x, y) \ {(x, y). P x y} \ P x y" by simp @@ -57,7 +57,6 @@ by (auto) lemma lang_rhs_union_distrib: - fixes A B::"('a trm) set" shows "lang_rhs A \ lang_rhs B = lang_rhs (A \ B)" by simp @@ -350,7 +349,7 @@ subsubsection {* Interation step *} -lemma Arden_keeps_eq: +lemma Arden_preserves_soundness: assumes l_eq_r: "X = lang_rhs rhs" and not_empty: "ardenable rhs" and finite: "finite rhs" @@ -379,37 +378,37 @@ finally show "X = lang_rhs (Arden X rhs)" by simp qed -lemma Append_keeps_finite: +lemma Append_preserves_finite: "finite rhs \ finite (Append_rexp_rhs rhs r)" by (auto simp: Append_rexp_rhs_def) -lemma Arden_keeps_finite: +lemma Arden_preserves_finite: "finite rhs \ finite (Arden X rhs)" -by (auto simp: Arden_def Append_keeps_finite) +by (auto simp: Arden_def Append_preserves_finite) -lemma Append_keeps_nonempty: +lemma Append_preserves_ardenable: "ardenable rhs \ ardenable (Append_rexp_rhs rhs r)" apply (auto simp: ardenable_def Append_rexp_rhs_def) by (case_tac x, auto simp: conc_def) -lemma nonempty_set_sub: +lemma ardenable_set_sub: "ardenable rhs \ ardenable (rhs - A)" by (auto simp:ardenable_def) -lemma nonempty_set_union: +lemma ardenable_set_union: "\ardenable rhs; ardenable rhs'\ \ ardenable (rhs \ rhs')" by (auto simp:ardenable_def) -lemma Arden_keeps_nonempty: +lemma Arden_preserves_ardenable: "ardenable rhs \ ardenable (Arden X rhs)" -by (simp only:Arden_def Append_keeps_nonempty nonempty_set_sub) +by (simp only:Arden_def Append_preserves_ardenable ardenable_set_sub) -lemma Subst_keeps_nonempty: +lemma Subst_preserves_ardenable: "\ardenable rhs; ardenable xrhs\ \ ardenable (Subst rhs X xrhs)" -by (simp only: Subst_def Append_keeps_nonempty nonempty_set_union nonempty_set_sub) +by (simp only: Subst_def Append_preserves_ardenable ardenable_set_union ardenable_set_sub) -lemma Subst_keeps_eq: +lemma Subst_preserves_soundness: assumes substor: "X = lang_rhs xrhs" and finite: "finite rhs" shows "lang_rhs (Subst rhs X xrhs) = lang_rhs rhs" (is "?Left = ?Right") @@ -433,11 +432,11 @@ ultimately show ?thesis by simp qed -lemma Subst_keeps_finite_rhs: +lemma Subst_preserves_finite_rhs: "\finite rhs; finite yrhs\ \ finite (Subst rhs Y yrhs)" -by (auto simp: Subst_def Append_keeps_finite) +by (auto simp: Subst_def Append_preserves_finite) -lemma Subst_all_keeps_finite: +lemma Subst_all_preserves_finite: assumes finite: "finite ES" shows "finite (Subst_all ES Y yrhs)" proof - @@ -450,11 +449,11 @@ show "finite (Subst_all ES Y yrhs)" by simp qed -lemma Subst_all_keeps_finite_rhs: +lemma Subst_all_preserves_finite_rhs: "\finite_rhs ES; finite yrhs\ \ finite_rhs (Subst_all ES Y yrhs)" -by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def) +by (auto intro:Subst_preserves_finite_rhs simp add:Subst_all_def finite_rhs_def) -lemma append_rhs_keeps_cls: +lemma append_rhs_preserves_cls: "rhss (Append_rexp_rhs rhs r) = rhss rhs" apply (auto simp: rhss_def Append_rexp_rhs_def) apply (case_tac xa, auto simp: image_def) @@ -462,20 +461,20 @@ lemma Arden_removes_cl: "rhss (Arden Y yrhs) = rhss yrhs - {Y}" -apply (simp add:Arden_def append_rhs_keeps_cls) +apply (simp add:Arden_def append_rhs_preserves_cls) by (auto simp: rhss_def) -lemma lhss_keeps_cls: +lemma lhss_preserves_cls: "lhss (Subst_all ES Y yrhs) = lhss ES" by (auto simp: lhss_def Subst_all_def) lemma Subst_updates_cls: "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) +apply (simp only:Subst_def append_rhs_preserves_cls rhss_union_distrib) by (auto simp: rhss_def) -lemma Subst_all_keeps_validity: +lemma Subst_all_preserves_validity: assumes sc: "validity (ES \ {(Y, yrhs)})" (is "validity ?A") shows "validity (Subst_all ES Y (Arden Y yrhs))" (is "validity ?B") proof - @@ -516,24 +515,24 @@ using invariant_ES by (simp only:invariant_def soundness_def, blast) have finite_yrhs: "finite yrhs" using invariant_ES by (auto simp:invariant_def finite_rhs_def) - have nonempty_yrhs: "ardenable yrhs" + have ardenable_yrhs: "ardenable yrhs" using invariant_ES by (auto simp:invariant_def ardenable_all_def) show "soundness (Subst_all ES Y (Arden Y yrhs))" proof - have "Y = lang_rhs (Arden Y yrhs)" using Y_eq_yrhs invariant_ES finite_yrhs using finite_Trn[OF finite_yrhs] - apply(rule_tac Arden_keeps_eq) + apply(rule_tac Arden_preserves_soundness) apply(simp_all) unfolding invariant_def ardenable_all_def ardenable_def apply(auto) done thus ?thesis using invariant_ES unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def - by (auto simp add: Subst_keeps_eq simp del: lang_rhs.simps) + by (auto simp add: Subst_preserves_soundness simp del: lang_rhs.simps) qed show "finite (Subst_all ES Y (Arden Y yrhs))" - using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite) + using invariant_ES by (simp add:invariant_def Subst_all_preserves_finite) show "distinctness (Subst_all ES Y (Arden Y yrhs))" using invariant_ES unfolding distinctness_def Subst_all_def invariant_def by auto @@ -543,10 +542,10 @@ assume "(X, rhs) \ ES" hence "ardenable rhs" using invariant_ES by (auto simp add:invariant_def ardenable_all_def) - with nonempty_yrhs + with ardenable_yrhs have "ardenable (Subst rhs Y (Arden Y yrhs))" - by (simp add:nonempty_yrhs - Subst_keeps_nonempty Arden_keeps_nonempty) + by (simp add:ardenable_yrhs + Subst_preserves_ardenable Arden_preserves_ardenable) } thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def) qed show "finite_rhs (Subst_all ES Y (Arden Y yrhs))" @@ -557,13 +556,13 @@ proof - have "finite yrhs" using invariant_ES by (auto simp:invariant_def finite_rhs_def) - thus ?thesis using Arden_keeps_finite by auto + thus ?thesis using Arden_preserves_finite by auto qed ultimately show ?thesis - by (simp add:Subst_all_keeps_finite_rhs) + by (simp add:Subst_all_preserves_finite_rhs) qed show "validity (Subst_all ES Y (Arden Y yrhs))" - using invariant_ES Subst_all_keeps_validity by (auto simp add: invariant_def) + using invariant_ES Subst_all_preserves_validity by (auto simp add: invariant_def) qed lemma Remove_in_card_measure: @@ -734,14 +733,14 @@ by (auto, case_tac x, auto) have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def - using Arden_keeps_finite by auto + using Arden_preserves_finite by auto then have fin: "finite {r. Lam r \ A}" by (rule finite_Lam) have "X = lang_rhs xrhs" using Inv_ES unfolding invariant_def soundness_def by simp then have "X = lang_rhs A" using Inv_ES unfolding A_def invariant_def ardenable_all_def finite_rhs_def - by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn) + by (rule_tac Arden_preserves_soundness) (simp_all add: finite_Trn) then have "X = lang_rhs {Lam r | r. Lam r \ A}" using eq by simp then have "X = lang (\{r. Lam r \ A})" using fin by auto then show "\r. X = lang r" by blast