theory Confine_S

lemma connected_tgs_connected:
  "\<lbrakk>s' \<in> step cmd s; (e\<^sub>x, e\<^sub>y) \<in> directly_tgs_connected s'\<rbrakk> \<Longrightarrow>
  (e\<^sub>x, e\<^sub>y) \<in> tgs_connected s" apply(case_tac "(e\<^sub>x, e\<^sub>y) \<in> directly_tgs_connected s") apply(simp add: tgs_connected_def) apply(case_tac cmd) apply(rule create_conTrans, fastforce+) apply(rule take_conTrans, fastforce+) apply(rule grant_conTrans, fastforce+) apply(frule copy_conTrans, fastforce+) apply(frule remove_conTrans, fastforce+) apply(frule removeSet_conTrans, fastforce+) apply(frule revoke_conTrans, fastforce+) apply(frule destroy_conTrans, fastforce+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 2. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysCreate x11 x12 x13\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 2. \<And>x21 x22 x23 x24. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysTake x21 x22 x23 x24\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 3. \<And>x31 x32 x33 x34. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysGrant x31 x32 x33 x34\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 4. \<And>x41 x42 x43 x44. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysCopy x41 x42 x43 x44\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 5. \<And>x51 x52 x53. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemove x51 x52 x53\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 6. \<And>x61 x62 x63. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 7. \<And>x71 x72. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 8. \<And>x81 x82. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal (7 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysTake x21 x22 x23 x24\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 2. \<And>x31 x32 x33 x34. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysGrant x31 x32 x33 x34\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 3. \<And>x41 x42 x43 x44. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysCopy x41 x42 x43 x44\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 4. \<And>x51 x52 x53. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemove x51 x52 x53\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 5. \<And>x61 x62 x63. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 6. \<And>x71 x72. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 7. \<And>x81 x82. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysGrant x31 x32 x33 x34\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 2. \<And>x41 x42 x43 x44. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysCopy x41 x42 x43 x44\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 3. \<And>x51 x52 x53. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemove x51 x52 x53\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 4. \<And>x61 x62 x63. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 5. \<And>x71 x72. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 6. \<And>x81 x82. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 x44. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysCopy x41 x42 x43 x44\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 2. \<And>x51 x52 x53. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemove x51 x52 x53\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 3. \<And>x61 x62 x63. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 4. \<And>x71 x72. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 5. \<And>x81 x82. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal (4 subgoals):
 1. \<And>x51 x52 x53. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemove x51 x52 x53\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 2. \<And>x61 x62 x63. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 3. \<And>x71 x72. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 4. \<And>x81 x82. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal (3 subgoals):
 1. \<And>x61 x62 x63. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRemoveSet x61 x62 x63\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 2. \<And>x71 x72. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 3. \<And>x81 x82. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal (2 subgoals):
 1. \<And>x71 x72. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysRevoke x71 x72\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y
 2. \<And>x81 x82. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal (1 subgoal):
 1. \<And>x81 x82. \<lbrakk>s' \<in> step cmd s; s' \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; \<not> s \<turnstile> e\<^sub>x \<leftrightarrow> e\<^sub>y; cmd = SysDestroy x81 x82\<rbrakk> \<Longrightarrow> s \<turnstile> e\<^sub>x \<leftrightarrow>* e\<^sub>y proof (prove)
goal:
No subgoals!