2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory CoreHaskell2
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../Nominal2"
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
(* Core Haskell by John Matthews *)
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
atom_decl var
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
atom_decl cvar
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
atom_decl tvar
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
nominal_datatype kinds:
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
Kind =
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
Klifted
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
| Kunlifted
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
| Kopen
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
| Karrow Kind Kind
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
| Keq Ty Ty
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
and Ty =
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
Tvar tvar
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
| Tcon string
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
| Tapp Ty Ty
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
| Tforall pb::PBind ty::Ty binds "bind_pb pb" in ty
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
and PBind =
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
Pbind tvar Kind
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
binder
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
bind_pb
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
where
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
"bind_pb (Pbind tv k) = [atom tv]"
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
nominal_datatype expressions:
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
Bind =
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
Vb var Ty
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
| Tb tvar Kind
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
and Exp =
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
Var var
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
| Dcon string
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
| App Exp Exp
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
| Appt Exp Ty
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
| Lam b::Bind e::Exp binds "bind_b b" in e
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
binder
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
bind_b
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
where
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
"bind_b (Vb v ty) = [atom v]"
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
| "bind_b (Tb tv kind) = [atom tv]"
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
thm kinds.distinct
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
thm kinds.induct
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
thm kinds.inducts
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
thm kinds.exhaust
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
thm kinds.strong_exhaust
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
thm kinds.fv_defs
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
thm kinds.bn_defs
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
thm kinds.perm_simps
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
thm kinds.eq_iff
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
thm kinds.fv_bn_eqvt
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
thm kinds.size_eqvt
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
thm kinds.supports
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
thm kinds.fsupp
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
thm kinds.supp
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
thm kinds.fresh
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
thm expressions.distinct
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
thm expressions.induct
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
thm expressions.inducts
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
thm expressions.exhaust
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
thm expressions.fv_defs
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
thm expressions.bn_defs
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
thm expressions.perm_simps
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
thm expressions.eq_iff
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
thm expressions.fv_bn_eqvt
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
thm expressions.size_eqvt
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
thm expressions.supports
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
thm expressions.fsupp
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
thm expressions.supp
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
thm expressions.fresh
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
end
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
|