theory GraphProof

theorem restr_trace_refine_Split':
  "let cpc = split_pc conc_seq rs1 tr;
        rel = split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr')
    in (\<forall>i. cpc (Suc i) --> cpc i)
    --> (\<forall>i. i < k --> cpc i --> rel i)
    --> (\<forall>i. cpc (i + k) --> (\<forall>j < k. rel (i + j)) --> rel (i + k))
    --> k \<noteq> 0 --> snd (snd conc_seq) \<noteq> 0 --> snd (snd abs_seq) \<noteq> 0
    --> (~ cpc k --> restr_trace_refine prec Gamma1 f1 Gamma2 f2
        (restrs_list rs1) (restrs_list rs2) orel tr tr')
    --> (\<forall>i. ~ cpc (i + k) --> (\<forall>j < k. rel (i + j))
        --> restr_trace_refine prec Gamma1 f1 Gamma2 f2
            (restrs_list rs1) (restrs_list rs2) orel tr tr')
    --> restr_trace_refine prec Gamma1 f1 Gamma2 f2
        (restrs_list rs1) (restrs_list rs2) orel tr tr'" apply (clarsimp simp only: Let_def) apply (erule notE, rule restr_trace_refine_Split[where conc_seq=conc_seq and abs_seq=abs_seq
      and k=k and rel=rel], simp_all) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. let cpc = \<lambda>i. pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + i * snd (snd conc_seq)]) # rs1)) tr; rel = split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') in (\<forall>i. cpc (Suc i) \<longrightarrow> cpc i) \<longrightarrow> (\<forall>i<k. cpc i \<longrightarrow> rel i) \<longrightarrow> (\<forall>i. cpc (i + k) \<longrightarrow> (\<forall>j<k. rel (i + j)) \<longrightarrow> rel (i + k)) \<longrightarrow> k \<noteq> 0 \<longrightarrow> snd (snd conc_seq) \<noteq> 0 \<longrightarrow> snd (snd abs_seq) \<noteq> 0 \<longrightarrow> (\<not> cpc k \<longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr') \<longrightarrow> (\<forall>i. \<not> cpc (i + k) \<longrightarrow> (\<forall>j<k. rel (i + j)) \<longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr') \<longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + Suc i * snd (snd conc_seq)]) # rs1)) tr \<longrightarrow> pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + i * snd (snd conc_seq)]) # rs1)) tr; \<forall>i<k. pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + i * snd (snd conc_seq)]) # rs1)) tr \<longrightarrow> split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') i; \<forall>i. pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + (i + k) * snd (snd conc_seq)]) # rs1)) tr \<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); 0 < k; 0 < snd (snd conc_seq); 0 < snd (snd abs_seq); \<forall>i. \<not> pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + (i + k) * snd (snd conc_seq)]) # rs1)) tr \<longrightarrow> (\<forall>j<k. split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') (i + j)) \<longrightarrow> False; \<not> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr'; pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + k * snd (snd conc_seq)]) # rs1)) tr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>\<forall>i. pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + (snd (snd conc_seq) + i * snd (snd conc_seq))]) # rs1)) tr \<longrightarrow> pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + i * snd (snd conc_seq)]) # rs1)) tr; \<forall>i<k. pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + i * snd (snd conc_seq)]) # rs1)) tr \<longrightarrow> split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') i; \<forall>i. pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + (i + k) * snd (snd conc_seq)]) # rs1)) tr \<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); 0 < k; 0 < snd (snd conc_seq); 0 < snd (snd abs_seq); \<forall>i. \<not> pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + (i + k) * snd (snd conc_seq)]) # rs1)) tr \<longrightarrow> (\<exists>j<k. \<not> split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') (i + j)); pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + k * snd (snd conc_seq)]) # rs1)) tr; induct_var (NextNode (fst conc_seq)) i; induct_var (NextNode (fst abs_seq)) i; \<not> pc' (fst conc_seq) (restrs_list ((fst conc_seq, [fst (snd conc_seq) + (i + k) * snd (snd conc_seq)]) # rs1)) tr; \<forall>j<k. split_visit_rel' rel conc_seq abs_seq (rs1, rs2) (tr, tr') (i + j)\<rbrakk> \<Longrightarrow> restr_trace_refine prec Gamma1 f1 Gamma2 f2 (restrs_list rs1) (restrs_list rs2) orel tr tr' proof (prove)
goal:
No subgoals!