theory GraphProof

lemma visit_impossible:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> function_graph gf = graph
    \<Longrightarrow> wf_graph_function gf ilen olen
    \<Longrightarrow> 0 \<notin> restrs n
    \<Longrightarrow> (NextNode n, nn) \<notin> rtrancl (reachable_step graph)
    \<Longrightarrow> visit tr nn restrs = None" apply (clarsimp simp: visit_eqs restrs_condition_def) apply (rule_tac x=n in exI) apply (subst arg_cong[where f=card and y="{}"], simp_all) apply clarsimp apply (drule(5) reachable_trace) apply (drule trancl_mono[OF _ Int_lower1]) apply (simp add: trancl_into_rtrancl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf = graph; wf_graph_function gf ilen olen; 0 \<notin> restrs n; (NextNode n, nn) \<notin> (reachable_step graph)\<^sup>*\<rbrakk> \<Longrightarrow> visit tr nn restrs = None proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; 0 \<notin> restrs n; (NextNode n, nn) \<notin> (reachable_step' gf)\<^sup>*; graph = function_graph gf; trace_addr tr i = Some nn\<rbrakk> \<Longrightarrow> \<exists>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<notin> restrs m proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; 0 \<notin> restrs n; (NextNode n, nn) \<notin> (reachable_step' gf)\<^sup>*; graph = function_graph gf; trace_addr tr i = Some nn\<rbrakk> \<Longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode n)} \<notin> restrs n proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; 0 \<notin> restrs n; (NextNode n, nn) \<notin> (reachable_step' gf)\<^sup>*; graph = function_graph gf; trace_addr tr i = Some nn\<rbrakk> \<Longrightarrow> \<forall>x<i. trace_addr tr x \<noteq> Some (NextNode n) proof (prove)
goal (1 subgoal):
 1. \<And>i x. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; 0 \<notin> restrs n; (NextNode n, nn) \<notin> (reachable_step' gf)\<^sup>*; graph = function_graph gf; trace_addr tr i = Some nn; x < i; trace_addr tr x = Some (NextNode n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i x. \<lbrakk>Gamma fn = Some gf; wf_graph_function gf ilen olen; 0 \<notin> restrs n; (NextNode n, nn) \<notin> (reachable_step' gf)\<^sup>*; graph = function_graph gf; trace_addr tr i = Some nn; x < i; trace_addr tr x = Some (NextNode n); (NextNode n, nn) \<in> (reachable_step' gf \<inter> {(xa, y). Some xa \<in> trace_addr tr ` {x..<i}})\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i x. \<lbrakk>Gamma fn = Some gf; wf_graph_function gf ilen olen; 0 \<notin> restrs n; (NextNode n, nn) \<notin> (reachable_step' gf)\<^sup>*; graph = function_graph gf; trace_addr tr i = Some nn; x < i; trace_addr tr x = Some (NextNode n); (NextNode n, nn) \<in> (reachable_step' gf)\<^sup>+\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!