Theory Axiomatised_BNF_CC

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

section ‹Axiomatisation›

theory Axiomatised_BNF_CC imports
  Preliminaries
  "HOL-Library.Rewrite"
begin

unbundle cardinal_syntax

text ‹
  This theory axiomatises two \BNFCC{}s, which will be used to demonstrate the closedness of \BNFCC{}s
  under various operations.
›

subsection ‹First abstract \BNFCC{}›

subsubsection ‹Axioms and basic definitions›

typedecl ('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F

text @{type F} has each three live, co-, and contravariant parameters, and one fixed parameter.›

consts
  rel_F :: "('l1  'l1'  bool)  ('l2  'l2'  bool)  ('l3  'l3'  bool) 
    ('co1  'co1'  bool)  ('co2  'co2'  bool)  ('co3  'co3'  bool) 
    ('contra1  'contra1'  bool)  ('contra2  'contra2'  bool) 
    ('contra3  'contra3'  bool) 
    ('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F 
    ('l1', 'l2', 'l3', 'co1', 'co2', 'co3', 'contra1', 'contra2', 'contra3', 'f) F  bool"
  map_F :: "('l1  'l1')  ('l2  'l2')  ('l3  'l3') 
    ('co1  'co1')  ('co2  'co2')  ('co3  'co3') 
    ('contra1'  'contra1)  ('contra2'  'contra2)  ('contra3'  'contra3) 
    ('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F 
    ('l1', 'l2', 'l3', 'co1', 'co2', 'co3', 'contra1', 'contra2', 'contra3', 'f) F"

axiomatization where
  rel_F_mono [mono]:
  "L1 L1' L2 L2' L3 L3' Co1 Co1' Co2 Co2' Co3 Co3'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3'.
     L1  L1'; L2  L2'; L3  L3'; Co1  Co1'; Co2  Co2'; Co3  Co3';
      Contra1'  Contra1; Contra2'  Contra2; Contra3'  Contra3  
    rel_F L1 L2 L3 Co1 Co2 Co3 Contra1 Contra2 Contra3 
    rel_F L1' L2' L3' Co1' Co2' Co3' Contra1' Contra2' Contra3'" and
  rel_F_eq: "rel_F (=) (=) (=) (=) (=) (=) (=) (=) (=) = (=)" and
  rel_F_conversep: "L1 L2 L3 Co1 Co2 Co3 Contra1 Contra2 Contra3.
    rel_F L1¯¯ L2¯¯ L3¯¯ Co1¯¯ Co2¯¯ Co3¯¯ Contra1¯¯ Contra2¯¯ Contra3¯¯ =
    (rel_F L1 L2 L3 Co1 Co2 Co3 Contra1 Contra2 Contra3)¯¯" and
  map_F_id0: "map_F id id id id id id id id id = id" and
  map_F_comp: "l1 l1' l2 l2' l3 l3' co1 co1' co2 co2' co3 co3'
    contra1 contra1' contra2 contra2' contra3 contra3'.
    map_F l1 l2 l3 co1 co2 co3 contra1 contra2 contra3 
      map_F l1' l2' l3' co1' co2' co3' contra1' contra2' contra3' =
    map_F (l1  l1') (l2  l2') (l3  l3') (co1  co1') (co2  co2') (co3  co3')
      (contra1'  contra1) (contra2'  contra2) (contra3'  contra3)" and
  map_F_parametric:
  "L1 L1' L2 L2' L3 L3' Co1 Co1' Co2 Co2' Co3 Co3'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3'.
    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 Contra1' Contra1) (rel_fun (rel_fun Contra2' Contra2)
      (rel_fun (rel_fun Contra3' Contra3)
      (rel_fun (rel_F L1 L2 L3 Co1 Co2 Co3 Contra1 Contra2 Contra3)
      (rel_F L1' L2' L3' Co1' Co2' Co3' Contra1' Contra2' Contra3')))))))))) map_F map_F"

definition rel_F_pos_distr_cond :: "('co1  'co1'  bool)  ('co1'  'co1''  bool) 
    ('co2  'co2'  bool)  ('co2'  'co2''  bool) 
    ('co3  'co3'  bool)  ('co3'  'co3''  bool) 
    ('contra1  'contra1'  bool)  ('contra1'  'contra1''  bool) 
    ('contra2  'contra2'  bool)  ('contra2'  'contra2''  bool) 
    ('contra3  'contra3'  bool)  ('contra3'  'contra3''  bool) 
    ('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'l3 × 'l3' × 'l3'' × 'f) itself  bool" where
  "rel_F_pos_distr_cond Co1 Co1' Co2 Co2' Co3 Co3'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' _ 
  ((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_F L1 L2 L3 Co1 Co2 Co3 Contra1 Contra2 Contra3 ::
      (_, _, _, _, _, _, _, _, _, 'f) F  _) OO
      rel_F L1' L2' L3' Co1' Co2' Co3' Contra1' Contra2' Contra3' 
    rel_F (L1 OO L1') (L2 OO L2') (L3 OO L3') (Co1 OO Co1') (Co2 OO Co2') (Co3 OO Co3')
      (Contra1 OO Contra1') (Contra2 OO Contra2') (Contra3 OO Contra3'))"

definition rel_F_neg_distr_cond :: "('co1  'co1'  bool)  ('co1'  'co1''  bool) 
    ('co2  'co2'  bool)  ('co2'  'co2''  bool) 
    ('co3  'co3'  bool)  ('co3'  'co3''  bool) 
    ('contra1  'contra1'  bool)  ('contra1'  'contra1''  bool) 
    ('contra2  'contra2'  bool)  ('contra2'  'contra2''  bool) 
    ('contra3  'contra3'  bool)  ('contra3'  'contra3''  bool) 
    ('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'l3 × 'l3' × 'l3'' × 'f) itself  bool" where
  "rel_F_neg_distr_cond Co1 Co1' Co2 Co2' Co3 Co3'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' _ 
  ((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_F (L1 OO L1') (L2 OO L2') (L3 OO L3') (Co1 OO Co1') (Co2 OO Co2') (Co3 OO Co3')
      (Contra1 OO Contra1') (Contra2 OO Contra2') (Contra3 OO Contra3') 
    (rel_F L1 L2 L3 Co1 Co2 Co3 Contra1 Contra2 Contra3 ::
      (_, _, _, _, _, _, _, _, _, 'f) F  _) OO
      rel_F L1' L2' L3' Co1' Co2' Co3' Contra1' Contra2' Contra3')"

axiomatization where
  rel_F_pos_distr_cond_eq:
  "tytok. rel_F_pos_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  and
  rel_F_neg_distr_cond_eq:
  "tytok. rel_F_neg_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) (=) tytok"

text ‹Restrictions to live variables.›

definition "rell_F L1 L2 L3 = rel_F L1 L2 L3 (=) (=) (=) (=) (=) (=)"
definition "mapl_F l1 l2 l3 = map_F l1 l2 l3 id id id id id id"

typedecl ('co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) Fbd

consts
  set1_F :: "('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F  'l1 set"
  set2_F :: "('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F  'l2 set"
  set3_F :: "('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F  'l3 set"
  bd_F :: "('co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) Fbd rel"

axiomatization where
  set1_F_map: "l1 l2 l3. set1_F  mapl_F l1 l2 l3 = image l1  set1_F" and
  set2_F_map: "l1 l2 l3. set2_F  mapl_F l1 l2 l3 = image l2  set2_F" and
  set3_F_map: "l1 l2 l3. set3_F  mapl_F l1 l2 l3 = image l3  set3_F" and
  bd_F_card_order: "card_order bd_F" and
  bd_F_cinfinite: "cinfinite bd_F" and
  bd_F_regularCard: "regularCard bd_F" and
  set1_F_bound: "x :: (_, _, _, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F.
    card_of (set1_F x) <o (bd_F :: ('co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) Fbd rel)" and
  set2_F_bound: "x :: (_, _, _, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F.
    card_of (set2_F x) <o (bd_F :: ('co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) Fbd rel)" and
  set3_F_bound: "x :: (_, _, _, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F.
    card_of (set3_F x) <o (bd_F :: ('co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) Fbd rel)" and
  mapl_F_cong: "l1 l1' l2 l2' l3 l3' x.
     z. z  set1_F x  l1 z = l1' z; z. z  set2_F x  l2 z = l2' z;
      z. z  set3_F x  l3 z = l3' z  
    mapl_F l1 l2 l3 x = mapl_F l1' l2' l3' x" and
  rell_F_mono_strong: "L1 L1' L2 L2' L3 L3' x y.
     rell_F L1 L2 L3 x y;
      a b. a  set1_F x  b  set1_F y  L1 a b  L1' a b;
      a b. a  set2_F x  b  set2_F y  L2 a b  L2' a b;
      a b. a  set3_F x  b  set3_F y  L3 a b  L3' a b  
    rell_F L1' L2' L3' x y"


subsubsection ‹Derived rules›

lemmas rel_F_mono' = rel_F_mono[THEN predicate2D, rotated -1]

lemma rel_F_eq_refl: "rel_F (=) (=) (=) (=) (=) (=) (=) (=) (=) x x"
  by (simp add: rel_F_eq)

lemma map_F_id: "map_F id id id id id id id id id x = x"
  by (simp add: map_F_id0)

lemmas map_F_rel_cong = map_F_parametric[unfolded rel_fun_def, rule_format, rotated -1]

lemma rell_F_mono: " L1  L1'; L2  L2'; L3  L3'   rell_F L1 L2 L3  rell_F L1' L2' L3'"
  unfolding rell_F_def by (rule rel_F_mono) (auto)

lemma mapl_F_id0: "mapl_F id id id = id"
  unfolding mapl_F_def using map_F_id0 .

lemma mapl_F_id: "mapl_F id id id x = x"
  by (simp add: mapl_F_id0)

lemma mapl_F_comp: "mapl_F l1 l2 l3  mapl_F l1' l2' l3' = mapl_F (l1  l1') (l2  l2') (l3  l3')"
  unfolding mapl_F_def
  apply (rule trans)
   apply (rule map_F_comp)
  apply (simp)
  done

lemma map_F_mapl_F: "map_F l1 l2 l3 co1 co2 co3 contra1 contra2 contra3 x =
  map_F id id id co1 co2 co3 contra1 contra2 contra3 (mapl_F l1 l2 l3 x)"
  unfolding mapl_F_def map_F_comp[THEN fun_cong, simplified] by simp

lemma mapl_F_map_F: "mapl_F l1 l2 l3 (map_F id id id co1 co2 co3 contra1 contra2 contra3 x) =
  map_F l1 l2 l3 co1 co2 co3 contra1 contra2 contra3 x"
  unfolding mapl_F_def map_F_comp[THEN fun_cong, simplified] by simp

lemma bd_F_Cinfinite: "Cinfinite bd_F"
  using bd_F_card_order bd_F_cinfinite card_order_on_Card_order by blast

text ‹Parametric mappers are unique:›

lemma rel_F_Grp_weak: "rel_F (Grp UNIV l1) (Grp UNIV l2) (Grp UNIV l3)
    (Grp UNIV co1) (Grp UNIV co2) (Grp UNIV co3)
    (Grp UNIV contra1)¯¯ (Grp UNIV contra2)¯¯ (Grp UNIV contra3)¯¯ =
  Grp UNIV (map_F l1 l2 l3 co1 co2 co3 contra1 contra2 contra3)"
  apply (rule antisym)
   apply (rule predicate2I)
   apply (rule GrpI)
    apply (rewrite in "_ = " map_F_id[symmetric])
    apply (subst rel_F_eq[symmetric])
    apply (erule map_F_rel_cong; simp add: Grp_def)
   apply (rule UNIV_I)
  apply (rule predicate2I)
  apply (erule GrpE)
  apply (drule sym)
  apply (hypsubst)
  apply (rewrite in "rel_F _ _ _ _ _ _ _ _ _ " map_F_id[symmetric])
  apply (rule map_F_rel_cong)
           apply (rule rel_F_eq_refl)
          apply (simp_all add: Grp_def)
  done

lemmas
  rel_F_pos_distr = rel_F_pos_distr_cond_def[THEN iffD1, rule_format] and
  rel_F_neg_distr = rel_F_neg_distr_cond_def[THEN iffD1, rule_format]

lemma rell_F_compp:
  "rell_F (L1 OO L1') (L2 OO L2') (L3 OO L3') = rell_F L1 L2 L3 OO rell_F L1' L2' L3'"
  unfolding rell_F_def
  apply (rule antisym)
   apply (rule order_trans[rotated])
    apply (rule rel_F_neg_distr)
    apply (rule rel_F_neg_distr_cond_eq)
   apply (simp add: eq_OO)
  apply (rule order_trans)
   apply (rule rel_F_pos_distr)
   apply (rule rel_F_pos_distr_cond_eq)
  apply (simp add: eq_OO)
  done


subsubsection ‹F is a BNF›

lemma rell_F_eq_onp: "rell_F (eq_onp P1) (eq_onp P2) (eq_onp P3) =
  eq_onp (λx. (zset1_F x. P1 z)  (zset2_F x. P2 z)  (zset3_F x. P3 z))"
  (is "?rel_eq_onp = ?eq_onp_pred")
proof (intro ext iffI)
  fix x y
  assume rel: "?rel_eq_onp x y"
  from rel have "rell_F (=) (=) (=) x y"
    unfolding rell_F_def by (auto elim: rel_F_mono' simp add: eq_onp_def)
  then have "y = x" unfolding rell_F_def rel_F_eq ..
  let ?true = "λ_. True" and ?label = "λP x. P x"
  from rel have "rell_F (=) (=) (=) (mapl_F ?true ?true ?true x)
    (mapl_F (?label P1) (?label P2) (?label P3) x)"
    unfolding rell_F_def mapl_F_def y = x
    by (auto simp add: eq_onp_def elim: map_F_rel_cong)
  then have *: "mapl_F ?true ?true ?true x = mapl_F (?label P1) (?label P2) (?label P3) x"
    unfolding rell_F_def rel_F_eq .
  note y = x
  moreover {
    from *
    have "set1_F (mapl_F ?true ?true ?true x) = set1_F (mapl_F (?label P1) (?label P2) (?label P3) x)"
      by simp
    then have "?true ` set1_F x = ?label P1 ` set1_F x"
      unfolding set1_F_map[THEN fun_cong, simplified] .
    then have "zset1_F x. P1 z" by auto
  }
  moreover {
    from *
    have "set2_F (mapl_F ?true ?true ?true x) = set2_F (mapl_F (?label P1) (?label P2) (?label P3) x)"
      by simp
    then have "?true ` set2_F x = ?label P2 ` set2_F x"
      unfolding set2_F_map[THEN fun_cong, simplified] .
    then have "zset2_F x. P2 z" by auto
  }
  moreover {
    from *
    have "set3_F (mapl_F ?true ?true ?true x) = set3_F (mapl_F (?label P1) (?label P2) (?label P3) x)"
      by simp
    then have "?true ` set3_F x = ?label P3 ` set3_F x"
      unfolding set3_F_map[THEN fun_cong, simplified] .
    then have "zset3_F x. P3 z" by auto
  }
  ultimately show "?eq_onp_pred x y" by (simp add: eq_onp_def)
next
  fix x y
  assume eq_onp: "?eq_onp_pred x y"
  then have "rell_F (=) (=) (=) x y"
    by (auto simp add: rell_F_def rel_F_eq eq_onp_def)
  then show "?rel_eq_onp x y"
    using eq_onp by (auto elim!: rell_F_mono_strong simp add: eq_onp_def)
qed

lemma rell_F_Grp: "rell_F (Grp A1 f1) (Grp A2 f2) (Grp A3 f3) =
  Grp {x. set1_F x  A1  set2_F x  A2  set3_F x  A3} (mapl_F f1 f2 f3)"
proof -
  have "rell_F (Grp A1 f1) (Grp A2 f2) (Grp A3 f3) = rell_F (eq_onp (λx. x  A1) OO Grp UNIV f1)
    (eq_onp (λx. x  A2) OO Grp UNIV f2) (eq_onp (λx. x  A3) OO Grp UNIV f3)"
    by (simp add: eq_onp_compp_Grp)
  also have "... = rell_F (eq_onp (λx. x  A1)) (eq_onp (λx. x  A2)) (eq_onp (λx. x  A3)) OO
    rell_F (Grp UNIV f1) (Grp UNIV f2) (Grp UNIV f3)"
    using rell_F_compp .
  also have "... = eq_onp (λx. set1_F x  A1  set2_F x  A2  set3_F x  A3) OO
    rell_F (Grp UNIV f1) (Grp UNIV f2) (Grp UNIV f3)"
    by (simp add: rell_F_eq_onp subset_eq)
  also have "... = eq_onp (λx. set1_F x  A1  set2_F x  A2  set3_F x  A3) OO
    Grp UNIV (mapl_F f1 f2 f3)"
    unfolding rell_F_def mapl_F_def
      rel_F_Grp_weak[of _ _ _ id id id id id id, folded eq_alt, simplified]
    ..
  also have "... = Grp {x. set1_F x  A1  set2_F x  A2  set3_F x  A3} (mapl_F f1 f2 f3)"
    by (simp add: eq_onp_compp_Grp)
  finally show ?thesis .
qed

lemma rell_F_compp_Grp: "rell_F L1 L2 L3 =
  (Grp {x. set1_F x  {(x, y). L1 x y}  set2_F x  {(x, y). L2 x y}  set3_F x  {(x, y). L3 x y}}
    (mapl_F fst fst fst))¯¯ OO
  Grp {x. set1_F x  {(x, y). L1 x y}  set2_F x  {(x, y). L2 x y}  set3_F x  {(x, y). L3 x y}}
    (mapl_F snd snd snd)"
  apply (unfold rell_F_Grp[symmetric])
  apply (unfold rell_F_def)
  apply (simp add: rel_F_conversep[symmetric])
  apply (fold rell_F_def)
  apply (simp add: rell_F_compp[symmetric] Grp_fst_snd)
  done

lemma F_in_rell: "rell_F L1 L2 L3 = (λx y. z. (set1_F z  {(x, y). L1 x y} 
  set2_F z  {(x, y). L2 x y}  set3_F z  {(x, y). L3 x y}) 
  mapl_F fst fst fst z = x  mapl_F snd snd snd z = y)"
  using rell_F_compp_Grp by (simp add: OO_Grp_alt)

bnf "('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F"
  map: mapl_F
  sets: set1_F set2_F set3_F
  bd: "bd_F :: ('co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) Fbd rel"
  rel: rell_F
  by (fact mapl_F_id0 mapl_F_comp[symmetric] mapl_F_cong set1_F_map set2_F_map set3_F_map
    bd_F_card_order bd_F_cinfinite bd_F_regularCard set1_F_bound set2_F_bound set3_F_bound
    rell_F_compp[symmetric, THEN eq_refl] F_in_rell)+


subsubsection ‹Composition witness›

consts
  rel_F_witness :: "('l1  'l1''  bool)  ('l2  'l2''  bool)  ('l3  'l3''  bool) 
    ('co1  'co1'  bool)  ('co1'  'co1''  bool) 
    ('co2  'co2'  bool)  ('co2'  'co2''  bool) 
    ('co3  'co3'  bool)  ('co3'  'co3''  bool) 
    ('contra1  'contra1'  bool)  ('contra1'  'contra1''  bool) 
    ('contra2  'contra2'  bool)  ('contra2'  'contra2''  bool) 
    ('contra3  'contra3'  bool)  ('contra3'  'contra3''  bool) 
    ('l1, 'l2, 'l3, 'co1, 'co2, 'co3, 'contra1, 'contra2, 'contra3, 'f) F ×
    ('l1'', 'l2'', 'l3'', 'co1'', 'co2'', 'co3'', 'contra1'', 'contra2'', 'contra3'', 'f) F 
    ('l1 × 'l1'', 'l2 × 'l2'', 'l3 × 'l3'', 'co1', 'co2', 'co3', 'contra1', 'contra2', 'contra3',
      'f) F"

specification (rel_F_witness)
  rel_F_witness1: "L1 L2 L3 Co1 Co1' Co2 Co2' Co3 Co3'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3'
    (tytok :: ('l1 × ('l1 × 'l1'') × 'l1'' × 'l2 × ('l2 × 'l2'') × 'l2'' ×
      'l3 × ('l3 × 'l3'') × 'l3'' × 'f) itself)
    (x :: ('l1, 'l2, 'l3, _, _, _, _, _, _, 'f) F)
    (y :: ('l1'', 'l2'', 'l3'', _, _, _, _, _, _, 'f) F).
     rel_F_neg_distr_cond Co1 Co1' Co2 Co2' Co3 Co3'
        Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' tytok;
      rel_F L1 L2 L3 (Co1 OO Co1') (Co2 OO Co2') (Co3 OO Co3')
          (Contra1 OO Contra1') (Contra2 OO Contra2') (Contra3 OO Contra3') x y  
    rel_F (λx (x', y). x' = x  L1 x y) (λx (x', y). x' = x  L2 x y)
    (λx (x', y). x' = x  L3 x y) Co1 Co2 Co3 Contra1 Contra2 Contra3 x
    (rel_F_witness L1 L2 L3 Co1 Co1' Co2 Co2' Co3 Co3'
      Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' (x, y))"
  rel_F_witness2:"L1 L2 L3 Co1 Co1' Co2 Co2' Co3 Co3'
    Contra1 Contra1' Contra2 Contra2' Contra3 Contra3'
    (tytok :: ('l1 × ('l1 × 'l1'') × 'l1'' × 'l2 × ('l2 × 'l2'') × 'l2'' ×
      'l3 × ('l3 × 'l3'') × 'l3'' × 'f) itself)
    (x :: ('l1, 'l2, 'l3, _, _, _, _, _, _, 'f) F)
    (y :: ('l1'', 'l2'', 'l3'', _, _, _, _, _, _, 'f) F).
     rel_F_neg_distr_cond Co1 Co1' Co2 Co2' Co3 Co3'
        Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' tytok;
      rel_F L1 L2 L3 (Co1 OO Co1') (Co2 OO Co2') (Co3 OO Co3')
          (Contra1 OO Contra1') (Contra2 OO Contra2') (Contra3 OO Contra3') x y  
    rel_F (λ(x, y') y. y' = y  L1 x y) (λ(x, y') y. y' = y  L2 x y)
    (λ(x, y') y. y' = y  L3 x y) Co1' Co2' Co3' Contra1' Contra2' Contra3'
    (rel_F_witness L1 L2 L3 Co1 Co1' Co2 Co2' Co3 Co3'
       Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' (x, y)) y"
  apply(rule exI[where x="λL1 L2 L3 Co1 Co1' Co2 Co2' Co3 Co3'
     Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' (x, y). SOME z.
     rel_F (λx (x', y). x' = x  L1 x y) (λx (x', y). x' = x  L2 x y) (λx (x', y). x' = x  L3 x y)
      Co1 Co2 Co3 Contra1 Contra2 Contra3 x z 
     rel_F (λ(x, y') y. y' = y  L1 x y) (λ(x, y') y. y' = y  L2 x y) (λ(x, y') y. y' = y  L3 x y)
      Co1' Co2' Co3' Contra1' Contra2' Contra3' z y"])
  apply(fold all_conj_distrib)
  apply(rule allI)+
  apply(fold imp_conjR)
  apply(rule impI)+
  apply clarify
  apply(rule someI_ex)
  subgoal for L1 L2 L3 Co1 Co1' Co2 Co2' Co3 Co3' Contra1 Contra1' Contra2 Contra2' Contra3 Contra3' x y
    apply(drule rel_F_neg_distr[where
          ?L1.0 = "λx (x', y). x' = x  L1 x y" and ?L1'.0 = "λ(x, y) y'. y = y'  L1 x y'" and
          ?L2.0 = "λx (x', y). x' = x  L2 x y" and ?L2'.0 = "λ(x, y) y'. y = y'  L2 x y'" and
          ?L3.0 = "λx (x', y). x' = x  L3 x y" and ?L3'.0 = "λ(x, y) y'. y = y'  L3 x y'"])
    apply(drule predicate2D)
     apply(erule rel_F_mono[THEN predicate2D, rotated -1]; fastforce)
    apply(erule relcomppE)
    apply(rule exI conjI)+
     apply assumption+
    done
  done


subsection ‹Second abstract \BNFCC{}›

subsubsection ‹Axioms and basic definitions›

typedecl ('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f) G

text @{type G} has each two live, co, and contravariant parameters, and one fixed parameter.›

consts
  rel_G :: "('l1  'l1'  bool)  ('l2  'l2'  bool) 
    ('co1  'co1'  bool)  ('co2  'co2'  bool) 
    ('contra1  'contra1'  bool)  ('contra2  'contra2'  bool) 
    ('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f) G 
    ('l1', 'l2', 'co1', 'co2', 'contra1', 'contra2', 'f) G  bool"
  map_G :: "('l1  'l1')  ('l2  'l2') 
    ('co1  'co1')  ('co2  'co2') 
    ('contra1'  'contra1)  ('contra2'  'contra2) 
    ('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f) G 
    ('l1', 'l2', 'co1', 'co2', 'contra1', 'contra2', 'f) G"

axiomatization where
  rel_G_mono [mono]:
  "L1 L1' L2 L2' Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2'.
     L1  L1'; L2  L2'; Co1  Co1'; Co2  Co2'; Contra1'  Contra1; Contra2'  Contra2  
    rel_G L1 L2 Co1 Co2 Contra1 Contra2  rel_G L1' L2' Co1' Co2' Contra1' Contra2'" and
  rel_G_eq: "rel_G (=) (=) (=) (=) (=) (=) = (=)" and
  rel_G_conversep: "L1 L2 Co1 Co2 Contra1 Contra2.
    rel_G L1¯¯ L2¯¯ Co1¯¯ Co2¯¯ Contra1¯¯ Contra2¯¯ = (rel_G L1 L2 Co1 Co2 Contra1 Contra2)¯¯" and
  map_G_id0: "map_G id id id id id id = id" and
  map_G_comp: "l1 l1' l2 l2' co1 co1' co2 co2' contra1 contra1' contra2 contra2'.
    map_G l1 l2 co1 co2 contra1 contra2  map_G l1' l2' co1' co2' contra1' contra2' =
      map_G (l1  l1') (l2  l2') (co1  co1') (co2  co2')
      (contra1'  contra1) (contra2'  contra2)" and
  map_G_parametric:
  "L1 L1' L2 L2' Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2'.
    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_G L1 L2 Co1 Co2 Contra1 Contra2)
      (rel_G L1' L2' Co1' Co2' Contra1' Contra2')))))))
      map_G map_G"

definition rel_G_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'' × 'f) itself  bool" where
  "rel_G_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_G L1 L2 Co1 Co2 Contra1 Contra2 :: (_, _, _, _, _, _, 'f) G  _) OO
      rel_G L1' L2' Co1' Co2' Contra1' Contra2' 
    rel_G (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2')
      (Contra1 OO Contra1') (Contra2 OO Contra2'))"

definition rel_G_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'' × 'f) itself  bool" where
  "rel_G_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_G (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2')
      (Contra1 OO Contra1') (Contra2 OO Contra2') 
    (rel_G L1 L2 Co1 Co2 Contra1 Contra2 :: (_, _, _, _, _, _, 'f) G  _) OO
      rel_G L1' L2' Co1' Co2' Contra1' Contra2')"

axiomatization where
  rel_G_pos_distr_cond_eq:
  "tytok. rel_G_pos_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) tytok" and
  rel_G_neg_distr_cond_eq:
  "tytok. rel_G_neg_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) tytok"

text ‹Restrictions to live variables.›

definition "rell_G L1 L2 = rel_G L1 L2 (=) (=) (=) (=)"
definition "mapl_G l1 l2 = map_G l1 l2 id id id id"

typedecl ('co1, 'co2, 'contra1, 'contra2, 'f) Gbd

consts
  set1_G :: "('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f) G  'l1 set"
  set2_G :: "('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f) G  'l2 set"
  bd_G :: "('co1, 'co2, 'contra1, 'contra2, 'f) Gbd rel"
  wit_G :: "'l2  ('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f) G"
    ― ‹non-emptiness witness for least fixpoint›

axiomatization where
  set1_G_map: "l1 l2. set1_G  mapl_G l1 l2 = image l1  set1_G" and
  set2_G_map: "l1 l2. set2_G  mapl_G l1 l2 = image l2  set2_G" and
  bd_G_card_order: "card_order bd_G" and
  bd_G_cinfinite: "cinfinite bd_G" and
  bd_G_regularCard: "regularCard bd_G" and
  set1_G_bound: "x :: (_, _, 'co1, 'co2, 'contra1, 'contra2, 'f) G.
    card_of (set1_G x) <o (bd_G :: ('co1, 'co2, 'contra1, 'contra2, 'f) Gbd rel)" and
  set2_G_bound: "x :: (_, _, 'co1, 'co2, 'contra1, 'contra2, 'f) G.
    card_of (set2_G x) <o (bd_G :: ('co1, 'co2, 'contra1, 'contra2, 'f) Gbd rel)" and
  mapl_G_cong: "l1 l1' l2 l2' l3 l3' x.
     z. z  set1_G x  l1 z = l1' z; z. z  set2_G x  l2 z = l2' z  
    mapl_G l1 l2 x = mapl_G l1' l2' x" and
  rell_G_mono_strong: "L1 L1' L2 L2' x y.
     rell_G L1 L2 x y;
      a b. a  set1_G x  b  set1_G y  L1 a b  L1' a b;
      a b. a  set2_G x  b  set2_G y  L2 a b  L2' a b  
    rell_G L1' L2' x y" and
  wit_G_set1: "l2 x. x  set1_G (wit_G l2)  False" and
  wit_G_set2: "l2 x. x  set2_G (wit_G l2)  x = l2"

lemma bd_G_Cinfinite: "Cinfinite bd_G"
  using bd_G_card_order bd_G_cinfinite card_order_on_Card_order by blast

subsubsection ‹Derived rules›

lemmas rel_G_mono' = rel_G_mono[THEN predicate2D, rotated -1]

lemma rel_G_eq_refl: "rel_G (=) (=) (=) (=) (=) (=) x x"
  by (simp add: rel_G_eq)

lemma map_G_id: "map_G id id id id id id x = x"
  by (simp add: map_G_id0)

lemmas map_G_rel_cong = map_G_parametric[unfolded rel_fun_def, rule_format, rotated -1]

lemma rell_G_mono: " L1  L1'; L2  L2'   rell_G L1 L2  rell_G L1' L2'"
  unfolding rell_G_def by (rule rel_G_mono) (auto)

lemma mapl_G_id0: "mapl_G id id = id"
  unfolding mapl_G_def using map_G_id0 .

lemma mapl_G_id: "mapl_G id id x = x"
  by (simp add: mapl_G_id0)

lemma mapl_G_comp: "mapl_G l1 l2  mapl_G l1' l2' = mapl_G (l1  l1') (l2  l2')"
  unfolding mapl_G_def
  apply (rule trans)
   apply (rule map_G_comp)
  apply (simp)
  done

lemma map_G_mapl_G:
  "map_G l1 l2 co1 co2 contra1 contra2 x = map_G id id co1 co2 contra1 contra2 (mapl_G l1 l2 x)"
  unfolding mapl_G_def map_G_comp[THEN fun_cong, simplified] by simp

lemma mapl_G_map_G:
  "mapl_G l1 l2 (map_G id id co1 co2 contra1 contra2 x) = map_G l1 l2 co1 co2 contra1 contra2 x"
  unfolding mapl_G_def map_G_comp[THEN fun_cong, simplified] by simp

text ‹Parametric mappers are unique:›

lemma rel_G_Grp_weak: "rel_G (Grp UNIV l1) (Grp UNIV l2) (Grp UNIV co1) (Grp UNIV co2)
  (Grp UNIV contra1)¯¯ (Grp UNIV contra2)¯¯ = Grp UNIV (map_G l1 l2 co1 co2 contra1 contra2)"
  apply (rule antisym)
   apply (rule predicate2I)
   apply (rule GrpI)
    apply (rewrite in "_ = " map_G_id[symmetric])
    apply (subst rel_G_eq[symmetric])
    apply (erule map_G_rel_cong; simp add: Grp_def)
   apply (rule UNIV_I)
  apply (rule predicate2I)
  apply (erule GrpE)
  apply (drule sym)
  apply (hypsubst)
  apply (rewrite in "rel_G _ _ _ _ _ _ " map_G_id[symmetric])
  apply (rule map_G_rel_cong)
        apply (rule rel_G_eq_refl)
       apply (simp_all add: Grp_def)
  done

lemmas
  rel_G_pos_distr = rel_G_pos_distr_cond_def[THEN iffD1, rule_format] and
  rel_G_neg_distr = rel_G_neg_distr_cond_def[THEN iffD1, rule_format]

lemma rell_G_compp:
  "rell_G (L1 OO L1') (L2 OO L2') = rell_G L1 L2 OO rell_G L1' L2'"
  unfolding rell_G_def
  apply (rule antisym)
   apply (rule order_trans[rotated])
    apply (rule rel_G_neg_distr)
    apply (rule rel_G_neg_distr_cond_eq)
   apply (simp add: eq_OO)
  apply (rule order_trans)
   apply (rule rel_G_pos_distr)
   apply (rule rel_G_pos_distr_cond_eq)
  apply (simp add: eq_OO)
  done


subsubsection ‹G is a BNF›

lemma rell_G_eq_onp:
  "rell_G (eq_onp P1) (eq_onp P2) = eq_onp (λx. (zset1_G x. P1 z)  (zset2_G x. P2 z))"
  (is "?rel_eq_onp = ?eq_onp_pred")
proof (intro ext iffI)
  fix x y
  assume rel: "?rel_eq_onp x y"
  from rel have "rell_G (=) (=) x y"
    unfolding rell_G_def by (auto elim: rel_G_mono' simp add: eq_onp_def)
  then have "y = x" unfolding rell_G_def rel_G_eq ..
  let ?true = "λ_. True" and ?label = "λP x. P x"
  from rel have "rell_G (=) (=) (mapl_G ?true ?true x) (mapl_G (?label P1) (?label P2) x)"
    unfolding rell_G_def mapl_G_def y = x
    by (auto simp add: eq_onp_def elim: map_G_rel_cong)
  then have *: "mapl_G ?true ?true x = mapl_G (?label P1) (?label P2) x"
    unfolding rell_G_def rel_G_eq .
  note y = x
  moreover {
    from *
    have "set1_G (mapl_G ?true ?true x) = set1_G (mapl_G (?label P1) (?label P2) x)"
      by simp
    then have "?true ` set1_G x = ?label P1 ` set1_G x"
      unfolding set1_G_map[THEN fun_cong, simplified] .
    then have "zset1_G x. P1 z" by auto
  }
  moreover {
    from *
    have "set2_G (mapl_G ?true ?true x) = set2_G (mapl_G (?label P1) (?label P2) x)"
      by simp
    then have "?true ` set2_G x = ?label P2 ` set2_G x"
      unfolding set2_G_map[THEN fun_cong, simplified] .
    then have "zset2_G x. P2 z" by auto
  }
  ultimately show "?eq_onp_pred x y" by (simp add: eq_onp_def)
next
  fix x y
  assume eq_onp: "?eq_onp_pred x y"
  then have "rell_G (=) (=) x y"
    by (auto simp add: rell_G_def rel_G_eq eq_onp_def)
  then show "?rel_eq_onp x y"
    using eq_onp by (auto elim!: rell_G_mono_strong simp add: eq_onp_def)
qed

lemma rell_G_Grp:
  "rell_G (Grp A1 f1) (Grp A2 f2) = Grp {x. set1_G x  A1  set2_G x  A2} (mapl_G f1 f2)"
proof -
  have "rell_G (Grp A1 f1) (Grp A2 f2) = rell_G (eq_onp (λx. x  A1) OO Grp UNIV f1)
    (eq_onp (λx. x  A2) OO Grp UNIV f2)"
    by (simp add: eq_onp_compp_Grp)
  also have "... = rell_G (eq_onp (λx. x  A1)) (eq_onp (λx. x  A2)) OO
    rell_G (Grp UNIV f1) (Grp UNIV f2)"
    using rell_G_compp .
  also have "... = eq_onp (λx. set1_G x  A1  set2_G x  A2) OO
    rell_G (Grp UNIV f1) (Grp UNIV f2)"
    by (simp add: rell_G_eq_onp subset_eq)
  also have "... = eq_onp (λx. set1_G x  A1  set2_G x  A2) OO Grp UNIV (mapl_G f1 f2)"
    unfolding rell_G_def mapl_G_def
      rel_G_Grp_weak[of _ _ id id id id, folded eq_alt, simplified]
    ..
  also have "... = Grp {x. set1_G x  A1  set2_G x  A2} (mapl_G f1 f2)"
    by (simp add: eq_onp_compp_Grp)
  finally show ?thesis .
qed

lemma rell_G_compp_Grp: "rell_G L1 L2 =
  (Grp {x. set1_G x  {(x, y). L1 x y}  set2_G x  {(x, y). L2 x y}} (mapl_G fst fst))¯¯ OO
  Grp {x. set1_G x  {(x, y). L1 x y}  set2_G x  {(x, y). L2 x y}} (mapl_G snd snd)"
  apply (unfold rell_G_Grp[symmetric])
  apply (unfold rell_G_def)
  apply (simp add: rel_G_conversep[symmetric])
  apply (fold rell_G_def)
  apply (simp add: rell_G_compp[symmetric] Grp_fst_snd)
  done

lemma G_in_rell: "rell_G L1 L2 = (λx y. z. (set1_G z  {(x, y). L1 x y} 
  set2_G z  {(x, y). L2 x y})  mapl_G fst fst z = x  mapl_G snd snd z = y)"
  using rell_G_compp_Grp by (simp add: OO_Grp_alt)

bnf "('l1, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f) G"
  map: mapl_G
  sets: set1_G set2_G
  bd: "bd_G :: ('co1, 'co2, 'contra1, 'contra2, 'f) Gbd rel"
  wits: wit_G
  rel: rell_G
  by (fact mapl_G_id0 mapl_G_comp[symmetric] mapl_G_cong set1_G_map set2_G_map
    bd_G_card_order bd_G_cinfinite bd_G_regularCard set1_G_bound set2_G_bound
    rell_G_compp[symmetric, THEN eq_refl] G_in_rell wit_G_set1 wit_G_set2)+


subsubsection ‹Composition witness›

consts
  rel_G_witness :: "('l1  'l1''  bool)  ('l2  'l2''  bool) 
    ('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, 'l2, 'co1, 'co2, 'contra1, 'contra2, 'f) G ×
    ('l1'', 'l2'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) G 
    ('l1 × 'l1'', 'l2 × 'l2'', 'co1', 'co2', 'contra1', 'contra2', 'f) G"

specification (rel_G_witness)
  rel_G_witness1: "L1 L2 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2'
    (tytok :: ('l1 × ('l1 × 'l1'') × 'l1'' × 'l2 × ('l2 × 'l2'') × 'l2'' × 'f) itself)
    (x :: ('l1, 'l2, _, _, _, _, 'f) G) (y :: ('l1'', 'l2'', _, _, _, _, 'f) G).
     rel_G_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok;
      rel_G L1 L2 (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y  
    rel_G (λx (x', y). x' = x  L1 x y) (λx (x', y). x' = x  L2 x y) Co1 Co2 Contra1 Contra2 x
    (rel_G_witness L1 L2 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y))"
  rel_G_witness2:"L1 L2 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2'
    (tytok :: ('l1 × ('l1 × 'l1'') × 'l1'' × 'l2 × ('l2 × 'l2'') × 'l2'' × 'f) itself)
    (x :: ('l1, 'l2, _, _, _, _, 'f) G) (y :: ('l1'', 'l2'', _, _, _, _, 'f) G).
     rel_G_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok;
      rel_G L1 L2 (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y  
    rel_G (λ(x, y') y. y' = y  L1 x y) (λ(x, y') y. y' = y  L2 x y) Co1' Co2' Contra1' Contra2'
    (rel_G_witness L1 L2 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y)) y"
  apply(rule exI[where x="λL1 L2 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y). SOME z.
     rel_G (λx (x', y). x' = x  L1 x y) (λx (x', y). x' = x  L2 x y) Co1 Co2 Contra1 Contra2 x z 
     rel_G (λ(x, y') y. y' = y  L1 x y) (λ(x, y') y. y' = y  L2 x y) Co1' Co2' Contra1' Contra2' z y"])
  apply(fold all_conj_distrib)
  apply(rule allI)+
  apply(fold imp_conjR)
  apply(rule impI)+
  apply clarify
  apply(rule someI_ex)
  subgoal for L1 L2 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' x y
    apply(drule rel_G_neg_distr[where
          ?L1.0 = "λx (x', y). x' = x  L1 x y" and ?L1'.0 = "λ(x, y) y'. y = y'  L1 x y'" and
          ?L2.0 = "λx (x', y). x' = x  L2 x y" and ?L2'.0 = "λ(x, y) y'. y = y'  L2 x y'"])
    apply(drule predicate2D)
     apply(erule rel_G_mono[THEN predicate2D, rotated -1]; fastforce)
    apply(erule relcomppE)
    apply(rule exI conjI)+
     apply assumption+
    done
  done

end