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
(*>*)