| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Tue, 20 Dec 2011 16:49:03 +0900 | |
| changeset 3081 | 660a4f5adee8 |
| parent 2950 | 0911cb7bf696 |
| permissions | -rw-r--r-- |
|
2083
9568f9f31822
tuned file names for examples
Christian Urban <urbanc@in.tum.de>
parents:
2064
diff
changeset
|
1 |
theory CoreHaskell |
|
2454
9ffee4eb1ae1
renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents:
2436
diff
changeset
|
2 |
imports "../Nominal2" |
| 1601 | 3 |
begin |
4 |
||
|
2308
387fcbd33820
fixed problem with bn_info
Christian Urban <urbanc@in.tum.de>
parents:
2142
diff
changeset
|
5 |
(* Core Haskell *) |
|
2100
705dc7532ee3
added comment about bind_set
Christian Urban <urbanc@in.tum.de>
parents:
2095
diff
changeset
|
6 |
|
| 1601 | 7 |
atom_decl var |
|
1698
69472e74bd3b
Update according to paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1695
diff
changeset
|
8 |
atom_decl cvar |
| 1601 | 9 |
atom_decl tvar |
10 |
||
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
11 |
nominal_datatype core_haskell: |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
12 |
tkind = |
| 1601 | 13 |
KStar |
14 |
| KFun "tkind" "tkind" |
|
15 |
and ckind = |
|
16 |
CKEq "ty" "ty" |
|
17 |
and ty = |
|
18 |
TVar "tvar" |
|
|
1684
b9e4c812d2c6
Core Haskell can now use proper strings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1667
diff
changeset
|
19 |
| TC "string" |
| 1601 | 20 |
| TApp "ty" "ty" |
|
1684
b9e4c812d2c6
Core Haskell can now use proper strings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1667
diff
changeset
|
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>
parents:
2630
diff
changeset
|
22 |
| TAll tv::"tvar" "tkind" T::"ty" binds (set) tv in T |
|
1698
69472e74bd3b
Update according to paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1695
diff
changeset
|
23 |
| TEq "ckind" "ty" |
|
1606
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
24 |
and ty_lst = |
|
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
25 |
TsNil |
|
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
26 |
| TsCons "ty" "ty_lst" |
| 1601 | 27 |
and co = |
|
1699
2dca07aca287
small changes in the core-haskell spec
Christian Urban <urbanc@in.tum.de>
parents:
1698
diff
changeset
|
28 |
CVar "cvar" |
|
1698
69472e74bd3b
Update according to paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1695
diff
changeset
|
29 |
| CConst "string" |
| 1601 | 30 |
| CApp "co" "co" |
|
1684
b9e4c812d2c6
Core Haskell can now use proper strings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1667
diff
changeset
|
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>
parents:
2630
diff
changeset
|
32 |
| CAll cv::"cvar" "ckind" C::"co" binds (set) cv in C |
|
1698
69472e74bd3b
Update according to paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1695
diff
changeset
|
33 |
| CEq "ckind" "co" |
|
69472e74bd3b
Update according to paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1695
diff
changeset
|
34 |
| CRefl "ty" |
| 1601 | 35 |
| CSym "co" |
|
1698
69472e74bd3b
Update according to paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1695
diff
changeset
|
36 |
| CCir "co" "co" |
|
69472e74bd3b
Update according to paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1695
diff
changeset
|
37 |
| CAt "co" "ty" |
| 1601 | 38 |
| CLeft "co" |
39 |
| CRight "co" |
|
|
1698
69472e74bd3b
Update according to paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1695
diff
changeset
|
40 |
| CSim "co" "co" |
| 1601 | 41 |
| CRightc "co" |
42 |
| CLeftc "co" |
|
43 |
| CCoe "co" "co" |
|
|
1606
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
44 |
and co_lst = |
|
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
45 |
CsNil |
|
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
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>
parents:
1606
diff
changeset
|
47 |
and trm = |
| 1601 | 48 |
Var "var" |
|
1699
2dca07aca287
small changes in the core-haskell spec
Christian Urban <urbanc@in.tum.de>
parents:
1698
diff
changeset
|
49 |
| K "string" |
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
parents:
2630
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>
parents:
2630
diff
changeset
|
51 |
| LAMC cv::"cvar" "ckind" t::"trm" binds (set) cv in t |
|
1698
69472e74bd3b
Update according to paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1695
diff
changeset
|
52 |
| AppT "trm" "ty" |
|
69472e74bd3b
Update according to paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1695
diff
changeset
|
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>
parents:
2630
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>
parents:
2630
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>
parents:
1606
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>
parents:
1606
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>
parents:
1606
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>
parents:
1606
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>
parents:
2630
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
231a20534950
improved abstract, some tuning
Christian Urban <urbanc@in.tum.de>
parents:
2142
diff
changeset
|
85 |
| "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t" |
|
231a20534950
improved abstract, some tuning
Christian Urban <urbanc@in.tum.de>
parents:
2142
diff
changeset
|
86 |
|
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
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>
parents:
2405
diff
changeset
|
88 |
|
|
2598
b136721eedb2
automated permute_bn theorems
Christian Urban <urbanc@in.tum.de>
parents:
2593
diff
changeset
|
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>
parents:
2481
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>
parents:
2481
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>
parents:
2481
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>
parents:
2481
diff
changeset
|
93 |
|
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
94 |
thm core_haskell.distinct |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
95 |
thm core_haskell.induct |
|
2630
8268b277d240
automated all strong induction lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2629
diff
changeset
|
96 |
thm core_haskell.inducts |
|
8268b277d240
automated all strong induction lemmas
Christian Urban <urbanc@in.tum.de>
parents:
2629
diff
changeset
|
97 |
thm core_haskell.strong_induct |
|
2436
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
98 |
thm core_haskell.exhaust |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
99 |
thm core_haskell.fv_defs |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
100 |
thm core_haskell.bn_defs |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
101 |
thm core_haskell.perm_simps |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
102 |
thm core_haskell.eq_iff |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
103 |
thm core_haskell.fv_bn_eqvt |
|
3885dc2669f9
cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents:
2434
diff
changeset
|
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>
parents:
2480
diff
changeset
|
105 |
thm core_haskell.supp |
|
2339
1e0b3992189c
more quotient-definitions
Christian Urban <urbanc@in.tum.de>
parents:
2336
diff
changeset
|
106 |
|
|
1868
26c0c35641cb
equivariance for alpha_raw in CoreHaskell is automatically derived
Christian Urban <urbanc@in.tum.de>
parents:
1867
diff
changeset
|
107 |
|
| 1601 | 108 |
end |
109 |