theory GraphProof

lemma pred_restrs_list:
  "pred_restrs nn (restrs_list xs)
    = restrs_list (map (\<lambda>(i, ns). (i, if nn = NextNode i
        then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) xs)" apply (clarsimp simp: pred_restrs_def split: next_node.split) apply (rule sym) apply (induct xs; simp, rule ext) apply (simp add: restrs_list_def) apply (clarsimp simp: restrs_list_Cons split del: if_split cong: if_cong) apply (auto intro: image_eqI[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pred_restrs nn (restrs_list xs) = restrs_list (map (\<lambda>(i, ns). (i, if nn = NextNode i then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) xs) proof (prove)
goal (1 subgoal):
 1. \<And>x1. nn = NextNode x1 \<Longrightarrow> (restrs_list xs)(x1 := {x. Suc x \<in> restrs_list xs x1}) = restrs_list (map (\<lambda>(i, ns). (i, if x1 = i then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) xs) proof (prove)
goal (1 subgoal):
 1. \<And>x1. nn = NextNode x1 \<Longrightarrow> restrs_list (map (\<lambda>(i, ns). (i, if x1 = i then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) xs) = (restrs_list xs)(x1 := {x. Suc x \<in> restrs_list xs x1}) proof (prove)
goal (2 subgoals):
 1. \<And>x1 x. nn = NextNode x1 \<Longrightarrow> restrs_list [] x = ((restrs_list [])(x1 := {x. Suc x \<in> restrs_list [] x1})) x
 2. \<And>x1 xs x1a x. \<lbrakk>restrs_list (map (\<lambda>(i, ns). (i, if x1a = i then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) xs) = (restrs_list xs)(x1a := {x. Suc x \<in> restrs_list xs x1a}); nn = NextNode x1a\<rbrakk> \<Longrightarrow> restrs_list ((case x1 of (i, ns) \<Rightarrow> (i, if x1a = i then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) # map (\<lambda>(i, ns). (i, if x1a = i then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) xs) x = ((restrs_list (x1 # xs))(x1a := {x. Suc x \<in> restrs_list (x1 # xs) x1a})) x proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs x1a x. \<lbrakk>restrs_list (map (\<lambda>(i, ns). (i, if x1a = i then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) xs) = (restrs_list xs)(x1a := {x. Suc x \<in> restrs_list xs x1a}); nn = NextNode x1a\<rbrakk> \<Longrightarrow> restrs_list ((case x1 of (i, ns) \<Rightarrow> (i, if x1a = i then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) # map (\<lambda>(i, ns). (i, if x1a = i then map (\<lambda>x. x - 1) (filter ((\<noteq>) 0) ns) else ns)) xs) x = ((restrs_list (x1 # xs))(x1a := {x. Suc x \<in> restrs_list (x1 # xs) x1a})) x proof (prove)
goal (1 subgoal):
 1. \<And>a b xs x1a x. \<lbrakk>restrs_list (map (\<lambda>(i, ns). (i, if x1a = i then map (\<lambda>x. x - Suc 0) (filter ((<) 0) ns) else ns)) xs) = (restrs_list xs)(x1a := {x. Suc x \<in> restrs_list xs x1a}); nn = NextNode x1a\<rbrakk> \<Longrightarrow> (if x = a then set (if x1a = a then map (\<lambda>x. x - Suc 0) (filter ((<) 0) b) else b) \<inter> (if a = x1a then {x. Suc x \<in> restrs_list xs x1a} else restrs_list xs a) else if x = x1a then {x. Suc x \<in> restrs_list xs x1a} else restrs_list xs x) = (if x = x1a then {x. Suc x \<in> (if x1a = a then set b \<inter> restrs_list xs a else restrs_list xs x1a)} else if x = a then set b \<inter> restrs_list xs a else restrs_list xs x) proof (prove)
goal:
No subgoals!