theory ADT_IF

lemma ADT_A_if_big_step_R_terminate:
  "rel_terminate (ADT_A_if utf) s0 big_step_R {s. invs_if s} measuref_if" apply (clarsimp simp: rel_terminate_def) apply (rule conjI) apply (rename_tac uc s mode as uc' s' mode' uc'' s'' mode'') apply (rule ADT_A_if_Step_measure_if) apply assumption apply (simp add: invs_if_sub_big_steps_ADT_A_if) apply (rule ADT_A_if_sub_big_steps_measuref_if) apply simp apply (simp add: ADT_A_if_def) apply (simp add: ADT_A_if_def) apply (drule tranclp_s0) apply (fastforce simp: measuref_if_def big_step_R_def Step_ADT_A_if
                         Step_ADT_A_if_def_global_automaton_if global_automaton_if_def
                 split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rel_terminate (ADT_A_if utf) s0 big_step_R (Collect invs_if) measuref_if proof (prove)
goal (1 subgoal):
 1. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((ab, bd), be) ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) < measuref_if ((a, b), ba) ((aa, bb), bc) \<and> (0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg)) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((ab, bd), be) ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) < measuref_if ((a, b), ba) ((aa, bb), bc)
 2. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((ab, bd), be) ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba uc s mode as uc' s' mode' uc'' s'' mode''. \<lbrakk>invs_if ((a, b), ba); ((uc', s'), mode') \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((uc', s'), mode') ((a, b), ba); (((s, mode), as), uc) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> measuref_if ((a, b), ba) ((uc'', s''), mode'') < measuref_if ((a, b), ba) ((s, mode), as)
 2. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((ab, bd), be) ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg) proof (prove)
goal (4 subgoals):
 1. \<And>a b ba uc s mode as uc' s' mode' uc'' s'' mode''. \<lbrakk>invs_if ((a, b), ba); ((uc', s'), mode') \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((uc', s'), mode') ((a, b), ba); (((s, mode), as), uc) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) (?x27 a b ba uc s mode as uc' s' mode' uc'' s'' mode'')
 2. \<And>a b ba uc s mode as uc' s' mode' uc'' s'' mode''. \<lbrakk>invs_if ((a, b), ba); ((uc', s'), mode') \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((uc', s'), mode') ((a, b), ba); (((s, mode), as), uc) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> invs_if ((s, mode), as)
 3. \<And>a b ba uc s mode as uc' s' mode' uc'' s'' mode''. \<lbrakk>invs_if ((a, b), ba); ((uc', s'), mode') \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((uc', s'), mode') ((a, b), ba); (((s, mode), as), uc) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((s, mode), as)
 4. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((ab, bd), be) ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba uc s mode as uc' s' mode' uc'' s'' mode''. \<lbrakk>invs_if ((a, b), ba); ((uc', s'), mode') \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((uc', s'), mode') ((a, b), ba); (((s, mode), as), uc) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> invs_if ((s, mode), as)
 2. \<And>a b ba uc s mode as uc' s' mode' uc'' s'' mode''. \<lbrakk>invs_if ((a, b), ba); ((uc', s'), mode') \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((uc', s'), mode') ((a, b), ba); (((s, mode), as), uc) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((s, mode), as)
 3. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((ab, bd), be) ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba uc s mode as uc' s' mode' uc'' s'' mode''. \<lbrakk>invs_if ((a, b), ba); ((uc', s'), mode') \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((uc', s'), mode') ((a, b), ba); (((s, mode), as), uc) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((s, mode), as)
 2. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((ab, bd), be) ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg) proof (prove)
goal (3 subgoals):
 1. \<And>a b ba uc s mode as uc' s' mode' uc'' s'' mode''. \<lbrakk>invs_if ((a, b), ba); ((uc', s'), mode') \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((uc', s'), mode') ((a, b), ba); (((s, mode), as), uc) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> (((s, mode), as), ?evs31 a b ba uc s mode as uc' s' mode' uc'' s'' mode'') \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba)
 2. \<And>a b ba uc s mode as uc' s' mode' uc'' s'' mode''. \<lbrakk>invs_if ((a, b), ba); ((uc', s'), mode') \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((uc', s'), mode') ((a, b), ba); (((s, mode), as), uc) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 ((a, b), ba)
 3. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((ab, bd), be) ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg) proof (prove)
goal (2 subgoals):
 1. \<And>a b ba uc s mode as uc' s' mode' uc'' s'' mode''. \<lbrakk>invs_if ((a, b), ba); ((uc', s'), mode') \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((uc', s'), mode') ((a, b), ba); (((s, mode), as), uc) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((s, mode), as), (uc'', s''), mode'') \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> big_step_R\<^sup>*\<^sup>* s0 ((a, b), ba)
 2. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((ab, bd), be) ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) \<in> Init (ADT_A_if utf) s0; big_step_R\<^sup>*\<^sup>* ((ab, bd), be) ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps (ADT_A_if utf) big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) = s0 \<and> ((ab, bd), be) \<in> full_invs_if \<and> step_restrict ((ab, bd), be); big_step_R\<^sup>*\<^sup>* s0 ((a, b), ba); (((aa, bb), bc), as) \<in> sub_big_steps \<lparr>Init = \<lambda>s. {s} \<inter> full_invs_if \<inter> {s. step_restrict s}, Fin = id, Step = \<lambda>u. global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<inter> {(s, s'). step_restrict s'}\<rparr> big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<and> step_restrict ((ac, bf), bg)\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba as aa bb bc ab bd be ac bf bg. \<lbrakk>invs_if ((a, b), ba); ((ab, bd), be) = s0 \<and> ((ab, bd), be) \<in> full_invs_if \<and> step_restrict ((ab, bd), be); (((aa, bb), bc), as) \<in> sub_big_steps \<lparr>Init = \<lambda>s. {s} \<inter> full_invs_if \<inter> {s. step_restrict s}, Fin = id, Step = \<lambda>u. global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<inter> {(s, s'). step_restrict s'}\<rparr> big_step_R ((a, b), ba); (((aa, bb), bc), (ac, bf), bg) \<in> global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<and> step_restrict ((ac, bf), bg); interrupted_modes (snd ((a, b), ba)) \<or> snd ((a, b), ba) = KernelExit\<rbrakk> \<Longrightarrow> 0 < measuref_if ((a, b), ba) ((aa, bb), bc) \<longrightarrow> measuref_if ((a, b), ba) ((ac, bf), bg) = 0 \<longrightarrow> big_step_R ((a, b), ba) ((ac, bf), bg) proof (prove)
goal:
No subgoals!