Theory Fixpoints

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

section ‹Least and greatest fixpoints›

theory Fixpoints imports
  Axiomatised_BNF_CC
begin

subsection ‹Least fixpoint›

subsubsection ‹\BNFCC{} structure›

context notes [[typedef_overloaded, bnf_internals]]
begin

datatype (set_T: 'l1, 'co1, 'co2, 'contra1, 'contra2, 'f) T =
  C_T (D_T: "(('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) T, 'l1, 'co1, 'co2, 'contra1, 'contra2, 'f) G")
  for
    map: mapl_T
    rel: rell_T

end

inductive rel_T :: "('l1 ⇒ 'l1' ⇒ bool) ⇒
    ('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co2 ⇒ 'co2' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra2 ⇒ 'contra2' ⇒ bool) ⇒
    ('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) T ⇒
    ('l1', 'co1', 'co2', 'contra1', 'contra2', 'f) T ⇒ bool"
  for L1 Co1 Co2 Contra1 Contra2 where
  "rel_T L1 Co1 Co2 Contra1 Contra2 (C_T x) (C_T y)"
    if "rel_G (rel_T L1 Co1 Co2 Contra1 Contra2) L1 Co1 Co2 Contra1 Contra2 x y"

primrec map_T :: "('l1 ⇒ 'l1') ⇒ ('co1 ⇒ 'co1') ⇒ ('co2 ⇒ 'co2') ⇒
    ('contra1' ⇒ 'contra1) ⇒ ('contra2' ⇒ 'contra2) ⇒
    ('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) T ⇒
    ('l1', 'co1', 'co2', 'contra1', 'contra2', 'f) T" where
  "map_T l1 co1 co2 contra1 contra2 (C_T x) =
    C_T (map_G id id co1 co2 contra1 contra2 (mapl_G (map_T l1 co1 co2 contra1 contra2) l1 x))"

text ‹
  The mapper and relator generated by the datatype package coincide with our generalised definitions
  restricted to live arguments.
›

lemma rell_T_alt_def: "rell_T L1 = rel_T L1 (=) (=) (=) (=)"
  apply (intro ext iffI)
   apply (erule T.rel_induct)
   apply (unfold rell_G_def)
   apply (erule rel_T.intros)
  apply (erule rel_T.induct)
  apply (rule T.rel_intros)
  apply (unfold rell_G_def)
  apply (erule rel_G_mono')
       apply (auto)
  done

lemma mapl_T_alt_def: "mapl_T l1 = map_T l1 id id id id"
  supply id_apply[simp del]
  apply (rule ext)
  subgoal for x
    apply (induction x)
    apply (simp add: mapl_G_def map_G_comp[THEN fun_cong, simplified])
    apply (fold mapl_G_def)
    apply (erule mapl_G_cong)
    apply (rule refl)
    done
  done

lemma rel_T_mono [mono]:
  "⟦ L1 ≤ L1'; Co1 ≤ Co1'; Co2 ≤ Co2'; Contra1' ≤ Contra1; Contra2' ≤ Contra2 ⟧ ⟹
  rel_T L1 Co1 Co2 Contra1 Contra2 ≤ rel_T L1' Co1' Co2' Contra1' Contra2'"
  apply (rule predicate2I)
  apply (erule rel_T.induct)
  apply (rule rel_T.intros)
  apply (erule rel_G_mono')
       apply (auto)
  done

lemma rel_T_eq: "rel_T (=) (=) (=) (=) (=) = (=)"
  unfolding rell_T_alt_def[symmetric] T.rel_eq ..

lemma rel_T_conversep:
  "rel_T L1¯¯ Co1¯¯ Co2¯¯ Contra1¯¯ Contra2¯¯ = (rel_T L1 Co1 Co2 Contra1 Contra2)¯¯"
  apply (intro ext iffI)
   apply (simp)
   apply (erule rel_T.induct)
   apply (rule rel_T.intros)
   apply (rewrite conversep_iff[symmetric])
   apply (fold rel_G_conversep)
   apply (erule rel_G_mono'; blast)
  apply (simp)
  apply (erule rel_T.induct)
  apply (rule rel_T.intros)
  apply (rewrite conversep_iff[symmetric])
  apply (unfold rel_G_conversep[symmetric] conversep_conversep)
  apply (erule rel_G_mono'; blast)
  done

lemma map_T_id0: "map_T id id id id id = id"
  unfolding mapl_T_alt_def[symmetric] T.map_id0 ..

lemma map_T_id: "map_T id id id id id x = x"
  by (simp add: map_T_id0)

lemma map_T_comp: "map_T l1 co1 co2 contra1 contra2 ∘ map_T l1' co1' co2' contra1' contra2' =
  map_T (l1 ∘ l1') (co1 ∘ co1') (co2 ∘ co2') (contra1' ∘ contra1) (contra2' ∘ contra2)"
  apply (rule ext)
  subgoal for x
    apply (induction x)
    apply (simp add: mapl_G_def map_G_comp[THEN fun_cong, simplified])
    apply (fold comp_def)
    apply (subst (1 2) map_G_mapl_G)
    apply (rule arg_cong[where f="map_G _ _ _ _ _ _"])
    apply (rule mapl_G_cong)
     apply (simp_all)
    done
  done

lemma map_T_parametric: "rel_fun (rel_fun L1 L1')
  (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_T L1 Co1 Co2 Contra1 Contra2) (rel_T L1' Co1' Co2' Contra1' Contra2'))))))
  map_T map_T"
  apply (intro rel_funI)
  apply (erule rel_T.induct)
  apply (simp)
  apply (rule rel_T.intros)
  apply (fold map_G_mapl_G)
  apply (erule map_G_rel_cong)
       apply (blast elim: rel_funE)+
  done

definition rel_T_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'' × 'f) itself ⇒ bool" where
  "rel_T_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool).
    (rel_T L1 Co1 Co2 Contra1 Contra2 :: (_, _, _, _, _, 'f) T ⇒ _) OO
      rel_T L1' Co1' Co2' Contra1' Contra2' ≤
    rel_T (L1 OO L1') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2'))"

definition rel_T_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'' × 'f) itself ⇒ bool" where
  "rel_T_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool).
    rel_T (L1 OO L1') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') ≤
    (rel_T L1 Co1 Co2 Contra1 Contra2 :: (_, _, _, _, _, 'f) T ⇒ _) OO
      rel_T L1' Co1' Co2' Contra1' Contra2')"

text ‹
  We inherit the conditions for subdistributivity over relation composition via
  a composition witness, which is derived from a witness for the underlying functor @{type G}.
›

primrec rel_T_witness :: "('l1 ⇒ 'l1'' ⇒ 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, 'co1, 'co2, 'contra1, 'contra2, 'f) T ⇒
    ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) T ⇒
    ('l1 × 'l1'', 'co1', 'co2', 'contra1', 'contra2', 'f) T" where
  "rel_T_witness L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (C_T x) Cy = C_T
  (mapl_G (λ((x, f), y). f y) id
    (rel_G_witness (λ(x, f) y. rel_T (λx (x', y). x' = x ∧ L1 x y) Co1 Co2 Contra1 Contra2 x (f y) ∧
      rel_T (λ(x, y') y. y' = y ∧ L1 x y) Co1' Co2' Contra1' Contra2' (f y) y)
    L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2'
    (mapl_G (λx. (x, rel_T_witness L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' x)) id x,
      D_T Cy)))"

lemma rel_T_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, 'co1, 'co2, 'contra1, 'contra2, 'f) T ×
      ('l1', 'co1', 'co2', 'contra1', 'contra2', 'f) T ×
      ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) T × 'l1 × 'l1' × 'l1'' × 'f) itself"
    and tytok_T :: "('l1 × 'l1' × 'l1'' × 'f) itself"
  assumes "rel_G_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_G"
  shows "rel_T_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_T"
  unfolding rel_T_pos_distr_cond_def
  apply (intro allI predicate2I)
  apply (erule relcomppE)
  subgoal premises prems for L1 L1' x z y
    using prems apply (induction arbitrary: z)
    apply (erule rel_T.cases)
    apply (simp)
    apply (rule rel_T.intros)
    apply (drule (1) rel_G_pos_distr[THEN predicate2D, OF assms relcomppI])
    apply (erule rel_G_mono'; blast)
    done
  done

lemma
  fixes L1 :: "'l1 ⇒ 'l1'' ⇒ 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_G :: "((('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) T ×
         (('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) T
          ⇒ ('l1 × 'l1'', 'co1', 'co2', 'contra1', 'contra2', 'f) T)) ×
        ((('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) T ×
          (('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) T
           ⇒ ('l1 × 'l1'', 'co1', 'co2', 'contra1', 'contra2', 'f) T)) ×
         ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) T) ×
        ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) T ×
        'l1 × ('l1 × 'l1'') × 'l1'' × 'f) itself"
    and x :: "(_, _, _, _, _, 'f) T"
  assumes cond: "rel_G_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_G"
    and rel_OO: "rel_T L1 (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y"
  shows rel_T_witness1: "rel_T (λx (x', y). x' = x ∧ L1 x y) Co1 Co2 Contra1 Contra2 x
      (rel_T_witness L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' x y)"
    and rel_T_witness2: "rel_T (λ(x, y') y. y' = y ∧ L1 x y) Co1' Co2' Contra1' Contra2'
      (rel_T_witness L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' x y) y"
  using rel_OO apply (induction)
  subgoal premises prems for x y
  proof-
    have x_expansion: "x = mapl_G fst id (mapl_G (λx.
      (x, rel_T_witness L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' x)) id x)"
      by (simp add: mapl_G_def map_G_comp[THEN fun_cong, simplified] map_G_id[unfolded id_def] comp_def)
    show ?thesis
      apply (simp)
      apply (rule rel_T.intros)
      apply (rewrite in "rel_G _ _ _ _ _ _ ⌑ _" x_expansion)
      apply (rewrite in "rel_G _ _ _ _ _ _ _ ⌑" mapl_G_def)
      apply (subst mapl_G_def)
      apply (rule map_G_rel_cong)
            apply (rule rel_G_witness1[OF cond])
            apply (rewrite in "rel_G _ _ _ _ _ _ ⌑ _" mapl_G_def)
            apply (rewrite in "rel_G _ _ _ _ _ _ _ ⌑" map_G_id[symmetric])
            apply (rule map_G_rel_cong[OF prems])
                 apply (clarsimp)+
      done
  qed
  subgoal for x y
    apply (simp)
    apply (rule rel_T.intros)
    apply (rewrite in "rel_G _ _ _ _ _ _ ⌑ _" mapl_G_def)
    apply (rewrite in "rel_G _ _ _ _ _ _ _ ⌑" map_G_id[symmetric])
    apply (rule map_G_rel_cong)
          apply (rule rel_G_witness2[OF cond[unfolded rel_T_neg_distr_cond_def]])
          apply (rewrite in "rel_G _ _ _ _ _ _ ⌑ _" mapl_G_def)
          apply (rewrite in "rel_G _ _ _ _ _ _ _ ⌑" map_G_id[symmetric])
          apply (erule map_G_rel_cong)
               apply (clarsimp)+
    done
  done

lemma rel_T_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_G :: "((('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) T ×
         (('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) T
          ⇒ ('l1 × 'l1'', 'co1', 'co2', 'contra1', 'contra2', 'f) T)) ×
        ((('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) T ×
          (('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) T
           ⇒ ('l1 × 'l1'', 'co1', 'co2', 'contra1', 'contra2', 'f) T)) ×
         ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) T) ×
        ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) T ×
        'l1 × ('l1 × 'l1'') × 'l1'' × 'f) itself"
    and tytok_T :: "('l1 × 'l1' × 'l1'' × 'f) itself"
  assumes "rel_G_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_G"
  shows "rel_T_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_T"
  unfolding rel_T_neg_distr_cond_def
proof (intro allI predicate2I relcomppI)
  fix L1 :: "'l1 ⇒ 'l1' ⇒ bool" and L1' :: "'l1' ⇒ 'l1'' ⇒ bool"
    and x :: "(_, _, _, _, _, 'f) T" and y :: "(_, _, _, _, _, 'f) T"
  assume *: "rel_T (L1 OO L1') (Co1 OO Co1') (Co2 OO Co2')
    (Contra1 OO Contra1') (Contra2 OO Contra2') x y"
  let ?z = "map_T (relcompp_witness L1 L1') id id id id
    (rel_T_witness (L1 OO L1') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' x y)"
  show "rel_T L1 Co1 Co2 Contra1 Contra2 x ?z"
    apply(subst map_T_id[symmetric])
    apply(rule map_T_parametric[unfolded rel_fun_def, rule_format, rotated -1])
         apply(rule rel_T_witness1[OF assms *])
        apply(auto simp add: vimage2p_def del: relcomppE elim!: relcompp_witness)
    done
  show "rel_T L1' Co1' Co2' Contra1' Contra2' ?z y"
    apply(rewrite in "rel_T _ _ _ _ _ _ ⌑" map_T_id[symmetric])
    apply(rule map_T_parametric[unfolded rel_fun_def, rule_format, rotated -1])
         apply(rule rel_T_witness2[OF assms *])
        apply(auto simp add: vimage2p_def del: relcomppE elim!: relcompp_witness)
    done
qed

lemma rel_T_pos_distr_cond_eq:
  "⋀tytok. rel_T_pos_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  by (intro rel_T_pos_distr_imp rel_G_pos_distr_cond_eq)

lemma rel_T_neg_distr_cond_eq:
  "⋀tytok. rel_T_neg_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  by (intro rel_T_neg_distr_imp rel_G_neg_distr_cond_eq)

text ‹The BNF axioms are proved by the datatype package.›

thm T.set_map T.bd_card_order T.bd_cinfinite T.set_bd T.map_cong[OF refl]
  T.rel_mono_strong T.wit


subsubsection ‹Parametricity laws›

context includes lifting_syntax begin

lemma C_T_parametric: "(rel_G (rel_T L1 Co1 Co2 Contra1 Contra2) L1 Co1 Co2 Contra1 Contra2 ===>
  rel_T L1 Co1 Co2 Contra1 Contra2) C_T C_T"
  by (fast elim: rel_T.intros)

lemma D_T_parametric: "(rel_T L1 Co1 Co2 Contra1 Contra2 ===>
  rel_G (rel_T L1 Co1 Co2 Contra1 Contra2) L1 Co1 Co2 Contra1 Contra2) D_T D_T"
  by (fastforce elim: rel_T.cases)

lemma rec_T_parametric:
  "((rel_G (rel_prod (rel_T L1 Co1 Co2 Contra1 Contra2) A) L1 Co1 Co2 Contra1 Contra2 ===> A) ===>
  rel_T L1 Co1 Co2 Contra1 Contra2 ===> A) rec_T rec_T"
  apply (intro rel_funI)
  subgoal premises prems for f g x y
    using prems(2) apply (induction)
    apply (simp)
    apply (rule prems(1)[THEN rel_funD])
    apply (unfold mapl_G_def)
    apply (erule map_G_rel_cong)
         apply (auto)
    done
  done

end


subsection ‹Greatest fixpoints›

subsubsection ‹\BNFCC{} structure›

context notes [[typedef_overloaded, bnf_internals]]
begin

codatatype (set_U: 'l1, 'co1, 'co2, 'contra1, 'contra2, 'f) U =
  C_U (D_U: "(('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) U, 'l1, 'co1, 'co2, 'contra1, 'contra2, 'f) G")
  for
    map: mapl_U
    rel: rell_U

end

coinductive rel_U :: "('l1 ⇒ 'l1' ⇒ bool) ⇒
    ('co1 ⇒ 'co1' ⇒ bool) ⇒ ('co2 ⇒ 'co2' ⇒ bool) ⇒
    ('contra1 ⇒ 'contra1' ⇒ bool) ⇒ ('contra2 ⇒ 'contra2' ⇒ bool) ⇒
    ('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) U ⇒
    ('l1', 'co1', 'co2', 'contra1', 'contra2', 'f) U ⇒ bool"
  for L1 Co1 Co2 Contra1 Contra2 where
  "rel_U L1 Co1 Co2 Contra1 Contra2 x y"
    if "rel_G (rel_U L1 Co1 Co2 Contra1 Contra2) L1 Co1 Co2 Contra1 Contra2 (D_U x) (D_U y)"

primcorec map_U :: "('l1 ⇒ 'l1') ⇒ ('co1 ⇒ 'co1') ⇒ ('co2 ⇒ 'co2') ⇒
    ('contra1' ⇒ 'contra1) ⇒ ('contra2' ⇒ 'contra2) ⇒
    ('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) U ⇒
    ('l1', 'co1', 'co2', 'contra1', 'contra2', 'f) U" where
  "D_U (map_U l1 co1 co2 contra1 contra2 x) =
    mapl_G (map_U l1 co1 co2 contra1 contra2) l1 (map_G id id co1 co2 contra1 contra2 (D_U x))"

lemma rell_U_alt_def: "rell_U L1 = rel_U L1 (=) (=) (=) (=)"
  apply (intro ext iffI)
   apply (erule rel_U.coinduct)
   apply (erule U.rel_cases)
   apply (simp add: rell_G_def)
   apply (erule rel_G_mono'; blast)
  apply (erule U.rel_coinduct)
  apply (erule rel_U.cases)
  apply (simp add: rell_G_def)
  done

lemma mapl_U_alt_def: "mapl_U l1 = map_U l1 id id id id"
  supply id_apply[simp del]
  apply (rule ext)
  subgoal for x
    apply (coinduction arbitrary: x)
    apply (simp add: mapl_G_def map_G_comp[THEN fun_cong, simplified] U.map_sel)
    apply (unfold rell_G_def)
    apply (rule map_G_rel_cong[OF rel_G_eq_refl])
         apply (auto)
    done
  done

lemma rel_U_mono [mono]:
  "⟦ L1 ≤ L1'; Co1 ≤ Co1'; Co2 ≤ Co2'; Contra1' ≤ Contra1; Contra2' ≤ Contra2 ⟧ ⟹
  rel_U L1 Co1 Co2 Contra1 Contra2 ≤ rel_U L1' Co1' Co2' Contra1' Contra2'"
  apply (rule predicate2I)
  apply (erule rel_U.coinduct[of "rel_U L1 Co1 Co2 Contra1 Contra2"])
  apply (erule rel_U.cases)
  apply (simp)
  apply (erule rel_G_mono')
       apply (blast)+
  done

lemma rel_U_eq: "rel_U (=) (=) (=) (=) (=) = (=)"
  unfolding rell_U_alt_def[symmetric] U.rel_eq ..

lemma rel_U_conversep:
  "rel_U L1¯¯ Co1¯¯ Co2¯¯ Contra1¯¯ Contra2¯¯ = (rel_U L1 Co1 Co2 Contra1 Contra2)¯¯"
  apply (intro ext iffI)
   apply (simp)
   apply (erule rel_U.coinduct)
   apply (erule rel_U.cases)
   apply (simp del: conversep_iff)
   apply (rewrite conversep_iff[symmetric])
   apply (fold rel_G_conversep)
   apply (erule rel_G_mono'; blast)
  apply (erule rel_U.coinduct)
  apply (subst (asm) conversep_iff)
  apply (erule rel_U.cases)
  apply (simp del: conversep_iff)
  apply (rewrite conversep_iff[symmetric])
  apply (unfold rel_G_conversep[symmetric] conversep_conversep)
  apply (erule rel_G_mono'; blast)
  done

lemma map_U_id0: "map_U id id id id id = id"
  unfolding mapl_U_alt_def[symmetric] U.map_id0 ..

lemma map_U_id: "map_U id id id id id x = x"
  by (simp add: map_U_id0)

lemma map_U_comp: "map_U l1 co1 co2 contra1 contra2 ∘ map_U l1' co1' co2' contra1' contra2' =
  map_U (l1 ∘ l1') (co1 ∘ co1') (co2 ∘ co2') (contra1' ∘ contra1) (contra2' ∘ contra2)"
  apply (rule ext)
  subgoal for x
    apply (coinduction arbitrary: x)
    apply (simp add: mapl_G_def map_G_comp[THEN fun_cong, simplified])
    apply (unfold rell_G_def)
    apply (rule map_G_rel_cong[OF rel_G_eq_refl])
         apply (auto)
    done
  done

lemma map_U_parametric: "rel_fun (rel_fun L1 L1')
  (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_U L1 Co1 Co2 Contra1 Contra2) (rel_U L1' Co1' Co2' Contra1' Contra2'))))))
  map_U map_U"
  apply (intro rel_funI)
  apply (coinduction)
  apply (simp add: mapl_G_def map_G_comp[THEN fun_cong, simplified])
  apply (erule rel_U.cases)
  apply (hypsubst)
  apply (erule map_G_rel_cong)
       apply (blast elim: rel_funE)+
  done

definition rel_U_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'' × 'f) itself ⇒ bool" where
  "rel_U_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool).
    (rel_U L1 Co1 Co2 Contra1 Contra2 :: (_, _, _, _, _, 'f) U ⇒ _) OO
      rel_U L1' Co1' Co2' Contra1' Contra2' ≤
    rel_U (L1 OO L1') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2'))"

definition rel_U_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'' × 'f) itself ⇒ bool" where
  "rel_U_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' _ ⟷
  (∀(L1 :: 'l1 ⇒ 'l1' ⇒ bool) (L1' :: 'l1' ⇒ 'l1'' ⇒ bool).
    rel_U (L1 OO L1') (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') ≤
    (rel_U L1 Co1 Co2 Contra1 Contra2 :: (_, _, _, _, _, 'f) U ⇒ _) OO
      rel_U L1' Co1' Co2' Contra1' Contra2')"

primcorec rel_U_witness :: "('l1 ⇒ 'l1'' ⇒ 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, 'co1, 'co2, 'contra1, 'contra2, 'f) U ×
    ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) U ⇒
    ('l1 × 'l1'', 'co1', 'co2', 'contra1', 'contra2', 'f) U" where
  "D_U (rel_U_witness L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' xy) =
  mapl_G (rel_U_witness L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2') id
    (rel_G_witness (rel_U L1 (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2'))
    L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (D_U (fst xy), D_U (snd xy)))"

lemma rel_U_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, 'co1, 'co2, 'contra1, 'contra2, 'f) U ×
      ('l1', 'co1', 'co2', 'contra1', 'contra2', 'f) U ×
      ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) U × 'l1 × 'l1' × 'l1'' × 'f) itself"
    and tytok_T :: "('l1 × 'l1' × 'l1'' × 'f) itself"
  assumes "rel_G_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_G"
  shows "rel_U_pos_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_T"
  unfolding rel_U_pos_distr_cond_def
  apply (intro allI predicate2I)
  apply (erule relcomppE)
  subgoal premises prems for L1 L1' x z y
    using prems apply (coinduction arbitrary: x y z)
    apply (simp)
    apply (rule rel_G_pos_distr[THEN predicate2D,
          OF assms relcomppI, THEN rel_G_mono'])
           apply (auto elim: rel_U.cases)
    done
  done

lemma rel_U_witness1:
  fixes L1 :: "'l1 ⇒ 'l1'' ⇒ 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_G :: "(('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) U ×
             (('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) U ×
              ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) U) ×
             ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) U ×
             'l1 × ('l1 × 'l1'') × 'l1'' × 'f) itself"
    and x :: "(_, _, _, _, _, 'f) U"
  assumes cond: "rel_G_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_G"
    and rel_OO: "rel_U L1 (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y"
  shows "rel_U (λx (x', y). x' = x ∧ L1 x y) Co1 Co2 Contra1 Contra2 x
      (rel_U_witness L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y))"
  using rel_OO apply (coinduction arbitrary: x y)
  apply (erule rel_U.cases)
  apply (clarsimp)
  apply (rewrite in "rel_G _ _ _ _ _ _ ⌑ _" map_G_id[symmetric])
  apply (subst mapl_G_def)
  apply (rule map_G_rel_cong)
        apply (erule rel_G_witness1[OF cond])
       apply (auto)
  done

lemma rel_U_witness2:
  fixes L1 :: "'l1 ⇒ 'l1'' ⇒ 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_G :: "(('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) U ×
             (('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) U ×
              ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) U) ×
             ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) U ×
             'l1 × ('l1 × 'l1'') × 'l1'' × 'f) itself"
    and x :: "(_, _, _, _, _, 'f) U"
  assumes cond: "rel_G_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_G"
    and rel_OO: "rel_U L1 (Co1 OO Co1') (Co2 OO Co2') (Contra1 OO Contra1') (Contra2 OO Contra2') x y"
  shows "rel_U (λ(x, y') y. y' = y ∧ L1 x y) Co1' Co2' Contra1' Contra2'
      (rel_U_witness L1 Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y)) y"
  using rel_OO apply (coinduction arbitrary: x y)
  apply (erule rel_U.cases)
  apply (clarsimp)
  apply (rewrite in "rel_G _ _ _ _ _ _ _ ⌑" map_G_id[symmetric])
  apply (subst mapl_G_def)
  apply (rule map_G_rel_cong)
        apply (erule rel_G_witness2[OF cond])
       apply (auto)
  done

lemma rel_U_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_G :: "(('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) U ×
          (('l1, 'co1, 'co2, 'contra1, 'contra2, 'f) U ×
           ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) U) ×
          ('l1'', 'co1'', 'co2'', 'contra1'', 'contra2'', 'f) U ×
          'l1 × ('l1 × 'l1'') × 'l1'' × 'f) itself"
    and tytok_T :: "('l1 × 'l1' × 'l1'' × 'f) itself"
  assumes "rel_G_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_G"
  shows "rel_U_neg_distr_cond Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' tytok_T"
  unfolding rel_U_neg_distr_cond_def
proof (intro allI predicate2I relcomppI)
  fix L1 :: "'l1 ⇒ 'l1' ⇒ bool" and L1' :: "'l1' ⇒ 'l1'' ⇒ bool"
    and x :: "(_, _, _, _, _, 'f) U" and y :: "(_, _, _, _, _, 'f) U"
  assume *: "rel_U (L1 OO L1') (Co1 OO Co1') (Co2 OO Co2')
    (Contra1 OO Contra1') (Contra2 OO Contra2') x y"
  let ?z = "map_U (relcompp_witness L1 L1') id id id id
    (rel_U_witness (L1 OO L1') Co1 Co1' Co2 Co2' Contra1 Contra1' Contra2 Contra2' (x, y))"
  show "rel_U L1 Co1 Co2 Contra1 Contra2 x ?z"
    apply(subst map_U_id[symmetric])
    apply(rule map_U_parametric[unfolded rel_fun_def, rule_format, rotated -1])
         apply(rule rel_U_witness1[OF assms *])
        apply(auto simp add: vimage2p_def del: relcomppE elim!: relcompp_witness)
    done
  show "rel_U L1' Co1' Co2' Contra1' Contra2' ?z y"
    apply(rewrite in "rel_U _ _ _ _ _ _ ⌑" map_U_id[symmetric])
    apply(rule map_U_parametric[unfolded rel_fun_def, rule_format, rotated -1])
         apply(rule rel_U_witness2[OF assms *])
        apply(auto simp add: vimage2p_def del: relcomppE elim!: relcompp_witness)
    done
qed

lemma rel_U_pos_distr_cond_eq:
  "⋀tytok. rel_U_pos_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  by (intro rel_U_pos_distr_imp rel_G_pos_distr_cond_eq)

lemma rel_U_neg_distr_cond_eq:
  "⋀tytok. rel_U_neg_distr_cond (=) (=) (=) (=) (=) (=) (=) (=) tytok"
  by (intro rel_U_neg_distr_imp rel_G_neg_distr_cond_eq)

text ‹The BNF axioms are proved by the datatype package.›

thm U.set_map U.bd_card_order U.bd_cinfinite U.set_bd U.map_cong[OF refl]
  U.rel_mono_strong U.wit


subsubsection ‹Parametricity laws›

context includes lifting_syntax begin

lemma C_U_parametric: "(rel_G (rel_U L1 Co1 Co2 Contra1 Contra2) L1 Co1 Co2 Contra1 Contra2 ===>
  rel_U L1 Co1 Co2 Contra1 Contra2) C_U C_U"
  by (fastforce intro: rel_U.intros)

lemma D_U_parametric: "(rel_U L1 Co1 Co2 Contra1 Contra2 ===>
  rel_G (rel_U L1 Co1 Co2 Contra1 Contra2) L1 Co1 Co2 Contra1 Contra2) D_U D_U"
  by (fast elim: rel_U.cases)

lemma corec_U_parametric:
  "((A ===> rel_G (rel_sum (rel_U L1 Co1 Co2 Contra1 Contra2) A) L1 Co1 Co2 Contra1 Contra2) ===>
  A ===> rel_U L1 Co1 Co2 Contra1 Contra2) corec_U corec_U"
  apply (intro rel_funI)
  subgoal premises prems for f g x y
    using prems(2) apply (coinduction arbitrary: x y)
    apply (simp)
    apply (unfold mapl_G_def)
    apply (rule map_G_rel_cong)
          apply (erule prems(1)[THEN rel_funD])
         apply (fastforce elim: rel_sum.cases)
        apply (simp_all)
    done
  done

end

end