theory AutoCorres_C

lemma L1corres_call_simpl_spec:
  "\<lbrakk> \<forall>s0. Gamma\<turnstile> (Collect (precond s0)) (Call proc) (Collect (postcond s0));
     \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s \<rbrakk> \<Longrightarrow>
   L1corres ct Gamma (L1_call_simpl_spec ct Gamma proc precond postcond) (Call proc)" apply (clarsimp simp: L1corres_def L1_call_simpl_spec_def L1_defs
                        assert_def snd_select snd_liftE snd_spec
                        in_monad' in_spec
                  split: xstate.splits) apply (case_tac t) apply (blast dest: exec_normal[rotated]) apply (blast dest: exec_abrupt[rotated]) apply (blast intro: exec_no_fault[rotated]) apply (blast intro: exec_no_stuck[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s\<rbrakk> \<Longrightarrow> L1corres ct Gamma (L1_call_simpl_spec ct Gamma proc precond postcond) (Call proc) proof (prove)
goal (1 subgoal):
 1. \<And>s t x. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck) proof (prove)
goal (4 subgoals):
 1. \<And>s t x x1. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x; t = Normal x1\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck)
 2. \<And>s t x x2. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x; t = Abrupt x2\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck)
 3. \<And>s t x x3. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x; t = Fault x3\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck)
 4. \<And>s t x. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x; t = Stuck\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck) proof (prove)
goal (3 subgoals):
 1. \<And>s t x x2. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x; t = Abrupt x2\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck)
 2. \<And>s t x x3. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x; t = Fault x3\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck)
 3. \<And>s t x. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x; t = Stuck\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck) proof (prove)
goal (2 subgoals):
 1. \<And>s t x x3. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x; t = Fault x3\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck)
 2. \<And>s t x. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x; t = Stuck\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck) proof (prove)
goal (1 subgoal):
 1. \<And>s t x. \<lbrakk>\<forall>s0. Gamma\<turnstile> (Collect (precond s0)) Call proc (Collect (postcond s0)); \<And>s. ct \<Longrightarrow> Gamma\<turnstile>Call proc \<down> Normal s; precond s s; postcond s x; t = Stuck\<rbrakk> \<Longrightarrow> (\<forall>x1. t = Normal x1 \<longrightarrow> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<longrightarrow> postcond s x1) \<and> (\<forall>x2. t = Abrupt x2 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Abrupt x2) \<and> (\<forall>x3. t = Fault x3 \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Fault x3) \<and> (t = Stuck \<longrightarrow> \<not> Gamma\<turnstile> \<langle>Call proc,Normal s\<rangle> \<Rightarrow> Stuck) proof (prove)
goal:
No subgoals!