Theory Kill

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

section ‹Removing Live Variables›

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

unbundle cardinal_syntax

declare [[bnf_internals]]
bnf_axiomatization (dead 'p, Fset1: 'a1, Fset2: 'a2, Fset3: 'a3) F for map: Fmap rel: Frel

abbreviation F1map :: "('a2  'b2)  ('a3  'b3)  ('p, 'a1, 'a2, 'a3) F  ('p, 'a1, 'b2, 'b3) F" where
  "F1map  Fmap id"
abbreviation F2map :: "('a3  'b3)  ('p, 'a1, 'a2, 'a3) F  ('p, 'a1, 'a2, 'b3) F" where
  "F2map  Fmap id id"

abbreviation "F1set1  Fset2"
abbreviation "F1set2  Fset3"
abbreviation "F2set  Fset3"


theorem F1map_id: "F1map id id = id"
  by (rule F.map_id0)

theorem F2map_id: "F2map id = id"
  by (rule F.map_id0)

theorem F1map_comp: "F1map (f1 o g1) (f2 o g2) = F1map f1 f2 o F1map g1 g2"
  by (unfold F.map_comp0[symmetric] o_id) (rule refl)

theorem F2map_comp: "F2map (f o g) = F2map f o F2map g"
  by (unfold F.map_comp0[symmetric] o_id) (rule refl)

theorem F1map_cong: "z. z  F1set1 x  f1 z = g1 z; z. z  F1set2 x  f2 z = g2 z
   F1map f1 f2 x = F1map g1 g2 x"
  apply (rule F.map_cong0)
    apply (rule refl)
   apply assumption
  apply assumption
  done

theorem F2map_cong: "z. z  F2set x  f z = g z  F2map f x = F2map g x"
  apply (rule F.map_cong0)
    apply (rule refl)
   apply (rule refl)
  apply assumption
  done

theorem F1set1_natural: "F1set1 o F1map f1 f2 = image f1 o F1set1"
  by (rule F.set_map0(2))

theorem F1set2_natural: "F1set2 o F1map f1 f2 = image f2 o F1set2"
  by (rule F.set_map0(3))

theorem F2set_natural: "F2set o F2map f = image f o F2set"
  by (rule F.set_map0(3))

abbreviation Fin :: "'a1 set  'a2 set  'a3 set  (('p, 'a1, 'a2, 'a3) F) set" where
  "Fin A1 A2 A3  {x. Fset1 x  A1  Fset2 x  A2  Fset3 x  A3}"

abbreviation F1in :: "'a2 set  'a3 set  (('p, 'a1, 'a2, 'a3) F) set" where
  "F1in A1 A2  {x. F1set1 x  A1  F1set2 x  A2}"

lemma F1in_alt: "F1in A2 A3 = Fin UNIV A2 A3"
  by (tactic BNF_Comp_Tactics.kill_in_alt_tac @{context})

abbreviation F2in :: "'a3 set  (('p, 'a1, 'a2, 'a3) F) set" where
  "F2in A  {x. F2set x  A}"

lemma F2in_alt: "F2in A3 = Fin UNIV UNIV A3"
  by (tactic BNF_Comp_Tactics.kill_in_alt_tac @{context})

lemma Frel_cong: "R1 = S1; R2 = S2; R3 = S3  Frel R1 R2 R3 = Frel S1 S2 S3"
  by hypsubst (rule refl)

definition F1rel where
  "F1rel R1 R2 = (BNF_Def.Grp (F1in (Collect (case_prod R1)) (Collect (case_prod R2))) (F1map fst fst))^--1 OO
                 (BNF_Def.Grp (F1in (Collect (case_prod R1)) (Collect (case_prod R2))) (F1map snd snd))"

lemmas F1rel_unfold = trans[OF F1rel_def trans[OF OO_Grp_cong[OF F1in_alt]
      trans[OF arg_cong2[of _ _ _ _ relcompp, OF trans[OF arg_cong[of _ _ conversep, OF sym[OF F.rel_Grp]] F.rel_conversep[symmetric]] sym[OF F.rel_Grp]]
        trans[OF F.rel_compp[symmetric] Frel_cong[OF trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]] Grp_fst_snd Grp_fst_snd]]]]]

definition F2rel where
  "F2rel R1 = (BNF_Def.Grp (F2in (Collect (case_prod R1))) (F2map fst))^--1 OO
              (BNF_Def.Grp (F2in (Collect (case_prod R1))) (F2map snd))"

lemmas F2rel_unfold = trans[OF F2rel_def trans[OF OO_Grp_cong[OF F2in_alt]
      trans[OF arg_cong2[of _ _ _ _ relcompp, OF trans[OF arg_cong[of _ _ conversep, OF sym[OF F.rel_Grp]] F.rel_conversep[symmetric]] sym[OF F.rel_Grp]]
        trans[OF F.rel_compp[symmetric] Frel_cong[OF trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]] trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]] Grp_fst_snd]]]]]

bnf F1: "('p, 'a1, 'a2, 'a3) F"
  map: F1map
  sets: F1set1 F1set2
  bd: "bd_F :: ('p bd_type_F) rel"
  rel: F1rel
             apply -
             apply (rule F1map_id)
            apply (rule F1map_comp)
           apply (erule F1map_cong) apply assumption
          apply (rule F1set1_natural)
         apply (rule F1set2_natural)
        apply (rule F.bd_card_order)
       apply (rule F.bd_cinfinite)
      apply (rule F.bd_regularCard)
     apply (rule F.set_bd(2))
    apply (rule F.set_bd(3))
   apply (unfold F1rel_unfold F.rel_compp[symmetric] eq_OO) [1] apply (rule order_refl)
  apply (rule F1rel_def[unfolded OO_Grp_alt mem_Collect_eq])
  done

bnf F2: "('p, 'a1, 'a2, 'a3) F"
  map: F2map
  sets: F2set
  bd: "bd_F :: ('p bd_type_F) rel"
  rel: F2rel
           apply -
           apply (rule F2map_id)
          apply (rule F2map_comp)
         apply (erule F2map_cong)
        apply (rule F2set_natural)
       apply (rule F.bd_card_order)
      apply (rule F.bd_cinfinite)
     apply (rule F.bd_regularCard)
    apply (rule F.set_bd(3))
   apply (unfold F2rel_unfold F.rel_compp[symmetric] eq_OO) [1] apply (rule order_refl)
  apply (rule F2rel_def[unfolded OO_Grp_alt mem_Collect_eq])
  done

(*<*)
end
(*>*)