theory ADT_IF

lemma Step_system_to_enabled_system:
  assumes single_event: "(\<forall>(x::'b) (y::'b). x = y)"
  assumes st: "Step_system A s0"
  assumes en: "\<And>s. system.reachable A s0 s \<Longrightarrow> \<exists>(x::'b) s'. (s,s') \<in> system.Step A x"
  shows "enabled_system A s0" apply (clarsimp simp: enabled_system_def) proof - fix s  js jsa assume a: "s \<in> execution A s0 js" show "\<exists>s'. s' \<in> execution A s jsa" proof - have er: "\<And>as. execution A s as = {s'. (s,s') \<in> Run (system.Step A) as}" apply (rule Step_system.execution_Run[OF st]) using a apply (fastforce simp: system.reachable_def) done show ?thesis apply (induct jsa rule: rev_induct) apply (simp add: er) apply (clarsimp simp: er) apply (cut_tac s=s' in en) apply (rule Step_system.reachable_execution[OF st]) using a apply (fastforce simp: system.reachable_def) apply (simp add: er) apply clarify apply (rename_tac b s'a) apply (rule_tac x=s'a in exI) apply (rule Run_trans, assumption) apply (rule system_Step_one) apply (cut_tac x=b and xa=x in single_event[rule_format], simp) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. enabled_system A s0 proof (prove)
goal (1 subgoal):
 1. \<And>s js jsa. s \<in> execution A s0 js \<Longrightarrow> \<exists>s'. s' \<in> execution A s jsa proof (state)
goal (1 subgoal):
 1. \<And>s js jsa. s \<in> execution A s0 js \<Longrightarrow> \<exists>s'. s' \<in> execution A s jsa proof (state)
goal (1 subgoal):
 1. \<And>s js jsa. s \<in> execution A s0 js \<Longrightarrow> \<exists>s'. s' \<in> execution A s jsa proof (state)
this:
s \<in> execution A s0 js

goal (1 subgoal):
 1. \<And>s js jsa. s \<in> execution A s0 js \<Longrightarrow> \<exists>s'. s' \<in> execution A s jsa proof (prove)
goal (1 subgoal):
 1. \<exists>s'. s' \<in> execution A s jsa proof (state)
goal (1 subgoal):
 1. \<exists>s'. s' \<in> execution A s jsa proof (prove)
goal (1 subgoal):
 1. \<And>as. execution A s as = {s'. (s, s') \<in> Run (system.Step A) as} proof (prove)
goal (1 subgoal):
 1. \<And>as. system.reachable A s0 s proof (prove)
using this:
s \<in> execution A s0 js

goal (1 subgoal):
 1. \<And>as. system.reachable A s0 s proof (prove)
goal:
No subgoals! proof (state)
this:
execution A s ?as = {s'. (s, s') \<in> Run (system.Step A) ?as}

goal (1 subgoal):
 1. \<exists>s'. s' \<in> execution A s jsa proof (prove)
goal (1 subgoal):
 1. \<exists>s'. s' \<in> execution A s jsa proof (prove)
goal (2 subgoals):
 1. \<exists>s'. s' \<in> execution A s []
 2. \<And>x xs. \<exists>s'. s' \<in> execution A s xs \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<exists>s'. s' \<in> execution A s xs \<Longrightarrow> \<exists>s'. s' \<in> execution A s (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s'. (s, s') \<in> Run (system.Step A) xs \<Longrightarrow> \<exists>s'. (s, s') \<in> Run (system.Step A) (xs @ [x]) proof (prove)
goal (2 subgoals):
 1. \<And>x xs s'. (s, s') \<in> Run (system.Step A) xs \<Longrightarrow> system.reachable A s0 s'
 2. \<And>x xs s'. \<lbrakk>(s, s') \<in> Run (system.Step A) xs; \<exists>x s'a. (s', s'a) \<in> system.Step A x\<rbrakk> \<Longrightarrow> \<exists>s'. (s, s') \<in> Run (system.Step A) (xs @ [x]) proof (prove)
goal (3 subgoals):
 1. \<And>x xs s'. (s, s') \<in> Run (system.Step A) xs \<Longrightarrow> system.reachable A s0 (?s5 x xs s')
 2. \<And>x xs s'. (s, s') \<in> Run (system.Step A) xs \<Longrightarrow> s' \<in> execution A (?s5 x xs s') (?js5 x xs s')
 3. \<And>x xs s'. \<lbrakk>(s, s') \<in> Run (system.Step A) xs; \<exists>x s'a. (s', s'a) \<in> system.Step A x\<rbrakk> \<Longrightarrow> \<exists>s'. (s, s') \<in> Run (system.Step A) (xs @ [x]) proof (prove)
using this:
s \<in> execution A s0 js

goal (3 subgoals):
 1. \<And>x xs s'. (s, s') \<in> Run (system.Step A) xs \<Longrightarrow> system.reachable A s0 (?s5 x xs s')
 2. \<And>x xs s'. (s, s') \<in> Run (system.Step A) xs \<Longrightarrow> s' \<in> execution A (?s5 x xs s') (?js5 x xs s')
 3. \<And>x xs s'. \<lbrakk>(s, s') \<in> Run (system.Step A) xs; \<exists>x s'a. (s', s'a) \<in> system.Step A x\<rbrakk> \<Longrightarrow> \<exists>s'. (s, s') \<in> Run (system.Step A) (xs @ [x]) proof (prove)
goal (2 subgoals):
 1. \<And>x xs s'. (s, s') \<in> Run (system.Step A) xs \<Longrightarrow> s' \<in> execution A s (?js5 x xs s')
 2. \<And>x xs s'. \<lbrakk>(s, s') \<in> Run (system.Step A) xs; \<exists>x s'a. (s', s'a) \<in> system.Step A x\<rbrakk> \<Longrightarrow> \<exists>s'. (s, s') \<in> Run (system.Step A) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s'. \<lbrakk>(s, s') \<in> Run (system.Step A) xs; \<exists>x s'a. (s', s'a) \<in> system.Step A x\<rbrakk> \<Longrightarrow> \<exists>s'. (s, s') \<in> Run (system.Step A) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s' xa s'a. \<lbrakk>(s, s') \<in> Run (system.Step A) xs; (s', s'a) \<in> system.Step A xa\<rbrakk> \<Longrightarrow> \<exists>s'. (s, s') \<in> Run (system.Step A) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s' b s'a. \<lbrakk>(s, s') \<in> Run (system.Step A) xs; (s', s'a) \<in> system.Step A b\<rbrakk> \<Longrightarrow> \<exists>s'. (s, s') \<in> Run (system.Step A) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s' b s'a. \<lbrakk>(s, s') \<in> Run (system.Step A) xs; (s', s'a) \<in> system.Step A b\<rbrakk> \<Longrightarrow> (s, s'a) \<in> Run (system.Step A) (xs @ [x]) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s' b s'a. \<lbrakk>(s, s') \<in> Run (system.Step A) xs; (s', s'a) \<in> system.Step A b\<rbrakk> \<Longrightarrow> (s', s'a) \<in> Run (system.Step A) [x] proof (prove)
goal (1 subgoal):
 1. \<And>x xs s' b s'a. \<lbrakk>(s, s') \<in> Run (system.Step A) xs; (s', s'a) \<in> system.Step A b\<rbrakk> \<Longrightarrow> (s', s'a) \<in> system.Step A x proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>s'. s' \<in> execution A s jsa

goal:
No subgoals! proof (state)
this:
\<exists>s'. s' \<in> execution A s jsa

goal:
No subgoals!