theory Invariants_H

lemma valid_dlist_def2:
  "no_0 m \<Longrightarrow> valid_dlist m = (\<forall>c c'. c \<noteq> 0 \<longrightarrow> c' \<noteq> 0 \<longrightarrow>  m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')" apply (rule iffI) apply (simp add: valid_dlist_prevD) apply (clarsimp simp: valid_dlist_def Let_def mdb_next_unfold mdb_prev_def) apply (subgoal_tac "p\<noteq>0") prefer 2 apply clarsimp apply (rule conjI) apply clarsimp apply (erule_tac x="mdbPrev (cteMDBNode cte)" in allE) apply simp apply (erule_tac x=p in allE) apply clarsimp apply clarsimp apply (erule_tac x=p in allE) apply simp apply (erule_tac x="mdbNext (cteMDBNode cte)" in allE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_0 m \<Longrightarrow> valid_dlist m = (\<forall>c c'. c \<noteq> 0 \<longrightarrow> c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>no_0 m; valid_dlist m\<rbrakk> \<Longrightarrow> \<forall>c c'. c \<noteq> 0 \<longrightarrow> c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'
 2. \<lbrakk>no_0 m; \<forall>c c'. c \<noteq> 0 \<longrightarrow> c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'\<rbrakk> \<Longrightarrow> valid_dlist m proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_0 m; \<forall>c c'. c \<noteq> 0 \<longrightarrow> c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'\<rbrakk> \<Longrightarrow> valid_dlist m proof (prove)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)) proof (prove)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p))
 2. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte\<rbrakk> \<Longrightarrow> p \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte\<rbrakk> \<Longrightarrow> p \<noteq> 0
 2. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)) proof (prove)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0\<rbrakk> \<Longrightarrow> (mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> (mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)) proof (prove)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p)
 2. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p) proof (prove)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p) proof (prove)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>no_0 m; m p = Some cte; p \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m (mdbPrev (cteMDBNode cte)) = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> mdbPrev (cteMDBNode cte) = mdbPrev (cteMDBNode z)))\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p) proof (prove)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>no_0 m; m p = Some cte; p \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0; \<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m (mdbPrev (cteMDBNode cte)) = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> mdbPrev (cteMDBNode cte) = mdbPrev (cteMDBNode z))\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p) proof (prove)
goal (2 subgoals):
 1. \<And>p cte. \<lbrakk>no_0 m; m p = Some cte; p \<noteq> 0; mdbPrev (cteMDBNode cte) \<noteq> 0; p \<noteq> 0 \<longrightarrow> (\<exists>z. m (mdbPrev (cteMDBNode cte)) = Some z \<and> p = mdbNext (cteMDBNode z)) = (\<exists>z. m p = Some z \<and> mdbPrev (cteMDBNode cte) = mdbPrev (cteMDBNode z))\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbPrev (cteMDBNode cte)) = Some cte' \<and> mdbNext (cteMDBNode cte') = p
 2. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p) proof (prove)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0\<rbrakk> \<Longrightarrow> mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (\<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p) proof (prove)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>no_0 m; \<forall>c. c \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m c = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))); m p = Some cte; p \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>no_0 m; m p = Some cte; p \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; p \<noteq> 0 \<longrightarrow> (\<forall>c'. c' \<noteq> 0 \<longrightarrow> (\<exists>z. m p = Some z \<and> c' = mdbNext (cteMDBNode z)) = (\<exists>z. m c' = Some z \<and> p = mdbPrev (cteMDBNode z)))\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>no_0 m; m p = Some cte; p \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; \<forall>c'. c' \<noteq> 0 \<longrightarrow> (c' = mdbNext (cteMDBNode cte)) = (\<exists>z. m c' = Some z \<and> p = mdbPrev (cteMDBNode z))\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal (1 subgoal):
 1. \<And>p cte. \<lbrakk>no_0 m; m p = Some cte; p \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0; mdbNext (cteMDBNode cte) \<noteq> 0 \<longrightarrow> (mdbNext (cteMDBNode cte) = mdbNext (cteMDBNode cte)) = (\<exists>z. m (mdbNext (cteMDBNode cte)) = Some z \<and> p = mdbPrev (cteMDBNode z))\<rbrakk> \<Longrightarrow> \<exists>cte'. m (mdbNext (cteMDBNode cte)) = Some cte' \<and> mdbPrev (cteMDBNode cte') = p proof (prove)
goal:
No subgoals!