# Theory Basic_BNFs

theory Basic_BNFs
imports BNF_Def
```(*  Title:      HOL/Basic_BNFs.thy
Author:     Dmitriy Traytel, TU Muenchen
Author:     Andrei Popescu, TU Muenchen
Author:     Jasmin Blanchette, TU Muenchen

Registration of basic types as bounded natural functors.
*)

section ‹Registration of Basic Types as Bounded Natural Functors›

theory Basic_BNFs
imports BNF_Def
begin

inductive_set setl :: "'a + 'b ⇒ 'a set" for s :: "'a + 'b" where
"s = Inl x ⟹ x ∈ setl s"
inductive_set setr :: "'a + 'b ⇒ 'b set" for s :: "'a + 'b" where
"s = Inr x ⟹ x ∈ setr s"

lemma sum_set_defs[code]:
"setl = (λx. case x of Inl z ⇒ {z} | _ ⇒ {})"
"setr = (λx. case x of Inr z ⇒ {z} | _ ⇒ {})"
by (auto simp: fun_eq_iff intro: setl.intros setr.intros elim: setl.cases setr.cases split: sum.splits)

lemma rel_sum_simps[code, simp]:
"rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
"rel_sum R1 R2 (Inl a1) (Inr b2) = False"
"rel_sum R1 R2 (Inr a2) (Inl b1) = False"
"rel_sum R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
by (auto intro: rel_sum.intros elim: rel_sum.cases)

inductive
pred_sum :: "('a ⇒ bool) ⇒ ('b ⇒ bool) ⇒ 'a + 'b ⇒ bool" for P1 P2
where
"P1 a ⟹ pred_sum P1 P2 (Inl a)"
| "P2 b ⟹ pred_sum P1 P2 (Inr b)"

lemma pred_sum_inject[code, simp]:
"pred_sum P1 P2 (Inl a) ⟷ P1 a"
"pred_sum P1 P2 (Inr b) ⟷ P2 b"

bnf "'a + 'b"
map: map_sum
sets: setl setr
bd: natLeq
wits: Inl Inr
rel: rel_sum
pred: pred_sum
proof -
show "map_sum id id = id" by (rule map_sum.id)
next
fix f1 :: "'o ⇒ 's" and f2 :: "'p ⇒ 't" and g1 :: "'s ⇒ 'q" and g2 :: "'t ⇒ 'r"
show "map_sum (g1 ∘ f1) (g2 ∘ f2) = map_sum g1 g2 ∘ map_sum f1 f2"
by (rule map_sum.comp[symmetric])
next
fix x and f1 :: "'o ⇒ 'q" and f2 :: "'p ⇒ 'r" and g1 g2
assume a1: "⋀z. z ∈ setl x ⟹ f1 z = g1 z" and
a2: "⋀z. z ∈ setr x ⟹ f2 z = g2 z"
thus "map_sum f1 f2 x = map_sum g1 g2 x"
proof (cases x)
case Inl thus ?thesis using a1 by (clarsimp simp: sum_set_defs(1))
next
case Inr thus ?thesis using a2 by (clarsimp simp: sum_set_defs(2))
qed
next
fix f1 :: "'o ⇒ 'q" and f2 :: "'p ⇒ 'r"
show "setl ∘ map_sum f1 f2 = image f1 ∘ setl"
by (rule ext, unfold o_apply) (simp add: sum_set_defs(1) split: sum.split)
next
fix f1 :: "'o ⇒ 'q" and f2 :: "'p ⇒ 'r"
show "setr ∘ map_sum f1 f2 = image f2 ∘ setr"
by (rule ext, unfold o_apply) (simp add: sum_set_defs(2) split: sum.split)
next
show "card_order natLeq" by (rule natLeq_card_order)
next
show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
fix x :: "'o + 'p"
show "|setl x| ≤o natLeq"
apply (rule ordLess_imp_ordLeq)
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
by (simp add: sum_set_defs(1) split: sum.split)
next
fix x :: "'o + 'p"
show "|setr x| ≤o natLeq"
apply (rule ordLess_imp_ordLeq)
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
by (simp add: sum_set_defs(2) split: sum.split)
next
fix R1 R2 S1 S2
show "rel_sum R1 R2 OO rel_sum S1 S2 ≤ rel_sum (R1 OO S1) (R2 OO S2)"
by (force elim: rel_sum.cases)
next
fix R S
show "rel_sum R S = (λx y.
∃z. (setl z ⊆ {(x, y). R x y} ∧ setr z ⊆ {(x, y). S x y}) ∧
map_sum fst fst z = x ∧ map_sum snd snd z = y)"
unfolding sum_set_defs relcompp.simps conversep.simps fun_eq_iff
by (fastforce elim: rel_sum.cases split: sum.splits)
qed (auto simp: sum_set_defs fun_eq_iff pred_sum.simps split: sum.splits)

inductive_set fsts :: "'a × 'b ⇒ 'a set" for p :: "'a × 'b" where
"fst p ∈ fsts p"
inductive_set snds :: "'a × 'b ⇒ 'b set" for p :: "'a × 'b" where
"snd p ∈ snds p"

lemma prod_set_defs[code]: "fsts = (λp. {fst p})" "snds = (λp. {snd p})"
by (auto intro: fsts.intros snds.intros elim: fsts.cases snds.cases)

inductive
rel_prod :: "('a ⇒ 'b ⇒ bool) ⇒ ('c ⇒ 'd ⇒ bool) ⇒ 'a × 'c ⇒ 'b × 'd ⇒ bool" for R1 R2
where
"⟦R1 a b; R2 c d⟧ ⟹ rel_prod R1 R2 (a, c) (b, d)"

inductive
pred_prod :: "('a ⇒ bool) ⇒ ('b ⇒ bool) ⇒ 'a × 'b ⇒ bool" for P1 P2
where
"⟦P1 a; P2 b⟧ ⟹ pred_prod P1 P2 (a, b)"

lemma rel_prod_inject [code, simp]:
"rel_prod R1 R2 (a, b) (c, d) ⟷ R1 a c ∧ R2 b d"
by (auto intro: rel_prod.intros elim: rel_prod.cases)

lemma pred_prod_inject [code, simp]:
"pred_prod P1 P2 (a, b) ⟷ P1 a ∧ P2 b"
by (auto intro: pred_prod.intros elim: pred_prod.cases)

lemma rel_prod_conv:
"rel_prod R1 R2 = (λ(a, b) (c, d). R1 a c ∧ R2 b d)"
by (rule ext, rule ext) auto

definition
pred_fun :: "('a ⇒ bool) ⇒ ('b ⇒ bool) ⇒ ('a ⇒ 'b) ⇒ bool"
where
"pred_fun A B = (λf. ∀x. A x ⟶ B (f x))"

lemma pred_funI: "(⋀x. A x ⟹ B (f x)) ⟹ pred_fun A B f"
unfolding pred_fun_def by simp

bnf "'a × 'b"
map: map_prod
sets: fsts snds
bd: natLeq
rel: rel_prod
pred: pred_prod
proof (unfold prod_set_defs)
show "map_prod id id = id" by (rule map_prod.id)
next
fix f1 f2 g1 g2
show "map_prod (g1 ∘ f1) (g2 ∘ f2) = map_prod g1 g2 ∘ map_prod f1 f2"
by (rule map_prod.comp[symmetric])
next
fix x f1 f2 g1 g2
assume "⋀z. z ∈ {fst x} ⟹ f1 z = g1 z" "⋀z. z ∈ {snd x} ⟹ f2 z = g2 z"
thus "map_prod f1 f2 x = map_prod g1 g2 x" by (cases x) simp
next
fix f1 f2
show "(λx. {fst x}) ∘ map_prod f1 f2 = image f1 ∘ (λx. {fst x})"
by (rule ext, unfold o_apply) simp
next
fix f1 f2
show "(λx. {snd x}) ∘ map_prod f1 f2 = image f2 ∘ (λx. {snd x})"
by (rule ext, unfold o_apply) simp
next
show "card_order natLeq" by (rule natLeq_card_order)
next
show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
fix x
show "|{fst x}| ≤o natLeq"
by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
next
fix x
show "|{snd x}| ≤o natLeq"
by (rule ordLess_imp_ordLeq) (simp add: finite_iff_ordLess_natLeq[symmetric])
next
fix R1 R2 S1 S2
show "rel_prod R1 R2 OO rel_prod S1 S2 ≤ rel_prod (R1 OO S1) (R2 OO S2)" by auto
next
fix R S
show "rel_prod R S = (λx y.
∃z. ({fst z} ⊆ {(x, y). R x y} ∧ {snd z} ⊆ {(x, y). S x y}) ∧
map_prod fst fst z = x ∧ map_prod snd snd z = y)"
unfolding prod_set_defs rel_prod_inject relcompp.simps conversep.simps fun_eq_iff
by auto
qed auto

bnf "'a ⇒ 'b"
map: "(∘)"
sets: range
bd: "natLeq +c |UNIV :: 'a set|"
rel: "rel_fun (=)"
pred: "pred_fun (λ_. True)"
proof
fix f show "id ∘ f = id f" by simp
next
fix f g show "(∘) (g ∘ f) = (∘) g ∘ (∘) f"
unfolding comp_def[abs_def] ..
next
fix x f g
assume "⋀z. z ∈ range x ⟹ f z = g z"
thus "f ∘ x = g ∘ x" by auto
next
fix f show "range ∘ (∘) f = (`) f ∘ range"
next
show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
apply (rule card_order_csum)
apply (rule natLeq_card_order)
by (rule card_of_card_order_on)
(*  *)
show "cinfinite (natLeq +c ?U)"
apply (rule cinfinite_csum)
apply (rule disjI1)
by (rule natLeq_cinfinite)
next
fix f :: "'d => 'a"
have "|range f| ≤o | (UNIV::'d set) |" (is "_ ≤o ?U") by (rule card_of_image)
also have "?U ≤o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
finally show "|range f| ≤o natLeq +c ?U" .
next
fix R S
show "rel_fun (=) R OO rel_fun (=) S ≤ rel_fun (=) (R OO S)" by (auto simp: rel_fun_def)
next
fix R
show "rel_fun (=) R = (λx y.
∃z. range z ⊆ {(x, y). R x y} ∧ fst ∘ z = x ∧ snd ∘ z = y)"
unfolding rel_fun_def subset_iff by (force simp: fun_eq_iff[symmetric])
qed (auto simp: pred_fun_def)

end
```