--- a/PIPBasics.thy Tue Jun 14 15:06:16 2016 +0100
+++ b/PIPBasics.thy Fri Jun 17 09:46:25 2016 +0100
@@ -1,5 +1,5 @@
theory PIPBasics
-imports PIPDefs
+imports PIPDefs RTree
begin
text {* (* ddd *)
@@ -147,7 +147,7 @@
obtain th' where "th' \<in> set (wq s cs)" "th' = hd (wq s cs)"
by (metis empty_iff hd_in_set list.set(1))
hence "holding s th' cs"
- by (unfold s_holding_def, fold wq_def, auto)
+ unfolding s_holding_def by auto
from that[OF this] show ?thesis .
qed
@@ -159,7 +159,7 @@
*}
lemma children_RAG_alt_def:
"children (RAG (s::state)) (Th th) = Cs ` {cs. holding s th cs}"
- by (unfold s_RAG_def, auto simp:children_def holding_eq)
+ by (unfold s_RAG_def, auto simp:children_def s_holding_abv)
text {*
The following two lemmas relate @{term holdents} and @{term cntCS}
@@ -279,8 +279,8 @@
lemma in_RAG_E:
assumes "(n1, n2) \<in> RAG (s::state)"
obtains (waiting) th cs where "n1 = Th th" "n2 = Cs cs" "waiting s th cs"
- | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
- using assms[unfolded s_RAG_def, folded waiting_eq holding_eq]
+ | (holding) th cs where "n1 = Cs cs" "n2 = Th th" "holding s th cs"
+ using assms[unfolded s_RAG_def, folded s_waiting_abv s_holding_abv]
by auto
text {*
@@ -584,8 +584,8 @@
thus ?thesis by simp
qed
thus ?thesis
- by (metis (no_types, lifting) cp_eq cpreced_def eq_dependants
- f_image_eq the_preced_def)
+ by (metis (no_types, lifting) cp_eq cpreced_def2 f_image_eq
+ s_dependants_abv the_preced_def)
qed
text {*
@@ -625,7 +625,7 @@
from h1 have "cs' = cs" by simp
from assms(2) cs_in[unfolded this]
have "holding s th'' cs" "holding s th2 cs"
- by (unfold s_RAG_def, fold holding_eq, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, auto)
from held_unique[OF this]
show ?thesis by simp
qed
@@ -990,9 +990,9 @@
obtain rest where eq_wq: "wq s cs = th#rest" by blast
with otherwise
have "holding s th cs"
- by (unfold s_holding_def, fold wq_def, simp)
+ unfolding s_holding_def by auto
hence cs_th_RAG: "(Cs cs, Th th) \<in> RAG s"
- by (unfold s_RAG_def, fold holding_eq, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, auto)
from pip_e[unfolded is_p]
show False
proof(cases)
@@ -1033,8 +1033,8 @@
proof(cases)
case (thread_V)
from this(2) show ?thesis
- by (unfold rest_def s_holding_def, fold wq_def,
- metis empty_iff list.collapse list.set(1))
+ unfolding s_holding_def
+ by (metis empty_iff empty_set hd_Cons_tl rest_def)
qed
qed
@@ -1168,8 +1168,9 @@
proof -
from pip_e[unfolded is_exit]
show ?thesis
- by (cases, unfold holdents_def s_holding_def, fold wq_def,
- auto elim!:running_wqE)
+ apply(cases)
+ unfolding holdents_def s_holding_def
+ by (metis (mono_tags, lifting) empty_iff list.sel(1) mem_Collect_eq running_wqE)
qed
lemma wq_threads_kept:
@@ -1562,7 +1563,7 @@
proof -
from assms(1) have "wq (e#s) c = wq s c" by auto
from assms(2)[unfolded s_holding_def, folded wq_def,
- folded this, unfolded wq_def, folded s_holding_def]
+ folded this, folded s_holding_def]
show ?thesis .
qed
@@ -1624,7 +1625,7 @@
lemma holding_taker:
shows "holding (e#s) taker cs"
- by (unfold s_holding_def, fold wq_def, unfold wq_es_cs,
+ by (unfold s_holding_def, unfold wq_es_cs,
auto simp:neq_wq' taker_def)
lemma waiting_esI2:
@@ -1692,7 +1693,7 @@
case False
hence "wq (e#s) c = wq s c" by auto
from assms[unfolded s_holding_def, folded wq_def,
- unfolded this, unfolded wq_def, folded s_holding_def]
+ unfolded this, folded s_holding_def]
have "holding s t c" .
from that(2)[OF False this] show ?thesis .
qed
@@ -1795,7 +1796,7 @@
case False
hence "wq (e#s) c = wq s c" by auto
from assms[unfolded s_holding_def, folded wq_def,
- unfolded this, unfolded wq_def, folded s_holding_def]
+ unfolded this, folded s_holding_def]
have "holding s t c" .
from that[OF False this] show ?thesis .
qed
@@ -1829,13 +1830,13 @@
with waiting(1,2)
show ?thesis
by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
- fold waiting_eq, auto)
+ fold s_waiting_abv, auto)
next
case 2
with waiting(1,2)
show ?thesis
by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
- fold waiting_eq, auto)
+ fold s_waiting_abv, auto)
qed
next
case True
@@ -1848,7 +1849,7 @@
with waiting(1,2)
show ?thesis
by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def,
- fold waiting_eq, auto)
+ fold s_waiting_abv, auto)
qed
qed
next
@@ -1865,13 +1866,13 @@
with holding(1,2)
show ?thesis
by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
- fold waiting_eq, auto)
+ fold s_waiting_abv, auto)
next
case 2
with holding(1,2)
show ?thesis
by (unfold h_n.waiting_set_eq h_n.holding_set_eq s_RAG_def,
- fold holding_eq, auto)
+ fold s_holding_abv, auto)
qed
next
case True
@@ -1884,7 +1885,7 @@
with holding(1,2)
show ?thesis
by (unfold h_e.waiting_set_eq h_e.holding_set_eq s_RAG_def,
- fold holding_eq, auto)
+ fold s_holding_abv, auto)
qed
qed
qed
@@ -1906,7 +1907,7 @@
assume "n2 = Th h_n.taker \<and> n1 = Cs cs"
with h_n.holding_taker
show ?thesis
- by (unfold s_RAG_def, fold holding_eq, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, auto)
next
assume h: "(n1, n2) \<in> RAG s \<and>
(n1 \<noteq> Cs cs \<or> n2 \<noteq> Th th) \<and> (n1 \<noteq> Th h_n.taker \<or> n2 \<noteq> Cs cs)"
@@ -1935,7 +1936,7 @@
qed
qed
thus ?thesis using waiting(1,2)
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
next
case (holding th' cs')
from h this(1,2)
@@ -1951,7 +1952,7 @@
show ?thesis .
qed
thus ?thesis using holding(1,2)
- by (unfold s_RAG_def, fold holding_eq, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, auto)
qed
qed
next
@@ -1967,7 +1968,7 @@
case (waiting th' cs')
from h_e.waiting_esI2[OF this(3)]
show ?thesis using waiting(1,2)
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
next
case (holding th' cs')
with h_s(2)
@@ -1977,12 +1978,12 @@
assume neq_cs: "cs' \<noteq> cs"
from holding_esI2[OF this holding(3)]
show ?thesis using holding(1,2)
- by (unfold s_RAG_def, fold holding_eq, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, auto)
next
assume "th' \<noteq> th"
from holding_esI1[OF holding(3) this]
show ?thesis using holding(1,2)
- by (unfold s_RAG_def, fold holding_eq, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, auto)
qed
qed
qed
@@ -2006,7 +2007,7 @@
proof(cases "cs' = cs")
case False
hence "wq (e#s) cs' = wq s cs'" by simp
- with assms show ?thesis unfolding holding_raw_def holding_eq by auto
+ with assms show ?thesis unfolding holding_raw_def s_holding_abv by auto
next
case True
from assms[unfolded s_holding_def, folded wq_def]
@@ -2015,7 +2016,7 @@
hence "wq (e#s) cs' = th'#(rest@[th])"
by (simp add: True wq_es_cs)
thus ?thesis
- by (simp add: holding_raw_def holding_eq)
+ by (simp add: holding_raw_def s_holding_abv)
qed
end
@@ -2038,11 +2039,11 @@
proof -
from wq_es_cs'
have "th \<in> set (wq (e#s) cs)" "th = hd (wq (e#s) cs)" by auto
- thus ?thesis unfolding holding_raw_def holding_eq by blast
+ thus ?thesis unfolding holding_raw_def s_holding_abv by blast
qed
lemma RAG_edge: "(Cs cs, Th th) \<in> RAG (e#s)"
- by (unfold s_RAG_def, fold holding_eq, insert holding_es_th_cs, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, insert holding_es_th_cs, auto)
lemma waiting_esE:
assumes "waiting (e#s) th' cs'"
@@ -2063,7 +2064,7 @@
next
case False
have "holding s th' cs'" using assms
- using False unfolding holding_raw_def holding_eq by auto
+ using False unfolding holding_raw_def s_holding_abv by auto
from that(1)[OF False this] show ?thesis .
qed
@@ -2079,7 +2080,7 @@
proof(cases rule:waiting_esE)
case 1
thus ?thesis using waiting(1,2)
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
qed
next
case (holding th' cs')
@@ -2088,7 +2089,7 @@
proof(cases rule:holding_esE)
case 1
with holding(1,2)
- show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
+ show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto)
next
case 2
with holding(1,2) show ?thesis by auto
@@ -2106,18 +2107,18 @@
case (waiting th' cs')
from waiting_kept[OF this(3)]
show ?thesis using waiting(1,2)
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
next
case (holding th' cs')
from holding_kept[OF this(3)]
show ?thesis using holding(1,2)
- by (unfold s_RAG_def, fold holding_eq, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, auto)
qed
next
assume "n1 = Cs cs \<and> n2 = Th th"
with holding_es_th_cs
show ?thesis
- by (unfold s_RAG_def, fold holding_eq, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, auto)
qed
qed
@@ -2133,11 +2134,12 @@
by (simp add: wq_es_cs wq_s_cs)
lemma waiting_es_th_cs: "waiting (e#s) th cs"
- using th_not_in_wq waiting_eq wq_es_cs' wq_s_cs
- by (simp add: s_waiting_def wq_def wq_es_cs)
+ using th_not_in_wq s_waiting_abv wq_es_cs' wq_s_cs
+ using Un_iff list.sel(1) list.set_intros(1) s_waiting_def
+ set_append wq_def wq_es_cs by auto
lemma RAG_edge: "(Th th, Cs cs) \<in> RAG (e#s)"
- by (unfold s_RAG_def, fold waiting_eq, insert waiting_es_th_cs, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, insert waiting_es_th_cs, auto)
lemma holding_esE:
assumes "holding (e#s) th' cs'"
@@ -2187,7 +2189,7 @@
proof(cases rule:waiting_esE)
case 1
thus ?thesis using waiting(1,2)
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
next
case 2
thus ?thesis using waiting(1,2) by auto
@@ -2199,7 +2201,7 @@
proof(cases rule:holding_esE)
case 1
with holding(1,2)
- show ?thesis by (unfold s_RAG_def, fold holding_eq, auto)
+ show ?thesis by (unfold s_RAG_def, fold s_holding_abv, auto)
qed
qed
next
@@ -2214,12 +2216,12 @@
case (waiting th' cs')
from waiting_kept[OF this(3)]
show ?thesis using waiting(1,2)
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
next
case (holding th' cs')
from holding_kept[OF this(3)]
show ?thesis using holding(1,2)
- by (unfold s_RAG_def, fold holding_eq, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, auto)
qed
next
assume "n1 = Th th \<and> n2 = Cs cs"
@@ -2620,7 +2622,7 @@
"(Th taker, Cs cs') \<in> RAG s"
by (unfold s_RAG_def, auto)
from this(2) have "waiting s taker cs'"
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
from waiting_unique[OF this waiting_taker]
have "cs' = cs" .
from h(1)[unfolded this] show False by auto
@@ -2655,7 +2657,7 @@
obtain cs' where h: "(Th th, Cs cs') \<in> RAG s"
by (unfold s_RAG_def, auto)
hence "waiting s th cs'"
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
with th_not_waiting show False by auto
qed
ultimately show ?thesis by auto
@@ -2784,7 +2786,7 @@
begin
lemma unique_RAG: "\<lbrakk>(n, n1) \<in> RAG s; (n, n2) \<in> RAG s\<rbrakk> \<Longrightarrow> n1 = n2"
- apply(unfold s_RAG_def, auto, fold waiting_eq holding_eq)
+ apply(unfold s_RAG_def, auto, fold s_waiting_abv s_holding_abv)
by(auto elim:waiting_unique held_unique)
lemma sgv_RAG: "single_valued (RAG s)"
@@ -2962,11 +2964,11 @@
obtain n where "(n, b) \<in> RAG s" by auto
from this[unfolded Cs]
obtain th1 where "waiting s th1 cs"
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
from waiting_holding[OF this]
obtain th2 where "holding s th2 cs" .
hence "(Cs cs, Th th2) \<in> RAG s"
- by (unfold s_RAG_def, fold holding_eq, auto)
+ by (unfold s_RAG_def, fold s_holding_abv, auto)
with h_b(2)[unfolded Cs, rule_format]
have False by auto
thus ?thesis by auto
@@ -2975,7 +2977,7 @@
proof -
from h_b(2)[unfolded eq_b]
have "\<forall>cs. \<not> waiting s th' cs"
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
moreover have "th' \<in> threads s"
proof(rule rg_RAG_threads)
from tranclD[OF h_b(1), unfolded eq_b]
@@ -3123,7 +3125,7 @@
have "(Th th1, Th th2) \<in> (RAG s)\<^sup>+" .
from tranclD[OF this]
obtain cs where "waiting s th1 cs"
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
with running_1 show False
by (unfold running_def readys_def, auto)
qed
@@ -3139,7 +3141,7 @@
have "(Th th2, Th th1) \<in> (RAG s)\<^sup>+" .
from tranclD[OF this]
obtain cs where "waiting s th2 cs"
- by (unfold s_RAG_def, fold waiting_eq, auto)
+ by (unfold s_RAG_def, fold s_waiting_abv, auto)
with running_2 show False
by (unfold running_def readys_def, auto)
qed
@@ -3232,7 +3234,7 @@
obtain z where "(Th th1, z) \<in> RAG s" by auto
from this[unfolded s_RAG_def, folded wq_def]
obtain cs' where "waiting s th1 cs'"
- by (auto simp:waiting_eq)
+ by (auto simp:s_waiting_abv)
with assms(1) show False by (auto simp:readys_def)
qed
next
@@ -3251,7 +3253,7 @@
obtain z where "(Th th2, z) \<in> RAG s" by auto
from this[unfolded s_RAG_def, folded wq_def]
obtain cs' where "waiting s th2 cs'"
- by (auto simp:waiting_eq)
+ by (auto simp:s_waiting_abv)
with assms(2) show False by (auto simp:readys_def)
qed
qed
@@ -3425,10 +3427,10 @@
begin
lemma holding_s_holder: "holding s holder cs"
- by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)
+ by (unfold s_holding_def, unfold wq_s_cs, auto)
lemma holding_es_holder: "holding (e#s) holder cs"
- by (unfold s_holding_def, fold wq_def, unfold wq_es_cs wq_s_cs, auto)
+ by (unfold s_holding_def, unfold wq_es_cs wq_s_cs, auto)
lemma holdents_es:
shows "holdents (e#s) th' = holdents s th'" (is "?L = ?R")
@@ -3448,7 +3450,7 @@
hence "wq (e#s) cs' = wq s cs'" by simp
from h[unfolded s_holding_def, folded wq_def, unfolded this]
show ?thesis
- by (unfold s_holding_def, fold wq_def, auto)
+ by (unfold s_holding_def, auto)
qed
hence "cs' \<in> ?R" by (auto simp:holdents_def)
} moreover {
@@ -3467,7 +3469,7 @@
hence "wq s cs' = wq (e#s) cs'" by simp
from h[unfolded s_holding_def, folded wq_def, unfolded this]
show ?thesis
- by (unfold s_holding_def, fold wq_def, auto)
+ by (unfold s_holding_def, auto)
qed
hence "cs' \<in> ?L" by (auto simp:holdents_def)
} ultimately show ?thesis by auto
@@ -3598,7 +3600,7 @@
from h_e[unfolded s_holding_def, folded wq_def, unfolded wq_neq_simp[OF this]]
have "th' \<in> set (wq s cs') \<and> th' = hd (wq s cs')" .
hence "cs' \<in> ?R"
- by (unfold holdents_def s_holding_def, fold wq_def, auto)
+ by (unfold holdents_def s_holding_def, auto)
} moreover {
fix cs'
assume "cs' \<in> ?R"
@@ -3738,7 +3740,7 @@
lemma holding_th_cs_s:
"holding s th cs"
- by (unfold s_holding_def, fold wq_def, unfold wq_s_cs, auto)
+ by (unfold s_holding_def, unfold wq_s_cs, auto)
lemma th_ready_s [simp]: "th \<in> readys s"
using running_th_s
@@ -3931,7 +3933,7 @@
from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)
from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
show ?thesis
- by (unfold holdents_def s_holding_def, fold wq_def, auto)
+ by (unfold holdents_def s_holding_def, auto)
next
case True
from h[unfolded this]
@@ -3950,7 +3952,7 @@
from h have "holding s th' cs'" by (auto simp:holdents_def)
from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
show ?thesis
- by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp)
+ by (unfold holdents_def s_holding_def, insert eq_wq, simp)
next
case True
from h[unfolded this]
@@ -4107,7 +4109,7 @@
from h have "holding (e#s) th' cs'" by (auto simp:holdents_def)
from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
show ?thesis
- by (unfold holdents_def s_holding_def, fold wq_def, auto)
+ by (unfold holdents_def s_holding_def, auto)
next
case True
from h[unfolded this]
@@ -4126,7 +4128,7 @@
from h have "holding s th' cs'" by (auto simp:holdents_def)
from this[unfolded s_holding_def, folded wq_def, unfolded eq_wq]
show ?thesis
- by (unfold holdents_def s_holding_def, fold wq_def, insert eq_wq, simp)
+ by (unfold holdents_def s_holding_def, insert eq_wq, simp)
next
case True
from h[unfolded this]
@@ -4315,14 +4317,12 @@
{ fix cs'
assume h: "cs' \<in> ?L"
hence "cs' \<in> ?R"
- by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_kept, auto)
+ by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
- by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_kept, auto)
+ by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
} ultimately show ?thesis by auto
qed
@@ -4432,7 +4432,7 @@
assume "holding (e # s) th cs'"
from this[unfolded s_holding_def, folded wq_def, unfolded wq_kept]
have "holding s th cs'"
- by (unfold s_holding_def, fold wq_def, auto)
+ by (unfold s_holding_def, auto)
with not_holding_th_s
show False by simp
qed
@@ -4462,14 +4462,12 @@
{ fix cs'
assume h: "cs' \<in> ?L"
hence "cs' \<in> ?R"
- by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_kept, auto)
+ by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
- by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_kept, auto)
+ by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
} ultimately show ?thesis by auto
qed
@@ -4567,14 +4565,12 @@
{ fix cs'
assume h: "cs' \<in> ?L"
hence "cs' \<in> ?R"
- by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_kept, auto)
+ by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
} moreover {
fix cs'
assume h: "cs' \<in> ?R"
hence "cs' \<in> ?L"
- by (unfold holdents_def s_holding_def, fold wq_def,
- unfold wq_kept, auto)
+ by (unfold holdents_def s_holding_def, unfold wq_kept, auto)
} ultimately show ?thesis by auto
qed
@@ -4639,8 +4635,8 @@
proof(induct rule:ind)
case Nil
thus ?case
- by (unfold cntP_def cntV_def pvD_def cntCS_def holdents_def
- s_holding_def, simp)
+ unfolding cntP_def cntV_def pvD_def cntCS_def holdents_def s_holding_def
+ by(simp add: wq_def)
next
case (Cons s e)
interpret vt_e: valid_trace_e s e using Cons by simp
@@ -4772,7 +4768,7 @@
lemma count_eq_tRAG_plus:
assumes "cntP s th = cntV s th"
shows "{th'. (Th th', Th th) \<in> (tRAG s)^+} = {}"
- using assms eq_pv_dependants dependants_alt_def eq_dependants by auto
+ using assms count_eq_RAG_plus dependants_alt_def s_dependants_def by blast
lemma count_eq_tRAG_plus_Th:
assumes "cntP s th = cntV s th"
@@ -4880,7 +4876,7 @@
with dtc
have "th \<in> readys s"
by (unfold readys_def detached_def Field_def Domain_def Range_def,
- auto simp:waiting_eq s_RAG_def)
+ auto simp:s_waiting_abv s_RAG_def)
with cncs_z show ?thesis using cnp_cnv_cncs by (simp add:pvD_def)
next
case False