5 

     5 

     6 (*

     6 (*

     7   The use of dependants has been abandoned. Through a series of lemma 

     7   The use of dependants has been abandoned. Through a series of lemma 

     8   named xxx_alt_def, lemma originally expressed using dependants 

     8   named xxx_alt_def, lemma originally expressed using dependants 

     9   is now expressed in terms of RAG, tRAG and tG.

     9   is now expressed in terms of RAG, tRAG and tG.

    11 

    11 

    12 text {*

    12 text {*

    13 

    13 

    14   This file contains lemmas used to guide the recalculation of current

    14   This file contains lemmas used to guide the recalculation of current

    15   precedence after every step of execution (or system operation, or event),

    15   precedence after every step of execution (or system operation, or event),

   861 *}

   861 *}

   862 lemma tRAG_kept: "tRAG (e#s) = tRAG s"

   862 lemma tRAG_kept: "tRAG (e#s) = tRAG s"

   863   by (unfold tRAG_alt_def RAG_es, auto)

   863   by (unfold tRAG_alt_def RAG_es, auto)

   864 

   864 

   865 lemma tG_kept: "tG (e#s) = tG s"

   865 lemma tG_kept: "tG (e#s) = tG s"

   867 

   867 

   868 text {*

   868 text {*

   869   The following lemma shows that @{text th} is completely isolated 

   869   The following lemma shows that @{text th} is completely isolated 

   870   from @{text RAG}.

   870   from @{text RAG}.

   871 *}

   871 *}

   969 

   969 

   970 text {*

   970 text {*

   971   Since @{term tG} is defined in terms of @{term tRAG}, @{term tG} is not changed neither.

   971   Since @{term tG} is defined in terms of @{term tRAG}, @{term tG} is not changed neither.

   972 *}

   972 *}

   973 lemma tG_kept: "tG (e#s) = tG s"

   973 lemma tG_kept: "tG (e#s) = tG s"

   975 

   975 

   976 lemma th_RAG: "Th th \<notin> Field (RAG s)"

   976 lemma th_RAG: "Th th \<notin> Field (RAG s)"

   977 proof -

   977 proof -

   978   have "Th th \<notin> Range (RAG s)"

   978   have "Th th \<notin> Range (RAG s)"

   979   proof

   979   proof

  1014 lemma eq_cp:

  1014 lemma eq_cp:

  1015   assumes neq_th: "th' \<noteq> th"

  1015   assumes neq_th: "th' \<noteq> th"

  1016   shows "cp (e#s) th' = cp s th'"

  1016   shows "cp (e#s) th' = cp s th'"

  1017 proof -

  1017 proof -

  1018   have "(the_preced (e # s) ` subtree (tG (e # s)) th') =

  1018   have "(the_preced (e # s) ` subtree (tG (e # s)) th') =

  1020   proof -

  1020   proof -

  1021     { fix a

  1021     { fix a

  1022       assume "a \<in> subtree (tG s) th'"

  1022       assume "a \<in> subtree (tG s) th'"

  1023       with th_not_in_tG have "a \<noteq> th"

  1023       with th_not_in_tG have "a \<noteq> th"

  1024         by (metis ex_in_conv neq_th root_def root_readys_tG subtree_ancestorsI th_ready_s)

  1024         by (metis ex_in_conv neq_th root_def root_readys_tG subtree_ancestorsI th_ready_s)