theory L4VerifiedLinks

lemma corres_impl_corresXF:
  "corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) \<top> P G G' \<Longrightarrow>
   corresXF st (\<lambda>_ _. ()) (\<lambda>_ _. ()) P G G'" apply (rule corresXF_I) apply (clarsimp simp: corres_underlying_def corresXF_def) apply (erule allE, erule (1) impE) apply force apply (clarsimp simp: corres_underlying_def corresXF_def) apply (erule allE, erule (1) impE) apply force apply (clarsimp simp: corres_underlying_def corresXF_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G' \<Longrightarrow> corresXF st (\<lambda>_ _. ()) (\<lambda>_ _. ()) P G G' proof (prove)
goal (3 subgoals):
 1. \<And>s' t' r'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s')); (Inr r', t') \<in> fst (G' s')\<rbrakk> \<Longrightarrow> (Inr (), st t') \<in> fst (G (st s'))
 2. \<And>s' t' r'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s')); (Inl r', t') \<in> fst (G' s')\<rbrakk> \<Longrightarrow> (Inl (), st t') \<in> fst (G (st s'))
 3. \<And>s'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s'))\<rbrakk> \<Longrightarrow> \<not> snd (G' s') proof (prove)
goal (3 subgoals):
 1. \<And>s' t' r'. \<lbrakk>\<forall>b. P b \<longrightarrow> (nf \<longrightarrow> \<not> snd (G (st b))) \<longrightarrow> (\<forall>x\<in>fst (G' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (G (st b)). case x of (r, t) \<Rightarrow> t = st t' \<and> (dc \<oplus> dc) r r') \<and> \<not> snd (G' b); P s'; \<not> snd (G (st s')); (Inr r', t') \<in> fst (G' s')\<rbrakk> \<Longrightarrow> (Inr (), st t') \<in> fst (G (st s'))
 2. \<And>s' t' r'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s')); (Inl r', t') \<in> fst (G' s')\<rbrakk> \<Longrightarrow> (Inl (), st t') \<in> fst (G (st s'))
 3. \<And>s'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s'))\<rbrakk> \<Longrightarrow> \<not> snd (G' s') proof (prove)
goal (3 subgoals):
 1. \<And>s' t' r'. \<lbrakk>P s'; \<not> snd (G (st s')); (Inr r', t') \<in> fst (G' s'); (nf \<longrightarrow> \<not> snd (G (st s'))) \<longrightarrow> (\<forall>x\<in>fst (G' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (G (st s')). case x of (r, t) \<Rightarrow> t = st t' \<and> (dc \<oplus> dc) r r') \<and> \<not> snd (G' s')\<rbrakk> \<Longrightarrow> (Inr (), st t') \<in> fst (G (st s'))
 2. \<And>s' t' r'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s')); (Inl r', t') \<in> fst (G' s')\<rbrakk> \<Longrightarrow> (Inl (), st t') \<in> fst (G (st s'))
 3. \<And>s'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s'))\<rbrakk> \<Longrightarrow> \<not> snd (G' s') proof (prove)
goal (2 subgoals):
 1. \<And>s' t' r'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s')); (Inl r', t') \<in> fst (G' s')\<rbrakk> \<Longrightarrow> (Inl (), st t') \<in> fst (G (st s'))
 2. \<And>s'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s'))\<rbrakk> \<Longrightarrow> \<not> snd (G' s') proof (prove)
goal (2 subgoals):
 1. \<And>s' t' r'. \<lbrakk>\<forall>b. P b \<longrightarrow> (nf \<longrightarrow> \<not> snd (G (st b))) \<longrightarrow> (\<forall>x\<in>fst (G' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (G (st b)). case x of (r, t) \<Rightarrow> t = st t' \<and> (dc \<oplus> dc) r r') \<and> \<not> snd (G' b); P s'; \<not> snd (G (st s')); (Inl r', t') \<in> fst (G' s')\<rbrakk> \<Longrightarrow> (Inl (), st t') \<in> fst (G (st s'))
 2. \<And>s'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s'))\<rbrakk> \<Longrightarrow> \<not> snd (G' s') proof (prove)
goal (2 subgoals):
 1. \<And>s' t' r'. \<lbrakk>P s'; \<not> snd (G (st s')); (Inl r', t') \<in> fst (G' s'); (nf \<longrightarrow> \<not> snd (G (st s'))) \<longrightarrow> (\<forall>x\<in>fst (G' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (G (st s')). case x of (r, t) \<Rightarrow> t = st t' \<and> (dc \<oplus> dc) r r') \<and> \<not> snd (G' s')\<rbrakk> \<Longrightarrow> (Inl (), st t') \<in> fst (G (st s'))
 2. \<And>s'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s'))\<rbrakk> \<Longrightarrow> \<not> snd (G' s') proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G'; P s'; \<not> snd (G (st s'))\<rbrakk> \<Longrightarrow> \<not> snd (G' s') proof (prove)
goal:
No subgoals!