954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 1
theory Test
1261
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 2
imports "Parser"
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 3
begin
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 4
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 5
text {* example 1 *}
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 6
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 7
nominal_datatype lam =
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 8
VAR "name"
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 9
| APP "lam" "lam"
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 10
| LET bp::"bp" t::"lam" bind "bi bp" in t ("Let _ in _" [100,100] 100)
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 11
and bp =
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 12
BP "name" "lam" ("_ ::= _" [100,100] 100)
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 13
binder
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 14
bi::"bp \<Rightarrow> name set"
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 15
where
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 16
"bi (BP x t) = {x}"
1228
c179ad9d2446
declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 17
c179ad9d2446
declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 18
typ lam_raw
c179ad9d2446
declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 19
term VAR_raw
1283
6a133abb7633
generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 20
term APP_raw
6a133abb7633
generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 21
term LET_raw
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 22
term Test.BP_raw
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
thm bi_raw.simps
1228
c179ad9d2446
declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24
961
+ − 25
print_theorems
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 26
1261
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 27
text {* example 2 *}
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 28
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 29
nominal_datatype trm' =
961
+ − 30
Var "name"
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 31
| App "trm'" "trm'"
1272
+ − 32
| Lam x::"name" t::"trm'" bind x in t
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
| Let p::"pat'" "trm'" t::"trm'" bind "f p" in t
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 34
and pat' =
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 35
PN
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 36
| PS "name"
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
| PD "name" "name"
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 38
binder
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 39
f::"pat' \<Rightarrow> name set"
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 40
where
978
b44592adf235
Improper interface for datatype and function packages and proper interface lateron.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
+ − 41
"f PN = {}"
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 42
| "f (PS x) = {x}"
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43
| "f (PD x y) = {x,y}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 45
thm f_raw.simps
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 46
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 47
nominal_datatype trm0 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 48
Var0 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 49
| App0 "trm0" "trm0"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 50
| Lam0 x::"name" t::"trm0" bind x in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 51
| Let0 p::"pat0" "trm0" t::"trm0" bind "f0 p" in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 52
and pat0 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 53
PN0
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 54
| PS0 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
| PD0 "pat0" "pat0"
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 56
binder
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 57
f0::"pat0 \<Rightarrow> name set"
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 58
where
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 59
"f0 PN0 = {}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
| "f0 (PS0 x) = {x}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 61
| "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 62
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 63
thm f0_raw.simps
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 64
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 65
text {* example type schemes *}
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 66
datatype t =
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 67
Var "name"
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 68
| Fun "t" "t"
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 69
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 70
nominal_datatype tyS =
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 71
All xs::"name list" ty::"t" bind xs in ty
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 72
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 73
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 74
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 75
(* example 1 from Terms.thy *)
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 76
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 77
nominal_datatype trm1 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 78
Vr1 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 79
| Ap1 "trm1" "trm1"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 80
| Lm1 x::"name" t::"trm1" bind x in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 81
| Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 82
and bp1 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 83
BUnit1
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 84
| BV1 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 85
| BP1 "bp1" "bp1"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 86
binder
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 87
bv1
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 88
where
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 89
"bv1 (BUnit1) = {}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 90
| "bv1 (BV1 x) = {atom x}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 91
| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 92
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 93
thm bv1_raw.simps
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 94
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 95
(* example 2 from Terms.thy *)
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 96
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 97
nominal_datatype trm2 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 98
Vr2 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 99
| Ap2 "trm2" "trm2"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 100
| Lm2 x::"name" t::"trm2" bind x in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 101
| Lt2 r::"rassign" t::"trm2" bind "bv2 r" in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 102
and rassign =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 103
As "name" "trm2"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 104
binder
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 105
bv2
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 106
where
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 107
"bv2 (As x t) = {atom x}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 108
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 109
(* example 3 from Terms.thy *)
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 110
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 111
nominal_datatype trm3 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 112
Vr3 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 113
| Ap3 "trm3" "trm3"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 114
| Lm3 x::"name" t::"trm3" bind x in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 115
| Lt3 r::"rassigns3" t::"trm3" bind "bv3 r" in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 116
and rassigns3 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 117
ANil
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 118
| ACons "name" "trm3" "rassigns3"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 119
binder
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 120
bv3
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 121
where
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 122
"bv3 ANil = {}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 123
| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 124
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 125
(* example 4 from Terms.thy *)
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 126
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 127
nominal_datatype trm4 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 128
Vr4 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 129
| Ap4 "trm4" "trm4 list"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 130
| Lm4 x::"name" t::"trm4" bind x in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 131
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 132
(* example 5 from Terms.thy *)
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 133
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 134
nominal_datatype trm5 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 135
Vr5 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 136
| Ap5 "trm5" "trm5"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 137
| Lt5 l::"lts" t::"trm5" bind "bv5 l" in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 138
and lts =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 139
Lnil
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 140
| Lcons "name" "trm5" "lts"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 141
binder
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 142
bv5
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 143
where
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 144
"bv5 Lnil = {}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 145
| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 146
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 147
(* example 6 from Terms.thy *)
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 148
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 149
nominal_datatype trm6 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 150
Vr6 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 151
| Lm6 x::"name" t::"trm6" bind x in t
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 152
| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 153
binder
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 154
bv6
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 155
where
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 156
"bv6 (Vr6 n) = {}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 157
| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 158
| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 159
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 160
(* example 7 from Terms.thy *)
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 161
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 162
nominal_datatype trm7 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 163
Vr7 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 164
| Lm7 l::"name" r::"trm7" bind l in r
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 165
| Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 166
binder
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 167
bv7
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 168
where
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 169
"bv7 (Vr7 n) = {atom n}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 170
| "bv7 (Lm7 n t) = bv7 t - {atom n}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 171
| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 172
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 173
(* example 8 from Terms.thy *)
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 174
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 175
nominal_datatype foo8 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 176
Foo0 "name"
1283
6a133abb7633
generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 177
| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 178
and bar8 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 179
Bar0 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 180
| Bar1 "name" s::"name" b::"bar8" bind s in b
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 181
binder
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 182
bv8
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 183
where
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 184
"bv8 (Bar0 x) = {}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 185
| "bv8 (Bar1 v x b) = {atom v}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 186
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 187
(* example 9 from Terms.thy *)
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 188
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 189
nominal_datatype lam9 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 190
Var9 "name"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 191
| Lam9 n::"name" l::"lam9" bind n in l
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 192
and bla9 =
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 193
Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 194
binder
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 195
bv9
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 196
where
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 197
"bv9 (Var9 x) = {}"
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 198
| "bv9 (Lam9 x b) = {atom x}"
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
+ − 199
1272
+ − 200
(* example form Leroy 96 about modules *)
+ − 201
+ − 202
nominal_datatype mexp =
+ − 203
Acc path
+ − 204
| Stru body
+ − 205
| Funct x::name sexp m::mexp bind x in m
+ − 206
| FApp mexp path
+ − 207
| Ascr mexp sexp
+ − 208
and body =
+ − 209
Empty
+ − 210
| Seq c::defn d::body bind "cbinders c" in d
+ − 211
and defn =
+ − 212
Type name tyty
+ − 213
| Dty name
+ − 214
| DStru name mexp
+ − 215
| Val name trmtrm
+ − 216
and sexp =
+ − 217
Sig sbody
+ − 218
| SFunc name sexp sexp
+ − 219
and sbody =
+ − 220
SEmpty
+ − 221
| SSeq C::spec D::sbody bind "Cbinders C" in D
+ − 222
and spec =
+ − 223
Type1 name
+ − 224
| Type2 name tyty
+ − 225
| SStru name sexp
+ − 226
| SVal name tyty
+ − 227
and tyty =
+ − 228
Tyref1 name
+ − 229
| Tyref2 path tyty
+ − 230
| Fun tyty tyty
+ − 231
and path =
+ − 232
Sref1 name
+ − 233
| Sref2 path name
+ − 234
and trmtrm =
+ − 235
Tref1 name
+ − 236
| Tref2 path name
+ − 237
| Lam v::name tyty M::trmtrm bind v in M
+ − 238
| App trmtrm trmtrm
+ − 239
| Let body trmtrm
+ − 240
binder
+ − 241
cbinders :: "defn \<Rightarrow> atom set"
+ − 242
and Cbinders :: "spec \<Rightarrow> atom set"
+ − 243
where
+ − 244
"cbinders (Type t T) = {atom t}"
+ − 245
| "cbinders (Dty t) = {atom t}"
+ − 246
| "cbinders (DStru x s) = {atom x}"
+ − 247
| "cbinders (Val v M) = {atom v}"
+ − 248
| "Cbinders (Type1 t) = {atom t}"
+ − 249
| "Cbinders (Type2 t T) = {atom t}"
+ − 250
| "Cbinders (SStru x S) = {atom x}"
+ − 251
| "Cbinders (SVal v T) = {atom v}"
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 252
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 253
(* core haskell *)
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 254
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 255
atom_decl var
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 256
atom_decl tvar
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 257
atom_decl co
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 258
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 259
datatype sort =
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 260
TY tvar
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 261
| CO co
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 262
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 263
datatype kind =
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 264
KStar
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 265
| KFun kind kind
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 266
| KEq kind kind
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 267
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 268
(* there are types, coercion types and regular types *)
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 269
nominal_datatype ty =
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 270
TVar tvar
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 271
| TFun string "ty list"
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 272
| TAll tvar kind ty --"some binding"
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 273
| TSym ty
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 274
| TCir ty ty
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 275
| TApp ty ty
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 276
| TLeft ty
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 277
| TRight ty
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 278
| TEq ty
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 279
| TRightc ty
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 280
| TLeftc ty
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 281
| TCoe ty ty
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 282
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 283
typedecl ty --"hack since ty is not yet defined"
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 284
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 285
abbreviation
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 286
"atoms A \<equiv> atom ` A"
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 287
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 288
nominal_datatype trm =
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 289
Var var
1283
6a133abb7633
generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 290
| LAM tv::tvar kind t::trm bind tv in t
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 291
| APP trm ty
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 292
| Lam v::var ty t::trm bind v in t
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 293
| App trm trm
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 294
| Let x::var ty trm t::trm bind x in t
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 295
| Case trm "assoc list"
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 296
| Cast trm ty --"ty is supposed to be a coercion type only"
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 297
and assoc =
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 298
A p::pat t::trm bind "bv p" in t
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 299
and pat =
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 300
K string "(tvar \<times> kind) list" "(var \<times> ty) list"
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 301
binder
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 302
bv :: "pat \<Rightarrow> atom set"
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 303
where
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 304
"bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 305
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 306
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 307
thm bv_raw.simps
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 308
961
+ − 309
end
1223
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 310
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 311
1228
c179ad9d2446
declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 312