13 definition "tRAG s = wRAG s O hRAG s"

    23 text {* The following lemma splits @{term "RAG"} graph into the above two sub-graphs. *}

    14 

   571 

   581 (* keep *)

   572 lemma eq_dependants: "dependants (wq s) = dependants s"

   573   by (simp add: s_dependants_abv wq_def)

   574  

   575 

   576 (* obvious lemma *)

   577 lemma not_thread_holdents:

   578   fixes th s

   579   assumes vt: "vt s"

   580   and not_in: "th \<notin> threads s" 

   581   shows "holdents s th = {}"

   582 proof -

   583   from vt not_in show ?thesis

   584   proof(induct arbitrary:th)

   585     case (vt_cons s e th)

   586     assume vt: "vt s"

   587       and ih: "\<And>th. th \<notin> threads s \<Longrightarrow> holdents s th = {}"

   588       and stp: "step s e"

   589       and not_in: "th \<notin> threads (e # s)"

   590     from stp show ?case

   591     proof(cases)

   592       case (thread_create thread prio)

   593       assume eq_e: "e = Create thread prio"

   594         and not_in': "thread \<notin> threads s"

   595       have "holdents (e # s) th = holdents s th"

   596         apply (unfold eq_e holdents_test)

   597         by (simp add:RAG_create_unchanged)

   598       moreover have "th \<notin> threads s" 

   599       proof -

   600         from not_in eq_e show ?thesis by simp

   601       qed

   602       moreover note ih ultimately show ?thesis by auto

   603     next

   604       case (thread_exit thread)

   605       assume eq_e: "e = Exit thread"

   606       and nh: "holdents s thread = {}"

   607       show ?thesis

   608       proof(cases "th = thread")

   609         case True

   610         with nh eq_e

   611         show ?thesis 

   612           by (auto simp:holdents_test RAG_exit_unchanged)

   613       next

   614         case False

   615         with not_in and eq_e

   616         have "th \<notin> threads s" by simp

   617         from ih[OF this] False eq_e show ?thesis 

   618           by (auto simp:holdents_test RAG_exit_unchanged)

   619       qed

   620     next

   621       case (thread_P thread cs)

   622       assume eq_e: "e = P thread cs"

   623       and is_runing: "thread \<in> runing s"

   624       from assms thread_exit ih stp not_in vt eq_e have vtp: "vt (P thread cs#s)" by auto

   625       have neq_th: "th \<noteq> thread" 

   626       proof -

   627         from not_in eq_e have "th \<notin> threads s" by simp

   628         moreover from is_runing have "thread \<in> threads s"

   629           by (simp add:runing_def readys_def)

   630         ultimately show ?thesis by auto

   631       qed

   632       hence "holdents (e # s) th  = holdents s th "

   633         apply (unfold cntCS_def holdents_test eq_e)

   634         by (unfold step_RAG_p[OF vtp], auto)

   635       moreover have "holdents s th = {}"

   636       proof(rule ih)

   637         from not_in eq_e show "th \<notin> threads s" by simp

   638       qed

   639       ultimately show ?thesis by simp

   640     next

   641       case (thread_V thread cs)

   642       assume eq_e: "e = V thread cs"

   643         and is_runing: "thread \<in> runing s"

   644         and hold: "holding s thread cs"

   645       have neq_th: "th \<noteq> thread" 

   646       proof -

   647         from not_in eq_e have "th \<notin> threads s" by simp

   648         moreover from is_runing have "thread \<in> threads s"

   649           by (simp add:runing_def readys_def)

   650         ultimately show ?thesis by auto

   651       qed

   652       from assms thread_V eq_e ih stp not_in vt have vtv: "vt (V thread cs#s)" by auto

   653       from hold obtain rest 

   654         where eq_wq: "wq s cs = thread # rest"

   655         by (case_tac "wq s cs", auto simp: wq_def s_holding_def)

   656       from not_in eq_e eq_wq

   657       have "\<not> next_th s thread cs th"

   658         apply (auto simp:next_th_def)

   659       proof -

   660         assume ne: "rest \<noteq> []"

   661           and ni: "hd (SOME q. distinct q \<and> set q = set rest) \<notin> threads s" (is "?t \<notin> threads s")

   662         have "?t \<in> set rest"

   663         proof(rule someI2)

   664           from wq_distinct[OF step_back_vt[OF vtv], of cs] and eq_wq

   665           show "distinct rest \<and> set rest = set rest" by auto

   666         next

   667           fix x assume "distinct x \<and> set x = set rest" with ne

   668           show "hd x \<in> set rest" by (cases x, auto)

   669         qed

   670         with eq_wq have "?t \<in> set (wq s cs)" by simp

   671         from wq_threads[OF step_back_vt[OF vtv], OF this] and ni

   672         show False by auto

   673       qed

   674       moreover note neq_th eq_wq

   675       ultimately have "holdents (e # s) th  = holdents s th"

   676         by (unfold eq_e cntCS_def holdents_test step_RAG_v[OF vtv], auto)

   677       moreover have "holdents s th = {}"

   678       proof(rule ih)

   679         from not_in eq_e show "th \<notin> threads s" by simp

   680       qed

   681       ultimately show ?thesis by simp

   682     next

   683       case (thread_set thread prio)

   684       print_facts

   685       assume eq_e: "e = Set thread prio"

   686         and is_runing: "thread \<in> runing s"

   687       from not_in and eq_e have "th \<notin> threads s" by auto

   688       from ih [OF this] and eq_e

   689       show ?thesis 

   690         apply (unfold eq_e cntCS_def holdents_test)

   691         by (simp add:RAG_set_unchanged)

   692     qed

   693     next

   694       case vt_nil

   695       show ?case

   696       by (auto simp:count_def holdents_test s_RAG_def wq_def cs_holding_def)

   697   qed

   698 qed

   699 

   700 (* obvious lemma *)

   701 lemma next_th_neq: 

   702   assumes vt: "vt s"

   703   and nt: "next_th s th cs th'"

   704   shows "th' \<noteq> th"

   705 proof -

   706   from nt show ?thesis

   707     apply (auto simp:next_th_def)

   708   proof -

   709     fix rest

   710     assume eq_wq: "wq s cs = hd (SOME q. distinct q \<and> set q = set rest) # rest"

   711       and ne: "rest \<noteq> []"

   712     have "hd (SOME q. distinct q \<and> set q = set rest) \<in> set rest" 

   713     proof(rule someI2)

   714       from wq_distinct[OF vt, of cs] eq_wq

   715       show "distinct rest \<and> set rest = set rest" by auto

   716     next

   717       fix x

   718       assume "distinct x \<and> set x = set rest"

   719       hence eq_set: "set x = set rest" by auto

   720       with ne have "x \<noteq> []" by auto

   721       hence "hd x \<in> set x" by auto

   722       with eq_set show "hd x \<in> set rest" by auto

   723     qed

   724     with wq_distinct[OF vt, of cs] eq_wq show False by auto

   725   qed

   726 qed

   727 

   728 (* obvious lemma *)

   729 lemma next_th_unique: 

   730   assumes nt1: "next_th s th cs th1"

   731   and nt2: "next_th s th cs th2"

   732   shows "th1 = th2"

   733 using assms by (unfold next_th_def, auto)

   734 

   735 lemma wf_RAG:

   736   assumes vt: "vt s"

   737   shows "wf (RAG s)"

   738 proof(rule finite_acyclic_wf)

   739   from finite_RAG[OF vt] show "finite (RAG s)" .

   740 next

   741   from acyclic_RAG[OF vt] show "acyclic (RAG s)" .

   742 qed

   743 

   744 definition child :: "state \<Rightarrow> (node \<times> node) set"

   745   where "child s \<equiv>

   746             {(Th th', Th th) | th th'. \<exists>cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"

   747 

   748 definition children :: "state \<Rightarrow> thread \<Rightarrow> thread set"

   749   where "children s th \<equiv> {th'. (Th th', Th th) \<in> child s}"

   750 

   751 lemma children_def2:

   752   "children s th \<equiv> {th'. \<exists> cs. (Th th', Cs cs) \<in> RAG s \<and> (Cs cs, Th th) \<in> RAG s}"

   753 unfolding child_def children_def by simp

   754 

   755 lemma children_dependants: 

   756   "children s th \<subseteq> dependants (wq s) th"

   757   unfolding children_def2

   758   unfolding cs_dependants_def

   759   by (auto simp add: eq_RAG)

   760 

   761 lemma child_unique:

   762   assumes vt: "vt s"

   763   and ch1: "(Th th, Th th1) \<in> child s"

   764   and ch2: "(Th th, Th th2) \<in> child s"

   765   shows "th1 = th2"

   766 using ch1 ch2 

   767 proof(unfold child_def, clarsimp)

   768   fix cs csa

   769   assume h1: "(Th th, Cs cs) \<in> RAG s"

   770     and h2: "(Cs cs, Th th1) \<in> RAG s"

   771     and h3: "(Th th, Cs csa) \<in> RAG s"

   772     and h4: "(Cs csa, Th th2) \<in> RAG s"

   773   from unique_RAG[OF vt h1 h3] have "cs = csa" by simp

   774   with h4 have "(Cs cs, Th th2) \<in> RAG s" by simp

   775   from unique_RAG[OF vt h2 this]

   776   show "th1 = th2" by simp

   777 qed 

   778 

   779 lemma RAG_children:

   780   assumes h: "(Th th1, Th th2) \<in> (RAG s)^+"

   781   shows "th1 \<in> children s th2 \<or> (\<exists> th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)^+)"

   782 proof -

   783   from h show ?thesis

   784   proof(induct rule: tranclE)

   785     fix c th2

   786     assume h1: "(Th th1, c) \<in> (RAG s)\<^sup>+"

   787     and h2: "(c, Th th2) \<in> RAG s"

   788     from h2 obtain cs where eq_c: "c = Cs cs"

   789       by (case_tac c, auto simp:s_RAG_def)

   790     show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"

   791     proof(rule tranclE[OF h1])

   792       fix ca

   793       assume h3: "(Th th1, ca) \<in> (RAG s)\<^sup>+"

   794         and h4: "(ca, c) \<in> RAG s"

   795       show "th1 \<in> children s th2 \<or> (\<exists>th3. th3 \<in> children s th2 \<and> (Th th1, Th th3) \<in> (RAG s)\<^sup>+)"

   796       proof -

   797         from eq_c and h4 obtain th3 where eq_ca: "ca = Th th3"

   798           by (case_tac ca, auto simp:s_RAG_def)

   799         from eq_ca h4 h2 eq_c

   800         have "th3 \<in> children s th2" by (auto simp:children_def child_def)

   801         moreover from h3 eq_ca have "(Th th1, Th th3) \<in> (RAG s)\<^sup>+" by simp

   802         ultimately show ?thesis by auto

   803       qed

   804     next

   805       assume "(Th th1, c) \<in> RAG s"

   806       with h2 eq_c

   807       have "th1 \<in> children s th2"

   808         by (auto simp:children_def child_def)

   809       thus ?thesis by auto

   810     qed

   811   next

   812     assume "(Th th1, Th th2) \<in> RAG s"

   813     thus ?thesis

   814       by (auto simp:s_RAG_def)

   815   qed

   816 qed

   817 

   818 lemma sub_child: "child s \<subseteq> (RAG s)^+"

   819   by (unfold child_def, auto)

   820 

   821 lemma wf_child: 

   822   assumes vt: "vt s"

   823   shows "wf (child s)"

   824 apply(rule wf_subset)

   825 apply(rule wf_trancl[OF wf_RAG[OF vt]])

   826 apply(rule sub_child)

   827 done

   828 

   829 lemma RAG_child_pre:

   830   assumes vt: "vt s"

   831   shows

   832   "(Th th, n) \<in> (RAG s)^+ \<longrightarrow> (\<forall> th'. n = (Th th') \<longrightarrow> (Th th, Th th') \<in> (child s)^+)" (is "?P n")

   833 proof -

   834   from wf_trancl[OF wf_RAG[OF vt]]

   835   have wf: "wf ((RAG s)^+)" .

   836   show ?thesis

   837   proof(rule wf_induct[OF wf, of ?P], clarsimp)

   838     fix th'

   839     assume ih[rule_format]: "\<forall>y. (y, Th th') \<in> (RAG s)\<^sup>+ \<longrightarrow>

   840                (Th th, y) \<in> (RAG s)\<^sup>+ \<longrightarrow> (\<forall>th'. y = Th th' \<longrightarrow> (Th th, Th th') \<in> (child s)\<^sup>+)"

   841     and h: "(Th th, Th th') \<in> (RAG s)\<^sup>+"

   842     show "(Th th, Th th') \<in> (child s)\<^sup>+"

   843     proof -

   844       from RAG_children[OF h]

   845       have "th \<in> children s th' \<or> (\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+)" .

   846       thus ?thesis

   847       proof

   848         assume "th \<in> children s th'"

   849         thus "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)

   850       next

   851         assume "\<exists>th3. th3 \<in> children s th' \<and> (Th th, Th th3) \<in> (RAG s)\<^sup>+"

   852         then obtain th3 where th3_in: "th3 \<in> children s th'" 

   853           and th_dp: "(Th th, Th th3) \<in> (RAG s)\<^sup>+" by auto

   854         from th3_in have "(Th th3, Th th') \<in> (RAG s)^+" by (auto simp:children_def child_def)

   855         from ih[OF this th_dp, of th3] have "(Th th, Th th3) \<in> (child s)\<^sup>+" by simp

   856         with th3_in show "(Th th, Th th') \<in> (child s)\<^sup>+" by (auto simp:children_def)

   857       qed

   858     qed

   859   qed

   860 qed

   861 

   862 lemma RAG_child: "\<lbrakk>vt s; (Th th, Th th') \<in> (RAG s)^+\<rbrakk> \<Longrightarrow> (Th th, Th th') \<in> (child s)^+"

   863   by (insert RAG_child_pre, auto)

   864 

   865 lemma child_RAG_p:

   866   assumes "(n1, n2) \<in> (child s)^+"

   867   shows "(n1, n2) \<in> (RAG s)^+"

   868 proof -

   869   from assms show ?thesis

   870   proof(induct)

   871     case (base y)

   872     with sub_child show ?case by auto

   873   next

   874     case (step y z)

   875     assume "(y, z) \<in> child s"

   876     with sub_child have "(y, z) \<in> (RAG s)^+" by auto

   877     moreover have "(n1, y) \<in> (RAG s)^+" by fact

   878     ultimately show ?case by auto

   879   qed

   880 qed

   881 

   882 text {* (* ddd *)

   883 *}

   884 lemma child_RAG_eq: 

   885   assumes vt: "vt s"

   886   shows "(Th th1, Th th2) \<in> (child s)^+  \<longleftrightarrow> (Th th1, Th th2) \<in> (RAG s)^+"

   887   by (auto intro: RAG_child[OF vt] child_RAG_p)

   888 

   889 text {* (* ddd *)

   890 *}

   891 lemma children_no_dep:

   892   fixes s th th1 th2 th3

   893   assumes vt: "vt s"

   894   and ch1: "(Th th1, Th th) \<in> child s"

   895   and ch2: "(Th th2, Th th) \<in> child s"

   896   and ch3: "(Th th1, Th th2) \<in> (RAG s)^+"

   897   shows "False"

   898 proof -

   899   from RAG_child[OF vt ch3]

   900   have "(Th th1, Th th2) \<in> (child s)\<^sup>+" .

   901   thus ?thesis

   902   proof(rule converse_tranclE)

   903     assume "(Th th1, Th th2) \<in> child s"

   904     from child_unique[OF vt ch1 this] have "th = th2" by simp

   905     with ch2 have "(Th th2, Th th2) \<in> child s" by simp

   906     with wf_child[OF vt] show ?thesis by auto

   907   next

   908     fix c

   909     assume h1: "(Th th1, c) \<in> child s"

   910       and h2: "(c, Th th2) \<in> (child s)\<^sup>+"

   911     from h1 obtain th3 where eq_c: "c = Th th3" by (unfold child_def, auto)

   912     with h1 have "(Th th1, Th th3) \<in> child s" by simp

   913     from child_unique[OF vt ch1 this] have eq_th3: "th3 = th" by simp

   914     with eq_c and h2 have "(Th th, Th th2) \<in> (child s)\<^sup>+" by simp

   915     with ch2 have "(Th th, Th th) \<in> (child s)\<^sup>+" by auto

   916     moreover have "wf ((child s)\<^sup>+)"

   917     proof(rule wf_trancl)

   918       from wf_child[OF vt] show "wf (child s)" .

   919     qed

   920     ultimately show False by auto

   921   qed

   922 qed

   923 

   924 text {* (* ddd *)

   925 *}

   926 lemma unique_RAG_p:

   927   assumes vt: "vt s"

   928   and dp1: "(n, n1) \<in> (RAG s)^+"

   929   and dp2: "(n, n2) \<in> (RAG s)^+"

   930   and neq: "n1 \<noteq> n2"

   931   shows "(n1, n2) \<in> (RAG s)^+ \<or> (n2, n1) \<in> (RAG s)^+"

   932 proof(rule unique_chain [OF _ dp1 dp2 neq])

   933   from unique_RAG[OF vt]

   934   show "\<And>a b c. \<lbrakk>(a, b) \<in> RAG s; (a, c) \<in> RAG s\<rbrakk> \<Longrightarrow> b = c" by auto

   935 qed

   936 

   937 text {* (* ddd *)

   938 *}

   939 lemma dependants_child_unique:

   940   fixes s th th1 th2 th3

   941   assumes vt: "vt s"

   942   and ch1: "(Th th1, Th th) \<in> child s"

   943   and ch2: "(Th th2, Th th) \<in> child s"

   944   and dp1: "th3 \<in> dependants s th1"

   945   and dp2: "th3 \<in> dependants s th2"

   946 shows "th1 = th2"

   947 proof -

   948   { assume neq: "th1 \<noteq> th2"

   949     from dp1 have dp1: "(Th th3, Th th1) \<in> (RAG s)^+" 

   950       by (simp add:s_dependants_def eq_RAG)

   951     from dp2 have dp2: "(Th th3, Th th2) \<in> (RAG s)^+" 

   952       by (simp add:s_dependants_def eq_RAG)

   953     from unique_RAG_p[OF vt dp1 dp2] and neq

   954     have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ \<or> (Th th2, Th th1) \<in> (RAG s)\<^sup>+" by auto

   955     hence False

   956     proof

   957       assume "(Th th1, Th th2) \<in> (RAG s)\<^sup>+ "

   958       from children_no_dep[OF vt ch1 ch2 this] show ?thesis .

   959     next

   960       assume " (Th th2, Th th1) \<in> (RAG s)\<^sup>+"

   961       from children_no_dep[OF vt ch2 ch1 this] show ?thesis .

   962     qed

   963   } thus ?thesis by auto

   964 qed

   965 

   966 lemma RAG_plus_elim:

   967   assumes "vt s"

   968   fixes x

   969   assumes "(Th x, Th th) \<in> (RAG (wq s))\<^sup>+"

   970   shows "\<exists>th'\<in>children s th. x = th' \<or> (Th x, Th th') \<in> (RAG (wq s))\<^sup>+"

   971   using assms(2)[unfolded eq_RAG, folded child_RAG_eq[OF `vt s`]]

   972   apply (unfold children_def)

   973   by (metis assms(2) children_def RAG_children eq_RAG)

   974 

   975 text {* (* ddd *)

   976 *}

   977 lemma dependants_expand:

   978   assumes "vt s"

   979   shows "dependants (wq s) th = (children s th) \<union> (\<Union>((dependants (wq s)) ` children s th))"

   980 apply(simp add: image_def)

   981 unfolding cs_dependants_def

   982 apply(auto)

   983 apply (metis assms RAG_plus_elim mem_Collect_eq)

   984 apply (metis child_RAG_p children_def eq_RAG mem_Collect_eq r_into_trancl')

   985 by (metis assms child_RAG_eq children_def eq_RAG mem_Collect_eq trancl.trancl_into_trancl)

   986 

   987 lemma finite_children:

   988   assumes "vt s"

   989   shows "finite (children s th)"

   990   using children_dependants dependants_threads[OF assms] finite_threads[OF assms]

   991   by (metis rev_finite_subset)

   992   

   993 lemma finite_dependants:

   994   assumes "vt s"

   995   shows "finite (dependants (wq s) th')"

   996   using dependants_threads[OF assms] finite_threads[OF assms]

   997   by (metis rev_finite_subset)

   998 

   999 abbreviation

  1000   "preceds s ths \<equiv> {preced th s| th. th \<in> ths}"

  1001 

  1002 abbreviation

  1003   "cpreceds s ths \<equiv> (cp s) ` ths"

  1004 

  1005 lemma Un_compr:

  1006   "{f th | th. R th \<or> Q th} = ({f th | th. R th} \<union> {f th' | th'. Q th'})"

  1007 by auto

  1008 

  1009 lemma in_disj:

  1010   shows "x \<in> A \<or> (\<exists>y \<in> A. x \<in> Q y) \<longleftrightarrow> (\<exists>y \<in> A. x = y \<or> x \<in> Q y)"

  1011 by metis

  1012 

  1013 lemma UN_exists:

  1014   shows "(\<Union>x \<in> A. {f y | y. Q y x}) = ({f y | y. (\<exists>x \<in> A. Q y x)})"

  1015 by auto

  1016 

  1017 text {* (* ddd *)

  1018   This is the recursive equation used to compute the current precedence of 

  1019   a thread (the @{text "th"}) here. 

  1020 *}

  1021 lemma cp_rec:

  1022   fixes s th

  1023   assumes vt: "vt s"

  1024   shows "cp s th = Max ({preced th s} \<union> (cp s ` children s th))"

  1025 proof(cases "children s th = {}")

  1026   case True

  1027   show ?thesis

  1028     unfolding cp_eq_cpreced cpreced_def 

  1029     by (subst dependants_expand[OF `vt s`]) (simp add: True)

  1030 next

  1031   case False

  1032   show ?thesis (is "?LHS = ?RHS")

  1033   proof -

  1034     have eq_cp: "cp s = (\<lambda>th. Max (preceds s ({th} \<union> dependants (wq s) th)))"

  1035       by (simp add: fun_eq_iff cp_eq_cpreced cpreced_def Un_compr image_Collect[symmetric])

  1036   

  1037     have not_emptyness_facts[simp]: 

  1038       "dependants (wq s) th \<noteq> {}" "children s th \<noteq> {}"

  1039       using False dependants_expand[OF assms] by(auto simp only: Un_empty)

  1040 

  1041     have finiteness_facts[simp]:

  1042       "\<And>th. finite (dependants (wq s) th)" "\<And>th. finite (children s th)"

  1043       by (simp_all add: finite_dependants[OF `vt s`] finite_children[OF `vt s`])

  1044 

  1045     (* expanding definition *)

  1046     have "?LHS = Max ({preced th s} \<union> preceds s (dependants (wq s) th))"

  1047       unfolding eq_cp by (simp add: Un_compr)

  1048     

  1049     (* moving Max in *)

  1050     also have "\<dots> = max (Max {preced th s}) (Max (preceds s (dependants (wq s) th)))"

  1051       by (simp add: Max_Un)

  1052 

  1053     (* expanding dependants *)

  1054     also have "\<dots> = max (Max {preced th s}) 

  1055       (Max (preceds s (children s th \<union> \<Union>(dependants (wq s) ` children s th))))"

  1056       by (subst dependants_expand[OF `vt s`]) (simp)

  1057 

  1058     (* moving out big Union *)

  1059     also have "\<dots> = max (Max {preced th s})

  1060       (Max (preceds s (\<Union> ({children s th} \<union> (dependants (wq s) ` children s th)))))"  

  1061       by simp

  1062 

  1063     (* moving in small union *)

  1064     also have "\<dots> = max (Max {preced th s})

  1065       (Max (preceds s (\<Union> ((\<lambda>th. {th} \<union> (dependants (wq s) th)) ` children s th))))"  

  1066       by (simp add: in_disj)

  1067 

  1068     (* moving in preceds *)

  1069     also have "\<dots> = max (Max {preced th s})  

  1070       (Max (\<Union> ((\<lambda>th. preceds s ({th} \<union> (dependants (wq s) th))) ` children s th)))" 

  1071       by (simp add: UN_exists)

  1072 

  1073     (* moving in Max *)

  1074     also have "\<dots> = max (Max {preced th s})  

  1075       (Max ((\<lambda>th. Max (preceds s ({th} \<union> (dependants (wq s) th)))) ` children s th))" 

  1076        by (subst Max_Union) (auto simp add: image_image) 

  1077 

  1078     (* folding cp + moving out Max *)

  1079     also have "\<dots> = ?RHS" 

  1080       unfolding eq_cp by (simp add: Max_insert)

  1081 

  1082     finally show "?LHS = ?RHS" .

  1083   qed

  1084 qed

  1085 

  1258   from readys_in_no_subtree[OF step_back_vt[OF vt_s[unfolded s_def]] this assms(1)]

   763   find_theorems readys subtree

   764   from vat_s'.readys_in_no_subtree[OF this assms(1)]

  1320   from readys_root[OF vt_s' ready_th_s']

   812   from vat_s'.readys_root[OF ready_th_s']

  1345   proof(rule RTree.rtree.ancestors_accum[OF rtree_RAGs'])

   836   proof(rule vat_s'.rtree_RAG.ancestors_accum)

  1418                 using next_th_RAG[OF vt_s' nt] .

   908                 using next_th_RAG[OF vat_s'.vt nt]  .

  1424   proof(rule  RTree.rtree.ancestors_accum[OF rtree_RAGs'])

   914   proof(rule  vat_s'.rtree_RAG.ancestors_accum)

  1555 proof(unfold RAG_s, fold subtree_cs, rule RTree.rtree.subtree_del_inside[OF rtree_RAGs'])

  1045 find_theorems "subtree" "_ - _" RAG

  1046 proof(unfold RAG_s, fold subtree_cs, rule vat_s'.rtree_RAG.subtree_del_inside)

  1611   using readys_root[OF vat_s'.vt readys_th] .

  1091   using readys_root[OF readys_th] .

  2042       from readys_in_no_subtree[OF vat_s'.vt th_ready assms]

  1522     find_theorems readys subtree s'

  1523       from vat_s'.readys_in_no_subtree[OF th_ready assms]