Theory Basic_BNF_LFPs

(*  Title:      HOL/Basic_BNF_LFPs.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2014

Registration of basic types as BNF least fixpoints (datatypes).
*)

theory Basic_BNF_LFPs
imports BNF_Least_Fixpoint
begin

definition xtor :: "'a ⇒ 'a" where
  "xtor x = x"

lemma xtor_map: "f (xtor x) = xtor (f x)"
  unfolding xtor_def by (rule refl)

lemma xtor_map_unique: "u ∘ xtor = xtor ∘ f ⟹ u = f"
  unfolding o_def xtor_def .

lemma xtor_set: "f (xtor x) = f x"
  unfolding xtor_def by (rule refl)

lemma xtor_rel: "R (xtor x) (xtor y) = R x y"
  unfolding xtor_def by (rule refl)

lemma xtor_induct: "(⋀x. P (xtor x)) ⟹ P z"
  unfolding xtor_def by assumption

lemma xtor_xtor: "xtor (xtor x) = x"
  unfolding xtor_def by (rule refl)

lemmas xtor_inject = xtor_rel[of "(=)"]

lemma xtor_rel_induct: "(⋀x y. vimage2p id_bnf id_bnf R x y ⟹ IR (xtor x) (xtor y)) ⟹ R ≤ IR"
  unfolding xtor_def vimage2p_def id_bnf_def ..

lemma xtor_iff_xtor: "u = xtor w ⟷ xtor u = w"
  unfolding xtor_def ..

lemma Inl_def_alt: "Inl ≡ (λa. xtor (id_bnf (Inl a)))"
  unfolding xtor_def id_bnf_def by (rule reflexive)

lemma Inr_def_alt: "Inr ≡ (λa. xtor (id_bnf (Inr a)))"
  unfolding xtor_def id_bnf_def by (rule reflexive)

lemma Pair_def_alt: "Pair ≡ (λa b. xtor (id_bnf (a, b)))"
  unfolding xtor_def id_bnf_def by (rule reflexive)

definition ctor_rec :: "'a ⇒ 'a" where
  "ctor_rec x = x"

lemma ctor_rec: "g = id ⟹ ctor_rec f (xtor x) = f ((id_bnf ∘ g ∘ id_bnf) x)"
  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)

lemma ctor_rec_unique: "g = id ⟹ f ∘ xtor = s ∘ (id_bnf ∘ g ∘ id_bnf) ⟹ f = ctor_rec s"
  unfolding ctor_rec_def id_bnf_def xtor_def comp_def id_def by hypsubst (rule refl)

lemma ctor_rec_def_alt: "f = ctor_rec (f ∘ id_bnf)"
  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)

lemma ctor_rec_o_map: "ctor_rec f ∘ g = ctor_rec (f ∘ (id_bnf ∘ g ∘ id_bnf))"
  unfolding ctor_rec_def id_bnf_def comp_def by (rule refl)

lemma ctor_rec_transfer: "rel_fun (rel_fun (vimage2p id_bnf id_bnf R) S) (rel_fun R S) ctor_rec ctor_rec"
  unfolding rel_fun_def vimage2p_def id_bnf_def ctor_rec_def by simp

lemma eq_fst_iff: "a = fst p ⟷ (∃b. p = (a, b))"
  by (cases p) auto

lemma eq_snd_iff: "b = snd p ⟷ (∃a. p = (a, b))"
  by (cases p) auto

lemma ex_neg_all_pos: "((∃x. P x) ⟹ Q) ≡ (⋀x. P x ⟹ Q)"
  by standard blast+

lemma hypsubst_in_prems: "(⋀x. y = x ⟹ z = f x ⟹ P) ≡ (z = f y ⟹ P)"
  by standard blast+

lemma isl_map_sum:
  "isl (map_sum f g s) = isl s"
  by (cases s) simp_all

lemma map_sum_sel:
  "isl s ⟹ projl (map_sum f g s) = f (projl s)"
  "¬ isl s ⟹ projr (map_sum f g s) = g (projr s)"
  by (cases s; simp)+

lemma set_sum_sel:
  "isl s ⟹ projl s ∈ setl s"
  "¬ isl s ⟹ projr s ∈ setr s"
  by (cases s; auto intro: setl.intros setr.intros)+

lemma rel_sum_sel: "rel_sum R1 R2 a b = (isl a = isl b ∧
  (isl a ⟶ isl b ⟶ R1 (projl a) (projl b)) ∧
  (¬ isl a ⟶ ¬ isl b ⟶ R2 (projr a) (projr b)))"
  by (cases a b rule: sum.exhaust[case_product sum.exhaust]) simp_all

lemma isl_transfer: "rel_fun (rel_sum A B) (=) isl isl"
  unfolding rel_fun_def rel_sum_sel by simp

lemma rel_prod_sel: "rel_prod R1 R2 p q = (R1 (fst p) (fst q) ∧ R2 (snd p) (snd q))"
  by (force simp: rel_prod.simps elim: rel_prod.cases)

ML_file ‹Tools/BNF/bnf_lfp_basic_sugar.ML›

declare prod.size [no_atp]

hide_const (open) xtor ctor_rec

hide_fact (open)
  xtor_def xtor_map xtor_set xtor_rel xtor_induct xtor_xtor xtor_inject ctor_rec_def ctor_rec
  ctor_rec_def_alt ctor_rec_o_map xtor_rel_induct Inl_def_alt Inr_def_alt Pair_def_alt

end