1 theory Correctness

     1 theory Correctness

     2 imports PIPBasics

     2 imports PIPBasics

     3 begin

     3 begin

     4 

     4 

     5 

     7 

     6 text {* 

     8 text {* 

     7   The following two auxiliary lemmas are used to reason about @{term Max}.

     9   The following two auxiliary lemmas are used to reason about @{term Max}.

     8 *}

    10 *}

     9 lemma image_Max_eqI: 

    11 lemma image_Max_eqI: 

   797   otherwise, the running thread is the @{text th'} given by lemma

   799   otherwise, the running thread is the @{text th'} given by lemma

   798   @{thm th_blockedE}.

   800   @{thm th_blockedE}.

   799 

   801 

   800 *}

   802 *}

   801 

   803 

   803 proof(cases "th \<in> runing (t@s)") 

   805 proof(cases "th \<in> runing (t@s)") 

   804   case True thus ?thesis by auto

   806   case True thus ?thesis by auto

   805 next

   807 next

   806   case False

   808   case False

   807   thus ?thesis using th_blockedE by auto

   809   thus ?thesis using th_blockedE by auto