theory GraphProof

theorem visit_explode_restr:
  assumes gf1: "tr \<in> exec_trace Gamma fn"
    "Gamma fn = Some gf"
    "function_graph gf = graph"
  and gf2: "(nn, NextNode addr) \<notin> (reachable_step graph)\<^sup>*"
    "wf_graph_function gf ilen olen"
  and rs: "restrs_list rs addr = set xs"
    "filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs = rs'"
  and xs: "distinct xs"
  shows "visit tr nn (restrs_list rs) =
        fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None" proof - from rs have Q1: "restrs_list rs addr = restrs_list ((addr, rev xs) # rs') addr" apply (clarsimp simp: restrs_list_def fun_eq_iff) apply (rule fold_invariant[where g="\<lambda>x. x", symmetric], auto) done { fix addr' from rs(2) have "addr \<noteq> addr'
        \<Longrightarrow> restrs_list rs addr' = restrs_list ((addr, rev xs) # rs') addr'" apply clarsimp apply hypsubst_thin apply (induct rs, simp_all add: restrs_list_Cons) apply (clarsimp simp: restrs_list_Cons) done } hence Q: "restrs_list rs = restrs_list ((addr, rev xs) # rs')" using Q1 apply (simp add: fun_eq_iff) apply metis done show "?thesis" using xs unfolding Q apply (induct xs rule: rev_induct) apply (simp add: restrs_list_Cons visit_def restrs_condition_def) apply metis apply (case_tac xs rule: rev_cases) apply (simp add: merge_opt_def) apply (clarsimp simp: visit_merge_restrs[OF gf1 _ gf2]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (state)
goal (1 subgoal):
 1. visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (chain)
picking this:
restrs_list rs addr = set xs
filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs = rs' proof (prove)
using this:
restrs_list rs addr = set xs
filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs = rs'

goal (1 subgoal):
 1. restrs_list rs addr = restrs_list ((addr, rev xs) # rs') addr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fold (\<lambda>(n, xs) S. if addr = n then set xs \<inter> S else S) rs UNIV = set xs; rs' = filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs\<rbrakk> \<Longrightarrow> set xs = fold (\<lambda>(n, xs) S. if addr = n then set xs \<inter> S else S) (filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs) (set xs) proof (prove)
goal:
No subgoals! proof (state)
this:
restrs_list rs addr = restrs_list ((addr, rev xs) # rs') addr

goal (1 subgoal):
 1. visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (state)
this:
restrs_list rs addr = restrs_list ((addr, rev xs) # rs') addr

goal (1 subgoal):
 1. visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (state)
goal (1 subgoal):
 1. visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (chain)
picking this:
filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs = rs' proof (prove)
using this:
filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs = rs'

goal (1 subgoal):
 1. addr \<noteq> addr' \<Longrightarrow> restrs_list rs addr' = restrs_list ((addr, rev xs) # rs') addr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>addr \<noteq> addr'; rs' = filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs\<rbrakk> \<Longrightarrow> restrs_list rs addr' = restrs_list ((addr, rev xs) # filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs) addr' proof (prove)
goal (1 subgoal):
 1. addr \<noteq> addr' \<Longrightarrow> restrs_list rs addr' = restrs_list ((addr, rev xs) # filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs) addr' proof (prove)
goal (1 subgoal):
 1. \<And>x1 rs. \<lbrakk>restrs_list rs addr' = restrs_list (filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs) addr'; addr \<noteq> addr'\<rbrakk> \<Longrightarrow> ((case x1 of (addr', xs) \<Rightarrow> addr' \<noteq> addr) \<longrightarrow> restrs_list (x1 # rs) addr' = restrs_list (x1 # filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs) addr') \<and> (\<not> (case x1 of (addr', xs) \<Rightarrow> addr' \<noteq> addr) \<longrightarrow> restrs_list (x1 # rs) addr' = restrs_list (filter (\<lambda>(addr', xs). addr' \<noteq> addr) rs) addr') proof (prove)
goal:
No subgoals! proof (state)
this:
addr \<noteq> addr' \<Longrightarrow> restrs_list rs addr' = restrs_list ((addr, rev xs) # rs') addr'

goal (1 subgoal):
 1. visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (state)
this:
addr \<noteq> ?addr'2 \<Longrightarrow> restrs_list rs ?addr'2 = restrs_list ((addr, rev xs) # rs') ?addr'2

goal (1 subgoal):
 1. visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (prove)
using this:
addr \<noteq> ?addr'2 \<Longrightarrow> restrs_list rs ?addr'2 = restrs_list ((addr, rev xs) # rs') ?addr'2

goal (1 subgoal):
 1. restrs_list rs = restrs_list ((addr, rev xs) # rs') proof (prove)
using this:
addr \<noteq> ?addr'2 \<Longrightarrow> restrs_list rs ?addr'2 = restrs_list ((addr, rev xs) # rs') ?addr'2
restrs_list rs addr = restrs_list ((addr, rev xs) # rs') addr

goal (1 subgoal):
 1. restrs_list rs = restrs_list ((addr, rev xs) # rs') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>addr'. addr \<noteq> addr' \<Longrightarrow> restrs_list rs addr' = restrs_list ((addr, rev xs) # rs') addr'; restrs_list rs addr = restrs_list ((addr, rev xs) # rs') addr\<rbrakk> \<Longrightarrow> \<forall>x. restrs_list rs x = restrs_list ((addr, rev xs) # rs') x proof (prove)
goal:
No subgoals! proof (state)
this:
restrs_list rs = restrs_list ((addr, rev xs) # rs')

goal (1 subgoal):
 1. visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (prove)
goal (1 subgoal):
 1. visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (prove)
using this:
distinct xs

goal (1 subgoal):
 1. visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (prove)
using this:
distinct xs

goal (1 subgoal):
 1. visit tr nn (restrs_list ((addr, rev xs) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None proof (prove)
goal (2 subgoals):
 1. distinct [] \<Longrightarrow> visit tr nn (restrs_list ((addr, rev []) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) [] None
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> visit tr nn (restrs_list ((addr, rev xs) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> visit tr nn (restrs_list ((addr, rev (xs @ [x])) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) (xs @ [x]) None proof (prove)
goal (2 subgoals):
 1. \<forall>i. (\<exists>m. m \<noteq> addr \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<notin> restrs_list rs' m) \<or> trace_addr tr i \<noteq> Some nn
 2. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> visit tr nn (restrs_list ((addr, rev xs) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> visit tr nn (restrs_list ((addr, rev (xs @ [x])) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) (xs @ [x]) None proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> visit tr nn (restrs_list ((addr, rev xs) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None; distinct (xs @ [x])\<rbrakk> \<Longrightarrow> visit tr nn (restrs_list ((addr, rev (xs @ [x])) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) (xs @ [x]) None proof (prove)
goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>distinct xs \<Longrightarrow> visit tr nn (restrs_list ((addr, rev xs) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None; distinct (xs @ [x]); xs = []\<rbrakk> \<Longrightarrow> visit tr nn (restrs_list ((addr, rev (xs @ [x])) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) (xs @ [x]) None
 2. \<And>x xs ys y. \<lbrakk>distinct xs \<Longrightarrow> visit tr nn (restrs_list ((addr, rev xs) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None; distinct (xs @ [x]); xs = ys @ [y]\<rbrakk> \<Longrightarrow> visit tr nn (restrs_list ((addr, rev (xs @ [x])) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) (xs @ [x]) None proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys y. \<lbrakk>distinct xs \<Longrightarrow> visit tr nn (restrs_list ((addr, rev xs) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None; distinct (xs @ [x]); xs = ys @ [y]\<rbrakk> \<Longrightarrow> visit tr nn (restrs_list ((addr, rev (xs @ [x])) # rs')) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) (xs @ [x]) None proof (prove)
goal:
No subgoals! proof (state)
this:
visit tr nn (restrs_list rs) = fold (\<lambda>x. merge_opt (visit tr nn (restrs_list ((addr, [x]) # rs')))) xs None

goal:
No subgoals!