src/HOL/Datatype_Examples/Lift_BNF.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Datatype_Examples/Lift_BNF.thy	Wed Aug 12 20:46:33 2015 +0200
@@ -0,0 +1,75 @@
+theory Lift_BNF
+imports Main
+begin
+
+typedef 'a nonempty_list = "{xs :: 'a list. xs \<noteq> []}"
+  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 \<noteq> []}"
+  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 \<times> 'b) set"
+  by blast
+
+copy_bnf ('a, 'b) T_prod
+
+typedef ('a, 'b, 'c) T_func = "UNIV :: ('a \<Rightarrow> '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 \<Rightarrow> 'a + 'b"]
+  by (auto simp: map_sum_def sum_set_defs split: sum.splits)
+
+typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct \<circ> map fst) xs}"
+  morphisms impl_of Alist
+proof
+  show "[] \<in> {xs. (distinct o map fst) xs}"
+    by simp
+qed
+
+lift_bnf (dead 'k, 'v) alist [wits: "Nil :: ('k \<times> 'v) list"]
+  by simp_all
+
+typedef 'a myopt = "{X :: 'a set. finite X \<and> card X \<le> 1}" by (rule exI[of _ "{}"]) auto
+lemma myopt_type_def: "type_definition
+  (\<lambda>X. if card (Rep_myopt X) = 1 then Some (the_elem (Rep_myopt X)) else None)
+  (\<lambda>x. Abs_myopt (case x of Some x \<Rightarrow> {x} | _ \<Rightarrow> {}))
+  (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
+
+end