theory ADT_IF

lemma big_step_adt_refines:
  "\<lbrakk> LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic \<rbrakk>
     \<Longrightarrow> refines (big_step_adt C (internal_R C R) exmap) (big_step_adt A (internal_R A R) exmap)" apply (subst refines_def) apply (clarsimp simp: execution_def steps_eq_Run) apply (clarsimp simp: image_def) apply (subst Bex_def, subst steps_eq_Run) apply (clarsimp simp: big_step_adt_def) apply (subgoal_tac "\<exists>a0'\<in> Init A s. (a0', s0') \<in> S") prefer 2 apply (force simp: LI_def) apply clarsimp apply (frule (4) refines_Run_big_steps) apply (force simp: invariant_holds_def) apply (force simp: invariant_holds_def) apply clarsimp apply (rule_tac x="t'" in exI) apply (clarsimp simp: LI_def) apply (rule conjI) apply blast apply (subgoal_tac "xa \<in> Ic") apply simp apply (rule_tac s="s0'" in inv_holds_Run_big_steps[OF invariant_holds_inv_holds], assumption+) apply (force simp: invariant_holds_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic\<rbrakk> \<Longrightarrow> big_step_adt C (internal_R C R) exmap \<sqsubseteq> big_step_adt A (internal_R A R) exmap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic\<rbrakk> \<Longrightarrow> \<forall>js s. execution (big_step_adt C (internal_R C R) exmap) s js \<subseteq> execution (big_step_adt A (internal_R A R) exmap) s js proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init (big_step_adt C (internal_R C R) exmap) s; (s0', xa) \<in> Run (Step (big_step_adt C (internal_R C R) exmap)) js\<rbrakk> \<Longrightarrow> Fin (big_step_adt C (internal_R C R) exmap) xa \<in> Fin (big_step_adt A (internal_R A R) exmap) ` steps (Step (big_step_adt A (internal_R A R) exmap)) (Init (big_step_adt A (internal_R A R) exmap) s) js proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init (big_step_adt C (internal_R C R) exmap) s; (s0', xa) \<in> Run (Step (big_step_adt C (internal_R C R) exmap)) js\<rbrakk> \<Longrightarrow> \<exists>x\<in>steps (Step (big_step_adt A (internal_R A R) exmap)) (Init (big_step_adt A (internal_R A R) exmap) s) js. Fin (big_step_adt C (internal_R C R) exmap) xa = Fin (big_step_adt A (internal_R A R) exmap) x proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init (big_step_adt C (internal_R C R) exmap) s; (s0', xa) \<in> Run (Step (big_step_adt C (internal_R C R) exmap)) js\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init (big_step_adt A (internal_R A R) exmap) s \<and> (s0', x) \<in> Run (Step (big_step_adt A (internal_R A R) exmap)) js) \<and> Fin (big_step_adt C (internal_R C R) exmap) xa = Fin (big_step_adt A (internal_R A R) exmap) x proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init A s \<and> (s0', x) \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A x proof (prove)
goal (2 subgoals):
 1. \<And>js s xa s0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; \<exists>a0'\<in>Init A s. (a0', s0') \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init A s \<and> (s0', x) \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A x
 2. \<And>js s xa s0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js\<rbrakk> \<Longrightarrow> \<exists>a0'\<in>Init A s. (a0', s0') \<in> S proof (prove)
goal (2 subgoals):
 1. \<And>js s xa s0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js\<rbrakk> \<Longrightarrow> \<exists>a0'\<in>Init A s. (a0', s0') \<in> S
 2. \<And>js s xa s0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; \<exists>a0'\<in>Init A s. (a0', s0') \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init A s \<and> (s0', x) \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A x proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; \<exists>a0'\<in>Init A s. (a0', s0') \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init A s \<and> (s0', x) \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A x proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0' a0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init A s \<and> (s0', x) \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A x proof (prove)
goal (3 subgoals):
 1. \<And>js s xa s0' a0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S\<rbrakk> \<Longrightarrow> s0' \<in> Ic
 2. \<And>js s xa s0' a0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S\<rbrakk> \<Longrightarrow> a0' \<in> Ia
 3. \<And>js s xa s0' a0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; \<exists>t'. (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js \<and> (t', xa) \<in> S \<and> t' \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init A s \<and> (s0', x) \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A x proof (prove)
goal (2 subgoals):
 1. \<And>js s xa s0' a0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S\<rbrakk> \<Longrightarrow> a0' \<in> Ia
 2. \<And>js s xa s0' a0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; \<exists>t'. (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js \<and> (t', xa) \<in> S \<and> t' \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init A s \<and> (s0', x) \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A x proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0' a0'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; \<exists>t'. (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js \<and> (t', xa) \<in> S \<and> t' \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init A s \<and> (s0', x) \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A x proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0' a0' t'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> \<exists>x. (\<exists>s0'. s0' \<in> Init A s \<and> (s0', x) \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A x proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0' a0' t'. \<lbrakk>LI A C S (Ia \<times> Ic); A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia\<rbrakk> \<Longrightarrow> (\<exists>s0'. s0' \<in> Init A s \<and> (s0', t') \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A t' proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0' a0' t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> (\<exists>s0'. s0' \<in> Init A s \<and> (s0', t') \<in> Run (big_steps A (internal_R A R) exmap) js) \<and> Fin C xa = Fin A t' proof (prove)
goal (2 subgoals):
 1. \<And>js s xa s0' a0' t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> \<exists>s0'. s0' \<in> Init A s \<and> (s0', t') \<in> Run (big_steps A (internal_R A R) exmap) js
 2. \<And>js s xa s0' a0' t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> Fin C xa = Fin A t' proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0' a0' t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> Fin C xa = Fin A t' proof (prove)
goal (2 subgoals):
 1. \<And>js s xa s0' a0' t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; xa \<in> Ic\<rbrakk> \<Longrightarrow> Fin C xa = Fin A t'
 2. \<And>js s xa s0' a0' t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> xa \<in> Ic proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0' a0' t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> xa \<in> Ic proof (prove)
goal (2 subgoals):
 1. \<And>js s xa s0' a0' t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> s0' \<in> Ic
 2. \<And>js s xa s0' a0' t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> (s0', xa) \<in> Run (big_steps C (?R63 js s xa s0' a0' t') (?exmap63 js s xa s0' a0' t')) (?js63 js s xa s0' a0' t') proof (prove)
goal (1 subgoal):
 1. \<And>js s xa s0' a0' t'. \<lbrakk>A \<Turnstile> Ia; C \<Turnstile> Ic; s0' \<in> Init C s; (s0', xa) \<in> Run (big_steps C (internal_R C R) exmap) js; a0' \<in> Init A s; (a0', s0') \<in> S; (a0', t') \<in> Run (big_steps A (internal_R A R) exmap) js; (t', xa) \<in> S; t' \<in> Ia; \<forall>s. Init C s \<subseteq> S `` Init A s; \<forall>j. S \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; S; \<forall>s s'. (s, s') \<in> S \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s\<rbrakk> \<Longrightarrow> (s0', xa) \<in> Run (big_steps C (?R63 js s xa s0' a0' t') (?exmap63 js s xa s0' a0' t')) (?js63 js s xa s0' a0' t') proof (prove)
goal:
No subgoals!