theory CCorresLemmas

lemma ccorres_Call_call_for_vcg:
  "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (call id f (\<lambda>s t. t) (\<lambda>s t. Basic id)) \<Longrightarrow>
  ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (Call f)" apply (erule iffD1 [OF ccorres_semantic_equiv, rotated -1]) apply (rule semantic_equivI) apply (rule iffI) apply (erule exec_call_Normal_elim) apply (erule exec_Normal_elim_cases)+ apply (simp, erule (1) exec.Call)+ apply simp apply (erule exec.intros) apply (erule exec_Normal_elim_cases) apply (case_tac s') apply simp apply (erule exec_call) apply simp apply (rule exec.Basic [where f = id, simplified]) apply (clarsimp elim!: exec_callAbrupt) apply (clarsimp elim!: exec_callFault) apply (clarsimp elim!: exec_callStuck) apply (clarsimp elim!: exec_callUndefined) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (call id f (\<lambda>s t. t) (\<lambda>s t. Basic id)) \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (Call f) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' (call id f (\<lambda>s t. t) (\<lambda>s t. Basic id)) (Call f) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (6 subgoals):
 1. \<And>s s' bdy t'. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (id s)\<rangle> \<Rightarrow> Normal t'; \<Gamma>\<turnstile> \<langle>Basic id,Normal t'\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s' bdy t'. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (id s)\<rangle> \<Rightarrow> Abrupt t'; s' = Abrupt t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 3. \<And>s s' bdy fa. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (id s)\<rangle> \<Rightarrow> Fault fa; s' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 4. \<And>s s' bdy. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (id s)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 5. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma> f = None; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 6. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (6 subgoals):
 1. \<And>s s' bdy t'. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (id s)\<rangle> \<Rightarrow> Normal t'; s' = Normal (id t')\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s' bdy t'. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (id s)\<rangle> \<Rightarrow> Abrupt t'; s' = Abrupt t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 3. \<And>s s' bdy fa. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (id s)\<rangle> \<Rightarrow> Fault fa; s' = Fault fa\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 4. \<And>s s' bdy. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal (id s)\<rangle> \<Rightarrow> Stuck; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 5. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma> f = None; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 6. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma> f = None; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma> f = None; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> Stuck
 2. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s \<in> G'; \<Gamma>\<turnstile> \<langle>Call f,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' bdy. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s'. \<lbrakk>s \<in> G'; s' = Stuck; \<Gamma> f = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (5 subgoals):
 1. \<And>s s' bdy x1. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s' bdy x2. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 3. \<And>s s' bdy x3. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 4. \<And>s s' bdy. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 5. \<And>s s'. \<lbrakk>s \<in> G'; s' = Stuck; \<Gamma> f = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (5 subgoals):
 1. \<And>s s' bdy x1. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> Normal x1
 2. \<And>s s' bdy x2. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 3. \<And>s s' bdy x3. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 4. \<And>s s' bdy. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 5. \<And>s s'. \<lbrakk>s \<in> G'; s' = Stuck; \<Gamma> f = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (6 subgoals):
 1. \<And>s s' bdy x1. \<lbrakk>s \<in> G'; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>bdy,Normal (id s)\<rangle> \<Rightarrow> Normal (?t29 s s' bdy x1)
 2. \<And>s s' bdy x1. \<lbrakk>s \<in> G'; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic id,Normal (?t29 s s' bdy x1)\<rangle> \<Rightarrow> Normal x1
 3. \<And>s s' bdy x2. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 4. \<And>s s' bdy x3. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 5. \<And>s s' bdy. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 6. \<And>s s'. \<lbrakk>s \<in> G'; s' = Stuck; \<Gamma> f = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (5 subgoals):
 1. \<And>s s' bdy x1. \<lbrakk>s \<in> G'; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> Normal x1; s' = Normal x1\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic id,Normal x1\<rangle> \<Rightarrow> Normal x1
 2. \<And>s s' bdy x2. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 3. \<And>s s' bdy x3. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 4. \<And>s s' bdy. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 5. \<And>s s'. \<lbrakk>s \<in> G'; s' = Stuck; \<Gamma> f = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (4 subgoals):
 1. \<And>s s' bdy x2. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Abrupt x2\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s' bdy x3. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 3. \<And>s s' bdy. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 4. \<And>s s'. \<lbrakk>s \<in> G'; s' = Stuck; \<Gamma> f = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (3 subgoals):
 1. \<And>s s' bdy x3. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Fault x3\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s' bdy. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 3. \<And>s s'. \<lbrakk>s \<in> G'; s' = Stuck; \<Gamma> f = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' bdy. \<lbrakk>s \<in> G'; \<Gamma> f = Some bdy; \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> s'; s' = Stuck\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s'
 2. \<And>s s'. \<lbrakk>s \<in> G'; s' = Stuck; \<Gamma> f = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s \<in> G'; s' = Stuck; \<Gamma> f = None\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>call id f (\<lambda>s t. t) (\<lambda>s t. Basic id),Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!