theory Syscall_IF

lemma reads_respects_f_g':
  "\<lbrakk> reads_respects_g aag l P f; \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> \<rbrakk>
     \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and P and Q) f" apply (clarsimp simp: equiv_valid_def2 equiv_valid_2_def reads_equiv_f_g_def reads_equiv_g_def) apply (rule conjI, fastforce) apply (rule conjI, fastforce) apply (rule conjI, fastforce) apply (subst conj_commute, rule conjI, fastforce) apply (rule silc_dom_equiv_trans) apply (rule silc_dom_equiv_sym) apply (rule silc_inv_silc_dom_equiv) apply (erule (1) use_valid, simp) apply (rule silc_inv_silc_dom_equiv) apply (erule (1) use_valid, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reads_equiv_valid_g_inv (affects_equiv aag l) aag P f; \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>\<rbrakk> \<Longrightarrow> reads_respects_f_g aag l (silc_inv aag st and P and Q) f proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> a = aa \<and> reads_equiv aag b ba \<and> globals_equiv b ba \<and> silc_dom_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> reads_equiv aag b ba \<and> globals_equiv b ba \<and> silc_dom_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> globals_equiv b ba \<and> silc_dom_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> silc_dom_equiv aag b ba \<and> affects_equiv aag l b ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> silc_dom_equiv aag b ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> silc_dom_equiv aag b (?t100 s t a b aa ba)
 2. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> silc_dom_equiv aag (?t100 s t a b aa ba) ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> silc_dom_equiv aag (?t100 s t a b aa ba) b
 2. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> silc_dom_equiv aag (?t100 s t a b aa ba) ba proof (prove)
goal (2 subgoals):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> silc_inv aag (?t100 s t a b aa ba) b
 2. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> silc_dom_equiv aag (?t100 s t a b aa ba) ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> silc_dom_equiv aag st ba proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s t. P s \<and> P t \<and> reads_equiv aag s t \<and> globals_equiv s t \<and> affects_equiv aag l s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> reads_equiv aag s' t' \<and> globals_equiv s' t' \<and> affects_equiv aag l s' t'); \<lbrace>silc_inv aag st and Q\<rbrace> f \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (f t); silc_inv aag st s; P s; Q s; silc_inv aag st t; P t; Q t; reads_equiv aag s t; globals_equiv s t; silc_dom_equiv aag s t; affects_equiv aag l s t\<rbrakk> \<Longrightarrow> silc_inv aag st ba proof (prove)
goal:
No subgoals!