theory Plus2_Prefix

theorem plus2_parallel:
  "\<lbrace>\<lambda>s0 s. s = 0 \<and> s = s0\<rbrace>,\<lbrace>\<lambda>a b. a = b\<rbrace>
    parallel plus2 plus2 \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ s0 s. s = 4\<rbrace>" apply (rule_tac sr="\<lambda>s t. t = mainv s" in prefix_refinement_validI) apply (rule prefix_refinement_parallel_triv;
      ((rule par_tr_fin_plus2_x prefix_closed_plus2)?)) apply (rule pfx_refn_plus2_x[where tid=1]) apply (rule pfx_refn_plus2_x[where tid=2]) apply clarsimp apply (rule rg_strengthen_post) apply (rule plus2_x_parallel[simplified]) apply clarsimp apply (clarsimp simp: plus2_xstate.splits) apply (strengthen exI[where x="f(1 := x, 2 := y)" for f x y]) apply simp apply clarsimp apply (intro prefix_closed_parallel prefix_closed_plus2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. s = 0 \<and> s = s0\<rbrace>, \<lbrace>(=)\<rbrace> Trace_Monad.parallel plus2 plus2 -, \<lbrace>\<lambda>_ s0 s. s = 4\<rbrace> proof (prove)
goal (5 subgoals):
 1. prefix_refinement (\<lambda>s t. t = mainv s) ?isr ?osr ?rvr ?prP' ?prP ?R' (=) ?f (Trace_Monad.parallel plus2 plus2)
 2. \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> ?f \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<longrightarrow> True\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. cs0 = mainv s0 \<and> ?osr s cs \<and> ?rvr rv rv' \<longrightarrow> cs = 4\<rbrace>
 3. \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> ?prP' s0 s \<and> ?prP t0 t \<and> ?isr s t \<and> t0 = mainv s0)
 4. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 5. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (6 subgoals):
 1. prefix_refinement (\<lambda>s t. t = mainv s) ?isr ?osr ?rvr ?prP' ?prP (?R' or (\<lambda>_ _. True)) ((=) or (\<lambda>_ _. True)) (plus2_x ?tid19) plus2
 2. prefix_refinement (\<lambda>s t. t = mainv s) ?isr ?osr ?rvr ?prP' ?prP (?R' or (\<lambda>_ _. True)) ((=) or (\<lambda>_ _. True)) (plus2_x ?tid16) plus2
 3. \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> Trace_Monad.parallel (plus2_x ?tid19) (plus2_x ?tid16) \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<longrightarrow> True\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. cs0 = mainv s0 \<and> ?osr s cs \<and> ?rvr rv rv' \<longrightarrow> cs = 4\<rbrace>
 4. \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> ?prP' s0 s \<and> ?prP t0 t \<and> ?isr s t \<and> t0 = mainv s0)
 5. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 6. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (5 subgoals):
 1. pfx_refn (\<lambda>s t. t = mainv s) (\<lambda>_ _. True) (=) (\<lambda>_ _. True) (?R' or (\<lambda>_ _. True)) ((=) or (\<lambda>_ _. True)) (plus2_x ?tid16) plus2
 2. \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> Trace_Monad.parallel (plus2_x 1) (plus2_x ?tid16) \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<longrightarrow> True\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<and> True \<longrightarrow> cs = 4\<rbrace>
 3. \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> s0 = s \<and> True \<and> t = mainv s \<and> t0 = mainv s0)
 4. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 5. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> Trace_Monad.parallel (plus2_x 1) (plus2_x 2) \<lbrace>\<lambda>s0 s. \<forall>cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<longrightarrow> True\<rbrace>, \<lbrace>\<lambda>rv s0 s. \<forall>rv' cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<and> True \<longrightarrow> cs = 4\<rbrace>
 2. \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> s0 = s \<and> True \<and> t = mainv s \<and> t0 = mainv s0)
 3. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 4. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> Trace_Monad.parallel (plus2_x (Suc 0)) (plus2_x 2) -, \<lbrace>\<lambda>rv s0 s. \<forall>cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<longrightarrow> cs = 4\<rbrace>
 2. \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> s0 = s \<and> True \<and> t = mainv s \<and> t0 = mainv s0)
 3. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 4. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (5 subgoals):
 1. \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> Trace_Monad.parallel (plus2_x (Suc 0)) (plus2_x 2) -, \<lbrace>?Q'29\<rbrace>
 2. \<And>v s0 s. ?Q'29 v s0 s \<Longrightarrow> \<forall>cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<longrightarrow> cs = 4
 3. \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> s0 = s \<and> True \<and> t = mainv s \<and> t0 = mainv s0)
 4. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 5. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (4 subgoals):
 1. \<And>v s0 s. mainv s = 4 \<Longrightarrow> \<forall>cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<longrightarrow> cs = 4
 2. \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. (mainv s = 0 \<and> threadv s (Suc 0) = 0 \<and> threadv s 2 = 0 \<and> s = s0) \<and> s0 = s \<and> True \<and> t = mainv s \<and> t0 = mainv s0)
 3. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. s0 = s \<and> t = mainv s)
 4. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (3 subgoals):
 1. \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. (mainv s = 0 \<and> threadv s (Suc 0) = 0 \<and> threadv s 2 = 0 \<and> s = s0) \<and> s0 = s \<and> True \<and> t = mainv s \<and> t0 = mainv s0)
 2. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. s0 = s \<and> t = mainv s)
 3. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (3 subgoals):
 1. \<exists>threadv. threadv (Suc 0) = 0 \<and> threadv 2 = 0
 2. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. s0 = s \<and> t = mainv s)
 3. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (3 subgoals):
 1. \<exists>y x f. (f(1 := x, 2 := y)) (Suc 0) = 0 \<and> (f(1 := x, 2 := y)) 2 = 0
 2. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. s0 = s \<and> t = mainv s)
 3. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (2 subgoals):
 1. \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. s0 = s \<and> t = mainv s)
 2. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal (1 subgoal):
 1. prefix_closed (Trace_Monad.parallel plus2 plus2) proof (prove)
goal:
No subgoals!