325   It is a major technical in this development to use 

   325   It is part of the scheme to use the counting 

   326   the counter of @{term "P"} and @{term "V"} (* ccc *)

   326   of @{term "P"} and @{term "V"} operations to reason about

   327   the number of resources occupied by one thread.

   692 section {* Distinctiveness of waiting queues *}

   697 section {* Waiting queues are distinct *}

   693 

   698 

   694 lemma (in valid_trace) finite_threads:

   699 text {*

   695   shows "finite (threads s)"

   700   This section proofs that every waiting queue in the system

   696   using vt by (induct) (auto elim: step.cases)

   701   is distinct, given in lemma @{text wq_distinct}.

   697 

   702 

   698 lemma (in valid_trace) finite_readys [simp]: "finite (readys s)"

   703   The proof is split into the locales for events (or operations),

   699   using finite_threads readys_threads rev_finite_subset by blast

   704   all contain a lemma named @{text "wq_distinct_kept"} to show that

   705   the distinctiveness is preserved by the respective operation. All lemmas

   706   before are to facilitate the proof of @{text "wq_distinct_kept"}.

   707 

   708   The proof also demonstrates the common pattern to prove

   709   invariant properties over valid traces, i.e. to spread the 

   710   invariant proof into locales and to assemble the results of all 

   711   locales to complete the final proof.

   712   

   713 *}

   763 

   777                   

   872 context valid_trace_e

   893 text {*

   873 begin

   894   This section shows that all threads withing waiting queues are

   874 

   895   in the @{term threads}-set. In other words, @{term threads} covers

   875 lemma wq_out_inv: 

   896   all the threads in waiting queue.

   876   assumes s_in: "thread \<in> set (wq s cs)"

   897 

   877   and s_hd: "thread = hd (wq s cs)"

   898   The proof follows the same pattern as @{thm valid_trace.wq_distinct}.

   878   and s_i: "thread \<noteq> hd (wq (e#s) cs)"

   899   The desired property is shown to be kept by all operations (or events)

   879   shows "e = V thread cs"

   900   in their respective locales, and finally the main lemmas is 

   880 proof(cases e)

   901   derived by assembling the invariant keeping results of the locales. 

   881 -- {* There are only two non-trivial cases: *}

   902 *}

   882   case (V th cs1)

   903 

   883   show ?thesis

   904 context valid_trace_create

   884   proof(cases "cs1 = cs")

   905 begin

   885     case True

   906 

   886     have "PIP s (V th cs)" using pip_e[unfolded V[unfolded True]] .

   907 lemma 

   887     thus ?thesis

   888     proof(cases)

   889       case (thread_V)

   890       moreover have "th = thread" using thread_V(2) s_hd

   891           by (unfold s_holding_def wq_def, simp)

   892       ultimately show ?thesis using V True by simp

   893     qed

   894   qed (insert assms V, auto simp:wq_def Let_def split:if_splits)

   895 next

   896   case (P th cs1)

   897   show ?thesis

   898   proof(cases "cs1 = cs")

   899     case True

   900     with P have "wq (e#s) cs = wq_fun (schs s) cs @ [th]"

   901       by (auto simp:wq_def Let_def split:if_splits)

   902     with s_i s_hd s_in have False

   903       by (metis empty_iff hd_append2 list.set(1) wq_def) 

   904     thus ?thesis by simp

   905   qed (insert assms P, auto simp:wq_def Let_def split:if_splits)

   906 qed (insert assms, auto simp:wq_def Let_def split:if_splits)

   907 

   908 lemma wq_in_inv: 

   909   assumes s_ni: "thread \<notin> set (wq s cs)"

   910   and s_i: "thread \<in> set (wq (e#s) cs)"

   911   shows "e = P thread cs"

   912 proof(cases e)

   913   -- {* This is the only non-trivial case: *}

   914   case (V th cs1)

   915   have False

   916   proof(cases "cs1 = cs")

   917     case True

   918     show ?thesis

   919     proof(cases "(wq s cs1)")

   920       case (Cons w_hd w_tl)

   921       have "set (wq (e#s) cs) \<subseteq> set (wq s cs)"

   922       proof -

   923         have "(wq (e#s) cs) = (SOME q. distinct q \<and> set q = set w_tl)"

   924           using  Cons V by (auto simp:wq_def Let_def True split:if_splits)

   925         moreover have "set ... \<subseteq> set (wq s cs)"

   926         proof(rule someI2)

   927           show "distinct w_tl \<and> set w_tl = set w_tl"

   928             by (metis distinct.simps(2) local.Cons wq_distinct)

   929         qed (insert Cons True, auto)

   930         ultimately show ?thesis by simp

   931       qed

   932       with assms show ?thesis by auto

   933     qed (insert assms V True, auto simp:wq_def Let_def split:if_splits)

   934   qed (insert assms V, auto simp:wq_def Let_def split:if_splits)

   935   thus ?thesis by auto

   936 qed (insert assms, auto simp:wq_def Let_def split:if_splits)

   937 

   938 end

   939 

   940 lemma (in valid_trace_create)

   947 lemma (in valid_trace_create)

   914 lemma 

   951 lemma (in valid_trace_exit)

   918 lemma wq_threads_kept:

   952   threads_es [simp]: "threads (e#s) = threads s - {th}"

   919   assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"

   920   and "th' \<in> set (wq (e#s) cs')"

   921   shows "th' \<in> threads (e#s)"

   922 proof -

   923   have "th' \<in> threads s"

   924   proof -

   925     from assms(2)[unfolded wq_kept]

   926     have "th' \<in> set (wq s cs')" .

   927     from assms(1)[OF this] show ?thesis .

   928   qed

   929   with threads_es show ?thesis by simp

   930 qed

   931 

   932 end

   933 

   934 context valid_trace_exit

   935 begin

   936 

   937 lemma threads_es [simp]: "threads (e#s) = threads s - {th}"

   955 lemma (in valid_trace_p)

   940 lemma 

   956   threads_es [simp]: "threads (e#s) = threads s"

   941   th_not_in_wq: "th \<notin> set (wq s cs)"

   957   by (unfold is_p, simp)

   942 proof -

   958 

   943   from pip_e[unfolded is_exit]

   959 lemma (in valid_trace_v)

   944   show ?thesis

   945   by (cases, unfold holdents_def s_holding_def, fold wq_def, 

   946              auto elim!:runing_wqE)

   947 qed

   948 

   949 lemma wq_threads_kept:

   950   assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"

   951   and "th' \<in> set (wq (e#s) cs')"

   952   shows "th' \<in> threads (e#s)"

   953 proof -

   954   have "th' \<in> threads s"

   955   proof -

   956     from assms(2)[unfolded wq_kept]

   957     have "th' \<in> set (wq s cs')" .

   958     from assms(1)[OF this] show ?thesis .

   959   qed

   960   moreover have "th' \<noteq> th"

   961   proof

   962     assume otherwise: "th' = th"

   963     from assms(2)[unfolded wq_kept]

   964     have "th' \<in> set (wq s cs')" .

   965     with th_not_in_wq[folded otherwise]

   966     show False by simp

   967   qed

   968   ultimately show ?thesis

   969     by (unfold threads_es, simp)

   970 qed

   971 

   972 end

   973 

   974 context valid_trace_v

   975 begin

   976 

   977 lemma 

   963 lemma (in valid_trace_v)

   981 lemma 

   964   th_not_in_rest[simp]: "th \<notin> set rest"

   982   th_not_in_rest: "th \<notin> set rest"

   972 lemma (in valid_trace_v) distinct_rest: "distinct rest"

   990 lemma distinct_rest: "distinct rest"

   975 lemma (in valid_trace_v)

   993 lemma

   984       by (unfold wq_s_cs, simp)

  1002       by (unfold wq_s_cs, simp add:th_not_in_rest)

   985 qed

  1003 qed

   986 

  1004 

   987 lemma (in valid_trace_exit)

  1005 lemma wq_threads_kept:

   988   th_not_in_wq: "th \<notin> set (wq s cs)"

  1006   assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"

   989 proof -

  1007   and "th' \<in> set (wq (e#s) cs')"

   990   from pip_e[unfolded is_exit]

  1008   shows "th' \<in> threads (e#s)"

   991   show ?thesis

  1009 proof(cases "cs' = cs")

   992   by (cases, unfold holdents_def s_holding_def, fold wq_def, 

  1010   case True

   993              auto elim!:runing_wqE)

  1011   have " th' \<in> threads s"

   994 qed

  1012   proof -

   995 

  1013     from assms(2)[unfolded True set_wq_es_cs]

  1014     have "th' \<in> set (wq s cs) - {th}" .

  1015     hence "th' \<in> set (wq s cs)" by simp

  1016     from assms(1)[OF this]

  1017     show ?thesis .

  1018   qed

  1019   with threads_es show ?thesis by simp

  1020 next

  1021     case False

  1022     have "th' \<in> threads s"

  1023     proof -

  1024       from wq_neq_simp[OF False]

  1025       have "wq (e # s) cs' = wq s cs'" .

  1026       from assms(2)[unfolded this]

  1027       have "th' \<in> set (wq s cs')" .

  1028       from assms(1)[OF this]

  1029       show ?thesis .

  1030     qed

  1031     with threads_es show ?thesis by simp

  1032 qed

  1033 end

  1034 

  1035 context valid_trace_p

  1036 begin

  1037 

  1038 lemma threads_es [simp]: "threads (e#s) = threads s"

  1039   by (unfold is_p, simp)

  1040 

  1041 lemma ready_th_s: "th \<in> readys s"

  1042   using runing_th_s

  1043   by (unfold runing_def, auto)

  1044 

  1045 lemma live_th_s: "th \<in> threads s"

  1046   using readys_threads ready_th_s by auto

  1047 

  1048 lemma wq_threads_kept:

  1049   assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"

  1050   and "th' \<in> set (wq (e#s) cs')"

  1051   shows "th' \<in> threads (e#s)"

  1052 proof(cases "cs' = cs")

  1053     case True

  1054     from assms(2)[unfolded True wq_es_cs]

  1055     have "th' \<in> set (wq s cs) \<or> th' = th" by auto

  1056     thus ?thesis

  1057     proof

  1058       assume "th' \<in> set (wq s cs)"

  1059       from assms(1)[OF this] have "th' \<in> threads s" .

  1060       with threads_es

  1061       show ?thesis by simp

  1062     next

  1063       assume "th' = th"

  1064       with live_th_s have "th' \<in> threads s" by simp

  1065       with threads_es show ?thesis by simp

  1066     qed

  1067 next

  1068     case False

  1069     have "th' \<in> threads s"

  1070     proof -

  1071       from wq_neq_simp[OF False]

  1072       have "wq (e # s) cs' = wq s cs'" .

  1073       from assms(2)[unfolded this]

  1074       have "th' \<in> set (wq s cs')" .

  1075       from assms(1)[OF this]

  1076       show ?thesis .

  1077     qed

  1078     with threads_es show ?thesis by simp

  1079 qed

  1080 

  1081 end

  1082 

  1083 context valid_trace_set

  1084 begin

  1085 

  1086 lemma threads_kept[simp]:

  1087   "threads (e#s) = threads s"

  1088   by (unfold is_set, simp)

  1089 

  1090 lemma wq_threads_kept: 

  1091   assumes "\<And> th' cs'. th' \<in> set (wq s cs') \<Longrightarrow> th' \<in> threads s"

  1092   and "th' \<in> set (wq (e#s) cs')"

  1093   shows "th' \<in> threads (e#s)"

  1094 proof -

  1095   have "th' \<in> threads s"

  1096      using assms(1)[OF assms(2)[unfolded wq_kept]] .

  1097   with threads_kept show ?thesis by simp

  1098 qed

  1099 

  1100 end

  1101 

  1102 text {*

  1103   The is the main lemma of this section, which is derived

  1104   by induction, case analysis on event @{text e} and 

  1105   assembling the @{text "wq_threads_kept"}-results of 

  1106   all possible cases of @{text "e"}.

  1107 *}

  1000 proof(induct rule:ind)

  1112 proof(induct arbitrary:th cs rule:ind)

  1011     show ?thesis

  1123     show ?thesis using vt.wq_threads_kept Cons by auto

  1012       using Cons.hyps(2) Cons.prems by auto

  1017     show ?thesis

  1128     show ?thesis using vt.wq_threads_kept Cons by auto

  1018       using Cons.hyps(2) Cons.prems vt.th_not_in_wq by auto 

  1023     show ?thesis

  1133    show ?thesis using vt.wq_threads_kept Cons by auto

  1024       using Cons.hyps(2) Cons.prems readys_threads 

  1025         runing_ready vt.is_p vt.runing_th_s vt_e.wq_in_inv 

  1026         by fastforce 

  1031     show ?thesis using Cons

  1138    show ?thesis using vt.wq_threads_kept Cons by auto

  1032       using vt.is_v vt.threads_es vt_e.wq_in_inv by blast

  1037     show ?thesis using Cons.hyps(2) Cons.prems vt.is_set 

  1143    show ?thesis using vt.wq_threads_kept Cons by auto

  1038         by (auto simp:wq_def Let_def)

  1042 section {* RAG and threads *}

  1147 subsection {* RAG and threads *}

  1672   by (metis cs_waiting_def event.distinct(15) is_p list.sel(1) 

  1783   by (metis empty_iff list.sel(1) list.set(1) s_waiting_def 

  1673         set_ConsD waiting_eq we wq_es_cs' wq_neq_simp wq_out_inv)

  1784       set_ConsD wq_def wq_es_cs' wq_neq_simp)

  1774     using event.inject(3) holder_def is_p s_holding_def s_waiting_def that 

  1885     using s_holding_def that wq_def wq_es_cs' wq_s_cs by auto

  1775       waiting_es_th_cs wq_def wq_es_cs' wq_in_inv

  1776     by(force)

  1873 section {* Finiteness of RAG *}

  1982 section {* RAG is finite *}

  3041   qed (auto simp:False subtree_def)

  3155   qed (auto simp:False subtree_def finite_readys)