Mercurial Mercurial > hg > pip / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CpsG.thy
changeset 56 0fd478e14e87
parent 55 b85cfbd58f59
child 58 ad57323fd4d6
equal deleted inserted replaced
55:b85cfbd58f59 56:0fd478e14e87 
     1 section {*
 
     1 section {*
 
     2   This file contains lemmas used to guide the recalculation of current precedence 
     2   This file contains lemmas used to guide the recalculation of current precedence 
     3   after every system call (or system operation)
 
     3   after every system call (or system operation)
 
     4 *}
 
     4 *}
 
     5 theory CpsG
 
     5 theory CpsG
 
     6 imports PrioG Max
 
     6 imports PrioG Max RTree
 
     7 begin
 
     7 begin
 
       
     8 
       
     9 locale pip = 
       
    10   fixes s
 
       
    11   assumes vt: "vt s"
 
       
    12 
       
    13 context pip
 
       
    14 begin
 
       
    15 
       
    16 interpretation rtree_RAG: rtree "RAG s"
 
       
    17 proof
 
       
    18   show "single_valued (RAG s)"
 
       
    19   apply (intro_locales)
 
       
    20     by (unfold single_valued_def, auto intro: unique_RAG[OF vt])
 
       
    21 
       
    22   show "acyclic (RAG s)"
 
       
    23      by (rule acyclic_RAG[OF vt])
 
       
    24 qed
 
       
    25 
       
    26 end
 
       
    27 
       
    28 
       
    29 
       
    30 definition "the_preced s th = preced th s"
 
       
    31 
       
    32 lemma cp_alt_def:
 
       
    33   "cp s th =  
       
    34            Max ((the_preced s) ` {th'. Th th' \<in> (subtree (RAG s) (Th th))})"
 
       
    35 proof -
 
       
    36   have "Max (the_preced s ` ({th} \<union> dependants (wq s) th)) =
 
       
    37         Max (the_preced s ` {th'. Th th' \<in> subtree (RAG s) (Th th)})" 
       
    38           (is "Max (_ ` ?L) = Max (_ ` ?R)")
 
       
    39   proof -
 
       
    40     have "?L = ?R" 
       
    41     by (auto dest:rtranclD simp:cs_dependants_def cs_RAG_def s_RAG_def subtree_def)
 
       
    42     thus ?thesis by simp
 
       
    43   qed
 
       
    44   thus ?thesis by (unfold cp_eq_cpreced cpreced_def, fold the_preced_def, simp)
 
       
    45 qed
 
     8 
    46 
     9 lemma eq_dependants: "dependants (wq s) = dependants s"
 
    47 lemma eq_dependants: "dependants (wq s) = dependants s"
 
    10   by (simp add: s_dependants_abv wq_def)
 
    48   by (simp add: s_dependants_abv wq_def)
 
    11   
    49   
    12 (* obvious lemma *)
 
    50 (* obvious lemma *)
 
   573     with eq_wq and wq_distinct[OF vt, of cs]
 
   611     with eq_wq and wq_distinct[OF vt, of cs]
 
   574     show False by auto
 
   612     show False by auto
 
   575   qed
 
   613   qed
 
   576 qed
 
   614 qed
 
   577 
   615 
       
   616 -- {* A useless definition *}
 
   578 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
 
   617 definition cps:: "state \<Rightarrow> (thread \<times> precedence) set"
 
   579 where "cps s = {(th, cp s th) | th . th \<in> threads s}"
 
   618 where "cps s = {(th, cp s th) | th . th \<in> threads s}"
 
       
   619 
   580 
   620 
   581 text {* (* ddd *)
 
   621 text {* (* ddd *)
 
   582   One beauty of our modelling is that we follow the definitional extension tradition of HOL.
 
   622   One beauty of our modelling is that we follow the definitional extension tradition of HOL.
 
   583   The benefit of such a concise and miniature model is that  large number of intuitively 
   623   The benefit of such a concise and miniature model is that  large number of intuitively 
   584   obvious facts are derived as lemmas, rather than asserted as axioms.
 
   624   obvious facts are derived as lemmas, rather than asserted as axioms.
 
   617          the legitimacy of @{text "s"} can be derived. *}
 
   657          the legitimacy of @{text "s"} can be derived. *}
 
   618   assumes vt_s: "vt s"
 
   658   assumes vt_s: "vt s"
 
   619 
   659 
   620 context step_set_cps 
   660 context step_set_cps 
   621 begin
 
   661 begin
 
       
   662 
       
   663 interpretation rtree_RAGs: rtree "RAG s"
 
       
   664 proof
 
       
   665   show "single_valued (RAG s)"
 
       
   666   apply (intro_locales)
 
       
   667     by (unfold single_valued_def, auto intro: unique_RAG[OF vt_s])
 
       
   668 
       
   669   show "acyclic (RAG s)"
 
       
   670      by (rule acyclic_RAG[OF vt_s])
 
       
   671 qed
 
       
   672 
       
   673 interpretation rtree_RAGs': rtree "RAG s'"
 
       
   674 proof
 
       
   675   show "single_valued (RAG s')"
 
       
   676   apply (intro_locales)
 
       
   677     by (unfold single_valued_def, 
       
   678         auto intro: unique_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
 
       
   679 
       
   680   show "acyclic (RAG s')"
 
       
   681      by (rule acyclic_RAG[OF step_back_vt[OF vt_s[unfolded s_def]]])
 
       
   682 qed
 
   622 
   683 
   623 text {* (* ddd *)
 
   684 text {* (* ddd *)
 
   624   The following lemma confirms that @{text "Set"}-operating only changes the precedence 
   685   The following lemma confirms that @{text "Set"}-operating only changes the precedence 
   625   of initiating thread.
 
   686   of initiating thread.
 
   626 *}
 
   687 *}
 
   730   fixes th' 
   791   fixes th' 
   731   assumes "th' \<noteq> th"
 
   792   assumes "th' \<noteq> th"
 
   732   shows "cp s th' = cp s' th'"
 
   793   shows "cp s th' = cp s' th'"
 
   733   by (rule eq_cp_pre[OF assms no_dependants])
 
   794   by (rule eq_cp_pre[OF assms no_dependants])
 
   734 
   795 
   735 
   796 end
 
   736 text {* (* ddd *) \noindent
 
   797 
   737    The following @{text "eq_up"} was originally designed to save the recalculations
 
   798 text {*
 
   738    of current precedence going upstream from thread @{text "th"} can stop earlier. 
   799   The following @{text "step_v_cps"} is the locale for @{text "V"}-operation.
 
   739    If at a certain point along way, the recalculation results in the same
 
       
   740    result, the recalculation can stop there. 
       
   741    This lemma is obsolete because we found that @{text "th"} is not contained in 
       
   742    any thread's dependants set. 
       
   743 
       
   744    The foregoing lemma says only those threads which 
       
   745 *}
 
   800 *}
 
   746 lemma eq_up:
 
   801 
   747   fixes th' th''
 
   802 locale step_v_cps =
 
   748   assumes dp1: "th \<in> dependants s th'"
 
   803   -- {* @{text "th"} is the initiating thread *}
 
   749   and dp2: "th' \<in> dependants s th''"
 
   804   -- {* @{text "cs"} is the critical resource release by the @{text "V"}-operation *}
 
   750   and eq_cps: "cp s th' = cp s' th'"
 
   805   fixes s' th cs s    -- {* @{text "s'"} is the state before operation*}
 
   751   shows "cp s th'' = cp s' th''"
 
   806   defines s_def : "s \<equiv> (V th cs#s')" -- {* @{text "s"} is the state after operation*}
 
   752 proof -
 
   807   -- {* @{text "s"} is assumed to be valid, which implies the validity of @{text "s'"} *}
 
   753   from dp2
 
   808   assumes vt_s: "vt s"
 
   754   have "(Th th', Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
 
   809 
   755   from RAG_child[OF vt_s this[unfolded eq_RAG]]
 
   810 text {*
 
   756   have ch_th': "(Th th', Th th'') \<in> (child s)\<^sup>+" .
 
   811   The following @{text "step_v_cps_nt"} is the sub-locale for @{text "V"}-operation, 
   757   moreover { fix n th''
 
   812   which represents the case when there is another thread @{text "th'"}
 
   758     have "\<lbrakk>(Th th', n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
 
   813   to take over the critical resource released by the initiating thread @{text "th"}.
 
   759                    (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
 
       
   760     proof(erule trancl_induct, auto)
 
       
   761       fix y th''
 
       
   762       assume y_ch: "(y, Th th'') \<in> child s"
 
       
   763         and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
 
       
   764         and ch': "(Th th', y) \<in> (child s)\<^sup>+"
 
       
   765       from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
 
       
   766       with ih have eq_cpy:"cp s thy = cp s' thy" by blast
 
       
   767       from dp1 have "(Th th, Th th') \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
 
       
   768       moreover from child_RAG_p[OF ch'] and eq_y
 
       
   769       have "(Th th', Th thy) \<in> (RAG s)^+" by simp
 
       
   770       ultimately have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by auto
 
       
   771       show "cp s th'' = cp s' th''"
 
       
   772         apply (subst cp_rec[OF vt_s])
 
       
   773       proof -
 
       
   774         have "preced th'' s = preced th'' s'"
 
       
   775         proof(rule eq_preced)
 
       
   776           show "th'' \<noteq> th"
 
       
   777           proof
 
       
   778             assume "th'' = th"
 
       
   779             with dp_thy y_ch[unfolded eq_y] 
       
   780             have "(Th th, Th th) \<in> (RAG s)^+"
 
       
   781               by (auto simp:child_def)
 
       
   782             with wf_trancl[OF wf_RAG[OF vt_s]] 
       
   783             show False by auto
 
       
   784           qed
 
       
   785         qed
 
       
   786         moreover { 
       
   787           fix th1
 
       
   788           assume th1_in: "th1 \<in> children s th''"
 
       
   789           have "cp s th1 = cp s' th1"
 
       
   790           proof(cases "th1 = thy")
 
       
   791             case True
 
       
   792             with eq_cpy show ?thesis by simp
 
       
   793           next
 
       
   794             case False
 
       
   795             have neq_th1: "th1 \<noteq> th"
 
       
   796             proof
 
       
   797               assume eq_th1: "th1 = th"
 
       
   798               with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
 
       
   799               from children_no_dep[OF vt_s _ _ this] and 
       
   800               th1_in y_ch eq_y show False by (auto simp:children_def)
 
       
   801             qed
 
       
   802             have "th \<notin> dependants s th1"
 
       
   803             proof
 
       
   804               assume h:"th \<in> dependants s th1"
 
       
   805               from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
 
       
   806               from dependants_child_unique[OF vt_s _ _ h this]
 
       
   807               th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
 
       
   808               with False show False by auto
 
       
   809             qed
 
       
   810             from eq_cp_pre[OF neq_th1 this]
 
       
   811             show ?thesis .
 
       
   812           qed
 
       
   813         }
 
       
   814         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
       
   815           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
 
       
   816         moreover have "children s th'' = children s' th''"
 
       
   817           by (unfold children_def child_def s_def RAG_set_unchanged, simp)
 
       
   818         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
 
       
   819           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
 
       
   820       qed
 
       
   821     next
 
       
   822       fix th''
 
       
   823       assume dp': "(Th th', Th th'') \<in> child s"
 
       
   824       show "cp s th'' = cp s' th''"
 
       
   825         apply (subst cp_rec[OF vt_s])
 
       
   826       proof -
 
       
   827         have "preced th'' s = preced th'' s'"
 
       
   828         proof(rule eq_preced)
 
       
   829           show "th'' \<noteq> th"
 
       
   830           proof
 
       
   831             assume "th'' = th"
 
       
   832             with dp1 dp'
 
       
   833             have "(Th th, Th th) \<in> (RAG s)^+"
 
       
   834               by (auto simp:child_def s_dependants_def eq_RAG)
 
       
   835             with wf_trancl[OF wf_RAG[OF vt_s]] 
       
   836             show False by auto
 
       
   837           qed
 
       
   838         qed
 
       
   839         moreover { 
       
   840           fix th1
 
       
   841           assume th1_in: "th1 \<in> children s th''"
 
       
   842           have "cp s th1 = cp s' th1"
 
       
   843           proof(cases "th1 = th'")
 
       
   844             case True
 
       
   845             with eq_cps show ?thesis by simp
 
       
   846           next
 
       
   847             case False
 
       
   848             have neq_th1: "th1 \<noteq> th"
 
       
   849             proof
 
       
   850               assume eq_th1: "th1 = th"
 
       
   851               with dp1 have "(Th th1, Th th') \<in> (RAG s)^+" 
       
   852                 by (auto simp:s_dependants_def eq_RAG)
 
       
   853               from children_no_dep[OF vt_s _ _ this]
 
       
   854               th1_in dp'
 
       
   855               show False by (auto simp:children_def)
 
       
   856             qed
 
       
   857             thus ?thesis
 
       
   858             proof(rule eq_cp_pre)
 
       
   859               show "th \<notin> dependants s th1"
 
       
   860               proof
 
       
   861                 assume "th \<in> dependants s th1"
 
       
   862                 from dependants_child_unique[OF vt_s _ _ this dp1]
 
       
   863                 th1_in dp' have "th1 = th'"
 
       
   864                   by (auto simp:children_def)
 
       
   865                 with False show False by auto
 
       
   866               qed
 
       
   867             qed
 
       
   868           qed
 
       
   869         }
 
       
   870         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
       
   871           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
 
       
   872         moreover have "children s th'' = children s' th''"
 
       
   873           by (unfold children_def child_def s_def RAG_set_unchanged, simp)
 
       
   874         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
 
       
   875           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
 
       
   876       qed     
       
   877     qed
 
       
   878   }
 
       
   879   ultimately show ?thesis by auto
 
       
   880 qed
 
       
   881 
       
   882 text {* (* ddd *)
 
       
   883   For those @{text "th''"},  @{text "th \<in> dependants s th''"} means that 
       
   884   the current precedence of such @{text "th''"} might possibly be boosted if the 
       
   885   current precedence of @{text "th"} somehow get raised. The following lemma
 
       
   886   says that if the resetting of its own priority by thread @{text "th"} does not
 
       
   887   change its current precedence, then the current precedence of such @{text "th''"}
 
       
   888   will remain unchanged. The situation such that @{text "th"}'s current 
       
   889   precedence does not change with the resetting of its priority might happen in many
 
       
   890   different cases. For example, if the current precedence of @{text "th"} is already an inherited one,
 
       
   891   the lowering of its priority will not change its current precedence, and the increasing 
       
   892   of its priority will not change its current precedence neither, if 
       
   893   incidental rising of its own precedence is not large enough to surpass the inherited precedence. 
       
   894 *}
 
   814 *}
 
   895 
       
   896 lemma eq_up_self:
 
       
   897   fixes th' th''
 
       
   898   assumes dp: "th \<in> dependants s th''"
 
       
   899   and eq_cps: "cp s th = cp s' th"
 
       
   900   shows "cp s th'' = cp s' th''"
 
       
   901 proof -
 
       
   902   from dp
 
       
   903   have "(Th th, Th th'') \<in> (RAG (wq s))\<^sup>+" by (simp add:s_dependants_def)
 
       
   904   from RAG_child[OF vt_s this[unfolded eq_RAG]]
 
       
   905   have ch_th': "(Th th, Th th'') \<in> (child s)\<^sup>+" .
 
       
   906   moreover { fix n th''
 
       
   907     have "\<lbrakk>(Th th, n) \<in> (child s)^+\<rbrakk> \<Longrightarrow>
 
       
   908                    (\<forall> th'' . n = Th th'' \<longrightarrow> cp s th'' = cp s' th'')"
 
       
   909     proof(erule trancl_induct, auto)
 
       
   910       fix y th''
 
       
   911       assume y_ch: "(y, Th th'') \<in> child s"
 
       
   912         and ih: "\<forall>th''. y = Th th'' \<longrightarrow> cp s th'' = cp s' th''"
 
       
   913         and ch': "(Th th, y) \<in> (child s)\<^sup>+"
 
       
   914       from y_ch obtain thy where eq_y: "y = Th thy" by (auto simp:child_def)
 
       
   915       with ih have eq_cpy:"cp s thy = cp s' thy" by blast
 
       
   916       from child_RAG_p[OF ch'] and eq_y
 
       
   917       have dp_thy: "(Th th, Th thy) \<in> (RAG s)^+" by simp
 
       
   918       show "cp s th'' = cp s' th''"
 
       
   919         apply (subst cp_rec[OF vt_s])
 
       
   920       proof -
 
       
   921         have "preced th'' s = preced th'' s'"
 
       
   922         proof(rule eq_preced)
 
       
   923           show "th'' \<noteq> th"
 
       
   924           proof
 
       
   925             assume "th'' = th"
 
       
   926             with dp_thy y_ch[unfolded eq_y] 
       
   927             have "(Th th, Th th) \<in> (RAG s)^+"
 
       
   928               by (auto simp:child_def)
 
       
   929             with wf_trancl[OF wf_RAG[OF vt_s]] 
       
   930             show False by auto
 
       
   931           qed
 
       
   932         qed
 
       
   933         moreover { 
       
   934           fix th1
 
       
   935           assume th1_in: "th1 \<in> children s th''"
 
       
   936           have "cp s th1 = cp s' th1"
 
       
   937           proof(cases "th1 = thy")
 
       
   938             case True
 
       
   939             with eq_cpy show ?thesis by simp
 
       
   940           next
 
       
   941             case False
 
       
   942             have neq_th1: "th1 \<noteq> th"
 
       
   943             proof
 
       
   944               assume eq_th1: "th1 = th"
 
       
   945               with dp_thy have "(Th th1, Th thy) \<in> (RAG s)^+" by simp
 
       
   946               from children_no_dep[OF vt_s _ _ this] and 
       
   947               th1_in y_ch eq_y show False by (auto simp:children_def)
 
       
   948             qed
 
       
   949             have "th \<notin> dependants s th1"
 
       
   950             proof
 
       
   951               assume h:"th \<in> dependants s th1"
 
       
   952               from eq_y dp_thy have "th \<in> dependants s thy" by (auto simp:s_dependants_def eq_RAG)
 
       
   953               from dependants_child_unique[OF vt_s _ _ h this]
 
       
   954               th1_in y_ch eq_y have "th1 = thy" by (auto simp:children_def child_def)
 
       
   955               with False show False by auto
 
       
   956             qed
 
       
   957             from eq_cp_pre[OF neq_th1 this]
 
       
   958             show ?thesis .
 
       
   959           qed
 
       
   960         }
 
       
   961         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
       
   962           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
 
       
   963         moreover have "children s th'' = children s' th''"
 
       
   964           by (unfold children_def child_def s_def RAG_set_unchanged, simp)
 
       
   965         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
 
       
   966           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
 
       
   967       qed
 
       
   968     next
 
       
   969       fix th''
 
       
   970       assume dp': "(Th th, Th th'') \<in> child s"
 
       
   971       show "cp s th'' = cp s' th''"
 
       
   972         apply (subst cp_rec[OF vt_s])
 
       
   973       proof -
 
       
   974         have "preced th'' s = preced th'' s'"
 
       
   975         proof(rule eq_preced)
 
       
   976           show "th'' \<noteq> th"
 
       
   977           proof
 
       
   978             assume "th'' = th"
 
       
   979             with dp dp'
 
       
   980             have "(Th th, Th th) \<in> (RAG s)^+"
 
       
   981               by (auto simp:child_def s_dependants_def eq_RAG)
 
       
   982             with wf_trancl[OF wf_RAG[OF vt_s]] 
       
   983             show False by auto
 
       
   984           qed
 
       
   985         qed
 
       
   986         moreover { 
       
   987           fix th1
 
       
   988           assume th1_in: "th1 \<in> children s th''"
 
       
   989           have "cp s th1 = cp s' th1"
 
       
   990           proof(cases "th1 = th")
 
       
   991             case True
 
       
   992             with eq_cps show ?thesis by simp
 
       
   993           next
 
       
   994             case False
 
       
   995             assume neq_th1: "th1 \<noteq> th"
 
       
   996             thus ?thesis
 
       
   997             proof(rule eq_cp_pre)
 
       
   998               show "th \<notin> dependants s th1"
 
       
   999               proof
 
       
  1000                 assume "th \<in> dependants s th1"
 
       
  1001                 hence "(Th th, Th th1) \<in> (RAG s)^+" by (auto simp:s_dependants_def eq_RAG)
 
       
  1002                 from children_no_dep[OF vt_s _ _ this]
 
       
  1003                 and th1_in dp' show False
 
       
  1004                   by (auto simp:children_def)
 
       
  1005               qed
 
       
  1006             qed
 
       
  1007           qed
 
       
  1008         }
 
       
  1009         ultimately have "{preced th'' s} \<union> (cp s ` children s th'') = 
       
  1010           {preced th'' s'} \<union> (cp s' ` children s th'')" by (auto simp:image_def)
 
       
  1011         moreover have "children s th'' = children s' th''"
 
       
  1012           by (unfold children_def child_def s_def RAG_set_unchanged, simp)
 
       
  1013         ultimately show "Max ({preced th'' s} \<union> cp s ` children s th'') = cp s' th''"
 
       
  1014           by (simp add:cp_rec[OF step_back_vt[OF vt_s[unfolded s_def]]])
 
       
  1015       qed     
       
  1016     qed
 
       
  1017   }
 
       
  1018   ultimately show ?thesis by auto
 
       
  1019 qed
 
       
  1020 end
 
       
  1021 
       
  1022 locale step_v_cps =
 
       
  1023   fixes s' th cs s 
       
  1024   defines s_def : "s \<equiv> (V th cs#s')"
 
       
  1025   assumes vt_s: "vt s"
 
       
  1026 
       
  1027 locale step_v_cps_nt = step_v_cps +
 
   815 locale step_v_cps_nt = step_v_cps +
 
  1028   fixes th'
 
   816   fixes th'
 
  1029   assumes nt: "next_th s' th cs th'"
 
   817   -- {* @{text "th'"} is assumed to take over @{text "cs"} *}
 
       
   818   assumes nt: "next_th s' th cs th'" 
  1030 
   819 
  1031 context step_v_cps_nt
 
   820 context step_v_cps_nt
 
  1032 begin
 
   821 begin
 
       
   822 
       
   823 text {*
 
       
   824   Lemma @{text "RAG_s"} confirms the change of RAG:
 
       
   825   two edges removed and one added, as shown by the following diagram.
 
       
   826 *}
 
       
   827 
       
   828 (*
 
       
   829   RAG before the V-operation
 
       
   830     th1 ----|
 
       
   831             |
 
       
   832     th' ----|
 
       
   833             |----> cs -----|
 
       
   834     th2 ----|              |
 
       
   835             |              |
 
       
   836     th3 ----|              |
 
       
   837                            |------> th
 
       
   838     th4 ----|              |
 
       
   839             |              |
 
       
   840     th5 ----|              |
 
       
   841             |----> cs'-----|
 
       
   842     th6 ----|
 
       
   843             |
 
       
   844     th7 ----|
 
       
   845 
       
   846  RAG after the V-operation
 
       
   847     th1 ----|
 
       
   848             |
 
       
   849             |----> cs ----> th'
 
       
   850     th2 ----|              
       
   851             |              
       
   852     th3 ----|              
       
   853                            
       
   854     th4 ----|              
       
   855             |              
       
   856     th5 ----|              
       
   857             |----> cs'----> th
 
       
   858     th6 ----|
 
       
   859             |
 
       
   860     th7 ----|
 
       
   861 *)
 
  1033 
   862 
  1034 lemma RAG_s:
 
   863 lemma RAG_s:
 
  1035   "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
 
   864   "RAG s = (RAG s' - {(Cs cs, Th th), (Th th', Cs cs)}) \<union>
 
  1036                                          {(Cs cs, Th th')}"
 
   865                                          {(Cs cs, Th th')}"
 
  1037 proof -
 
   866 proof -
 
  1038   from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]
 
   867   from step_RAG_v[OF vt_s[unfolded s_def], folded s_def]
 
  1039     and nt show ?thesis  by (auto intro:next_th_unique)
 
   868     and nt show ?thesis  by (auto intro:next_th_unique)
 
  1040 qed
 
   869 qed
 
  1041 
   870 
       
   871 text {*
 
       
   872   Lemma @{text "dependants_kept"} shows only @{text "th"} and @{text "th'"}
 
       
   873   have their dependants changed.
 
       
   874 *}
 
  1042 lemma dependants_kept:
 
   875 lemma dependants_kept:
 
  1043   fixes th''
 
   876   fixes th''
 
  1044   assumes neq1: "th'' \<noteq> th"
 
   877   assumes neq1: "th'' \<noteq> th"
 
  1045   and neq2: "th'' \<noteq> th'"
 
   878   and neq2: "th'' \<noteq> th'"
 
  1046   shows "dependants (wq s) th'' = dependants (wq s') th''"
 
   879   shows "dependants (wq s) th'' = dependants (wq s') th''"
 
  1047 proof(auto)
 
   880 proof(auto) (* ccc *)
 
  1048   fix x
 
   881   fix x
 
  1049   assume "x \<in> dependants (wq s) th''"
 
   882   assume "x \<in> dependants (wq s) th''"
 
  1050   hence dp: "(Th x, Th th'') \<in> (RAG s)^+"
 
   883   hence dp: "(Th x, Th th'') \<in> (RAG s)^+"
 
  1051     by (auto simp:cs_dependants_def eq_RAG)
 
   884     by (auto simp:cs_dependants_def eq_RAG)
 
  1052   { fix n
 
   885   { fix n
 
  1526 lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
 
  1359 lemma RAG_s: "RAG s = RAG s' \<union> {(Th th, Cs cs)}"
 
  1527 proof -
 
  1360 proof -
 
  1528   from step_RAG_p[OF vt_s[unfolded s_def]] and ne
 
  1361   from step_RAG_p[OF vt_s[unfolded s_def]] and ne
 
  1529   show ?thesis by (simp add:s_def)
 
  1362   show ?thesis by (simp add:s_def)
 
  1530 qed
 
  1363 qed
 
       
  1364 
  1531 
  1365 
  1532 lemma eq_child_left:
 
  1366 lemma eq_child_left:
 
  1533   assumes nd: "(Th th, Th th') \<notin> (child s)^+"
 
  1367   assumes nd: "(Th th, Th th') \<notin> (child s)^+"
 
  1534   shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"
 
  1368   shows "(n1, Th th') \<in> (child s)^+ \<Longrightarrow> (n1, Th th') \<in> (child s')^+"
 
  1535 proof(induct rule:converse_trancl_induct)
 
  1369 proof(induct rule:converse_trancl_induct)
pip