Theory CAVA_Automata.Automata_Impl

section ‹Implementing Automata›
(* Author: Peter Lammich *)
theory Automata_Impl
imports Digraph_Impl Automata
begin

subsection ‹Indexed Generalized Buchi Graphs›


consts
  i_igbg_eext :: "interface  interface  interface"

abbreviation "i_igbg Ie Iv  Ie,Ivii_igbg_eext,Ivii_g_ext"

context begin interpretation autoref_syn .

lemma igbg_type[autoref_itype]:
  "igbg_num_acc ::i i_igbg Ie Iv i i_nat"
  "igbg_acc ::i i_igbg Ie Iv i Iv i i_natii_set"
  "igb_graph_rec_ext
    ::i i_nat i (Iv i i_natii_set) i Ie i Ie,Ivii_igbg_eext"
  by simp_all
end


record ('vi,'ei,'v0i,'acci) gen_igbg_impl = "('vi,'ei,'v0i) gen_g_impl" +
  igbgi_num_acc :: nat
  igbgi_acc :: 'acci

definition gen_igbg_impl_rel_eext_def_internal: 
  "gen_igbg_impl_rel_eext Rm Racc  { (
   igbgi_num_acc = num_acci, igbgi_acc = acci, =mi , 
   igbg_num_acc = num_acc, igbg_acc = acc, =m ) 
  | num_acci acci mi num_acc acc m. 
    (num_acci,num_acc)nat_rel 
   (acci,acc)Racc
   (mi,m)Rm
  }"

lemma gen_igbg_impl_rel_eext_def: 
  "Rm,Raccgen_igbg_impl_rel_eext = { (
   igbgi_num_acc = num_acci, igbgi_acc = acci, =mi , 
   igbg_num_acc = num_acc, igbg_acc = acc, =m ) 
  | num_acci acci mi num_acc acc m. 
    (num_acci,num_acc)nat_rel 
   (acci,acc)Racc
   (mi,m)Rm
  }"
  unfolding gen_igbg_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_igbg_impl_rel_sv[relator_props]: 
  "single_valued Racc; single_valued Rm 
   single_valued (Rm,Raccgen_igbg_impl_rel_eext)"
  unfolding gen_igbg_impl_rel_eext_def
  apply (rule single_valuedI)
  apply (clarsimp)
  apply (intro conjI)
  apply (rule single_valuedD[rotated], assumption+)
  apply (rule single_valuedD[rotated], assumption+)
  done

abbreviation gen_igbg_impl_rel_ext 
  :: "_  _  _  _  _  (_×(_,_)igb_graph_rec_scheme) set"
  where "gen_igbg_impl_rel_ext Rm Racc 
   Rm,Raccgen_igbg_impl_rel_eextgen_g_impl_rel_ext "

lemma gen_igbg_refine:
  fixes Rv Re Rv0 Racc
  assumes "TERM (Rv,Re,Rv0)"
  assumes "TERM (Racc)"
  shows
  "(igbgi_num_acc,igbg_num_acc) 
     Rv,Re,Rv0gen_igbg_impl_rel_ext Rm Racc  nat_rel"
  "(igbgi_acc,igbg_acc) 
     Rv,Re,Rv0gen_igbg_impl_rel_ext Rm Racc  Racc"
  "(gen_igbg_impl_ext, igb_graph_rec_ext) 
     nat_rel  Racc  Rm  Rm,Raccgen_igbg_impl_rel_eext"
  unfolding gen_igbg_impl_rel_eext_def gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation with bit-set›

definition igbg_impl_rel_eext_internal_def: 
  "igbg_impl_rel_eext Rm Rv  Rm, Rv  nat_relbs_set_relgen_igbg_impl_rel_eext"

lemma igbg_impl_rel_eext_def: 
  "Rm,Rvigbg_impl_rel_eext  Rm, Rv  nat_relbs_set_relgen_igbg_impl_rel_eext"
  unfolding igbg_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of igbg_impl_rel_eext i_igbg_eext]

lemma [relator_props, simp]: 
  "Range Rv = UNIV; single_valued Rm 
   single_valued (Rm,Rvigbg_impl_rel_eext)"
  unfolding igbg_impl_rel_eext_def by tagged_solver

lemma g_tag: "TERM (Rvfun_set_rel,Rvslg_rel,Rvlist_set_rel)" .
lemma frgv_tag: "TERM (Rvlist_set_rel,Rvslg_rel,Rvlist_set_rel)" .
lemma igbg_bs_tag: "TERM (Rv  nat_relbs_set_rel)" .

abbreviation "igbgv_impl_rel_ext Rm Rv 
   Rm, Rvigbg_impl_rel_eext, Rvfrgv_impl_rel_ext"

abbreviation "igbg_impl_rel_ext Rm Rv 
   Rm, Rvigbg_impl_rel_eext, Rvg_impl_rel_ext"

type_synonym ('v,'m) igbgv_impl_scheme = 
  "('v,  igbgi_num_acc::nat, igbgi_acc::'vinteger, ::'m  ) 
    frgv_impl_scheme"
type_synonym ('v,'m) igbg_impl_scheme = 
  "('v,  igbgi_num_acc::nat, igbgi_acc::'vinteger, ::'m  ) 
    g_impl_scheme"

context fixes Rv :: "('vi×'v) set" begin
lemmas [autoref_rules] = gen_igbg_refine[
  OF frgv_tag[of Rv] igbg_bs_tag[of Rv], 
  folded frgv_impl_rel_ext_def igbg_impl_rel_eext_def]

lemmas [autoref_rules] = gen_igbg_refine[
  OF g_tag[of Rv] igbg_bs_tag[of Rv], 
  folded g_impl_rel_ext_def igbg_impl_rel_eext_def]
end



schematic_goal "(?c::?'c, 
    λG x. if igbg_num_acc G = 0  1igbg_acc G x then (g_E G `` {x}) else {} 
  )?R"
  apply (autoref (keep_goal))
  done


schematic_goal "(?c, 
  λV0 E num_acc acc. 
     g_V = UNIV, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc 
  )Rlist_set_rel  Rslg_rel  nat_rel  (R  nat_relbs_set_rel) 
     igbg_impl_rel_ext unit_rel R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?c, 
  λV0 E num_acc acc. 
     g_V = {}, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc 
  )Rlist_set_rel  Rslg_rel  nat_rel  (R  nat_relbs_set_rel) 
     igbgv_impl_rel_ext unit_rel R"
  apply (autoref (keep_goal))
  done

subsection ‹Indexed Generalized Buchi Automata›

consts
  i_igba_eext :: "interface  interface  interface  interface"

abbreviation "i_igba Ie Iv Il 
   Ie,Iv,Ilii_igba_eext,Ivii_igbg_eext,Ivii_g_ext"
context begin interpretation autoref_syn .

lemma igba_type[autoref_itype]:
  "igba_L ::i i_igba Ie Iv Il i (Iv i Il i i_bool)"
  "igba_rec_ext ::i (Iv i Il i i_bool) i Ie i Ie,Iv,Ilii_igba_eext"
  by simp_all
end


record ('vi,'ei,'v0i,'acci,'Li) gen_igba_impl = 
  "('vi,'ei,'v0i,'acci)gen_igbg_impl" +
  igbai_L :: "'Li"

definition gen_igba_impl_rel_eext_def_internal: 
  "gen_igba_impl_rel_eext Rm Rl   { (
   igbai_L = Li, =mi , 
   igba_L = L, =m ) 
  | Li mi L m. 
    (Li,L)Rl
   (mi,m)Rm
  }"

lemma gen_igba_impl_rel_eext_def: 
  "Rm,Rlgen_igba_impl_rel_eext = { (
   igbai_L = Li, =mi , 
   igba_L = L, =m ) 
  | Li mi L m. 
    (Li,L)Rl
   (mi,m)Rm
  }"
  unfolding gen_igba_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_igba_impl_rel_sv[relator_props]: 
  "single_valued Rl; single_valued Rm 
   single_valued (Rm,Rlgen_igba_impl_rel_eext)"
  unfolding gen_igba_impl_rel_eext_def
  apply (rule single_valuedI)
  apply (clarsimp)
  apply (intro conjI)
  apply (rule single_valuedD[rotated], assumption+)
  apply (rule single_valuedD[rotated], assumption+)
  done

abbreviation gen_igba_impl_rel_ext 
  :: "_  _  _  _  _  _  (_ × ('a,'b,'c) igba_rec_scheme) set"
  where "gen_igba_impl_rel_ext Rm Rl 
     gen_igbg_impl_rel_ext (Rm,Rlgen_igba_impl_rel_eext)"

lemma gen_igba_refine:
  fixes Rv Re Rv0 Racc Rl
  assumes "TERM (Rv,Re,Rv0)"
  assumes "TERM (Racc)"
  assumes "TERM (Rl)"
  shows
  "(igbai_L,igba_L) 
     Rv,Re,Rv0gen_igba_impl_rel_ext Rm Rl Racc  Rl"
  "(gen_igba_impl_ext, igba_rec_ext) 
     Rl  Rm  Rm,Rlgen_igba_impl_rel_eext"
  unfolding gen_igba_impl_rel_eext_def gen_igbg_impl_rel_eext_def
    gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation as function›
definition igba_impl_rel_eext_internal_def: 
  "igba_impl_rel_eext Rm Rv Rl  Rm, Rv  Rl  bool_relgen_igba_impl_rel_eext"

lemma igba_impl_rel_eext_def: 
  "Rm,Rv,Rligba_impl_rel_eext  Rm, Rv  Rl  bool_relgen_igba_impl_rel_eext"
  unfolding igba_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of igba_impl_rel_eext i_igba_eext]

lemma [relator_props, simp]: 
  "Range Rv = UNIV; single_valued Rm; Range Rl = UNIV 
   single_valued (Rm,Rv,Rligba_impl_rel_eext)"
  unfolding igba_impl_rel_eext_def by tagged_solver

lemma igba_f_tag: "TERM (Rv  Rl  bool_rel)" .

abbreviation "igbav_impl_rel_ext Rm Rv Rl
   igbgv_impl_rel_ext (Rm, Rv, Rligba_impl_rel_eext) Rv"

abbreviation "igba_impl_rel_ext Rm Rv Rl 
   igbg_impl_rel_ext (Rm, Rv, Rligba_impl_rel_eext) Rv"

type_synonym ('v,'l,'m) igbav_impl_scheme = 
  "('v,  igbai_L :: 'v  'l  bool , ::'m  ) 
    igbgv_impl_scheme"

type_synonym ('v,'l,'m) igba_impl_scheme = 
  "('v,  igbai_L :: 'v  'l  bool , ::'m  ) 
    igbg_impl_scheme"

context 
  fixes Rv :: "('vi×'v) set" 
  fixes Rl :: "('Li×'l) set"
begin
lemmas [autoref_rules] = gen_igba_refine[
  OF frgv_tag[of Rv] igbg_bs_tag[of Rv] igba_f_tag[of Rv Rl], 
  folded frgv_impl_rel_ext_def igbg_impl_rel_eext_def igba_impl_rel_eext_def]

lemmas [autoref_rules] = gen_igba_refine[
  OF g_tag[of Rv] igbg_bs_tag[of Rv] igba_f_tag[of Rv Rl], 
  folded g_impl_rel_ext_def igbg_impl_rel_eext_def igba_impl_rel_eext_def]
end

thm autoref_itype

schematic_goal 
  "(?c::?'c, λG x l. if igba_L G x l then (g_E G `` {x}) else {} )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) num_acc acc L. 
   g_V = UNIV, g_E = E, g_V0 = V0, 
    igbg_num_acc = num_acc, igbg_acc = acc, igba_L = L 
  )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) num_acc acc L. 
   g_V = V0, g_E = E, g_V0 = V0, 
    igbg_num_acc = num_acc, igbg_acc = acc, igba_L = L 
  )?R"
  apply (autoref (keep_goal))
  done

subsection ‹Generalized Buchi Graphs›

consts
  i_gbg_eext :: "interface  interface  interface"

abbreviation "i_gbg Ie Iv  Ie,Ivii_gbg_eext,Ivii_g_ext"

context begin interpretation autoref_syn .

lemma gbg_type[autoref_itype]:
  "gbg_F ::i i_gbg Ie Iv i Ivii_setii_set"
  "gb_graph_rec_ext ::i Ivii_setii_set i Ie i Ie,Ivii_gbg_eext"
  by simp_all
end

record ('vi,'ei,'v0i,'fi) gen_gbg_impl = "('vi,'ei,'v0i) gen_g_impl" +
  gbgi_F :: 'fi

definition gen_gbg_impl_rel_eext_def_internal: 
  "gen_gbg_impl_rel_eext Rm Rf  { (
   gbgi_F = Fi, =mi , 
   gbg_F = F, =m ) 
  | Fi mi F m. 
    (Fi,F)Rf
   (mi,m)Rm
  }"

lemma gen_gbg_impl_rel_eext_def: 
  "Rm,Rfgen_gbg_impl_rel_eext = { (
   gbgi_F = Fi, =mi , 
   gbg_F = F, =m ) 
  | Fi mi F m. 
    (Fi,F)Rf
   (mi,m)Rm
  }"
  unfolding gen_gbg_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_gbg_impl_rel_sv[relator_props]: 
  "single_valued Rm; single_valued Rf 
   single_valued (Rm,Rfgen_gbg_impl_rel_eext)"
  unfolding gen_gbg_impl_rel_eext_def
  apply (rule single_valuedI)
  apply (clarsimp)
  apply (intro conjI)
  apply (rule single_valuedD[rotated], assumption+)
  apply (rule single_valuedD[rotated], assumption+)
  done

abbreviation gen_gbg_impl_rel_ext 
  :: "_  _  _  _  _  (_ × ('q,_) gb_graph_rec_scheme) set"
  where "gen_gbg_impl_rel_ext Rm Rf 
   Rm,Rfgen_gbg_impl_rel_eextgen_g_impl_rel_ext"

lemma gen_gbg_refine:
  fixes Rv Re Rv0 Rf
  assumes "TERM (Rv,Re,Rv0)"
  assumes "TERM (Rf)"
  shows
  "(gbgi_F,gbg_F) 
     Rv,Re,Rv0gen_gbg_impl_rel_ext Rm Rf  Rf"
  "(gen_gbg_impl_ext, gb_graph_rec_ext) 
     Rf  Rm  Rm,Rfgen_gbg_impl_rel_eext"
  unfolding gen_gbg_impl_rel_eext_def gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation with list of lists›

definition gbg_impl_rel_eext_internal_def: 
  "gbg_impl_rel_eext Rm Rv 
   Rm, Rvlist_set_rellist_set_relgen_gbg_impl_rel_eext"

lemma gbg_impl_rel_eext_def: 
  "Rm,Rvgbg_impl_rel_eext 
     Rm, Rvlist_set_rellist_set_relgen_gbg_impl_rel_eext"
  unfolding gbg_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of gbg_impl_rel_eext i_gbg_eext]

lemma [relator_props, simp]: 
  "single_valued Rm; single_valued Rv 
   single_valued (Rm,Rvgbg_impl_rel_eext)"
  unfolding gbg_impl_rel_eext_def by tagged_solver

lemma gbg_ls_tag: "TERM (Rvlist_set_rellist_set_rel)" .

abbreviation "gbgv_impl_rel_ext Rm Rv 
   Rm, Rvgbg_impl_rel_eext, Rvfrgv_impl_rel_ext"

abbreviation "gbg_impl_rel_ext Rm Rv 
   Rm, Rvgbg_impl_rel_eext, Rvg_impl_rel_ext"

context fixes Rv :: "('vi×'v) set" begin
lemmas [autoref_rules] = gen_gbg_refine[
  OF frgv_tag[of Rv] gbg_ls_tag[of Rv], 
  folded frgv_impl_rel_ext_def gbg_impl_rel_eext_def]

lemmas [autoref_rules] = gen_gbg_refine[
  OF g_tag[of Rv] gbg_ls_tag[of Rv], 
  folded g_impl_rel_ext_def gbg_impl_rel_eext_def]
end

schematic_goal "(?c::?'c, 
    λG x. if gbg_F G = {} then (g_E G `` {x}) else {} 
  )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) F. 
     g_V = {}, g_E = E, g_V0 = V0, gbg_F = F )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) F. 
     g_V = UNIV, g_E = E, g_V0 = V0, gbg_F = insert {} F )?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?c::?'c, it_to_sorted_list (λ_ _. True) {1,2::nat} )?R"
  apply (autoref (keep_goal))
  done

subsection ‹GBAs›

consts
  i_gba_eext :: "interface  interface  interface  interface"

abbreviation "i_gba Ie Iv Il 
   Ie,Iv,Ilii_gba_eext,Ivii_gbg_eext,Ivii_g_ext"
context begin interpretation autoref_syn .

lemma gba_type[autoref_itype]:
  "gba_L ::i i_gba Ie Iv Il i (Iv i Il i i_bool)"
  "gba_rec_ext ::i (Iv i Il i i_bool) i Ie i Ie,Iv,Ilii_gba_eext"
  by simp_all
end

record ('vi,'ei,'v0i,'acci,'Li) gen_gba_impl = 
  "('vi,'ei,'v0i,'acci)gen_gbg_impl" +
  gbai_L :: "'Li"

definition gen_gba_impl_rel_eext_def_internal: 
  "gen_gba_impl_rel_eext Rm Rl   { (
   gbai_L = Li, =mi , 
   gba_L = L, =m ) 
  | Li mi L m. 
    (Li,L)Rl
   (mi,m)Rm
  }"

lemma gen_gba_impl_rel_eext_def: 
  "Rm,Rlgen_gba_impl_rel_eext = { (
   gbai_L = Li, =mi , 
   gba_L = L, =m ) 
  | Li mi L m. 
    (Li,L)Rl
   (mi,m)Rm
  }"
  unfolding gen_gba_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_gba_impl_rel_sv[relator_props]: 
  "single_valued Rl; single_valued Rm 
   single_valued (Rm,Rlgen_gba_impl_rel_eext)"
  unfolding gen_gba_impl_rel_eext_def
  apply (rule single_valuedI)
  apply (clarsimp)
  apply (intro conjI)
  apply (rule single_valuedD[rotated], assumption+)
  apply (rule single_valuedD[rotated], assumption+)
  done

abbreviation gen_gba_impl_rel_ext 
  :: "_  _  _  _  _  _  (_ × ('a,'b,'c) gba_rec_scheme) set"
  where "gen_gba_impl_rel_ext Rm Rl 
     gen_gbg_impl_rel_ext (Rm,Rlgen_gba_impl_rel_eext)"

lemma gen_gba_refine:
  fixes Rv Re Rv0 Racc Rl
  assumes "TERM (Rv,Re,Rv0)"
  assumes "TERM (Racc)"
  assumes "TERM (Rl)"
  shows
  "(gbai_L,gba_L) 
     Rv,Re,Rv0gen_gba_impl_rel_ext Rm Rl Racc  Rl"
  "(gen_gba_impl_ext, gba_rec_ext) 
     Rl  Rm  Rm,Rlgen_gba_impl_rel_eext"
  unfolding gen_gba_impl_rel_eext_def gen_gbg_impl_rel_eext_def
    gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation as function›
definition gba_impl_rel_eext_internal_def: 
  "gba_impl_rel_eext Rm Rv Rl  Rm, Rv  Rl  bool_relgen_gba_impl_rel_eext"

lemma gba_impl_rel_eext_def: 
  "Rm,Rv,Rlgba_impl_rel_eext  Rm, Rv  Rl  bool_relgen_gba_impl_rel_eext"
  unfolding gba_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of gba_impl_rel_eext i_gba_eext]

lemma [relator_props, simp]: 
  "Range Rv = UNIV; single_valued Rm; Range Rl = UNIV 
   single_valued (Rm,Rv,Rlgba_impl_rel_eext)"
  unfolding gba_impl_rel_eext_def by tagged_solver

lemma gba_f_tag: "TERM (Rv  Rl  bool_rel)" .

abbreviation "gbav_impl_rel_ext Rm Rv Rl
   gbgv_impl_rel_ext (Rm, Rv, Rlgba_impl_rel_eext) Rv"

abbreviation "gba_impl_rel_ext Rm Rv Rl 
   gbg_impl_rel_ext (Rm, Rv, Rlgba_impl_rel_eext) Rv"

context 
  fixes Rv :: "('vi×'v) set" 
  fixes Rl :: "('Li×'l) set"
begin
lemmas [autoref_rules] = gen_gba_refine[
  OF frgv_tag[of Rv] gbg_ls_tag[of Rv] gba_f_tag[of Rv Rl], 
  folded frgv_impl_rel_ext_def gbg_impl_rel_eext_def gba_impl_rel_eext_def]

lemmas [autoref_rules] = gen_gba_refine[
  OF g_tag[of Rv] gbg_ls_tag[of Rv] gba_f_tag[of Rv Rl], 
  folded g_impl_rel_ext_def gbg_impl_rel_eext_def gba_impl_rel_eext_def]
end

thm autoref_itype

schematic_goal 
  "(?c::?'c, λG x l. if gba_L G x l then (g_E G `` {x}) else {} )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) F L. 
   g_V = UNIV, g_E = E, g_V0 = V0, 
    gbg_F = F, gba_L = L 
  )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) F L. 
   g_V = V0, g_E = E, g_V0 = V0, 
    gbg_F = F, gba_L = L 
  )?R"
  apply (autoref (keep_goal))
  done

subsection ‹Buchi Graphs›

consts
  i_bg_eext :: "interface  interface  interface"

abbreviation "i_bg Ie Iv  Ie,Ivii_bg_eext,Ivii_g_ext"

context begin interpretation autoref_syn .
lemma bg_type[autoref_itype]:
  "bg_F ::i i_bg Ie Iv i Ivii_set"
  "gb_graph_rec_ext ::i Ivii_setii_set i Ie i Ie,Ivii_bg_eext"
  by simp_all
end

record ('vi,'ei,'v0i,'fi) gen_bg_impl = "('vi,'ei,'v0i) gen_g_impl" +
  bgi_F :: 'fi

definition gen_bg_impl_rel_eext_def_internal: 
  "gen_bg_impl_rel_eext Rm Rf  { (
   bgi_F = Fi, =mi , 
   bg_F = F, =m ) 
  | Fi mi F m. 
    (Fi,F)Rf
   (mi,m)Rm
  }"

lemma gen_bg_impl_rel_eext_def: 
  "Rm,Rfgen_bg_impl_rel_eext = { (
   bgi_F = Fi, =mi , 
   bg_F = F, =m ) 
  | Fi mi F m. 
    (Fi,F)Rf
   (mi,m)Rm
  }"
  unfolding gen_bg_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_bg_impl_rel_sv[relator_props]: 
  "single_valued Rm; single_valued Rf 
   single_valued (Rm,Rfgen_bg_impl_rel_eext)"
  unfolding gen_bg_impl_rel_eext_def
  apply (rule single_valuedI)
  apply (clarsimp)
  apply (intro conjI)
  apply (rule single_valuedD[rotated], assumption+)
  apply (rule single_valuedD[rotated], assumption+)
  done

abbreviation gen_bg_impl_rel_ext 
  :: "_  _  _  _  _  (_ × ('q,_) b_graph_rec_scheme) set"
  where "gen_bg_impl_rel_ext Rm Rf 
   Rm,Rfgen_bg_impl_rel_eextgen_g_impl_rel_ext"

lemma gen_bg_refine:
  fixes Rv Re Rv0 Rf
  assumes "TERM (Rv,Re,Rv0)"
  assumes "TERM (Rf)"
  shows
  "(bgi_F,bg_F) 
     Rv,Re,Rv0gen_bg_impl_rel_ext Rm Rf  Rf"
  "(gen_bg_impl_ext, b_graph_rec_ext) 
     Rf  Rm  Rm,Rfgen_bg_impl_rel_eext"
  unfolding gen_bg_impl_rel_eext_def gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation with Characteristic Functions›

definition bg_impl_rel_eext_internal_def: 
  "bg_impl_rel_eext Rm Rv 
   Rm, Rvfun_set_relgen_bg_impl_rel_eext"

lemma bg_impl_rel_eext_def: 
  "Rm,Rvbg_impl_rel_eext 
     Rm, Rvfun_set_relgen_bg_impl_rel_eext"
  unfolding bg_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of bg_impl_rel_eext i_bg_eext]

lemma [relator_props, simp]: 
  "single_valued Rm; single_valued Rv; Range Rv = UNIV 
   single_valued (Rm,Rvbg_impl_rel_eext)"
  unfolding bg_impl_rel_eext_def by tagged_solver

lemma bg_fs_tag: "TERM (Rvfun_set_rel)" .

abbreviation "bgv_impl_rel_ext Rm Rv 
   Rm, Rvbg_impl_rel_eext, Rvfrgv_impl_rel_ext"

abbreviation "bg_impl_rel_ext Rm Rv 
   Rm, Rvbg_impl_rel_eext, Rvg_impl_rel_ext"

context fixes Rv :: "('vi×'v) set" begin
lemmas [autoref_rules] = gen_bg_refine[
  OF frgv_tag[of Rv] bg_fs_tag[of Rv], 
  folded frgv_impl_rel_ext_def bg_impl_rel_eext_def]

lemmas [autoref_rules] = gen_bg_refine[
  OF g_tag[of Rv] bg_fs_tag[of Rv], 
  folded g_impl_rel_ext_def bg_impl_rel_eext_def]
end

schematic_goal "(?c::?'c, 
    λG x. if x  bg_F G then (g_E G `` {x}) else {} 
  )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) F. 
     g_V = {}, g_E = E, g_V0 = V0, bg_F = F )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) F. 
     g_V = UNIV, g_E = E, g_V0 = V0, bg_F = F )?R"
  apply (autoref (keep_goal))
  done

subsection ‹System Automata›

consts
  i_sa_eext :: "interface  interface  interface  interface"

abbreviation "i_sa Ie Iv Il  Ie,Iv,Ilii_sa_eext,Ivii_g_ext"

context begin interpretation autoref_syn .
term sa_L
lemma sa_type[autoref_itype]:
  "sa_L ::i i_sa Ie Iv Il i Iv i Il"
  "sa_rec_ext ::i (Iv i Il) i Ie i Ie,Iv,Ilii_sa_eext"
  by simp_all
end

record ('vi,'ei,'v0i,'li) gen_sa_impl = "('vi,'ei,'v0i) gen_g_impl" +
  sai_L :: 'li

definition gen_sa_impl_rel_eext_def_internal: 
  "gen_sa_impl_rel_eext Rm Rl  { (
   sai_L = Li, =mi , 
   sa_L = L, =m ) 
  | Li mi L m. 
    (Li,L)Rl
   (mi,m)Rm
  }"

lemma gen_sa_impl_rel_eext_def: 
  "Rm,Rlgen_sa_impl_rel_eext = { (
   sai_L = Li, =mi , 
   sa_L = L, =m ) 
  | Li mi L m. 
    (Li,L)Rl
   (mi,m)Rm
  }"
  unfolding gen_sa_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_sa_impl_rel_sv[relator_props]: 
  "single_valued Rm; single_valued Rf 
   single_valued (Rm,Rfgen_sa_impl_rel_eext)"
  unfolding gen_sa_impl_rel_eext_def
  apply (rule single_valuedI)
  apply (clarsimp)
  apply (intro conjI)
  apply (rule single_valuedD[rotated], assumption+)
  apply (rule single_valuedD[rotated], assumption+)
  done

abbreviation gen_sa_impl_rel_ext 
  :: "_  _  _  _  _  (_ × ('q,'l,_) sa_rec_scheme) set"
  where "gen_sa_impl_rel_ext Rm Rf 
   Rm,Rfgen_sa_impl_rel_eextgen_g_impl_rel_ext"

lemma gen_sa_refine:
  fixes Rv Re Rv0
  assumes "TERM (Rv,Re,Rv0)"
  assumes "TERM (Rl)"
  shows
  "(sai_L,sa_L) 
     Rv,Re,Rv0gen_sa_impl_rel_ext Rm Rl  Rl"
  "(gen_sa_impl_ext, sa_rec_ext) 
     Rl  Rm  Rm,Rlgen_sa_impl_rel_eext"
  unfolding gen_sa_impl_rel_eext_def gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation with Function›

definition sa_impl_rel_eext_internal_def: 
  "sa_impl_rel_eext Rm Rv Rl
   Rm, RvRlgen_sa_impl_rel_eext"

lemma sa_impl_rel_eext_def: 
  "Rm,Rv,Rlsa_impl_rel_eext 
     Rm, RvRlgen_sa_impl_rel_eext"
  unfolding sa_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of sa_impl_rel_eext i_sa_eext]

lemma [relator_props, simp]: 
  "single_valued Rm; single_valued Rl; Range Rv = UNIV 
   single_valued (Rm,Rv,Rlsa_impl_rel_eext)"
  unfolding sa_impl_rel_eext_def by tagged_solver

lemma sa_f_tag: "TERM (RvRl)" .

abbreviation "sav_impl_rel_ext Rm Rv Rl 
   Rm, Rv, Rlsa_impl_rel_eext, Rvfrgv_impl_rel_ext"

abbreviation "sa_impl_rel_ext Rm Rv Rl 
   Rm, Rv, Rlsa_impl_rel_eext, Rvg_impl_rel_ext"

type_synonym ('v,'l,'m) sav_impl_scheme = 
  "('v,  sai_L :: 'v  'l , ::'m  ) frgv_impl_scheme"

type_synonym ('v,'l,'m) sa_impl_scheme = 
  "('v,  sai_L :: 'v  'l , ::'m  ) g_impl_scheme"

context fixes Rv :: "('vi×'v) set" begin
lemmas [autoref_rules] = gen_sa_refine[
  OF frgv_tag[of Rv] sa_f_tag[of Rv], 
  folded frgv_impl_rel_ext_def sa_impl_rel_eext_def]

lemmas [autoref_rules] = gen_sa_refine[
  OF g_tag[of Rv] sa_f_tag[of Rv], 
  folded g_impl_rel_ext_def sa_impl_rel_eext_def]
end

schematic_goal "(?c::?'c, 
    λG x l. if sa_L G x = l then (g_E G `` {x}) else {} 
  )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) L. 
     g_V = {}, g_E = E, g_V0 = V0, sa_L = L )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) L. 
     g_V = UNIV, g_E = E, g_V0 = V0, sa_L = L )?R"
  apply (autoref (keep_goal))
  done

subsection ‹Index Conversion›

schematic_goal gbg_to_idx_ext_impl_aux:
  fixes Re and Rv :: "('qi × 'q) set"
  assumes [autoref_ga_rules]: "is_bounded_hashcode Rv eq bhc"
  assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('qi) (def_size)"
  shows "(?c, gbg_to_idx_ext :: _  ('q, _) gb_graph_rec_scheme  _)
    (gbgv_impl_rel_ext Re Rv  Ri) 
     gbgv_impl_rel_ext Re Rv 
     igbgv_impl_rel_ext Ri Rvnres_rel"
  unfolding gbg_to_idx_ext_def[abs_def] F_to_idx_impl_def mk_acc_impl_def
  using [[autoref_trace_failed_id]]
  apply (autoref (keep_goal))
  done
concrete_definition gbg_to_idx_ext_impl 
  for eq bhc def_size uses gbg_to_idx_ext_impl_aux

lemmas [autoref_rules] = 
  gbg_to_idx_ext_impl.refine[ 
  OF SIDE_GEN_ALGO_D SIDE_GEN_ALGO_D]

schematic_goal gbg_to_idx_ext_code_aux: 
  "RETURN ?c  gbg_to_idx_ext_impl eq bhc def_size ecnv G"
  unfolding gbg_to_idx_ext_impl_def
  by (refine_transfer)
concrete_definition gbg_to_idx_ext_code 
  for eq bhc ecnv G uses gbg_to_idx_ext_code_aux
lemmas [refine_transfer] = gbg_to_idx_ext_code.refine

term ahm_rel

context begin interpretation autoref_syn .
  lemma [autoref_op_pat]: "gba_to_idx_ext ecnv  OP gba_to_idx_ext $ ecnv" by simp
end

schematic_goal gba_to_idx_ext_impl_aux:
  fixes Re and Rv :: "('qi × 'q) set"
  assumes [autoref_ga_rules]: "is_bounded_hashcode Rv eq bhc"
  assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('qi) (def_size)"
  shows "(?c, gba_to_idx_ext :: _  ('q, 'l, _) gba_rec_scheme  _)
    (gbav_impl_rel_ext Re Rv RlRi) 
     gbav_impl_rel_ext Re Rv Rl 
     igbav_impl_rel_ext Ri Rv Rlnres_rel"
  using [[autoref_trace_failed_id]] unfolding ti_Lcnv_def[abs_def]
  apply (autoref (keep_goal))
  done
concrete_definition gba_to_idx_ext_impl for eq bhc uses gba_to_idx_ext_impl_aux
lemmas [autoref_rules] = 
  gba_to_idx_ext_impl.refine[OF SIDE_GEN_ALGO_D SIDE_GEN_ALGO_D]

schematic_goal gba_to_idx_ext_code_aux: 
  "RETURN ?c  gba_to_idx_ext_impl eq bhc def_size ecnv G"
  unfolding gba_to_idx_ext_impl_def
  by (refine_transfer)
concrete_definition gba_to_idx_ext_code for ecnv G uses gba_to_idx_ext_code_aux
lemmas [refine_transfer] = gba_to_idx_ext_code.refine

subsection ‹Degeneralization›

context igb_graph begin

lemma degen_impl_aux_alt: "degeneralize_ext ecnv = (
      if num_acc = 0 then 
        g_V = Collect (λ(q,x). x=0  qV),
        g_E= E_of_succ (λ(q,x). if x=0 then (λq'. (q',0))`succ_of_E E q else {}),
        g_V0 = (λq'. (q',0))`V0, 
        bg_F = Collect (λ(q,x). x=0  qV),
         = ecnv G
      
      else 
        g_V = Collect (λ(q,x). x<num_acc  qV),
        g_E = E_of_succ (λ(q,i). 
          if i<num_acc then
            let
              i' = if i  acc q then (i + 1) mod num_acc else i
            in (λq'. (q',i'))`succ_of_E E q
          else {}
        ),
        g_V0 = (λq'. (q',0))`V0,
        bg_F = Collect (λ(q,x). x=0  0acc q),
         = ecnv G
      )"
  unfolding degeneralize_ext_def
  apply (cases "num_acc = 0")
  apply simp_all
  apply (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm) []
  apply (fastforce simp: E_of_succ_def succ_of_E_def split: if_split_asm) []
  done

schematic_goal degeneralize_ext_impl_aux:
  fixes Re Rv
  assumes [autoref_rules]: "(Gi,G)  igbg_impl_rel_ext Re Rv"
  shows "(?c, degeneralize_ext) 
   (igbg_impl_rel_ext Re Rv  Re')  bg_impl_rel_ext Re' (Rv ×r nat_rel)"
  unfolding degen_impl_aux_alt[abs_def]
  using [[autoref_trace_failed_id]]
  apply (autoref (keep_goal))
  done

end

definition [simp]: 
  "op_igb_graph_degeneralize_ext ecnv G  igb_graph.degeneralize_ext G ecnv"

lemma [autoref_op_pat]: 
  "igb_graph.degeneralize_ext  λG ecnv. op_igb_graph_degeneralize_ext ecnv G"
  by simp

thm igb_graph.degeneralize_ext_impl_aux[param_fo]
concrete_definition degeneralize_ext_impl
  uses igb_graph.degeneralize_ext_impl_aux[param_fo]

thm degeneralize_ext_impl.refine

context begin interpretation autoref_syn .
lemma [autoref_rules]:
  fixes Re
  assumes "SIDE_PRECOND (igb_graph G)"
  assumes CNVR: "(ecnvi,ecnv)  (igbg_impl_rel_ext Re Rv  Re')"
  assumes GR: "(Gi,G)igbg_impl_rel_ext Re Rv"
  shows "(degeneralize_ext_impl Gi ecnvi, 
    (OP op_igb_graph_degeneralize_ext 
       ::: (igbg_impl_rel_ext Re Rv  Re')  igbg_impl_rel_ext Re Rv 
         bg_impl_rel_ext Re' (Rv ×r nat_rel) )$ecnv$G ) 
   bg_impl_rel_ext Re' (Rv ×r nat_rel)"
proof -
  from assms have A: "igb_graph G" by simp

  show ?thesis
    apply simp
    using degeneralize_ext_impl.refine[OF A GR CNVR]
    .
qed

end
thm autoref_itype(1)

schematic_goal
  assumes [simp]: "igb_graph G"
  assumes [autoref_rules]: "(Gi,G)igbg_impl_rel_ext unit_rel nat_rel"
  shows "(?c::?'c, igb_graph.degeneralize_ext G (λ_. ()))  ?R"
  apply (autoref (keep_goal))
  done

subsection ‹Product Construction›

context igba_sys_prod_precond begin

lemma prod_impl_aux_alt:
  "prod = (
    g_V = Collect (λ(q,s). q  igba.V  s  sa.V),
    g_E = E_of_succ (λ(q,s). 
      if igba.L q (sa.L s) then     
        succ_of_E (igba.E) q × succ_of_E sa.E s
      else
        {}
    ),
    g_V0 = igba.V0 × sa.V0,
    igbg_num_acc = igba.num_acc,
    igbg_acc = λ(q,s). if ssa.V then igba.acc q else {}
  )"
  unfolding prod_def
  apply (auto simp: succ_of_E_def E_of_succ_def split: if_split_asm)
  done

schematic_goal prod_impl_aux:
  fixes Re
  (*assumes [autoref_rules]: "(eqq,(=)) ∈ Rq → Rq → bool_rel"
  assumes [autoref_rules]: "(eqs,(=)) ∈ Rs → Rs → bool_rel"*)
  assumes [autoref_rules]: "(Gi,G)  igba_impl_rel_ext Re Rq Rl"
  assumes [autoref_rules]: "(Si,S)  sa_impl_rel_ext Re2 Rs Rl"
  shows "(?c, prod)  igbg_impl_rel_ext unit_rel (Rq ×r Rs)"
  unfolding prod_impl_aux_alt[abs_def]
  apply (autoref (keep_goal))
  done

end


definition [simp]: "op_igba_sys_prod  igba_sys_prod_precond.prod"

lemma [autoref_op_pat]: 
  "igba_sys_prod_precond.prod  op_igba_sys_prod"
  by simp

thm igba_sys_prod_precond.prod_impl_aux[param_fo]
concrete_definition igba_sys_prod_impl
  uses igba_sys_prod_precond.prod_impl_aux[param_fo]

thm igba_sys_prod_impl.refine

context begin interpretation autoref_syn .
lemma [autoref_rules]:
  fixes Re
  assumes "SIDE_PRECOND (igba G)"
  assumes "SIDE_PRECOND (sa S)"
  assumes GR: "(Gi,G)igba_impl_rel_ext unit_rel Rq Rl"
  assumes SR: "(Si,S)sa_impl_rel_ext unit_rel Rs Rl"
  shows "(igba_sys_prod_impl Gi Si, 
    (OP op_igba_sys_prod 
       :::  igba_impl_rel_ext unit_rel Rq Rl
         sa_impl_rel_ext unit_rel Rs Rl
         igbg_impl_rel_ext unit_rel (Rq ×r Rs) )$G$S ) 
   igbg_impl_rel_ext unit_rel (Rq ×r Rs)"
proof -
  from assms interpret igba: igba G + sa: sa S by simp_all
  have A: "igba_sys_prod_precond G S" by unfold_locales

  show ?thesis
    apply simp
    using igba_sys_prod_impl.refine[OF A GR SR]
    .
qed

end

schematic_goal
  assumes [simp]: "igba G" "sa S"
  assumes [autoref_rules]: "(Gi,G)igba_impl_rel_ext unit_rel Rq Rl"
  assumes [autoref_rules]: "(Si,S)sa_impl_rel_ext unit_rel Rs Rl"
  shows "(?c::?'c,igba_sys_prod_precond.prod G S)?R"
  apply (autoref (keep_goal))
  done

end