diff -r 8ce9a432680b -r e6b13c7b9494 prio/PrioG.thy --- a/prio/PrioG.thy Mon Apr 23 08:01:37 2012 +0000 +++ b/prio/PrioG.thy Mon Apr 30 15:32:34 2012 +0000 @@ -1114,7 +1114,7 @@ apply (ind_cases "step s (Exit th')") apply (auto simp:runing_def readys_def s_holding_def s_waiting_def holdents_def s_depend_def s_holding_def cs_holding_def) - by (fold wq_def, auto) + done next case (V th' cs') show ?thesis @@ -1354,7 +1354,7 @@ shows "holdents (P th cs#s) th = holdents s th \ {cs}" proof - from assms show ?thesis - unfolding holdents_def step_depend_p[OF vt] by auto + unfolding holdents_test step_depend_p[OF vt] by (auto) qed lemma step_holdents_p_eq: @@ -1364,7 +1364,7 @@ shows "holdents (P th cs#s) th = holdents s th" proof - from assms show ?thesis - unfolding holdents_def step_depend_p[OF vt] by auto + unfolding holdents_test step_depend_p[OF vt] by auto qed @@ -1386,7 +1386,7 @@ ultimately have "x \ (\(x, y). the_cs x) ` depend s" by simp } thus ?thesis by auto qed - ultimately show ?thesis by (unfold holdents_def, auto intro:finite_subset) + ultimately show ?thesis by (unfold holdents_test, auto intro:finite_subset) qed lemma cntCS_v_dec: @@ -1396,12 +1396,12 @@ proof - from step_back_step[OF vtv] have cs_in: "cs \ holdents s thread" - apply (cases, unfold holdents_def s_depend_def, simp) + apply (cases, unfold holdents_test s_depend_def, simp) by (unfold cs_holding_def s_holding_def wq_def, auto) moreover have cs_not_in: "(holdents (V thread cs#s) thread) = holdents s thread - {cs}" apply (insert wq_distinct[OF step_back_vt[OF vtv], of cs]) - apply (unfold holdents_def, unfold step_depend_v[OF vtv], + apply (unfold holdents_test, unfold step_depend_v[OF vtv], auto simp:next_th_def) proof - fix rest @@ -1492,7 +1492,7 @@ from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) have eq_cncs: "cntCS (e#s) th = cntCS s th" - unfolding cntCS_def holdents_def + unfolding cntCS_def holdents_test by (simp add:depend_create_unchanged eq_e) { assume "th \ thread" with eq_readys eq_e @@ -1517,7 +1517,7 @@ from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) have eq_cncs: "cntCS (e#s) th = cntCS s th" - unfolding cntCS_def holdents_def + unfolding cntCS_def holdents_test by (simp add:depend_exit_unchanged eq_e) { assume "th \ thread" with eq_e @@ -1559,7 +1559,7 @@ apply (erule_tac x = cs in allE, auto) by (case_tac "(wq_fun (schs s) cs)", auto) moreover from neq_th eq_e have "cntCS (e # s) th = cntCS s th" - apply (simp add:cntCS_def holdents_def) + apply (simp add:cntCS_def holdents_test) by (unfold step_depend_p [OF vtp], auto) moreover from eq_e neq_th have "cntP (e # s) th = cntP s th" by (simp add:cntP_def count_def) @@ -1594,7 +1594,7 @@ proof(rule card_insert) from finite_holding [OF vt, of thread] show " finite {cs. (Cs cs, Th thread) \ depend s}" - by (unfold holdents_def, simp) + by (unfold holdents_test, simp) qed moreover have "?R - {cs} = ?R" proof - @@ -1609,7 +1609,7 @@ qed thus ?thesis apply (unfold eq_e eq_th cntCS_def) - apply (simp add: holdents_def) + apply (simp add: holdents_test) by (unfold step_depend_p [OF vtp], auto simp:True) qed moreover from is_runing have "th \ readys s" @@ -1637,7 +1637,7 @@ moreover from is_runing have "th \ threads (e#s)" by (unfold eq_e, auto simp:runing_def readys_def eq_th) moreover have "cntCS (e # s) th = cntCS s th" - apply (unfold cntCS_def holdents_def eq_e step_depend_p[OF vtp]) + apply (unfold cntCS_def holdents_test eq_e step_depend_p[OF vtp]) by (auto simp:False) moreover note eq_cnp eq_cnv ih[of th] moreover from is_runing have "th \ readys s" @@ -1734,7 +1734,7 @@ apply (insert step_back_vt[OF vtv]) by (unfold eq_e, rule readys_v_eq [OF _ neq_th eq_wq False], auto) moreover have "cntCS (e#s) th = cntCS s th" - apply (insert neq_th, unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto) + apply (insert neq_th, unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto) proof - have "{csa. (Cs csa, Th th) \ depend s \ csa = cs \ next_th s thread cs th} = {cs. (Cs cs, Th th) \ depend s}" @@ -1796,7 +1796,7 @@ from eq_wq and th_in and neq_hd have "(holdents (e # s) th) = (holdents s th)" apply (unfold eq_e step_depend_v[OF vtv], - auto simp:next_th_def eq_set s_depend_def holdents_def wq_def + auto simp:next_th_def eq_set s_depend_def holdents_test wq_def Let_def cs_holding_def) by (insert wq_distinct[OF step_back_vt[OF vtv], of cs], auto simp:wq_def) thus ?thesis by (simp add:cntCS_def) @@ -1861,7 +1861,7 @@ ultimately show ?thesis using ih by auto qed moreover from True neq_th have "cntCS (e # s) th = 1 + cntCS s th" - apply (unfold cntCS_def holdents_def eq_e step_depend_v[OF vtv], auto) + apply (unfold cntCS_def holdents_test eq_e step_depend_v[OF vtv], auto) proof - show "card {csa. (Cs csa, Th th) \ depend s \ csa = cs} = Suc (card {cs. (Cs cs, Th th) \ depend s})" @@ -1903,7 +1903,7 @@ from eq_e have eq_cnp: "cntP (e#s) th = cntP s th" by (simp add:cntP_def count_def) from eq_e have eq_cnv: "cntV (e#s) th = cntV s th" by (simp add:cntV_def count_def) have eq_cncs: "cntCS (e#s) th = cntCS s th" - unfolding cntCS_def holdents_def + unfolding cntCS_def holdents_test by (simp add:depend_set_unchanged eq_e) from eq_e have eq_readys: "readys (e#s) = readys s" by (simp add:readys_def cs_waiting_def s_waiting_def wq_def, @@ -1930,7 +1930,7 @@ case vt_nil show ?case by (unfold cntP_def cntV_def cntCS_def, - auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def) + auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def) qed qed @@ -1953,7 +1953,7 @@ assume eq_e: "e = Create thread prio" and not_in': "thread \ threads s" have "cntCS (e # s) th = cntCS s th" - apply (unfold eq_e cntCS_def holdents_def) + apply (unfold eq_e cntCS_def holdents_test) by (simp add:depend_create_unchanged) moreover have "th \ threads s" proof - @@ -1965,7 +1965,7 @@ assume eq_e: "e = Exit thread" and nh: "holdents s thread = {}" have eq_cns: "cntCS (e # s) th = cntCS s th" - apply (unfold eq_e cntCS_def holdents_def) + apply (unfold eq_e cntCS_def holdents_test) by (simp add:depend_exit_unchanged) show ?thesis proof(cases "th = thread") @@ -1991,7 +1991,7 @@ ultimately show ?thesis by auto qed hence "cntCS (e # s) th = cntCS s th " - apply (unfold cntCS_def holdents_def eq_e) + apply (unfold cntCS_def holdents_test eq_e) by (unfold step_depend_p[OF vtp], auto) moreover have "cntCS s th = 0" proof(rule ih) @@ -2034,7 +2034,7 @@ qed moreover note neq_th eq_wq ultimately have "cntCS (e # s) th = cntCS s th" - by (unfold eq_e cntCS_def holdents_def step_depend_v[OF vtv], auto) + by (unfold eq_e cntCS_def holdents_test step_depend_v[OF vtv], auto) moreover have "cntCS s th = 0" proof(rule ih) from not_in eq_e show "th \ threads s" by simp @@ -2048,14 +2048,14 @@ from not_in and eq_e have "th \ threads s" by auto from ih [OF this] and eq_e show ?thesis - apply (unfold eq_e cntCS_def holdents_def) + apply (unfold eq_e cntCS_def holdents_test) by (simp add:depend_set_unchanged) qed next case vt_nil show ?case by (unfold cntCS_def, - auto simp:count_def holdents_def s_depend_def wq_def cs_holding_def) + auto simp:count_def holdents_test s_depend_def wq_def cs_holding_def) qed qed @@ -2425,10 +2425,10 @@ moreover have "finite {cs. (Cs cs, Th th) \ depend s}" proof - from finite_holding[OF vt, of th] show ?thesis - by (simp add:holdents_def) + by (simp add:holdents_test) qed ultimately have h: "{cs. (Cs cs, Th th) \ depend s} = {}" - by (unfold cntCS_def holdents_def cs_dependents_def, auto) + by (unfold cntCS_def holdents_test cs_dependents_def, auto) show ?thesis proof(unfold cs_dependents_def) { assume "{th'. (Th th', Th th) \ (depend (wq s))\<^sup>+} \ {}" @@ -2773,10 +2773,20 @@ by (rule image_subsetI, auto intro:h[symmetric]) qed + definition detached :: "state \ thread \ bool" - where "detached s th \ (Th th \ Field (depend s))" + where "detached s th \ (\(\ cs. holding s th cs)) \ (\(\cs. waiting s th cs))" + -thm Field_def +lemma detached_test: + shows "detached s th = (Th th \ Field (depend s))" +apply(simp add: detached_def Field_def) +apply(simp add: s_depend_def) +apply(simp add: s_holding_abv s_waiting_abv) +apply(simp add: Domain_iff Range_iff) +apply(simp add: wq_def) +apply(auto) +done lemma detached_intro: fixes s th @@ -2796,7 +2806,7 @@ assume "th \ threads s" with range_in[OF vt] dm_depend_threads[OF vt] show ?thesis - by (auto simp:detached_def Field_def Domain_def Range_def) + by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def Domain_iff Range_iff) next assume "th \ readys s" moreover have "Th th \ Range (depend s)" @@ -2805,15 +2815,13 @@ have "holdents s th = {}" by (simp add:cntCS_def) thus ?thesis - apply(auto simp:holdents_def) + apply(auto simp:holdents_test) apply(case_tac a) - apply(auto simp:holdents_def s_depend_def) + apply(auto simp:holdents_test s_depend_def) done qed ultimately show ?thesis - apply (auto simp:detached_def Field_def Domain_def readys_def) - apply (case_tac b, auto simp:s_depend_def) - by (erule_tac x = "nat" in allE, simp add: eq_waiting) + by (auto simp add: detached_def s_depend_def s_waiting_abv s_holding_abv wq_def readys_def) qed qed @@ -2829,7 +2837,8 @@ have cncs_z: "cntCS s th = 0" proof - from dtc have "holdents s th = {}" - by (unfold detached_def holdents_def, auto simp:Field_def Domain_def Range_def) + unfolding detached_def holdents_test s_depend_def + by (simp add: s_waiting_abv wq_def s_holding_abv Domain_iff Range_iff) thus ?thesis by (auto simp:cntCS_def) qed show ?thesis