regexp: comparison prio/ExtGG.thy

equal deleted inserted replaced

-:0a4be67ea7f8
+:f2e0d031a395
 apply (drule_tac th_in_ne)
 by (unfold preced_def, auto intro: birth_time_lt)
 locale highest_gen =
 fixes s th prio tm
-assumes vt_s: "vt step s"
+assumes vt_s: "vt s"
 and threads_s: "th \<in> threads s"
 and highest: "preced th s = Max ((cp s)`threads s)"
 and preced_th: "preced th s = Prc prio tm"
 context highest_gen
 end
 locale extend_highest_gen = highest_gen +
 fixes t
-assumes vt_t: "vt step (t@s)"
+assumes vt_t: "vt (t@s)"
 and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio"
 and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio"
 and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th"
 lemma step_back_vt_app:
-assumes vt_ts: "vt cs (t@s)"
+assumes vt_ts: "vt (t@s)"
-shows "vt cs s"
+shows "vt s"
 proof -
 from vt_ts show ?thesis
 proof(induct t)
 case Nil
 from Nil show ?case by auto
 next
 case (Cons e t)
-assume ih: " vt cs (t @ s) \<Longrightarrow> vt cs s"
+assume ih: " vt (t @ s) \<Longrightarrow> vt s"
-and vt_et: "vt cs ((e # t) @ s)"
+and vt_et: "vt ((e # t) @ s)"
 show ?case
 proof(rule ih)
-show "vt cs (t @ s)"
+show "vt (t @ s)"
 proof(rule step_back_vt)
-from vt_et show "vt cs (e # t @ s)" by simp
+from vt_et show "vt (e # t @ s)" by simp
 qed
 qed
 qed
 qed
 by (unfold highest_gen_def, auto dest:step_back_vt_app)
 lemma ind [consumes 0, case_names Nil Cons, induct type]:
 assumes
 h0: "R []"
-and h2: "\<And> e t. \<lbrakk>vt step (t@s); step (t@s) e;
+and h2: "\<And> e t. \<lbrakk>vt (t@s); step (t@s) e;
 extend_highest_gen s th prio tm t;
 extend_highest_gen s th prio tm (e#t); R t\<rbrakk> \<Longrightarrow> R (e#t)"
 shows "R t"
 proof -
 from vt_t extend_highest_gen_axioms show ?thesis
 proof(induct t)
 from h0 show "R []" .
 next
 case (Cons e t')
-assume ih: "\<lbrakk>vt step (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"
+assume ih: "\<lbrakk>vt (t' @ s); extend_highest_gen s th prio tm t'\<rbrakk> \<Longrightarrow> R t'"
-and vt_e: "vt step ((e # t') @ s)"
+and vt_e: "vt ((e # t') @ s)"
 and et: "extend_highest_gen s th prio tm (e # t')"
 from vt_e and step_back_step have stp: "step (t'@s) e" by auto
-from vt_e and step_back_vt have vt_ts: "vt step (t'@s)" by auto
+from vt_e and step_back_vt have vt_ts: "vt (t'@s)" by auto
 show ?case
 proof(rule h2 [OF vt_ts stp _ _ _ ])
 show "R t'"
 proof(rule ih)
 from et show ext': "extend_highest_gen s th prio tm t'"
 by (unfold extend_highest_gen_def extend_highest_gen_axioms_def, auto dest:step_back_vt)
 next
-from vt_ts show "vt step (t' @ s)" .
+from vt_ts show "vt (t' @ s)" .
 qed
 next
 from et show "extend_highest_gen s th prio tm (e # t')" .
 next
 from et show ext': "extend_highest_gen s th prio tm t'"
 proof -
 have "Max (?f ` ?A) = Max(insert (?f thread) (?f ` (threads (t@s))))"
 by (unfold eq_e, simp)
 moreover have "\<dots> = max (?f thread) (Max (?f ` (threads (t@s))))"
 proof(rule Max_insert)
-from Cons have "vt step (t @ s)" by auto
+from Cons have "vt (t @ s)" by auto
 from finite_threads[OF this]
 show "finite (?f ` (threads (t@s)))" by simp
 next
 from h' show "(?f ` (threads (t@s))) \<noteq> {}" by auto
 qed
 ultimately show ?thesis by (auto simp:max_def)
 qed
 next
 case (Exit thread)
 assume eq_e: "e = Exit thread"
-from Cons have vt_e: "vt step (e#(t @ s))" by auto
+from Cons have vt_e: "vt (e#(t @ s))" by auto
 from Cons and eq_e have stp: "step (t@s) (Exit thread)" by auto
 from stp have thread_ts: "thread \<in> threads (t @ s)"
 by(cases, unfold runing_def readys_def, auto)
 from Cons have "extend_highest_gen s th prio tm (e # t)" by auto
 from extend_highest_gen.exit_diff[OF this] and eq_e
 from Cons
 have "?t = Max ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"
 (is "?t = Max (?g ` ?B)") by simp
 moreover have "?g thread \<le> \<dots>"
 proof(rule Max_ge)
-have "vt step (t@s)" by fact
+have "vt (t@s)" by fact
 from finite_threads [OF this]
 show "finite (?g ` ?B)" by simp
 next
 from thread_ts
 show "?g thread \<in> (?g ` ?B)" by auto
 show "preced th1 (t @ s) \<in> (\<lambda>th'. preced th' (t @ s)) ` threads (t @ s)"
 by simp
 next
 show "finite ((\<lambda>th'. preced th' (t @ s)) ` threads (t @ s))"
 proof -
-from Cons have "vt step (t @ s)" by auto
+from Cons have "vt (t @ s)" by auto
 from finite_threads[OF this] show ?thesis by auto
 qed
 qed
 ultimately show ?thesis by auto
 qed
 [OF this, OF in_thread neq_th' not_holding]
 have not_runing: "th' \<notin> runing (t @ s)" .
 show ?case
 proof(cases e)
 case (V thread cs)
-from Cons and V have vt_v: "vt step (V thread cs#(t@s))" by auto
+from Cons and V have vt_v: "vt (V thread cs#(t@s))" by auto
 show ?thesis
 proof -
 from Cons and V have "step (t@s) (V thread cs)" by auto
 hence neq_th': "thread \<noteq> th'"
 obtain e where
 eq_me: "moment (Suc(i+k)) t = e#(moment (i+k) t)"
 by blast
 from red_moment[of "Suc(i+k)"]
 and eq_me have "extend_highest_gen s th prio tm (e # moment (i + k) t)" by simp
-hence vt_e: "vt step (e#(moment (i + k) t)@s)"
+hence vt_e: "vt (e#(moment (i + k) t)@s)"
 by (unfold extend_highest_gen_def extend_highest_gen_axioms_def
 highest_gen_def, auto)
 have not_runing': "th' \<notin>  runing (moment (i + k) t @ s)"
 proof -
 show "th' \<notin> runing (moment (i + k) t @ s)"
 from lt_its have "Suc i \<le> length t" by auto
 from moment_head[OF this] obtain e where
 eq_me: "moment (Suc i) t = e # moment i t" by blast
 from red_moment[of "Suc i"] and eq_me
 have "extend_highest_gen s th prio tm (e # moment i t)" by simp
-hence vt_e: "vt step (e#(moment i t)@s)"
+hence vt_e: "vt (e#(moment i t)@s)"
 by (unfold extend_highest_gen_def extend_highest_gen_axioms_def
 highest_gen_def, auto)
 from step_back_step[OF this] have stp_i: "step (moment i t @ s) e" .
 from post[rule_format, of "Suc i"] and eq_me
 have not_in': "th' \<in> threads (e # moment i t@s)" by auto
 from create_pre[OF stp_i pre this]
 obtain prio where eq_e: "e = Create th' prio" .
 have "cntP (moment i t@s) th' = cntV (moment i t@s) th'"
 proof(rule cnp_cnv_eq)
 from step_back_vt [OF vt_e]
-show "vt step (moment i t @ s)" .
+show "vt (moment i t @ s)" .
 next
 from eq_e and stp_i
 have "step (moment i t @ s) (Create th' prio)" by simp
 thus "th' \<notin> threads (moment i t @ s)" by (cases, simp)
 qed

changeset 298	f2e0d031a395
parent 290	6a6d0bd16035
child 302	06241c45cb17