theory Scheduler_IF

lemma midstrength_reads_respects_scheduler_cases:
  assumes domains_distinct: "pas_domains_distinct aag"
  assumes b: "pasObjectAbs aag t \<in> reads_scheduler aag l
              \<Longrightarrow> midstrength_reads_respects_scheduler aag l P' (f t)"
  assumes b': "\<And>s. Q s \<Longrightarrow> pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> P' s"
  assumes c: "pasObjectAbs aag t \<notin> reads_scheduler aag l
              \<Longrightarrow> reads_respects_scheduler aag l P'' (f t)"
  assumes c': "\<And>s. Q s \<Longrightarrow> pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> P'' s"
  assumes d: "\<And>s. Q s \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)"
  shows "midstrength_reads_respects_scheduler aag l Q (f t)" apply (case_tac "pasObjectAbs aag t \<in> reads_scheduler aag l") apply (rule equiv_valid_guard_imp) apply (rule b) apply simp+ apply (rule b') apply simp+ apply (rule equiv_valid_guard_imp) apply (rule midstrength_cur_domain_unobservable) apply (rule equiv_valid_guard_imp) apply (rule c) apply simp+ apply fastforce apply clarsimp apply (rule conjI) apply (rule c') apply simp+ apply (fastforce dest: d domains_distinct[THEN pas_domains_distinct_inj]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l Q (f t) proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l Q (f t)
 2. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l Q (f t) proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l ?Q1 (f t)
 2. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> ?Q1 s
 3. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l Q (f t) proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> pasObjectAbs aag t \<in> reads_scheduler aag l
 2. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> P' s
 3. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l Q (f t) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> P' s
 2. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l Q (f t) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> Q s
 2. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> reads_scheduler aag l
 3. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l Q (f t) proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l Q (f t) proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l ?Q15 (f t)
 2. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> ?Q15 s proof (prove)
goal (2 subgoals):
 1. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (?P18 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) (f t)
 2. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> (?P18 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q20 (f t)
 2. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; (?P18 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s\<rbrakk> \<Longrightarrow> ?Q20 s
 3. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> (?P18 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> pasObjectAbs aag t \<notin> reads_scheduler aag l
 2. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; (?P18 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s\<rbrakk> \<Longrightarrow> P'' s
 3. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> (?P18 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; ?P18 s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}\<rbrakk> \<Longrightarrow> P'' s
 2. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> (?P18 and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> (P'' and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> P'' s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> P'' s
 2. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> Q s
 2. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<notin> reads_scheduler aag l
 3. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; Q s\<rbrakk> \<Longrightarrow> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} proof (prove)
goal:
No subgoals!