2559
add799cf0817
adapted to changes by Florian on the quotient package and removed local fix for function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1 |
|
2485
|
2 |
theory Datatypes
|
|
3 |
imports "../Nominal2"
|
|
4 |
begin
|
|
5 |
|
|
6 |
(*
|
|
7 |
plain nominal_datatype definition without an
|
|
8 |
atom_decl - example by John Matthews
|
|
9 |
*)
|
|
10 |
|
|
11 |
nominal_datatype 'a Maybe =
|
|
12 |
Nothing
|
|
13 |
| Just 'a
|
|
14 |
|
|
15 |
|
|
16 |
thm Maybe.distinct
|
|
17 |
thm Maybe.induct
|
|
18 |
thm Maybe.exhaust
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
thm Maybe.strong_exhaust
|
2485
|
20 |
thm Maybe.fv_defs
|
|
21 |
thm Maybe.bn_defs
|
|
22 |
thm Maybe.perm_simps
|
|
23 |
thm Maybe.eq_iff
|
|
24 |
thm Maybe.fv_bn_eqvt
|
|
25 |
thm Maybe.size_eqvt
|
|
26 |
thm Maybe.supp
|
|
27 |
|
|
28 |
(*
|
|
29 |
using a datatype inside a nominal_datatype
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
the datatype needs to be shown to be an instance
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
of the pure class (this is usually trivial)
|
2485
|
33 |
*)
|
|
34 |
|
|
35 |
atom_decl name
|
|
36 |
|
|
37 |
datatype foo = Foo | Bar
|
|
38 |
|
|
39 |
|
|
40 |
instantiation foo :: pure
|
|
41 |
begin
|
|
42 |
|
|
43 |
definition
|
|
44 |
"p \<bullet> (f::foo) = f"
|
|
45 |
|
|
46 |
instance
|
|
47 |
apply(default)
|
|
48 |
apply(simp_all add: permute_foo_def)
|
|
49 |
done
|
|
50 |
|
|
51 |
end
|
|
52 |
|
|
53 |
|
|
54 |
nominal_datatype baz =
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
Baz x::name t::foo binds x in t
|
2485
|
56 |
|
|
57 |
|
2868
|
58 |
|
2485
|
59 |
thm baz.distinct
|
|
60 |
thm baz.induct
|
|
61 |
thm baz.exhaust
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
62 |
thm baz.strong_exhaust
|
2485
|
63 |
thm baz.fv_defs
|
|
64 |
thm baz.bn_defs
|
|
65 |
thm baz.perm_simps
|
|
66 |
thm baz.eq_iff
|
|
67 |
thm baz.fv_bn_eqvt
|
|
68 |
thm baz.size_eqvt
|
|
69 |
thm baz.supp
|
2777
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
(*
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
a nominal datatype with a set argument of
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
pure type
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
74 |
*)
|
2485
|
75 |
|
2777
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
nominal_datatype set_ty =
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
77 |
Set_ty "nat set"
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
78 |
| Fun "nat \<Rightarrow> nat"
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
79 |
| Var "name"
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
80 |
| Lam x::"name" t::"set_ty" binds x in t
|
2868
|
81 |
thm meta_eq_to_obj_eq
|
2777
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
82 |
thm set_ty.distinct
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
83 |
thm set_ty.induct
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
84 |
thm set_ty.exhaust
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
85 |
thm set_ty.strong_exhaust
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
86 |
thm set_ty.fv_defs
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
87 |
thm set_ty.bn_defs
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
88 |
thm set_ty.perm_simps
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
89 |
thm set_ty.eq_iff
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
90 |
thm set_ty.fv_bn_eqvt
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
91 |
thm set_ty.size_eqvt
|
75a95431cd8b
proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
92 |
thm set_ty.supp
|
2485
|
93 |
|
2781
|
94 |
|
|
95 |
|
2485
|
96 |
end
|
|
97 |
|
|
98 |
|
|
99 |
|