|
2083
|
1 |
theory CoreHaskell
|
|
2454
|
2 |
imports "../Nominal2"
|
|
1601
|
3 |
begin
|
|
|
4 |
|
|
2308
|
5 |
(* Core Haskell *)
|
|
2100
|
6 |
|
|
1601
|
7 |
atom_decl var
|
|
1698
|
8 |
atom_decl cvar
|
|
1601
|
9 |
atom_decl tvar
|
|
|
10 |
|
|
2436
|
11 |
nominal_datatype core_haskell:
|
|
|
12 |
tkind =
|
|
1601
|
13 |
KStar
|
|
|
14 |
| KFun "tkind" "tkind"
|
|
|
15 |
and ckind =
|
|
|
16 |
CKEq "ty" "ty"
|
|
|
17 |
and ty =
|
|
|
18 |
TVar "tvar"
|
|
1684
|
19 |
| TC "string"
|
|
1601
|
20 |
| TApp "ty" "ty"
|
|
1684
|
21 |
| TFun "string" "ty_lst"
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
| TAll tv::"tvar" "tkind" T::"ty" binds (set) tv in T
|
|
1698
|
23 |
| TEq "ckind" "ty"
|
|
1606
|
24 |
and ty_lst =
|
|
|
25 |
TsNil
|
|
|
26 |
| TsCons "ty" "ty_lst"
|
|
1601
|
27 |
and co =
|
|
1699
|
28 |
CVar "cvar"
|
|
1698
|
29 |
| CConst "string"
|
|
1601
|
30 |
| CApp "co" "co"
|
|
1684
|
31 |
| CFun "string" "co_lst"
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
| CAll cv::"cvar" "ckind" C::"co" binds (set) cv in C
|
|
1698
|
33 |
| CEq "ckind" "co"
|
|
|
34 |
| CRefl "ty"
|
|
1601
|
35 |
| CSym "co"
|
|
1698
|
36 |
| CCir "co" "co"
|
|
|
37 |
| CAt "co" "ty"
|
|
1601
|
38 |
| CLeft "co"
|
|
|
39 |
| CRight "co"
|
|
1698
|
40 |
| CSim "co" "co"
|
|
1601
|
41 |
| CRightc "co"
|
|
|
42 |
| CLeftc "co"
|
|
|
43 |
| CCoe "co" "co"
|
|
1606
|
44 |
and co_lst =
|
|
|
45 |
CsNil
|
|
|
46 |
| CsCons "co" "co_lst"
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
47 |
and trm =
|
|
1601
|
48 |
Var "var"
|
|
1699
|
49 |
| K "string"
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
| LAMT tv::"tvar" "tkind" t::"trm" binds (set) tv in t
|
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
51 |
| LAMC cv::"cvar" "ckind" t::"trm" binds (set) cv in t
|
|
1698
|
52 |
| AppT "trm" "ty"
|
|
|
53 |
| AppC "trm" "co"
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
54 |
| Lam v::"var" "ty" t::"trm" binds (set) v in t
|
|
1601
|
55 |
| App "trm" "trm"
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
| Let x::"var" "ty" "trm" t::"trm" binds (set) x in t
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
57 |
| Case "trm" "assoc_lst"
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
58 |
| Cast "trm" "ty" --"ty is supposed to be a coercion type only"
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
59 |
and assoc_lst =
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
60 |
ANil
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
61 |
| ACons p::"pat" t::"trm" "assoc_lst" binds "bv p" in t
|
|
1601
|
62 |
and pat =
|
|
1700
|
63 |
Kpat "string" "tvars" "cvars" "vars"
|
|
|
64 |
and vars =
|
|
|
65 |
VsNil
|
|
|
66 |
| VsCons "var" "ty" "vars"
|
|
|
67 |
and tvars =
|
|
|
68 |
TvsNil
|
|
|
69 |
| TvsCons "tvar" "tkind" "tvars"
|
|
|
70 |
and cvars =
|
|
|
71 |
CvsNil
|
|
|
72 |
| CvsCons "cvar" "ckind" "cvars"
|
|
1601
|
73 |
binder
|
|
1695
|
74 |
bv :: "pat \<Rightarrow> atom list"
|
|
1700
|
75 |
and bv_vs :: "vars \<Rightarrow> atom list"
|
|
|
76 |
and bv_tvs :: "tvars \<Rightarrow> atom list"
|
|
|
77 |
and bv_cvs :: "cvars \<Rightarrow> atom list"
|
|
1601
|
78 |
where
|
|
1700
|
79 |
"bv (Kpat s tvts tvcs vs) = append (bv_tvs tvts) (append (bv_cvs tvcs) (bv_vs vs))"
|
|
|
80 |
| "bv_vs VsNil = []"
|
|
|
81 |
| "bv_vs (VsCons v k t) = (atom v) # bv_vs t"
|
|
|
82 |
| "bv_tvs TvsNil = []"
|
|
|
83 |
| "bv_tvs (TvsCons v k t) = (atom v) # bv_tvs t"
|
|
|
84 |
| "bv_cvs CvsNil = []"
|
|
2213
|
85 |
| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
|
|
|
86 |
|
|
2436
|
87 |
(* generated theorems *)
|
2406
428d9cb9a243
can also lift the various eqvt lemmas for bn, fv, fv_bn and size
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
88 |
|
|
2598
|
89 |
thm core_haskell.permute_bn
|
2593
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
90 |
thm core_haskell.perm_bn_alpha
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
91 |
thm core_haskell.perm_bn_simps
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
92 |
thm core_haskell.bn_finite
|
25dcb2b1329e
ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
93 |
|
|
2436
|
94 |
thm core_haskell.distinct
|
|
|
95 |
thm core_haskell.induct
|
|
2630
|
96 |
thm core_haskell.inducts
|
|
|
97 |
thm core_haskell.strong_induct
|
|
2436
|
98 |
thm core_haskell.exhaust
|
|
|
99 |
thm core_haskell.fv_defs
|
|
|
100 |
thm core_haskell.bn_defs
|
|
|
101 |
thm core_haskell.perm_simps
|
|
|
102 |
thm core_haskell.eq_iff
|
|
|
103 |
thm core_haskell.fv_bn_eqvt
|
|
|
104 |
thm core_haskell.size_eqvt
|
2481
3a5ebb2fcdbf
made supp proofs more robust by not using the standard induction; renamed some example files
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
105 |
thm core_haskell.supp
|
|
2339
|
106 |
|
1868
26c0c35641cb
equivariance for alpha_raw in CoreHaskell is automatically derived
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
107 |
|
|
1601
|
108 |
end
|
|
|
109 |
|