Theory Subtypes

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

section ‹Subtypes›

theory Subtypes imports
  Axiomatised_BNF_CC
  "HOL-Library.BNF_Axiomatization"
begin

subsection ‹\BNFCC{} structure›

consts P :: "('live1, 'live2, 'co1, 'co2, 'contra1, 'contra2, 'fixed) G ⇒ bool"

axiomatization where
  P_map: "⋀x l1 l2 co1 co2 contra1 contra2. P x ⟹ P (map_G l1 l2 co1 co2 contra1 contra2 x)"
  ― ‹@{term "{x. P x}"} is closed under the mapper of @{type G}›
and
  ex_P: "∃x. P x" ― ‹@{term "{x. P x}"} is non-empty›

typedef (overloaded) ('live1, 'live2, 'co1, 'co2, 'contra1, 'contra2, 'fixed) S =
  "{x :: ('live1, 'live2, 'co1, 'co2, 'contra1, 'contra2, 'fixed) G. P x}" by (simp add: ex_P)

text ‹The subtype @{type S} is isomorphic to the set @{term "{x. P x}"}.›

context includes lifting_syntax
begin

definition rel_S :: "('live1 ⇒ 'live1' ⇒ bool) ⇒ ('live2 ⇒ 'live2' ⇒ bool) ⇒
    ('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co2 ⇒ 'co2' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra2 ⇒ 'contra2' ⇒ bool) ⇒
    ('live1, 'live2, 'co1, 'co2, 'contra1, 'contra2, 'fixed) S ⇒
    ('live1', 'live2', 'co1', 'co2', 'contra1', 'contra2', 'fixed) S ⇒ bool"
  where
    "rel_S L1 L2 Co1 Co2 Contra1 Contra2 = vimage2p Rep_S Rep_S (rel_G L1 L2 Co1 Co2 Contra1 Contra2)"

definition map_S :: "('live1 ⇒ 'live1') ⇒ ('live2 ⇒ 'live2') ⇒
    ('co1 ⇒ 'co1') ⇒ ('co2 ⇒ 'co2') ⇒
    ('contra1' ⇒ 'contra1) ⇒ ('contra2' ⇒ 'contra2) ⇒
    ('live1, 'live2, 'co1, 'co2, 'contra1, 'contra2, 'fixed) S ⇒
    ('live1', 'live2', 'co1', 'co2', 'contra1', 'contra2', 'fixed) S"
  where
    "map_S = (id ---> id ---> id ---> id ---> id ---> id ---> Rep_S ---> Abs_S) map_G"

lemma rel_S_mono:
  "⟦ L1 ≤ L1'; L2 ≤ L2'; Co1 ≤ Co1'; Co2 ≤ Co2'; Contra1' ≤ Contra1; Contra2' ≤ Contra2 ⟧
  ⟹ rel_S L1 L2 Co1 Co2 Contra1 Contra2 ≤ rel_S L1' L2' Co1' Co2' Contra1' Contra2'"
  unfolding rel_S_def
  apply(rule predicate2I)
  apply(simp add: vimage2p_def)
  by(erule rel_G_mono')

lemma rel_S_eq: "rel_S (=) (=) (=) (=) (=) (=) = (=)"
  unfolding rel_S_def by(clarsimp simp add: vimage2p_def fun_eq_iff rel_G_eq Rep_S_inject)

lemma rel_S_conversep:
  "rel_S L1¯¯ L2¯¯ Co1¯¯ Co2¯¯ Contra1¯¯ Contra2¯¯ = (rel_S L1 L2 Co1 Co2 Contra1 Contra2)¯¯"
  unfolding rel_S_def apply(simp add: vimage2p_def)
  apply(subst rel_G_conversep)
  apply(simp add: map_fun_def fun_eq_iff)
  done

lemma map_S_id0: "map_S id id id id id id = id"
  by(simp add: map_S_def fun_eq_iff map_G_id Rep_S_inverse)

lemma map_S_id: "map_S id id id id id id x = x"
  by (simp add: map_S_id0)

lemma map_S_comp:
  "map_S l1 l2 co1 co2 contra1 contra2 ∘ map_S l1' l2' co1' co2' contra1' contra2' =
  map_S (l1 ∘ l1') (l2 ∘ l2') (co1 ∘ co1') (co2 ∘ co2') (contra1' ∘ contra1) (contra2' ∘ contra2)"
  apply (rule ext)
  apply (simp add: map_S_def)
  apply (subst Abs_S_inverse)
  subgoal for x using Rep_S[of x] by(simp add: P_map)
  apply (subst map_G_comp[THEN fun_cong, simplified])
  apply simp
  done

lemma map_S_parametric:
  "((L1 ===> L1') ===> (L2 ===> L2') ===> (Co1 ===> Co1') ===> (Co2 ===> Co2') ===>
    (Contra1' ===> Contra1) ===> (Contra2' ===> Contra2) ===>
  rel_S L1 L2 Co1 Co2 Contra1 Contra2 ===> rel_S L1' L2' Co1' Co2' Contra1' Contra2')
  map_S map_S"
  apply(rule rel_funI)+
  unfolding rel_S_def map_S_def
  apply(simp add: vimage2p_def)
  apply(subst Abs_S_inverse)
  subgoal for … x _ using Rep_S[of x] by(simp add: P_map)
  apply(subst Abs_S_inverse)
  subgoal for … y using Rep_S[of y] by(simp add: P_map)
  by(erule map_G_parametric[THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD,
        THEN rel_funD, THEN rel_funD, THEN rel_funD, rotated -1])

lemmas map_S_rel_cong = map_S_parametric[unfolded rel_fun_def, rule_format, rotated -1]

end (* context includes lifting_syntax *)

definition rel_S_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_S_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_S L1 L2 Co1 Co2 Contra1 Contra2 :: (_, _, _, _, _, _, 'f) S ⇒ _) OO
      rel_S L1' L2' Co1' Co2' Contra1' Contra2' ≤
    rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2')
      (Contra1 OO Contra1') (Contra2 OO Contra2'))"

definition rel_S_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_S_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_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2')
      (Contra1 OO Contra1') (Contra2 OO Contra2') ≤
    (rel_S L1 L2 Co1 Co2 Contra1 Contra2 :: (_, _, _, _, _, _, 'f) S ⇒ _) OO
      rel_S L1' L2' Co1' Co2' Contra1' Contra2')"

axiomatization where
  rel_S_neg_distr_cond_eq:
  "⋀tytok. rel_S_neg_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) tytok"


text ‹The subtype inherits the conditions for positive subdistributivity.›

lemma rel_S_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_G :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'f) itself"
    and tytok_S :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'f) itself"
  assumes "rel_G_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_G"
  shows "rel_S_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_S"
  unfolding rel_S_pos_distr_cond_def rel_S_def
  apply(simp add: vimage2p_def)
  apply(intro allI predicate2I)
  apply(clarsimp)
  apply(rule rel_G_pos_distr[THEN predicate2D])
   apply(rule assms)
  apply(rule relcomppI)
   apply simp
  apply simp
  done

lemma rel_S_pos_distr_cond_eq:
  "⋀tytok. rel_S_pos_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  by (intro rel_S_pos_distr_imp rel_G_pos_distr_cond_eq)

lemmas
  rel_S_pos_distr = rel_S_pos_distr_cond_def[THEN iffD1, rule_format] and
  rel_S_neg_distr = rel_S_neg_distr_cond_def[THEN iffD1, rule_format]

text ‹
  The following composition witness depends only on the abstract condition
  @{const rel_S_neg_distr_cond}, without additional assumptions.
›

consts
  rel_S_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) S ×
    ('l1'', 'l2'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) S ⇒
    ('l1 × 'l1'', 'l2 × 'l2'', 'co1', 'co2', 'contra1', 'contra2', 'f) S"

specification (rel_S_witness)
  rel_S_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) S) (y :: ('l1'', 'l2'', _, _, _, _, 'f) S).
    ⟦ rel_S_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok;
      rel_S L1 L2 (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y ⟧ ⟹
    rel_S (λx (x', y). x' = x ∧ L1 x y) (λx (x', y). x' = x ∧ L2 x y) Co1 Co2 Contra1 Contra2 x
    (rel_S_witness L1 L2 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y))"
  rel_S_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) S) (y :: ('l1'', 'l2'', _, _, _, _, 'f) S).
    ⟦ rel_S_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok;
      rel_S L1 L2 (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y ⟧ ⟹
    rel_S (λ(x, y') y. y' = y ∧ L1 x y) (λ(x, y') y. y' = y ∧ L2 x y) Co1' Co2' Contra1' Contra2'
    (rel_S_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_S (λx (x', y). x' = x ∧ L1 x y) (λx (x', y). x' = x ∧ L2 x y) Co1 Co2 Contra1 Contra2 x z ∧
     rel_S (λ(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_S_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_S_mono[THEN predicate2D, rotated -1]; fastforce)
    apply(erule relcomppE)
    apply(rule exI conjI)+
     apply assumption+
    done
  done

definition set1_S :: "('live1, 'live2, 'co1, 'co2, 'contra1, 'contra2, 'fixed) S ⇒ 'live1 set"
  where "set1_S = set1_G ∘ Rep_S"

definition set2_S :: "('live1, 'live2, 'co1, 'co2, 'contra1, 'contra2, 'fixed) S ⇒ 'live2 set"
  where "set2_S = set2_G ∘ Rep_S"

lemma rel_S_alt:
  "rel_S L1 L2 (=) (=) (=) (=) x y ⟷ (∃z. (set1_S z ⊆ {(x, y). L1 x y} ∧
  set2_S z ⊆ {(x, y). L2 x y}) ∧ map_S fst fst id id id id z = x ∧ map_S snd snd id id id id z = y)"
  unfolding set1_S_def set2_S_def o_def
  apply(rule iffI)
  subgoal
    apply(subst (asm) (3 4 5 7) OO_eq[symmetric])
    apply(rule exI[where x="rel_S_witness L1 L2 (=) (=) (=) (=) (=) (=) (=) (=) (x, y)"])
    apply(frule rel_S_witness1[OF rel_S_neg_distr_cond_eq])
    apply(drule rel_S_witness2[OF rel_S_neg_distr_cond_eq])
    apply(auto simp add: rel_S_def vimage2p_def rell_G_def[symmetric])
       apply(drule (1) G.Domainp_rel[THEN eq_refl, THEN predicate1D,
          OF DomainPI, unfolded pred_G_def, THEN conjunct1, THEN bspec,
          of "conversep _" "conversep _",
          unfolded G.rel_conversep Domainp_conversep, unfolded conversep_iff])
       apply(simp add: Rangep.simps)
      apply(drule (1) G.Domainp_rel[THEN eq_refl, THEN predicate1D, OF DomainPI,
          unfolded pred_G_def, THEN conjunct2, THEN bspec, of "conversep _" "conversep _",
          unfolded G.rel_conversep Domainp_conversep, unfolded conversep_iff])
      apply(simp add: Rangep.simps)
     apply(rewrite in "_ = ⌑" map_S_id[symmetric])
     apply(rule sym)
     apply(subst rel_S_eq[symmetric])
     apply(rule map_S_parametric[THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD,
          THEN rel_funD, THEN rel_funD, THEN rel_funD, rotated -1])
           apply(simp add: rel_S_def vimage2p_def)
           apply(subst rell_G_def[symmetric])
           apply assumption
          apply(simp_all add: rel_fun_def)
    apply(rewrite in "_ = ⌑" map_S_id[symmetric])
    apply(subst rel_S_eq[symmetric])
    apply(rule map_S_parametric[THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD,
          THEN rel_funD, THEN rel_funD, THEN rel_funD, rotated -1])
          apply(simp add: rel_S_def vimage2p_def)
          apply(subst rell_G_def[symmetric])
          apply assumption
         apply(simp_all add: rel_fun_def)
    done
  subgoal
    apply(elim conjE exE)
    apply hypsubst
    apply(rule map_S_parametric[where ?L1.0="eq_onp (λ(x, y). L1 x y)" and
          ?L2.0="eq_onp (λ(x, y). L2 x y)", THEN rel_funD, THEN rel_funD, THEN rel_funD,
          THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD, rotated -1])
          apply(simp add: rel_S_def vimage2p_def)
          apply(subst rell_G_def[symmetric])
          apply(rule G.rel_refl_strong)
           apply(drule (1) subsetD)
           apply(simp add: eq_onp_def)
          apply(drule (1) subsetD)
          apply(simp add: eq_onp_def)
         apply(simp_all add: rel_fun_def eq_onp_def)
    done
  done

bnf "('live1, 'live2, 'co1, 'co2, 'contra1, 'contra2, 'fixed) S"
  map: "λl1 l2. map_S l1 l2 id id id id"
  sets: "set1_S" "set2_S"
  bd: "bd_G :: ('co1, 'co2, 'contra1, 'contra2, 'fixed) Gbd rel"
  rel: "λL1 L2. rel_S L1 L2 (=) (=) (=) (=)"
  subgoal by (rule map_S_id0)
  subgoal by (simp add: map_S_comp)
  subgoal
    apply(simp add: map_S_def set1_S_def set2_S_def)
    apply(rule arg_cong[where f="Abs_S"])
    apply(fold mapl_G_def)
    apply(rule G.map_cong[OF refl])
     apply simp_all
    done
  subgoal
    apply(simp add: set1_S_def map_S_def fun_eq_iff)
    apply(subst Abs_S_inverse)
    subgoal for x using Rep_S[of x] by(simp add: P_map)
    apply(simp add: G.set_map mapl_G_def[symmetric])
    done
  subgoal
    apply(simp add: set2_S_def map_S_def fun_eq_iff)
    apply(subst Abs_S_inverse)
    subgoal for x using Rep_S[of x] by(simp add: P_map)
    apply(simp add: G.set_map mapl_G_def[symmetric])
    done
  subgoal by(rule bd_G_card_order)
  subgoal by(rule bd_G_cinfinite)
  subgoal by(rule bd_G_regularCard)
  subgoal
    apply (simp add: set1_S_def)
    apply (rule set1_G_bound)
    done
  subgoal
    apply (simp add: set2_S_def)
    apply (rule set2_G_bound)
    done
  subgoal
    apply(subst (23 24 25 27) eq_OO[symmetric])
    apply(rule rel_S_pos_distr_cond_def[THEN iffD1, rule_format])
    apply(rule rel_S_pos_distr_imp)
    apply(rule rel_G_pos_distr_cond_eq)
    done
  subgoal
    apply(rule ext)+
    apply(rule rel_S_alt)
    done
  done


subsection ‹Closedness under zippings›

lemma P_zip_closed: ― ‹This is @{command lift_bnf}'s property that is too strong.›
  assumes "P (mapl_G fst fst z)" "P (mapl_G snd snd z)"
  shows "P z"
  oops

consts rel_S_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"

text ‹
  If the set @{term "{x. P x}"} is closed under zippings for @{const rel_S_neg_distr_cond'},
  we inherit the condition for negative subdistributivity from @{type G}.
›

axiomatization where
  P_rel_G_zipping: "⋀(L1 :: 'l1 ⇒ 'l1'' ⇒ bool) (L2 :: 'l2 ⇒ 'l2'' ⇒ bool)
    Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2'
    (tytok :: ('l1 × ('l1 × 'l1'') × 'l1'' × 'l2 × ('l2 × 'l2'') × 'l2'' × 'f) itself) x y z.
    ⟦ P x; P y;
      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 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;
      rel_S_neg_distr_cond' Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok ⟧
    ⟹ P z"
  and
  rel_S_neg_distr_cond'_stronger: "⋀Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok.
    rel_S_neg_distr_cond' Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok ⟹
    rel_G_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok"
  and
  rel_S_neg_distr_cond'_eq:
  "⋀tytok. rel_S_neg_distr_cond' (=) (=) (=) (=) (=) (=) (=) (=) tytok"

context includes lifting_syntax
begin

definition rel_S_witness' :: "('live1 ⇒ 'live1'' ⇒ bool) ⇒ ('live2 ⇒ 'live2'' ⇒ 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) ⇒
    ('live1, 'live2, 'co1, 'co2, 'contra1, 'contra2, 'fixed) S ×
    ('live1'', 'live2'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'fixed) S ⇒
    ('live1 × 'live1'', 'live2 × 'live2'', 'co1', 'co2', 'contra1', 'contra2', 'fixed) S"
  where
    "rel_S_witness' = (id ---> id ---> id ---> id ---> id ---> id --->
    id ---> id ---> id ---> id ---> map_prod Rep_S Rep_S ---> Abs_S) rel_G_witness"

lemma rel_S_witness'1:
  fixes L1 :: "'l1 ⇒ 'l1'' ⇒ bool" and L2 :: "'l2 ⇒ 'l2'' ⇒ bool"
    and 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 :: "('l1 × ('l1 × 'l1'') × 'l1'' × 'l2 × ('l2 × 'l2'') × 'l2'' × 'f) itself"
    and x :: "(_, _, _, _, _, _, 'f) S"
  assumes "rel_S L1 L2 (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y"
    and "rel_S_neg_distr_cond' Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok"
  shows "rel_S (λx (x', y). x' = x ∧ L1 x y) (λx (x', y). x' = x ∧ L2 x y) Co1 Co2 Contra1 Contra2 x
    (rel_S_witness' L1 L2 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y))"
  using assms unfolding rel_S_def rel_S_witness'_def
  apply(simp add: vimage2p_def)
  apply(subst Abs_S_inverse)
   apply(simp)
   apply(rule P_rel_G_zipping[OF Rep_S[of x, simplified] Rep_S[of y, simplified], rotated])
      apply(erule rel_G_witness1[rotated])
      apply(erule rel_S_neg_distr_cond'_stronger)
     apply(erule rel_G_witness2[rotated])
     apply(erule rel_S_neg_distr_cond'_stronger)
    apply(assumption)
   apply(assumption)
  apply(erule rel_G_witness1[rotated])
  apply(erule rel_S_neg_distr_cond'_stronger)
  done

lemma rel_S_witness'2:
  fixes L1 :: "'l1 ⇒ 'l1'' ⇒ bool" and L2 :: "'l2 ⇒ 'l2'' ⇒ bool"
    and 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 :: "('l1 × ('l1 × 'l1'') × 'l1'' × 'l2 × ('l2 × 'l2'') × 'l2'' × 'f) itself"
    and x :: "(_, _, _, _, _, _, 'f) S"
  assumes "rel_S L1 L2 (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y"
    and "rel_S_neg_distr_cond' Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok"
  shows "rel_S (λ(x, y') y. y' = y ∧ L1 x y) (λ(x, y') y. y' = y ∧ L2 x y) Co1' Co2' Contra1' Contra2'
    (rel_S_witness' L1 L2 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y)) y"
  using assms unfolding rel_S_def rel_S_witness'_def
  apply(simp add: vimage2p_def)
  apply(subst Abs_S_inverse)
   apply(simp)
   apply(rule P_rel_G_zipping[OF Rep_S[of x, simplified] Rep_S[of y, simplified], rotated])
      apply(erule rel_G_witness1[rotated])
      apply(erule rel_S_neg_distr_cond'_stronger)
     apply(erule rel_G_witness2[rotated])
     apply(erule rel_S_neg_distr_cond'_stronger)
    apply(assumption)
   apply(assumption)
  apply(erule rel_G_witness2[rotated])
  apply(erule rel_S_neg_distr_cond'_stronger)
  done

lemma rel_S_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_S' :: "('l1 × ('l1 × 'l1'') × 'l1'' × 'l2 × ('l2 × 'l2'') × 'l2'' × 'f) itself"
    and tytok_S :: "('l1 × 'l1' × 'l1'' × 'l2 × 'l2' × 'l2'' × 'f) itself"
  assumes "rel_S_neg_distr_cond' Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_S'"
  shows "rel_S_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_S"
  unfolding rel_S_neg_distr_cond_def
proof (intro allI predicate2I relcomppI)
  fix L1 :: "'l1 ⇒ 'l1' ⇒ bool" and L1' :: "'l1' ⇒ 'l1'' ⇒ bool"
    and L2 :: "'l2 ⇒ 'l2' ⇒ bool" and L2' :: "'l2' ⇒ 'l2'' ⇒ bool"
    and x :: "(_, _, _, _, _, _, 'f) S" and y :: "(_, _, _, _, _, _, 'f) S"
  assume *: "rel_S (L1 OO L1') (L2 OO L2') (Co1 OO Co1') (Co2 OO Co2')
    (Contra1 OO Contra1') (Contra2 OO Contra2') x y"
  let ?z = "map_S (relcompp_witness L1 L1') (relcompp_witness L2 L2') id id id id
    (rel_S_witness' (L1 OO L1') (L2 OO L2') Co1 Co1' Co2 Co2'
    Contra1 Contra1' Contra2 Contra2' (x, y))"
  show "rel_S L1 L2 Co1 Co2 Contra1 Contra2 x ?z"
    apply(subst map_S_id[symmetric])
    apply(rule map_S_rel_cong)
          apply(rule rel_S_witness'1[OF * assms])
         apply(auto simp add: vimage2p_def del: relcomppE elim!: relcompp_witness)
    done
  show "rel_S L1' L2' Co1' Co2' Contra1' Contra2' ?z y"
    apply(rewrite in "rel_S _ _ _ _ _ _ _ ⌑" map_S_id[symmetric])
    apply(rule map_S_rel_cong)
          apply(rule rel_S_witness'2[OF * assms])
         apply(auto simp add: vimage2p_def del: relcomppE elim!: relcompp_witness)
    done
qed

end (* context includes lifting_syntax *)


subsection ‹Subtypes of BNFs without co- and contravariance›

text ‹
  If all variables are live, @{command lift_bnf}'s requirement ‹P_zip_closed› is equivalent
  to our closedness under zippings, and Popescu's weaker condition is equivalent to negative
  subdistributivity restricted to the subset.
›

bnf_axiomatization 'a H

consts Q :: "'a H ⇒ bool"

axiomatization where
  Q_map: "⋀x l. Q x ⟹ Q (map_H l x)"

lemma Q_rel_H_zipping:
  fixes x :: "'a H" and y :: "'c H" and z :: "('a × 'c) H"
  assumes Q_zip: "⋀z :: ('a × 'c) H. ⟦ Q (map_H fst z); Q (map_H snd z) ⟧ ⟹ Q z"
    and "Q x" and "Q y" and "rel_H L x y"
    and related: "rel_H (λx (x', y). x' = x ∧ L x y) x z" "rel_H (λ(x, y') y. y' = y ∧ L x y) z y"
  shows "Q z"
proof -
  have "map_H fst z = x" proof -
    from related(1) have "rel_H (=) x (map_H fst z)"
      by (auto simp add: H.rel_map elim: H.rel_mono_strong)
    then show ?thesis by (simp add: H.rel_eq)
  qed
  moreover have "map_H snd z = y" proof -
    from related(2) have "rel_H (=) (map_H snd z) y"
      by (auto simp add: H.rel_map elim: H.rel_mono_strong)
    then show ?thesis by (simp add: H.rel_eq)
  qed
  moreover note ‹Q x› ‹Q y›
  ultimately show ?thesis using Q_zip by blast
qed

lemma Q_zip:
  fixes z :: "('a × 'c) H"
  assumes Q_rel_H_zipping: "⋀(L :: 'a ⇒ 'c ⇒ _) x y z.
      ⟦ Q x; Q y; rel_H L x y; rel_H (λx (x', y). x' = x ∧ L x y) x z;
        rel_H (λ(x, y') y. y' = y ∧ L x y) z y ⟧ ⟹ Q z"
    and "Q (map_H fst z)" and "Q (map_H snd z)"
  shows "Q z"
proof -
  let ?L = "λa (a', b). a' = a ∧ top a b" and ?L' = "λ(b, c') c. c' = c ∧ top b c"
  have *: "rel_H ?L (map_H fst z) z" "rel_H ?L' z (map_H snd z)"
    by (auto simp add: H.rel_map Grp_apply intro!: H.rel_refl_strong)
  then have "rel_H (?L OO ?L') (map_H fst z) (map_H snd z)"
    by (auto simp add: H.rel_compp)
  then have "rel_H top (map_H fst z) (map_H snd z)"
    by (simp add: relcompp_apply[abs_def] top_fun_def)
  with ‹Q (map_H fst z)› ‹Q (map_H snd z)› * show "Q z"
    using Q_rel_H_zipping by blast
qed

lemma Q_neg_distr:
  fixes x :: "'a H" and y :: "'c H"
  assumes Q_zip_weak: "⋀z :: ('a × 'c) H. ⟦ Q (map_H fst z); Q (map_H snd z) ⟧ ⟹
      ∃z'. Q z' ∧ set_H z' ⊆ set_H z ∧ map_H fst z' = map_H fst z ∧ map_H snd z' = map_H snd z"
    and "Q x" and "Q y" and related: "rel_H (L OO L') x y"
  shows "(rel_H L OO eq_onp Q OO rel_H L') x y"
proof -
  from related obtain z where
    *: "set_H z ⊆ {(x, y). (L OO L') x y}" "map_H fst z = x" "map_H snd z = y"
    unfolding H.rel_compp_Grp by (blast elim: GrpE)
  with ‹Q x› ‹Q y› have "Q (map_H fst z)" and "Q (map_H snd z)" by simp_all
  then obtain z' where "Q z'" "set_H z' ⊆ set_H z"
    "map_H fst z' = map_H fst z" "map_H snd z' = map_H snd z"
    using Q_zip_weak by blast
  with * have **: "set_H z' ⊆ {(x, y). (L OO L') x y}" "x = map_H fst z'" "y = map_H snd z'"
    by simp_all
  let ?z = "map_H (relcompp_witness L L') z'"
  from ‹Q z'› have "Q ?z" by (rule Q_map)
  moreover have "rel_H L x ?z" "rel_H L' ?z y"
    using ** by (auto simp add: H.rel_map intro!: H.rel_refl_strong
        relcompp_witness[of L L' "fst p" "snd p" for p, simplified])
  ultimately show ?thesis unfolding eq_onp_def by blast
qed

lemma Q_zip_weak:
  fixes z :: "('a × 'c) H"
  assumes Q_neg_distr: "⋀(L :: 'a ⇒ ('a × 'c) ⇒ _) (L' :: ('a × 'c) ⇒ 'c ⇒ bool) x y.
      ⟦ Q x; Q y; rel_H (L OO L') x y ⟧ ⟹ (rel_H L OO eq_onp Q OO rel_H L') x y"
    and "Q (map_H fst z)" and "Q (map_H snd z)"
  obtains z' where "Q z'" and "set_H z' ⊆ set_H z"
    and "map_H fst z' = map_H fst z" and "map_H snd z' = map_H snd z"
proof -
  let ?L = "(Grp (set_H z) fst)¯¯" and ?L' = "Grp (set_H z) snd"
  have "rel_H ?L (map_H fst z) z" "rel_H ?L' z (map_H snd z)"
    by (auto simp add: H.rel_map Grp_apply intro!: H.rel_refl_strong)
  then have "rel_H (?L OO ?L') (map_H fst z) (map_H snd z)"
    by (auto simp add: H.rel_compp)
  with ‹Q (map_H fst z)› ‹Q (map_H snd z)›
  have "(rel_H ?L OO eq_onp Q OO rel_H ?L') (map_H fst z) (map_H snd z)"
    by (rule Q_neg_distr)
  then obtain z' where "Q z'" "rel_H ?L (map_H fst z) z'" "rel_H ?L' z' (map_H snd z)"
    unfolding eq_onp_def by blast
  then have "rel_H (λa b. snd b = snd a ∧ a ∈ set_H z) z' z"
    by (simp add: H.rel_map Grp_apply)
  then have "rel_H (λa b. a ∈ set_H z) z' z"
    by (auto elim: H.rel_mono_strong)
  then have "pred_H (Domainp (λa (b :: ('a × 'c)). a ∈ set_H z)) z'"
    by (auto simp add: H.Domainp_rel[symmetric] Domainp_iff)
  then have "set_H z' ⊆ set_H z"
    unfolding H.axiom11_H by auto
  moreover have "map_H fst z' = map_H fst z"
    apply (rule sym)
    apply (subst H.rel_eq[symmetric])
    apply (subst H.rel_map(2))
    apply (rule H.rel_mono_strong)
     apply (fact ‹rel_H ?L (map_H fst z) z'›)
    apply (simp add: Grp_apply)
    done
  moreover have "map_H snd z' = map_H snd z"
    apply (subst H.rel_eq[symmetric])
    apply (subst H.rel_map(1))
    apply (rule H.rel_mono_strong)
     apply (fact ‹rel_H ?L' z' (map_H snd z)›)
    apply (simp add: Grp_apply)
    done
  moreover note ‹Q z'›
  ultimately show thesis using that by blast
qed

end