theory GraphProof

lemma restrs_visit_abstract:
  assumes dist: "distinct (map fst rs)"
  shows "restrs_list (restrs_visit rs nn gf)
    = (\<lambda>j. if (nn, NextNode j) \<in> rtrancl (reachable_step' gf)
        then {k. \<exists>l. l \<in> restrs_list rs j \<and> k \<le> l}
        else restrs_list rs j)" proof - have P: "\<And>j. {x \<in> set (restrs_visit rs nn gf). fst x = j}
        = (if (nn, NextNode j) \<in> rtrancl (reachable_step' gf)
            then (\<lambda>(k, xsf). (k, fill_in_below xsf))
                ` {x \<in> set rs. fst x = j}
            else {x \<in> set rs. fst x = j})" by (force simp: restrs_visit_def elim: image_eqI[rotated]) show ?thesis apply (rule ext, clarsimp simp: restrs_list_Int2 split_def P) apply (cut_tac dist[THEN set_map_of_compr]) apply (case_tac "\<exists>b. (j, b) \<in> set rs") apply (auto simp: set_fill_in_below) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. restrs_list (restrs_visit rs nn gf) = (\<lambda>j. if (nn, NextNode j) \<in> (reachable_step' gf)\<^sup>* then {k. \<exists>l. l \<in> restrs_list rs j \<and> k \<le> l} else restrs_list rs j) proof (state)
goal (1 subgoal):
 1. restrs_list (restrs_visit rs nn gf) = (\<lambda>j. if (nn, NextNode j) \<in> (reachable_step' gf)\<^sup>* then {k. \<exists>l. l \<in> restrs_list rs j \<and> k \<le> l} else restrs_list rs j) proof (prove)
goal (1 subgoal):
 1. \<And>j. {x \<in> set (restrs_visit rs nn gf). fst x = j} = (if (nn, NextNode j) \<in> (reachable_step' gf)\<^sup>* then (\<lambda>(k, xsf). (k, fill_in_below xsf)) ` {x \<in> set rs. fst x = j} else {x \<in> set rs. fst x = j}) proof (state)
this:
{x \<in> set (restrs_visit rs nn gf). fst x = ?j} = (if (nn, NextNode ?j) \<in> (reachable_step' gf)\<^sup>* then (\<lambda>(k, xsf). (k, fill_in_below xsf)) ` {x \<in> set rs. fst x = ?j} else {x \<in> set rs. fst x = ?j})

goal (1 subgoal):
 1. restrs_list (restrs_visit rs nn gf) = (\<lambda>j. if (nn, NextNode j) \<in> (reachable_step' gf)\<^sup>* then {k. \<exists>l. l \<in> restrs_list rs j \<and> k \<le> l} else restrs_list rs j) proof (prove)
goal (1 subgoal):
 1. restrs_list (restrs_visit rs nn gf) = (\<lambda>j. if (nn, NextNode j) \<in> (reachable_step' gf)\<^sup>* then {k. \<exists>l. l \<in> restrs_list rs j \<and> k \<le> l} else restrs_list rs j) proof (prove)
goal (1 subgoal):
 1. \<And>j. (nn, NextNode j) \<in> (reachable_step' gf)\<^sup>* \<Longrightarrow> (\<Inter>x\<in>{x \<in> set rs. fst x = j}. set (fill_in_below (snd x))) = {k. \<exists>l. (\<forall>b. (j, b) \<in> set rs \<longrightarrow> l \<in> set b) \<and> k \<le> l} proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>(nn, NextNode j) \<in> (reachable_step' gf)\<^sup>*; set rs = {(k, v). map_of rs k = Some v}\<rbrakk> \<Longrightarrow> (\<Inter>x\<in>{x \<in> set rs. fst x = j}. set (fill_in_below (snd x))) = {k. \<exists>l. (\<forall>b. (j, b) \<in> set rs \<longrightarrow> l \<in> set b) \<and> k \<le> l} proof (prove)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>(nn, NextNode j) \<in> (reachable_step' gf)\<^sup>*; set rs = {(k, v). map_of rs k = Some v}; \<exists>b. (j, b) \<in> set rs\<rbrakk> \<Longrightarrow> (\<Inter>x\<in>{x \<in> set rs. fst x = j}. set (fill_in_below (snd x))) = {k. \<exists>l. (\<forall>b. (j, b) \<in> set rs \<longrightarrow> l \<in> set b) \<and> k \<le> l}
 2. \<And>j. \<lbrakk>(nn, NextNode j) \<in> (reachable_step' gf)\<^sup>*; set rs = {(k, v). map_of rs k = Some v}; \<nexists>b. (j, b) \<in> set rs\<rbrakk> \<Longrightarrow> (\<Inter>x\<in>{x \<in> set rs. fst x = j}. set (fill_in_below (snd x))) = {k. \<exists>l. (\<forall>b. (j, b) \<in> set rs \<longrightarrow> l \<in> set b) \<and> k \<le> l} proof (prove)
goal:
No subgoals! proof (state)
this:
restrs_list (restrs_visit rs nn gf) = (\<lambda>j. if (nn, NextNode j) \<in> (reachable_step' gf)\<^sup>* then {k. \<exists>l. l \<in> restrs_list rs j \<and> k \<le> l} else restrs_list rs j)

goal:
No subgoals!