Theory CFG_wf

header {* \isaheader{CFG well-formedness} *}

theory CFG_wf imports CFG begin

locale CFG_wf = CFG sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main
  for sourcenode :: "'edge => 'node" and targetnode :: "'edge => 'node"
  and kind :: "'edge => ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge => bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node => 'pname"
  and get_return_edges :: "'edge => 'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname" +
  fixes Def::"'node => 'var set"
  fixes Use::"'node => 'var set"
  fixes ParamDefs::"'node => 'var list"
  fixes ParamUses::"'node => 'var set list"
  assumes Entry_empty:"Def (_Entry_) = {} ∧ Use (_Entry_) = {}"
  and ParamUses_call_source_length:
    "[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘p⇙fs; (p,ins,outs) ∈ set procs|]
    ==> length(ParamUses (sourcenode a)) = length ins"
  and distinct_ParamDefs:"valid_edge a ==> distinct (ParamDefs (targetnode a))"
  and ParamDefs_return_target_length:
    "[|valid_edge a; kind a = Q'\<hookleftarrow>⇘p⇙f'; (p,ins,outs) ∈ set procs|]
    ==> length(ParamDefs (targetnode a)) = length outs"
  and ParamDefs_in_Def:
    "[|valid_node n; V ∈ set (ParamDefs n)|] ==> V ∈ Def n"
  and ins_in_Def:
    "[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘p⇙fs; (p,ins,outs) ∈ set procs; V ∈ set ins|]
    ==> V ∈ Def (targetnode a)"
  and call_source_Def_empty:
    "[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘p⇙fs|] ==> Def (sourcenode a) = {}"
  and ParamUses_in_Use:
    "[|valid_node n; V ∈ Union (set (ParamUses n))|] ==> V ∈ Use n"
  and outs_in_Use:
    "[|valid_edge a; kind a = Q\<hookleftarrow>⇘p⇙f; (p,ins,outs) ∈ set procs; V ∈ set outs|] 
    ==> V ∈ Use (sourcenode a)"
  and CFG_intra_edge_no_Def_equal:
    "[|valid_edge a; V ∉ Def (sourcenode a); intra_kind (kind a); pred (kind a) s|]
    ==> state_val (transfer (kind a) s) V = state_val s V"
  and CFG_intra_edge_transfer_uses_only_Use:
    "[|valid_edge a; ∀V ∈ Use (sourcenode a). state_val s V = state_val s' V;
      intra_kind (kind a); pred (kind a) s; pred (kind a) s'|]
    ==> ∀V ∈ Def (sourcenode a). state_val (transfer (kind a) s) V =
                                state_val (transfer (kind a) s') V"
  and CFG_edge_Uses_pred_equal:
    "[|valid_edge a; pred (kind a) s; snd (hd s) = snd (hd s');
      ∀V ∈ Use (sourcenode a). state_val s V = state_val s' V; length s = length s'|]
    ==> pred (kind a) s'"
  and CFG_call_edge_length:
    "[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘p⇙fs; (p,ins,outs) ∈ set procs|]
    ==> length fs = length ins"
  and CFG_call_determ:
    "[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘p⇙fs; valid_edge a'; kind a' = Q':r'\<hookrightarrow>⇘p'⇙fs';
      sourcenode a = sourcenode a'; pred (kind a) s; pred (kind a') s|]
    ==> a = a'"
  and CFG_call_edge_params:
    "[|valid_edge a; kind a = Q:r\<hookrightarrow>⇘p⇙fs; i < length ins; 
      (p,ins,outs) ∈ set procs; pred (kind a) s; pred (kind a) s';
      ∀V ∈ (ParamUses (sourcenode a))!i. state_val s V = state_val s' V|]
    ==> (params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i"  
  and CFG_return_edge_fun:
    "[|valid_edge a; kind a = Q'\<hookleftarrow>⇘p⇙f'; (p,ins,outs) ∈ set procs|]
     ==> f' vmap vmap' = vmap'(ParamDefs (targetnode a) [:=] map vmap outs)"
  and deterministic:"[|valid_edge a; valid_edge a'; sourcenode a = sourcenode a';
    targetnode a ≠ targetnode a'; intra_kind (kind a); intra_kind (kind a')|] 
    ==> ∃Q Q'. kind a = (Q)⇣\<surd> ∧ kind a' = (Q')⇣\<surd> ∧ 
             (∀s. (Q s --> ¬ Q' s) ∧ (Q' s --> ¬ Q s))"

begin


lemma CFG_equal_Use_equal_call:
  assumes "valid_edge a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs" and "valid_edge a'"
  and "kind a' = Q':r'\<hookrightarrow>⇘p'⇙fs'" and "sourcenode a = sourcenode a'"
  and "pred (kind a) s" and "pred (kind a') s'" 
  and "snd (hd s) = snd (hd s')" and "length s = length s'"
  and "∀V ∈ Use (sourcenode a). state_val s V = state_val s' V"
  shows "a = a'"
proof -
  from `valid_edge a` `pred (kind a) s` `snd (hd s) = snd (hd s')`
    `∀V ∈ Use (sourcenode a). state_val s V = state_val s' V` `length s = length s'`
  have "pred (kind a) s'" by(rule CFG_edge_Uses_pred_equal)
  with `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `valid_edge a'` `kind a' = Q':r'\<hookrightarrow>⇘p'⇙fs'`
    `sourcenode a = sourcenode a'` `pred (kind a') s'`
  show ?thesis by -(rule CFG_call_determ)
qed


lemma CFG_call_edge_param_in:
  assumes "valid_edge a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs" and "i < length ins"
  and "(p,ins,outs) ∈ set procs" and "pred (kind a) s" and "pred (kind a) s'"
  and "∀V ∈ (ParamUses (sourcenode a))!i. state_val s V = state_val s' V"
  shows "state_val (transfer (kind a) s) (ins!i) = 
         state_val (transfer (kind a) s') (ins!i)"
proof -
  from assms have params:"(params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i"
    by(rule CFG_call_edge_params)
  from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `(p,ins,outs) ∈ set procs`
  have [simp]:"(THE ins. ∃outs. (p,ins,outs) ∈ set procs) = ins"
    by(rule formal_in_THE)
  from `pred (kind a) s` obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
  from `pred (kind a) s'` obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
    by(cases s') auto
  from `kind a = Q:r\<hookrightarrow>⇘p⇙fs`
  have eqs:"fst (hd (transfer (kind a) s)) = (empty(ins [:=] params fs (fst cf)))"
    "fst (hd (transfer (kind a) s')) = (empty(ins [:=] params fs (fst cf')))"
    by simp_all
  from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `(p,ins,outs) ∈ set procs`
  have "length fs = length ins" by(rule CFG_call_edge_length)
  from `(p,ins,outs) ∈ set procs` have "distinct ins" by(rule distinct_formal_ins)
  with `i < length ins` `length fs = length ins`
  have "(empty(ins [:=] params fs (fst cf))) (ins!i) = (params fs (fst cf))!i"
    "(empty(ins [:=] params fs (fst cf'))) (ins!i) = (params fs (fst cf'))!i"
    by(fastforce intro:fun_upds_nth)+
  with eqs `kind a = Q:r\<hookrightarrow>⇘p⇙fs` params
  show ?thesis by simp
qed


lemma CFG_call_edge_no_param:
  assumes "valid_edge a" and "kind a = Q:r\<hookrightarrow>⇘p⇙fs" and "V ∉ set ins"
  and "(p,ins,outs) ∈ set procs" and "pred (kind a) s"
  shows "state_val (transfer (kind a) s) V = None"
proof -
  from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `(p,ins,outs) ∈ set procs`
  have [simp]:"(THE ins. ∃outs. (p,ins,outs) ∈ set procs) = ins"
    by(rule formal_in_THE)
  from `pred (kind a) s` obtain cf cfs where [simp]:"s = cf#cfs" by(cases s) auto
  from `V ∉ set ins` have "(empty(ins [:=] params fs (fst cf))) V = None"
    by(auto dest:fun_upds_notin)
  with `kind a = Q:r\<hookrightarrow>⇘p⇙fs` show ?thesis by simp
qed



lemma CFG_return_edge_param_out:
  assumes "valid_edge a" and "kind a = Q\<hookleftarrow>⇘p⇙f" and "i < length outs"
  and "(p,ins,outs) ∈ set procs" and "state_val s (outs!i) = state_val s' (outs!i)"
  and "s = cf#cfx#cfs" and "s' = cf'#cfx'#cfs'"
  shows "state_val (transfer (kind a) s) ((ParamDefs (targetnode a))!i) =
         state_val (transfer (kind a) s') ((ParamDefs (targetnode a))!i)"
proof -
  from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f` `(p,ins,outs) ∈ set procs`
  have [simp]:"(THE outs. ∃ins. (p,ins,outs) ∈ set procs) = outs"
    by(rule formal_out_THE)
  from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f` `(p,ins,outs) ∈ set procs` `s = cf#cfx#cfs`
  have transfer:"fst (hd (transfer (kind a) s)) = 
    (fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf) outs)"
    by(fastforce intro:CFG_return_edge_fun)
  from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f` `(p,ins,outs) ∈ set procs` `s' = cf'#cfx'#cfs'`
  have transfer':"fst (hd (transfer (kind a) s')) = 
    (fst cfx')(ParamDefs (targetnode a) [:=] map (fst cf') outs)"
    by(fastforce intro:CFG_return_edge_fun)
  from `state_val s (outs!i) = state_val s' (outs!i)` `i < length outs`
    `s = cf#cfx#cfs` `s' = cf'#cfx'#cfs'`
  have "(fst cf) (outs!i) = (fst cf') (outs!i)" by simp
  from `valid_edge a` have "distinct (ParamDefs (targetnode a))"
    by(fastforce intro:distinct_ParamDefs)
  from `valid_edge a` `kind a = Q\<hookleftarrow>⇘p⇙f` `(p,ins,outs) ∈ set procs`
  have "length(ParamDefs (targetnode a)) = length outs"
    by(fastforce intro:ParamDefs_return_target_length)
  with `i < length outs` `distinct (ParamDefs (targetnode a))`
  have "(fst cfx)(ParamDefs (targetnode a) [:=] map (fst cf) outs)
    ((ParamDefs (targetnode a))!i) = (map (fst cf) outs)!i" 
    and "(fst cfx')(ParamDefs (targetnode a) [:=] map (fst cf') outs)
             ((ParamDefs (targetnode a))!i) = (map (fst cf') outs)!i"
    by(fastforce intro:fun_upds_nth)+
  with transfer transfer' `(fst cf) (outs!i) = (fst cf') (outs!i)` `i < length outs`
  show ?thesis by simp
qed


lemma CFG_slp_no_Def_equal:
  assumes "n -as->⇘sl⇙* n'" and "valid_edge a" and "a' ∈ get_return_edges a"
  and "V ∉ set (ParamDefs (targetnode a'))" and "preds (kinds (a#as@[a'])) s"
  shows "state_val (transfers (kinds (a#as@[a'])) s) V = state_val s V"
proof -
  from `valid_edge a` `a' ∈ get_return_edges a` 
  obtain Q r p fs where "kind a = Q:r\<hookrightarrow>⇘p⇙fs"
    by(fastforce dest!:only_call_get_return_edges)
  with `valid_edge a` `a' ∈ get_return_edges a` obtain Q' f' where "kind a' = Q'\<hookleftarrow>⇘p⇙f'"
    by(fastforce dest!:call_return_edges)
  from `valid_edge a` `a' ∈ get_return_edges a` have "valid_edge a'"
    by(rule get_return_edges_valid)
  from `preds (kinds (a#as@[a'])) s` obtain cf cfs where [simp]:"s = cf#cfs"
    by(cases s,auto simp:kinds_def)
  from `valid_edge a` `kind a = Q:r\<hookrightarrow>⇘p⇙fs` obtain ins outs 
    where "(p,ins,outs) ∈ set procs" by(fastforce dest!:callee_in_procs)
  from `kind a = Q:r\<hookrightarrow>⇘p⇙fs` obtain cfx where "transfer (kind a) s = cfx#cf#cfs"
    by simp
  moreover
  from `n -as->⇘sl⇙* n'` obtain cfx' 
    where "transfers (kinds as) (cfx#cf#cfs) = cfx'#cf#cfs"
    by(fastforce elim:slp_callstack_length_equal)
  moreover
  from `kind a' = Q'\<hookleftarrow>⇘p⇙f'` `valid_edge a'` `(p,ins,outs) ∈ set procs`
  have "fst (hd (transfer (kind a') (cfx'#cf#cfs))) = 
    (fst cf)(ParamDefs (targetnode a') [:=] map (fst cfx') outs)"
    by(simp,simp only:formal_out_THE,fastforce intro:CFG_return_edge_fun)
  ultimately have "fst (hd (transfers (kinds (a#as@[a'])) s)) = 
    (fst cf)(ParamDefs (targetnode a') [:=] map (fst cfx') outs)"
    by(simp add:kinds_def transfers_split)
  with `V ∉ set (ParamDefs (targetnode a'))` show ?thesis
    by(simp add:fun_upds_notin)
qed



lemma [dest!]: "V ∈ Use (_Entry_) ==> False"
by(simp add:Entry_empty)

lemma [dest!]: "V ∈ Def (_Entry_) ==> False"
by(simp add:Entry_empty)


lemma CFG_intra_path_no_Def_equal:
  assumes "n -as->⇣ι* n'" and "∀n ∈ set (sourcenodes as). V ∉ Def n"
  and "preds (kinds as) s"
  shows "state_val (transfers (kinds as) s) V = state_val s V"
proof -
  from `n -as->⇣ι* n'` have "n -as->* n'" and "∀a ∈ set as. intra_kind (kind a)"
    by(simp_all add:intra_path_def)
  from this `∀n ∈ set (sourcenodes as). V ∉ Def n` `preds (kinds as) s`
  have "state_val (transfers (kinds as) s) V = state_val s V"
  proof(induct arbitrary:s rule:path.induct)
    case (empty_path n)
    thus ?case by(simp add:sourcenodes_def kinds_def)
  next
    case (Cons_path n'' as n' a n)
    note IH = `!!s. [|∀a∈set as. intra_kind (kind a); 
                    ∀n∈set (sourcenodes as). V ∉ Def n; preds (kinds as) s|] 
      ==> state_val (transfers (kinds as) s) V = state_val s V`
    from `preds (kinds (a#as)) s` have "pred (kind a) s"
      and "preds (kinds as) (transfer (kind a) s)" by(simp_all add:kinds_def)
    from `∀n∈set (sourcenodes (a#as)). V ∉ Def n`
    have noDef:"V ∉ Def (sourcenode a)" 
      and all:"∀n∈set (sourcenodes as). V ∉ Def n"
      by(auto simp:sourcenodes_def)
    from `∀a∈set (a#as). intra_kind (kind a)`
    have "intra_kind (kind a)" and all':"∀a∈set as. intra_kind (kind a)"
      by auto
    from `valid_edge a` noDef `intra_kind (kind a)` `pred (kind a) s`
    have "state_val (transfer (kind a) s) V = state_val s V"
     by -(rule CFG_intra_edge_no_Def_equal)
    with IH[OF all' all `preds (kinds as) (transfer (kind a) s)`] show ?case
      by(simp add:kinds_def)
  qed
  thus ?thesis by blast
qed


lemma slpa_preds:
  "[|same_level_path_aux cs as; s = cfsx@cf#cfs; s' = cfsx@cf#cfs'; 
    length cfs = length cfs'; ∀a ∈ set as. valid_edge a; length cs = length cfsx; 
    preds (kinds as) s|]
  ==> preds (kinds as) s'"
proof(induct arbitrary:s s' cf cfsx rule:slpa_induct)
  case (slpa_empty cs) thus ?case by(simp add:kinds_def)
next
  case (slpa_intra cs a as)
  note IH = `!!s s' cf cfsx. [|s = cfsx@cf#cfs; s' = cfsx@cf#cfs';
    length cfs = length cfs'; ∀a ∈ set as. valid_edge a; length cs = length cfsx; 
    preds (kinds as) s|] ==> preds (kinds as) s'`
  from `∀a∈set (a#as). valid_edge a` have "valid_edge a"
    and "∀a ∈ set as. valid_edge a" by simp_all
  from `preds (kinds (a#as)) s` have "pred (kind a) s"
    and "preds (kinds as) (transfer (kind a) s)" by(simp_all add:kinds_def)
  show ?case
  proof(cases cfsx)
    case Nil
    with `length cs = length cfsx` have "length cs = length []" by simp
    from Nil `s = cfsx@cf#cfs` `s' = cfsx@cf#cfs'` `intra_kind (kind a)` 
    obtain cfx where "transfer (kind a) s = []@cfx#cfs"
      and "transfer (kind a) s' = []@cfx#cfs'"
      by(cases "kind a",auto simp:kinds_def intra_kind_def)
    from IH[OF this `length cfs = length cfs'` `∀a ∈ set as. valid_edge a`
      `length cs = length []` `preds (kinds as) (transfer (kind a) s)`]
    have "preds (kinds as) (transfer (kind a) s')" .
    moreover
    from Nil `valid_edge a` `pred (kind a) s` `s = cfsx@cf#cfs` `s' = cfsx@cf#cfs'`
      `length cfs = length cfs'`
    have "pred (kind a) s'" by(fastforce intro:CFG_edge_Uses_pred_equal)
    ultimately show ?thesis by(simp add:kinds_def)
  next
    case (Cons x xs)
    with `s = cfsx@cf#cfs` `s' = cfsx@cf#cfs'` `intra_kind (kind a)`
    obtain cfx where "transfer (kind a) s = (cfx#xs)@cf#cfs"
      and "transfer (kind a) s' = (cfx#xs)@cf#cfs'"
      by(cases "kind a",auto simp:kinds_def intra_kind_def)
    from IH[OF this `length cfs = length cfs'` `∀a ∈ set as. valid_edge a` _ 
      `preds (kinds as) (transfer (kind a) s)`] `length cs = length cfsx` Cons
    have "preds (kinds as) (transfer (kind a) s')" by simp
    moreover
    from Cons `valid_edge a` `pred (kind a) s` `s = cfsx@cf#cfs` `s' = cfsx@cf#cfs'`
      `length cfs = length cfs'` 
    have "pred (kind a) s'" by(fastforce intro:CFG_edge_Uses_pred_equal)
    ultimately show ?thesis by(simp add:kinds_def)
  qed
next
  case (slpa_Call cs a as Q r p fs)
  note IH = `!!s s' cf cfsx. [|s = cfsx@cf#cfs; s' = cfsx@cf#cfs';
    length cfs = length cfs'; ∀a ∈ set as. valid_edge a; length (a#cs) = length cfsx;
    preds (kinds as) s|] ==> preds (kinds as) s'`
  from `∀a∈set (a#as). valid_edge a` have "valid_edge a"
    and "∀a ∈ set as. valid_edge a" by simp_all
  from `preds (kinds (a#as)) s` have "pred (kind a) s"
    and "preds (kinds as) (transfer (kind a) s)" by(simp_all add:kinds_def)
  from `kind a = Q:r\<hookrightarrow>⇘p⇙fs` `s = cfsx@cf#cfs` `s' = cfsx@cf#cfs'` obtain cfx
    where "transfer (kind a) s = (cfx#cfsx)@cf#cfs"
    and "transfer (kind a) s' = (cfx#cfsx)@cf#cfs'" by(cases cfsx) auto
  from IH[OF this `length cfs = length cfs'` `∀a ∈ set as. valid_edge a` _ 
    `preds (kinds as) (transfer (kind a) s)`] `length cs = length cfsx`
  have "preds (kinds as) (transfer (kind a) s')" by simp
  moreover
  from `valid_edge a` `pred (kind a) s` `s = cfsx@cf#cfs` `s' = cfsx@cf#cfs'`
    `length cfs = length cfs'` have "pred (kind a) s'" 
    by(cases cfsx)(auto intro:CFG_edge_Uses_pred_equal)
  ultimately show ?case by(simp add:kinds_def)
next
  case (slpa_Return cs a as Q p f c' cs')
  note IH = `!!s s' cf cfsx. [|s = cfsx@cf#cfs; s' = cfsx@cf#cfs';
    length cfs = length cfs'; ∀a ∈ set as. valid_edge a; length cs' = length cfsx; 
    preds (kinds as) s|] ==> preds (kinds as) s'`
  from `∀a∈set (a#as). valid_edge a` have "valid_edge a"
    and "∀a ∈ set as. valid_edge a" by simp_all
  from `preds (kinds (a#as)) s` have "pred (kind a) s"
    and "preds (kinds as) (transfer (kind a) s)" by(simp_all add:kinds_def)
  show ?case
  proof(cases cs')
    case Nil
    with `cs = c'#cs'` `s = cfsx@cf#cfs` `s' = cfsx@cf#cfs'`
      `length cs = length cfsx` 
    obtain cf' where "s = cf'#cf#cfs" and "s' = cf'#cf#cfs'" by(cases cfsx) auto
    with `kind a = Q\<hookleftarrow>⇘p⇙f` obtain cf'' where "transfer (kind a) s = []@cf''#cfs"
      and "transfer (kind a) s' = []@cf''#cfs'" by auto
    from IH[OF this `length cfs = length cfs'` `∀a ∈ set as. valid_edge a` _ 
      `preds (kinds as) (transfer (kind a) s)`] Nil
    have "preds (kinds as) (transfer (kind a) s')" by simp
    moreover
    from `valid_edge a` `pred (kind a) s` `s = cfsx@cf#cfs` `s' = cfsx@cf#cfs'`
      `length cfs = length cfs'`  have "pred (kind a) s'" 
      by(cases cfsx)(auto intro:CFG_edge_Uses_pred_equal)
    ultimately show ?thesis by(simp add:kinds_def)
  next
    case (Cons cx csx)
    with `cs = c'#cs'` `length cs = length cfsx` `s = cfsx@cf#cfs` `s' = cfsx@cf#cfs'`
    obtain x x' xs where "s = (x#x'#xs)@cf#cfs" and "s' = (x#x'#xs)@cf#cfs'"
      and "length xs = length csx"
      by(cases cfsx,auto,case_tac list,fastforce+)
    with `kind a = Q\<hookleftarrow>⇘p⇙f` obtain cf' where "transfer (kind a) s = (cf'#xs)@cf#cfs"
      and "transfer (kind a) s' = (cf'#xs)@cf#cfs'"
      by fastforce
    from IH[OF this `length cfs = length cfs'` `∀a ∈ set as. valid_edge a` _ 
      `preds (kinds as) (transfer (kind a) s)`] Cons `length xs = length csx`
    have "preds (kinds as) (transfer (kind a) s')" by simp
    moreover
    from `valid_edge a` `pred (kind a) s` `s = cfsx@cf#cfs` `s' = cfsx@cf#cfs'`
      `length cfs = length cfs'`  have "pred (kind a) s'" 
      by(cases cfsx)(auto intro:CFG_edge_Uses_pred_equal)
    ultimately show ?thesis by(simp add:kinds_def)
  qed
qed


lemma slp_preds:
  assumes "n -as->⇘sl⇙* n'" and "preds (kinds as) (cf#cfs)" 
  and "length cfs = length cfs'"
  shows "preds (kinds as) (cf#cfs')"
proof -
  from `n -as->⇘sl⇙* n'` have "n -as->* n'" and "same_level_path_aux [] as"
    by(simp_all add:slp_def same_level_path_def)
  from `n -as->* n'` have "∀a ∈ set as. valid_edge a" by(rule path_valid_edges)
  with `same_level_path_aux [] as` `preds (kinds as) (cf#cfs)` 
    `length cfs = length cfs'`
  show ?thesis by(fastforce elim!:slpa_preds)
qed
end


end