Theory Call_Graph_Scc_Decomp

theory Call_Graph_Scc_Decomp
imports
  Auxx.Gabow_SCC_RBT
  Cooperation_Program
  Auxx.Shows_Literal_List
begin
      
locale call_graph_indexed_rewriting = indexed_rewriting induce for
  induce :: "'a ⇒ ('b × 'b)set" + 
  fixes call_locs :: "'a ⇒ 'l × 'l"     
  and loc :: "'b ⇒ 'l"
  and call_graph :: "'a set ⇒ ('l × 'l)set" 
assumes call_rel: "(b1,b2) ∈ induce a ⟹ call_locs a = (loc b1, loc b2)" 
  and call_graph: "call_graph as = call_locs ` as" 
begin
  
lemma cooperation_SN_on_decomposition:  
  assumes SN: "⋀ C. is_scc (call_graph P) C 
    ⟹ C × C ⊆ (call_graph P)^+ 
    ⟹ cooperation_SN_on R ({a . a ∈ P ∧ call_locs a ∈ C × C}) I" 
  shows "cooperation_SN_on R P I" 
proof 
  fix seq
  assume I: "seq 0 ∈ I" and chain: "cooperation_chain R P seq" 
  from cooperation_chainE[OF chain] obtain P' cp where 
    P': "P' ⊆ P" and rec: "recurring P' (shift seq cp)" and R: "⋀i. i < cp ⟹ (seq i, seq (Suc i)) ∈ Induce R" 
    by metis
  define ss where "ss = shift seq cp" 
  let ?loc = "λ i. loc (ss i)" 
  define L where "L = (λ i. loc (ss i))" 
  have locP': "(?loc i, ?loc (Suc i)) ∈ call_graph P'" for i using recurring_imp_chain[OF rec[folded ss_def], rule_format, of i]
    unfolding call_graph using call_rel by force
  then have locP: "(L i, L (Suc i)) ∈ call_graph P" for i using P' unfolding call_graph L_def by auto
  define C where "C = range ?loc"
  have Cne: "C ≠ {}" unfolding C_def by auto
  have "C × C ⊆ (call_graph P)^+" 
  proof
    fix a b
    assume "(a,b) ∈ C × C" 
    then have a: "a ∈ C" "b ∈ C" by auto
    from a(1)[unfolded C_def] obtain i where ai: "a = L i" by (auto simp: L_def)
    from a(2)[unfolded C_def] obtain j where bj: "b = L j" by (auto simp: L_def)
    {
      from recurring_imp_chain[OF rec, folded ss_def, rule_format, of j] obtain tau where 
        tau: "tau ∈ P'" and step: "(ss j, ss (Suc j)) ∈ induce tau" by auto
      from recurring_imp_INFM[OF rec tau, unfolded INFM_nat, rule_format, of i, folded ss_def]
        obtain J where iJ: "i < J" and step': "(ss J, ss (Suc J)) ∈ induce tau" by auto
      from call_rel[OF step] call_rel[OF step'] bj have "b = L J" by (auto simp: L_def)
      with iJ have "∃ j. i < j ∧ b = L j" by auto  
    }
    then obtain j where ij: "i < j" and bj: "b = L j" by auto
    show "(a,b) ∈ (call_graph P)^+" unfolding ai bj using ij locP
      using chain_imp_trancl by blast
  qed
  from get_scc_from_component[OF Cne this] obtain S where 
    CS: "C ⊆ S" and scc: "is_scc (call_graph P) S" "S × S ⊆ (call_graph P)^+" by auto
  let ?P' = "{a ∈ P. call_locs a ∈ S × S}" 
  have P': "P' ⊆ ?P'" 
  proof
    fix tau
    assume tau: "tau ∈ P'" 
    from recurring_imp_INFM[OF rec this, folded ss_def] obtain i where "(ss i, ss (Suc i)) ∈ induce tau" 
      unfolding INFM_nat_le by auto
    from call_rel[OF this] have "call_locs tau ∈ C × C" unfolding C_def by auto
    with CS P' tau  
    show "tau ∈ ?P'" by auto
  qed
  from SN[OF scc] have SN: "cooperation_SN_on R ?P' I" .
  show False
  proof (rule cooperation_SN_onE[OF SN, of seq, OF I])
    show "cooperation_chain R ?P' seq" 
      by (rule cooperation_chainI[of P' _ _ cp, OF P' rec], rule R)
  qed
qed
end

type_synonym 'l scc_repr = "'l list"  
type_synonym 'l scc_decomposition_info = "'l scc_repr list"  

context lts
begin
lemma call_graph: "call_graph_indexed_rewriting (transition_step lc) (λ tau. (source tau, target tau)) location (λ taus. { (source τ, target τ) | τ. τ ∈ taus})"  
  by (unfold_locales, auto)

definition "call_graph_sharp_impl R = remdups [(source (snd τ), target (snd τ)). τ ← transitions_impl R, is_sharp_transition (snd τ)]"

definition scc_decomposition :: "('f,'v,'ty,'l :: {showl,compare_order} sharp,'tr) lts_impl ⇒ 'l sharp scc_decomposition_info ⇒ showsl + _" where
  "scc_decomposition CP sccs_info = do {
      let CG = call_graph_sharp_impl CP;
      let sccs = scc_decomp CG;
      check_allm (λ C. check (∃ D ∈ set sccs_info. set C = set D) 
        (showsl_lit (STR ''could not find SCC '') o showsl C o showsl_lit (STR '' in provided decomposition'')))
        sccs;
      let trans = lts_impl.transitions_impl CP;
      let (sharp, flat) = partition (λ tau. is_sharp_transition (snd tau)) trans;
      let CPs = map (λ C. let L = set C in 
        Lts_Impl (lts_impl.initial CP) (flat @ filter (λ tau. source (snd tau) ∈ L ∧ target (snd tau) ∈ L) sharp) 
          (assertion_impl CP)) sccs_info
      in return CPs <+? (λ s. showsl_lit (STR ''error is SCC-decomposition w.r.t. sccs_info⏎'') o showsl sccs_info o showsl_nl o s)
    }" 
  
lemma scc_decomposition: assumes SN: "⋀ C. C ∈ set CPs ⟹ cooperation_SN_impl C" 
  and ret: "scc_decomposition CP sccs_info = return CPs" 
shows "cooperation_SN_impl CP" 
proof -
  note ret = ret[unfolded scc_decomposition_def, simplified, unfolded]
  show ?thesis 
  proof (intro cooperation_SN_implI)
    assume CP: "lts_impl CP"
    show "indexed_rewriting.cooperation_SN_on (transition_step_lts (lts_of CP)) (flat_transitions_of (lts_of CP)) (sharp_transitions_of (lts_of CP)) (initial_states (lts_of CP))"      
    proof (rule call_graph_indexed_rewriting.cooperation_SN_on_decomposition[OF call_graph], goal_cases)
      case (1 C)
      let ?CG = "{(source τ, target τ) |τ. τ ∈ sharp_transitions_of (lts_of CP)}" 
      have CG: "?CG = set (call_graph_sharp_impl CP)" unfolding call_graph_sharp_impl_def 
        by (cases CP, auto)
      from 1 have "C ∈ {C. is_scc (set (call_graph_sharp_impl CP)) C ∧ C × C ⊆ (set (call_graph_sharp_impl CP))⇧+}" 
        unfolding CG by auto
      from this[folded scc_decomp] 
      obtain CC where "set CC = C" and "CC ∈ set (scc_decomp (call_graph_sharp_impl CP))" by auto
      with ret obtain D where DC: "set D = C" and D: "D ∈ set sccs_info" by auto
      let ?Q = "Lts_Impl (lts_impl.initial CP)
            ([tau←transitions_impl CP . ¬ is_sharp_transition (snd tau)] @
             [tau←transitions_impl CP . is_sharp_transition (snd tau) ∧ source (snd tau) ∈ C ∧ target (snd tau) ∈ C])
            (assertion_impl CP)" 
      have subI: "sub_lts_impl ?Q CP" by (cases CP, auto simp: mset_filter subseteq_mset_def)
      note sub = sub_lts_impl_sub_lts[OF subI]
      from SN D DC ret have SN: "cooperation_SN_impl ?Q" by (auto simp: o_def)
      from sub_lts_impl[OF subI CP(1)] have lts: "lts_impl ?Q" .
      with SN have SN: "cooperation_SN (lts_of ?Q)" by(elim cooperation_SN_implE)
      also have "flat_transitions_of (lts_of ?Q) = flat_transitions_of (lts_of CP)" by force
      also have "initial_states (lts_of ?Q) = initial_states (lts_of CP)" 
        by (auto simp: initial_states_def assertion_of_def)
      also have "sharp_transitions_of (lts_of ?Q) = {a ∈ sharp_transitions_of (lts_of CP). (source a, target a) ∈ C × C}"
        by auto
      finally show ?case by (simp add: assertion_of_def)
    qed
  qed
qed

lemma length_scc_decomposition: assumes "scc_decomposition cp infos = return xs" 
  shows "length infos = length xs" 
  using assms unfolding scc_decomposition_def Let_def by auto

end

  
declare lts.call_graph_sharp_impl_def[code]
declare lts.scc_decomposition_def[code]
  
end