theory AutoCorres_C

lemma terminates_spec_no_fail:
  fixes \<Gamma>
  assumes ac: "ac \<equiv> AC_call_L1 arg_rel globals ret_xf (L1_call_simpl check_termination \<Gamma> f_'proc)"
  assumes p_spec: "\<forall>s. \<Gamma>,{} \<turnstile> {s'. s = s' \<and> P s s'} (Call f_'proc) (Q s)"
  assumes terminates: "\<forall>s. P s s \<longrightarrow> \<Gamma> \<turnstile> Call f_'proc \<down> Normal s"
  assumes nf_pre: "\<And>s. N (globals s) \<Longrightarrow> arg_rel s \<Longrightarrow> P s s"
  shows "no_fail N ac" proof - have normal: "\<forall>s t. P s s \<longrightarrow> \<Gamma> \<turnstile> \<langle>Call f_'proc, Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal" using spec_result_Normal p_spec by simp have L1_call_simpl_no_fail:
      "no_fail (\<lambda>s. P s s) (L1_call_simpl check_termination \<Gamma> f_'proc)" apply (wpsimp simp: L1_call_simpl_def) using terminates normal by auto have select_f_L1_call_simpl_no_fail:
      "\<And>s. no_fail (\<lambda>_. P s s) (select_f (L1_call_simpl check_termination \<Gamma> f_'proc s))" using L1_call_simpl_no_fail[unfolded no_fail_def] by wpsimp have select_f_L1_call_simpl_rv:
      "\<And>s. \<lbrace>\<lambda>_. P s s\<rbrace> select_f (L1_call_simpl check_termination \<Gamma> f_'proc s) \<lbrace>\<lambda>r s. fst r = Inr ()\<rbrace>" apply (wp, clarsimp simp: L1_call_simpl_def in_monad in_select split: xstate.splits) apply (match premises in "s \<noteq> Stuck" for s \<Rightarrow> \<open>cases s\<close>) using normal by auto show ?thesis apply (clarsimp simp: ac AC_call_L1_def L2_call_L1_def) apply (wpsimp wp_del: select_f_wp) apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce) apply (wpsimp wp: select_f_L1_call_simpl_no_fail)+ apply (fastforce simp: nf_pre) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail N ac proof (state)
goal (1 subgoal):
 1. no_fail N ac proof (prove)
goal (1 subgoal):
 1. \<forall>s t. P s s \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal proof (prove)
using this:
\<forall>s. ?\<Gamma>\<turnstile> {s'. s = s' \<and> ?P s s'} ?p (?Q s) \<Longrightarrow> \<forall>s t. ?P s s \<longrightarrow> ?\<Gamma>\<turnstile> \<langle>?p,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal
\<forall>s. \<Gamma>\<turnstile> {s'. s = s' \<and> P s s'} Call f_'proc (Q s)

goal (1 subgoal):
 1. \<forall>s t. P s s \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal proof (state)
this:
\<forall>s t. P s s \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal

goal (1 subgoal):
 1. no_fail N ac proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. P s s) (L1_call_simpl check_termination \<Gamma> f_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s s \<Longrightarrow> (check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s) \<and> ((check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s) \<longrightarrow> (\<forall>x. \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> x \<longrightarrow> (\<forall>xa. x \<noteq> Fault xa) \<and> x \<noteq> Stuck)) proof (prove)
using this:
\<forall>s. P s s \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s
\<forall>s t. P s s \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal

goal (1 subgoal):
 1. \<And>s. P s s \<Longrightarrow> (check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s) \<and> ((check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s) \<longrightarrow> (\<forall>x. \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> x \<longrightarrow> (\<forall>xa. x \<noteq> Fault xa) \<and> x \<noteq> Stuck)) proof (state)
this:
no_fail (\<lambda>s. P s s) (L1_call_simpl check_termination \<Gamma> f_'proc)

goal (1 subgoal):
 1. no_fail N ac proof (prove)
goal (1 subgoal):
 1. \<And>s. no_fail (\<lambda>_. P s s) (select_f (L1_call_simpl check_termination \<Gamma> f_'proc s)) proof (prove)
using this:
\<forall>s. P s s \<longrightarrow> \<not> snd (L1_call_simpl check_termination \<Gamma> f_'proc s)

goal (1 subgoal):
 1. \<And>s. no_fail (\<lambda>_. P s s) (select_f (L1_call_simpl check_termination \<Gamma> f_'proc s)) proof (state)
this:
no_fail (\<lambda>_. P ?s1 ?s1) (select_f (L1_call_simpl check_termination \<Gamma> f_'proc ?s1))

goal (1 subgoal):
 1. no_fail N ac proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>\<lambda>_. P s s\<rbrace> select_f (L1_call_simpl check_termination \<Gamma> f_'proc s) \<lbrace>\<lambda>r s. fst r = Inr ()\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>P s s; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> a = Inr () \<and> b = x1; \<forall>x2. x = Abrupt x2 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Abrupt x2 \<and> a = Inl () \<and> b = x2; \<forall>x3. x \<noteq> Fault x3; x \<noteq> Stuck\<rbrakk> \<Longrightarrow> a = Inr () proof (prove)
goal (4 subgoals):
 1. \<And>s a b x x1. \<lbrakk>P s s; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> a = Inr () \<and> b = x1; \<forall>x2. x = Abrupt x2 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Abrupt x2 \<and> a = Inl () \<and> b = x2; \<forall>x3. x \<noteq> Fault x3; x \<noteq> Stuck; x = Normal x1\<rbrakk> \<Longrightarrow> a = Inr ()
 2. \<And>s a b x x2. \<lbrakk>P s s; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> a = Inr () \<and> b = x1; \<forall>x2. x = Abrupt x2 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Abrupt x2 \<and> a = Inl () \<and> b = x2; \<forall>x3. x \<noteq> Fault x3; x \<noteq> Stuck; x = Abrupt x2\<rbrakk> \<Longrightarrow> a = Inr ()
 3. \<And>s a b x x3. \<lbrakk>P s s; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> a = Inr () \<and> b = x1; \<forall>x2. x = Abrupt x2 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Abrupt x2 \<and> a = Inl () \<and> b = x2; \<forall>x3. x \<noteq> Fault x3; x \<noteq> Stuck; x = Fault x3\<rbrakk> \<Longrightarrow> a = Inr ()
 4. \<And>s a b x. \<lbrakk>P s s; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> a = Inr () \<and> b = x1; \<forall>x2. x = Abrupt x2 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Abrupt x2 \<and> a = Inl () \<and> b = x2; \<forall>x3. x \<noteq> Fault x3; x \<noteq> Stuck; x = Stuck\<rbrakk> \<Longrightarrow> a = Inr () proof (prove)
using this:
\<forall>s t. P s s \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> range Normal

goal (4 subgoals):
 1. \<And>s a b x x1. \<lbrakk>P s s; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> a = Inr () \<and> b = x1; \<forall>x2. x = Abrupt x2 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Abrupt x2 \<and> a = Inl () \<and> b = x2; \<forall>x3. x \<noteq> Fault x3; x \<noteq> Stuck; x = Normal x1\<rbrakk> \<Longrightarrow> a = Inr ()
 2. \<And>s a b x x2. \<lbrakk>P s s; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> a = Inr () \<and> b = x1; \<forall>x2. x = Abrupt x2 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Abrupt x2 \<and> a = Inl () \<and> b = x2; \<forall>x3. x \<noteq> Fault x3; x \<noteq> Stuck; x = Abrupt x2\<rbrakk> \<Longrightarrow> a = Inr ()
 3. \<And>s a b x x3. \<lbrakk>P s s; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> a = Inr () \<and> b = x1; \<forall>x2. x = Abrupt x2 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Abrupt x2 \<and> a = Inl () \<and> b = x2; \<forall>x3. x \<noteq> Fault x3; x \<noteq> Stuck; x = Fault x3\<rbrakk> \<Longrightarrow> a = Inr ()
 4. \<And>s a b x. \<lbrakk>P s s; check_termination \<longrightarrow> \<Gamma>\<turnstile>Call f_'proc \<down> Normal s; \<forall>x1. x = Normal x1 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Normal x1 \<and> a = Inr () \<and> b = x1; \<forall>x2. x = Abrupt x2 \<longrightarrow> \<Gamma>\<turnstile> \<langle>Call f_'proc,Normal s\<rangle> \<Rightarrow> Abrupt x2 \<and> a = Inl () \<and> b = x2; \<forall>x3. x \<noteq> Fault x3; x \<noteq> Stuck; x = Stuck\<rbrakk> \<Longrightarrow> a = Inr () proof (state)
this:
\<lbrace>\<lambda>_. P ?s2 ?s2\<rbrace> select_f (L1_call_simpl check_termination \<Gamma> f_'proc ?s2) \<lbrace>\<lambda>r s. fst r = Inr ()\<rbrace>

goal (1 subgoal):
 1. no_fail N ac proof (prove)
goal (1 subgoal):
 1. no_fail N ac proof (prove)
goal (1 subgoal):
 1. no_fail N (do cur_gs <- get;
s <- select {s. globals s = cur_gs \<and> arg_rel s};
(rv, s') <- select_f (L1_call_simpl check_termination \<Gamma> f_'proc s);
y <- put (globals s');
case rv of Inl x \<Rightarrow> fail | Inr x \<Rightarrow> return (Inr (ret_xf s'))
od) proof (prove)
goal (7 subgoals):
 1. \<And>cur_gs s. \<lbrace>?Q4 cur_gs s\<rbrace> select_f (L1_call_simpl check_termination \<Gamma> f_'proc s) \<lbrace>\<lambda>rv s. \<forall>x. (\<exists>xa. rv = (x, xa)) \<longrightarrow> x = Inr ()\<rbrace>
 2. \<And>cur_gs s. no_fail (?P4 cur_gs s) (select_f (L1_call_simpl check_termination \<Gamma> f_'proc s))
 3. \<And>cur_gs. \<lbrace>?Q3 cur_gs\<rbrace> select {s. globals s = cur_gs \<and> arg_rel s} \<lbrace>\<lambda>s. ?P4 cur_gs s and ?Q4 cur_gs s\<rbrace>
 4. \<And>cur_gs. no_fail (?P3 cur_gs) (select {s. globals s = cur_gs \<and> arg_rel s})
 5. \<lbrace>?Q2\<rbrace> get \<lbrace>\<lambda>cur_gs. ?P3 cur_gs and ?Q3 cur_gs\<rbrace>
 6. no_fail ?P2 get
 7. \<And>s. N s \<Longrightarrow> (?P2 and ?Q2) s proof (prove)
goal (6 subgoals):
 1. \<And>cur_gs s. no_fail (?P4 cur_gs s) (select_f (L1_call_simpl check_termination \<Gamma> f_'proc s))
 2. \<And>cur_gs. \<lbrace>?Q3 cur_gs\<rbrace> select {s. globals s = cur_gs \<and> arg_rel s} \<lbrace>\<lambda>s. ?P4 cur_gs s and (\<lambda>_. P s s)\<rbrace>
 3. \<And>cur_gs. no_fail (?P3 cur_gs) (select {s. globals s = cur_gs \<and> arg_rel s})
 4. \<lbrace>?Q2\<rbrace> get \<lbrace>\<lambda>cur_gs. ?P3 cur_gs and ?Q3 cur_gs\<rbrace>
 5. no_fail ?P2 get
 6. \<And>s. N s \<Longrightarrow> (?P2 and ?Q2) s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>N (globals x); arg_rel x\<rbrakk> \<Longrightarrow> P x x proof (prove)
goal:
No subgoals! proof (state)
this:
no_fail N ac

goal:
No subgoals!