theory GraphProof

theorem restr_trace_refine_Split:
  assumes Suc: "\<forall>i. split_pc conc_seq rs1 tr (Suc i) \<longrightarrow> split_pc conc_seq rs1 tr i"
  and init: "\<forall>i. i < k \<longrightarrow> split_pc conc_seq rs1 tr i
        \<longrightarrow> split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') i"
  and induct: "\<forall>i. split_pc conc_seq rs1 tr (i + k)
        \<longrightarrow> (\<forall>j < k. split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') (i + j))
        \<longrightarrow> split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') (i + k)"
  and zero: "k \<noteq> 0" "snd (snd conc_seq) \<noteq> 0" "snd (snd abs_seq) \<noteq> 0"
  and init_case: "\<not> split_pc conc_seq rs1 tr k
    \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2)
        orel tr tr'"
  and induct_case: "\<And>i. induct_var (NextNode (fst conc_seq)) i
    \<Longrightarrow> induct_var (NextNode (fst abs_seq)) i
    \<Longrightarrow> \<not> split_pc conc_seq rs1 tr (i + k)
    \<Longrightarrow> \<forall>j < k. split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') (i + j)
    \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2)
            orel tr tr'"
  shows "restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr'" apply (rule restr_trace_refine_Split_orig[where
            ccall="\<lambda>i. (False, NextNode (fst conc_seq), split_restr conc_seq rs1 i)"
        and acall="\<lambda>i. (True, NextNode (fst abs_seq), split_restr abs_seq rs2 i)"
        and k=k and rel=rel],
         simp_all add: Suc init induct init_case induct_case zero[simplified]
                       double_pc_def[folded pc_def] split_visit_rel') apply (clarsimp, drule(1) restrs_condition_unique) apply (simp add: zero) apply (clarsimp, drule(1) restrs_condition_unique) apply (simp add: zero) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<forall>tr i j k. restrs_condition tr (restrs_list ((fst conc_seq, [fst (snd conc_seq) + i * snd (snd conc_seq)]) # rs1)) k \<longrightarrow> restrs_condition tr (restrs_list ((fst conc_seq, [fst (snd conc_seq) + j * snd (snd conc_seq)]) # rs1)) k \<longrightarrow> i = j
 2. \<forall>tr i j k. restrs_condition tr (restrs_list ((fst abs_seq, [fst (snd abs_seq) + i * snd (snd abs_seq)]) # rs2)) k \<longrightarrow> restrs_condition tr (restrs_list ((fst abs_seq, [fst (snd abs_seq) + j * snd (snd abs_seq)]) # rs2)) k \<longrightarrow> i = j proof (prove)
goal (2 subgoals):
 1. \<And>tr i j k. \<lbrakk>restrs_condition tr (restrs_list ((fst conc_seq, [fst (snd conc_seq) + j * snd (snd conc_seq)]) # rs1)) k; fst (snd conc_seq) + i * snd (snd conc_seq) = fst (snd conc_seq) + j * snd (snd conc_seq)\<rbrakk> \<Longrightarrow> i = j
 2. \<forall>tr i j k. restrs_condition tr (restrs_list ((fst abs_seq, [fst (snd abs_seq) + i * snd (snd abs_seq)]) # rs2)) k \<longrightarrow> restrs_condition tr (restrs_list ((fst abs_seq, [fst (snd abs_seq) + j * snd (snd abs_seq)]) # rs2)) k \<longrightarrow> i = j proof (prove)
goal (1 subgoal):
 1. \<forall>tr i j k. restrs_condition tr (restrs_list ((fst abs_seq, [fst (snd abs_seq) + i * snd (snd abs_seq)]) # rs2)) k \<longrightarrow> restrs_condition tr (restrs_list ((fst abs_seq, [fst (snd abs_seq) + j * snd (snd abs_seq)]) # rs2)) k \<longrightarrow> i = j proof (prove)
goal (1 subgoal):
 1. \<And>tr i j k. \<lbrakk>restrs_condition tr (restrs_list ((fst abs_seq, [fst (snd abs_seq) + j * snd (snd abs_seq)]) # rs2)) k; fst (snd abs_seq) + i * snd (snd abs_seq) = fst (snd abs_seq) + j * snd (snd abs_seq)\<rbrakk> \<Longrightarrow> i = j proof (prove)
goal:
No subgoals!