theory Syscall_IF

lemma dmo_ev:
  "(\<And>s s'. equiv_valid (\<lambda>ms ms'. I (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>))
                        (\<lambda>ms ms'. A (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>))
                        (\<lambda>ms ms'. B (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>))
                        (K (P s \<and> P s')) f)
   \<Longrightarrow> equiv_valid I A B P (do_machine_op f)" apply (clarsimp simp: do_machine_op_def bind_def equiv_valid_def2 equiv_valid_2_def
                        gets_def get_def select_f_def modify_def put_def return_def split_def) apply atomize apply (erule_tac x=s in allE) apply (erule_tac x=t in allE) apply simp apply (erule_tac x="machine_state s" in allE) apply (erule_tac x="machine_state t" in allE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. equiv_valid (\<lambda>ms ms'. I (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>)) (\<lambda>ms ms'. A (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>)) (\<lambda>ms ms'. B (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>)) (K (P s \<and> P s')) f) \<Longrightarrow> equiv_valid I A B P (do_machine_op f) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<And>s s'. \<forall>sa t. P s \<and> P s' \<and> P s \<and> P s' \<and> I (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>) \<and> A (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>) \<longrightarrow> (\<forall>x\<in>fst (f sa). \<forall>xa\<in>fst (f t). fst x = fst xa \<and> I (s\<lparr>machine_state := snd x\<rparr>) (s'\<lparr>machine_state := snd xa\<rparr>) \<and> B (s\<lparr>machine_state := snd x\<rparr>) (s'\<lparr>machine_state := snd xa\<rparr>)); (a, b) \<in> fst (f (machine_state s)); (aa, ba) \<in> fst (f (machine_state t)); P s; P t; I s t; A s t\<rbrakk> \<Longrightarrow> a = aa \<and> I (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) \<and> B (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>\<forall>s s' sa t. P s \<and> P s' \<and> P s \<and> P s' \<and> I (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>) \<and> A (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>) \<longrightarrow> (\<forall>x\<in>fst (f sa). \<forall>xa\<in>fst (f t). fst x = fst xa \<and> I (s\<lparr>machine_state := snd x\<rparr>) (s'\<lparr>machine_state := snd xa\<rparr>) \<and> B (s\<lparr>machine_state := snd x\<rparr>) (s'\<lparr>machine_state := snd xa\<rparr>)); (a, b) \<in> fst (f (machine_state s)); (aa, ba) \<in> fst (f (machine_state t)); P s; P t; I s t; A s t\<rbrakk> \<Longrightarrow> a = aa \<and> I (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) \<and> B (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f (machine_state s)); (aa, ba) \<in> fst (f (machine_state t)); P s; P t; I s t; A s t; \<forall>s' sa t. P s \<and> P s' \<and> P s \<and> P s' \<and> I (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>) \<and> A (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>) \<longrightarrow> (\<forall>x\<in>fst (f sa). \<forall>xa\<in>fst (f t). fst x = fst xa \<and> I (s\<lparr>machine_state := snd x\<rparr>) (s'\<lparr>machine_state := snd xa\<rparr>) \<and> B (s\<lparr>machine_state := snd x\<rparr>) (s'\<lparr>machine_state := snd xa\<rparr>))\<rbrakk> \<Longrightarrow> a = aa \<and> I (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) \<and> B (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f (machine_state s)); (aa, ba) \<in> fst (f (machine_state t)); P s; P t; I s t; A s t; \<forall>sa ta. P s \<and> P t \<and> P s \<and> P t \<and> I (s\<lparr>machine_state := sa\<rparr>) (t\<lparr>machine_state := ta\<rparr>) \<and> A (s\<lparr>machine_state := sa\<rparr>) (t\<lparr>machine_state := ta\<rparr>) \<longrightarrow> (\<forall>x\<in>fst (f sa). \<forall>xa\<in>fst (f ta). fst x = fst xa \<and> I (s\<lparr>machine_state := snd x\<rparr>) (t\<lparr>machine_state := snd xa\<rparr>) \<and> B (s\<lparr>machine_state := snd x\<rparr>) (t\<lparr>machine_state := snd xa\<rparr>))\<rbrakk> \<Longrightarrow> a = aa \<and> I (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) \<and> B (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f (machine_state s)); (aa, ba) \<in> fst (f (machine_state t)); P s; P t; I s t; A s t; \<forall>sa ta. I (s\<lparr>machine_state := sa\<rparr>) (t\<lparr>machine_state := ta\<rparr>) \<and> A (s\<lparr>machine_state := sa\<rparr>) (t\<lparr>machine_state := ta\<rparr>) \<longrightarrow> (\<forall>x\<in>fst (f sa). \<forall>xa\<in>fst (f ta). fst x = fst xa \<and> I (s\<lparr>machine_state := snd x\<rparr>) (t\<lparr>machine_state := snd xa\<rparr>) \<and> B (s\<lparr>machine_state := snd x\<rparr>) (t\<lparr>machine_state := snd xa\<rparr>))\<rbrakk> \<Longrightarrow> a = aa \<and> I (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) \<and> B (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f (machine_state s)); (aa, ba) \<in> fst (f (machine_state t)); P s; P t; I s t; A s t; \<forall>ta. I (s\<lparr>machine_state := machine_state s\<rparr>) (t\<lparr>machine_state := ta\<rparr>) \<and> A (s\<lparr>machine_state := machine_state s\<rparr>) (t\<lparr>machine_state := ta\<rparr>) \<longrightarrow> (\<forall>x\<in>fst (f (machine_state s)). \<forall>xa\<in>fst (f ta). fst x = fst xa \<and> I (s\<lparr>machine_state := snd x\<rparr>) (t\<lparr>machine_state := snd xa\<rparr>) \<and> B (s\<lparr>machine_state := snd x\<rparr>) (t\<lparr>machine_state := snd xa\<rparr>))\<rbrakk> \<Longrightarrow> a = aa \<and> I (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) \<and> B (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba. \<lbrakk>(a, b) \<in> fst (f (machine_state s)); (aa, ba) \<in> fst (f (machine_state t)); P s; P t; I s t; A s t; I (s\<lparr>machine_state := machine_state s\<rparr>) (t\<lparr>machine_state := machine_state t\<rparr>) \<and> A (s\<lparr>machine_state := machine_state s\<rparr>) (t\<lparr>machine_state := machine_state t\<rparr>) \<longrightarrow> (\<forall>x\<in>fst (f (machine_state s)). \<forall>xa\<in>fst (f (machine_state t)). fst x = fst xa \<and> I (s\<lparr>machine_state := snd x\<rparr>) (t\<lparr>machine_state := snd xa\<rparr>) \<and> B (s\<lparr>machine_state := snd x\<rparr>) (t\<lparr>machine_state := snd xa\<rparr>))\<rbrakk> \<Longrightarrow> a = aa \<and> I (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) \<and> B (s\<lparr>machine_state := b\<rparr>) (t\<lparr>machine_state := ba\<rparr>) proof (prove)
goal:
No subgoals!