theory GraphProof

lemma visit_merge_restrs:
  assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn = Some gf"
     and geq: "function_graph gf = graph"
  assumes indep: "opt \<notin> set (opt2 # opts)"
  assumes reach: "(nn, NextNode addr) \<notin> rtrancl (reachable_step graph)"
         and wf: "wf_graph_function gf ilen olen"
  fixes rs
  defines "rs1 \<equiv> restrs_list ((addr, [opt]) # rs)"
      and "rs2 \<equiv> restrs_list ((addr, opt2 # opts) # rs)"
      and "rs3 \<equiv> restrs_list ((addr, opt # opt2 # opts) # rs)"
  shows
  "visit tr nn rs3
    = merge_opt (visit tr nn rs1) (visit tr nn rs2)" proof - let ?card = "\<lambda>i. card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)}" obtain n where vis: "\<forall>i. trace_addr tr i = Some nn \<longrightarrow> ?card i = n" apply (case_tac "\<exists>i. trace_addr tr i = Some nn") apply clarsimp apply (erule_tac x="?card i" in meta_allE) apply (erule meta_mp) apply clarsimp apply (auto dest: not_reachable_visits_same_symm[OF tr _ _ reach[folded geq] wf]) done have indep2: "\<forall>i. restrs_condition tr rs1 i
    \<longrightarrow> \<not> restrs_condition tr rs2 i" using indep apply (clarsimp, clarsimp simp: restrs_condition_def rs1_def rs2_def restrs_list_Cons) apply (drule_tac x=addr in spec)+ apply (clarsimp simp: restrs_list_def) done have disj:
    "\<forall>i. restrs_condition tr rs3 i
        = (restrs_condition tr rs1 i \<or> restrs_condition tr rs2 i)" apply (clarsimp simp: restrs_condition_def rs1_def rs2_def rs3_def restrs_list_Cons) apply blast done have indep3: "\<forall>j i. trace_addr tr i = Some nn \<longrightarrow> restrs_condition tr rs1 i
    \<longrightarrow> trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr rs2 j" using indep apply (clarsimp, clarsimp simp: restrs_condition_def rs1_def rs2_def restrs_list_Cons) apply (drule_tac x=addr in spec)+ apply (clarsimp simp: restrs_list_def vis) done show ?thesis unfolding visit_def by (auto simp: disj dest: indep3[rule_format]; metis) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. visit tr nn rs3 = merge_opt (visit tr nn rs1) (visit tr nn rs2) proof (state)
goal (1 subgoal):
 1. visit tr nn rs3 = merge_opt (visit tr nn rs1) (visit tr nn rs2) proof (state)
goal (1 subgoal):
 1. visit tr nn rs3 = merge_opt (visit tr nn rs1) (visit tr nn rs2) proof (prove)
goal (1 subgoal):
 1. (\<And>n. \<forall>i. trace_addr tr i = Some nn \<longrightarrow> card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)} = n \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>n. \<forall>i. trace_addr tr i = Some nn \<longrightarrow> card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)} = n \<Longrightarrow> thesis; \<exists>i. trace_addr tr i = Some nn\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>n. \<forall>i. trace_addr tr i = Some nn \<longrightarrow> card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)} = n \<Longrightarrow> thesis; \<nexists>i. trace_addr tr i = Some nn\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>\<And>n. \<forall>i. trace_addr tr i = Some nn \<longrightarrow> card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)} = n \<Longrightarrow> thesis; trace_addr tr i = Some nn\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>n. \<forall>i. trace_addr tr i = Some nn \<longrightarrow> card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)} = n \<Longrightarrow> thesis; \<nexists>i. trace_addr tr i = Some nn\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>trace_addr tr i = Some nn; \<forall>ia. trace_addr tr ia = Some nn \<longrightarrow> card {j. j < ia \<and> trace_addr tr j = Some (NextNode addr)} = card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)} \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
 2. \<lbrakk>\<And>n. \<forall>i. trace_addr tr i = Some nn \<longrightarrow> card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)} = n \<Longrightarrow> thesis; \<nexists>i. trace_addr tr i = Some nn\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (2 subgoals):
 1. \<And>i. trace_addr tr i = Some nn \<Longrightarrow> \<forall>ia. trace_addr tr ia = Some nn \<longrightarrow> card {j. j < ia \<and> trace_addr tr j = Some (NextNode addr)} = card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)}
 2. \<lbrakk>\<And>n. \<forall>i. trace_addr tr i = Some nn \<longrightarrow> card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)} = n \<Longrightarrow> thesis; \<nexists>i. trace_addr tr i = Some nn\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal (2 subgoals):
 1. \<And>i ia. \<lbrakk>trace_addr tr i = Some nn; trace_addr tr ia = Some nn\<rbrakk> \<Longrightarrow> card {j. j < ia \<and> trace_addr tr j = Some (NextNode addr)} = card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)}
 2. \<lbrakk>\<And>n. \<forall>i. trace_addr tr i = Some nn \<longrightarrow> card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)} = n \<Longrightarrow> thesis; \<nexists>i. trace_addr tr i = Some nn\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>i. trace_addr tr i = Some nn \<longrightarrow> card {j. j < i \<and> trace_addr tr j = Some (NextNode addr)} = n

goal (1 subgoal):
 1. visit tr nn rs3 = merge_opt (visit tr nn rs1) (visit tr nn rs2) proof (prove)
goal (1 subgoal):
 1. \<forall>i. restrs_condition tr rs1 i \<longrightarrow> \<not> restrs_condition tr rs2 i proof (prove)
using this:
opt \<notin> set (opt2 # opts)

goal (1 subgoal):
 1. \<forall>i. restrs_condition tr rs1 i \<longrightarrow> \<not> restrs_condition tr rs2 i proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>opt \<noteq> opt2; opt \<notin> set opts; \<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> (if m = addr then set [opt] \<inter> restrs_list rs m else restrs_list rs m); \<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> (if m = addr then set (opt2 # opts) \<inter> restrs_list rs m else restrs_list rs m)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>opt \<noteq> opt2; opt \<notin> set opts; card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} \<in> (if addr = addr then set [opt] \<inter> restrs_list rs addr else restrs_list rs addr); card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} \<in> (if addr = addr then set (opt2 # opts) \<inter> restrs_list rs addr else restrs_list rs addr)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>i. restrs_condition tr rs1 i \<longrightarrow> \<not> restrs_condition tr rs2 i

goal (1 subgoal):
 1. visit tr nn rs3 = merge_opt (visit tr nn rs1) (visit tr nn rs2) proof (prove)
goal (1 subgoal):
 1. \<forall>i. restrs_condition tr rs3 i = (restrs_condition tr rs1 i \<or> restrs_condition tr rs2 i) proof (prove)
goal (1 subgoal):
 1. \<And>i. (\<forall>m. (m = addr \<longrightarrow> (card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} = opt \<or> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} = opt2 \<or> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} \<in> set opts) \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} \<in> restrs_list rs addr) \<and> (m \<noteq> addr \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m)) = ((\<forall>m. (m = addr \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} = opt \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} \<in> restrs_list rs addr) \<and> (m \<noteq> addr \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m)) \<or> (\<forall>m. (m = addr \<longrightarrow> (card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} = opt2 \<or> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} \<in> set opts) \<and> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} \<in> restrs_list rs addr) \<and> (m \<noteq> addr \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs_list rs m))) proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>i. restrs_condition tr rs3 i = (restrs_condition tr rs1 i \<or> restrs_condition tr rs2 i)

goal (1 subgoal):
 1. visit tr nn rs3 = merge_opt (visit tr nn rs1) (visit tr nn rs2) proof (prove)
goal (1 subgoal):
 1. \<forall>j i. trace_addr tr i = Some nn \<longrightarrow> restrs_condition tr rs1 i \<longrightarrow> trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr rs2 j proof (prove)
using this:
opt \<notin> set (opt2 # opts)

goal (1 subgoal):
 1. \<forall>j i. trace_addr tr i = Some nn \<longrightarrow> restrs_condition tr rs1 i \<longrightarrow> trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr rs2 j proof (prove)
goal (1 subgoal):
 1. \<And>j i. \<lbrakk>opt \<noteq> opt2; opt \<notin> set opts; trace_addr tr i = Some nn; \<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> (if m = addr then set [opt] \<inter> restrs_list rs m else restrs_list rs m); trace_addr tr j = Some nn; \<forall>m. card {i. i < j \<and> trace_addr tr i = Some (NextNode m)} \<in> (if m = addr then set (opt2 # opts) \<inter> restrs_list rs m else restrs_list rs m)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>j i. \<lbrakk>opt \<noteq> opt2; opt \<notin> set opts; trace_addr tr i = Some nn; trace_addr tr j = Some nn; card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode addr)} \<in> (if addr = addr then set [opt] \<inter> restrs_list rs addr else restrs_list rs addr); card {i. i < j \<and> trace_addr tr i = Some (NextNode addr)} \<in> (if addr = addr then set (opt2 # opts) \<inter> restrs_list rs addr else restrs_list rs addr)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>j i. trace_addr tr i = Some nn \<longrightarrow> restrs_condition tr rs1 i \<longrightarrow> trace_addr tr j = Some nn \<longrightarrow> \<not> restrs_condition tr rs2 j

goal (1 subgoal):
 1. visit tr nn rs3 = merge_opt (visit tr nn rs1) (visit tr nn rs2) proof (prove)
goal (1 subgoal):
 1. visit tr nn rs3 = merge_opt (visit tr nn rs1) (visit tr nn rs2) proof (prove)
goal (1 subgoal):
 1. (if \<exists>i. restrs_condition tr rs3 i \<and> trace_addr tr i = Some nn then Some (fst (snd (hd (the (tr (LEAST i. restrs_condition tr rs3 i \<and> trace_addr tr i = Some nn)))))) else None) = merge_opt (if \<exists>i. restrs_condition tr rs1 i \<and> trace_addr tr i = Some nn then Some (fst (snd (hd (the (tr (LEAST i. restrs_condition tr rs1 i \<and> trace_addr tr i = Some nn)))))) else None) (if \<exists>i. restrs_condition tr rs2 i \<and> trace_addr tr i = Some nn then Some (fst (snd (hd (the (tr (LEAST i. restrs_condition tr rs2 i \<and> trace_addr tr i = Some nn)))))) else None) proof (state)
this:
visit tr nn rs3 = merge_opt (visit tr nn rs1) (visit tr nn rs2)

goal:
No subgoals!