Theory CAVA_Automata.Automata

section ‹Automata›
(* Author: Peter Lammich *)
theory Automata
imports Digraph
begin
  text ‹
    In this theory, we define Generalized Buchi Automata and Buchi Automata 
    based on directed graphs
›

hide_const (open) prod
  
subsection "Generalized Buchi Graphs"
text ‹
  A generalized Buchi graph is a graph where each node belongs to a set of
  acceptance classes. An infinite run on this graph is accepted, iff
  it visits nodes from each acceptance class infinitely often.

  The standard encoding of acceptance classes is as a set of sets of nodes,
  each inner set representing one acceptance class.
›

record 'Q gb_graph_rec = "'Q graph_rec" +
  gbg_F :: "'Q set set"


locale gb_graph =
  graph G 
  for G :: "('Q,'more) gb_graph_rec_scheme" +
  assumes finite_F[simp, intro!]: "finite (gbg_F G)"
  assumes F_ss: "gbg_F G  Pow V"
begin
  abbreviation "F  gbg_F G"

  lemma is_gb_graph: "gb_graph G" by unfold_locales


  definition 
    is_acc :: "'Q word  bool" where "is_acc r  (AF. i. r i  A)"

  definition "is_acc_run r  is_run r  is_acc r"

  (* For presentation in paper *)
  lemma "is_acc_run r  is_run r  (AF. i. r i  A)"
    unfolding is_acc_run_def is_acc_def .

  lemma acc_run_run: "is_acc_run r  is_run r"
    unfolding is_acc_run_def by simp

  lemmas acc_run_reachable = run_reachable[OF acc_run_run]


  lemma acc_eq_limit: 
    assumes FIN: "finite (range r)"  
    shows "is_acc r  (AF. limit r  A  {})"
  proof 
    assume "AF. limit r  A  {}"
    thus "is_acc r"
      unfolding is_acc_def
      by (metis limit_inter_INF)
  next
    from FIN have FIN': "A. finite (A  range r)"
      by simp

    assume "is_acc r"
    hence AUX: "AF. i. r i  (A  range r)"
      unfolding is_acc_def by auto
    have "AF. limit r  (A  range r)  {}"
      apply (rule ballI)
      apply (drule bspec[OF AUX])
      apply (subst (asm) fin_ex_inf_eq_limit[OF FIN'])
      .
    thus "AF. limit r  A  {}" 
      by auto
  qed

  lemma is_acc_run_limit_alt:
    assumes "finite (E* `` V0)"
    shows "is_acc_run r  is_run r  (AF. limit r  A  {})"
    using assms acc_eq_limit[symmetric] unfolding is_acc_run_def
    by (auto dest: run_reachable finite_subset)

  lemma is_acc_suffix[simp]: "is_acc (suffix i r)  is_acc r"
    unfolding is_acc_def suffix_def
    apply (clarsimp simp: INFM_nat)
    apply (rule iffI)
    apply (metis trans_less_add2)
    by (metis add_lessD1 less_imp_add_positive nat_add_left_cancel_less)

  lemma finite_V_Fe:
    assumes "finite V" "A  F"
    shows "finite A"
    using assms by (metis Pow_iff infinite_super rev_subsetD F_ss)

end


definition "gb_rename_ecnv ecnv f G  
  gbg_F = { f`A | A. Agbg_F G },  = ecnv G
"


abbreviation "gb_rename_ext ecnv f  fr_rename_ext (gb_rename_ecnv ecnv f) f"


locale gb_rename_precond =
  gb_graph G +
  g_rename_precond G f "gb_rename_ecnv ecnv f"
  for G :: "('u,'more) gb_graph_rec_scheme"
  and f :: "'u  'v" and ecnv
begin
  lemma G'_gb_fields: "gbg_F G' = { f`A | A. AF }"
    unfolding gb_rename_ecnv_def fr_rename_ext_def
    by simp

  sublocale G': gb_graph G' 
    apply unfold_locales
    apply (simp_all add: G'_fields G'_gb_fields)
    using F_ss 
    by auto

  lemma acc_sim1: "is_acc r  G'.is_acc (f o r)"
    unfolding is_acc_def G'.is_acc_def G'_gb_fields
    by (fastforce intro: imageI simp: INFM_nat)

  lemma acc_sim2: 
    assumes "G'.is_acc r" shows "is_acc (fi o r)"
  proof -
    from assms have 1: "A m. A  gbg_F G  i>m. r i  f`A"
      unfolding G'.is_acc_def G'_gb_fields
      by (auto simp: INFM_nat)

    { fix A m 
      assume 2: "A  gbg_F G"  
      from 1[OF this, of m] have "i>m. fi (r i)  A"
        using F_ss
        apply clarsimp
        by (metis Pow_iff 2 fi_f in_mono)
    } thus ?thesis
      unfolding is_acc_def
      by (auto simp: INFM_nat)
  qed

  lemma acc_run_sim1: "is_acc_run r  G'.is_acc_run (f o r)"
    using acc_sim1 run_sim1 unfolding G'.is_acc_run_def is_acc_run_def
    by auto

  lemma acc_run_sim2: "G'.is_acc_run r  is_acc_run (fi o r)"
    using acc_sim2 run_sim2 unfolding G'.is_acc_run_def is_acc_run_def
    by auto

end

subsection "Generalized Buchi Automata"
text ‹
  A GBA is obtained from a GBG by adding a labeling function, that associates
  each state with a set of labels. A word is accepted if there is an
  accepting run that can be labeld with this word.
›

record ('Q,'L) gba_rec = "'Q gb_graph_rec" +
  gba_L :: "'Q  'L  bool"

locale gba =
  gb_graph G
  for G :: "('Q,'L,'more) gba_rec_scheme" +
  assumes L_ss: "gba_L G q l  q  V"
begin
  abbreviation "L  gba_L G"

  lemma is_gba: "gba G" by unfold_locales

  definition "accept w  r. is_acc_run r  (i. L (r i) (w i))"
  lemma acceptI[intro?]: "is_acc_run r; i. L (r i) (w i)  accept w"
    by (auto simp: accept_def)

  definition "lang  Collect (accept)"
  lemma langI[intro?]: "accept w  wlang" by (auto simp: lang_def)
end

definition "gba_rename_ecnv ecnv f G  
  gba_L = λq l. 
    if qf`g_V G then 
      gba_L G (the_inv_into (g_V G) f q) l
    else
      False, 
   = ecnv G
"

abbreviation "gba_rename_ext ecnv f  gb_rename_ext (gba_rename_ecnv ecnv f) f"

locale gba_rename_precond =  
  gb_rename_precond G f "gba_rename_ecnv ecnv f" + gba G
  for G :: "('u,'L,'more) gba_rec_scheme"
  and f :: "'u  'v" and ecnv
begin
  lemma G'_gba_fields: "gba_L G' = (λq l. 
    if qf`V then L (fi q) l else False)"
    unfolding gb_rename_ecnv_def gba_rename_ecnv_def fr_rename_ext_def fi_def
    by simp

  sublocale G': gba G'
    apply unfold_locales
    apply (auto simp add: G'_gba_fields G'_fields split: if_split_asm)
    done

  lemma L_sim1: "range r  V; L (r i) l  G'.L (f (r i)) l"
    by (auto simp: G'_gba_fields fi_def[symmetric] fi_f 
      dest: inj_onD[OF INJ]
      dest!: rev_subsetD[OF rangeI[of _ i]])

  lemma L_sim2: " range r  f`V; G'.L (r i) l   L (fi (r i)) l"
    by (auto
      simp: G'_gba_fields fi_def[symmetric] f_fi
      dest!: rev_subsetD[OF rangeI[of _ i]])
    
  lemma accept_eq[simp]: "G'.accept = accept"
    apply (rule ext)
    unfolding accept_def G'.accept_def
  proof safe
    fix w r
    assume R: "G'.is_acc_run r"
    assume L: "i. G'.L (r i) (w i)"
    from R have RAN: "range r  f`V"
      using G'.run_reachable[OF G'.acc_run_run[OF R]] G'.reachable_V
      unfolding G'_fields
      by simp
    from L show "r. is_acc_run r  (i. L (r i) (w i))"
      using acc_run_sim2[OF R] L_sim2[OF RAN]
      by auto
  next
    fix w r
    assume R: "is_acc_run r" 
    assume L: "i. L (r i) (w i)"
    
    from R have RAN: "range r  V"
      using run_reachable[OF acc_run_run[OF R]] reachable_V by simp
      
    from L show "r. 
        G'.is_acc_run r 
       (i. G'.L (r i) (w i))"
      using acc_run_sim1[OF R] L_sim1[OF RAN]
      by auto
  qed

  lemma lang_eq[simp]: "G'.lang = lang"
    unfolding G'.lang_def lang_def by simp

  lemma finite_G'_V:
    assumes "finite V"
    shows "finite G'.V"
    using assms by (auto simp add: G'_gba_fields G'_fields split: if_split_asm)

end


abbreviation "gba_rename  gba_rename_ext (λ_. ())"

lemma gba_rename_correct:
  fixes G :: "('v,'l,'m) gba_rec_scheme"
  assumes "gba G" 
  assumes INJ: "inj_on f (g_V G)" 
  defines "G'  gba_rename f G"
  shows "gba G'"
  and "finite (g_V G)  finite (g_V G')"
  and "gba.accept G' = gba.accept G"
  and "gba.lang G' = gba.lang G"
  unfolding G'_def
proof -
  let ?G' = "gba_rename f G"
  interpret gba G by fact
  
  from INJ interpret gba_rename_precond G f "λ_. ()"
    by unfold_locales simp_all

  show "gba ?G'" by (rule G'.is_gba)
  show "finite (g_V G)  finite (g_V ?G')" by (fact finite_G'_V)
  show "G'.accept = accept" by simp
  show "G'.lang = lang" by simp
qed

subsection "Buchi Graphs"

text ‹A Buchi graph has exactly one acceptance class›

record 'Q b_graph_rec = "'Q graph_rec" +
  bg_F :: "'Q set"

locale b_graph =
  graph G 
  for G :: "('Q,'more) b_graph_rec_scheme"
  +
  assumes F_ss: "bg_F G  V"
begin
  abbreviation F where "F  bg_F G"

  lemma is_b_graph: "b_graph G" by unfold_locales

  definition "to_gbg_ext m 
      g_V = V, 
        g_E=E, 
        g_V0=V0, 
        gbg_F = if F=UNIV then {} else {F}, 
         = m "
  abbreviation "to_gbg  to_gbg_ext ()"

  sublocale gbg: gb_graph "to_gbg_ext m"
    apply unfold_locales 
    using V0_ss E_ss F_ss
    apply (auto simp: to_gbg_ext_def split: if_split_asm)
    done

  definition is_acc :: "'Q word  bool" where "is_acc r  (i. r i  F)"
  definition is_acc_run where "is_acc_run r  is_run r  is_acc r"

  lemma to_gbg_alt:
    "gbg.V T m = V"
    "gbg.E T m = E"
    "gbg.V0 T m = V0"
    "gbg.F T m = (if F=UNIV then {} else {F})"
    "gbg.is_run T m = is_run"
    "gbg.is_acc T m = is_acc"
    "gbg.is_acc_run T m = is_acc_run"
    unfolding is_run_def[abs_def] gbg.is_run_def[abs_def]
      is_acc_def[abs_def] gbg.is_acc_def[abs_def]
      is_acc_run_def[abs_def] gbg.is_acc_run_def[abs_def]
    by (auto simp: to_gbg_ext_def)

end

subsection "Buchi Automata"
text ‹Buchi automata are labeled Buchi graphs›

record ('Q,'L) ba_rec = "'Q b_graph_rec" +
  ba_L :: "'Q  'L  bool"

locale ba =
  bg?: b_graph G 
  for G :: "('Q,'L,'more) ba_rec_scheme"
  +
  assumes L_ss: "ba_L G q l  q  V"
begin
  abbreviation L where "L == ba_L G"

  lemma is_ba: "ba G" by unfold_locales


  abbreviation "to_gba_ext m  to_gbg_ext  gba_L = L, =m "
  abbreviation "to_gba  to_gba_ext ()"

  sublocale gba: gba "to_gba_ext m" 
    apply unfold_locales
    unfolding to_gbg_ext_def
    using L_ss apply auto []
    done

  lemma ba_acc_simps[simp]: "gba.L T m = L"
    by (simp add: to_gbg_ext_def)

  definition "accept w  (r. is_acc_run r  (i. L (r i) (w i)))"
  definition "lang  Collect accept"

  lemma to_gba_alt_accept: 
    "gba.accept T m = accept"
    apply (intro ext)
    unfolding accept_def gba.accept_def
    apply (simp_all add: to_gbg_alt)
    done

  lemma to_gba_alt_lang: 
    "gba.lang T m = lang"
    unfolding lang_def gba.lang_def
    apply (simp_all add: to_gba_alt_accept)
    done

  lemmas to_gba_alt = to_gbg_alt to_gba_alt_accept to_gba_alt_lang
end

subsection "Indexed acceptance classes"
record 'Q igb_graph_rec = "'Q graph_rec" +
  igbg_num_acc :: nat
  igbg_acc :: "'Q  nat set"

locale igb_graph = 
  graph G
  for G :: "('Q,'more) igb_graph_rec_scheme"
  +
  assumes acc_bound: "(range (igbg_acc G))  {0..<(igbg_num_acc G)}"
  assumes acc_ss: "igbg_acc G q  {}  qV"
begin
  abbreviation num_acc where "num_acc  igbg_num_acc G"
  abbreviation acc where "acc  igbg_acc G"

  lemma is_igb_graph: "igb_graph G" by unfold_locales


  lemma acc_boundI[simp, intro]: "xacc q  x<num_acc"
    using acc_bound by fastforce

  definition "accn i  {q . iacc q}"
  definition "F  { accn i | i. i<num_acc }"

  definition "to_gbg_ext m 
      g_V = V, g_E = E, g_V0 = V0, gbg_F = F, =m "

  sublocale gbg: gb_graph "to_gbg_ext m" 
    apply unfold_locales
    using V0_ss E_ss acc_ss
    apply (auto simp: to_gbg_ext_def F_def accn_def)
    done

  lemma to_gbg_alt1: 
    "gbg.E T m = E"
    "gbg.V0 T m = V0"
    "gbg.F T m = F" 
    by (simp_all add: to_gbg_ext_def)

  lemma F_fin[simp,intro!]: "finite F"
    unfolding F_def
    by auto

  definition is_acc :: "'Q word  bool" 
    where "is_acc r  (n<num_acc. i. n  acc (r i))"
  definition "is_acc_run r  is_run r  is_acc r"

  lemma is_run_gbg: 
    "gbg.is_run T m = is_run"
    unfolding is_run_def[abs_def] is_acc_run_def[abs_def] 
      gbg.is_run_def[abs_def] gbg.is_acc_run_def[abs_def] 
    by (simp_all add: to_gbg_ext_def)

  lemma is_acc_gbg: 
    "gbg.is_acc T m = is_acc"
    apply (intro ext)
    unfolding gbg.is_acc_def is_acc_def
    apply (simp add: to_gbg_alt1 is_run_gbg)
    unfolding F_def accn_def
    apply (blast intro: INFM_mono)
    done

  lemma is_acc_run_gbg: 
    "gbg.is_acc_run T m = is_acc_run"
    apply (intro ext)
    unfolding gbg.is_acc_run_def is_acc_run_def
    by (simp_all add: to_gbg_alt1 is_run_gbg is_acc_gbg)

  lemmas to_gbg_alt = to_gbg_alt1 is_run_gbg is_acc_gbg is_acc_run_gbg

  lemma acc_limit_alt: 
    assumes FIN: "finite (range r)"
    shows "is_acc r  (n<num_acc. limit r  accn n  {})"
  proof
    assume "n<num_acc. limit r  accn n  {}"
    thus "is_acc r"
      unfolding is_acc_def accn_def
      by (auto dest!: limit_inter_INF)
  next
    from FIN have FIN': "A. finite (A  range r)" by simp
    assume "is_acc r"
    hence "n<num_acc. limit r  (accn n  range r)  {}"
      unfolding is_acc_def accn_def
      by (auto simp: fin_ex_inf_eq_limit[OF FIN', symmetric])
    thus "n<num_acc. limit r  accn n  {}" by auto
  qed

  lemma acc_limit_alt': 
    "finite (range r)  is_acc r  ((acc ` limit r) = {0..<num_acc})"
    unfolding acc_limit_alt
    by (auto simp: accn_def)

end

record ('Q,'L) igba_rec = "'Q igb_graph_rec" +
  igba_L :: "'Q  'L  bool"

locale igba =
  igbg?: igb_graph G
  for G :: "('Q,'L,'more) igba_rec_scheme"
  +
  assumes L_ss: "igba_L G q l  q  V"
begin
  abbreviation L where "L  igba_L G"

  lemma is_igba: "igba G" by unfold_locales


  abbreviation "to_gba_ext m  to_gbg_ext  gba_L = igba_L G, =m "

  sublocale gba: gba "to_gba_ext m" 
    apply unfold_locales
    unfolding to_gbg_ext_def
    using L_ss
    apply auto
    done
  
  lemma to_gba_alt_L:
    "gba.L T m = L"
    by (auto simp: to_gbg_ext_def)

  definition "accept w  r. is_acc_run r  (i. L (r i) (w i))"
  definition "lang  Collect accept"

  lemma accept_gba_alt: "gba.accept T m = accept"
    apply (intro ext)
    unfolding accept_def gba.accept_def
    apply (simp add: to_gbg_alt to_gba_alt_L)
    done

  lemma lang_gba_alt: "gba.lang T m = lang"
    unfolding lang_def gba.lang_def
    apply (simp add: accept_gba_alt)
    done

  lemmas to_gba_alt = to_gbg_alt to_gba_alt_L accept_gba_alt lang_gba_alt

end

subsubsection ‹Indexing Conversion›
definition F_to_idx :: "'Q set set  (nat × ('Q  nat set)) nres" where
  "F_to_idx F  do {
    Flist  SPEC (λFlist. distinct Flist  set Flist = F);
    let num_acc = length Flist;
    let acc = (λv. {i . i<num_acc  vFlist!i});
    RETURN (num_acc,acc)
  }"

lemma F_to_idx_correct:
  shows "F_to_idx F  SPEC (λ(num_acc,acc). F = { {q. iacc q} | i. i<num_acc } 
     (range acc)  {0..<num_acc})"
  unfolding F_to_idx_def
  apply (refine_rcg refine_vcg)
  apply (clarsimp dest!: sym[where t=F])
  apply (intro equalityI subsetI)
  apply (auto simp: in_set_conv_nth) [2]

  apply auto []
  done

definition "mk_acc_impl Flist  do {
  let acc = Map.empty;

  (_,acc)  nfoldli Flist (λ_. True) (λA (i,acc). do {
    acc  FOREACHi (λit acc'. 
      acc' = (λv. 
        if vA-it then 
          Some (insert i (the_default {} (acc v))) 
        else 
          acc v
      )
    ) 
      A (λv acc. RETURN (acc(vinsert i (the_default {} (acc v))))) acc;
    RETURN (Suc i,acc)
  }) (0,acc);
  RETURN (λx. the_default {} (acc x))
}"

lemma mk_acc_impl_correct: 
  assumes F: "(Flist',Flist)Id"
  assumes FIN: "Aset Flist. finite A"
  shows "mk_acc_impl Flist'  Id (RETURN (λv. {i . i<length Flist  vFlist!i}))"
  using F apply simp
  unfolding mk_acc_impl_def

  apply (refine_rcg 
    nfoldli_rule[where 
      I="λl1 l2 (i,res). i=length l1 
         the_default {} o res = (λv. {j . j<i  vFlist!j})"
    ]
    refine_vcg 
  )
  using FIN apply (simp_all)
  apply (rule ext) apply auto []

  apply (rule ext) apply (auto split: if_split_asm simp: nth_append nth_Cons') []
  apply (rule ext) apply (auto split: if_split_asm simp: nth_append nth_Cons' 
    fun_comp_eq_conv) []

  apply (rule ext) apply (auto simp: fun_comp_eq_conv) []
  done

definition F_to_idx_impl :: "'Q set set  (nat × ('Q  nat set)) nres" where
  "F_to_idx_impl F  do {
    Flist  SPEC (λFlist. distinct Flist  set Flist = F);
    let num_acc = length Flist;
    acc  mk_acc_impl Flist;
    RETURN (num_acc,acc)
  }"

lemma F_to_idx_refine: 
  assumes FIN: "AF. finite A"
  shows "F_to_idx_impl F  Id (F_to_idx F)"
  using assms
  unfolding F_to_idx_impl_def F_to_idx_def

  apply (refine_rcg bind_Let_refine2[OF mk_acc_impl_correct])

  apply auto
  done

definition gbg_to_idx_ext 
  :: "_  ('a, 'more) gb_graph_rec_scheme  ('a, 'more') igb_graph_rec_scheme nres"
  where "gbg_to_idx_ext ecnv A = do {
  (num_acc,acc)  F_to_idx_impl (gbg_F A); 
  RETURN  
    g_V = g_V A,
    g_E = g_E A, 
    g_V0=g_V0 A, 
    igbg_num_acc = num_acc, 
    igbg_acc = acc,
     = ecnv A
  
}"

lemma (in gb_graph) gbg_to_idx_ext_correct:
  assumes [simp, intro]: " A. A  F  finite A"
  shows "gbg_to_idx_ext ecnv G  SPEC (λG'. 
    igb_graph.is_acc_run G' = is_acc_run 
   g_V G' = V
   g_E G' = E
   g_V0 G' = V0
   igb_graph_rec.more G' = ecnv G
   igb_graph G'
)"
proof -
  note F_to_idx_refine[of F]
  also note F_to_idx_correct
  finally have R: "F_to_idx_impl F
     SPEC (λ(num_acc, acc). F = {{q. i  acc q} |i. i < num_acc}
       (range acc)  {0..<num_acc})" by simp

  have eq_conjI: "a b c. (bc)  (a&b  a&c)" by simp

  {
    fix acc :: "'Q  nat set" and num_acc r
    have "(A. (i. A = {q. i  acc q}  i < num_acc)  (limit r  A  {})) 
       (i<num_acc. qlimit r. iacc q)"
      by blast
  } note aux1=this

  {
    fix acc :: "'Q  nat set" and num_acc i
    assume FE: "F = {{q. i  acc q} |i. i < num_acc}"
    assume INR: "(x. acc x)  {0..<num_acc}"
    have "finite {q. i  acc q}" 
    proof (cases "i<num_acc")
      case True thus ?thesis using FE by auto
    next
      case False hence "{q. i  acc q} = {}" using INR by force
      thus ?thesis by simp
    qed
  } note aux2=this

  {
    fix acc :: "'Q  nat set" and num_acc q
    assume FE: "F = {{q. i  acc q} |i. i < num_acc}"
      and INR: "(x. acc x)  {0..<num_acc}"
      and "acc q  {}"
    then obtain i where "iacc q" by auto
    moreover with INR have "i<num_acc" by force
    ultimately have "qF" by (auto simp: FE)
    with F_ss have "qV" by auto
  } note aux3=this

  show ?thesis
    unfolding gbg_to_idx_ext_def
    apply (refine_rcg order_trans[OF R] refine_vcg)
  proof clarsimp_all
    fix acc and num_acc :: nat
    assume FE[simp]: "F = {{q. i  acc q} |i. i < num_acc}"
      and BOUND: "(x. acc x)  {0..<num_acc}"
    let ?G' = "
      g_V = V, 
      g_E = E, 
      g_V0 = V0, 
      igbg_num_acc = num_acc, 
      igbg_acc = acc,
       = ecnv G"

    interpret G': igb_graph ?G'
      apply unfold_locales
      using V0_ss E_ss 
      apply (auto simp add: aux2 aux3 BOUND)
      done

    show "igb_graph ?G'" by unfold_locales

    show "G'.is_acc_run = is_acc_run"
      unfolding G'.is_acc_run_def[abs_def] is_acc_run_def[abs_def] 
        G'.is_run_def[abs_def] is_run_def[abs_def]
        G'.is_acc_def[abs_def] is_acc_def[abs_def]
      
      apply (clarsimp intro!: ext eq_conjI)
      apply auto []
      apply (metis (lifting, no_types) INFM_mono mem_Collect_eq)
      done
  qed
qed

abbreviation gbg_to_idx :: "('q,_) gb_graph_rec_scheme  'q igb_graph_rec nres"
  where "gbg_to_idx  gbg_to_idx_ext (λ_. ())"

definition ti_Lcnv where "ti_Lcnv ecnv A   igba_L = gba_L A, =ecnv A "

abbreviation "gba_to_idx_ext ecnv  gbg_to_idx_ext (ti_Lcnv ecnv)"
abbreviation "gba_to_idx  gba_to_idx_ext (λ_. ())"

lemma (in gba) gba_to_idx_ext_correct:
  assumes [simp, intro]: " A. A  F  finite A"
  shows "gba_to_idx_ext ecnv G  
    SPEC (λG'.
    igba.accept G' = accept 
   g_V G' = V
   g_E G' = E
   g_V0 G' = V0
   igba_rec.more G' = ecnv G
   igba G')"
  apply (rule order_trans[OF gbg_to_idx_ext_correct])
  apply (rule, assumption)
  apply (rule SPEC_rule)
  apply (elim conjE, intro conjI)
proof -
  fix G'
  assume 
    ARUN: "igb_graph.is_acc_run G' = is_acc_run"
    and MORE: "igb_graph_rec.more G' = ti_Lcnv ecnv G" 
    and LOC: "igb_graph G'"
    and FIELDS: "g_V G' = V" "g_E G' = E" "g_V0 G' = V0"
  
  from LOC interpret igb: igb_graph G' .

  interpret igb: igba G'
    apply unfold_locales
    using MORE FIELDS L_ss
    unfolding ti_Lcnv_def
    apply (cases G')
    apply simp
    done

  show "igba.accept G' = accept" and "igba_rec.more G' = ecnv G"
    using ARUN MORE 
    unfolding accept_def[abs_def] igb.accept_def[abs_def] ti_Lcnv_def
    apply (cases G', (auto) []) +
    done

  show "igba G'" by unfold_locales
qed

corollary (in gba) gba_to_idx_ext_lang_correct:
  assumes [simp, intro]: " A. A  F  finite A"
  shows "gba_to_idx_ext ecnv G  
    SPEC (λG'. igba.lang G' = lang  igba_rec.more G' = ecnv G  igba G')"
  apply (rule order_trans[OF gba_to_idx_ext_correct])
  apply (rule, assumption)
  apply (rule SPEC_rule)
  unfolding lang_def[abs_def]
  apply (subst igba.lang_def)
  apply auto
  done

subsubsection ‹Degeneralization›

context igb_graph
begin

  definition degeneralize_ext :: "_  ('Q × nat, _) b_graph_rec_scheme" where
    "degeneralize_ext ecnv  
      if num_acc = 0 then 
        g_V = V × {0},
        g_E = {((q,0),(q',0)) | q q'. (q,q')E}, 
        g_V0 = V0×{0}, 
        bg_F = V × {0},
         = ecnv G
      
      else 
        g_V = V × {0..<num_acc},
        g_E = { ((q,i),(q',i')) | i i' q q'. 
            i<num_acc 
           (q,q')E 
           i' = (if iacc q then (i+1) mod num_acc else i) },
        g_V0 = V0 × {0},
        bg_F = {(q,0)| q. 0acc q},
         = ecnv G
      "

  abbreviation degeneralize where "degeneralize  degeneralize_ext (λ_. ())"

  lemma degen_more[simp]: "b_graph_rec.more (degeneralize_ext ecnv) = ecnv G"
    unfolding degeneralize_ext_def
    by auto

  lemma degen_invar: "b_graph (degeneralize_ext ecnv)"
  proof
    let ?G' = "degeneralize_ext ecnv"

    show "g_V0 ?G'  g_V ?G'"
      unfolding degeneralize_ext_def
      using V0_ss
      by auto

    show "g_E ?G'  g_V ?G' × g_V ?G'"
      unfolding degeneralize_ext_def
      using E_ss
      by auto

    show "bg_F ?G'  g_V ?G'"
      unfolding degeneralize_ext_def
      using acc_ss
      by auto

  qed

  sublocale degen: b_graph "degeneralize_ext m" using degen_invar .

  lemma degen_finite_reachable:
    assumes [simp, intro]: "finite (E* `` V0)"
    shows "finite ((g_E (degeneralize_ext ecnv))* `` g_V0 (degeneralize_ext ecnv))"
  proof -
    let ?G' = "degeneralize_ext ecnv"
    have "((g_E ?G')* `` g_V0 ?G')
       E*``V0 × {0..num_acc}"
    proof -
      {
        fix q n q' n'
        assume "((q,n),(q',n'))(g_E ?G')*" 
          and 0: "(q,n)g_V0 ?G'"
        hence G1: "(q,q')E*  n'num_acc"
          apply (induction rule: rtrancl_induct2)
          by (auto simp: degeneralize_ext_def split: if_split_asm)
        
        from 0 have G2: "qV0  nnum_acc"
          by (auto simp: degeneralize_ext_def split: if_split_asm)
        note G1 G2
      } thus ?thesis by fastforce
    qed
    also have "finite " by auto
    finally (finite_subset) show "finite ((g_E ?G')* `` g_V0 ?G')" .
  qed

  lemma degen_is_run_sound: 
    "degen.is_run T m r  is_run (fst o r)"
    unfolding degen.is_run_def is_run_def
    unfolding degeneralize_ext_def
    apply (clarsimp split: if_split_asm simp: ipath_def)
    apply (metis fst_conv)+
    done

  lemma degen_path_sound: 
    assumes "path (degen.E T m) u p v" 
    shows "path E (fst u) (map fst p) (fst v)"
    using assms
    by induction (auto simp: degeneralize_ext_def path_simps split: if_split_asm)

  lemma degen_V0_sound: 
    assumes "u  degen.V0 T m" 
    shows "fst u  V0"
    using assms
    by (auto simp: degeneralize_ext_def path_simps split: if_split_asm)


  lemma degen_visit_acc:
    assumes "path (degen.E T m) (q,n) p (q',n')"
    assumes "nn'"
    shows "qa. (qa,n)set p  nacc qa"
    using assms
  proof (induction _ "(q,n)" p "(q',n')" arbitrary: q rule: path.induct)
    case (path_prepend qnh p)
    then obtain qh nh where [simp]: "qnh=(qh,nh)" by (cases qnh)
    from ((q,n),qnh)  degen.E T m 
    have "nh=n  (nh=(n+1) mod num_acc  nacc q)"
      by (auto simp: degeneralize_ext_def split: if_split_asm)
    thus ?case proof
      assume [simp]: "nh=n"
      from path_prepend obtain qa where "(qa, n)  set p" and "n  acc qa" 
        by auto
      thus ?case by auto
    next
      assume "(nh=(n+1) mod num_acc  nacc q)" thus ?case by auto
    qed
  qed simp

  lemma degen_run_complete0:
    assumes [simp]: "num_acc = 0"
    assumes R: "is_run r"
    shows "degen.is_run T m (λi. (r i,0))"
    using R
    unfolding degen.is_run_def is_run_def
    unfolding ipath_def degeneralize_ext_def
    by auto

  lemma degen_acc_run_complete0:
    assumes [simp]: "num_acc = 0"
    assumes R: "is_acc_run r"
    shows "degen.is_acc_run T m (λi. (r i,0))"
    using R
    unfolding degen.is_acc_run_def is_acc_run_def is_acc_def degen.is_acc_def
    apply (simp add: degen_run_complete0)
    unfolding degeneralize_ext_def
    using run_reachable[of r] reachable_V
    by (auto simp: INFM_nat)

  lemma degen_run_complete:
    assumes [simp]: "num_acc  0"
    assumes R: "is_run r"
    shows "r'. degen.is_run T m r'  r = fst o r'"
    using R
    unfolding degen.is_run_def is_run_def ipath_def
    apply (elim conjE)
  proof -
    assume R0: "r 0  V0" and RS: "i. (r i, r (Suc i))  E"

    define r' where "r' = rec_nat
      (r 0,0) 
      (λi (q,n). (r (Suc i), if n  acc q then (n+1) mod num_acc else n))"

    have [simp]:
      "r' 0 = (r 0,0)"
      "i. r' (Suc i) = (
        let 
          (q,n)=r' i 
        in 
          (r (Suc i), if n  acc q then (n+1) mod num_acc else n)
      )"
      unfolding r'_def
      by auto

    have R0': "r' 0  degen.V0 T m" using R0
      unfolding degeneralize_ext_def by auto

    have MAP: "r = fst o r'"
    proof (rule ext)
      fix i
      show "r i = (fst o r') i"
        by (cases i) (auto simp: split: prod.split)
    qed

    have [simp]: "0<num_acc" by (cases num_acc) auto

    have SND_LESS: "i. snd (r' i) < num_acc"
    proof -
      fix i show "snd (r' i) < num_acc" by (induction i) (auto split: prod.split) 
    qed

    have RS': "i. (r' i, r' (Suc i))  degen.E T m"
    proof
      fix i
      obtain n where [simp]: "r' i = (r i,n)"
        apply (cases i)
        apply (force)
        apply (force split: prod.split)
        done
      from SND_LESS[of i] have [simp]: "n<num_acc" by simp

      show "(r' i, r' (Suc i))  degen.E T m" using RS
        by (auto simp: degeneralize_ext_def)
    qed

    from R0' RS' MAP show 
      "r'. (r' 0  degen.V0 T m
       (i. (r' i, r' (Suc i))  degen.E T m)) 
       r = fst  r'" by blast
  qed

  lemma degen_run_bound:
    assumes [simp]: "num_acc  0"
    assumes R: "degen.is_run T m r"
    shows "snd (r i) < num_acc"
    apply (induction i)
    using R 
    unfolding degen.is_run_def is_run_def
    unfolding degeneralize_ext_def ipath_def
    apply -
    apply auto []
    apply clarsimp
    by (metis snd_conv)
  
  lemma degen_acc_run_complete_aux1: 
    assumes NN0[simp]: "num_acc  0"
    assumes R: "degen.is_run T m r"
    assumes EXJ: "ji. n  acc (fst (r j))"
    assumes RI: "r i = (q,n)"
    shows "ji. q'. r j = (q',n)  n  acc q'"
  proof -
    define j where "j = (LEAST j. ji  n  acc (fst (r j)))"

    from RI have "n<num_acc" using degen_run_bound[OF NN0 R, of i] by auto
    from EXJ have 
      "ji" 
      "n  acc (fst (r j))" 
      "ki. n  acc (fst (r k))  jk"
      using LeastI_ex[OF EXJ]
      unfolding j_def
      apply (auto) [2]
      apply (metis (lifting) Least_le)
      done
    hence "ki. k<j  n  acc (fst (r k))" by auto

    have "k. ki  kj  (snd (r k) = n)"
    proof (clarify)
      fix k
      assume "ik" "kj"
      thus "snd (r k) = n"
      proof (induction k rule: less_induct)
        case (less k)
        show ?case proof (cases "k=i")
          case True thus ?thesis using RI by simp
        next
          case False with less.prems have "k - 1 < k" "i  k - 1" "k - 1j"
            by auto
          from less.IH[OF this] have "snd (r (k - 1)) = n" .
          moreover from R have 
            "(r (k - 1), r k)  degen.E T m"
            unfolding degen.is_run_def is_run_def ipath_def
            by clarsimp (metis One_nat_def Suc_diff_1 k - 1 < k 
              less_nat_zero_code neq0_conv)
          moreover have "n  acc (fst (r (k - 1)))"
            using ki. k < j  n  acc (fst (r k)) i  k - 1 k - 1 < k 
              dual_order.strict_trans1 less.prems(2) 
              by blast
          ultimately show ?thesis
            by (auto simp: degeneralize_ext_def)
        qed
      qed
    qed

    thus ?thesis 
      by (metis i  j n  local.acc (fst (r j)) 
        order_refl surjective_pairing)
  qed
      
  lemma degen_acc_run_complete_aux1': 
    assumes NN0[simp]: "num_acc  0"
    assumes R: "degen.is_run T m r"
    assumes ACC: "n<num_acc. i. n  acc (fst (r i))"
    assumes RI: "r i = (q,n)"
    shows "ji. q'. r j = (q',n)  n  acc q'"
  proof -
    from RI have "n<num_acc" using degen_run_bound[OF NN0 R, of i] by auto
    with ACC have EXJ: "ji. n  acc (fst (r j))" 
      unfolding INFM_nat_le by blast

    from degen_acc_run_complete_aux1[OF NN0 R EXJ RI] show ?thesis .
  qed

  lemma degen_acc_run_complete_aux2:
    assumes NN0[simp]: "num_acc  0"
    assumes R: "degen.is_run T m r"
    assumes ACC: "n<num_acc. i. n  acc (fst (r i))"
    assumes RI: "r i = (q,n)" and OFS: "ofs<num_acc"
    shows "ji. q'. 
      r j = (q',(n + ofs) mod num_acc)  (n + ofs) mod num_acc  acc q'"
    using RI OFS
  proof (induction ofs arbitrary: q n i)
    case 0 
    from degen_run_bound[OF NN0 R, of i] r i = (q, n) 
    have NLE: "n<num_acc" 
      by simp

    with degen_acc_run_complete_aux1'[OF NN0 R ACC r i = (q, n)] show ?case
      by auto
  next
    case (Suc ofs)
    from Suc.IH[OF Suc.prems(1)] Suc.prems(2)
    obtain j q' where "ji" and RJ: "r j = (q',(n+ofs) mod num_acc)" 
      and A: "(n+ofs) mod num_acc  acc q'"
      by auto
    from R have "(r j, r (Suc j))  degen.E T m" 
      by (auto simp: degen.is_run_def is_run_def ipath_def)
    with RJ A obtain q2 where RSJ: "r (Suc j) = (q2,(n+Suc ofs) mod num_acc)" 
      by (auto simp: degeneralize_ext_def mod_simps)

    have aux: "j'. ij  Suc j  j'  ij'" by auto
    from degen_acc_run_complete_aux1'[OF NN0 R ACC RSJ] ji 
    show ?case 
      by (auto dest: aux)
  qed

  lemma degen_acc_run_complete:
    assumes AR: "is_acc_run r"
    obtains r' 
    where "degen.is_acc_run T m r'" and "r = fst o r'"
  proof (cases "num_acc = 0")
    case True 
    with AR degen_acc_run_complete0 
    show ?thesis by (auto intro!: that[of "(λi. (r i, 0))"])
  next
    case False
    assume NN0[simp]: "num_acc  0"

    from AR have R: "is_run r" and ACC: "n<num_acc. i. n  acc (r i)"
      unfolding is_acc_run_def is_acc_def by auto

    from degen_run_complete[OF NN0 R] obtain r' where 
      R': "degen.is_run T m r'" 
      and [simp]: "r = fst  r'" 
      by auto

    from ACC have ACC': "n<num_acc. i. n  acc (fst (r' i))" by simp

    have "i. j>i. r' j  degen.F T m"
    proof
      fix i
      obtain q n where RI: "r' (Suc i) = (q,n)" by (cases "r' (Suc i)")
      have "(n + (num_acc - n mod num_acc)) mod num_acc = 0"
        apply (rule dvd_imp_mod_0)
        apply (metis (mono_tags, lifting) NN0 add_diff_inverse mod_0_imp_dvd
          mod_add_left_eq mod_less_divisor mod_self nat_diff_split not_gr_zero zero_less_diff)
        done
      then obtain ofs where 
        OFS_LESS: "ofs<num_acc" 
        and [simp]: "(n + ofs) mod num_acc = 0"
        by (metis NN0 Nat.add_0_right diff_less neq0_conv)
      with degen_acc_run_complete_aux2[OF NN0 R' ACC' RI OFS_LESS]
      obtain j q' where 
        "j>i" "r' j = (q',0)" and "0acc q'" 
        by (auto simp: less_eq_Suc_le)
      thus "j>i. r' j  degen.F T m" 
        by (auto simp: degeneralize_ext_def)
    qed
    hence "i. r' i  degen.F T m" by (auto simp: INFM_nat)

    have "degen.is_acc_run T m r'"
      unfolding degen.is_acc_run_def degen.is_acc_def
      by rule fact+
    thus ?thesis by (auto intro: that)
  qed

  lemma degen_run_find_change:
    assumes NN0[simp]: "num_acc  0"
    assumes R: "degen.is_run T m r"
    assumes A: "ij" "r i = (q,n)" "r j = (q',n')" "nn'"
    obtains k qk where "ik" "k<j" "r k = (qk,n)" "n  acc qk"
  proof -
    from degen_run_bound[OF NN0 R] A have "n<num_acc" "n'<num_acc"
      by (metis snd_conv)+

    define k where "k = (LEAST k. i<k  snd (r k)  n)"

    have "i<k" "snd (r k)  n"
      by (metis (lifting, mono_tags) LeastI_ex A k_def leD less_linear snd_conv)+

    from Least_le[where P="λk. i<k  snd (r k)  n", folded k_def]
    have LEK_EQN: "k'. ik'  k'<k  snd (r k') = n"
      using r i = (q,n)
      by clarsimp (metis le_neq_implies_less not_le snd_conv)
    hence SND_RKMO: "snd (r (k - 1)) = n" using i<k by auto
    moreover from R have "(r (k - 1), r k)  degen.E T m"
      unfolding degen.is_run_def ipath_def using i<k
      by clarsimp (metis Suc_pred gr_implies_not0 neq0_conv) 
    moreover note snd (r k)  n
    ultimately have "n  acc (fst (r (k - 1)))"
      by (auto simp: degeneralize_ext_def split: if_split_asm)
    moreover have "k - 1 < j" using A LEK_EQN 
      apply (rule_tac ccontr)
      apply clarsimp
      by (metis One_nat_def snd (r (k - 1)) = n less_Suc_eq 
        less_imp_diff_less not_less_eq snd_conv)
    ultimately show thesis
      apply -
      apply (rule that[of "k - 1" "fst (r (k - 1))"])
      using i<k SND_RKMO by auto
  qed


  lemma degen_run_find_acc_aux:
    assumes NN0[simp]: "num_acc  0"
    assumes AR: "degen.is_acc_run T m r"
    assumes A: "r i = (q,0)" "0  acc q" "n<num_acc"
    shows "j qj. ij  r j = (qj,n)  n  acc qj"
  proof -
    from AR have R: "degen.is_run T m r" 
      and ACC: "i. r i  degen.F T m"
      (*and ACC: "limit r ∩ bg_F (degeneralize_ext ecnv) ≠ {}"*)
      unfolding degen.is_acc_run_def degen.is_acc_def by auto
    from ACC have ACC': "i. j>i. r j  degen.F T m"
      by (auto simp: INFM_nat)
    
    show ?thesis using n<num_acc
    proof (induction n)
      case 0 thus ?case using A by auto
    next
      case (Suc n)
      then obtain j qj where "ij" "r j = (qj,n)" "nacc qj" by auto
      moreover from R have "(r j, r (Suc j))  degen.E T m" 
        unfolding degen.is_run_def ipath_def
        by auto
      ultimately obtain qsj where RSJ: "r (Suc j) = (qsj,Suc n)"
        unfolding degeneralize_ext_def using Suc n<num_acc by auto
      
      from ACC' obtain k q0 where "Suc j  k" "r k = (q0, 0)"
        unfolding degeneralize_ext_def apply auto
        by (metis less_imp_le_nat)
      from degen_run_find_change[OF NN0 R Suc j  k RSJ r k = (q0, 0)] 
      obtain l ql where
        "Suc j  l" "l < k" "r l = (ql, Suc n)" "Suc n  acc ql" 
        by blast
      thus ?case using i  j
        by (intro exI[where x=l] exI[where x=ql]) auto
    qed
  qed
      
  lemma degen_acc_run_sound:
    assumes A: "degen.is_acc_run T m r"
    shows "is_acc_run (fst o r)"
  proof -
    from A have R: "degen.is_run T m r" 
      and ACC: "i. r i  degen.F T m"
      unfolding degen.is_acc_run_def degen.is_acc_def by auto
    from degen_is_run_sound[OF R] have R': "is_run (fst o r)" .

    show ?thesis
    proof (cases "num_acc = 0")
      case NN0[simp]: False

      from ACC have ACC': "i. j>i. r j  degen.F T m"
        by (auto simp: INFM_nat)

      have "n<num_acc. i. j>i. n  acc (fst (r j))" 
      proof (intro allI impI)
        fix n i

        obtain j qj where "j>i" and RJ: "r j = (qj,0)" and ACCJ: "0  acc (qj)"
          using ACC' unfolding degeneralize_ext_def by fastforce

        assume NLESS: "n<num_acc"
        show "j>i. n  acc (fst (r j))"
        proof (cases n)
          case 0 thus ?thesis using j>i RJ ACCJ by auto
        next
          case [simp]: (Suc n')
          from degen_run_find_acc_aux[OF NN0 A RJ ACCJ NLESS] obtain k qk where
            "jk" "r k = (qk,n)" "n  acc qk" by auto
          thus ?thesis
            by (metis i < j dual_order.strict_trans1 fst_conv)
        qed
      qed
      hence "n<num_acc. i. n  acc (fst (r i))"
        by (auto simp: INFM_nat)
      with R' show ?thesis
        unfolding is_acc_run_def is_acc_def by auto
    next
      case [simp]: True
      with R' show ?thesis
        unfolding is_acc_run_def is_acc_def
        by auto
    qed
  qed

  lemma degen_acc_run_iff:
    "is_acc_run r  (r'. fst o r' = r  degen.is_acc_run T m r')"
    using degen_acc_run_complete degen_acc_run_sound
    by blast

end

subsection "System Automata"
text ‹
  System automata are (finite) rooted graphs with a labeling function. They are 
  used to describe the model (system) to be checked.
›

record ('Q,'L) sa_rec = "'Q graph_rec" +
  sa_L :: "'Q  'L"

locale sa =
  g?: graph G
  for G :: "('Q, 'L, 'more) sa_rec_scheme"
begin

  abbreviation L where "L  sa_L G"

  definition "accept w  r. is_run r  w = L o r"

  lemma acceptI[intro?]: "is_run r; w = L o r  accept w" by (auto simp: accept_def)

  definition "lang  Collect accept"

  lemma langI[intro?]: "accept w  wlang" by (auto simp: lang_def)

end

subsubsection "Product Construction"
text ‹
  In this section we formalize the product construction between a GBA and a system
  automaton. The result is a GBG and a projection function, such that projected 
  runs of the GBG correspond to words accepted by the GBA and the system.
›

locale igba_sys_prod_precond = igba: igba G + sa: sa S for
  G :: "('q,'l,'moreG) igba_rec_scheme"
  and S :: "('s,'l,'moreS) sa_rec_scheme"
begin

  definition "prod  
    g_V = igba.V × sa.V,
    g_E = { ((q,s),(q',s')). 
      igba.L q (sa.L s)  (q,q')  igba.E  (s,s')  sa.E },
    g_V0 = igba.V0 × sa.V0,
    igbg_num_acc = igba.num_acc,
    igbg_acc = (λ(q,s). if ssa.V then igba.acc q else {} ) "

  lemma prod_invar: "igb_graph prod" 
    apply unfold_locales

    using igba.V0_ss sa.V0_ss
    apply (auto simp: prod_def) []

    using igba.E_ss sa.E_ss
    apply (auto simp: prod_def) []

    using igba.acc_bound
    apply (auto simp: prod_def split: if_split_asm) []

    using igba.acc_ss
    apply (fastforce simp: prod_def split: if_split_asm) []
    done
  
  sublocale prod: igb_graph prod using prod_invar .

  lemma prod_finite_reachable:
    assumes "finite (igba.E* `` igba.V0)" "finite (sa.E* `` sa.V0)"
    shows "finite ((g_E prod)* `` g_V0 prod)"
  proof -
    {
      fix q s q' s'
      assume "((q,s),(q',s'))  (g_E prod)*"
      hence "(q,q')  (igba.E)*  (s,s')  (sa.E)*"
        apply (induction rule: rtrancl_induct2)
        apply (auto simp: prod_def)
        done
    } note gsp_reach=this

    have [simp]: "q s. (q,s)  g_V0 prod  q  igba.V0  s  sa.V0"
      by (auto simp: prod_def)

    have reachSS: 
      "((g_E prod)* `` g_V0 prod) 
       ((igba.E)* `` igba.V0) × (sa.E* `` sa.V0)"
      by (auto dest: gsp_reach)
    show ?thesis
      apply (rule finite_subset[OF reachSS])
      using assms
      by simp
  qed

  lemma prod_fields:
    "prod.V = igba.V × sa.V"
    "prod.E = { ((q,s),(q',s')). 
      igba.L q (sa.L s)  (q,q')  igba.E  (s,s')  sa.E }"
    "prod.V0 = igba.V0 × sa.V0"
    "prod.num_acc = igba.num_acc"
    "prod.acc = (λ(q,s). if ssa.V then igba.acc q else {} )"
    unfolding prod_def
    apply simp_all
    done

  lemma prod_run: "prod.is_run r  
      igba.is_run (fst o r) 
     sa.is_run (snd o r)
     (i. igba.L (fst (r i)) (sa.L (snd (r i))))" (is "?L=?R")
    apply rule
    unfolding igba.is_run_def sa.is_run_def prod.is_run_def
    unfolding prod_def ipath_def
    apply (auto split: prod.split_asm intro: in_prod_fst_sndI)
    apply (metis surjective_pairing)
    apply (metis surjective_pairing)
    apply (metis fst_conv snd_conv)
    apply (metis fst_conv snd_conv)
    apply (metis fst_conv snd_conv)
    done

  lemma prod_acc:
    assumes A: "range (snd o r)  sa.V"
    shows "prod.is_acc r  igba.is_acc (fst o r)"
  proof -
    {
      fix i
      from A have "prod.acc (r i) = igba.acc (fst (r i))"
        unfolding prod_fields
        apply safe
        apply (clarsimp_all split: if_split_asm)
        by (metis UNIV_I comp_apply imageI snd_conv subsetD)
    } note [simp] = this
    show ?thesis
      unfolding prod.is_acc_def igba.is_acc_def
      by (simp add: prod_fields(4))
  qed
  
  lemma gsp_correct1: 
    assumes A: "prod.is_acc_run r"
    shows "sa.is_run (snd o r)  (sa.L o snd o r  igba.lang)"
  proof -
    from A have PR: "prod.is_run r" and PA: "prod.is_acc r" 
      unfolding prod.is_acc_run_def by auto

    have PRR: "range r  prod.V" using prod.run_reachable prod.reachable_V PR by auto

    have RSR: "range (snd o r)  sa.V" using PRR unfolding prod_fields by auto
  
    show ?thesis
      using PR PA
      unfolding igba.is_acc_run_def
        igba.lang_def igba.accept_def[abs_def]
      apply (auto simp: prod_run prod_acc[OF RSR])
      done
  qed
  
  lemma gsp_correct2: 
    assumes A: "sa.is_run r" "sa.L o r  igba.lang"
    shows "r'. r = snd o r'  prod.is_acc_run r'"
  proof -
    have [simp]: "r r'. fst o (λi. (r i, r' i)) = r" 
      "r r'. snd o (λi. (r i, r' i)) = r'"
      by auto

    from A show ?thesis
      unfolding prod.is_acc_run_def 
        igba.lang_def igba.accept_def[abs_def] igba.is_acc_run_def
      apply (clarsimp simp: prod_run)
      apply (rename_tac ra)
      apply (rule_tac x="λi. (ra i, r i)" in exI)
      apply clarsimp
      
      apply (subst prod_acc)
      using order_trans[OF sa.run_reachable sa.reachable_V]
      apply auto []

      apply auto []
      done
  qed

end

end