equal
deleted
inserted
replaced
47 -- {* The internal structure of @{term th}'s precedence is exposed:*} |
47 -- {* The internal structure of @{term th}'s precedence is exposed:*} |
48 and preced_th: "preced th s = Prc prio tm" |
48 and preced_th: "preced th s = Prc prio tm" |
49 |
49 |
50 -- {* @{term s} is a valid trace, so it will inherit all results derived for |
50 -- {* @{term s} is a valid trace, so it will inherit all results derived for |
51 a valid trace: *} |
51 a valid trace: *} |
52 sublocale highest_gen < vat_s: valid_trace "s" |
52 sublocale highest_gen < vat_s?: valid_trace "s" |
53 by (unfold_locales, insert vt_s, simp) |
53 by (unfold_locales, insert vt_s, simp) |
54 |
54 |
55 context highest_gen |
55 context highest_gen |
56 begin |
56 begin |
57 |
57 |
96 assumes vt_t: "vt (t@s)" |
96 assumes vt_t: "vt (t@s)" |
97 and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio" |
97 and create_low: "Create th' prio' \<in> set t \<Longrightarrow> prio' \<le> prio" |
98 and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio" |
98 and set_diff_low: "Set th' prio' \<in> set t \<Longrightarrow> th' \<noteq> th \<and> prio' \<le> prio" |
99 and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th" |
99 and exit_diff: "Exit th' \<in> set t \<Longrightarrow> th' \<noteq> th" |
100 |
100 |
101 sublocale extend_highest_gen < vat_t: valid_trace "t@s" |
101 sublocale extend_highest_gen < vat_t?: valid_trace "t@s" |
102 by (unfold_locales, insert vt_t, simp) |
102 by (unfold_locales, insert vt_t, simp) |
103 |
103 |
104 lemma step_back_vt_app: |
104 lemma step_back_vt_app: |
105 assumes vt_ts: "vt (t@s)" |
105 assumes vt_ts: "vt (t@s)" |
106 shows "vt s" |
106 shows "vt s" |