theory Tcb_IF

lemma invoke_tcb_reads_respects_f_g:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
    "reads_respects_f_g aag l
       (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag
                        and einvs and simple_sched_action and tcb_inv_wf ti
                        and (\<lambda>s. is_subject aag (cur_thread s))
                        and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti))
       (invoke_tcb ti)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_f_g) apply (rule invoke_tcb_reads_respects_f[OF domains_distinct]) apply (rule doesnt_touch_globalsI) apply (wp invoke_tcb_globals_equiv | clarsimp | assumption | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (2 subgoals):
 1. reads_respects_f_g aag l ?Q (invoke_tcb ti)
 2. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. reads_respects_f aag l ?P3 (invoke_tcb ti)
 2. doesnt_touch_globals ?Q3 (invoke_tcb ti)
 3. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) s \<Longrightarrow> (?P3 and ?Q3) s proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q3 (invoke_tcb ti)
 2. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) s \<Longrightarrow> (silc_inv aag ?st6 and only_timer_irq_inv ?irq6 ?st'6 and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti) and ?Q3) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q3\<rbrace> invoke_tcb ti \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) s \<Longrightarrow> (silc_inv aag ?st6 and only_timer_irq_inv ?irq6 ?st'6 and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti) and ?Q3) s proof (prove)
goal:
No subgoals!