509 qed |
509 qed |
510 hence "th' \<in> ?L" by auto |
510 hence "th' \<in> ?L" by auto |
511 } ultimately show ?thesis by blast |
511 } ultimately show ?thesis by blast |
512 qed |
512 qed |
513 |
513 |
|
514 (* |
514 lemma image_eq: |
515 lemma image_eq: |
515 assumes "A = B" |
516 assumes "A = B" |
516 shows "f ` A = f ` B" |
517 shows "f ` A = f ` B" |
517 using assms by auto |
518 using assms by auto |
|
519 *) |
518 |
520 |
519 lemma tRAG_trancl_eq_Th: |
521 lemma tRAG_trancl_eq_Th: |
520 "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = |
522 "{Th th' | th'. (Th th', Th th) \<in> (tRAG s)^+} = |
521 {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" |
523 {Th th' | th'. (Th th', Th th) \<in> (RAG s)^+}" |
522 using tRAG_trancl_eq by auto |
524 using tRAG_trancl_eq by auto |
905 next |
907 next |
906 show "PIP s e" using Step by simp |
908 show "PIP s e" using Step by simp |
907 qed |
909 qed |
908 qed |
910 qed |
909 |
911 |
910 text {* |
|
911 The following lemma says that if @{text "s"} is a valid state, so |
|
912 is its any postfix. Where @{term "monent t s"} is the postfix of |
|
913 @{term "s"} with length @{term "t"}. |
|
914 *} |
|
915 lemma vt_moment: "\<And> t. vt (moment t s)" |
|
916 proof(induct rule:ind) |
|
917 case Nil |
|
918 thus ?case by (simp add:vt_nil) |
|
919 next |
|
920 case (Cons s e t) |
|
921 show ?case |
|
922 proof(cases "t \<ge> length (e#s)") |
|
923 case True |
|
924 from True have "moment t (e#s) = e#s" by simp |
|
925 thus ?thesis using Cons |
|
926 by (simp add:valid_trace_def valid_trace_e_def, auto) |
|
927 next |
|
928 case False |
|
929 from Cons have "vt (moment t s)" by simp |
|
930 moreover have "moment t (e#s) = moment t s" |
|
931 proof - |
|
932 from False have "t \<le> length s" by simp |
|
933 from moment_app [OF this, of "[e]"] |
|
934 show ?thesis by simp |
|
935 qed |
|
936 ultimately show ?thesis by simp |
|
937 qed |
|
938 qed |
|
939 |
|
940 text {* |
|
941 The following two lemmas are fundamental, because they assure |
|
942 that the numbers of both living and ready threads are finite. |
|
943 *} |
|
944 |
912 |
945 lemma finite_threads: |
913 lemma finite_threads: |
946 shows "finite (threads s)" |
914 shows "finite (threads s)" |
947 using vt by (induct) (auto elim: step.cases) |
915 using vt by (induct) (auto elim: step.cases) |
948 |
916 |
949 lemma finite_readys: "finite (readys s)" |
917 lemma finite_readys: "finite (readys s)" |
950 using finite_threads readys_threads rev_finite_subset by blast |
918 using finite_threads readys_threads rev_finite_subset by blast |
951 |
919 |
952 end |
920 end |
953 |
921 |
954 text {* |
|
955 The following locale @{text "valid_moment"} is to inherit the properties |
|
956 derived on any valid state to the prefix of it, with length @{text "i"}. |
|
957 *} |
|
958 locale valid_moment = valid_trace + |
|
959 fixes i :: nat |
|
960 |
|
961 sublocale valid_moment < vat_moment: valid_trace "(moment i s)" |
|
962 by (unfold_locales, insert vt_moment, auto) |
|
963 |
|
964 locale valid_moment_e = valid_moment + |
|
965 assumes less_i: "i < length s" |
|
966 begin |
|
967 definition "next_e = hd (moment (Suc i) s)" |
|
968 |
|
969 lemma trace_e: |
|
970 "moment (Suc i) s = next_e#moment i s" |
|
971 proof - |
|
972 from less_i have "Suc i \<le> length s" by auto |
|
973 from moment_plus[OF this, folded next_e_def] |
|
974 show ?thesis . |
|
975 qed |
|
976 |
|
977 end |
|
978 |
|
979 sublocale valid_moment_e < vat_moment_e: valid_trace_e "moment i s" "next_e" |
|
980 using vt_moment[of "Suc i", unfolded trace_e] |
|
981 by (unfold_locales, simp) |
|
982 |
922 |
983 section {* Waiting queues are distinct *} |
923 section {* Waiting queues are distinct *} |
984 |
924 |
985 text {* |
925 text {* |
986 This section proves that every waiting queue in the system |
926 This section proves that every waiting queue in the system |
1383 with threads_kept show ?thesis by simp |
1323 with threads_kept show ?thesis by simp |
1384 qed |
1324 qed |
1385 |
1325 |
1386 end |
1326 end |
1387 |
1327 |
|
1328 context valid_trace |
|
1329 begin |
|
1330 |
1388 text {* |
1331 text {* |
1389 The is the main lemma of this section, which is derived |
1332 The is the main lemma of this section, which is derived |
1390 by induction, case analysis on event @{text e} and |
1333 by induction, case analysis on event @{text e} and |
1391 assembling the @{text "wq_threads_kept"}-results of |
1334 assembling the @{text "wq_threads_kept"}-results of |
1392 all possible cases of @{text "e"}. |
1335 all possible cases of @{text "e"}. |
1393 *} |
1336 *} |
1394 lemma (in valid_trace) wq_threads: |
1337 lemma wq_threads: |
1395 assumes "th \<in> set (wq s cs)" |
1338 assumes "th \<in> set (wq s cs)" |
1396 shows "th \<in> threads s" |
1339 shows "th \<in> threads s" |
1397 using assms |
1340 using assms |
1398 proof(induct arbitrary:th cs rule:ind) |
1341 proof(induct arbitrary:th cs rule:ind) |
1399 case (Nil) |
1342 case (Nil) |
1867 |
1808 |
1868 lemma RAG_es: |
1809 lemma RAG_es: |
1869 "RAG (e # s) = |
1810 "RAG (e # s) = |
1870 RAG s - {(Cs cs, Th th)} - |
1811 RAG s - {(Cs cs, Th th)} - |
1871 {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> |
1812 {(Th th', Cs cs) |th'. next_th s th cs th'} \<union> |
1872 {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R") |
1813 {(Cs cs, Th th') |th'. next_th s th cs th'}" (is "?L = ?R") |
1873 proof(rule rel_eqI) |
1814 proof(rule rel_eqI) |
1874 fix n1 n2 |
1815 fix n1 n2 |
1875 assume "(n1, n2) \<in> ?L" |
1816 assume "(n1, n2) \<in> ?L" |
1876 thus "(n1, n2) \<in> ?R" |
1817 thus "(n1, n2) \<in> ?R" |
1877 proof(cases rule:in_RAG_E) |
1818 proof(cases rule:in_RAG_E) |
3206 from rpath_dest_eq[OF rp1 rp2[unfolded this]] |
3147 from rpath_dest_eq[OF rp1 rp2[unfolded this]] |
3207 show ?thesis by simp |
3148 show ?thesis by simp |
3208 qed |
3149 qed |
3209 qed |
3150 qed |
3210 |
3151 |
3211 lemma card_running: "card (running s) \<le> 1" |
3152 lemma card_running: |
|
3153 shows "card (running s) \<le> 1" |
3212 proof(cases "running s = {}") |
3154 proof(cases "running s = {}") |
3213 case True |
3155 case True |
3214 thus ?thesis by auto |
3156 thus ?thesis by auto |
3215 next |
3157 next |
3216 case False |
3158 case False |
3217 then obtain th where [simp]: "th \<in> running s" by auto |
3159 then obtain th where "th \<in> running s" by auto |
3218 from running_unique[OF this] |
3160 with running_unique |
3219 have "running s = {th}" by auto |
3161 have "running s = {th}" by auto |
3220 thus ?thesis by auto |
3162 thus ?thesis by auto |
3221 qed |
3163 qed |
3222 |
3164 |
3223 text {* |
3165 text {* |