theory Finalise_C

lemma tcb_queue_relation2_concat:
  "tcb_queue_relation2 getNext getPrev hp
            (xs @ ys) before after
     = (tcb_queue_relation2 getNext getPrev hp
            xs before (hd (ys @ [after]))
         \<and> tcb_queue_relation2 getNext getPrev hp
              ys (last (before # xs)) after)" apply (induct xs arbitrary: before) apply simp apply (rename_tac x xs before) apply (simp split del: if_split) apply (case_tac "hp x") apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation2 getNext getPrev hp (xs @ ys) before after = (tcb_queue_relation2 getNext getPrev hp xs before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (last (before # xs)) after) proof (prove)
goal (2 subgoals):
 1. \<And>before. tcb_queue_relation2 getNext getPrev hp ([] @ ys) before after = (tcb_queue_relation2 getNext getPrev hp [] before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (last [before]) after)
 2. \<And>x1 xs before. (\<And>before. tcb_queue_relation2 getNext getPrev hp (xs @ ys) before after = (tcb_queue_relation2 getNext getPrev hp xs before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (last (before # xs)) after)) \<Longrightarrow> tcb_queue_relation2 getNext getPrev hp ((x1 # xs) @ ys) before after = (tcb_queue_relation2 getNext getPrev hp (x1 # xs) before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (last (before # x1 # xs)) after) proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs before. (\<And>before. tcb_queue_relation2 getNext getPrev hp (xs @ ys) before after = (tcb_queue_relation2 getNext getPrev hp xs before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (last (before # xs)) after)) \<Longrightarrow> tcb_queue_relation2 getNext getPrev hp ((x1 # xs) @ ys) before after = (tcb_queue_relation2 getNext getPrev hp (x1 # xs) before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (last (before # x1 # xs)) after) proof (prove)
goal (1 subgoal):
 1. \<And>x xs before. (\<And>before. tcb_queue_relation2 getNext getPrev hp (xs @ ys) before after = (tcb_queue_relation2 getNext getPrev hp xs before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (last (before # xs)) after)) \<Longrightarrow> tcb_queue_relation2 getNext getPrev hp ((x # xs) @ ys) before after = (tcb_queue_relation2 getNext getPrev hp (x # xs) before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (last (before # x # xs)) after) proof (prove)
goal (1 subgoal):
 1. \<And>x xs before. (\<And>before. tcb_queue_relation2 getNext getPrev hp (xs @ ys) before after = (tcb_queue_relation2 getNext getPrev hp xs before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then before else last xs) after)) \<Longrightarrow> (\<exists>tcb. hp x = Some tcb \<and> getPrev tcb = before \<and> getNext tcb = hd (xs @ ys @ [after]) \<and> tcb_queue_relation2 getNext getPrev hp xs x (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then x else last xs) after) = ((\<exists>tcb. hp x = Some tcb \<and> getPrev tcb = before \<and> getNext tcb = hd (xs @ [hd (ys @ [after])]) \<and> tcb_queue_relation2 getNext getPrev hp xs x (hd (ys @ [after]))) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then x else last xs) after) proof (prove)
goal (2 subgoals):
 1. \<And>x xs before. \<lbrakk>\<And>before. tcb_queue_relation2 getNext getPrev hp (xs @ ys) before after = (tcb_queue_relation2 getNext getPrev hp xs before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then before else last xs) after); hp x = None\<rbrakk> \<Longrightarrow> (\<exists>tcb. hp x = Some tcb \<and> getPrev tcb = before \<and> getNext tcb = hd (xs @ ys @ [after]) \<and> tcb_queue_relation2 getNext getPrev hp xs x (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then x else last xs) after) = ((\<exists>tcb. hp x = Some tcb \<and> getPrev tcb = before \<and> getNext tcb = hd (xs @ [hd (ys @ [after])]) \<and> tcb_queue_relation2 getNext getPrev hp xs x (hd (ys @ [after]))) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then x else last xs) after)
 2. \<And>x xs before a. \<lbrakk>\<And>before. tcb_queue_relation2 getNext getPrev hp (xs @ ys) before after = (tcb_queue_relation2 getNext getPrev hp xs before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then before else last xs) after); hp x = Some a\<rbrakk> \<Longrightarrow> (\<exists>tcb. hp x = Some tcb \<and> getPrev tcb = before \<and> getNext tcb = hd (xs @ ys @ [after]) \<and> tcb_queue_relation2 getNext getPrev hp xs x (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then x else last xs) after) = ((\<exists>tcb. hp x = Some tcb \<and> getPrev tcb = before \<and> getNext tcb = hd (xs @ [hd (ys @ [after])]) \<and> tcb_queue_relation2 getNext getPrev hp xs x (hd (ys @ [after]))) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then x else last xs) after) proof (prove)
goal (1 subgoal):
 1. \<And>x xs before a. \<lbrakk>\<And>before. tcb_queue_relation2 getNext getPrev hp (xs @ ys) before after = (tcb_queue_relation2 getNext getPrev hp xs before (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then before else last xs) after); hp x = Some a\<rbrakk> \<Longrightarrow> (\<exists>tcb. hp x = Some tcb \<and> getPrev tcb = before \<and> getNext tcb = hd (xs @ ys @ [after]) \<and> tcb_queue_relation2 getNext getPrev hp xs x (hd (ys @ [after])) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then x else last xs) after) = ((\<exists>tcb. hp x = Some tcb \<and> getPrev tcb = before \<and> getNext tcb = hd (xs @ [hd (ys @ [after])]) \<and> tcb_queue_relation2 getNext getPrev hp xs x (hd (ys @ [after]))) \<and> tcb_queue_relation2 getNext getPrev hp ys (if xs = [] then x else last xs) after) proof (prove)
goal:
No subgoals!