# HG changeset patch # User Christian Urban # Date 1506046110 -3600 # Node ID ca4ddf26a7c76ea139a8c9ef2f58efa04da379f5 # Parent 704fd8749dad19a99a2a9e07508aa6c668556a06 updated to Isabelle 2016-1 diff -r 704fd8749dad -r ca4ddf26a7c7 Correctness.thy --- a/Correctness.thy Thu Sep 21 14:33:13 2017 +0100 +++ b/Correctness.thy Fri Sep 22 03:08:30 2017 +0100 @@ -2,8 +2,6 @@ imports PIPBasics begin -(* hg cat -r 176 Correctness.thy *) - lemma actions_of_len_cons [iff]: "length (actions_of ts (e#t)) \ length ((actions_of ts t)) + 1" by (unfold actions_of_def, simp) @@ -88,8 +86,8 @@ by (unfold highest, rule Max_ge, auto simp:threads_s finite_threads) moreover have "?R \ ?L" - by (unfold vat_s.cp_rec, rule Max_ge, - auto simp:the_preced_def vat_s.fsbttRAGs.finite_children) + apply(subst vat_s.cp_rec) + using cp_rec le_cp by auto ultimately show ?thesis by auto qed @@ -843,8 +841,8 @@ show "finite (threads (t @ s))" by (simp add: vat_t.finite_threads) next show "the_thread ` subtree (tRAG (t @ s)) (Th th') \ threads (t @ s)" - by (smt imageE mem_Collect_eq readys_def subsetCE subsetI th'_in - the_thread.simps vat_t.subtree_tRAG_thread) + by (metis DiffI Diff_eq_empty_iff empty_iff readys_threads + subtree_tG_tRAG th'_in vat_t.subtree_tG_thread) next show "th \ the_thread ` subtree (tRAG (t @ s)) (Th th')" proof - @@ -1313,8 +1311,7 @@ by (unfold occs'_def, simp) lemma occs'_cons [simp]: - shows "occs' Q (x#xs) = (if Q xs then 1 + occs' Q xs else occs' Q xs)" - using assms + shows "occs' Q (x#xs) = (if Q xs then 1 + occs' Q xs else occs' Q xs)" by (unfold occs'_def, simp) lemma occs_len': "occs' Q t + occs' (\e. \ Q e) t = length t" @@ -1644,7 +1641,7 @@ from len_actions_of_sigma[OF finite_blockers] have "?L = (\th'\blockers. length (actions_of {th'} t))" by simp also have "... \ ?R" - by (rule Groups_Big.setsum_mono, insert le_span, auto) + by (simp add: le_span sum_mono) finally show ?thesis . qed diff -r 704fd8749dad -r ca4ddf26a7c7 Implementation.thy --- a/Implementation.thy Thu Sep 21 14:33:13 2017 +0100 +++ b/Implementation.thy Fri Sep 22 03:08:30 2017 +0100 @@ -82,7 +82,11 @@ have [simp]: "preceds {th} s = {the_preced s th}" by (unfold the_preced_def, simp) show ?thesis - by (unfold cp_rec cprecs_def, simp add:the_preced_def) + unfolding cprecs_def + apply(subst cp_rec) + apply(simp add: the_preced_def) + done + qed text {* @@ -963,8 +967,11 @@ equals its precedence: *} lemma eq_cp_th: "cp (e#s) th = preced th (e#s)" - by (unfold vat_es.cp_rec children_of_th, simp add:the_preced_def) - + unfolding children_of_th + apply(subst vat_es.cp_rec) + apply(simp add:the_preced_def children_of_th) + done + end text {* diff -r 704fd8749dad -r ca4ddf26a7c7 Journal/Paper.thy --- a/Journal/Paper.thy Thu Sep 21 14:33:13 2017 +0100 +++ b/Journal/Paper.thy Fri Sep 22 03:08:30 2017 +0100 @@ -28,34 +28,40 @@ declare [[show_question_marks = false]] notation (latex output) - Cons ("_::_" [78,77] 73) and - If ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and + Cons ("_::_" [78,77] 73) + +notation (latex output) vt ("valid'_state") and Prc ("'(_, _')") and holding_raw ("holds") and holding ("holds") and - waiting_raw ("waits") and + waiting_raw ("waits") + +notation (latex output) waiting ("waits") and tG_raw ("TDG") and tG ("TDG") and - RAG_raw ("RAG") and + RAG_raw ("RAG") and RAG ("RAG") and - Th ("T") and + Th ("T") + +notation (latex output) Cs ("C") and readys ("ready") and preced ("prec") and preceds ("precs") and cpreced ("cprec") and cpreceds ("cprecs") and - (*wq_fun ("wq") and*) cp ("cprec") and - (*cprec_fun ("cp_fun") and*) - holdents ("resources") and - DUMMY ("\<^raw:\mbox{$\_\!\_$}>") and + holdents ("resources") and cntP ("c\<^bsub>P\<^esub>") and cntV ("c\<^bsub>V\<^esub>") - +notation (latex output) + DUMMY ("\<^latex>\\\mbox{$\\_\\!\\_$}\") + +notation (latex output) + If ("(\<^latex>\\\textrm{\if\<^latex>\}\ (_)/ \<^latex>\\\textrm{\then\<^latex>\}\ (_)/ \<^latex>\\\textrm{\else\<^latex>\}\ (_))" 10) (*>*) section {* Introduction *} diff -r 704fd8749dad -r ca4ddf26a7c7 Max.thy --- a/Max.thy Thu Sep 21 14:33:13 2017 +0100 +++ b/Max.thy Fri Sep 22 03:08:30 2017 +0100 @@ -128,10 +128,11 @@ using assms[simp] proof - have "?L = Max (\(f ` A))" - by (fold Union_image_eq, simp) + by simp also have "... = ?R" by (subst Max_Union, simp+) - finally show ?thesis . + finally show ?thesis + using \Max (UNION A f) = Max (Max ` f ` A)\ by blast qed lemma max_Max_eq: diff -r 704fd8749dad -r ca4ddf26a7c7 PIPBasics.thy --- a/PIPBasics.thy Thu Sep 21 14:33:13 2017 +0100 +++ b/PIPBasics.thy Fri Sep 22 03:08:30 2017 +0100 @@ -173,7 +173,7 @@ lemma last_set_unique: "\last_set th1 s = last_set th2 s; th1 \ threads s; th2 \ threads s\ \ th1 = th2" - apply (induct s, auto) + apply (induct s, auto) by (case_tac a, auto split:if_splits dest:last_set_lt) lemma preced_unique : @@ -1052,7 +1052,7 @@ lemma wq_kept [simp]: shows "wq (e#s) cs' = wq s cs'" - using assms unfolding is_create wq_def + unfolding is_create wq_def by (auto simp:Let_def) lemma wq_distinct_kept: @@ -1066,7 +1066,7 @@ lemma wq_kept [simp]: shows "wq (e#s) cs' = wq s cs'" - using assms unfolding is_exit wq_def + unfolding is_exit wq_def by (auto simp:Let_def) lemma wq_distinct_kept: @@ -1171,7 +1171,7 @@ lemma wq_kept [simp]: shows "wq (e#s) cs' = wq s cs'" - using assms unfolding is_set wq_def + unfolding is_set wq_def by (auto simp:Let_def) lemma wq_distinct_kept: @@ -3720,7 +3720,6 @@ lemma KK: shows "(\x\C. B x) = (\ {B x |x. x \ C})" -(* and "\" *) by (simp_all add: Setcompr_eq_image) lemma Max_Segments: @@ -3731,7 +3730,7 @@ apply(subst Max_Union) apply(auto)[3] apply(simp add: Setcompr_eq_image) -apply(simp add: image_eq_UN) +apply(auto simp add: image_image) done lemma max_cp_readys_max_preced_tG: @@ -4570,7 +4569,7 @@ lemma readys_simp [simp]: shows "(th' \ readys (e#s)) = (th' \ readys s)" - using readys_kept1[OF assms] readys_kept2[OF assms] + using readys_kept1 readys_kept2 by metis lemma cnp_cnv_cncs_kept: @@ -5109,7 +5108,9 @@ assumes eq_pv: "cntP s th = cntV s th" shows "subtree (RAG s) (Th th) = {Th th}" using eq_pv_children[OF assms] - by (unfold subtree_children, simp) + apply(subst subtree_children) + apply(simp) + done lemma count_eq_RAG_plus: assumes "cntP s th = cntV s th" @@ -5320,7 +5321,11 @@ proof(cases "children (tRAG s) x = {}") case True show ?thesis - by (unfold True cp_gen_def subtree_children, simp add:assms) + apply(subst True) + apply(subst cp_gen_def) + apply(subst subtree_children) + apply(simp add: assms) + using True assms by auto next case False hence [simp]: "children (tRAG s) x \ {}" by auto @@ -5349,9 +5354,10 @@ proof - have "?L1 = ?f ` (\ x \ ?B.(?g x))" by simp also have "... = (\ x \ ?B. ?f ` (?g x))" by auto - finally have "Max ?L1 = Max ..." by simp + finally have "Max ?L1 = Max ..." + by (simp add: \(the_preced s \ the_thread) ` (\x\children (tRAG s) x. subtree (tRAG s) x) = (\x\children (tRAG s) x. (the_preced s \ the_thread) ` subtree (tRAG s) x)\) also have "... = Max (Max ` (\x. ?f ` subtree (tRAG s) x) ` ?B)" - by (subst Max_UNION, simp+) + by(subst Max_Union, auto) also have "... = Max (cp_gen s ` children (tRAG s) x)" by (unfold image_comp cp_gen_alt_def, simp) finally show ?thesis . @@ -5486,16 +5492,15 @@ have "?R = length (actions_of {actor e} (e # t)) + (\th'\A - {actor e}. length (actions_of {th'} (e # t)))" (is "_ = ?F (e#t) + ?G (e#t)") - by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", - OF assms True], simp) + by (meson True assms sum.remove) moreover have "?F (e#t) = 1 + ?F t" using True by (simp add:actions_of_def) - moreover have "?G (e#t) = ?G t" - by (rule setsum.cong, auto simp:actions_of_def) + moreover have "?G (e#t) = ?G t" + by (auto simp:actions_of_def) moreover have "?F t + ?G t = ?T t" - by (subst comm_monoid_add_class.setsum.remove[where x = "actor e", - OF assms True], simp) - ultimately show ?thesis by simp + by (metis (no_types, lifting) True assms sum.remove) + ultimately show ?thesis + by simp qed ultimately show ?thesis by simp next @@ -5504,7 +5509,8 @@ by (simp add:actions_of_def) also have "... = (\th'\A. length (actions_of {th'} t))" by (simp add: h) also have "... = ?R" - by (rule setsum.cong; insert False, auto simp:actions_of_def) + unfolding actions_of_def + by (metis (no_types, lifting) False filter.simps(2) singletonD sum.cong) finally show ?thesis . qed qed (auto simp:actions_of_def) diff -r 704fd8749dad -r ca4ddf26a7c7 PIPDefs.thy --- a/PIPDefs.thy Thu Sep 21 14:33:13 2017 +0100 +++ b/PIPDefs.thy Fri Sep 22 03:08:30 2017 +0100 @@ -162,6 +162,7 @@ definition "waiting_raw wq thread cs \ (thread \ set (wq cs) \ thread \ hd (wq cs))" + text {* Resource Allocation Graphs (RAG for short) are used extensively in our diff -r 704fd8749dad -r ca4ddf26a7c7 Precedence_ord.thy --- a/Precedence_ord.thy Thu Sep 21 14:33:13 2017 +0100 +++ b/Precedence_ord.thy Fri Sep 22 03:08:30 2017 +0100 @@ -1,9 +1,9 @@ -header {* Order on product types *} - theory Precedence_ord imports Main begin +section {* Order on product types *} + datatype precedence = Prc nat nat instantiation precedence :: order diff -r 704fd8749dad -r ca4ddf26a7c7 README --- a/README Thu Sep 21 14:33:13 2017 +0100 +++ b/README Fri Sep 22 03:08:30 2017 +0100 @@ -13,7 +13,7 @@ Implementation.thy Properties interesting for an implementation. -The repository can be checked using Isabelle 2013-2. +The repository can be checked using Isabelle 2016. isabelle build -c -v -d . PIP diff -r 704fd8749dad -r ca4ddf26a7c7 ROOT --- a/ROOT Thu Sep 21 14:33:13 2017 +0100 +++ b/ROOT Fri Sep 22 03:08:30 2017 +0100 @@ -1,5 +1,5 @@ session "PIP" = HOL + - theories [document = false, quick_and_dirty] + theories [document = false] "Implementation" "Correctness" diff -r 704fd8749dad -r ca4ddf26a7c7 RTree.thy --- a/RTree.thy Thu Sep 21 14:33:13 2017 +0100 +++ b/RTree.thy Fri Sep 22 03:08:30 2017 +0100 @@ -1496,7 +1496,9 @@ show "finite M" . qed thus ?case - by (unfold subtree_children finite_Un, auto) + apply(subst subtree_children finite_Un) + apply(auto) + done qed end diff -r 704fd8749dad -r ca4ddf26a7c7 journal.pdf Binary file journal.pdf has changed