theory Simulation

lemma fw_sim_steps:
  assumes steps: "t' \<in> steps (Step C) S' js" "S' \<subseteq> R `` S"
  assumes sim: "fw_sim R C A"
  shows "\<exists>t \<in> steps (Step A) S js. (t,t') \<in> R" using steps proof (induct js arbitrary: S' S) case Nil thus ?case by (simp add: steps_def) blast next case (Cons j js) hence "t' \<in> steps (Step C) (Step C j `` S') js" by (clarsimp simp: steps_def) moreover { from Cons.prems have "S' \<subseteq> R `` S" by simp moreover from sim have "R ;;; Step C j \<subseteq> Step A j ;;; R" by (simp add: fw_sim_def) ultimately have "Step C j `` S' \<subseteq> R `` (Step A j `` S)" by (simp add: rel_semi_def) blast } ultimately show ?case using Cons.hyps by (auto simp: steps_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R proof (prove)
using this:
t' \<in> steps (Step C) S' js
S' \<subseteq> R `` S

goal (1 subgoal):
 1. \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R proof (state)
goal (2 subgoals):
 1. \<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' []; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S []. (t, t') \<in> R
 2. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (state)
this:
t' \<in> steps (Step C) S' []
S' \<subseteq> R `` S

goal (2 subgoals):
 1. \<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' []; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S []. (t, t') \<in> R
 2. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (prove)
using this:
t' \<in> steps (Step C) S' []
S' \<subseteq> R `` S

goal (1 subgoal):
 1. \<exists>t\<in>steps (Step A) S []. (t, t') \<in> R proof (state)
this:
\<exists>t\<in>steps (Step A) S []. (t, t') \<in> R

goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (state)
goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (state)
this:
\<lbrakk>t' \<in> steps (Step C) ?S' js; ?S' \<subseteq> R `` ?S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) ?S js. (t, t') \<in> R
t' \<in> steps (Step C) S' (j # js)
S' \<subseteq> R `` S

goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (prove)
using this:
\<lbrakk>t' \<in> steps (Step C) ?S' js; ?S' \<subseteq> R `` ?S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) ?S js. (t, t') \<in> R
t' \<in> steps (Step C) S' (j # js)
S' \<subseteq> R `` S

goal (1 subgoal):
 1. t' \<in> steps (Step C) (Step C j `` S') js proof (state)
this:
t' \<in> steps (Step C) (Step C j `` S') js

goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (state)
this:
t' \<in> steps (Step C) (Step C j `` S') js

goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (state)
this:
t' \<in> steps (Step C) (Step C j `` S') js

goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (chain)
picking this:
t' \<in> steps (Step C) S' (j # js)
S' \<subseteq> R `` S proof (prove)
using this:
t' \<in> steps (Step C) S' (j # js)
S' \<subseteq> R `` S

goal (1 subgoal):
 1. S' \<subseteq> R `` S proof (state)
this:
S' \<subseteq> R `` S

goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (state)
this:
S' \<subseteq> R `` S

goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (chain)
picking this:
fw_sim R C A proof (prove)
using this:
fw_sim R C A

goal (1 subgoal):
 1. R ;;; Step C j \<subseteq> Step A j ;;; R proof (state)
this:
R ;;; Step C j \<subseteq> Step A j ;;; R

goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (chain)
picking this:
S' \<subseteq> R `` S
R ;;; Step C j \<subseteq> Step A j ;;; R proof (prove)
using this:
S' \<subseteq> R `` S
R ;;; Step C j \<subseteq> Step A j ;;; R

goal (1 subgoal):
 1. Step C j `` S' \<subseteq> R `` Step A j `` S proof (state)
this:
Step C j `` S' \<subseteq> R `` Step A j `` S

goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (state)
this:
Step C j `` S' \<subseteq> R `` Step A j `` S

goal (1 subgoal):
 1. \<And>a js S' S. \<lbrakk>\<And>S' S. \<lbrakk>t' \<in> steps (Step C) S' js; S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S js. (t, t') \<in> R; t' \<in> steps (Step C) S' (a # js); S' \<subseteq> R `` S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) S (a # js). (t, t') \<in> R proof (chain)
picking this:
t' \<in> steps (Step C) (Step C j `` S') js
Step C j `` S' \<subseteq> R `` Step A j `` S proof (prove)
using this:
t' \<in> steps (Step C) (Step C j `` S') js
Step C j `` S' \<subseteq> R `` Step A j `` S

goal (1 subgoal):
 1. \<exists>t\<in>steps (Step A) S (j # js). (t, t') \<in> R proof (prove)
using this:
t' \<in> steps (Step C) (Step C j `` S') js
Step C j `` S' \<subseteq> R `` Step A j `` S
\<lbrakk>t' \<in> steps (Step C) ?S' js; ?S' \<subseteq> R `` ?S\<rbrakk> \<Longrightarrow> \<exists>t\<in>steps (Step A) ?S js. (t, t') \<in> R

goal (1 subgoal):
 1. \<exists>t\<in>steps (Step A) S (j # js). (t, t') \<in> R proof (state)
this:
\<exists>t\<in>steps (Step A) S (j # js). (t, t') \<in> R

goal:
No subgoals!