theory SimplRewrite

lemma spec_simulates_to_exec_simulates:
  "\<lbrakk> G \<turnstile> \<langle>a, xs\<rangle> \<Rightarrow> t; spec_simulates G G' \<rbrakk>
    \<Longrightarrow> G' \<turnstile> \<langle>a, xs\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G' \<turnstile> \<langle>a, xs\<rangle> \<Rightarrow> Fault ft)" proof (induct rule: exec.induct) case (Call p bdy s t) show ?case using Call apply clarsimp apply (frule_tac x=p in spec_simulates_def[THEN iffD1, rule_format]) apply (clarsimp simp: exec_simulates_def) apply (rule exec.Call, simp) apply (blast intro: exec.intros) done next case (CallUndefined p) show ?case using CallUndefined apply clarsimp apply (frule_tac x=p in spec_simulates_def[THEN iffD1, rule_format]) apply (fastforce intro: exec.CallUndefined) done qed (auto intro: exec.intros, (force intro: exec.intros)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G\<turnstile> \<langle>a,xs\<rangle> \<Rightarrow> t; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>a,xs\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>a,xs\<rangle> \<Rightarrow> Fault ft) proof (state)
goal (20 subgoals):
 1. \<And>s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Normal s \<or> (\<exists>ft. G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Fault ft)
 2. \<And>s g c t f. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 3. \<And>s g f c. \<lbrakk>s \<notin> g; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 4. \<And>c f. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault ft)
 5. \<And>f s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Fault ft)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Normal t \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Stuck \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s' \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 9. \<And>s b c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 10. \<And>s b c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
A total of 20 subgoals... proof (state)
this:
G p = Some bdy
G\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t
spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> Fault ft)
spec_simulates G G'

goal (20 subgoals):
 1. \<And>s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Normal s \<or> (\<exists>ft. G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Fault ft)
 2. \<And>s g c t f. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 3. \<And>s g f c. \<lbrakk>s \<notin> g; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 4. \<And>c f. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault ft)
 5. \<And>f s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Fault ft)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Normal t \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Stuck \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s' \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 9. \<And>s b c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 10. \<And>s b c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
A total of 20 subgoals... proof (prove)
goal (1 subgoal):
 1. G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Fault ft) proof (prove)
using this:
G p = Some bdy
G\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t
spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> Fault ft)
spec_simulates G G'

goal (1 subgoal):
 1. G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Fault ft) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G p = Some bdy; G\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'; \<forall>ft. \<not> G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G p = Some bdy; G\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'; \<forall>ft. \<not> G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Fault ft; (G p = None) = (G' p = None) \<and> (\<forall>b b'. G p = Some b \<and> G' p = Some b' \<longrightarrow> exec_simulates UNIV UNIV b b')\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>G p = Some bdy; G\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'; \<forall>ft. \<not> G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>s \<Gamma> t. \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile> \<langle>y,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. \<Gamma>\<turnstile> \<langle>y,Normal s\<rangle> \<Rightarrow> Fault ft); G' p = Some y\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>G p = Some bdy; G\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t; G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'; \<forall>ft. \<not> G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Fault ft; \<forall>s \<Gamma> t. \<Gamma>\<turnstile> \<langle>bdy,Normal s\<rangle> \<Rightarrow> t \<longrightarrow> \<Gamma>\<turnstile> \<langle>y,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. \<Gamma>\<turnstile> \<langle>y,Normal s\<rangle> \<Rightarrow> Fault ft); G' p = Some y\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>y,Normal s\<rangle> \<Rightarrow> t proof (prove)
goal:
No subgoals! proof (state)
this:
G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow> Fault ft)

goal (19 subgoals):
 1. \<And>s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Normal s \<or> (\<exists>ft. G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Fault ft)
 2. \<And>s g c t f. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 3. \<And>s g f c. \<lbrakk>s \<notin> g; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 4. \<And>c f. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault ft)
 5. \<And>f s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Fault ft)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Normal t \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Stuck \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s' \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 9. \<And>s b c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 10. \<And>s b c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
A total of 19 subgoals... proof (state)
goal (19 subgoals):
 1. \<And>s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Normal s \<or> (\<exists>ft. G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Fault ft)
 2. \<And>s g c t f. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 3. \<And>s g f c. \<lbrakk>s \<notin> g; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 4. \<And>c f. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault ft)
 5. \<And>f s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Fault ft)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Normal t \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Stuck \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s' \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 9. \<And>s b c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 10. \<And>s b c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
A total of 19 subgoals... proof (state)
this:
G p = None
spec_simulates G G'

goal (19 subgoals):
 1. \<And>s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Normal s \<or> (\<exists>ft. G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Fault ft)
 2. \<And>s g c t f. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 3. \<And>s g f c. \<lbrakk>s \<notin> g; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 4. \<And>c f. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault ft)
 5. \<And>f s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Fault ft)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Normal t \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Stuck \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s' \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 9. \<And>s b c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 10. \<And>s b c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
A total of 19 subgoals... proof (prove)
goal (1 subgoal):
 1. G'\<turnstile> \<langle>Call p,Normal s_\<rangle> \<Rightarrow> Stuck \<or> (\<exists>ft. G'\<turnstile> \<langle>Call p,Normal s_\<rangle> \<Rightarrow> Fault ft) proof (prove)
using this:
G p = None
spec_simulates G G'

goal (1 subgoal):
 1. G'\<turnstile> \<langle>Call p,Normal s_\<rangle> \<Rightarrow> Stuck \<or> (\<exists>ft. G'\<turnstile> \<langle>Call p,Normal s_\<rangle> \<Rightarrow> Fault ft) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G p = None; spec_simulates G G'; \<forall>ft. \<not> G'\<turnstile> \<langle>Call p,Normal s_\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Call p,Normal s_\<rangle> \<Rightarrow> Stuck proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G p = None; spec_simulates G G'; \<forall>ft. \<not> G'\<turnstile> \<langle>Call p,Normal s_\<rangle> \<Rightarrow> Fault ft; (G p = None) = (G' p = None) \<and> (\<forall>b b'. G p = Some b \<and> G' p = Some b' \<longrightarrow> exec_simulates UNIV UNIV b b')\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Call p,Normal s_\<rangle> \<Rightarrow> Stuck proof (prove)
goal:
No subgoals! proof (state)
this:
G'\<turnstile> \<langle>Call p,Normal s_\<rangle> \<Rightarrow> Stuck \<or> (\<exists>ft. G'\<turnstile> \<langle>Call p,Normal s_\<rangle> \<Rightarrow> Fault ft)

goal (18 subgoals):
 1. \<And>s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Normal s \<or> (\<exists>ft. G'\<turnstile> \<langle>SKIP,Normal s\<rangle> \<Rightarrow> Fault ft)
 2. \<And>s g c t f. \<lbrakk>s \<in> g; G\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 3. \<And>s g f c. \<lbrakk>s \<notin> g; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>Guard f g c,Normal s\<rangle> \<Rightarrow> Fault ft)
 4. \<And>c f. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault f \<or> (\<exists>ft. G'\<turnstile> \<langle>c,Fault f\<rangle> \<Rightarrow> Fault ft)
 5. \<And>f s. spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Normal (f s) \<or> (\<exists>ft. G'\<turnstile> \<langle>Basic f,Normal s\<rangle> \<Rightarrow> Fault ft)
 6. \<And>s t r. \<lbrakk>(s, t) \<in> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Normal t \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 7. \<And>s r. \<lbrakk>\<forall>t. (s, t) \<notin> r; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Stuck \<or> (\<exists>ft. G'\<turnstile> \<langle>Spec r,Normal s\<rangle> \<Rightarrow> Fault ft)
 8. \<And>c\<^sub>1 s s' c\<^sub>2 t. \<lbrakk>G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s'; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> s' \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); G\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,s'\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1;;
c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 9. \<And>s b c\<^sub>1 t c\<^sub>2. \<lbrakk>s \<in> b; G\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>1,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
 10. \<And>s b c\<^sub>2 t c\<^sub>1. \<lbrakk>s \<notin> b; G\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t; spec_simulates G G' \<Longrightarrow> G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft); spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>Cond b c\<^sub>1 c\<^sub>2,Normal s\<rangle> \<Rightarrow> Fault ft)
A total of 18 subgoals...