--- 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)) \<le> 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 \<le> ?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') \<subseteq> 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 \<in> 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' (\<lambda>e. \<not> Q e) t = length t"
@@ -1644,7 +1641,7 @@
from len_actions_of_sigma[OF finite_blockers]
have "?L = (\<Sum>th'\<in>blockers. length (actions_of {th'} t))" by simp
also have "... \<le> ?R"
- by (rule Groups_Big.setsum_mono, insert le_span, auto)
+ by (simp add: le_span sum_mono)
finally show ?thesis .
qed
--- 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 {*
--- 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>\<open>\\mbox{$\\_\\!\\_$}\<close>")
+
+notation (latex output)
+ If ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10)
(*>*)
section {* Introduction *}
--- 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 (\<Union>(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 \<open>Max (UNION A f) = Max (Max ` f ` A)\<close> by blast
qed
lemma max_Max_eq:
--- 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:
"\<lbrakk>last_set th1 s = last_set th2 s; th1 \<in> threads s; th2 \<in> threads s\<rbrakk>
\<Longrightarrow> 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 "(\<Union>x\<in>C. B x) = (\<Union> {B x |x. x \<in> C})"
-(* and "\<Union>" *)
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' \<in> readys (e#s)) = (th' \<in> 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 \<noteq> {}" by auto
@@ -5349,9 +5354,10 @@
proof -
have "?L1 = ?f ` (\<Union> x \<in> ?B.(?g x))" by simp
also have "... = (\<Union> x \<in> ?B. ?f ` (?g x))" by auto
- finally have "Max ?L1 = Max ..." by simp
+ finally have "Max ?L1 = Max ..."
+ by (simp add: \<open>(the_preced s \<circ> the_thread) ` (\<Union>x\<in>children (tRAG s) x. subtree (tRAG s) x) = (\<Union>x\<in>children (tRAG s) x. (the_preced s \<circ> the_thread) ` subtree (tRAG s) x)\<close>)
also have "... = Max (Max ` (\<lambda>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)) +
(\<Sum>th'\<in>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 "... = (\<Sum>th'\<in>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)
--- 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 \<equiv> (thread \<in> set (wq cs) \<and> thread \<noteq> hd (wq cs))"
+
text {*
Resource Allocation Graphs (RAG for short) are used extensively in our
--- 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
--- 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
--- 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"
--- 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
Binary file journal.pdf has changed