theory Invoke_C

lemma ccorres_throwError_inl_rrel:
  "ccorres_underlying sr Gamm (inl_rrel r) xf arrel axf hs P P'
            (throwError v) c
   \<Longrightarrow> ccorres_underlying sr Gamm r xf (inl_rrel arrel) axf hs P P'
            (throwError v) c" apply (rule ccorresI') apply (erule(3) ccorresE) apply (simp add: throwError_def return_def) apply assumption apply (simp add: throwError_def return_def
                   unif_rrel_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamm (inl_rrel r) xf arrel axf hs P P' (throwError v) c \<Longrightarrow> ccorres_underlying sr Gamm r xf (inl_rrel arrel) axf hs P P' (throwError v) c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr Gamm (inl_rrel r) xf arrel axf hs P P' (throwError v) c; (s, s') \<in> sr; hs s; s' \<in> P; Gamm\<turnstile>\<^sub>h \<langle>c # P',s'\<rangle> \<Rightarrow> (n, z); \<not> snd (throwError v s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError v s). (t, t') \<in> sr \<and> unif_rrel (n = length P') r xf (inl_rrel arrel) axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; hs s; s' \<in> P; Gamm\<turnstile>\<^sub>h \<langle>c # P',s'\<rangle> \<Rightarrow> (n, z); \<not> snd (throwError v s)\<rbrakk> \<Longrightarrow> \<not> snd (throwError v s)
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; hs s; s' \<in> P; Gamm\<turnstile>\<^sub>h \<langle>c # P',s'\<rangle> \<Rightarrow> (n, z); \<not> snd (throwError v s)\<rbrakk> \<Longrightarrow> Gamm\<turnstile>\<^sub>h \<langle>c # P',s'\<rangle> \<Rightarrow> (?n2 s s' n z, ?x2 s s' n z)
 3. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; hs s; s' \<in> P; Gamm\<turnstile>\<^sub>h \<langle>c # P',s'\<rangle> \<Rightarrow> (n, z); \<not> snd (throwError v s); ?x2 s s' n z = Normal t'; (ra, t) \<in> fst (throwError v s); (t, t') \<in> sr; unif_rrel (?n2 s s' n z = length P') (inl_rrel r) xf arrel axf ra t'; ?n2 s s' n z \<le> length P'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError v s). (t, t') \<in> sr \<and> unif_rrel (n = length P') r xf (inl_rrel arrel) axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; hs s; s' \<in> P; Gamm\<turnstile>\<^sub>h \<langle>c # P',s'\<rangle> \<Rightarrow> (n, z); \<not> snd (throwError v s)\<rbrakk> \<Longrightarrow> Gamm\<turnstile>\<^sub>h \<langle>c # P',s'\<rangle> \<Rightarrow> (?n2 s s' n z, ?x2 s s' n z)
 2. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; hs s; s' \<in> P; Gamm\<turnstile>\<^sub>h \<langle>c # P',s'\<rangle> \<Rightarrow> (n, z); \<not> snd (throwError v s); ?x2 s s' n z = Normal t'; (ra, t) \<in> fst (throwError v s); (t, t') \<in> sr; unif_rrel (?n2 s s' n z = length P') (inl_rrel r) xf arrel axf ra t'; ?n2 s s' n z \<le> length P'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError v s). (t, t') \<in> sr \<and> unif_rrel (n = length P') r xf (inl_rrel arrel) axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; hs s; s' \<in> P; Gamm\<turnstile>\<^sub>h \<langle>c # P',s'\<rangle> \<Rightarrow> (n, z); \<not> snd (throwError v s); z = Normal t'; (ra, t) \<in> fst (throwError v s); (t, t') \<in> sr; unif_rrel (n = length P') (inl_rrel r) xf arrel axf ra t'; n \<le> length P'\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError v s). (t, t') \<in> sr \<and> unif_rrel (n = length P') r xf (inl_rrel arrel) axf ra t') proof (prove)
goal:
No subgoals!