Theory Composition

(* Author: Andreas Lochbihler, ETH Zurich
   Author: Joshua Schneider, ETH Zurich *)

section ‹Simple operations: demotion, merging, composition›

theory Composition imports
  Axiomatised_BNF_CC
begin

text ‹
  We illustrate the composition of \BNFCC{}s with one example for each kind of parameters
  (live/co-/contravariant/fixed). We do not show demotion and merging in isolation, as the
  examples for composition use these operations, too.
›

subsection ‹Composition in a live position›

type_synonym
  ('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'co4, 'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGl =
    "(('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f1) G,
    'l1, 'l3, 'co1, 'co3, 'co4, 'contra1, 'contra3, 'contra4, 'f2) F"

text ‹The type variables @{typ 'l1}, @{typ 'co1} and @{typ 'contra1} have each been merged.›

definition "rel_FGl L1 L2 L3 Co1 Co2 Co3 Co4 Contra1 Contra2 Contra3 Contra4 =
  rel_F (rel_G L1 L2 Co1 Co2 Contra1 Contra2) L1 L3 Co1 Co3 Co4 Contra1 Contra3 Contra4"

definition "map_FGl l1 l2 l3 co1 co2 co3 co4 contra1 contra2 contra3 contra4 =
  map_F (map_G l1 l2 co1 co2 contra1 contra2) l1 l3 co1 co3 co4 contra1 contra3 contra4"

lemma rel_FGl_mono:
  "⟦ L1 ≤ L1'; L2 ≤ L2'; L3 ≤ L3'; Co1 ≤ Co1'; Co2 ≤ Co2'; Co3 ≤ Co3'; Co4 ≤ Co4';
     Contra1' ≤ Contra1; Contra2' ≤ Contra2; Contra3' ≤ Contra3; Contra4' ≤ Contra4 ⟧ ⟹
  rel_FGl L1 L2 L3 Co1 Co2 Co3 Co4 Contra1 Contra2 Contra3 Contra4 ≤
  rel_FGl L1' L2' L3' Co1' Co2' Co3' Co4' Contra1' Contra2' Contra3' Contra4'"
  unfolding rel_FGl_def
  apply (rule rel_F_mono)
          apply (rule rel_G_mono)
               apply (assumption)+
  done

lemma rel_FGl_eq: "rel_FGl (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) = (=)"
  unfolding rel_FGl_def by (simp add: rel_F_eq rel_G_eq)

lemma rel_FGl_conversep:
  "rel_FGl L1¯¯ L2¯¯ L3¯¯ Co1¯¯ Co2¯¯ Co3¯¯ Co4¯¯ Contra1¯¯ Contra2¯¯ Contra3¯¯ Contra4¯¯ =
  (rel_FGl L1 L2 L3 Co1 Co2 Co3 Co4 Contra1 Contra2 Contra3 Contra4)¯¯"
  unfolding rel_FGl_def by (simp add: rel_F_conversep rel_G_conversep)

lemma map_FGl_id0: "map_FGl id id id id id id id id id id id = id"
  unfolding map_FGl_def by (simp add: map_F_id0 map_G_id0)

lemma map_FGl_comp: "map_FGl l1 l2 l3 co1 co2 co3 co4 contra1 contra2 contra3 contra4 ∘
  map_FGl l1' l2' l3' co1' co2' co3' co4' contra1' contra2' contra3' contra4' =
  map_FGl (l1 ∘ l1') (l2 ∘ l2') (l3 ∘ l3') (co1 ∘ co1') (co2 ∘ co2') (co3 ∘ co3') (co4 ∘ co4')
    (contra1' ∘ contra1) (contra2' ∘ contra2) (contra3' ∘ contra3) (contra4' ∘ contra4)"
  unfolding map_FGl_def by (simp add: map_F_comp map_G_comp)

lemma map_FGl_parametric:
  "rel_fun (rel_fun L1 L1') (rel_fun (rel_fun L2 L2') (rel_fun (rel_fun L3 L3')
  (rel_fun (rel_fun Co1 Co1') (rel_fun (rel_fun Co2 Co2')
    (rel_fun (rel_fun Co3 Co3') (rel_fun (rel_fun Co4 Co4')
  (rel_fun (rel_fun Contra1' Contra1) (rel_fun (rel_fun Contra2' Contra2)
    (rel_fun (rel_fun Contra3' Contra3) (rel_fun (rel_fun Contra4' Contra4)
  (rel_fun (rel_FGl L1 L2 L3 Co1 Co2 Co3 Co4 Contra1 Contra2 Contra3 Contra4)
  (rel_FGl L1' L2' L3' Co1' Co2' Co3' Co4' Contra1' Contra2' Contra3' Contra4'))))))))))))
  map_FGl map_FGl"
  unfolding rel_FGl_def map_FGl_def
  apply (intro rel_funI)
  apply (elim map_F_rel_cong map_G_rel_cong)
               apply (erule (2) rel_funE)+
  done

definition rel_FGl_pos_distr_cond :: "('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co1' ⇒ 'co1'' ⇒ bool) ⇒
    ('co2 ⇒ 'co2' ⇒ bool) ⇒ ('co2' ⇒ 'co2'' ⇒ bool) ⇒
    ('co3 ⇒ 'co3' ⇒ bool) ⇒ ('co3' ⇒ 'co3'' ⇒ bool) ⇒
    ('co4 ⇒ 'co4' ⇒ bool) ⇒ ('co4' ⇒ 'co4'' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra1' ⇒ 'contra1'' ⇒ bool) ⇒
    ('contra2 ⇒ 'contra2' ⇒ bool) ⇒ ('contra2' ⇒ 'contra2'' ⇒ bool) ⇒
    ('contra3 ⇒ 'contra3' ⇒ bool) ⇒ ('contra3' ⇒ 'contra3'' ⇒ bool) ⇒
    ('contra4 ⇒ 'contra4' ⇒ bool) ⇒ ('contra4' ⇒ 'contra4'' ⇒ bool) ⇒
    ('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'l3 × 'l3' × 'l3'' × 'f1 × 'f2) itself ⇒ bool"
  where
  "rel_FGl_pos_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool)
    (L2 :: 'l2 ⇒ 'l2' ⇒ bool) (L2' :: 'l2' ⇒ 'l2'' ⇒ bool)
    (L3 :: 'l3 ⇒ 'l3' ⇒ bool) (L3' :: 'l3' ⇒ 'l3'' ⇒ bool).
    (rel_FGl L1 L2 L3 Co1 Co2 Co3 Co4 Contra1 Contra2 Contra3 Contra4 ::
      (_, _, _, _, _, _, _, _, _, _, _, 'f1, 'f2) FGl ⇒ _) OO
      rel_FGl L1' L2' L3' Co1' Co2' Co3' Co4' Contra1' Contra2' Contra3' Contra4' ≤
    rel_FGl (L1 OO L1') (L2 OO L2') (L3 OO L3') (Co1 OO Co1') (Co2 OO Co2') (Co3 OO Co3') (Co4 OO Co4')
      (Contra1 OO Contra1') (Contra2 OO Contra2') (Contra3 OO Contra3') (Contra4 OO Contra4'))"

definition rel_FGl_neg_distr_cond :: "('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co1' ⇒ 'co1'' ⇒ bool) ⇒
    ('co2 ⇒ 'co2' ⇒ bool) ⇒ ('co2' ⇒ 'co2'' ⇒ bool) ⇒
    ('co3 ⇒ 'co3' ⇒ bool) ⇒ ('co3' ⇒ 'co3'' ⇒ bool) ⇒
    ('co4 ⇒ 'co4' ⇒ bool) ⇒ ('co4' ⇒ 'co4'' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra1' ⇒ 'contra1'' ⇒ bool) ⇒
    ('contra2 ⇒ 'contra2' ⇒ bool) ⇒ ('contra2' ⇒ 'contra2'' ⇒ bool) ⇒
    ('contra3 ⇒ 'contra3' ⇒ bool) ⇒ ('contra3' ⇒ 'contra3'' ⇒ bool) ⇒
    ('contra4 ⇒ 'contra4' ⇒ bool) ⇒ ('contra4' ⇒ 'contra4'' ⇒ bool) ⇒
    ('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'l3 × 'l3' × 'l3'' × 'f1 × 'f2) itself ⇒ bool"
  where
  "rel_FGl_neg_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool)
    (L2 :: 'l2 ⇒ 'l2' ⇒ bool) (L2' :: 'l2' ⇒ 'l2'' ⇒ bool)
    (L3 :: 'l3 ⇒ 'l3' ⇒ bool) (L3' :: 'l3' ⇒ 'l3'' ⇒ bool).
    rel_FGl (L1 OO L1') (L2 OO L2') (L3 OO L3')
      (Co1 OO Co1') (Co2 OO Co2') (Co3 OO Co3') (Co4 OO Co4')
      (Contra1 OO Contra1') (Contra2 OO Contra2') (Contra3 OO Contra3') (Contra4 OO Contra4') ≤
    (rel_FGl L1 L2 L3 Co1 Co2 Co3 Co4 Contra1 Contra2 Contra3 Contra4 ::
      (_, _, _, _, _, _, _, _, _, _, _, 'f1, 'f2) FGl ⇒ _) OO
      rel_FGl L1' L2' L3' Co1' Co2' Co3' Co4' Contra1' Contra2' Contra3' Contra4')"

text ‹Sufficient conditions for subdistributivity over relation composition.›

lemma rel_FGl_pos_distr_imp:
  fixes Co1 :: "'co1 ⇒ 'co1' ⇒ bool" and Co1' :: "'co1' ⇒ 'co1'' ⇒ bool"
    and Co2 :: "'co2 ⇒ 'co2' ⇒ bool" and Co2' :: "'co2' ⇒ 'co2'' ⇒ bool"
    and Contra1 :: "'contra1 ⇒ 'contra1' ⇒ bool" and Contra1' :: "'contra1' ⇒ 'contra1'' ⇒ bool"
    and Contra2 :: "'contra2 ⇒ 'contra2' ⇒ bool" and Contra2' :: "'contra2' ⇒ 'contra2'' ⇒ bool"
    and tytok_F :: "(('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f1) G ×
      ('l1', 'l2', 'co1', 'co2', 'contra1', 'contra2', 'f1) G ×
      ('l1'', 'l2'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f1) G ×
      'l1 × 'l1' × 'l1'' × 'l3 × 'l3' × 'l3'' × 'f2) itself"
    and tytok_G :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'f1) itself"
    and tytok_FGl :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'l3 × 'l3' × 'l3'' ×
      'f1 × 'f2) itself"
  assumes "rel_F_pos_distr_cond Co1 Co1' Co3 Co3' Co4 Co4'
      Contra1 Contra1' Contra3 Contra3' Contra4 Contra4' tytok_F"
    and "rel_G_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_G"
  shows "rel_FGl_pos_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' tytok_FGl"
  unfolding rel_FGl_pos_distr_cond_def rel_FGl_def
  apply (intro allI)
  apply (rule order_trans)
   apply (rule rel_F_pos_distr)
   apply (rule assms(1))
  apply (rule rel_F_mono)
          apply (rule rel_G_pos_distr)
          apply (rule assms(2))
         apply (rule order_refl)+
  done

lemma rel_FGl_neg_distr_imp:
  fixes Co1 :: "'co1 ⇒ 'co1' ⇒ bool" and Co1' :: "'co1' ⇒ 'co1'' ⇒ bool"
    and Co2 :: "'co2 ⇒ 'co2' ⇒ bool" and Co2' :: "'co2' ⇒ 'co2'' ⇒ bool"
    and Contra1 :: "'contra1 ⇒ 'contra1' ⇒ bool" and Contra1' :: "'contra1' ⇒ 'contra1'' ⇒ bool"
    and Contra2 :: "'contra2 ⇒ 'contra2' ⇒ bool" and Contra2' :: "'contra2' ⇒ 'contra2'' ⇒ bool"
    and tytok_F :: "(('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f1) G ×
      ('l1', 'l2', 'co1', 'co2', 'contra1', 'contra2', 'f1) G ×
      ('l1'', 'l2'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f1) G ×
      'l1 × 'l1' × 'l1'' × 'l3 × 'l3' × 'l3'' × 'f2) itself"
    and tytok_G :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'f1) itself"
    and tytok_FGl :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'l3 × 'l3' × 'l3'' ×
      'f1 × 'f2) itself"
  assumes "rel_F_neg_distr_cond Co1 Co1' Co3 Co3' Co4 Co4'
      Contra1 Contra1' Contra3 Contra3' Contra4 Contra4' tytok_F"
    and "rel_G_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_G"
  shows "rel_FGl_neg_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' tytok_FGl"
  unfolding rel_FGl_neg_distr_cond_def rel_FGl_def
  apply (intro allI)
  apply (rule order_trans[rotated])
   apply (rule rel_F_neg_distr)
   apply (rule assms(1))
  apply (rule rel_F_mono)
          apply (rule rel_G_neg_distr)
          apply (rule assms(2))
         apply (rule order_refl)+
  done

lemma rel_FGl_pos_distr_cond_eq:
  fixes tytok :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'l3 × 'l3' × 'l3'' ×
    'f1 × 'f2) itself"
  shows "rel_FGl_pos_distr_cond (=) (=) (=) (=) (=) (=) (=) (=)
    (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  by (rule rel_FGl_pos_distr_imp rel_F_pos_distr_cond_eq rel_G_pos_distr_cond_eq)+

lemma rel_FGl_neg_distr_cond_eq:
  fixes tytok :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'l3 × 'l3' × 'l3'' ×
    'f1 × 'f2) itself"
  shows "rel_FGl_neg_distr_cond (=) (=) (=) (=) (=) (=) (=) (=)
    (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  by (rule rel_FGl_neg_distr_imp rel_F_neg_distr_cond_eq rel_G_neg_distr_cond_eq)+

definition "rell_FGl L1 L2 L3 = rel_FGl L1 L2 L3 (=) (=) (=) (=) (=) (=) (=) (=)"
definition "mapl_FGl l1 l2 l3 = map_FGl l1 l2 l3 id id id id id id id id"

type_synonym ('co1, 'co2, 'co3, 'co4, 'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGlbd =
  "('co1, 'co3, 'co4, 'contra1, 'contra3, 'contra4, 'f2) Fbd ×
    ('co1, 'co2, 'contra1, 'contra2, 'f1) Gbd +
    ('co1, 'co3, 'co4, 'contra1, 'contra3, 'contra4, 'f2) Fbd"

definition set1_FGl :: "('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'co4,
    'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGl ⇒ 'l1 set" where
  "set1_FGl x = (⋃y∈set1_F x. set1_G y) ∪ set2_F x"

definition set2_FGl :: "('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'co4,
    'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGl ⇒ 'l2 set" where
  "set2_FGl x = (⋃y∈set1_F x. set2_G y)"

definition set3_FGl :: "('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'co4,
    'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGl ⇒ 'l3 set" where
  "set3_FGl x = set3_F x"

definition
  bd_FGl :: "('co1, 'co2, 'co3, 'co4, 'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGlbd rel"
  where "bd_FGl = bd_F *c bd_G +c bd_F"

lemma set1_FGl_map: "set1_FGl ∘ mapl_FGl l1 l2 l3 = image l1 ∘ set1_FGl"
  by (simp add: fun_eq_iff set1_FGl_def mapl_FGl_def map_FGl_def
      mapl_F_def[symmetric] mapl_G_def[symmetric]
      set1_F_map[THEN fun_cong, simplified] set2_F_map[THEN fun_cong, simplified]
      set1_G_map[THEN fun_cong, simplified]
      image_Un image_UN)

lemma set2_FGl_map: "set2_FGl ∘ mapl_FGl l1 l2 l3 = image l2 ∘ set2_FGl"
  by (simp add: fun_eq_iff set2_FGl_def mapl_FGl_def map_FGl_def
      mapl_F_def[symmetric] mapl_G_def[symmetric]
      set1_F_map[THEN fun_cong, simplified] set2_G_map[THEN fun_cong, simplified] image_UN)

lemma set3_FGl_map: "set3_FGl ∘ mapl_FGl l1 l2 l3 = image l3 ∘ set3_FGl"
  by (simp add: fun_eq_iff set3_FGl_def mapl_FGl_def map_FGl_def
      mapl_F_def[symmetric] mapl_G_def[symmetric] set3_F_map[THEN fun_cong, simplified])

lemma bd_FGl_card_order: "card_order bd_FGl"
  unfolding bd_FGl_def using bd_F_card_order bd_G_card_order
  by (intro card_order_csum card_order_cprod)

lemma bd_FGl_cinfinite: "cinfinite bd_FGl"
  unfolding bd_FGl_def using bd_F_cinfinite bd_G_cinfinite
  by (intro cinfinite_csum disjI2)

lemma
  fixes x :: "(_, _, _, 'co1, 'co2, 'co3, 'co4, 'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGl"
  shows set1_FGl_bound: "card_of (set1_FGl x) <o
      (bd_FGl :: ('co1, 'co2, 'co3, 'co4, 'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGlbd rel)"
    and set2_FGl_bound: "card_of (set2_FGl x) <o
      (bd_FGl :: ('co1, 'co2, 'co3, 'co4, 'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGlbd rel)"
    and set3_FGl_bound: "card_of (set3_FGl x) <o
      (bd_FGl :: ('co1, 'co2, 'co3, 'co4, 'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGlbd rel)"
  unfolding set1_FGl_def set2_FGl_def set3_FGl_def bd_FGl_def
    apply (simp)
    apply (rule ordLeq_ordLess_trans)
     apply (rule Un_csum)
    apply (rule csum_mono_strict)
         apply (rule card_of_Card_order)+
       apply (rule Cinfinite_cprod2)
        apply (rule Cinfinite_Cnotzero)
        apply (rule bd_F_Cinfinite)
       apply (rule bd_G_Cinfinite)
      apply (rule bd_F_Cinfinite)
     apply (rule comp_single_set_bd_strict[where fset=set1_G and gset=set1_F, rotated])
          apply (rule bd_G_regularCard)
         apply (rule bd_F_Cinfinite)
        apply (rule bd_F_regularCard)
       apply (rule set1_G_bound)
      apply (rule set1_F_bound)
     apply (rule bd_G_Cinfinite)
    apply (rule set2_F_bound)
   apply (rule ordLess_ordLeq_trans)
    apply (rule comp_single_set_bd_strict[where fset=set2_G and gset=set1_F, rotated])
         apply (rule bd_G_regularCard)
        apply (rule bd_F_Cinfinite)
       apply (rule bd_F_regularCard)
      apply (rule set2_G_bound)
     apply (rule set1_F_bound)
    apply (rule bd_G_Cinfinite)
   apply (rule ordLeq_csum1)
   apply (rule Card_order_cprod)
  apply (rule ordLess_ordLeq_trans)
   apply (rule set3_F_bound)
  apply (rule ordLeq_csum2)
  apply (rule conjunct2[OF bd_F_Cinfinite])
  done

lemma mapl_FGl_cong:
  assumes "⋀z. z ∈ set1_FGl x ⟹ l1 z = l1' z" and "⋀z. z ∈ set2_FGl x ⟹ l2 z = l2' z"
    and "⋀z. z ∈ set3_FGl x ⟹ l3 z = l3' z"
  shows "mapl_FGl l1 l2 l3 x = mapl_FGl l1' l2' l3' x"
  unfolding mapl_FGl_def map_FGl_def mapl_G_def[symmetric] mapl_F_def[symmetric]
  by (auto 0 5 intro: mapl_F_cong mapl_G_cong assms simp add: set1_FGl_def set2_FGl_def set3_FGl_def)

lemma rell_FGl_mono_strong:
  assumes "rell_FGl L1 L2 L3 x y"
    and "⋀a b. a ∈ set1_FGl x ⟹ b ∈ set1_FGl y ⟹ L1 a b ⟹ L1' a b"
    and "⋀a b. a ∈ set2_FGl x ⟹ b ∈ set2_FGl y ⟹ L2 a b ⟹ L2' a b"
    and "⋀a b. a ∈ set3_FGl x ⟹ b ∈ set3_FGl y ⟹ L3 a b ⟹ L3' a b"
  shows "rell_FGl L1' L2' L3' x y"
  using assms(1) unfolding rell_FGl_def rel_FGl_def rell_G_def[symmetric] rell_F_def[symmetric]
  by (auto 0 5 intro: rell_F_mono_strong rell_G_mono_strong assms(2-4)
      simp add: set1_FGl_def set2_FGl_def set3_FGl_def)


subsection ‹Composition in a covariant position›

type_synonym
  ('l1, 'co1, 'co2, 'co3, 'co4, 'co5, 'co6, 'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGco =
    "('l1, 'co1, 'co5, ('co1, 'co2, 'co3, 'co4, 'contra1, 'contra2, 'f1) G, 'co3, 'co6,
    'contra1, 'contra3, 'contra4, 'f2) F"

text ‹The type variables @{typ 'co1}, @{typ 'co3} and @{typ 'contra1} have each been merged.›

definition "rel_FGco L1 Co1 Co2 Co3 Co4 Co5 Co6 Contra1 Contra2 Contra3 Contra4 =
  rel_F L1 Co1 Co5 (rel_G Co1 Co2 Co3 Co4 Contra1 Contra2) Co3 Co6 Contra1 Contra3 Contra4"

definition "map_FGco l1 co1 co2 co3 co4 co5 co6 contra1 contra2 contra3 contra4 =
  map_F l1 co1 co5 (map_G co1 co2 co3 co4 contra1 contra2) co3 co6 contra1 contra3 contra4"

lemma rel_FGco_mono:
  "⟦ L1 ≤ L1'; Co1 ≤ Co1'; Co2 ≤ Co2'; Co3 ≤ Co3'; Co4 ≤ Co4'; Co5 ≤ Co5'; Co6 ≤ Co6';
     Contra1' ≤ Contra1; Contra2' ≤ Contra2; Contra3' ≤ Contra3; Contra4' ≤ Contra4 ⟧ ⟹
  rel_FGco L1 Co1 Co2 Co3 Co4 Co5 Co6 Contra1 Contra2 Contra3 Contra4 ≤
  rel_FGco L1' Co1' Co2' Co3' Co4' Co5' Co6' Contra1' Contra2' Contra3' Contra4'"
  unfolding rel_FGco_def
  apply (rule rel_F_mono)
          apply (assumption)+
       apply (rule rel_G_mono)
            apply (assumption)+
  done

lemma rel_FGco_eq: "rel_FGco (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) = (=)"
  unfolding rel_FGco_def by (simp add: rel_F_eq rel_G_eq)

lemma rel_FGco_conversep:
  "rel_FGco L1¯¯ Co1¯¯ Co2¯¯ Co3¯¯ Co4¯¯ Co5¯¯ Co6¯¯ Contra1¯¯ Contra2¯¯ Contra3¯¯ Contra4¯¯ =
  (rel_FGco L1 Co1 Co2 Co3 Co4 Co5 Co6 Contra1 Contra2 Contra3 Contra4)¯¯"
  unfolding rel_FGco_def by (simp add: rel_F_conversep rel_G_conversep)

lemma map_FGco_id0: "map_FGco id id id id id id id id id id id = id"
  unfolding map_FGco_def by (simp add: map_F_id0 map_G_id0)

lemma map_FGco_comp: "map_FGco l1 co1 co2 co3 co4 co5 co6 contra1 contra2 contra3 contra4 ∘
  map_FGco l1' co1' co2' co3' co4' co5' co6' contra1' contra2' contra3' contra4' =
  map_FGco (l1 ∘ l1') (co1 ∘ co1') (co2 ∘ co2') (co3 ∘ co3') (co4 ∘ co4') (co5 ∘ co5') (co6 ∘ co6')
    (contra1' ∘ contra1) (contra2' ∘ contra2) (contra3' ∘ contra3) (contra4' ∘ contra4)"
  unfolding map_FGco_def by (simp add: map_F_comp map_G_comp)

lemma map_FGco_parametric:
  "rel_fun (rel_fun L1 L1') (rel_fun (rel_fun Co1 Co1') (rel_fun (rel_fun Co2 Co2')
    (rel_fun (rel_fun Co3 Co3') (rel_fun (rel_fun Co4 Co4')
    (rel_fun (rel_fun Co5 Co5') (rel_fun (rel_fun Co6 Co6')
  (rel_fun (rel_fun Contra1' Contra1) (rel_fun (rel_fun Contra2' Contra2)
    (rel_fun (rel_fun Contra3' Contra3) (rel_fun (rel_fun Contra4' Contra4)
  (rel_fun (rel_FGco L1 Co1 Co2 Co3 Co4 Co5 Co6 Contra1 Contra2 Contra3 Contra4)
  (rel_FGco L1' Co1' Co2' Co3' Co4' Co5' Co6' Contra1' Contra2' Contra3' Contra4'))))))))))))
  map_FGco map_FGco"
  unfolding rel_FGco_def map_FGco_def
  apply (intro rel_funI)
  apply (elim map_F_rel_cong map_G_rel_cong)
               apply (erule (2) rel_funE)+
  done

definition rel_FGco_pos_distr_cond :: "('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co1' ⇒ 'co1'' ⇒ bool) ⇒
    ('co2 ⇒ 'co2' ⇒ bool) ⇒ ('co2' ⇒ 'co2'' ⇒ bool) ⇒
    ('co3 ⇒ 'co3' ⇒ bool) ⇒ ('co3' ⇒ 'co3'' ⇒ bool) ⇒
    ('co4 ⇒ 'co4' ⇒ bool) ⇒ ('co4' ⇒ 'co4'' ⇒ bool) ⇒
    ('co5 ⇒ 'co5' ⇒ bool) ⇒ ('co5' ⇒ 'co5'' ⇒ bool) ⇒
    ('co6 ⇒ 'co6' ⇒ bool) ⇒ ('co6' ⇒ 'co6'' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra1' ⇒ 'contra1'' ⇒ bool) ⇒
    ('contra2 ⇒ 'contra2' ⇒ bool) ⇒ ('contra2' ⇒ 'contra2'' ⇒ bool) ⇒
    ('contra3 ⇒ 'contra3' ⇒ bool) ⇒ ('contra3' ⇒ 'contra3'' ⇒ bool) ⇒
    ('contra4 ⇒ 'contra4' ⇒ bool) ⇒ ('contra4' ⇒ 'contra4'' ⇒ bool) ⇒
    ('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself ⇒ bool" where
  "rel_FGco_pos_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4' Co5 Co5' Co6 Co6'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool).
    (rel_FGco L1 Co1 Co2 Co3 Co4 Co5 Co6 Contra1 Contra2 Contra3 Contra4 ::
      (_, _, _, _, _, _, _, _, _, _, _, 'f1, 'f2) FGco ⇒ _) OO
      rel_FGco L1' Co1' Co2' Co3' Co4' Co5' Co6' Contra1' Contra2' Contra3' Contra4' ≤
    rel_FGco (L1 OO L1') (Co1 OO Co1') (Co2 OO Co2') (Co3 OO Co3')
      (Co4 OO Co4') (Co5 OO Co5') (Co6 OO Co6')
      (Contra1 OO Contra1') (Contra2 OO Contra2') (Contra3 OO Contra3') (Contra4 OO Contra4'))"

definition rel_FGco_neg_distr_cond :: "('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co1' ⇒ 'co1'' ⇒ bool) ⇒
    ('co2 ⇒ 'co2' ⇒ bool) ⇒ ('co2' ⇒ 'co2'' ⇒ bool) ⇒
    ('co3 ⇒ 'co3' ⇒ bool) ⇒ ('co3' ⇒ 'co3'' ⇒ bool) ⇒
    ('co4 ⇒ 'co4' ⇒ bool) ⇒ ('co4' ⇒ 'co4'' ⇒ bool) ⇒
    ('co5 ⇒ 'co5' ⇒ bool) ⇒ ('co5' ⇒ 'co5'' ⇒ bool) ⇒
    ('co6 ⇒ 'co6' ⇒ bool) ⇒ ('co6' ⇒ 'co6'' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra1' ⇒ 'contra1'' ⇒ bool) ⇒
    ('contra2 ⇒ 'contra2' ⇒ bool) ⇒ ('contra2' ⇒ 'contra2'' ⇒ bool) ⇒
    ('contra3 ⇒ 'contra3' ⇒ bool) ⇒ ('contra3' ⇒ 'contra3'' ⇒ bool) ⇒
    ('contra4 ⇒ 'contra4' ⇒ bool) ⇒ ('contra4' ⇒ 'contra4'' ⇒ bool) ⇒
    ('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself ⇒ bool" where
  "rel_FGco_neg_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4' Co5 Co5' Co6 Co6'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool).
    rel_FGco (L1 OO L1') (Co1 OO Co1') (Co2 OO Co2') (Co3 OO Co3')
      (Co4 OO Co4') (Co5 OO Co5') (Co6 OO Co6')
      (Contra1 OO Contra1') (Contra2 OO Contra2') (Contra3 OO Contra3') (Contra4 OO Contra4') ≤
    (rel_FGco L1 Co1 Co2 Co3 Co4 Co5 Co6 Contra1 Contra2 Contra3 Contra4 ::
      (_, _, _, _, _, _, _, _, _, _, _, 'f1, 'f2) FGco ⇒ _) OO
      rel_FGco L1' Co1' Co2' Co3' Co4' Co5' Co6' Contra1' Contra2' Contra3' Contra4')"

text ‹Sufficient conditions for subdistributivity over relation composition.›

lemma rel_FGco_pos_distr_imp:
  fixes Co1 :: "'co1 ⇒ 'co1' ⇒ bool" and Co1' :: "'co1' ⇒ 'co1'' ⇒ bool"
    and Co2 :: "'co2 ⇒ 'co2' ⇒ bool" and Co2' :: "'co2' ⇒ 'co2'' ⇒ bool"
    and Co5 :: "'co5 ⇒ 'co5' ⇒ bool" and Co5' :: "'co5' ⇒ 'co5'' ⇒ bool"
    and tytok_F :: "('l1 × 'l1' × 'l1'' × 'co1 × 'co1' × 'co1'' × 'co5 × 'co5' × 'co5'' ×
      'f2) itself"
    and tytok_G :: "('co1 × 'co1' × 'co1'' × 'co2 × 'co2' × 'co2'' × 'f1) itself"
    and tytok_FGco :: "('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself"
  assumes "rel_F_pos_distr_cond
      (rel_G Co1 Co2 Co3 Co4 Contra1 Contra2 :: (_, _, _, _, _, _, 'f1) G ⇒ _)
      (rel_G Co1' Co2' Co3' Co4' Contra1' Contra2') Co3 Co3' Co6 Co6'
      Contra1 Contra1' Contra3 Contra3' Contra4 Contra4' tytok_F"
    and "rel_G_pos_distr_cond Co3 Co3' Co4 Co4' Contra1 Contra1' Contra2 Contra2' tytok_G"
  shows "rel_FGco_pos_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4' Co5 Co5' Co6 Co6'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' tytok_FGco"
  unfolding rel_FGco_pos_distr_cond_def rel_FGco_def
  apply (intro allI)
  apply (rule order_trans)
   apply (rule rel_F_pos_distr)
   apply (rule assms(1))
  apply (rule rel_F_mono)
          apply (rule order_refl)+
       apply (rule rel_G_pos_distr)
       apply (rule assms(2))
      apply (rule order_refl)+
  done

lemma rel_FGco_neg_distr_imp:
  fixes Co1 :: "'co1 ⇒ 'co1' ⇒ bool" and Co1' :: "'co1' ⇒ 'co1'' ⇒ bool"
    and Co2 :: "'co2 ⇒ 'co2' ⇒ bool" and Co2' :: "'co2' ⇒ 'co2'' ⇒ bool"
    and Co5 :: "'co5 ⇒ 'co5' ⇒ bool" and Co5' :: "'co5' ⇒ 'co5'' ⇒ bool"
    and tytok_F :: "('l1 × 'l1' × 'l1'' × 'co1 × 'co1' × 'co1'' × 'co5 × 'co5' × 'co5'' × 'f2) itself"
    and tytok_G :: "('co1 × 'co1' × 'co1'' × 'co2 × 'co2' × 'co2'' × 'f1) itself"
    and tytok_FGco :: "('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself"
  assumes "rel_F_neg_distr_cond
      (rel_G Co1 Co2 Co3 Co4 Contra1 Contra2 :: (_, _, _, _, _, _, 'f1) G ⇒ _)
      (rel_G Co1' Co2' Co3' Co4' Contra1' Contra2') Co3 Co3' Co6 Co6'
      Contra1 Contra1' Contra3 Contra3' Contra4 Contra4' tytok_F"
    and "rel_G_neg_distr_cond Co3 Co3' Co4 Co4' Contra1 Contra1' Contra2 Contra2' tytok_G"
  shows "rel_FGco_neg_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4' Co5 Co5' Co6 Co6'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' tytok_FGco"
  unfolding rel_FGco_neg_distr_cond_def rel_FGco_def
  apply (intro allI)
  apply (rule order_trans[rotated])
   apply (rule rel_F_neg_distr)
   apply (rule assms(1))
  apply (rule rel_F_mono)
          apply (rule order_refl)+
       apply (rule rel_G_neg_distr)
       apply (rule assms(2))
      apply (rule order_refl)+
  done

lemma rel_FGco_pos_distr_cond_eq:
  fixes tytok :: "('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself"
  shows "rel_FGco_pos_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=)
    (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  apply (rule rel_FGco_pos_distr_imp)
   apply (simp add: rel_G_eq)
   apply (rule rel_F_pos_distr_cond_eq rel_G_pos_distr_cond_eq)+
  done

lemma rel_FGco_neg_distr_cond_eq:
  fixes tytok :: "('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself"
  shows "rel_FGco_neg_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=)
    (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  apply (rule rel_FGco_neg_distr_imp)
   apply (simp add: rel_G_eq)
   apply (rule rel_F_neg_distr_cond_eq rel_G_neg_distr_cond_eq)+
  done

definition "rell_FGco L1 = rel_FGco L1 (=) (=) (=) (=) (=) (=) (=) (=) (=) (=)"
definition "mapl_FGco l1 = map_FGco l1 id id id id id id id id id id"

type_synonym ('co1, 'co2, 'co3, 'co4, 'co5, 'co6,
    'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGcobd =
  "(('co1, 'co2, 'co3, 'co4, 'contra1, 'contra2, 'f1) G,
    'co3, 'co6, 'contra1, 'contra3, 'contra4, 'f2) Fbd"

definition set1_FGco :: "('l1, 'co1, 'co2, 'co3, 'co4, 'co5, 'co6,
    'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGco ⇒ 'l1 set" where
  "set1_FGco x = set1_F x"

definition bd_FGco :: "('co1, 'co2, 'co3, 'co4, 'co5, 'co6,
    'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGcobd rel" where
  "bd_FGco = bd_F"

lemma set1_FGco_map: "set1_FGco ∘ mapl_FGco l1 = image l1 ∘ set1_FGco"
  by (simp add: fun_eq_iff set1_FGco_def mapl_FGco_def map_FGco_def
      mapl_F_def[symmetric] mapl_G_def[symmetric] mapl_G_id0
      set1_F_map[THEN fun_cong, simplified])

lemma bd_FGco_card_order: "card_order bd_FGco"
  unfolding bd_FGco_def using bd_F_card_order .

lemma bd_FGco_cinfinite: "cinfinite bd_FGco"
  unfolding bd_FGco_def using bd_F_cinfinite .

lemma set1_FGco_bound:
  fixes x :: "(_, 'co1, 'co2, 'co3, 'co4, 'co5, 'co6,
    'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGco"
  shows "card_of (set1_FGco x) <o (bd_FGco :: ('co1, 'co2, 'co3, 'co4, 'co5, 'co6,
    'contra1, 'contra2, 'contra3, 'contra4, 'f1, 'f2) FGcobd rel)"
  unfolding set1_FGco_def bd_FGco_def using set1_F_bound .

lemma mapl_FGco_cong:
  assumes "⋀z. z ∈ set1_FGco x ⟹ l1 z = l1' z"
  shows "mapl_FGco l1 x = mapl_FGco l1' x"
  unfolding mapl_FGco_def map_FGco_def mapl_G_def[symmetric] mapl_F_def[symmetric] mapl_G_id0
  by (auto 0 3 intro: mapl_F_cong assms simp add: set1_FGco_def)

lemma rell_FGco_mono_strong:
  assumes "rell_FGco L1 x y"
    and "⋀a b. a ∈ set1_FGco x ⟹ b ∈ set1_FGco y ⟹ L1 a b ⟹ L1' a b"
  shows "rell_FGco L1' x y"
  using assms(1) unfolding rell_FGco_def rel_FGco_def rel_G_eq rell_F_def[symmetric]
  by (auto 0 3 intro: rell_F_mono_strong assms(2) simp add: set1_FGco_def)


subsection ‹Composition in a contravariant position›

type_synonym
  ('l1, 'co1, 'co2, 'co3, 'co4, 'co5, 'contra1,
    'contra2, 'contra3, 'contra4, 'contra5, 'f1, 'f2) FGcontra =
  "('l1, 'co1, 'co3, 'co1, 'co4, 'co5, ('contra1, 'contra2, 'contra3, 'contra4, 'co1, 'co2, 'f1) G,
    'contra1, 'contra5, 'f2) F"

text ‹The type variables @{typ 'co1} and @{typ 'contra1} have each been merged.›

definition "rel_FGcontra L1 Co1 Co2 Co3 Co4 Co5 Contra1 Contra2 Contra3 Contra4 Contra5 =
  rel_F L1 Co1 Co3 Co1 Co4 Co5 (rel_G Contra1 Contra2 Contra3 Contra4 Co1 Co2) Contra1 Contra5"

definition "map_FGcontra l1 co1 co2 co3 co4 co5 contra1 contra2 contra3 contra4 contra5 =
  map_F l1 co1 co3 co1 co4 co5 (map_G contra1 contra2 contra3 contra4 co1 co2) contra1 contra5"

lemma rel_FGcontra_mono:
  "⟦ L1 ≤ L1'; Co1 ≤ Co1'; Co2 ≤ Co2'; Co3 ≤ Co3'; Co4 ≤ Co4'; Co5 ≤ Co5';
     Contra1' ≤ Contra1; Contra2' ≤ Contra2; Contra3' ≤ Contra3;
     Contra4' ≤ Contra4; Contra5' ≤ Contra5 ⟧ ⟹
  rel_FGcontra L1 Co1 Co2 Co3 Co4 Co5 Contra1 Contra2 Contra3 Contra4 Contra5 ≤
  rel_FGcontra L1' Co1' Co2' Co3' Co4' Co5' Contra1' Contra2' Contra3' Contra4' Contra5'"
  unfolding rel_FGcontra_def
  apply (rule rel_F_mono)
          apply (assumption)+
    apply (rule rel_G_mono)
         apply (assumption)+
  done

lemma rel_FGcontra_eq: "rel_FGcontra (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) = (=)"
  unfolding rel_FGcontra_def by (simp add: rel_F_eq rel_G_eq)

lemma rel_FGcontra_conversep:
  "rel_FGcontra L1¯¯ Co1¯¯ Co2¯¯ Co3¯¯ Co4¯¯ Co5¯¯ Contra1¯¯ Contra2¯¯ Contra3¯¯ Contra4¯¯ Contra5¯¯ =
  (rel_FGcontra L1 Co1 Co2 Co3 Co4 Co5 Contra1 Contra2 Contra3 Contra4 Contra5)¯¯"
  unfolding rel_FGcontra_def by (simp add: rel_F_conversep rel_G_conversep)

lemma map_FGcontra_id0: "map_FGcontra id id id id id id id id id id id = id"
  unfolding map_FGcontra_def by (simp add: map_F_id0 map_G_id0)

lemma map_FGcontra_comp:
  "map_FGcontra l1 co1 co2 co3 co4 co5 contra1 contra2 contra3 contra4 contra5 ∘
  map_FGcontra l1' co1' co2' co3' co4' co5' contra1' contra2' contra3' contra4' contra5' =
  map_FGcontra (l1 ∘ l1') (co1 ∘ co1') (co2 ∘ co2') (co3 ∘ co3') (co4 ∘ co4') (co5 ∘ co5')
    (contra1' ∘ contra1) (contra2' ∘ contra2) (contra3' ∘ contra3)
    (contra4' ∘ contra4) (contra5' ∘ contra5)"
  unfolding map_FGcontra_def by (simp add: map_F_comp map_G_comp)

lemma map_FGcontra_parametric:
  "rel_fun (rel_fun L1 L1') (rel_fun (rel_fun Co1 Co1') (rel_fun (rel_fun Co2 Co2')
    (rel_fun (rel_fun Co3 Co3') (rel_fun (rel_fun Co4 Co4') (rel_fun (rel_fun Co5 Co5')
  (rel_fun (rel_fun Contra1' Contra1) (rel_fun (rel_fun Contra2' Contra2)
    (rel_fun (rel_fun Contra3' Contra3) (rel_fun (rel_fun Contra4' Contra4)
    (rel_fun (rel_fun Contra5' Contra5)
  (rel_fun (rel_FGcontra L1 Co1 Co2 Co3 Co4 Co5 Contra1 Contra2 Contra3 Contra4 Contra5)
  (rel_FGcontra L1' Co1' Co2' Co3' Co4' Co5' Contra1' Contra2' Contra3' Contra4' Contra5'))))))))))))
  map_FGcontra map_FGcontra"
  unfolding rel_FGcontra_def map_FGcontra_def
  apply (intro rel_funI)
  apply (elim map_F_rel_cong map_G_rel_cong)
               apply (erule (2) rel_funE)+
  done

definition rel_FGcontra_pos_distr_cond :: "('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co1' ⇒ 'co1'' ⇒ bool) ⇒
    ('co2 ⇒ 'co2' ⇒ bool) ⇒ ('co2' ⇒ 'co2'' ⇒ bool) ⇒
    ('co3 ⇒ 'co3' ⇒ bool) ⇒ ('co3' ⇒ 'co3'' ⇒ bool) ⇒
    ('co4 ⇒ 'co4' ⇒ bool) ⇒ ('co4' ⇒ 'co4'' ⇒ bool) ⇒
    ('co5 ⇒ 'co5' ⇒ bool) ⇒ ('co5' ⇒ 'co5'' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra1' ⇒ 'contra1'' ⇒ bool) ⇒
    ('contra2 ⇒ 'contra2' ⇒ bool) ⇒ ('contra2' ⇒ 'contra2'' ⇒ bool) ⇒
    ('contra3 ⇒ 'contra3' ⇒ bool) ⇒ ('contra3' ⇒ 'contra3'' ⇒ bool) ⇒
    ('contra4 ⇒ 'contra4' ⇒ bool) ⇒ ('contra4' ⇒ 'contra4'' ⇒ bool) ⇒
    ('contra5 ⇒ 'contra5' ⇒ bool) ⇒ ('contra5' ⇒ 'contra5'' ⇒ bool) ⇒
    ('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself ⇒ bool" where
  "rel_FGcontra_pos_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4' Co5 Co5'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' Contra5 Contra5' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool).
    (rel_FGcontra L1 Co1 Co2 Co3 Co4 Co5 Contra1 Contra2 Contra3 Contra4 Contra5 ::
      (_, _, _, _, _, _, _, _, _, _, _, 'f1, 'f2) FGcontra ⇒ _) OO
      rel_FGcontra L1' Co1' Co2' Co3' Co4' Co5' Contra1' Contra2' Contra3' Contra4' Contra5' ≤
    rel_FGcontra (L1 OO L1') (Co1 OO Co1') (Co2 OO Co2') (Co3 OO Co3') (Co4 OO Co4') (Co5 OO Co5')
      (Contra1 OO Contra1') (Contra2 OO Contra2') (Contra3 OO Contra3')
      (Contra4 OO Contra4') (Contra5 OO Contra5'))"

definition rel_FGcontra_neg_distr_cond :: "('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co1' ⇒ 'co1'' ⇒ bool) ⇒
    ('co2 ⇒ 'co2' ⇒ bool) ⇒ ('co2' ⇒ 'co2'' ⇒ bool) ⇒
    ('co3 ⇒ 'co3' ⇒ bool) ⇒ ('co3' ⇒ 'co3'' ⇒ bool) ⇒
    ('co4 ⇒ 'co4' ⇒ bool) ⇒ ('co4' ⇒ 'co4'' ⇒ bool) ⇒
    ('co5 ⇒ 'co5' ⇒ bool) ⇒ ('co5' ⇒ 'co5'' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra1' ⇒ 'contra1'' ⇒ bool) ⇒
    ('contra2 ⇒ 'contra2' ⇒ bool) ⇒ ('contra2' ⇒ 'contra2'' ⇒ bool) ⇒
    ('contra3 ⇒ 'contra3' ⇒ bool) ⇒ ('contra3' ⇒ 'contra3'' ⇒ bool) ⇒
    ('contra4 ⇒ 'contra4' ⇒ bool) ⇒ ('contra4' ⇒ 'contra4'' ⇒ bool) ⇒
    ('contra5 ⇒ 'contra5' ⇒ bool) ⇒ ('contra5' ⇒ 'contra5'' ⇒ bool) ⇒
    ('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself ⇒ bool" where
  "rel_FGcontra_neg_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4' Co5 Co5'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' Contra5 Contra5' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool).
    rel_FGcontra (L1 OO L1') (Co1 OO Co1') (Co2 OO Co2') (Co3 OO Co3') (Co4 OO Co4') (Co5 OO Co5')
      (Contra1 OO Contra1') (Contra2 OO Contra2') (Contra3 OO Contra3')
      (Contra4 OO Contra4') (Contra5 OO Contra5') ≤
    (rel_FGcontra L1 Co1 Co2 Co3 Co4 Co5 Contra1 Contra2 Contra3 Contra4 Contra5 ::
      (_, _, _, _, _, _, _, _, _, _, _, 'f1, 'f2) FGcontra ⇒ _) OO
      rel_FGcontra L1' Co1' Co2' Co3' Co4' Co5' Contra1' Contra2' Contra3' Contra4' Contra5')"

text ‹Sufficient conditions for subdistributivity over relation composition.›

lemma rel_FGcontra_pos_distr_imp:
  fixes Co1 :: "'co1 ⇒ 'co1' ⇒ bool" and Co1' :: "'co1' ⇒ 'co1'' ⇒ bool"
    and Co3 :: "'co3 ⇒ 'co3' ⇒ bool" and Co3' :: "'co3' ⇒ 'co3'' ⇒ bool"
    and Contra1 :: "'contra1 ⇒ 'contra1' ⇒ bool" and Contra1' :: "'contra1' ⇒ 'contra1'' ⇒ bool"
    and Contra2 :: "'contra2 ⇒ 'contra2' ⇒ bool" and Contra2' :: "'contra2' ⇒ 'contra2'' ⇒ bool"
    and tytok_F :: "('l1 × 'l1' × 'l1'' × 'co1 × 'co1' × 'co1'' × 'co3 × 'co3' × 'co3'' ×
      'f2) itself"
    and tytok_G :: "('contra1 × 'contra1' × 'contra1'' × 'contra2 × 'contra2' × 'contra2'' ×
      'f1) itself"
    and tytok_FGcontra :: "('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself"
  assumes "rel_F_pos_distr_cond Co1 Co1' Co4 Co4' Co5 Co5'
      (rel_G Contra1 Contra2 Contra3 Contra4 Co1 Co2 :: (_, _, _, _, _, _, 'f1) G ⇒ _)
      (rel_G Contra1' Contra2' Contra3' Contra4' Co1' Co2')
      Contra1 Contra1' Contra5 Contra5' tytok_F"
    and "rel_G_neg_distr_cond Contra3 Contra3' Contra4 Contra4' Co1 Co1' Co2 Co2' tytok_G"
  shows "rel_FGcontra_pos_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4' Co5 Co5'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' Contra5 Contra5'
    tytok_FGcontra"
  unfolding rel_FGcontra_pos_distr_cond_def rel_FGcontra_def
  apply (intro allI)
  apply (rule order_trans)
   apply (rule rel_F_pos_distr)
   apply (rule assms(1))
  apply (rule rel_F_mono)
          apply (rule order_refl)+
    apply (rule rel_G_neg_distr)
    apply (rule assms(2))
   apply (rule order_refl)+
  done

lemma rel_FGcontra_neg_distr_imp:
  fixes Co1 :: "'co1 ⇒ 'co1' ⇒ bool" and Co1' :: "'co1' ⇒ 'co1'' ⇒ bool"
    and Co3 :: "'co3 ⇒ 'co3' ⇒ bool" and Co3' :: "'co3' ⇒ 'co3'' ⇒ bool"
    and Contra1 :: "'contra1 ⇒ 'contra1' ⇒ bool" and Contra1' :: "'contra1' ⇒ 'contra1'' ⇒ bool"
    and Contra2 :: "'contra2 ⇒ 'contra2' ⇒ bool" and Contra2' :: "'contra2' ⇒ 'contra2'' ⇒ bool"
    and tytok_F :: "('l1 × 'l1' × 'l1'' × 'co1 × 'co1' × 'co1'' × 'co3 × 'co3' × 'co3'' ×
      'f2) itself"
    and tytok_G :: "('contra1 × 'contra1' × 'contra1'' × 'contra2 × 'contra2' × 'contra2'' ×
      'f1) itself"
    and tytok_FGcontra :: "('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself"
  assumes "rel_F_neg_distr_cond Co1 Co1' Co4 Co4' Co5 Co5'
      (rel_G Contra1 Contra2 Contra3 Contra4 Co1 Co2 :: (_, _, _, _, _, _, 'f1) G ⇒ _)
      (rel_G Contra1' Contra2' Contra3' Contra4' Co1' Co2')
      Contra1 Contra1' Contra5 Contra5' tytok_F"
    and "rel_G_pos_distr_cond Contra3 Contra3' Contra4 Contra4' Co1 Co1' Co2 Co2' tytok_G"
  shows "rel_FGcontra_neg_distr_cond Co1 Co1' Co2 Co2' Co3 Co3' Co4 Co4' Co5 Co5'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' Contra4 Contra4' Contra5 Contra5' tytok_FGcontra"
  unfolding rel_FGcontra_neg_distr_cond_def rel_FGcontra_def
  apply (intro allI)
  apply (rule order_trans[rotated])
   apply (rule rel_F_neg_distr)
   apply (rule assms(1))
  apply (rule rel_F_mono)
          apply (rule order_refl)+
    apply (rule rel_G_pos_distr)
    apply (rule assms(2))
   apply (rule order_refl)+
  done

lemma rel_FGcontra_pos_distr_cond_eq:
  fixes tytok :: "('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself"
  shows "rel_FGcontra_pos_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) (=) (=)
    (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  apply (rule rel_FGcontra_pos_distr_imp)
   apply (simp add: rel_G_eq)
   apply (rule rel_F_pos_distr_cond_eq rel_G_neg_distr_cond_eq)+
  done

lemma rel_FGcontra_neg_distr_cond_eq:
  fixes tytok :: "('l1 × 'l1' × 'l1'' × 'f1 × 'f2) itself"
  shows "rel_FGcontra_neg_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) (=) (=)
    (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  apply (rule rel_FGcontra_neg_distr_imp)
   apply (simp add: rel_G_eq)
   apply (rule rel_F_neg_distr_cond_eq rel_G_pos_distr_cond_eq)+
  done

definition "rell_FGcontra L1 = rel_FGcontra L1 (=) (=) (=) (=) (=) (=) (=) (=) (=) (=)"
definition "mapl_FGcontra l1 = map_FGcontra l1 id id id id id id id id id id"

type_synonym ('co1, 'co2, 'co3, 'co4, 'co5, 'contra1, 'contra2, 'contra3, 'contra4, 'contra5,
    'f1, 'f2) FGcontrabd =
  "('co1, 'co4, 'co5, ('contra1, 'contra2, 'contra3, 'contra4, 'co1, 'co2, 'f1) G,
    'contra1, 'contra5, 'f2) Fbd"

definition set1_FGcontra :: "('l1, 'co1, 'co2, 'co3, 'co4, 'co5,
    'contra1, 'contra2, 'contra3, 'contra4, 'contra5, 'f1, 'f2) FGcontra ⇒ 'l1 set" where
  "set1_FGcontra x = set1_F x"

definition bd_FGcontra :: "('co1, 'co2, 'co3, 'co4, 'co5,
    'contra1, 'contra2, 'contra3, 'contra4, 'contra5, 'f1, 'f2) FGcontrabd rel" where
  "bd_FGcontra = bd_F"

lemma set1_FGcontra_map: "set1_FGcontra ∘ mapl_FGcontra l1 = image l1 ∘ set1_FGcontra"
  by (simp add: fun_eq_iff set1_FGcontra_def mapl_FGcontra_def map_FGcontra_def
      mapl_F_def[symmetric] mapl_G_def[symmetric] mapl_G_id0
      set1_F_map[THEN fun_cong, simplified])

lemma bd_FGcontra_card_order: "card_order bd_FGcontra"
  unfolding bd_FGcontra_def using bd_F_card_order .

lemma bd_FGcontra_cinfinite: "cinfinite bd_FGcontra"
  unfolding bd_FGcontra_def using bd_F_cinfinite .

lemma set1_FGcontra_bound:
  fixes x :: "(_, 'co1, 'co2, 'co3, 'co4, 'co5,
    'contra1, 'contra2, 'contra3, 'contra4, 'contra5, 'f1, 'f2) FGcontra"
  shows "card_of (set1_FGcontra x) <o (bd_FGcontra :: ('co1, 'co2, 'co3, 'co4, 'co5,
    'contra1, 'contra2, 'contra3, 'contra4, 'contra5, 'f1, 'f2) FGcontrabd rel)"
  unfolding set1_FGcontra_def bd_FGcontra_def using set1_F_bound .

lemma mapl_FGcontra_contrang:
  assumes "⋀z. z ∈ set1_FGcontra x ⟹ l1 z = l1' z"
  shows "mapl_FGcontra l1 x = mapl_FGcontra l1' x"
  unfolding mapl_FGcontra_def map_FGcontra_def mapl_G_def[symmetric] mapl_F_def[symmetric] mapl_G_id0
  by (auto 0 3 intro: mapl_F_cong assms simp add: set1_FGcontra_def)

lemma rell_FGcontra_mono_strong:
  assumes "rell_FGcontra L1 x y"
    and "⋀a b. a ∈ set1_FGcontra x ⟹ b ∈ set1_FGcontra y ⟹ L1 a b ⟹ L1' a b"
  shows "rell_FGcontra L1' x y"
  using assms(1) unfolding rell_FGcontra_def rel_FGcontra_def rel_G_eq rell_F_def[symmetric]
  by (auto 0 3 intro: rell_F_mono_strong assms(2) simp add: set1_FGcontra_def)


subsection ‹Composition in a fixed position›

type_synonym ('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) FGf =
  "('l1, 'l2, 'f2, 'co1, 'co2, 'f4, 'contra1, 'contra2, 'f6, ('f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) G) F"

text ‹The type variables @{typ 'f2}, @{typ 'f4} and @{typ 'f6} have each been merged.›

definition "rel_FGf L1 L2 Co1 Co2 Contra1 Contra2 =
  rel_F L1 L2 (=) Co1 Co2 (=) Contra1 Contra2 (=)"

definition "map_FGf l1 l2 co1 co2 contra1 contra2 = map_F l1 l2 id co1 co2 id contra1 contra2 id"

lemma rel_FGf_mono:
  "⟦ L1 ≤ L1'; L2 ≤ L2'; Co1 ≤ Co1'; Co2 ≤ Co2'; Contra1' ≤ Contra1; Contra2' ≤ Contra2 ⟧ ⟹
  rel_FGf L1 L2 Co1 Co2 Contra1 Contra2 ≤ rel_FGf L1' L2' Co1' Co2' Contra1' Contra2'"
  unfolding rel_FGf_def by (rule rel_F_mono) (auto)

lemma rel_FGf_eq: "rel_FGf (=) (=) (=) (=) (=) (=) = (=)"
  unfolding rel_FGf_def by (simp add: rel_F_eq)

lemma rel_FGf_conversep:
  "rel_FGf L1¯¯ L2¯¯ Co1¯¯ Co2¯¯ Contra1¯¯ Contra2¯¯ = (rel_FGf L1 L2 Co1 Co2 Contra1 Contra2)¯¯"
  unfolding rel_FGf_def by (simp add: rel_F_conversep[symmetric])

lemma map_FGf_id0: "map_FGf id id id id id id = id"
  unfolding map_FGf_def by (simp add: map_F_id0)

lemma map_FGf_comp: "map_FGf l1 l2 co1 co2 contra1 contra2 ∘
  map_FGf l1' l2' co1' co2' contra1' contra2' =
  map_FGf (l1 ∘ l1') (l2 ∘ l2') (co1 ∘ co1') (co2 ∘ co2') (contra1' ∘ contra1) (contra2' ∘ contra2)"
  unfolding map_FGf_def by (simp add: map_F_comp)

lemma map_FGf_parametric:
  "rel_fun (rel_fun L1 L1') (rel_fun (rel_fun L2 L2')
    (rel_fun (rel_fun Co1 Co1') (rel_fun (rel_fun Co2 Co2')
  (rel_fun (rel_fun Contra1' Contra1) (rel_fun (rel_fun Contra2' Contra2)
  (rel_fun (rel_FGf L1 L2 Co1 Co2 Contra1 Contra2)
  (rel_FGf L1' L2' Co1' Co2' Contra1' Contra2')))))))
  map_FGf map_FGf"
  unfolding rel_FGf_def map_FGf_def
  apply (intro rel_funI)
  apply (elim map_F_rel_cong)
          apply (simp_all)
       apply (erule (2) rel_funE)+
  done

definition rel_FGf_pos_distr_cond :: "('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co1' ⇒ 'co1'' ⇒ bool) ⇒
    ('co2 ⇒ 'co2' ⇒ bool) ⇒ ('co2' ⇒ 'co2'' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra1' ⇒ 'contra1'' ⇒ bool) ⇒
    ('contra2 ⇒ 'contra2' ⇒ bool) ⇒ ('contra2' ⇒ 'contra2'' ⇒ bool) ⇒
    ('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' ×
      'f1 × 'f2 × 'f3 × 'f4 × 'f5 × 'f6 × 'f7) itself ⇒ bool" where
  "rel_FGf_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool)
    (L2 :: 'l2 ⇒ 'l2' ⇒ bool) (L2' :: 'l2' ⇒ 'l2'' ⇒ bool).
    (rel_FGf L1 L2 Co1 Co2 Contra1 Contra2 ::
      (_, _, _, _, _, _, 'f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) FGf ⇒ _) OO
      rel_FGf L1' L2' Co1' Co2' Contra1' Contra2' ≤
    rel_FGf (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2')
      (Contra1 OO Contra1') (Contra2 OO Contra2'))"

definition rel_FGf_neg_distr_cond :: "('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co1' ⇒ 'co1'' ⇒ bool) ⇒
    ('co2 ⇒ 'co2' ⇒ bool) ⇒ ('co2' ⇒ 'co2'' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra1' ⇒ 'contra1'' ⇒ bool) ⇒
    ('contra2 ⇒ 'contra2' ⇒ bool) ⇒ ('contra2' ⇒ 'contra2'' ⇒ bool) ⇒
    ('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' ×
      'f1 × 'f2 × 'f3 × 'f4 × 'f5 × 'f6 × 'f7) itself ⇒ bool" where
  "rel_FGf_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool)
    (L2 :: 'l2 ⇒ 'l2' ⇒ bool) (L2' :: 'l2' ⇒ 'l2'' ⇒ bool).
    rel_FGf (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2')
      (Contra1 OO Contra1') (Contra2 OO Contra2') ≤
    (rel_FGf L1 L2 Co1 Co2 Contra1 Contra2 ::
      (_, _, _, _, _, _,'f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) FGf ⇒ _) OO
      rel_FGf L1' L2' Co1' Co2' Contra1' Contra2')"

text ‹Sufficient conditions for subdistributivity over relation composition.›

lemma rel_FGf_pos_distr_imp:
  fixes tytok_F :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'f2 × 'f2 × 'f2 ×
      ('f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) G) itself"
    and tytok_FGf :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' ×
      'f1 × 'f2 × 'f3 × 'f4 × 'f5 × 'f6 × 'f7) itself"
  assumes "rel_F_pos_distr_cond Co1 Co1' Co2 Co2' ((=) :: 'f4 ⇒ _) ((=) :: 'f4 ⇒ _)
      Contra1 Contra1' Contra2 Contra2' ((=) :: 'f6 ⇒ _) ((=) :: 'f6 ⇒ _) tytok_F"
  shows "rel_FGf_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_FGf"
  unfolding rel_FGf_pos_distr_cond_def rel_FGf_def
  apply (intro allI)
  apply (rule order_trans)
   apply (rule rel_F_pos_distr)
   apply (rule assms(1))
  apply (rule rel_F_mono)
          apply (simp_all add: eq_OO)
  done

lemma rel_FGf_neg_distr_imp:
  fixes tytok_F :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'f2 × 'f2 × 'f2 ×
      ('f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) G) itself"
    and tytok_FGf :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' ×
      'f1 × 'f2 × 'f3 × 'f4 × 'f5 × 'f6 × 'f7) itself"
  assumes "rel_F_neg_distr_cond Co1 Co1' Co2 Co2' ((=) :: 'f4 ⇒ _) ((=) :: 'f4 ⇒ _)
      Contra1 Contra1' Contra2 Contra2' ((=) :: 'f6 ⇒ _) ((=) :: 'f6 ⇒ _) tytok_F"
  shows "rel_FGf_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_FGf"
  unfolding rel_FGf_neg_distr_cond_def rel_FGf_def
  apply (intro allI)
  apply (rule order_trans[rotated])
   apply (rule rel_F_neg_distr)
   apply (rule assms(1))
  apply (rule rel_F_mono)
          apply (simp_all add: eq_OO)
  done

lemma rel_FGf_pos_distr_cond_eq:
  fixes tytok :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' ×
      'f1 × 'f2 × 'f3 × 'f4 × 'f5 × 'f6 × 'f7) itself"
  shows "rel_FGf_pos_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  by (intro rel_FGf_pos_distr_imp rel_F_pos_distr_cond_eq)

lemma rel_FGf_neg_distr_cond_eq:
  fixes tytok :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' ×
      'f1 × 'f2 × 'f3 × 'f4 × 'f5 × 'f6 × 'f7) itself"
  shows "rel_FGf_neg_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  by (intro rel_FGf_neg_distr_imp rel_F_neg_distr_cond_eq)

definition "rell_FGf L1 L2 = rel_FGf L1 L2 (=) (=) (=) (=)"
definition "mapl_FGf l1 l2 = map_FGf l1 l2 id id id id"

type_synonym ('co1, 'co2, 'contra1, 'contra2, 'f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) FGfbd =
  "('co1, 'co2, 'f4, 'contra1, 'contra2, 'f6, ('f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) G) Fbd"

definition set1_FGf :: "('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2,
    'f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) FGf ⇒ 'l1 set" where
  "set1_FGf x = set1_F x"

definition set2_FGf :: "('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2,
    'f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) FGf ⇒ 'l2 set" where
  "set2_FGf x = set2_F x"

definition bd_FGf :: "('co1, 'co2, 'contra1, 'contra2, 'f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) FGfbd rel"
  where "bd_FGf = bd_F"

lemma set1_FGf_map: "set1_FGf ∘ mapl_FGf l1 l2 = image l1 ∘ set1_FGf"
  by (simp add: fun_eq_iff set1_FGf_def mapl_FGf_def map_FGf_def mapl_F_def[symmetric]
      set1_F_map[THEN fun_cong, simplified])

lemma bd_FGf_card_order: "card_order bd_FGf"
  unfolding bd_FGf_def using bd_F_card_order .

lemma bd_FGf_cinfinite: "cinfinite bd_FGf"
  unfolding bd_FGf_def using bd_F_cinfinite .

lemma
  fixes x :: "(_, _, 'co1, 'co2, 'contra1, 'contra2, 'f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) FGf"
  shows set1_FGf_bound: "card_of (set1_FGf x) <o (bd_FGf :: ('co1, 'co2, 'contra1, 'contra2,
      'f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) FGfbd rel)"
    and set2_FGf_bound: "card_of (set2_FGf x) <o (bd_FGf :: ('co1, 'co2, 'contra1, 'contra2,
      'f1, 'f2, 'f3, 'f4, 'f5, 'f6, 'f7) FGfbd rel)"
  unfolding set1_FGf_def set2_FGf_def bd_FGf_def by (rule set1_F_bound set2_F_bound)+

lemma mapl_FGf_cong:
  assumes "⋀z. z ∈ set1_FGf x ⟹ l1 z = l1' z" and "⋀z. z ∈ set2_FGf x ⟹ l2 z = l2' z"
  shows "mapl_FGf l1 l2 x = mapl_FGf l1' l2' x"
  unfolding mapl_FGf_def map_FGf_def mapl_F_def[symmetric]
  by (auto 0 3 intro: mapl_F_cong assms simp add: set1_FGf_def set2_FGf_def)

lemma rell_FGf_mono_strong:
  assumes "rell_FGf L1 L2 x y"
    and "⋀a b. a ∈ set1_FGf x ⟹ b ∈ set1_FGf y ⟹ L1 a b ⟹ L1' a b"
    and "⋀a b. a ∈ set2_FGf x ⟹ b ∈ set2_FGf y ⟹ L2 a b ⟹ L2' a b"
  shows "rell_FGf L1' L2' x y"
  using assms(1) unfolding rell_FGf_def rel_FGf_def rell_F_def[symmetric]
  by (auto 0 3 intro: rell_F_mono_strong assms(2-3) simp add: set1_FGf_def set2_FGf_def)

end