theory Invariants_H

lemma valid_dlist_def3:
  "valid_dlist m = ((\<forall>c c'. m \<turnstile> c \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leftarrow> c') \<and>
                    (\<forall>c c'. m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow>  m \<turnstile> c \<leadsto> c'))" apply (rule iffI) apply (simp add: valid_dlist_def Let_def mdb_next_unfold mdb_prev_def) apply fastforce apply (clarsimp simp add: valid_dlist_def Let_def mdb_next_unfold mdb_prev_def) apply fastforce done

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