|
62695
|
1 |
(* Title: HOL/Datatype_Examples/Lift_BNF.thy
|
|
|
2 |
Author: Dmitriy Traytel, ETH Zürich
|
|
|
3 |
Copyright 2015
|
|
|
4 |
|
|
|
5 |
Demonstration of the "lift_bnf" command.
|
|
|
6 |
*)
|
|
|
7 |
|
|
63167
|
8 |
section \<open>Demonstration of the \textbf{lift_bnf} Command\<close>
|
|
62695
|
9 |
|
|
60918
|
10 |
theory Lift_BNF
|
|
|
11 |
imports Main
|
|
|
12 |
begin
|
|
|
13 |
|
|
|
14 |
typedef 'a nonempty_list = "{xs :: 'a list. xs \<noteq> []}"
|
|
|
15 |
by blast
|
|
|
16 |
|
|
|
17 |
lift_bnf (no_warn_wits) (neset: 'a) nonempty_list
|
|
|
18 |
for map: nemap rel: nerel
|
|
|
19 |
by simp_all
|
|
|
20 |
|
|
|
21 |
typedef ('a :: finite, 'b) fin_nonempty_list = "{(xs :: 'a set, ys :: 'b list). ys \<noteq> []}"
|
|
|
22 |
by blast
|
|
|
23 |
|
|
|
24 |
lift_bnf (dead 'a :: finite, 'b) fin_nonempty_list
|
|
|
25 |
by auto
|
|
|
26 |
|
|
|
27 |
datatype 'a tree = Leaf | Node 'a "'a tree nonempty_list"
|
|
|
28 |
|
|
|
29 |
record 'a point =
|
|
|
30 |
xCoord :: 'a
|
|
|
31 |
yCoord :: 'a
|
|
|
32 |
|
|
|
33 |
copy_bnf ('a, 's) point_ext
|
|
|
34 |
|
|
|
35 |
typedef 'a it = "UNIV :: 'a set"
|
|
|
36 |
by blast
|
|
|
37 |
|
|
|
38 |
copy_bnf (plugins del: size) 'a it
|
|
|
39 |
|
|
|
40 |
typedef ('a, 'b) T_prod = "UNIV :: ('a \<times> 'b) set"
|
|
|
41 |
by blast
|
|
|
42 |
|
|
|
43 |
copy_bnf ('a, 'b) T_prod
|
|
|
44 |
|
|
|
45 |
typedef ('a, 'b, 'c) T_func = "UNIV :: ('a \<Rightarrow> 'b * 'c) set"
|
|
|
46 |
by blast
|
|
|
47 |
|
|
|
48 |
copy_bnf ('a, 'b, 'c) T_func
|
|
|
49 |
|
|
|
50 |
typedef ('a, 'b) sum_copy = "UNIV :: ('a + 'b) set"
|
|
|
51 |
by blast
|
|
|
52 |
|
|
|
53 |
copy_bnf ('a, 'b) sum_copy
|
|
|
54 |
|
|
|
55 |
typedef ('a, 'b) T_sum = "{Inl x | x. True} :: ('a + 'b) set"
|
|
|
56 |
by blast
|
|
|
57 |
|
|
|
58 |
lift_bnf (no_warn_wits) ('a, 'b) T_sum [wits: "Inl :: 'a \<Rightarrow> 'a + 'b"]
|
|
|
59 |
by (auto simp: map_sum_def sum_set_defs split: sum.splits)
|
|
|
60 |
|
|
|
61 |
typedef ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. (distinct \<circ> map fst) xs}"
|
|
|
62 |
morphisms impl_of Alist
|
|
|
63 |
proof
|
|
|
64 |
show "[] \<in> {xs. (distinct o map fst) xs}"
|
|
|
65 |
by simp
|
|
|
66 |
qed
|
|
|
67 |
|
|
|
68 |
lift_bnf (dead 'k, 'v) alist [wits: "Nil :: ('k \<times> 'v) list"]
|
|
|
69 |
by simp_all
|
|
|
70 |
|
|
|
71 |
typedef 'a myopt = "{X :: 'a set. finite X \<and> card X \<le> 1}" by (rule exI[of _ "{}"]) auto
|
|
|
72 |
lemma myopt_type_def: "type_definition
|
|
|
73 |
(\<lambda>X. if card (Rep_myopt X) = 1 then Some (the_elem (Rep_myopt X)) else None)
|
|
|
74 |
(\<lambda>x. Abs_myopt (case x of Some x \<Rightarrow> {x} | _ \<Rightarrow> {}))
|
|
|
75 |
(UNIV :: 'a option set)"
|
|
|
76 |
apply unfold_locales
|
|
|
77 |
apply (auto simp: Abs_myopt_inverse dest!: card_eq_SucD split: option.splits)
|
|
|
78 |
apply (metis Rep_myopt_inverse)
|
|
|
79 |
apply (metis One_nat_def Rep_myopt Rep_myopt_inverse Suc_le_mono card_0_eq le0 le_antisym mem_Collect_eq nat.exhaust)
|
|
|
80 |
done
|
|
|
81 |
|
|
|
82 |
copy_bnf 'a myopt via myopt_type_def
|
|
|
83 |
|
|
62137
|
84 |
typedef ('k, 'v) fmap = "{M :: ('k \<rightharpoonup> 'v). finite (dom M)}"
|
|
|
85 |
by (rule exI[of _ Map.empty]) simp_all
|
|
|
86 |
|
|
|
87 |
lift_bnf (dead 'k, 'v) fmap [wits: "Map.empty :: 'k \<Rightarrow> 'v option"]
|
|
|
88 |
by auto
|
|
|
89 |
|
|
60918
|
90 |
end
|