theory Plus2_Prefix

lemma plus2_x_n_parallel_induct:
  "n > 0 \<Longrightarrow> n \<le> N \<Longrightarrow>
  \<lbrace>\<lambda>s0 s. plus2_inv {..< N} s \<and> (\<forall>i < N. threadv s i = 0) \<and> s = s0\<rbrace>,\<lbrace>plus2_rel {..< N} {..< n}\<rbrace>
    fold parallel (map plus2_x [1 ..< n]) (plus2_x 0) \<lbrace>plus2_rel {..< N} ( - {..< n})\<rbrace>,\<lbrace>\<lambda>_ _ s.
        plus2_inv {..< N} s \<and> (\<forall>i < n. threadv s i = 2)\<rbrace>" apply (induct n) apply simp apply (case_tac n) apply (simp only: lessThan_Suc) apply simp apply (wp plus2_x_property) apply clarsimp apply (clarsimp split del: if_split) apply (rule rg_weaken_pre, rule rg_strengthen_post,
    rule rg_validI, rule plus2_x_property[where tids="{..< N}"],
    assumption, (clarsimp simp: plus2_rel_def)+) apply (auto dest: less_Suc_eq[THEN iffD1])[1] apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < 0; 0 \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<0}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<0]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<0})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<0. threadv s i = 2)\<rbrace>
 2. \<And>n. \<lbrakk>\<lbrakk>0 < n; n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrace>; 0 < Suc n; Suc n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<Suc n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<Suc n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc n. threadv s i = 2)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>0 < n; n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrace>; 0 < Suc n; Suc n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<Suc n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<Suc n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc n. threadv s i = 2)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<lbrakk>0 < n; n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrace>; 0 < Suc n; Suc n \<le> N; n = 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<Suc n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<Suc n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc n. threadv s i = 2)\<rbrace>
 2. \<And>n nat. \<lbrakk>\<lbrakk>0 < n; n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrace>; 0 < Suc n; Suc n \<le> N; n = Suc nat\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<Suc n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<Suc n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc n. threadv s i = 2)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<lbrakk>0 < 0; 0 \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<0}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<0]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<0})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<0. threadv s i = 2)\<rbrace>; 0 < Suc 0; Suc 0 \<le> N; n = 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} (insert 0 {..<0})\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<Suc 0]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- insert 0 {..<0})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc 0. threadv s i = 2)\<rbrace>
 2. \<And>n nat. \<lbrakk>\<lbrakk>0 < n; n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrace>; 0 < Suc n; Suc n \<le> N; n = Suc nat\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<Suc n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<Suc n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc n. threadv s i = 2)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>Suc 0 \<le> N; n = 0\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {0}\<rbrace> plus2_x 0 \<lbrace>plus2_rel {..<N} (- {0})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> threadv s 0 = 2\<rbrace>
 2. \<And>n nat. \<lbrakk>\<lbrakk>0 < n; n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrace>; 0 < Suc n; Suc n \<le> N; n = Suc nat\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<Suc n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<Suc n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc n. threadv s i = 2)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>n s0 s. \<lbrakk>Suc 0 \<le> N; n = 0; plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrakk> \<Longrightarrow> plus2_inv {..<N} s \<and> threadv s 0 = 0 \<and> s = s0 \<and> 0 \<in> {..<N} \<and> finite {..<N}
 2. \<And>n nat. \<lbrakk>\<lbrakk>0 < n; n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrace>; 0 < Suc n; Suc n \<le> N; n = Suc nat\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<Suc n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<Suc n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc n. threadv s i = 2)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>n nat. \<lbrakk>\<lbrakk>0 < n; n \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrace>; 0 < Suc n; Suc n \<le> N; n = Suc nat\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<Suc n]) (plus2_x 0) \<lbrace>plus2_rel {..<N} (- {..<Suc n})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc n. threadv s i = 2)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>\<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc nat}\<rbrace> fold Trace_Monad.parallel (map plus2_x (if Suc 0 \<le> nat then [Suc 0..<nat] @ [nat] else [])) (plus2_x 0) \<lbrace>plus2_rel {..<N} {Suc nat..}\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc nat. threadv s i = 2)\<rbrace>; Suc (Suc nat) \<le> N\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc (Suc nat)}\<rbrace> Trace_Monad.parallel (plus2_x (Suc nat)) (fold Trace_Monad.parallel (map plus2_x (if Suc 0 \<le> nat then [Suc 0..<nat] @ [nat] else [])) (plus2_x 0)) \<lbrace>plus2_rel {..<N} {Suc (Suc nat)..}\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc (Suc nat). threadv s i = 2)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>nat s i. \<lbrakk>\<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc nat}\<rbrace> fold Trace_Monad.parallel (map plus2_x (if Suc 0 \<le> nat then [Suc 0..<nat] @ [nat] else [])) (plus2_x 0) \<lbrace>plus2_rel {..<N} {Suc nat..}\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc nat. threadv s i = 2)\<rbrace>; Suc (Suc nat) \<le> N; threadv s (Suc nat) = 2; plus2_inv {..<N} s; \<forall>i<Suc nat. threadv s i = 2; i < Suc (Suc nat)\<rbrakk> \<Longrightarrow> threadv s i = 2
 2. \<And>nat s0 s. \<lbrakk>\<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc nat}\<rbrace> fold Trace_Monad.parallel (map plus2_x (if Suc 0 \<le> nat then [Suc 0..<nat] @ [nat] else [])) (plus2_x 0) \<lbrace>plus2_rel {..<N} {Suc nat..}\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc nat. threadv s i = 2)\<rbrace>; Suc (Suc nat) \<le> N; plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrakk> \<Longrightarrow> ((\<lambda>s0 s. plus2_inv {..<N} s \<and> threadv s (Suc nat) = 0 \<and> s = s0 \<and> Suc nat \<in> {..<N} \<and> finite {..<N}) and (\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0)) s0 s proof (prove)
goal (1 subgoal):
 1. \<And>nat s0 s. \<lbrakk>\<lbrace>\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<N} {..<Suc nat}\<rbrace> fold Trace_Monad.parallel (map plus2_x (if Suc 0 \<le> nat then [Suc 0..<nat] @ [nat] else [])) (plus2_x 0) \<lbrace>plus2_rel {..<N} {Suc nat..}\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv {..<N} s \<and> (\<forall>i<Suc nat. threadv s i = 2)\<rbrace>; Suc (Suc nat) \<le> N; plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0\<rbrakk> \<Longrightarrow> ((\<lambda>s0 s. plus2_inv {..<N} s \<and> threadv s (Suc nat) = 0 \<and> s = s0 \<and> Suc nat \<in> {..<N} \<and> finite {..<N}) and (\<lambda>s0 s. plus2_inv {..<N} s \<and> (\<forall>i<N. threadv s i = 0) \<and> s = s0)) s0 s proof (prove)
goal:
No subgoals!