theory Plus2_Prefix

theorem plus2_n_parallel:
  "n > 0
    \<Longrightarrow> \<lbrace>\<lambda>s0 s. s = 0 \<and> s = s0\<rbrace>,\<lbrace>\<lambda>a b. a = b\<rbrace>
        fold parallel (replicate (n - 1) plus2) plus2 \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ s0 s. s = n * 2\<rbrace>" apply (rule_tac sr="\<lambda>s t. t = mainv s" in prefix_refinement_validI) apply (rule prefix_refinement_weaken_rely,
      rule_tac xs="map plus2_x [1 ..< n]" in fold_parallel_pfx_refn) apply (clarsimp simp: list_all2_conv_all_nth) apply (rule pfx_refn_plus2_x) apply (rule pfx_refn_plus2_x[where tid=0]) apply (simp add: par_tr_fin_plus2_x) apply (simp add: prefix_closed_plus2) apply (simp add: le_fun_def) apply (simp add: le_fun_def) apply simp apply (rule rg_strengthen_post, rule plus2_x_n_parallel[simplified], simp) apply clarsimp apply (clarsimp simp: plus2_xstate.splits exI[where x="\<lambda>_. 0"]) apply clarsimp apply (rule exI, strengthen refl) apply (clarsimp simp: plus2_rel_def plus2_inv_def) apply (rule fold_parallel_prefix_closed) apply (simp add: prefix_closed_plus2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<lbrace>\<lambda>s0 s. s = 0 \<and> s = s0\<rbrace>, \<lbrace>(=)\<rbrace> fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2 -, \<lbrace>\<lambda>_ s0 s. s = n * 2\<rbrace> proof (prove)
goal (5 subgoals):
 1. 0 < n \<Longrightarrow> prefix_refinement (\<lambda>s t. t = mainv s) ?isr ?osr ?rvr ?prP' ?prP ?R' (=) ?f (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2)
 2. 0 < n \<Longrightarrow> \<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 = n * 2\<rbrace>
 3. 0 < n \<Longrightarrow> \<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. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 5. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (10 subgoals):
 1. 0 < n \<Longrightarrow> list_all2 (pfx_refn (\<lambda>s t. t = mainv s) (\<lambda>_ _. True) ?prP' ?prP (\<lambda>_ _. True) (\<lambda>_ _. True)) (map plus2_x [1..<n]) (replicate (n - 1) plus2)
 2. 0 < n \<Longrightarrow> pfx_refn (\<lambda>s t. t = mainv s) (\<lambda>_ _. True) ?prP' ?prP (\<lambda>_ _. True) (\<lambda>_ _. True) ?x6 plus2
 3. 0 < n \<Longrightarrow> par_tr_fin_principle ?x6 \<and> (\<forall>x\<in>set (map plus2_x [1..<n]). par_tr_fin_principle x)
 4. 0 < n \<Longrightarrow> prefix_closed plus2 \<and> (\<forall>x\<in>set (replicate (n - 1) plus2). prefix_closed x)
 5. 0 < n \<Longrightarrow> (=) \<le> (\<lambda>_ _. True)
 6. 0 < n \<Longrightarrow> ?R' \<le> (\<lambda>_ _. True)
 7. 0 < n \<Longrightarrow> \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) ?x6 \<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 = n * 2\<rbrace>
 8. 0 < n \<Longrightarrow> \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> ?prP' s0 s \<and> ?prP t0 t \<and> t = mainv s \<and> t0 = mainv s0)
 9. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 10. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (10 subgoals):
 1. \<And>i. \<lbrakk>0 < n; i < n - Suc 0\<rbrakk> \<Longrightarrow> pfx_refn (\<lambda>s t. t = mainv s) (\<lambda>_ _. True) ?prP' ?prP (\<lambda>_ _. True) (\<lambda>_ _. True) (plus2_x (Suc i)) plus2
 2. 0 < n \<Longrightarrow> pfx_refn (\<lambda>s t. t = mainv s) (\<lambda>_ _. True) ?prP' ?prP (\<lambda>_ _. True) (\<lambda>_ _. True) ?x6 plus2
 3. 0 < n \<Longrightarrow> par_tr_fin_principle ?x6 \<and> (\<forall>x\<in>set (map plus2_x [1..<n]). par_tr_fin_principle x)
 4. 0 < n \<Longrightarrow> prefix_closed plus2 \<and> (\<forall>x\<in>set (replicate (n - 1) plus2). prefix_closed x)
 5. 0 < n \<Longrightarrow> (=) \<le> (\<lambda>_ _. True)
 6. 0 < n \<Longrightarrow> ?R' \<le> (\<lambda>_ _. True)
 7. 0 < n \<Longrightarrow> \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) ?x6 \<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 = n * 2\<rbrace>
 8. 0 < n \<Longrightarrow> \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. ?P' s0 s \<and> ?prP' s0 s \<and> ?prP t0 t \<and> t = mainv s \<and> t0 = mainv s0)
 9. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 10. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (9 subgoals):
 1. 0 < n \<Longrightarrow> pfx_refn (\<lambda>s t. t = mainv s) (\<lambda>_ _. True) (=) (\<lambda>_ _. True) (\<lambda>_ _. True) (\<lambda>_ _. True) ?x6 plus2
 2. 0 < n \<Longrightarrow> par_tr_fin_principle ?x6 \<and> (\<forall>x\<in>set (map plus2_x [1..<n]). par_tr_fin_principle x)
 3. 0 < n \<Longrightarrow> prefix_closed plus2 \<and> (\<forall>x\<in>set (replicate (n - 1) plus2). prefix_closed x)
 4. 0 < n \<Longrightarrow> (=) \<le> (\<lambda>_ _. True)
 5. 0 < n \<Longrightarrow> ?R' \<le> (\<lambda>_ _. True)
 6. 0 < n \<Longrightarrow> \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) ?x6 \<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 = n * 2\<rbrace>
 7. 0 < n \<Longrightarrow> \<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)
 8. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 9. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (8 subgoals):
 1. 0 < n \<Longrightarrow> par_tr_fin_principle (plus2_x 0) \<and> (\<forall>x\<in>set (map plus2_x [1..<n]). par_tr_fin_principle x)
 2. 0 < n \<Longrightarrow> prefix_closed plus2 \<and> (\<forall>x\<in>set (replicate (n - 1) plus2). prefix_closed x)
 3. 0 < n \<Longrightarrow> (=) \<le> (\<lambda>_ _. True)
 4. 0 < n \<Longrightarrow> ?R' \<le> (\<lambda>_ _. True)
 5. 0 < n \<Longrightarrow> \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<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 = n * 2\<rbrace>
 6. 0 < n \<Longrightarrow> \<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)
 7. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 8. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (7 subgoals):
 1. 0 < n \<Longrightarrow> prefix_closed plus2 \<and> (\<forall>x\<in>set (replicate (n - 1) plus2). prefix_closed x)
 2. 0 < n \<Longrightarrow> (=) \<le> (\<lambda>_ _. True)
 3. 0 < n \<Longrightarrow> ?R' \<le> (\<lambda>_ _. True)
 4. 0 < n \<Longrightarrow> \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<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 = n * 2\<rbrace>
 5. 0 < n \<Longrightarrow> \<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)
 6. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 7. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (6 subgoals):
 1. 0 < n \<Longrightarrow> (=) \<le> (\<lambda>_ _. True)
 2. 0 < n \<Longrightarrow> ?R' \<le> (\<lambda>_ _. True)
 3. 0 < n \<Longrightarrow> \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<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 = n * 2\<rbrace>
 4. 0 < n \<Longrightarrow> \<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)
 5. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 6. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (5 subgoals):
 1. 0 < n \<Longrightarrow> ?R' \<le> (\<lambda>_ _. True)
 2. 0 < n \<Longrightarrow> \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<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 = n * 2\<rbrace>
 3. 0 < n \<Longrightarrow> \<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. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 5. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (4 subgoals):
 1. 0 < n \<Longrightarrow> \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<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 = n * 2\<rbrace>
 2. 0 < n \<Longrightarrow> \<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. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 4. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (4 subgoals):
 1. 0 < n \<Longrightarrow> \<lbrace>?P'\<rbrace>, \<lbrace>?R'\<rbrace> fold Trace_Monad.parallel (map plus2_x [Suc 0..<n]) (plus2_x 0) -, \<lbrace>\<lambda>rv s0 s. \<forall>cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<longrightarrow> cs = n * 2\<rbrace>
 2. 0 < n \<Longrightarrow> \<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. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. ?R' s0 s \<and> t = mainv s)
 4. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (4 subgoals):
 1. \<And>v s0 s. \<lbrakk>0 < n; mainv s = n * 2\<rbrakk> \<Longrightarrow> \<forall>cs0 cs. cs0 = mainv s0 \<and> cs = mainv s \<longrightarrow> cs = n * 2
 2. 0 < n \<Longrightarrow> \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. (mainv s = 0 \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0) \<and> s0 = s \<and> True \<and> t = mainv s \<and> t0 = mainv s0)
 3. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. plus2_rel {..<n} {..<n} s0 s \<and> t = mainv s)
 4. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (3 subgoals):
 1. 0 < n \<Longrightarrow> \<forall>t0 t. t = 0 \<and> t = t0 \<longrightarrow> (\<exists>s0 s. (mainv s = 0 \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0) \<and> s0 = s \<and> True \<and> t = mainv s \<and> t0 = mainv s0)
 2. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. plus2_rel {..<n} {..<n} s0 s \<and> t = mainv s)
 3. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (2 subgoals):
 1. 0 < n \<Longrightarrow> \<forall>s0 t0 t. t0 = mainv s0 \<and> t0 = t \<longrightarrow> (\<exists>s. plus2_rel {..<n} {..<n} s0 s \<and> t = mainv s)
 2. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (2 subgoals):
 1. \<And>s0. 0 < n \<Longrightarrow> \<exists>s. plus2_rel {..<n} {..<n} s0 s \<and> mainv s0 = mainv s
 2. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (2 subgoals):
 1. \<And>s0. 0 < n \<Longrightarrow> plus2_rel {..<n} {..<n} s0 s0 \<and> True
 2. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (replicate (n - 1) plus2) plus2) proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> prefix_closed plus2 \<and> (\<forall>x\<in>set (replicate (n - 1) plus2). prefix_closed x) proof (prove)
goal:
No subgoals!