Theory Compose

(*  Title:       Compose
    Authors:     Jasmin Blanchette, Andrei Popescu, Dmitriy Traytel
    Maintainer:  Dmitriy Traytel <traytel at inf.ethz.ch>
*)

section ‹Normalized Composition of BNFs›

text ‹Expected normal form: outer m-ary BNF is composed with m inner n-ary BNFs.›

(*<*)
theory Compose
  imports "HOL-Library.BNF_Axiomatization"
begin
(*>*)

unbundle cardinal_syntax

declare [[bnf_internals]]
bnf_axiomatization (dead 'p1, F1set1: 'a1, F1set2: 'a2) F1
  [wits: "('p1, 'a1, 'a2) F1"]
  for map: F1map rel: F1rel
bnf_axiomatization (dead 'p2, F2set1: 'a1, F2set2: 'a2) F2
  [wits: "'a1 ⇒ ('p2, 'a1, 'a2) F2" "'a2 ⇒ ('p2, 'a1, 'a2) F2"]
  for map: F2map rel: F2rel
bnf_axiomatization (dead 'p3, F3set1: 'a1, F3set2: 'a2) F3
  [wits: "'a1 ⇒ 'a2 ⇒ ('p3, 'a1, 'a2) F3"]
  for map: F3map rel: F3rel
bnf_axiomatization (dead 'p, Gset1: 'b1, Gset2: 'b2, Gset3: 'b3) G
  [wits: "'b1 ⇒ 'b3 ⇒ ('p, 'b1, 'b2, 'b3) G" "'b2 ⇒ 'b3 ⇒ ('p, 'b1, 'b2, 'b3) G"]
  for map: Gmap rel: Grel
type_synonym ('p1, 'p2, 'p3, 'p, 'a1, 'a2) H =
  "('p, ('p1, 'a1, 'a2) F1, ('p2, 'a1, 'a2) F2, ('p3, 'a1, 'a2) F3) G"
type_synonym ('p1, 'p2, 'p3, 'p) Hbd_type =
  "('p1 bd_type_F1 + 'p2 bd_type_F2 + 'p3 bd_type_F3) × 'p bd_type_G"

abbreviation F1in where "F1in A1 A2 ≡ {x. F1set1 x ⊆ A1 ∧ F1set2 x ⊆ A2}"
abbreviation F2in where "F2in A1 A2 ≡ {x. F2set1 x ⊆ A1 ∧ F2set2 x ⊆ A2}"
abbreviation F3in where "F3in A1 A2 ≡ {x. F3set1 x ⊆ A1 ∧ F3set2 x ⊆ A2}"
abbreviation Gin where "Gin A1 A2 A3 ≡ {x. Gset1 x ⊆ A1 ∧ Gset2 x ⊆ A2 ∧ Gset3 x ⊆ A3}"

abbreviation Gset where
  "Gset ≡ BNF_Def.collect {Gset1, Gset2, Gset3}"

abbreviation Hmap :: "('a1 ⇒ 'b1) ⇒ ('a2 ⇒ 'b2) ⇒
  ('p1, 'p2, 'p3, 'p, 'a1, 'a2) H ⇒ ('p1, 'p2, 'p3, 'p, 'b1, 'b2) H" where
  "Hmap f g ≡ Gmap (F1map f g) (F2map f g) (F3map f g)"

abbreviation Hset1 :: "('p1, 'p2, 'p3, 'p, 'a1, 'a2) H ⇒ 'a1 set" where
  "Hset1 ≡ Union o Gset o Gmap F1set1 F2set1 F3set1"

abbreviation Hset2 :: "('p1, 'p2, 'p3, 'p, 'a1, 'a2) H ⇒ 'a2 set" where
  "Hset2 ≡ Union o Gset o Gmap F1set2 F2set2 F3set2"

lemma Hset1_alt:
  "Hset1 = Union o BNF_Def.collect {image F1set1 o Gset1, image F2set1 o Gset2, image F3set1 o Gset3}"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_set_alt_tac @{context} @{thm G.collect_set_map}›)

lemma Hset2_alt:
  "Hset2 = Union o BNF_Def.collect {image F1set2 o Gset1, image F2set2 o Gset2, image F3set2 o Gset3}"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_set_alt_tac @{context} @{thm G.collect_set_map}›)

abbreviation Hbd where
  "Hbd ≡ (bd_F1 +c bd_F2 +c bd_F3) *c bd_G"

theorem Hmap_id: "Hmap id id = id"
  unfolding G.map_id0 F1.map_id0 F2.map_id0 F3.map_id0 ..

theorem Hmap_comp: "Hmap (f1 o g1) (f2 o g2) = Hmap f1 f2 o Hmap g1 g2"
  unfolding G.map_comp0 F1.map_comp0 F2.map_comp0 F3.map_comp0 ..

theorem Hmap_cong: "⟦⋀z. z ∈ Hset1 x ⟹ f1 z = g1 z; ⋀z. z ∈ Hset2 x ⟹ f2 z = g2 z⟧ ⟹
  Hmap f1 f2 x = Hmap g1 g2 x"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_map_cong0_tac @{context}
  [] @{thms Hset1_alt Hset2_alt} @{thm G.map_cong0} @{thms F1.map_cong0 F2.map_cong0 F3.map_cong0}›)

theorem Hset1_natural: "Hset1 o Hmap f1 f2 = image f1 o Hset1"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_set_map0_tac @{context} @{thm refl} @{thm G.map_comp0} @{thm G.map_cong0}
  @{thm G.collect_set_map} @{thms F1.set_map0(1) F2.set_map0(1) F3.set_map0(1)}›)

theorem Hset2_natural: "Hset2 o Hmap f1 f2 = image f2 o Hset2"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_set_map0_tac @{context} @{thm refl} @{thm G.map_comp0} @{thm G.map_cong0}
  @{thm G.collect_set_map} @{thms F1.set_map0(2) F2.set_map0(2) F3.set_map0(2)}›)

theorem Hbd_card_order: "card_order Hbd"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_bd_card_order_tac @{context}
  @{thms F1.bd_card_order F2.bd_card_order F3.bd_card_order} @{thm G.bd_card_order}›)

theorem Hbd_cinfinite: "cinfinite Hbd"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_bd_cinfinite_tac @{context}
  @{thm F1.bd_cinfinite} @{thm G.bd_cinfinite}›)

theorem Hbd_regularCard: "regularCard Hbd"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_bd_regularCard_tac @{context}
  @{thms F1.bd_regularCard F2.bd_regularCard F3.bd_regularCard} @{thm G.bd_regularCard}
  @{thms F1.bd_Cinfinite F2.bd_Cinfinite F3.bd_Cinfinite} @{thm G.bd_Cinfinite}›)

theorem Hset1_bd: "|Hset1 (x :: ('p1, 'p2, 'p3, 'p, 'a1, 'a2) H )| <o
  (Hbd :: ('p1, 'p2, 'p3, 'p) Hbd_type rel)"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_set_bd_tac @{context} @{thm refl} NONE @{thm Hset1_alt}
      @{thms comp_single_set_bd_strict[OF F1.bd_Cinfinite F1.bd_regularCard G.bd_Cinfinite
               G.bd_regularCard F1.set_bd(1) G.set_bd(1)]
             comp_single_set_bd_strict[OF F2.bd_Cinfinite F2.bd_regularCard G.bd_Cinfinite
               G.bd_regularCard F2.set_bd(1) G.set_bd(2)]
             comp_single_set_bd_strict[OF F3.bd_Cinfinite F3.bd_regularCard G.bd_Cinfinite
               G.bd_regularCard F3.set_bd(1) G.set_bd(3)]}
      @{thms Cinfinite_cprod2[OF Cinfinite_Cnotzero[OF G.bd_Cinfinite] F1.bd_Cinfinite]
             Cinfinite_cprod2[OF Cinfinite_Cnotzero[OF G.bd_Cinfinite] F2.bd_Cinfinite]
             Cinfinite_cprod2[OF Cinfinite_Cnotzero[OF G.bd_Cinfinite] F3.bd_Cinfinite]}›)

theorem Hset2_bd: "|Hset2 (x :: ('p1, 'p2, 'p3, 'p, 'a1, 'a2) H )| <o
  (Hbd :: ('p1, 'p2, 'p3, 'p) Hbd_type rel)"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_set_bd_tac @{context} @{thm refl} NONE @{thm Hset2_alt}
      @{thms comp_single_set_bd_strict[OF F1.bd_Cinfinite F1.bd_regularCard G.bd_Cinfinite
               G.bd_regularCard F1.set_bd(2) G.set_bd(1)]
             comp_single_set_bd_strict[OF F2.bd_Cinfinite F2.bd_regularCard G.bd_Cinfinite
               G.bd_regularCard F2.set_bd(2) G.set_bd(2)]
             comp_single_set_bd_strict[OF F3.bd_Cinfinite F3.bd_regularCard G.bd_Cinfinite
               G.bd_regularCard F3.set_bd(2) G.set_bd(3)]}
      @{thms Cinfinite_cprod2[OF Cinfinite_Cnotzero[OF G.bd_Cinfinite] F1.bd_Cinfinite]
             Cinfinite_cprod2[OF Cinfinite_Cnotzero[OF G.bd_Cinfinite] F2.bd_Cinfinite]
             Cinfinite_cprod2[OF Cinfinite_Cnotzero[OF G.bd_Cinfinite] F3.bd_Cinfinite]}›)

abbreviation Hin where "Hin A1 A2 ≡ {x. Hset1 x ⊆ A1 ∧ Hset2 x ⊆ A2}"

lemma Hin_alt: "Hin A1 A2 = Gin (F1in A1 A2) (F2in A1 A2) (F3in A1 A2)"
  by (tactic ‹BNF_Comp_Tactics.mk_comp_in_alt_tac @{context} @{thms Hset1_alt Hset2_alt}›)

definition Hwit1 where "Hwit1 b c = wit1_G wit_F1 (wit_F3 b c)"
definition Hwit21 where "Hwit21 b c = wit2_G (wit1_F2 b) (wit_F3 b c)"
definition Hwit22 where "Hwit22 b c = wit2_G (wit2_F2 c) (wit_F3 b c)"

lemma Hwit1:
  "⋀x. x ∈ Hset1 (Hwit1 b c) ⟹ x = b"
  "⋀x. x ∈ Hset2 (Hwit1 b c) ⟹ x = c"
  unfolding Hwit1_def
  by (tactic ‹BNF_Comp_Tactics.mk_comp_wit_tac @{context} [] @{thms G.wit1 G.wit2}
  @{thm G.collect_set_map} @{thms F1.wit F2.wit1 F2.wit2 F3.wit}›)

lemma Hwit21:
  "⋀x. x ∈ Hset1 (Hwit21 b c) ⟹ x = b"
  "⋀x. x ∈ Hset2 (Hwit21 b c) ⟹ x = c"
  unfolding Hwit21_def
  by (tactic ‹BNF_Comp_Tactics.mk_comp_wit_tac @{context} [] @{thms G.wit1 G.wit2}
  @{thm G.collect_set_map} @{thms F1.wit F2.wit1 F2.wit2 F3.wit}›)


lemma Hwit22:
  "⋀x. x ∈ Hset1 (Hwit22 b c) ⟹ x = b"
  "⋀x. x ∈ Hset2 (Hwit22 b c) ⟹ x = c"
  unfolding Hwit22_def
  by (tactic ‹BNF_Comp_Tactics.mk_comp_wit_tac @{context} [] @{thms G.wit1 G.wit2}
  @{thm G.collect_set_map} @{thms F1.wit F2.wit1 F2.wit2 F3.wit}›)

(* Relator structure for H *)

lemma Grel_cong: "⟦R1 = S1; R2 = S2; R3 = S3⟧ ⟹ Grel R1 R2 R3 = Grel S1 S2 S3"
  by hypsubst (rule refl)

definition Hrel where
  "Hrel R1 R2 = (BNF_Def.Grp (Hin (Collect (case_prod R1)) (Collect (case_prod R2))) (Hmap fst fst))^--1 OO
                (BNF_Def.Grp (Hin (Collect (case_prod R1)) (Collect (case_prod R2))) (Hmap snd snd))"

lemmas Hrel_unfold = trans[OF Hrel_def trans[OF OO_Grp_cong[OF Hin_alt]
      trans[OF arg_cong2[of _ _ _ _ relcompp, OF trans[OF arg_cong[of _ _ conversep, OF sym[OF G.rel_Grp]] G.rel_conversep[symmetric]] sym[OF G.rel_Grp]]
        trans[OF G.rel_compp[symmetric] Grel_cong[OF sym[OF F1.rel_compp_Grp] sym[OF F2.rel_compp_Grp] sym[OF F3.rel_compp_Grp]]]]]]

bnf H: "('p1, 'p2, 'p3, 'p, 'a1, 'a2) H"
  map: Hmap
  sets: Hset1 Hset2
  bd: "Hbd :: ('p1, 'p2, 'p3, 'p) Hbd_type rel"
  rel: Hrel
             apply -
             apply (rule Hmap_id)
            apply (rule Hmap_comp)
           apply (erule Hmap_cong) apply assumption
          apply (rule Hset1_natural)
         apply (rule Hset2_natural)
        apply (rule Hbd_card_order)
       apply (rule Hbd_cinfinite)
      apply (rule Hbd_regularCard)
     apply (rule Hset1_bd)
    apply (rule Hset2_bd)
   apply (unfold Hrel_unfold G.rel_compp[symmetric] F1.rel_compp[symmetric] F2.rel_compp[symmetric] F3.rel_compp[symmetric] eq_OO) [1] apply (rule order_refl)
  apply (rule Hrel_def[unfolded OO_Grp_alt mem_Collect_eq])
  done

(*<*)
end
(*>*)