theory CSpace_I

lemma no_loops_prev_next_0:
  fixes m :: cte_heap
  assumes src: "m src = Some (CTE src_cap src_node)"
  assumes no_loops: "no_loops m"
  assumes dlist: "valid_dlist m"
  shows "(mdbPrev src_node = mdbNext src_node) =
         (mdbPrev src_node = 0 \<and> mdbNext src_node = 0)" proof - { assume "mdbPrev src_node = mdbNext src_node" moreover assume "mdbNext src_node \<noteq> 0" ultimately obtain cte where
      "m (mdbNext src_node) = Some cte"
      "mdbNext (cteMDBNode cte) = src" using src dlist by (fastforce simp add: valid_dlist_def Let_def) hence "m \<turnstile> src \<leadsto>\<^sup>+ src" using src apply - apply (rule trancl_trans) apply (rule r_into_trancl) apply (simp add: next_unfold') apply (rule r_into_trancl) apply (simp add: next_unfold') done with no_loops have False by (simp add: no_loops_def) } thus ?thesis by auto blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (state)
goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (state)
goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (state)
this:
mdbPrev src_node = mdbNext src_node

goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (state)
this:
mdbPrev src_node = mdbNext src_node

goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (state)
this:
mdbNext src_node \<noteq> 0

goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (chain)
picking this:
mdbPrev src_node = mdbNext src_node
mdbNext src_node \<noteq> 0 proof (prove)
using this:
mdbPrev src_node = mdbNext src_node
mdbNext src_node \<noteq> 0

goal (1 subgoal):
 1. (\<And>cte. \<lbrakk>m (mdbNext src_node) = Some cte; mdbNext (cteMDBNode cte) = src\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
mdbPrev src_node = mdbNext src_node
mdbNext src_node \<noteq> 0
m src = Some (CTE src_cap src_node)
valid_dlist m

goal (1 subgoal):
 1. (\<And>cte. \<lbrakk>m (mdbNext src_node) = Some cte; mdbNext (cteMDBNode cte) = src\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
m (mdbNext src_node) = Some cte
mdbNext (cteMDBNode cte) = src

goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (prove)
using this:
m (mdbNext src_node) = Some cte
mdbNext (cteMDBNode cte) = src

goal (1 subgoal):
 1. m \<turnstile> src \<leadsto>\<^sup>+ src proof (prove)
using this:
m (mdbNext src_node) = Some cte
mdbNext (cteMDBNode cte) = src
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. m \<turnstile> src \<leadsto>\<^sup>+ src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m (mdbNext src_node) = Some cte; mdbNext (cteMDBNode cte) = src; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto>\<^sup>+ src proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m (mdbNext src_node) = Some cte; mdbNext (cteMDBNode cte) = src; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto>\<^sup>+ ?y3
 2. \<lbrakk>m (mdbNext src_node) = Some cte; mdbNext (cteMDBNode cte) = src; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> m \<turnstile> ?y3 \<leadsto>\<^sup>+ src proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m (mdbNext src_node) = Some cte; mdbNext (cteMDBNode cte) = src; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> m \<turnstile> src \<leadsto> ?y3
 2. \<lbrakk>m (mdbNext src_node) = Some cte; mdbNext (cteMDBNode cte) = src; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> m \<turnstile> ?y3 \<leadsto>\<^sup>+ src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m (mdbNext src_node) = Some cte; mdbNext (cteMDBNode cte) = src; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext src_node \<leadsto>\<^sup>+ src proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m (mdbNext src_node) = Some cte; mdbNext (cteMDBNode cte) = src; m src = Some (CTE src_cap src_node)\<rbrakk> \<Longrightarrow> m \<turnstile> mdbNext src_node \<leadsto> src proof (prove)
goal:
No subgoals! proof (state)
this:
m \<turnstile> src \<leadsto>\<^sup>+ src

goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (chain)
picking this:
no_loops m
m \<turnstile> src \<leadsto>\<^sup>+ src proof (prove)
using this:
no_loops m
m \<turnstile> src \<leadsto>\<^sup>+ src

goal (1 subgoal):
 1. False proof (state)
this:
False

goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (state)
this:
\<lbrakk>mdbPrev src_node = mdbNext src_node; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (prove)
using this:
\<lbrakk>mdbPrev src_node = mdbNext src_node; mdbNext src_node \<noteq> 0\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0) proof (state)
this:
(mdbPrev src_node = mdbNext src_node) = (mdbPrev src_node = 0 \<and> mdbNext src_node = 0)

goal:
No subgoals!