theory ExtraSpecs

lemma simple_simpl_refines_guarded_Basic_guarded_spec_body:
  "(\<forall>s s'. (s, s') \<in> R \<longrightarrow> (s \<in> G \<and> (s, f s) \<in> R))
    \<Longrightarrow> simple_simpl_refines \<Gamma> (Guard F' G (Basic f)) (guarded_spec_body F R)" apply (simp add: guarded_spec_body_def simple_simpl_refines_def) apply (intro allI, drule_tac x=s in spec) apply (erule impCE) apply (rule disjI1) apply (fastforce intro: exec.GuardFault) apply (rule disjI2) apply (auto intro!: exec.Guard terminates.Guard
               intro: exec.GuardFault exec.Spec terminates.Basic image_eqI[rotated]
              elim!: exec_Normal_elim_cases terminates_Normal_elim_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> R \<longrightarrow> s \<in> G \<and> (s, f s) \<in> R \<Longrightarrow> simple_simpl_refines \<Gamma> (Guard F' G (Basic f)) (guarded_spec_body F R) proof (prove)
goal (1 subgoal):
 1. \<forall>s. (\<exists>s'. (s, s') \<in> R) \<longrightarrow> s \<in> G \<and> (s, f s) \<in> R \<Longrightarrow> \<forall>s. (\<exists>ft. \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> Fault ft) \<or> (\<forall>xs. \<Gamma>\<turnstile> \<langle>Guard F' G (Basic f),Normal s\<rangle> \<Rightarrow> xs \<longrightarrow> \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> xs) \<and> (\<not> \<Gamma>\<turnstile>Guard F' G (Basic f) \<down> Normal s \<longrightarrow> \<not> \<Gamma>\<turnstile>Guard F (fst ` R) (Spec R) \<down> Normal s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>s'. (s, s') \<in> R) \<longrightarrow> s \<in> G \<and> (s, f s) \<in> R \<Longrightarrow> (\<exists>ft. \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> Fault ft) \<or> (\<forall>xs. \<Gamma>\<turnstile> \<langle>Guard F' G (Basic f),Normal s\<rangle> \<Rightarrow> xs \<longrightarrow> \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> xs) \<and> (\<not> \<Gamma>\<turnstile>Guard F' G (Basic f) \<down> Normal s \<longrightarrow> \<not> \<Gamma>\<turnstile>Guard F (fst ` R) (Spec R) \<down> Normal s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<nexists>s'. (s, s') \<in> R \<Longrightarrow> (\<exists>ft. \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> Fault ft) \<or> (\<forall>xs. \<Gamma>\<turnstile> \<langle>Guard F' G (Basic f),Normal s\<rangle> \<Rightarrow> xs \<longrightarrow> \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> xs) \<and> (\<not> \<Gamma>\<turnstile>Guard F' G (Basic f) \<down> Normal s \<longrightarrow> \<not> \<Gamma>\<turnstile>Guard F (fst ` R) (Spec R) \<down> Normal s)
 2. \<And>s. s \<in> G \<and> (s, f s) \<in> R \<Longrightarrow> (\<exists>ft. \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> Fault ft) \<or> (\<forall>xs. \<Gamma>\<turnstile> \<langle>Guard F' G (Basic f),Normal s\<rangle> \<Rightarrow> xs \<longrightarrow> \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> xs) \<and> (\<not> \<Gamma>\<turnstile>Guard F' G (Basic f) \<down> Normal s \<longrightarrow> \<not> \<Gamma>\<turnstile>Guard F (fst ` R) (Spec R) \<down> Normal s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<nexists>s'. (s, s') \<in> R \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> Fault ft
 2. \<And>s. s \<in> G \<and> (s, f s) \<in> R \<Longrightarrow> (\<exists>ft. \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> Fault ft) \<or> (\<forall>xs. \<Gamma>\<turnstile> \<langle>Guard F' G (Basic f),Normal s\<rangle> \<Rightarrow> xs \<longrightarrow> \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> xs) \<and> (\<not> \<Gamma>\<turnstile>Guard F' G (Basic f) \<down> Normal s \<longrightarrow> \<not> \<Gamma>\<turnstile>Guard F (fst ` R) (Spec R) \<down> Normal s) proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> G \<and> (s, f s) \<in> R \<Longrightarrow> (\<exists>ft. \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> Fault ft) \<or> (\<forall>xs. \<Gamma>\<turnstile> \<langle>Guard F' G (Basic f),Normal s\<rangle> \<Rightarrow> xs \<longrightarrow> \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> xs) \<and> (\<not> \<Gamma>\<turnstile>Guard F' G (Basic f) \<down> Normal s \<longrightarrow> \<not> \<Gamma>\<turnstile>Guard F (fst ` R) (Spec R) \<down> Normal s) proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> G \<and> (s, f s) \<in> R \<Longrightarrow> (\<forall>xs. \<Gamma>\<turnstile> \<langle>Guard F' G (Basic f),Normal s\<rangle> \<Rightarrow> xs \<longrightarrow> \<Gamma>\<turnstile> \<langle>Guard F (fst ` R) (Spec R),Normal s\<rangle> \<Rightarrow> xs) \<and> (\<not> \<Gamma>\<turnstile>Guard F' G (Basic f) \<down> Normal s \<longrightarrow> \<not> \<Gamma>\<turnstile>Guard F (fst ` R) (Spec R) \<down> Normal s) proof (prove)
goal:
No subgoals!