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,Iv⟩⇩ii_igbg_eext,Iv⟩⇩ii_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_nat⟩⇩ii_set"
  "igb_graph_rec_ext
    ::⇩i i_nat →⇩i (Iv →⇩i ⟨i_nat⟩⇩ii_set) →⇩i Ie →⇩i ⟨Ie,Iv⟩⇩ii_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,Racc⟩gen_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,Racc⟩gen_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,Racc⟩gen_igbg_impl_rel_eext⟩gen_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,Rv0⟩gen_igbg_impl_rel_ext Rm Racc → nat_rel"
  "(igbgi_acc,igbg_acc) 
    ∈ ⟨Rv,Re,Rv0⟩gen_igbg_impl_rel_ext Rm Racc → Racc"
  "(gen_igbg_impl_ext, igb_graph_rec_ext) 
    ∈ nat_rel → Racc → Rm → ⟨Rm,Racc⟩gen_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_rel⟩bs_set_rel⟩gen_igbg_impl_rel_eext"

lemma igbg_impl_rel_eext_def: 
  "⟨Rm,Rv⟩igbg_impl_rel_eext ≡ ⟨Rm, Rv → ⟨nat_rel⟩bs_set_rel⟩gen_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,Rv⟩igbg_impl_rel_eext)"
  unfolding igbg_impl_rel_eext_def by tagged_solver

lemma g_tag: "TERM (⟨Rv⟩fun_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel)" .
lemma frgv_tag: "TERM (⟨Rv⟩list_set_rel,⟨Rv⟩slg_rel,⟨Rv⟩list_set_rel)" .
lemma igbg_bs_tag: "TERM (Rv → ⟨nat_rel⟩bs_set_rel)" .

abbreviation "igbgv_impl_rel_ext Rm Rv 
  ≡ ⟨⟨Rm, Rv⟩igbg_impl_rel_eext, Rv⟩frgv_impl_rel_ext"

abbreviation "igbg_impl_rel_ext Rm Rv 
  ≡ ⟨⟨Rm, Rv⟩igbg_impl_rel_eext, Rv⟩g_impl_rel_ext"

type_synonym ('v,'m) igbgv_impl_scheme = 
  "('v, ⦇ igbgi_num_acc::nat, igbgi_acc::'v⇒integer, …::'m  ⦈) 
    frgv_impl_scheme"
type_synonym ('v,'m) igbg_impl_scheme = 
  "('v, ⦇ igbgi_num_acc::nat, igbgi_acc::'v⇒integer, …::'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 ∧ 1∈igbg_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 ⦈
  )∈⟨R⟩list_set_rel → ⟨R⟩slg_rel → nat_rel → (R → ⟨nat_rel⟩bs_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 ⦈
  )∈⟨R⟩list_set_rel → ⟨R⟩slg_rel → nat_rel → (R → ⟨nat_rel⟩bs_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,Il⟩⇩ii_igba_eext,Iv⟩⇩ii_igbg_eext,Iv⟩⇩ii_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,Il⟩⇩ii_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,Rl⟩gen_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,Rl⟩gen_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,Rl⟩gen_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,Rv0⟩gen_igba_impl_rel_ext Rm Rl Racc → Rl"
  "(gen_igba_impl_ext, igba_rec_ext) 
    ∈ Rl → Rm → ⟨Rm,Rl⟩gen_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_rel⟩gen_igba_impl_rel_eext"

lemma igba_impl_rel_eext_def: 
  "⟨Rm,Rv,Rl⟩igba_impl_rel_eext ≡ ⟨Rm, Rv → Rl → bool_rel⟩gen_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,Rl⟩igba_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, Rl⟩igba_impl_rel_eext) Rv"

abbreviation "igba_impl_rel_ext Rm Rv Rl 
  ≡ igbg_impl_rel_ext (⟨Rm, Rv, Rl⟩igba_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,Iv⟩⇩ii_gbg_eext,Iv⟩⇩ii_g_ext"

context begin interpretation autoref_syn .

lemma gbg_type[autoref_itype]:
  "gbg_F ::⇩i i_gbg Ie Iv →⇩i ⟨⟨Iv⟩⇩ii_set⟩⇩ii_set"
  "gb_graph_rec_ext ::⇩i ⟨⟨Iv⟩⇩ii_set⟩⇩ii_set →⇩i Ie →⇩i ⟨Ie,Iv⟩⇩ii_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,Rf⟩gen_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,Rf⟩gen_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,Rf⟩gen_gbg_impl_rel_eext⟩gen_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,Rv0⟩gen_gbg_impl_rel_ext Rm Rf → Rf"
  "(gen_gbg_impl_ext, gb_graph_rec_ext) 
    ∈ Rf → Rm → ⟨Rm,Rf⟩gen_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, ⟨⟨Rv⟩list_set_rel⟩list_set_rel⟩gen_gbg_impl_rel_eext"

lemma gbg_impl_rel_eext_def: 
  "⟨Rm,Rv⟩gbg_impl_rel_eext 
    ≡ ⟨Rm, ⟨⟨Rv⟩list_set_rel⟩list_set_rel⟩gen_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,Rv⟩gbg_impl_rel_eext)"
  unfolding gbg_impl_rel_eext_def by tagged_solver

lemma gbg_ls_tag: "TERM (⟨⟨Rv⟩list_set_rel⟩list_set_rel)" .

abbreviation "gbgv_impl_rel_ext Rm Rv 
  ≡ ⟨⟨Rm, Rv⟩gbg_impl_rel_eext, Rv⟩frgv_impl_rel_ext"

abbreviation "gbg_impl_rel_ext Rm Rv 
  ≡ ⟨⟨Rm, Rv⟩gbg_impl_rel_eext, Rv⟩g_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,Il⟩⇩ii_gba_eext,Iv⟩⇩ii_gbg_eext,Iv⟩⇩ii_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,Il⟩⇩ii_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,Rl⟩gen_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,Rl⟩gen_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,Rl⟩gen_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,Rv0⟩gen_gba_impl_rel_ext Rm Rl Racc → Rl"
  "(gen_gba_impl_ext, gba_rec_ext) 
    ∈ Rl → Rm → ⟨Rm,Rl⟩gen_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_rel⟩gen_gba_impl_rel_eext"

lemma gba_impl_rel_eext_def: 
  "⟨Rm,Rv,Rl⟩gba_impl_rel_eext ≡ ⟨Rm, Rv → Rl → bool_rel⟩gen_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,Rl⟩gba_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, Rl⟩gba_impl_rel_eext) Rv"

abbreviation "gba_impl_rel_ext Rm Rv Rl 
  ≡ gbg_impl_rel_ext (⟨Rm, Rv, Rl⟩gba_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,Iv⟩⇩ii_bg_eext,Iv⟩⇩ii_g_ext"

context begin interpretation autoref_syn .
lemma bg_type[autoref_itype]:
  "bg_F ::⇩i i_bg Ie Iv →⇩i ⟨Iv⟩⇩ii_set"
  "gb_graph_rec_ext ::⇩i ⟨⟨Iv⟩⇩ii_set⟩⇩ii_set →⇩i Ie →⇩i ⟨Ie,Iv⟩⇩ii_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,Rf⟩gen_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,Rf⟩gen_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,Rf⟩gen_bg_impl_rel_eext⟩gen_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,Rv0⟩gen_bg_impl_rel_ext Rm Rf → Rf"
  "(gen_bg_impl_ext, b_graph_rec_ext) 
    ∈ Rf → Rm → ⟨Rm,Rf⟩gen_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, ⟨Rv⟩fun_set_rel⟩gen_bg_impl_rel_eext"

lemma bg_impl_rel_eext_def: 
  "⟨Rm,Rv⟩bg_impl_rel_eext 
    ≡ ⟨Rm, ⟨Rv⟩fun_set_rel⟩gen_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,Rv⟩bg_impl_rel_eext)"
  unfolding bg_impl_rel_eext_def by tagged_solver

lemma bg_fs_tag: "TERM (⟨Rv⟩fun_set_rel)" .

abbreviation "bgv_impl_rel_ext Rm Rv 
  ≡ ⟨⟨Rm, Rv⟩bg_impl_rel_eext, Rv⟩frgv_impl_rel_ext"

abbreviation "bg_impl_rel_ext Rm Rv 
  ≡ ⟨⟨Rm, Rv⟩bg_impl_rel_eext, Rv⟩g_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,Il⟩⇩ii_sa_eext,Iv⟩⇩ii_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,Il⟩⇩ii_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,Rl⟩gen_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,Rf⟩gen_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,Rf⟩gen_sa_impl_rel_eext⟩gen_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,Rv0⟩gen_sa_impl_rel_ext Rm Rl → Rl"
  "(gen_sa_impl_ext, sa_rec_ext) 
    ∈ Rl → Rm → ⟨Rm,Rl⟩gen_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, Rv→Rl⟩gen_sa_impl_rel_eext"

lemma sa_impl_rel_eext_def: 
  "⟨Rm,Rv,Rl⟩sa_impl_rel_eext 
    ≡ ⟨Rm, Rv→Rl⟩gen_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,Rl⟩sa_impl_rel_eext)"
  unfolding sa_impl_rel_eext_def by tagged_solver

lemma sa_f_tag: "TERM (Rv→Rl)" .

abbreviation "sav_impl_rel_ext Rm Rv Rl 
  ≡ ⟨⟨Rm, Rv, Rl⟩sa_impl_rel_eext, Rv⟩frgv_impl_rel_ext"

abbreviation "sa_impl_rel_ext Rm Rv Rl 
  ≡ ⟨⟨Rm, Rv, Rl⟩sa_impl_rel_eext, Rv⟩g_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 Rv⟩nres_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 Rl→Ri) 
    → gbav_impl_rel_ext Re Rv Rl 
    → ⟨igbav_impl_rel_ext Ri Rv Rl⟩nres_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 ∧ q∈V),
        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 ∧ q∈V),
        … = ecnv G
      ⦈
      else ⦇
        g_V = Collect (λ(q,x). x<num_acc ∧ q∈V),
        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 ∧ 0∈acc 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 s∈sa.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