Theory Lift_BNF

theory Lift_BNF
imports Main
begin

typedef 'a nonempty_list = "{xs :: 'a list. xs ≠ []}"
  by blast

lift_bnf (no_warn_wits) (neset: 'a) nonempty_list
  for map: nemap rel: nerel
  by simp_all

typedef ('a :: finite, 'b) fin_nonempty_list = "{(xs :: 'a set, ys :: 'b list). ys ≠ []}"
  by blast

lift_bnf (dead 'a :: finite, 'b) fin_nonempty_list
  by auto

datatype 'a tree = Leaf | Node 'a "'a tree nonempty_list"

record 'a point =
  xCoord :: 'a
  yCoord :: 'a

copy_bnf ('a, 's) point_ext

typedef 'a it = "UNIV :: 'a set"
  by blast

copy_bnf (plugins del: size) 'a it

typedef ('a, 'b) T_prod = "UNIV :: ('a × 'b) set"
  by blast

copy_bnf ('a, 'b) T_prod

typedef ('a, 'b, 'c) T_func = "UNIV :: ('a ⇒ 'b * 'c) set"
  by blast

copy_bnf ('a, 'b, 'c) T_func

typedef ('a, 'b) sum_copy = "UNIV :: ('a + 'b) set"
  by blast

copy_bnf ('a, 'b) sum_copy

typedef ('a, 'b) T_sum = "{Inl x | x. True} :: ('a + 'b) set"
  by blast

lift_bnf (no_warn_wits) ('a, 'b) T_sum [wits: "Inl :: 'a ⇒ 'a + 'b"]
  by (auto simp: map_sum_def sum_set_defs split: sum.splits)

typedef ('key, 'value) alist = "{xs :: ('key × 'value) list. (distinct ∘ map fst) xs}"
  morphisms impl_of Alist
proof
  show "[] ∈ {xs. (distinct o map fst) xs}"
    by simp
qed

lift_bnf (dead 'k, 'v) alist [wits: "Nil :: ('k × 'v) list"]
  by simp_all

typedef 'a myopt = "{X :: 'a set. finite X ∧ card X ≤ 1}" by (rule exI[of _ "{}"]) auto
lemma myopt_type_def: "type_definition
  (λX. if card (Rep_myopt X) = 1 then Some (the_elem (Rep_myopt X)) else None)
  (λx. Abs_myopt (case x of Some x ⇒ {x} | _ ⇒ {}))
  (UNIV :: 'a option set)"
  apply unfold_locales
    apply (auto simp: Abs_myopt_inverse dest!: card_eq_SucD split: option.splits)
   apply (metis Rep_myopt_inverse)
  apply (metis One_nat_def Rep_myopt Rep_myopt_inverse Suc_le_mono card_0_eq le0 le_antisym mem_Collect_eq nat.exhaust)
  done

copy_bnf 'a myopt via myopt_type_def

typedef ('k, 'v) fmap = "{M :: ('k ⇀ 'v). finite (dom M)}"
  by (rule exI[of _ Map.empty]) simp_all

lift_bnf (dead 'k, 'v) fmap [wits: "Map.empty :: 'k ⇒ 'v option"]
  by auto

end