440 |
440 |
441 definition |
441 definition |
442 "subst_op_all ES X xrhs \<equiv> {(Y, subst_op yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}" |
442 "subst_op_all ES X xrhs \<equiv> {(Y, subst_op yrhs X xrhs) | Y yrhs. (Y, yrhs) \<in> ES}" |
443 |
443 |
444 |
444 |
445 section {* Well-founded iteration *} |
445 section {* While-combinator *} |
446 |
446 |
447 text {* |
447 text {* |
448 The computation of regular expressions for equivalence classes is accomplished |
448 The following term @{text "remove ES Y yrhs"} removes the equation |
449 using a iteration principle given by the following lemma. |
449 @{text "Y = yrhs"} from equational system @{text "ES"} by replacing |
450 *} |
450 all occurences of @{text "Y"} by its definition (using @{text "eqs_subst"}). |
451 |
451 The @{text "Y"}-definition is made non-recursive using Arden's transformation |
452 lemma wf_iter [rule_format]: |
452 @{text "arden_variate Y yrhs"}. |
453 fixes f |
453 *} |
454 assumes step: "\<And> e. \<lbrakk>P e; \<not> Q e\<rbrakk> \<Longrightarrow> (\<exists> e'. P e' \<and> (f(e'), f(e)) \<in> less_than)" |
454 |
455 shows pe: "P e \<longrightarrow> (\<exists> e'. P e' \<and> Q e')" |
455 definition |
456 proof(induct e rule: wf_induct |
456 "remove_op ES Y yrhs \<equiv> |
457 [OF wf_inv_image[OF wf_less_than, where f = "f"]], clarify) |
457 subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)" |
458 fix x |
458 |
459 assume h [rule_format]: |
459 text {* |
460 "\<forall>y. (y, x) \<in> inv_image less_than f \<longrightarrow> P y \<longrightarrow> (\<exists>e'. P e' \<and> Q e')" |
460 The following term @{text "iterm X ES"} represents one iteration in the while loop. |
461 and px: "P x" |
461 It arbitrarily chooses a @{text "Y"} different from @{text "X"} to remove. |
462 show "\<exists>e'. P e' \<and> Q e'" |
462 *} |
463 proof(cases "Q x") |
463 |
464 assume "Q x" with px show ?thesis by blast |
464 definition |
465 next |
465 "iter X ES \<equiv> (let (Y, yrhs) = SOME (Y, yrhs). (Y, yrhs) \<in> ES \<and> (X \<noteq> Y) |
466 assume nq: "\<not> Q x" |
466 in remove_op ES Y yrhs)" |
467 from step [OF px nq] |
467 |
468 obtain e' where pe': "P e'" and ltf: "(f e', f x) \<in> less_than" by auto |
468 text {* |
469 show ?thesis |
469 The following term @{text "reduce X ES"} repeatedly removes characteriztion equations |
470 proof(rule h) |
470 for unknowns other than @{text "X"} until one is left. |
471 from ltf show "(e', x) \<in> inv_image less_than f" |
471 *} |
472 by (simp add:inv_image_def) |
472 |
473 next |
473 definition |
474 from pe' show "P e'" . |
474 "reduce X ES \<equiv> while (\<lambda> ES. card ES \<noteq> 1) (iter X) ES" |
475 qed |
475 |
476 qed |
476 text {* |
477 qed |
477 Since the @{text "while"} combinator from HOL library is used to implement @{text "reduce X ES"}, |
478 |
478 the induction principle @{thm [source] while_rule} is used to proved the desired properties |
479 text {* |
479 of @{text "reduce X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined |
480 The @{text "P"} in lemma @{text "wf_iter"} is an invariant kept throughout the iteration procedure. |
480 in terms of a series of auxilliary predicates: |
481 The particular invariant used to solve our problem is defined by function @{text "Inv(ES)"}, |
481 *} |
482 an invariant over equal system @{text "ES"}. |
|
483 Every definition starting next till @{text "Inv"} stipulates a property to be satisfied by @{text "ES"}. |
|
484 *} |
|
485 |
|
486 |
482 |
487 section {* Invariants *} |
483 section {* Invariants *} |
488 |
484 |
489 text {* Every variable is defined at most onece in @{text ES}. *} |
485 text {* Every variable is defined at most onece in @{text ES}. *} |
490 |
486 |
1017 qed |
1010 qed |
1018 hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp) |
1011 hence "S - {e} \<noteq> {}" using finite by (rule_tac notI, simp) |
1019 thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto |
1012 thus "(\<And>e'. e' \<in> S \<and> e \<noteq> e' \<Longrightarrow> thesis) \<Longrightarrow> thesis" by auto |
1020 qed |
1013 qed |
1021 |
1014 |
1022 lemma iteration_step: |
1015 lemma iteration_step: |
1023 assumes invariant_ES: "invariant ES" |
1016 assumes Inv_ES: "invariant ES" |
1024 and X_in_ES: "(X, xrhs) \<in> ES" |
1017 and X_in_ES: "(X, xrhs) \<in> ES" |
1025 and not_T: "card ES \<noteq> 1" |
1018 and not_T: "card ES \<noteq> 1" |
1026 shows "\<exists> ES'. (invariant ES' \<and> (\<exists> xrhs'.(X, xrhs') \<in> ES')) \<and> |
1019 shows "(invariant (iter X ES) \<and> (\<exists> xrhs'.(X, xrhs') \<in> (iter X ES)) \<and> |
1027 (card ES', card ES) \<in> less_than" (is "\<exists> ES'. ?P ES'") |
1020 (iter X ES, ES) \<in> measure card)" |
1028 proof - |
1021 proof - |
1029 have finite_ES: "finite ES" using invariant_ES by (simp add:invariant_def) |
1022 have finite_ES: "finite ES" using Inv_ES by (simp add: invariant_def) |
1030 then obtain Y yrhs |
1023 then obtain Y yrhs |
1031 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1024 where Y_in_ES: "(Y, yrhs) \<in> ES" and not_eq: "(X, xrhs) \<noteq> (Y, yrhs)" |
1032 using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto) |
1025 using not_T X_in_ES by (drule_tac card_noteq_1_has_more, auto) |
1033 def ES' == "ES - {(Y, yrhs)}" |
1026 let ?ES' = "iter X ES" |
1034 let ?ES'' = "subst_op_all ES' Y (arden_op Y yrhs)" |
1027 show ?thesis |
1035 have "?P ?ES''" |
1028 proof(unfold iter_def remove_op_def, rule someI2 [where a = "(Y, yrhs)"], clarsimp) |
1036 proof - |
1029 from X_in_ES Y_in_ES and not_eq and Inv_ES |
1037 have "invariant ?ES''" using Y_in_ES invariant_ES |
1030 show "(Y, yrhs) \<in> ES \<and> X \<noteq> Y" |
1038 by (rule_tac subst_op_all_satisfy_invariant, simp add:ES'_def insert_absorb) |
1031 by (auto simp: invariant_def distinct_equas_def) |
1039 moreover have "\<exists>xrhs'. (X, xrhs') \<in> ?ES''" using not_eq X_in_ES |
1032 next |
1040 by (rule_tac ES = ES' in subst_op_all_cls_remains, auto simp add:ES'_def) |
1033 fix x |
1041 moreover have "(card ?ES'', card ES) \<in> less_than" |
1034 let ?ES' = "let (Y, yrhs) = x in subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)" |
1042 proof - |
1035 assume prem: "case x of (Y, yrhs) \<Rightarrow> (Y, yrhs) \<in> ES \<and> (X \<noteq> Y)" |
1043 have "finite ES'" using finite_ES ES'_def by auto |
1036 thus "invariant (?ES') \<and> (\<exists>xrhs'. (X, xrhs') \<in> ?ES') \<and> (?ES', ES) \<in> measure card" |
1044 moreover have "card ES' < card ES" using finite_ES Y_in_ES |
1037 proof(cases "x", simp) |
1045 by (auto simp:ES'_def card_gt_0_iff intro:diff_Suc_less) |
1038 fix Y yrhs |
1046 ultimately show ?thesis |
1039 assume h: "(Y, yrhs) \<in> ES \<and> X \<noteq> Y" |
1047 by (auto dest:subst_op_all_card_le elim:le_less_trans) |
1040 show "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<and> |
|
1041 (\<exists>xrhs'. (X, xrhs') \<in> subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<and> |
|
1042 card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES" |
|
1043 proof - |
|
1044 have "invariant (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))" |
|
1045 proof(rule subst_op_all_satisfy_invariant) |
|
1046 from h have "(Y, yrhs) \<in> ES" by simp |
|
1047 hence "ES - {(Y, yrhs)} \<union> {(Y, yrhs)} = ES" by auto |
|
1048 with Inv_ES show "invariant (ES - {(Y, yrhs)} \<union> {(Y, yrhs)})" by auto |
|
1049 qed |
|
1050 moreover have |
|
1051 "(\<exists>xrhs'. (X, xrhs') \<in> subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs))" |
|
1052 proof(rule subst_op_all_cls_remains) |
|
1053 from X_in_ES and h |
|
1054 show "(X, xrhs) \<in> ES - {(Y, yrhs)}" by auto |
|
1055 qed |
|
1056 moreover have |
|
1057 "card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) < card ES" |
|
1058 proof(rule le_less_trans) |
|
1059 show |
|
1060 "card (subst_op_all (ES - {(Y, yrhs)}) Y (arden_op Y yrhs)) \<le> |
|
1061 card (ES - {(Y, yrhs)})" |
|
1062 proof(rule subst_op_all_card_le) |
|
1063 show "finite (ES - {(Y, yrhs)})" using finite_ES by auto |
|
1064 qed |
|
1065 next |
|
1066 show "card (ES - {(Y, yrhs)}) < card ES" using finite_ES h |
|
1067 by (auto simp:card_gt_0_iff intro:diff_Suc_less) |
|
1068 qed |
|
1069 ultimately show ?thesis |
|
1070 by (auto dest: subst_op_all_card_le elim:le_less_trans) |
|
1071 qed |
1048 qed |
1072 qed |
1049 ultimately show ?thesis by simp |
|
1050 qed |
1073 qed |
1051 thus ?thesis by blast |
1074 qed |
1052 qed |
1075 |
1053 |
1076 |
1054 subsubsection {* |
1077 subsubsection {* Conclusion of the proof *} |
1055 Conclusion of the proof |
|
1056 *} |
|
1057 |
1078 |
1058 text {* |
1079 text {* |
1059 From this point until @{text "hard_direction"}, the hard direction is proved |
1080 From this point until @{text "hard_direction"}, the hard direction is proved |
1060 through a simple application of the iteration principle. |
1081 through a simple application of the iteration principle. |
1061 *} |
1082 *} |
1062 |
1083 |
1063 lemma iteration_conc: |
1084 lemma reduce_x: |
1064 assumes history: "invariant ES" |
1085 assumes inv: "invariant ES" |
1065 and X_in_ES: "\<exists> xrhs. (X, xrhs) \<in> ES" |
1086 and contain_x: "(X, xrhs) \<in> ES" |
1066 shows |
1087 shows "\<exists> xrhs'. reduce X ES = {(X, xrhs')} \<and> invariant(reduce X ES)" |
1067 "\<exists> ES'. (invariant ES' \<and> (\<exists> xrhs'. (X, xrhs') \<in> ES')) \<and> card ES' = 1" |
1088 proof - |
1068 (is "\<exists> ES'. ?P ES'") |
1089 let ?Inv = "\<lambda> ES. (invariant ES \<and> (\<exists> xrhs. (X, xrhs) \<in> ES))" |
1069 proof (cases "card ES = 1") |
1090 show ?thesis |
1070 case True |
1091 proof (unfold reduce_def, |
1071 thus ?thesis using history X_in_ES |
1092 rule while_rule [where P = ?Inv and r = "measure card"]) |
1072 by blast |
1093 from inv and contain_x show "?Inv ES" by auto |
1073 next |
1094 next |
1074 case False |
1095 show "wf (measure card)" by simp |
1075 thus ?thesis using history iteration_step X_in_ES |
1096 next |
1076 by (rule_tac f = card in wf_iter, auto) |
1097 fix ES |
1077 qed |
1098 assume inv: "?Inv ES" and crd: "card ES \<noteq> 1" |
1078 |
1099 show "(iter X ES, ES) \<in> measure card" |
|
1100 proof - |
|
1101 from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto |
|
1102 from inv have "invariant ES" by simp |
|
1103 from iteration_step [OF this x_in crd] |
|
1104 show ?thesis by auto |
|
1105 qed |
|
1106 next |
|
1107 fix ES |
|
1108 assume inv: "?Inv ES" and crd: "card ES \<noteq> 1" |
|
1109 thus "?Inv (iter X ES)" |
|
1110 proof - |
|
1111 from inv obtain xrhs where x_in: "(X, xrhs) \<in> ES" by auto |
|
1112 from inv have "invariant ES" by simp |
|
1113 from iteration_step [OF this x_in crd] |
|
1114 show ?thesis by auto |
|
1115 qed |
|
1116 next |
|
1117 fix ES |
|
1118 assume "?Inv ES" and "\<not> card ES \<noteq> 1" |
|
1119 thus "\<exists>xrhs'. ES = {(X, xrhs')} \<and> invariant ES" |
|
1120 apply (auto, rule_tac x = xrhs in exI) |
|
1121 by (auto simp: invariant_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) |
|
1122 qed |
|
1123 qed |
|
1124 |
1079 lemma last_cl_exists_rexp: |
1125 lemma last_cl_exists_rexp: |
1080 assumes ES_single: "ES = {(X, xrhs)}" |
1126 assumes Inv_ES: "invariant {(X, xrhs)}" |
1081 and invariant_ES: "invariant ES" |
|
1082 shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r") |
1127 shows "\<exists> (r::rexp). L r = X" (is "\<exists> r. ?P r") |
1083 proof- |
1128 proof- |
1084 def A \<equiv> "arden_op X xrhs" |
1129 def A \<equiv> "arden_op X xrhs" |
1085 have "?P (\<Uplus>{r. Lam r \<in> A})" |
1130 have "?P (\<Uplus>{r. Lam r \<in> A})" |
1086 proof - |
1131 proof - |
1087 have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})" |
1132 have "L (\<Uplus>{r. Lam r \<in> A}) = L ({Lam r | r. Lam r \<in> A})" |
1088 proof(rule rexp_of_lam_eq_lam_set) |
1133 proof(rule rexp_of_lam_eq_lam_set) |
1089 show "finite A" |
1134 show "finite A" |
1090 unfolding A_def |
1135 unfolding A_def |
1091 using invariant_ES ES_single |
1136 using Inv_ES |
1092 by (rule_tac arden_op_keeps_finite) |
1137 by (rule_tac arden_op_keeps_finite) |
1093 (auto simp add: invariant_def finite_rhs_def) |
1138 (auto simp add: invariant_def finite_rhs_def) |
1094 qed |
1139 qed |
1095 also have "\<dots> = L A" |
1140 also have "\<dots> = L A" |
1096 proof- |
1141 proof- |
1097 have "{Lam r | r. Lam r \<in> A} = A" |
1142 have "{Lam r | r. Lam r \<in> A} = A" |
1098 proof- |
1143 proof- |
1099 have "classes_of A = {}" using invariant_ES ES_single |
1144 have "classes_of A = {}" using Inv_ES |
1100 unfolding A_def |
1145 unfolding A_def |
1101 by (simp add:arden_op_removes_cl |
1146 by (simp add:arden_op_removes_cl |
1102 self_contained_def invariant_def lefts_of_def) |
1147 self_contained_def invariant_def lefts_of_def) |
1103 thus ?thesis |
1148 thus ?thesis |
1104 unfolding A_def |
1149 unfolding A_def |
1107 thus ?thesis by simp |
1152 thus ?thesis by simp |
1108 qed |
1153 qed |
1109 also have "\<dots> = X" |
1154 also have "\<dots> = X" |
1110 unfolding A_def |
1155 unfolding A_def |
1111 proof(rule arden_op_keeps_eq [THEN sym]) |
1156 proof(rule arden_op_keeps_eq [THEN sym]) |
1112 show "X = L xrhs" using invariant_ES ES_single |
1157 show "X = L xrhs" using Inv_ES |
1113 by (auto simp only:invariant_def valid_eqns_def) |
1158 by (auto simp only: invariant_def valid_eqns_def) |
1114 next |
1159 next |
1115 from invariant_ES ES_single show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})" |
1160 from Inv_ES show "[] \<notin> L (\<Uplus>{r. Trn X r \<in> xrhs})" |
1116 by(simp add:invariant_def ardenable_def rexp_of_empty finite_rhs_def) |
1161 by(simp add: invariant_def ardenable_def rexp_of_empty finite_rhs_def) |
1117 next |
1162 next |
1118 from invariant_ES ES_single show "finite xrhs" |
1163 from Inv_ES show "finite xrhs" |
1119 by (simp add:invariant_def finite_rhs_def) |
1164 by (simp add: invariant_def finite_rhs_def) |
1120 qed |
1165 qed |
1121 finally show ?thesis by simp |
1166 finally show ?thesis by simp |
1122 qed |
1167 qed |
1123 thus ?thesis by auto |
1168 thus ?thesis by auto |
1124 qed |
1169 qed |
1125 |
1170 |
1126 lemma every_eqcl_has_reg: |
1171 lemma every_eqcl_has_reg: |
1127 assumes finite_CS: "finite (UNIV // (\<approx>Lang))" |
1172 assumes finite_CS: "finite (UNIV // (\<approx>Lang))" |
1128 and X_in_CS: "X \<in> (UNIV // (\<approx>Lang))" |
1173 and X_in_CS: "X \<in> (UNIV // (\<approx>Lang))" |
1129 shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r") |
1174 shows "\<exists> (reg::rexp). L reg = X" (is "\<exists> r. ?E r") |
1130 proof - |
1175 proof - |
1131 from X_in_CS have "\<exists> xrhs. (X, xrhs) \<in> (eqs (UNIV // (\<approx>Lang)))" |
1176 let ?ES = " eqs (UNIV // \<approx>Lang)" |
|
1177 from X_in_CS |
|
1178 obtain xrhs where "(X, xrhs) \<in> ?ES" |
1132 by (auto simp:eqs_def init_rhs_def) |
1179 by (auto simp:eqs_def init_rhs_def) |
1133 then obtain ES xrhs where invariant_ES: "invariant ES" |
1180 from reduce_x [OF init_ES_satisfy_invariant [OF finite_CS] this] |
1134 and X_in_ES: "(X, xrhs) \<in> ES" |
1181 have "\<exists>xrhs'. reduce X ?ES = {(X, xrhs')} \<and> invariant (reduce X ?ES)" . |
1135 and card_ES: "card ES = 1" |
1182 then obtain xrhs' where "invariant {(X, xrhs')}" by auto |
1136 using finite_CS X_in_CS init_ES_satisfy_invariant iteration_conc |
1183 from last_cl_exists_rexp [OF this] |
1137 by blast |
1184 show ?thesis . |
1138 hence ES_single_equa: "ES = {(X, xrhs)}" |
1185 qed |
1139 by (auto simp:invariant_def dest!:card_Suc_Diff1 simp:card_eq_0_iff) |
1186 |
1140 thus ?thesis using invariant_ES |
|
1141 by (rule last_cl_exists_rexp) |
|
1142 qed |
|
1143 |
1187 |
1144 theorem hard_direction: |
1188 theorem hard_direction: |
1145 assumes finite_CS: "finite (UNIV // \<approx>A)" |
1189 assumes finite_CS: "finite (UNIV // \<approx>A)" |
1146 shows "\<exists>r::rexp. A = L r" |
1190 shows "\<exists>r::rexp. A = L r" |
1147 proof - |
1191 proof - |