equal
deleted
inserted
replaced
1 theory Correctness |
1 theory Correctness |
2 imports PIPBasics |
2 imports PIPBasics |
3 begin |
3 begin |
4 |
|
5 (* hg cat -r 176 Correctness.thy *) |
|
6 |
4 |
7 lemma actions_of_len_cons [iff]: |
5 lemma actions_of_len_cons [iff]: |
8 "length (actions_of ts (e#t)) \<le> length ((actions_of ts t)) + 1" |
6 "length (actions_of ts (e#t)) \<le> length ((actions_of ts t)) + 1" |
9 by (unfold actions_of_def, simp) |
7 by (unfold actions_of_def, simp) |
10 |
8 |
86 proof - |
84 proof - |
87 have "?L \<le> ?R" |
85 have "?L \<le> ?R" |
88 by (unfold highest, rule Max_ge, |
86 by (unfold highest, rule Max_ge, |
89 auto simp:threads_s finite_threads) |
87 auto simp:threads_s finite_threads) |
90 moreover have "?R \<le> ?L" |
88 moreover have "?R \<le> ?L" |
91 by (unfold vat_s.cp_rec, rule Max_ge, |
89 apply(subst vat_s.cp_rec) |
92 auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) |
90 using cp_rec le_cp by auto |
93 ultimately show ?thesis by auto |
91 ultimately show ?thesis by auto |
94 qed |
92 qed |
95 |
93 |
96 lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)" |
94 lemma highest_cp_preced: "cp s th = Max (the_preced s ` threads s)" |
97 using eq_cp_s_th highest max_cp_eq the_preced_def by presburger |
95 using eq_cp_s_th highest max_cp_eq the_preced_def by presburger |
841 also have "... = (the_preced (t @ s) th)" |
839 also have "... = (the_preced (t @ s) th)" |
842 proof(rule image_Max_subset) |
840 proof(rule image_Max_subset) |
843 show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads) |
841 show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads) |
844 next |
842 next |
845 show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)" |
843 show "the_thread ` subtree (tRAG (t @ s)) (Th th') \<subseteq> threads (t @ s)" |
846 by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in |
844 by (metis DiffI Diff_eq_empty_iff empty_iff readys_threads |
847 the_thread.simps vat_t.subtree_tRAG_thread) |
845 subtree_tG_tRAG th'_in vat_t.subtree_tG_thread) |
848 next |
846 next |
849 show "th \<in> the_thread ` subtree (tRAG (t @ s)) (Th th')" |
847 show "th \<in> the_thread ` subtree (tRAG (t @ s)) (Th th')" |
850 proof - |
848 proof - |
851 have "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp |
849 have "Th th \<in> subtree (tRAG (t @ s)) (Th th')" using dp |
852 by (unfold tRAG_subtree_eq, auto simp:subtree_def) |
850 by (unfold tRAG_subtree_eq, auto simp:subtree_def) |
1311 |
1309 |
1312 lemma occs'_nil [simp]: "occs' Q [] = 0" |
1310 lemma occs'_nil [simp]: "occs' Q [] = 0" |
1313 by (unfold occs'_def, simp) |
1311 by (unfold occs'_def, simp) |
1314 |
1312 |
1315 lemma occs'_cons [simp]: |
1313 lemma occs'_cons [simp]: |
1316 shows "occs' Q (x#xs) = (if Q xs then 1 + occs' Q xs else occs' Q xs)" |
1314 shows "occs' Q (x#xs) = (if Q xs then 1 + occs' Q xs else occs' Q xs)" |
1317 using assms |
|
1318 by (unfold occs'_def, simp) |
1315 by (unfold occs'_def, simp) |
1319 |
1316 |
1320 lemma occs_len': "occs' Q t + occs' (\<lambda>e. \<not> Q e) t = length t" |
1317 lemma occs_len': "occs' Q t + occs' (\<lambda>e. \<not> Q e) t = length t" |
1321 unfolding occs'_def |
1318 unfolding occs'_def |
1322 by (induct t, auto) |
1319 by (induct t, auto) |
1642 (is "?L \<le> ?R") |
1639 (is "?L \<le> ?R") |
1643 proof - |
1640 proof - |
1644 from len_actions_of_sigma[OF finite_blockers] |
1641 from len_actions_of_sigma[OF finite_blockers] |
1645 have "?L = (\<Sum>th'\<in>blockers. length (actions_of {th'} t))" by simp |
1642 have "?L = (\<Sum>th'\<in>blockers. length (actions_of {th'} t))" by simp |
1646 also have "... \<le> ?R" |
1643 also have "... \<le> ?R" |
1647 by (rule Groups_Big.setsum_mono, insert le_span, auto) |
1644 by (simp add: le_span sum_mono) |
1648 finally show ?thesis . |
1645 finally show ?thesis . |
1649 qed |
1646 qed |
1650 |
1647 |
1651 text {* |
1648 text {* |
1652 By combining forgoing lemmas, it is proved that the number of |
1649 By combining forgoing lemmas, it is proved that the number of |