theory Scheduler_IF

lemma reads_respects_scheduler_cases':
  assumes b: "reads_respects_scheduler aag l P' (f t)"
  assumes b': "\<And>s. Q s \<Longrightarrow> reads_scheduler_cur_domain aag l s \<Longrightarrow> P' s"
  assumes c: "reads_respects_scheduler aag l P'' (f t)"
  assumes c': "\<And>s. Q s \<Longrightarrow> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> P'' s"
  shows "reads_respects_scheduler aag l Q (f t)" apply (rule_tac P="\<lambda>s. reads_scheduler_cur_domain aag l s" in equiv_valid_cases) apply (rule equiv_valid_guard_imp) apply (rule b) apply (simp add: b') apply (rule equiv_valid_guard_imp) apply (rule c) apply (simp add: c') apply (simp add: scheduler_equiv_def domain_fields_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) Q (f t) proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (Q and reads_scheduler_cur_domain aag l) (f t)
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and Q) (f t)
 3. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (4 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q1 (f t)
 2. \<And>s. (Q and reads_scheduler_cur_domain aag l) s \<Longrightarrow> ?Q1 s
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and Q) (f t)
 4. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (3 subgoals):
 1. \<And>s. (Q and reads_scheduler_cur_domain aag l) s \<Longrightarrow> P' s
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and Q) (f t)
 3. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and Q) (f t)
 2. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q4 (f t)
 2. \<And>s. ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and Q) s \<Longrightarrow> ?Q4 s
 3. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (2 subgoals):
 1. \<And>s. ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and Q) s \<Longrightarrow> P'' s
 2. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s = reads_scheduler_cur_domain aag l t proof (prove)
goal:
No subgoals!