kings-crown/FVELER_Isabelle huggingface dataset:
theory Example2

lemma island_e3:
  "\<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> island s x =  {i. i \<noteq> 1 \<and> i \<noteq> 2}" apply rule apply (clarsimp simp: island_def) apply (insert tgs_connected_in_inv_image)[1] apply fastforce apply (clarsimp simp: island_def) apply (frule_tac x=x  in e0_connected_to, simp) apply (frule_tac x=xa in e0_connected_to, simp) apply (drule_tac x=0 and y=xa in directly_tgs_connected_comm) apply (rule tgs_connected_comm) apply (simp add: tgs_connected_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> island s x = {i. i \<noteq> 1 \<and> i \<noteq> 2} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> island s x \<subseteq> {i. i \<noteq> 1 \<and> i \<noteq> 2}
 2. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> {i. i \<noteq> 1 \<and> i \<noteq> 2} \<subseteq> island s x proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; s \<turnstile> x \<leftrightarrow>* xa\<rbrakk> \<Longrightarrow> xa \<noteq> 1 \<and> xa \<noteq> 2
 2. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> {i. i \<noteq> 1 \<and> i \<noteq> 2} \<subseteq> island s x proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; s \<turnstile> x \<leftrightarrow>* xa; tgs_connected s \<subseteq> inv_image Id (\<lambda>x. x = 1 \<or> x = 2)\<rbrakk> \<Longrightarrow> xa \<noteq> 1 \<and> xa \<noteq> 2
 2. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> {i. i \<noteq> 1 \<and> i \<noteq> 2} \<subseteq> island s x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> {i. i \<noteq> 1 \<and> i \<noteq> 2} \<subseteq> island s x proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; s \<turnstile> 0 \<leftrightarrow> x\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; s \<turnstile> 0 \<leftrightarrow> x; s \<turnstile> 0 \<leftrightarrow> xa\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; s \<turnstile> 0 \<leftrightarrow> x; s \<turnstile> xa \<leftrightarrow> 0\<rbrakk> \<Longrightarrow> s \<turnstile> x \<leftrightarrow>* xa proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; s \<turnstile> 0 \<leftrightarrow> x; s \<turnstile> xa \<leftrightarrow> 0\<rbrakk> \<Longrightarrow> s \<turnstile> xa \<leftrightarrow>* x proof (prove)
goal:
No subgoals!
theory Example2

lemma e2_flow_to:
  "s \<turnstile> 2 \<leadsto> x \<Longrightarrow> x = 1 \<or> x = 2" apply (rule ccontr) apply (clarsimp simp: flow_def set_flow_def island_e2 island_e3) apply (erule disjE, clarsimp) apply (erule disjE) apply (drule cap_in_caps_caps_of_to_e1, clarsimp+) apply (drule cap_in_caps_caps_of_e1, clarsimp+) apply (erule disjE) apply (drule cap_in_caps_caps_of_to_e2, clarsimp+) apply (drule cap_in_caps_caps_of_e2, clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> 2 \<leadsto> x \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> 2 \<leadsto> x; \<not> (x = 1 \<or> x = 2)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>y. y \<noteq> 1 \<and> y \<noteq> 2 \<and> (read_cap 1 \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s 1)) \<or> (\<exists>y. y \<noteq> 1 \<and> y \<noteq> 2 \<and> (read_cap 2 \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s 2)); x \<noteq> 1; x \<noteq> 2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>x \<noteq> 1; x \<noteq> 2; y \<noteq> 1; y \<noteq> 2; read_cap 1 \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s 1\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<noteq> 1; x \<noteq> 2; \<exists>y. y \<noteq> 1 \<and> y \<noteq> 2 \<and> (read_cap 2 \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s 2)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrakk>x \<noteq> 1; x \<noteq> 2; y \<noteq> 1; y \<noteq> 2; read_cap 1 \<in>cap caps_of s y\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrakk>x \<noteq> 1; x \<noteq> 2; y \<noteq> 1; y \<noteq> 2; write_cap y \<in>cap caps_of s 1\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>x \<noteq> 1; x \<noteq> 2; \<exists>y. y \<noteq> 1 \<and> y \<noteq> 2 \<and> (read_cap 2 \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s 2)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>x \<noteq> 1; x \<noteq> 2; y \<noteq> 1; y \<noteq> 2; write_cap y \<in>cap caps_of s 1\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>x \<noteq> 1; x \<noteq> 2; \<exists>y. y \<noteq> 1 \<and> y \<noteq> 2 \<and> (read_cap 2 \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s 2)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>x \<noteq> 1; x \<noteq> 2; y \<noteq> 1; y \<noteq> 2; read_cap 2 \<in>cap caps_of s y \<or> write_cap y \<in>cap caps_of s 2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>x \<noteq> 1; x \<noteq> 2; y \<noteq> 1; y \<noteq> 2; read_cap 2 \<in>cap caps_of s y\<rbrakk> \<Longrightarrow> False
 2. \<And>y. \<lbrakk>x \<noteq> 1; x \<noteq> 2; y \<noteq> 1; y \<noteq> 2; write_cap y \<in>cap caps_of s 2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>x \<noteq> 1; x \<noteq> 2; y \<noteq> 1; y \<noteq> 2; write_cap y \<in>cap caps_of s 2\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Example2

lemma flow_to_e1:
  "s \<turnstile> x \<leadsto> 1 \<Longrightarrow> x = 1 \<or> x = 2" apply (rule ccontr) apply (clarsimp simp: flow_def set_flow_def island_e1 island_e3) apply (erule disjE) apply (drule cap_in_caps_caps_of_e1, clarsimp+) apply (erule disjE) apply (drule cap_in_caps_caps_of_to_e1, clarsimp+) apply (erule disjE) apply (drule cap_in_caps_caps_of_e2, clarsimp+) apply (drule cap_in_caps_caps_of_to_e2, clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> x \<leadsto> 1 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> x \<leadsto> 1; \<not> (x = 1 \<or> x = 2)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; read_cap xa \<in>cap caps_of s 1 \<or> write_cap 1 \<in>cap caps_of s xa \<or> read_cap xa \<in>cap caps_of s 2 \<or> write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; read_cap xa \<in>cap caps_of s 1\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; write_cap 1 \<in>cap caps_of s xa \<or> read_cap xa \<in>cap caps_of s 2 \<or> write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; write_cap 1 \<in>cap caps_of s xa \<or> read_cap xa \<in>cap caps_of s 2 \<or> write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; write_cap 1 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; read_cap xa \<in>cap caps_of s 2 \<or> write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; read_cap xa \<in>cap caps_of s 2 \<or> write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; read_cap xa \<in>cap caps_of s 2\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Example2

lemma flow_to_e2:
  "s \<turnstile> x \<leadsto> 2 \<Longrightarrow> x = 1 \<or> x = 2" apply (rule ccontr) apply (clarsimp simp: flow_def set_flow_def island_e2 island_e3) apply (erule disjE) apply (drule cap_in_caps_caps_of_e1, clarsimp+) apply (erule disjE) apply (drule cap_in_caps_caps_of_to_e1, clarsimp+) apply (erule disjE) apply (drule cap_in_caps_caps_of_e2, clarsimp+) apply (drule cap_in_caps_caps_of_to_e2, clarsimp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> x \<leadsto> 2 \<Longrightarrow> x = 1 \<or> x = 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> x \<leadsto> 2; \<not> (x = 1 \<or> x = 2)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; read_cap xa \<in>cap caps_of s 1 \<or> write_cap 1 \<in>cap caps_of s xa \<or> read_cap xa \<in>cap caps_of s 2 \<or> write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; read_cap xa \<in>cap caps_of s 1\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; write_cap 1 \<in>cap caps_of s xa \<or> read_cap xa \<in>cap caps_of s 2 \<or> write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; write_cap 1 \<in>cap caps_of s xa \<or> read_cap xa \<in>cap caps_of s 2 \<or> write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; write_cap 1 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; read_cap xa \<in>cap caps_of s 2 \<or> write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; read_cap xa \<in>cap caps_of s 2 \<or> write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; read_cap xa \<in>cap caps_of s 2\<rbrakk> \<Longrightarrow> False
 2. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>x \<noteq> 1; x \<noteq> 2; xa \<noteq> 1; xa \<noteq> 2; write_cap 2 \<in>cap caps_of s xa\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Example2

lemma flow_in_inv_image:
  "(flow s) \<subseteq> inv_image Id (\<lambda> x. x=1 \<or> x=2)" by (fastforce simp: inv_image_def
              dest!: e1_flow_to flow_to_e1
                     e2_flow_to flow_to_e2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. flow s \<subseteq> inv_image Id (\<lambda>x. x = 1 \<or> x = 2)
theory Example2

lemma e0_not_flow_trans_e1:
  "\<not> s \<turnstile> 0 \<leadsto>* 1" apply clarsimp apply (drule set_mp [OF flow_trans_in_inv_image]) apply (simp add: inv_image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> s \<turnstile> 0 \<leadsto>* 1 proof (prove)
goal (1 subgoal):
 1. s \<turnstile> 0 \<leadsto>* 1 \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. (0, 1) \<in> inv_image Id (\<lambda>x. x = 1 \<or> x = 2) \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Example2

lemma e1_not_flow_trans_e0:
  "\<not> s \<turnstile> 1 \<leadsto>* 0" apply clarsimp apply (drule set_mp [OF flow_trans_in_inv_image]) apply (simp add: inv_image_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> s \<turnstile> 1 \<leadsto>* 0 proof (prove)
goal (1 subgoal):
 1. s \<turnstile> 1 \<leadsto>* 0 \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. (1, 0) \<in> inv_image Id (\<lambda>x. x = 1 \<or> x = 2) \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Example2

lemma e0_e1_isolated:
  "s' \<in> execute cmds s \<Longrightarrow> \<not> s' \<turnstile> 0 \<leadsto>* 1 \<and> \<not> s' \<turnstile> 1 \<leadsto>* 0" apply (rule conjI) apply (erule information_flow) apply (rule e0_not_flow_trans_e1) apply (erule information_flow) apply (rule e1_not_flow_trans_e0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s' \<in> execute cmds s \<Longrightarrow> \<not> s' \<turnstile> 0 \<leadsto>* 1 \<and> \<not> s' \<turnstile> 1 \<leadsto>* 0 proof (prove)
goal (2 subgoals):
 1. s' \<in> execute cmds s \<Longrightarrow> \<not> s' \<turnstile> 0 \<leadsto>* 1
 2. s' \<in> execute cmds s \<Longrightarrow> \<not> s' \<turnstile> 1 \<leadsto>* 0 proof (prove)
goal (2 subgoals):
 1. \<not> s \<turnstile> 0 \<leadsto>* 1
 2. s' \<in> execute cmds s \<Longrightarrow> \<not> s' \<turnstile> 1 \<leadsto>* 0 proof (prove)
goal (1 subgoal):
 1. s' \<in> execute cmds s \<Longrightarrow> \<not> s' \<turnstile> 1 \<leadsto>* 0 proof (prove)
goal (1 subgoal):
 1. \<not> s \<turnstile> 1 \<leadsto>* 0 proof (prove)
goal:
No subgoals!
theory Simulation

lemma hoare_triple_refinement:
  "C \<sqsubseteq> A = (\<forall>P Q js. hoare_triple A P js Q \<longrightarrow> hoare_triple C P js Q)" by (simp add: refines_def hoare_triple_def) blast


\<comment> \<open>composing two relations\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. C \<sqsubseteq> A = (\<forall>P Q js. hoare_triple A P js Q \<longrightarrow> hoare_triple C P js Q)
theory Simulation

lemma sim_imp_refines:
  "C \<sqsubseteq>\<^sub>F A \<Longrightarrow> C \<sqsubseteq> A" apply (clarsimp simp: refines_def execution_def fw_simulates_def) apply (rename_tac t) apply (drule fw_sim_steps) prefer 2 apply assumption apply (simp add: fw_sim_def) apply blast apply clarsimp apply (erule rev_image_eqI) apply (simp add: fw_sim_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. C \<sqsubseteq>\<^sub>F A \<Longrightarrow> C \<sqsubseteq> A proof (prove)
goal (1 subgoal):
 1. \<And>R js s xa. \<lbrakk>fw_sim R C A; xa \<in> steps (Step C) (Init C s) js\<rbrakk> \<Longrightarrow> Fin C xa \<in> Fin A ` steps (Step A) (Init A s) js proof (prove)
goal (1 subgoal):
 1. \<And>R js s t. \<lbrakk>fw_sim R C A; t \<in> steps (Step C) (Init C s) js\<rbrakk> \<Longrightarrow> Fin C t \<in> Fin A ` steps (Step A) (Init A s) js proof (prove)
goal (3 subgoals):
 1. \<And>R js s t. fw_sim R C A \<Longrightarrow> Init C s \<subseteq> ?R10 R js s t `` ?S10 R js s t
 2. \<And>R js s t. fw_sim R C A \<Longrightarrow> fw_sim (?R10 R js s t) C (?A10 R js s t)
 3. \<And>R js s t. \<lbrakk>fw_sim R C A; \<exists>ta\<in>steps (Step (?A10 R js s t)) (?S10 R js s t) js. (ta, t) \<in> ?R10 R js s t\<rbrakk> \<Longrightarrow> Fin C t \<in> Fin A ` steps (Step A) (Init A s) js proof (prove)
goal (3 subgoals):
 1. \<And>R js s t. fw_sim R C A \<Longrightarrow> fw_sim (?R10 R js s t) C (?A10 R js s t)
 2. \<And>R js s t. fw_sim R C A \<Longrightarrow> Init C s \<subseteq> ?R10 R js s t `` ?S10 R js s t
 3. \<And>R js s t. \<lbrakk>fw_sim R C A; \<exists>ta\<in>steps (Step (?A10 R js s t)) (?S10 R js s t) js. (ta, t) \<in> ?R10 R js s t\<rbrakk> \<Longrightarrow> Fin C t \<in> Fin A ` steps (Step A) (Init A s) js proof (prove)
goal (2 subgoals):
 1. \<And>R js s t. fw_sim R C A \<Longrightarrow> Init C s \<subseteq> R `` ?S10 R js s t
 2. \<And>R js s t. \<lbrakk>fw_sim R C A; \<exists>ta\<in>steps (Step A) (?S10 R js s t) js. (ta, t) \<in> R\<rbrakk> \<Longrightarrow> Fin C t \<in> Fin A ` steps (Step A) (Init A s) js proof (prove)
goal (2 subgoals):
 1. \<And>R js s t. (\<forall>s. Init C s \<subseteq> R `` Init A s) \<and> (\<forall>j. R ;;; Step C j \<subseteq> Step A j ;;; R) \<and> (\<forall>s s'. (s, s') \<in> R \<longrightarrow> Fin C s' = Fin A s) \<Longrightarrow> Init C s \<subseteq> R `` ?S10 R js s t
 2. \<And>R js s t. \<lbrakk>fw_sim R C A; \<exists>ta\<in>steps (Step A) (?S10 R js s t) js. (ta, t) \<in> R\<rbrakk> \<Longrightarrow> Fin C t \<in> Fin A ` steps (Step A) (Init A s) js proof (prove)
goal (1 subgoal):
 1. \<And>R js s t. \<lbrakk>fw_sim R C A; \<exists>ta\<in>steps (Step A) (Init A s) js. (ta, t) \<in> R\<rbrakk> \<Longrightarrow> Fin C t \<in> Fin A ` steps (Step A) (Init A s) js proof (prove)
goal (1 subgoal):
 1. \<And>R js s t ta. \<lbrakk>fw_sim R C A; ta \<in> steps (Step A) (Init A s) js; (ta, t) \<in> R\<rbrakk> \<Longrightarrow> Fin C t \<in> Fin A ` steps (Step A) (Init A s) js proof (prove)
goal (1 subgoal):
 1. \<And>R js s t ta. \<lbrakk>fw_sim R C A; (ta, t) \<in> R\<rbrakk> \<Longrightarrow> Fin C t = Fin A ta proof (prove)
goal:
No subgoals!
theory Simulation

lemma invariant_T [iff]: "D \<Turnstile> UNIV" by (simp add: invariant_holds_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. D \<Turnstile> UNIV
theory Simulation

lemma invariantI:
  "\<lbrakk> \<forall>s. Init D s \<subseteq> I; \<forall>j. Step D j `` I \<subseteq> I \<rbrakk> \<Longrightarrow> D \<Turnstile> I" by (simp add: invariant_holds_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. Init D s \<subseteq> I; \<forall>j. Step D j `` I \<subseteq> I\<rbrakk> \<Longrightarrow> D \<Turnstile> I
theory Simulation

lemma invariant_CollectI [intro?]:
  assumes init: "\<And>s a. s \<in> Init D a \<Longrightarrow> I s"
  assumes step: "\<And>j s s'. \<lbrakk> I s; (s,s') \<in> Step D j \<rbrakk> \<Longrightarrow> I s'"
  shows "D \<Turnstile> Collect I" proof (rule invariantI) show "\<forall>a. Init D a \<subseteq> Collect I" by (fast intro: init) next show "\<forall>j. Step D j `` Collect I \<subseteq> Collect I" by (auto simp add: Image_def intro: step) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. D \<Turnstile> Collect I proof (state)
goal (2 subgoals):
 1. \<forall>s. Init D s \<subseteq> Collect I
 2. \<forall>j. Step D j `` Collect I \<subseteq> Collect I proof (prove)
goal (1 subgoal):
 1. \<forall>a. Init D a \<subseteq> Collect I proof (state)
this:
\<forall>a. Init D a \<subseteq> Collect I

goal (1 subgoal):
 1. \<forall>j. Step D j `` Collect I \<subseteq> Collect I proof (state)
goal (1 subgoal):
 1. \<forall>j. Step D j `` Collect I \<subseteq> Collect I proof (prove)
goal (1 subgoal):
 1. \<forall>j. Step D j `` Collect I \<subseteq> Collect I proof (state)
this:
\<forall>j. Step D j `` Collect I \<subseteq> Collect I

goal:
No subgoals!
theory Simulation

lemma invariant_conjI2:
  "\<lbrakk> D \<Turnstile> I; \<And>s. Init D s \<subseteq> I \<Longrightarrow> Init D s \<subseteq> J;
    \<forall>j. Step D j `` (I \<inter> J) \<subseteq> J \<rbrakk> \<Longrightarrow> D \<Turnstile> I \<inter> J" by (simp add: invariant_holds_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>D \<Turnstile> I; \<And>s. Init D s \<subseteq> I \<Longrightarrow> Init D s \<subseteq> J; \<forall>j. Step D j `` (I \<inter> J) \<subseteq> J\<rbrakk> \<Longrightarrow> D \<Turnstile> I \<inter> J
theory Simulation

lemma fw_sim_eq_LI: "fw_sim r C A = LI A C r UNIV" by (simp add: fw_sim_def LI_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fw_sim r C A = LI A C r UNIV
theory Simulation

lemma fw_sim_LI: "fw_sim r C A \<Longrightarrow> LI A C r I" by (simp add: fw_sim_eq_LI weaken_LI[where I'=UNIV])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fw_sim r C A \<Longrightarrow> LI A C r I
theory Simulation

lemma refinement_refl[simp]:
  "A \<sqsubseteq> A" by (simp add: refines_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<sqsubseteq> A
theory Simulation

lemma refinement_trans [trans]:
  "\<lbrakk>C \<sqsubseteq> B; B \<sqsubseteq> A\<rbrakk> \<Longrightarrow> C \<sqsubseteq> A" by (simp add: refines_def) blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<sqsubseteq> B; B \<sqsubseteq> A\<rbrakk> \<Longrightarrow> C \<sqsubseteq> A
theory Simulation

lemma fw_sim_trans:
  "\<lbrakk>fw_sim Q C B; fw_sim R B A\<rbrakk> \<Longrightarrow> fw_sim (R O Q) C A" by (auto simp: fw_sim_def rel_semi_def; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fw_sim Q C B; fw_sim R B A\<rbrakk> \<Longrightarrow> fw_sim (R O Q) C A
theory Simulation

lemma fw_simulates_trans:
  "\<lbrakk>C \<sqsubseteq>\<^sub>F B; B \<sqsubseteq>\<^sub>F A\<rbrakk> \<Longrightarrow> C \<sqsubseteq>\<^sub>F A" apply (auto simp: fw_simulates_def dest: fw_sim_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<sqsubseteq>\<^sub>F B; B \<sqsubseteq>\<^sub>F A\<rbrakk> \<Longrightarrow> C \<sqsubseteq>\<^sub>F A proof (prove)
goal:
No subgoals!
theory WPEx

lemma in_mresults_export:
  "(rv, s', s) \<in> mresults (assert_value_exported (rv', s'') f rv'')
      = ((rv, s', s) \<in> mresults f \<and> rv' = rv'' \<and> s'' = s)" by (simp add: assert_value_exported_def mresults_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rv, s', s) \<in> mresults (assert_value_exported (rv', s'') f rv'')) = ((rv, s', s) \<in> mresults f \<and> rv' = rv'' \<and> s'' = s)
theory WPEx

lemma in_mresults_bind:
  "(rv, s', s) \<in> mresults (a >>= b)
       = (\<exists>rv' s''. (rv, s', s'') \<in> mresults (b rv') \<and> (rv', s'', s) \<in> mresults a)" by (auto simp: mresults_def bind_def elim: rev_bexI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rv, s', s) \<in> mresults (a >>= b)) = (\<exists>rv' s''. (rv, s', s'') \<in> mresults (b rv') \<and> (rv', s'', s) \<in> mresults a)
theory WPEx

lemma mresults_export_bindD:
  "(rv, s', s) \<in> mresults (a >>= assert_value_exported (rv', s'') b) \<Longrightarrow> (rv, s', s'') \<in> mresults b"
  "(rv, s', s) \<in> mresults (a >>= assert_value_exported (rv', s'') b) \<Longrightarrow> (rv', s'', s) \<in> mresults a" by (simp_all add: in_mresults_export in_mresults_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rv, s', s) \<in> mresults (a >>= assert_value_exported (rv', s'') b) \<Longrightarrow> (rv, s', s'') \<in> mresults b) &&& ((rv, s', s) \<in> mresults (a >>= assert_value_exported (rv', s'') b) \<Longrightarrow> (rv', s'', s) \<in> mresults a)
theory WPEx

lemma use_valid_mresults:
  "\<lbrakk> (rv, s', s) \<in> mresults f; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> P s \<longrightarrow> Q rv s'" by (auto simp: mresults_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(rv, s', s) \<in> mresults f; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> P s \<longrightarrow> Q rv s'