theory SIMPL_Lemmas

lemma exec_eq_is_valid_eq0:
  fixes P :: "'a set"
  assumes eq: "\<And>t t'. (\<Gamma> \<turnstile> \<langle>a, Normal t\<rangle> \<Rightarrow> t') = (\<Gamma> \<turnstile> \<langle>a', Normal t\<rangle> \<Rightarrow> t')"
  and     vl: "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a Q,A"
  shows   "\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a' Q,A" using vl apply - apply (drule hoare_sound) apply (rule hoare_complete) apply (simp add: HoarePartialDef.valid_def cvalid_def) apply (intro allI impI) apply clarsimp apply (subst (asm) eq [symmetric]) apply (drule spec, drule spec, drule (1) mp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a' Q,A proof (prove)
using this:
\<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a Q,A

goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a' Q,A proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a Q,A \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a' Q,A proof (prove)
goal (1 subgoal):
 1. \<Gamma>,{}\<Turnstile>\<^bsub>/F\<^esub> P a Q,A \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a' Q,A proof (prove)
goal (1 subgoal):
 1. \<Gamma>,{}\<Turnstile>\<^bsub>/F\<^esub> P a Q,A \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> P a' Q,A proof (prove)
goal (1 subgoal):
 1. \<forall>s t. \<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A \<Longrightarrow> \<forall>s t. \<Gamma>\<turnstile> \<langle>a',s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A; \<Gamma>\<turnstile> \<langle>a',s\<rangle> \<Rightarrow> t; s \<in> Normal ` P; t \<notin> Fault ` F\<rbrakk> \<Longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A; \<Gamma>\<turnstile> \<langle>a',Normal x\<rangle> \<Rightarrow> t; t \<notin> Fault ` F; x \<in> P; t \<notin> Abrupt ` A\<rbrakk> \<Longrightarrow> t \<in> Normal ` Q proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A; \<Gamma>\<turnstile> \<langle>a,Normal x\<rangle> \<Rightarrow> t; t \<notin> Fault ` F; x \<in> P; t \<notin> Abrupt ` A\<rbrakk> \<Longrightarrow> t \<in> Normal ` Q proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,Normal x\<rangle> \<Rightarrow> t; t \<notin> Fault ` F; x \<in> P; t \<notin> Abrupt ` A; Normal x \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A\<rbrakk> \<Longrightarrow> t \<in> Normal ` Q proof (prove)
goal:
No subgoals!