theory GraphProof

lemma split_visit_rel':
  "split_visit_rel rel (\<lambda>i. (False, NextNode (fst cseq), split_restr cseq rs1 i))
    (\<lambda>i. (True, NextNode (fst aseq), split_restr aseq rs2 i)) j trs
    = split_visit_rel' rel cseq aseq (rs1, rs2) trs j" apply (simp add: split_visit_rel_def split_visit_rel'_def
                   double_pc_def[folded pc_def] split_def double_visit_def) apply (auto elim!: rsubst[where P="rel j", OF _ ext]) apply (auto simp: tuple_switch_def switch_val_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. split_visit_rel rel (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1))) (\<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) j trs = split_visit_rel' rel cseq aseq (rs1, rs2) trs j proof (prove)
goal (1 subgoal):
 1. (pc' (fst cseq) (restrs_list ((fst cseq, [fst (snd cseq) + j * snd (snd cseq)]) # rs1)) (fst trs) \<and> pc' (fst aseq) (restrs_list ((fst aseq, [fst (snd aseq) + j * snd (snd aseq)]) # rs2)) (snd trs) \<and> rel j (\<lambda>p. the (visit (if fst (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) (fst p) (tuple_switch (0, j) (snd p))) then snd trs else fst trs) (fst (snd (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) (fst p) (tuple_switch (0, j) (snd p))))) (snd (snd (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) (fst p) (tuple_switch (0, j) (snd p)))))))) = (pc' (fst cseq) (restrs_list ((fst cseq, [fst (snd cseq) + j * snd (snd cseq)]) # rs1)) (fst trs) \<and> pc' (fst aseq) (restrs_list ((fst aseq, [fst (snd aseq) + j * snd (snd aseq)]) # rs2)) (snd trs) \<and> rel j (\<lambda>p. the (visit (tuple_switch trs (fst p)) (NextNode (fst (tuple_switch (cseq, aseq) (fst p)))) (restrs_list ((fst (tuple_switch (cseq, aseq) (fst p)), [fst (snd (tuple_switch (cseq, aseq) (fst p))) + tuple_switch (0, j) (snd p) * snd (snd (tuple_switch (cseq, aseq) (fst p)))]) # tuple_switch (rs1, rs2) (fst p)))))) proof (prove)
goal (4 subgoals):
 1. \<And>a b. \<lbrakk>pc' (fst cseq) (restrs_list ((fst cseq, [fst (snd cseq) + j * snd (snd cseq)]) # rs1)) (fst trs); pc' (fst aseq) (restrs_list ((fst aseq, [fst (snd aseq) + j * snd (snd aseq)]) # rs2)) (snd trs); fst (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b))\<rbrakk> \<Longrightarrow> the (visit (snd trs) (fst (snd (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b)))) (snd (snd (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b))))) = the (visit (tuple_switch trs a) (NextNode (fst (tuple_switch (cseq, aseq) a))) (restrs_list ((fst (tuple_switch (cseq, aseq) a), [fst (snd (tuple_switch (cseq, aseq) a)) + tuple_switch (0, j) b * snd (snd (tuple_switch (cseq, aseq) a))]) # tuple_switch (rs1, rs2) a)))
 2. \<And>a b. \<lbrakk>pc' (fst cseq) (restrs_list ((fst cseq, [fst (snd cseq) + j * snd (snd cseq)]) # rs1)) (fst trs); pc' (fst aseq) (restrs_list ((fst aseq, [fst (snd aseq) + j * snd (snd aseq)]) # rs2)) (snd trs); \<not> fst (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b))\<rbrakk> \<Longrightarrow> the (visit (fst trs) (fst (snd (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b)))) (snd (snd (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b))))) = the (visit (tuple_switch trs a) (NextNode (fst (tuple_switch (cseq, aseq) a))) (restrs_list ((fst (tuple_switch (cseq, aseq) a), [fst (snd (tuple_switch (cseq, aseq) a)) + tuple_switch (0, j) b * snd (snd (tuple_switch (cseq, aseq) a))]) # tuple_switch (rs1, rs2) a)))
 3. \<And>a b. \<lbrakk>pc' (fst cseq) (restrs_list ((fst cseq, [fst (snd cseq) + j * snd (snd cseq)]) # rs1)) (fst trs); pc' (fst aseq) (restrs_list ((fst aseq, [fst (snd aseq) + j * snd (snd aseq)]) # rs2)) (snd trs); fst (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b))\<rbrakk> \<Longrightarrow> the (visit (tuple_switch trs a) (NextNode (fst (tuple_switch (cseq, aseq) a))) (restrs_list ((fst (tuple_switch (cseq, aseq) a), [fst (snd (tuple_switch (cseq, aseq) a)) + tuple_switch (0, j) b * snd (snd (tuple_switch (cseq, aseq) a))]) # tuple_switch (rs1, rs2) a))) = the (visit (snd trs) (fst (snd (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b)))) (snd (snd (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b)))))
 4. \<And>a b. \<lbrakk>pc' (fst cseq) (restrs_list ((fst cseq, [fst (snd cseq) + j * snd (snd cseq)]) # rs1)) (fst trs); pc' (fst aseq) (restrs_list ((fst aseq, [fst (snd aseq) + j * snd (snd aseq)]) # rs2)) (snd trs); \<not> fst (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b))\<rbrakk> \<Longrightarrow> the (visit (tuple_switch trs a) (NextNode (fst (tuple_switch (cseq, aseq) a))) (restrs_list ((fst (tuple_switch (cseq, aseq) a), [fst (snd (tuple_switch (cseq, aseq) a)) + tuple_switch (0, j) b * snd (snd (tuple_switch (cseq, aseq) a))]) # tuple_switch (rs1, rs2) a))) = the (visit (fst trs) (fst (snd (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b)))) (snd (snd (tuple_switch (\<lambda>i. (False, NextNode (fst cseq), restrs_list ((fst cseq, [fst (snd cseq) + i * snd (snd cseq)]) # rs1)), \<lambda>i. (True, NextNode (fst aseq), restrs_list ((fst aseq, [fst (snd aseq) + i * snd (snd aseq)]) # rs2))) a (tuple_switch (0, j) b))))) proof (prove)
goal:
No subgoals!