theory Finalise_AI

lemma use_bcorres: "bcorres f g \<Longrightarrow> (\<And>f f'.
        \<lbrace>P o (trans_state f)\<rbrace> g \<lbrace>\<lambda>r s. Q r (trans_state f' s)\<rbrace>)\<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" apply (clarsimp simp add: bcorres_underlying_def s_bcorres_underlying_def valid_def) apply (drule_tac x="\<lambda>_.exst s" in meta_spec) apply (drule_tac x="\<lambda>_.exst b" in meta_spec) apply (drule_tac x="truncate_state s" in spec) apply (simp add: trans_state_update') apply (drule_tac x="(a,truncate_state b)" in bspec) apply force apply (simp add:  trans_state_update') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bcorres f g; \<And>f f'. \<lbrace>P \<circ> trans_state f\<rbrace> g \<lbrace>\<lambda>r s. Q r (trans_state f' s)\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (g (truncate_state s)); \<And>f f'. \<forall>s. P (trans_state f s) \<longrightarrow> (\<forall>x\<in>fst (g s). case x of (r, s') \<Rightarrow> Q r (trans_state f' s')); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (g (truncate_state s)); P s; (a, b) \<in> fst (f s); \<And>f'. \<forall>sa. P (trans_state (\<lambda>_. exst s) sa) \<longrightarrow> (\<forall>x\<in>fst (g sa). case x of (r, s') \<Rightarrow> Q r (trans_state f' s'))\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (g (truncate_state s)); P s; (a, b) \<in> fst (f s); \<forall>sa. P (trans_state (\<lambda>_. exst s) sa) \<longrightarrow> (\<forall>x\<in>fst (g sa). case x of (r, s') \<Rightarrow> Q r (trans_state (\<lambda>_. exst b) s'))\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (g (truncate_state s)); P s; (a, b) \<in> fst (f s); P (trans_state (\<lambda>_. exst s) (truncate_state s)) \<longrightarrow> (\<forall>x\<in>fst (g (truncate_state s)). case x of (r, s') \<Rightarrow> Q r (trans_state (\<lambda>_. exst b) s'))\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (g (truncate_state s)); P s; (a, b) \<in> fst (f s); \<forall>(r, s')\<in>fst (g (truncate_state s)). Q r (trans_state (\<lambda>_. exst b) s')\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (g (truncate_state s)); P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> (a, truncate_state b) \<in> fst (g (truncate_state s))
 2. \<And>s a b. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (g (truncate_state s)); P s; (a, b) \<in> fst (f s); case (a, truncate_state b) of (r, s') \<Rightarrow> Q r (trans_state (\<lambda>_. exst b) s')\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. (\<lambda>x. case x of (x, y) \<Rightarrow> (x, truncate_state y)) ` fst (f s) \<subseteq> fst (g (truncate_state s)); P s; (a, b) \<in> fst (f s); case (a, truncate_state b) of (r, s') \<Rightarrow> Q r (trans_state (\<lambda>_. exst b) s')\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal:
No subgoals!