diff -r 2aa3756dcc9f -r 5b12cd0a3b3c Myhill_1.thy --- a/Myhill_1.thy Thu Feb 10 08:40:38 2011 +0000 +++ b/Myhill_1.thy Thu Feb 10 12:32:45 2011 +0000 @@ -249,6 +249,33 @@ show "X = B ;; A\" by simp qed +(* +corollary arden_eq: + assumes nemp: "[] \ A" + shows "(X ;; A \ B) = (B ;; A\)" +proof - + { assume "X = X ;; A \ B" + then have "X = B ;; A\" + then have ?thesis + thm arden[THEN iffD1] +apply(rule set_eqI) +thm arden[THEN iffD1] +apply(rule iffI) +apply(rule trans) +apply(rule arden[THEN iffD2, symmetric]) +apply(rule arden[OF iffD1, symmetric]) +thm trans +proof - + { assume "X = X ;; A \ B" + then have "X = B ;; A\" using arden[OF nemp] by blast + moreover + + +using arden[of "A" "X" "B", OF nemp] +apply(erule_tac iffE) +apply(blast) +*) + section {* Regular Expressions *} @@ -287,7 +314,7 @@ abbreviation Setalt ("\_" [1000] 999) where - "\A == folds ALT NULL A" + "\A \ folds ALT NULL A" text {* For finite sets, @{term Setalt} is preserved under @{term L}. @@ -297,8 +324,8 @@ fixes rs::"rexp set" assumes a: "finite rs" shows "L (\rs) = \ (L ` rs)" +unfolding folds_def apply(rule set_eqI) -apply(simp add: folds_def) apply(rule someI2_ex) apply(rule_tac finite_imp_fold_graph[OF a]) apply(erule fold_graph.induct) @@ -346,8 +373,7 @@ lemma finals_in_partitions: shows "finals A \ (UNIV // \A)" -unfolding finals_def -unfolding quotient_def +unfolding finals_def quotient_def by auto @@ -376,9 +402,6 @@ "L_rhs rhs = \ (L ` rhs)" end -definition - "trns_of rhs X \ {Trn X r | r. Trn X r \ rhs}" - text {* Transitions between equivalence classes *} definition @@ -418,8 +441,8 @@ "append_rhs_rexp rhs rexp \ (append_rexp rexp) ` rhs" definition - "arden_op X rhs \ - append_rhs_rexp (rhs - trns_of rhs X) (STAR (\ {r. Trn X r \ rhs}))" + "Arden X rhs \ + append_rhs_rexp (rhs - {Trn X r | r. Trn X r \ rhs}) (STAR (\ {r. Trn X r \ rhs}))" section {* Substitution Operation on equations *} @@ -430,8 +453,8 @@ *} definition - "subst_op rhs X xrhs \ - (rhs - (trns_of rhs X)) \ (append_rhs_rexp xrhs (\ {r. Trn X r \ rhs}))" + "Subst rhs X xrhs \ + (rhs - {Trn X r | r. Trn X r \ rhs}) \ (append_rhs_rexp xrhs (\ {r. Trn X r \ rhs}))" text {* @{text "eqs_subst ES X xrhs"} substitutes @{text xrhs} into every @@ -439,7 +462,7 @@ *} definition - "subst_op_all ES X xrhs \ {(Y, subst_op yrhs X xrhs) | Y yrhs. (Y, yrhs) \ ES}" + "Subst_all ES X xrhs \ {(Y, Subst yrhs X xrhs) | Y yrhs. (Y, yrhs) \ ES}" section {* While-combinator *} @@ -454,7 +477,7 @@ definition "remove_op ES Y yrhs \ - subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)" + Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)" text {* The following term @{text "iterm X ES"} represents one iteration in the while loop. @@ -760,20 +783,19 @@ the correctness of the iteration step @{text "iter X ES"} is proved. *} -lemma arden_op_keeps_eq: +lemma Arden_keeps_eq: assumes l_eq_r: "X = L rhs" and not_empty: "[] \ L (\{r. Trn X r \ rhs})" and finite: "finite rhs" - shows "X = L (arden_op X rhs)" + shows "X = L (Arden X rhs)" proof - def A \ "L (\{r. Trn X r \ rhs})" - def b \ "rhs - trns_of rhs X" + def b \ "rhs - {Trn X r | r. Trn X r \ rhs}" def B \ "L b" have "X = B ;; A\" proof- - have "L rhs = L(trns_of rhs X \ b)" by (auto simp: b_def trns_of_def) + have "L rhs = L({Trn X r | r. Trn X r \ rhs} \ b)" by (auto simp: b_def) also have "\ = X ;; A \ B" - unfolding trns_of_def unfolding L_rhs_union_distrib[symmetric] by (simp only: lang_of_rexp_of finite B_def A_def) finally show ?thesis @@ -783,8 +805,8 @@ apply(simp) done qed - moreover have "L (arden_op X rhs) = (B ;; A\)" - by (simp only:arden_op_def L_rhs_union_distrib lang_of_append_rhs + moreover have "L (Arden X rhs) = B ;; A\" + by (simp only:Arden_def L_rhs_union_distrib lang_of_append_rhs B_def A_def b_def L_rexp.simps seq_union_distrib_left) ultimately show ?thesis by simp qed @@ -793,9 +815,9 @@ "finite rhs \ finite (append_rhs_rexp rhs r)" by (auto simp:append_rhs_rexp_def) -lemma arden_op_keeps_finite: - "finite rhs \ finite (arden_op X rhs)" -by (auto simp:arden_op_def append_keeps_finite) +lemma Arden_keeps_finite: + "finite rhs \ finite (Arden X rhs)" +by (auto simp:Arden_def append_keeps_finite) lemma append_keeps_nonempty: "rhs_nonempty rhs \ rhs_nonempty (append_rhs_rexp rhs r)" @@ -810,32 +832,31 @@ "\rhs_nonempty rhs; rhs_nonempty rhs'\ \ rhs_nonempty (rhs \ rhs')" by (auto simp:rhs_nonempty_def) -lemma arden_op_keeps_nonempty: - "rhs_nonempty rhs \ rhs_nonempty (arden_op X rhs)" -by (simp only:arden_op_def append_keeps_nonempty nonempty_set_sub) +lemma Arden_keeps_nonempty: + "rhs_nonempty rhs \ rhs_nonempty (Arden X rhs)" +by (simp only:Arden_def append_keeps_nonempty nonempty_set_sub) -lemma subst_op_keeps_nonempty: - "\rhs_nonempty rhs; rhs_nonempty xrhs\ \ rhs_nonempty (subst_op rhs X xrhs)" -by (simp only:subst_op_def append_keeps_nonempty nonempty_set_union nonempty_set_sub) +lemma Subst_keeps_nonempty: + "\rhs_nonempty rhs; rhs_nonempty xrhs\ \ rhs_nonempty (Subst rhs X xrhs)" +by (simp only:Subst_def append_keeps_nonempty nonempty_set_union nonempty_set_sub) -lemma subst_op_keeps_eq: +lemma Subst_keeps_eq: assumes substor: "X = L xrhs" and finite: "finite rhs" - shows "L (subst_op rhs X xrhs) = L rhs" (is "?Left = ?Right") + shows "L (Subst rhs X xrhs) = L rhs" (is "?Left = ?Right") proof- - def A \ "L (rhs - trns_of rhs X)" + def A \ "L (rhs - {Trn X r | r. Trn X r \ rhs})" have "?Left = A \ L (append_rhs_rexp xrhs (\{r. Trn X r \ rhs}))" - unfolding subst_op_def + unfolding Subst_def unfolding L_rhs_union_distrib[symmetric] by (simp add: A_def) moreover have "?Right = A \ L ({Trn X r | r. Trn X r \ rhs})" proof- - have "rhs = (rhs - trns_of rhs X) \ (trns_of rhs X)" by (auto simp add: trns_of_def) + have "rhs = (rhs - {Trn X r | r. Trn X r \ rhs}) \ ({Trn X r | r. Trn X r \ rhs})" by auto thus ?thesis unfolding A_def unfolding L_rhs_union_distrib - unfolding trns_of_def by simp qed moreover have "L (append_rhs_rexp xrhs (\{r. Trn X r \ rhs})) = L ({Trn X r | r. Trn X r \ rhs})" @@ -843,29 +864,29 @@ ultimately show ?thesis by simp qed -lemma subst_op_keeps_finite_rhs: - "\finite rhs; finite yrhs\ \ finite (subst_op rhs Y yrhs)" -by (auto simp:subst_op_def append_keeps_finite) +lemma Subst_keeps_finite_rhs: + "\finite rhs; finite yrhs\ \ finite (Subst rhs Y yrhs)" +by (auto simp:Subst_def append_keeps_finite) -lemma subst_op_all_keeps_finite: +lemma Subst_all_keeps_finite: assumes finite:"finite (ES:: (string set \ rhs_item set) set)" - shows "finite (subst_op_all ES Y yrhs)" + shows "finite (Subst_all ES Y yrhs)" proof - - have "finite {(Ya, subst_op yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \ ES}" + have "finite {(Ya, Subst yrhsa Y yrhs) |Ya yrhsa. (Ya, yrhsa) \ ES}" (is "finite ?A") proof- def eqns' \ "{((Ya::string set), yrhsa)| Ya yrhsa. (Ya, yrhsa) \ ES}" - def h \ "\ ((Ya::string set), yrhsa). (Ya, subst_op yrhsa Y yrhs)" + def h \ "\ ((Ya::string set), 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_op_all_def) + thus ?thesis by (simp add:Subst_all_def) qed -lemma subst_op_all_keeps_finite_rhs: - "\finite_rhs ES; finite yrhs\ \ finite_rhs (subst_op_all ES Y yrhs)" -by (auto intro:subst_op_keeps_finite_rhs simp add:subst_op_all_def finite_rhs_def) +lemma Subst_all_keeps_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) lemma append_rhs_keeps_cls: "classes_of (append_rhs_rexp rhs r) = classes_of rhs" @@ -873,61 +894,61 @@ 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_op_removes_cl: - "classes_of (arden_op Y yrhs) = classes_of yrhs - {Y}" -apply (simp add:arden_op_def append_rhs_keeps_cls trns_of_def) +lemma Arden_removes_cl: + "classes_of (Arden Y yrhs) = classes_of yrhs - {Y}" +apply (simp add:Arden_def append_rhs_keeps_cls) by (auto simp:classes_of_def) lemma lefts_of_keeps_cls: - "lefts_of (subst_op_all ES Y yrhs) = lefts_of ES" -by (auto simp:lefts_of_def subst_op_all_def) + "lefts_of (Subst_all ES Y yrhs) = lefts_of ES" +by (auto simp:lefts_of_def Subst_all_def) -lemma subst_op_updates_cls: +lemma Subst_updates_cls: "X \ classes_of xrhs \ - classes_of (subst_op rhs X xrhs) = classes_of rhs \ classes_of xrhs - {X}" -apply (simp only:subst_op_def append_rhs_keeps_cls + 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[THEN sym]) -by (auto simp:classes_of_def trns_of_def) +by (auto simp:classes_of_def) -lemma subst_op_all_keeps_self_contained: +lemma Subst_all_keeps_self_contained: fixes Y assumes sc: "self_contained (ES \ {(Y, yrhs)})" (is "self_contained ?A") - shows "self_contained (subst_op_all ES Y (arden_op Y yrhs))" + shows "self_contained (Subst_all ES Y (Arden Y yrhs))" (is "self_contained ?B") proof- { fix X xrhs' assume "(X, xrhs') \ ?B" then obtain xrhs - where xrhs_xrhs': "xrhs' = subst_op xrhs Y (arden_op Y yrhs)" - and X_in: "(X, xrhs) \ ES" by (simp add:subst_op_all_def, blast) + 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" proof- - have "lefts_of ?B = lefts_of ES" by (auto simp add:lefts_of_def subst_op_all_def) + 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" proof- have "classes_of xrhs' \ - classes_of xrhs \ classes_of (arden_op Y yrhs) - {Y}" + classes_of xrhs \ classes_of (Arden Y yrhs) - {Y}" proof- - have "Y \ classes_of (arden_op Y yrhs)" - using arden_op_removes_cl by simp - thus ?thesis using xrhs_xrhs' by (auto simp:subst_op_updates_cls) + have "Y \ classes_of (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 \ lefts_of ES \ {Y}" using X_in sc apply (simp only:self_contained_def lefts_of_union_distrib[THEN sym]) by (drule_tac x = "(X, xrhs)" in bspec, auto simp:lefts_of_def) - moreover have "classes_of (arden_op Y yrhs) \ lefts_of ES \ {Y}" + moreover have "classes_of (Arden Y yrhs) \ lefts_of ES \ {Y}" using sc - by (auto simp add:arden_op_removes_cl self_contained_def lefts_of_def) + by (auto simp add:Arden_removes_cl self_contained_def lefts_of_def) ultimately show ?thesis by auto qed ultimately show ?thesis by simp qed - } thus ?thesis by (auto simp only:subst_op_all_def self_contained_def) + } thus ?thesis by (auto simp only:Subst_all_def self_contained_def) qed -lemma subst_op_all_satisfy_invariant: +lemma Subst_all_satisfy_invariant: assumes invariant_ES: "invariant (ES \ {(Y, yrhs)})" - shows "invariant (subst_op_all ES Y (arden_op Y yrhs))" + shows "invariant (Subst_all ES Y (Arden Y yrhs))" proof - have finite_yrhs: "finite yrhs" using invariant_ES by (auto simp:invariant_def finite_rhs_def) @@ -935,66 +956,66 @@ using invariant_ES by (auto simp:invariant_def ardenable_def) have Y_eq_yrhs: "Y = L yrhs" using invariant_ES by (simp only:invariant_def valid_eqns_def, blast) - have "distinct_equas (subst_op_all ES Y (arden_op Y yrhs))" + have "distinct_equas (Subst_all ES Y (Arden Y yrhs))" using invariant_ES - by (auto simp:distinct_equas_def subst_op_all_def invariant_def) - moreover have "finite (subst_op_all ES Y (arden_op Y yrhs))" - using invariant_ES by (simp add:invariant_def subst_op_all_keeps_finite) - moreover have "finite_rhs (subst_op_all ES Y (arden_op Y yrhs))" + by (auto simp:distinct_equas_def Subst_all_def invariant_def) + moreover have "finite (Subst_all ES Y (Arden Y yrhs))" + using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite) + moreover have "finite_rhs (Subst_all ES Y (Arden Y yrhs))" proof- have "finite_rhs ES" using invariant_ES by (simp add:invariant_def finite_rhs_def) - moreover have "finite (arden_op Y yrhs)" + moreover have "finite (Arden Y yrhs)" proof - have "finite yrhs" using invariant_ES by (auto simp:invariant_def finite_rhs_def) - thus ?thesis using arden_op_keeps_finite by simp + thus ?thesis using Arden_keeps_finite by simp qed ultimately show ?thesis - by (simp add:subst_op_all_keeps_finite_rhs) + by (simp add:Subst_all_keeps_finite_rhs) qed - moreover have "ardenable (subst_op_all ES Y (arden_op Y yrhs))" + moreover have "ardenable (Subst_all ES Y (Arden Y yrhs))" proof - { fix X rhs assume "(X, rhs) \ ES" hence "rhs_nonempty rhs" using prems invariant_ES by (simp add:invariant_def ardenable_def) with nonempty_yrhs - have "rhs_nonempty (subst_op rhs Y (arden_op Y yrhs))" + have "rhs_nonempty (Subst rhs Y (Arden Y yrhs))" by (simp add:nonempty_yrhs - subst_op_keeps_nonempty arden_op_keeps_nonempty) - } thus ?thesis by (auto simp add:ardenable_def subst_op_all_def) + Subst_keeps_nonempty Arden_keeps_nonempty) + } thus ?thesis by (auto simp add:ardenable_def Subst_all_def) qed - moreover have "valid_eqns (subst_op_all ES Y (arden_op Y yrhs))" + moreover have "valid_eqns (Subst_all ES Y (Arden Y yrhs))" proof- - have "Y = L (arden_op Y yrhs)" + have "Y = L (Arden Y yrhs)" using Y_eq_yrhs invariant_ES finite_yrhs nonempty_yrhs - by (rule_tac arden_op_keeps_eq, (simp add:rexp_of_empty)+) + by (rule_tac Arden_keeps_eq, (simp add:rexp_of_empty)+) thus ?thesis using invariant_ES by (clarsimp simp add:valid_eqns_def - subst_op_all_def subst_op_keeps_eq invariant_def finite_rhs_def + Subst_all_def Subst_keeps_eq invariant_def finite_rhs_def simp del:L_rhs.simps) qed moreover - have self_subst: "self_contained (subst_op_all ES Y (arden_op Y yrhs))" - using invariant_ES subst_op_all_keeps_self_contained by (simp add:invariant_def) + have self_subst: "self_contained (Subst_all ES Y (Arden Y yrhs))" + using invariant_ES Subst_all_keeps_self_contained by (simp add:invariant_def) ultimately show ?thesis using invariant_ES by (simp add:invariant_def) qed -lemma subst_op_all_card_le: +lemma Subst_all_card_le: assumes finite: "finite (ES::(string set \ rhs_item set) set)" - shows "card (subst_op_all ES Y yrhs) <= card ES" + shows "card (Subst_all ES Y yrhs) <= card ES" proof- - def f \ "\ x. ((fst x)::string set, subst_op (snd x) Y yrhs)" - have "subst_op_all ES Y yrhs = f ` ES" - apply (auto simp:subst_op_all_def f_def image_def) + def f \ "\ x. ((fst x)::string set, Subst (snd x) Y yrhs)" + have "Subst_all ES Y yrhs = f ` ES" + apply (auto simp:Subst_all_def f_def image_def) by (rule_tac x = "(Ya, yrhsa)" in bexI, simp+) thus ?thesis using finite by (auto intro:card_image_le) qed -lemma subst_op_all_cls_remains: - "(X, xrhs) \ ES \ \ xrhs'. (X, xrhs') \ (subst_op_all ES Y yrhs)" -by (auto simp:subst_op_all_def) +lemma Subst_all_cls_remains: + "(X, xrhs) \ ES \ \ xrhs'. (X, xrhs') \ (Subst_all ES Y yrhs)" +by (auto simp:Subst_all_def) lemma card_noteq_1_has_more: assumes card:"card S \ 1" @@ -1031,35 +1052,35 @@ by (auto simp: invariant_def distinct_equas_def) next fix x - let ?ES' = "let (Y, yrhs) = x in subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)" + let ?ES' = "let (Y, yrhs) = x in Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)" assume prem: "case x of (Y, yrhs) \ (Y, yrhs) \ ES \ (X \ Y)" thus "invariant (?ES') \ (\xrhs'. (X, xrhs') \ ?ES') \ (?ES', ES) \ measure card" proof(cases "x", simp) fix Y yrhs assume h: "(Y, yrhs) \ ES \ X \ Y" - show "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \ - (\xrhs'. (X, xrhs') \ subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \ - card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES" + show "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \ + (\xrhs'. (X, xrhs') \ Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \ + card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES" proof - - have "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))" - proof(rule subst_op_all_satisfy_invariant) + have "invariant (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))" + proof(rule Subst_all_satisfy_invariant) from h have "(Y, yrhs) \ ES" by simp hence "ES - {(Y, yrhs)} \ {(Y, yrhs)} = ES" by auto with Inv_ES show "invariant (ES - {(Y, yrhs)} \ {(Y, yrhs)})" by auto qed moreover have - "(\xrhs'. (X, xrhs') \ subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))" - proof(rule subst_op_all_cls_remains) + "(\xrhs'. (X, xrhs') \ Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs))" + proof(rule Subst_all_cls_remains) from X_in_ES and h show "(X, xrhs) \ ES - {(Y, yrhs)}" by auto qed moreover have - "card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES" + "card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) < card ES" proof(rule le_less_trans) show - "card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \ + "card (Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)) \ card (ES - {(Y, yrhs)})" - proof(rule subst_op_all_card_le) + proof(rule Subst_all_card_le) show "finite (ES - {(Y, yrhs)})" using finite_ES by auto qed next @@ -1067,7 +1088,7 @@ by (auto simp:card_gt_0_iff intro:diff_Suc_less) qed ultimately show ?thesis - by (auto dest: subst_op_all_card_le elim:le_less_trans) + by (auto dest: Subst_all_card_le elim:le_less_trans) qed qed qed @@ -1126,7 +1147,7 @@ assumes Inv_ES: "invariant {(X, xrhs)}" shows "\ (r::rexp). L r = X" (is "\ r. ?P r") proof- - def A \ "arden_op X xrhs" + def A \ "Arden X xrhs" have "?P (\{r. Lam r \ A})" proof - have "L (\{r. Lam r \ A}) = L ({Lam r | r. Lam r \ A})" @@ -1134,7 +1155,7 @@ show "finite A" unfolding A_def using Inv_ES - by (rule_tac arden_op_keeps_finite) + by (rule_tac Arden_keeps_finite) (auto simp add: invariant_def finite_rhs_def) qed also have "\ = L A" @@ -1143,7 +1164,7 @@ proof- have "classes_of A = {}" using Inv_ES unfolding A_def - by (simp add:arden_op_removes_cl + by (simp add:Arden_removes_cl self_contained_def invariant_def lefts_of_def) thus ?thesis unfolding A_def @@ -1153,7 +1174,7 @@ qed also have "\ = X" unfolding A_def - proof(rule arden_op_keeps_eq [THEN sym]) + proof(rule Arden_keeps_eq [THEN sym]) show "X = L xrhs" using Inv_ES by (auto simp only: invariant_def valid_eqns_def) next