208 

   208 

   209 (* Wrong:

   209 (* Wrong:

   210     lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"

   210     lemma \<lbrakk>thread \<in> set (wq_fun cs1 s); thread \<in> set (wq_fun cs2 s)\<rbrakk> \<Longrightarrow> cs1 = cs2"

   211 *)

   211 *)

   212 

   212 

   214   The nature of the work is like this: since it starts from a very simple and basic 

   214   The nature of the work is like this: since it starts from a very simple and basic 

   215   model, even intuitively very `basic` and `obvious` properties need to derived from scratch.

   215   model, even intuitively very `basic` and `obvious` properties need to derived from scratch.

   216   For instance, the fact 

   216   For instance, the fact 

   217   that one thread can not be blocked by two critical resources at the same time

   217   that one thread can not be blocked by two critical resources at the same time

   218   is obvious, because only running threads can make new requests, if one is waiting for 

   218   is obvious, because only running threads can make new requests, if one is waiting for 

   840       show False by auto

   840       show False by auto

   841     qed

   841     qed

   842   qed

   842   qed

   843 qed

   843 qed

   844 

   844 

   846   The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed

   846   The following @{text "step_RAG_v"} lemma charaterizes how @{text "RAG"} is changed

   847   with the happening of @{text "V"}-events:

   847   with the happening of @{text "V"}-events:

   848 *}

   848 *}

   849 lemma step_RAG_v:

   849 lemma step_RAG_v:

   850 fixes th::thread

   850 fixes th::thread

  1542   moreover from cs_not_in 

  1542   moreover from cs_not_in 

  1543   have "cs \<notin> (holdents (V thread cs#s) thread)" by auto

  1543   have "cs \<notin> (holdents (V thread cs#s) thread)" by auto

  1544   ultimately show ?thesis by (simp add:cntCS_def)

  1544   ultimately show ?thesis by (simp add:cntCS_def)

  1545 qed 

  1545 qed 

  1546 

  1546 

  1548   The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} 

  1548   The relationship between @{text "cntP"}, @{text "cntV"} and @{text "cntCS"} 

  1549   of one particular thread. 

  1549   of one particular thread. 

  1550 *} 

  1550 *} 

  1551 

  1551 

  1552 lemma cnp_cnv_cncs:

  1552 lemma cnp_cnv_cncs: