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
|
|
1335
|
2 |
imports "Parser" "../Attic/Prove"
|
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 |
|
|
1398
|
5 |
text {* example 1, equivalent to example 2 from Terms *}
|
1316
0577afdb1732
Porting from Lift to Parser; until defining the Quotient type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
6 |
|
|
1428
|
7 |
atom_decl name
|
|
|
8 |
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
nominal_datatype lam =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
VAR "name"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
| APP "lam" "lam"
|
|
1287
|
12 |
| LET bp::"bp" t::"lam" bind "bi bp" in t
|
|
1398
|
13 |
and bp =
|
|
|
14 |
BP "name" "lam"
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
binder
|
1295
0ecc775e5fce
Link calls to Raw permutations, FV definition and alpha_definition into the parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
16 |
bi::"bp \<Rightarrow> atom set"
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
where
|
1295
0ecc775e5fce
Link calls to Raw permutations, FV definition and alpha_definition into the parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
18 |
"bi (BP x t) = {atom 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
|
19 |
|
|
1418
|
20 |
thm lam_bp_fv
|
|
|
21 |
thm lam_bp_inject
|
|
|
22 |
thm lam_bp_bn
|
|
|
23 |
thm lam_bp_perm
|
|
|
24 |
thm lam_bp_induct
|
|
|
25 |
thm lam_bp_distinct
|
|
1428
|
26 |
ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
|
|
|
27 |
|
|
|
28 |
term "supp (x :: lam)"
|
|
1436
|
29 |
lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted]
|
|
1418
|
30 |
|
|
1436
|
31 |
lemma infinite_Un:
|
|
|
32 |
shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
|
|
|
33 |
apply(auto)
|
|
|
34 |
done
|
|
|
35 |
|
|
|
36 |
lemma bi_eqvt:
|
|
|
37 |
shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
|
|
|
38 |
sorry
|
|
|
39 |
|
|
|
40 |
lemma supp_fv:
|
|
|
41 |
"supp t = fv_lam t" and
|
|
|
42 |
"supp b = fv_bp b"
|
|
|
43 |
apply(induct t and b rule: lam_bp_inducts)
|
|
|
44 |
apply(simp_all add: lam_bp_fv)
|
|
|
45 |
(* VAR case *)
|
|
|
46 |
apply(simp only: supp_def)
|
|
|
47 |
apply(simp only: lam_bp_perm)
|
|
|
48 |
apply(simp only: lam_bp_inject)
|
|
|
49 |
apply(simp only: supp_def[symmetric])
|
|
|
50 |
apply(simp only: supp_at_base)
|
|
|
51 |
(* APP case *)
|
|
|
52 |
apply(simp only: supp_def)
|
|
|
53 |
apply(simp only: lam_bp_perm)
|
|
|
54 |
apply(simp only: lam_bp_inject)
|
|
|
55 |
apply(simp only: de_Morgan_conj)
|
|
|
56 |
apply(simp only: Collect_disj_eq)
|
|
|
57 |
apply(simp only: infinite_Un)
|
|
|
58 |
apply(simp only: Collect_disj_eq)
|
|
|
59 |
(* LET case *)
|
|
|
60 |
defer
|
|
|
61 |
(* BP case *)
|
|
|
62 |
apply(simp only: supp_def)
|
|
|
63 |
apply(simp only: lam_bp_perm)
|
|
|
64 |
apply(simp only: lam_bp_inject)
|
|
|
65 |
apply(simp only: de_Morgan_conj)
|
|
|
66 |
apply(simp only: Collect_disj_eq)
|
|
|
67 |
apply(simp only: infinite_Un)
|
|
|
68 |
apply(simp only: Collect_disj_eq)
|
|
|
69 |
apply(simp only: supp_def[symmetric])
|
|
|
70 |
apply(simp only: supp_at_base)
|
|
|
71 |
apply(simp)
|
|
|
72 |
(* LET case *)
|
|
|
73 |
apply(simp only: supp_def)
|
|
|
74 |
apply(simp only: lam_bp_perm)
|
|
|
75 |
apply(simp only: lam_bp_inject)
|
|
|
76 |
apply(simp only: alpha_gen)
|
|
|
77 |
|
|
|
78 |
thm alpha_gen
|
|
|
79 |
thm lam_bp_fv
|
|
|
80 |
thm lam_bp_inject
|
|
|
81 |
oops
|
|
|
82 |
|
|
|
83 |
|
|
1367
|
84 |
|
1261
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
85 |
text {* example 2 *}
|
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
86 |
|
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
87 |
nominal_datatype trm' =
|
|
961
|
88 |
Var "name"
|
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
89 |
| App "trm'" "trm'"
|
|
1398
|
90 |
| 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
|
91 |
| 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
|
92 |
and pat' =
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
PN
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
94 |
| 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
|
95 |
| 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
|
96 |
binder
|
|
1299
|
97 |
f::"pat' \<Rightarrow> atom set"
|
|
1398
|
98 |
where
|
978
b44592adf235
Improper interface for datatype and function packages and proper interface lateron.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
99 |
"f PN = {}"
|
1380
dab8d99b37c1
added bn-information, but it is not yet ordered according to the dts
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
100 |
| "f (PD x y) = {atom x, atom y}"
|
|
1299
|
101 |
| "f (PS x) = {atom x}"
|
1380
dab8d99b37c1
added bn-information, but it is not yet ordered according to the dts
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
102 |
|
|
1418
|
103 |
thm trm'_pat'_fv
|
|
|
104 |
thm trm'_pat'_inject
|
|
|
105 |
thm trm'_pat'_bn
|
|
|
106 |
thm trm'_pat'_perm
|
|
|
107 |
thm trm'_pat'_induct
|
|
|
108 |
thm trm'_pat'_distinct
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
109 |
|
|
1367
|
110 |
(* compat should be
|
|
1368
|
111 |
compat (PN) pi (PN) == True
|
|
|
112 |
compat (PS x) pi (PS x') == pi o x = x'
|
|
|
113 |
compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2'
|
|
1367
|
114 |
*)
|
|
|
115 |
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
116 |
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
|
117 |
Var0 "name"
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
118 |
| App0 "trm0" "trm0"
|
|
1398
|
119 |
| Lam0 x::"name" t::"trm0" bind x in t
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
120 |
| 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
|
121 |
and pat0 =
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
122 |
PN0
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
123 |
| PS0 "name"
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
124 |
| 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
|
125 |
binder
|
|
1299
|
126 |
f0::"pat0 \<Rightarrow> atom set"
|
|
1398
|
127 |
where
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
128 |
"f0 PN0 = {}"
|
|
1299
|
129 |
| "f0 (PS0 x) = {atom x}"
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
130 |
| "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
|
131 |
|
|
1418
|
132 |
thm trm0_pat0_fv
|
|
|
133 |
thm trm0_pat0_inject
|
|
|
134 |
thm trm0_pat0_bn
|
|
1340
|
135 |
thm trm0_pat0_perm
|
|
1418
|
136 |
thm trm0_pat0_induct
|
|
|
137 |
thm trm0_pat0_distinct
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
138 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
139 |
text {* example type schemes *}
|
|
1285
|
140 |
|
|
1302
|
141 |
nominal_datatype t =
|
|
1416
|
142 |
VarTS "name"
|
|
|
143 |
| FunTS "t" "t"
|
|
1398
|
144 |
and tyS =
|
1341
c25f797c7e6e
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
145 |
All xs::"name set" 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
|
146 |
|
|
1418
|
147 |
thm t_tyS_fv
|
|
|
148 |
thm t_tyS_inject
|
|
|
149 |
thm t_tyS_bn
|
|
|
150 |
thm t_tyS_perm
|
|
|
151 |
thm t_tyS_induct
|
|
|
152 |
thm t_tyS_distinct
|
|
|
153 |
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
154 |
(* 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
|
155 |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
156 |
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
|
157 |
Vr1 "name"
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
158 |
| Ap1 "trm1" "trm1"
|
|
1398
|
159 |
| Lm1 x::"name" t::"trm1" bind x in t
|
|
|
160 |
| Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
161 |
and bp1 =
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
162 |
BUnit1
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
163 |
| BV1 "name"
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
164 |
| 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
|
165 |
binder
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
166 |
bv1
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
167 |
where
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
168 |
"bv1 (BUnit1) = {}"
|
|
1392
|
169 |
| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
170 |
| "bv1 (BV1 x) = {atom x}"
|
|
1392
|
171 |
|
|
1418
|
172 |
thm trm1_bp1_fv
|
|
|
173 |
thm trm1_bp1_inject
|
|
|
174 |
thm trm1_bp1_bn
|
|
|
175 |
thm trm1_bp1_perm
|
|
|
176 |
thm trm1_bp1_induct
|
|
|
177 |
thm trm1_bp1_distinct
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
178 |
|
|
1367
|
179 |
text {* example 3 from Terms.thy *}
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
180 |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
181 |
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
|
182 |
Vr3 "name"
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
183 |
| 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
|
184 |
| 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
|
185 |
| 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
|
186 |
and rassigns3 =
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
ANil
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
188 |
| 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
|
189 |
binder
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
190 |
bv3
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
191 |
where
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
192 |
"bv3 ANil = {}"
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
193 |
| "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
|
194 |
|
|
1418
|
195 |
thm trm3_rassigns3_fv
|
|
|
196 |
thm trm3_rassigns3_inject
|
|
|
197 |
thm trm3_rassigns3_bn
|
|
|
198 |
thm trm3_rassigns3_perm
|
|
|
199 |
thm trm3_rassigns3_induct
|
|
|
200 |
thm trm3_rassigns3_distinct
|
|
1367
|
201 |
|
|
|
202 |
(* compat should be
|
|
|
203 |
compat (ANil) pi (PNil) \<equiv> TRue
|
|
|
204 |
compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts'
|
|
|
205 |
*)
|
|
|
206 |
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
207 |
(* 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
|
208 |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
209 |
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
|
210 |
Vr5 "name"
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
211 |
| 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
|
212 |
| 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
|
213 |
and lts =
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
214 |
Lnil
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
215 |
| 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
|
216 |
binder
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
217 |
bv5
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
218 |
where
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
219 |
"bv5 Lnil = {}"
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
220 |
| "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
|
221 |
|
|
1418
|
222 |
thm trm5_lts_fv
|
|
|
223 |
thm trm5_lts_inject
|
|
|
224 |
thm trm5_lts_bn
|
|
|
225 |
thm trm5_lts_perm
|
|
|
226 |
thm trm5_lts_induct
|
|
|
227 |
thm trm5_lts_distinct
|
|
|
228 |
|
|
1285
|
229 |
(* example from my PHD *)
|
|
|
230 |
|
|
|
231 |
atom_decl coname
|
|
1272
|
232 |
|
1341
c25f797c7e6e
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
233 |
nominal_datatype phd =
|
|
1290
|
234 |
Ax "name" "coname"
|
|
|
235 |
| Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2
|
|
|
236 |
| AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2
|
|
|
237 |
| AndL1 n::"name" t::"phd" "name" bind n in t
|
|
|
238 |
| AndL2 n::"name" t::"phd" "name" bind n in t
|
|
|
239 |
| ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2
|
1319
d793ce9cd06f
potential problem with the phd-example, where two permutations are generated, but only one is used
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
240 |
| ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t
|
d793ce9cd06f
potential problem with the phd-example, where two permutations are generated, but only one is used
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
241 |
|
|
1418
|
242 |
thm phd_fv
|
|
|
243 |
thm phd_inject
|
|
|
244 |
thm phd_bn
|
|
|
245 |
thm phd_perm
|
|
|
246 |
thm phd_induct
|
|
|
247 |
thm phd_distinct
|
|
1285
|
248 |
|
|
|
249 |
(* example form Leroy 96 about modules; OTT *)
|
|
1284
|
250 |
|
|
1272
|
251 |
nominal_datatype mexp =
|
|
1296
|
252 |
Acc "path"
|
|
|
253 |
| Stru "body"
|
|
|
254 |
| Funct x::"name" "sexp" m::"mexp" bind x in m
|
|
|
255 |
| FApp "mexp" "path"
|
|
|
256 |
| Ascr "mexp" "sexp"
|
|
1272
|
257 |
and body =
|
|
|
258 |
Empty
|
|
1296
|
259 |
| Seq c::defn d::"body" bind "cbinders c" in d
|
|
1398
|
260 |
and defn =
|
|
1296
|
261 |
Type "name" "tyty"
|
|
|
262 |
| Dty "name"
|
|
|
263 |
| DStru "name" "mexp"
|
|
|
264 |
| Val "name" "trmtrm"
|
|
1272
|
265 |
and sexp =
|
|
|
266 |
Sig sbody
|
|
1296
|
267 |
| SFunc "name" "sexp" "sexp"
|
|
1398
|
268 |
and sbody =
|
|
1272
|
269 |
SEmpty
|
|
1296
|
270 |
| SSeq C::spec D::sbody bind "Cbinders C" in D
|
|
1272
|
271 |
and spec =
|
|
1398
|
272 |
Type1 "name"
|
|
1296
|
273 |
| Type2 "name" "tyty"
|
|
|
274 |
| SStru "name" "sexp"
|
|
|
275 |
| SVal "name" "tyty"
|
|
1272
|
276 |
and tyty =
|
|
1296
|
277 |
Tyref1 "name"
|
|
|
278 |
| Tyref2 "path" "tyty"
|
|
|
279 |
| Fun "tyty" "tyty"
|
|
1272
|
280 |
and path =
|
|
1296
|
281 |
Sref1 "name"
|
|
|
282 |
| Sref2 "path" "name"
|
|
1272
|
283 |
and trmtrm =
|
|
1296
|
284 |
Tref1 "name"
|
|
|
285 |
| Tref2 "path" "name"
|
|
1340
|
286 |
| Lam' v::"name" "tyty" M::"trmtrm" bind v in M
|
|
|
287 |
| App' "trmtrm" "trmtrm"
|
|
|
288 |
| Let' "body" "trmtrm"
|
|
1272
|
289 |
binder
|
|
|
290 |
cbinders :: "defn \<Rightarrow> atom set"
|
|
|
291 |
and Cbinders :: "spec \<Rightarrow> atom set"
|
|
|
292 |
where
|
|
|
293 |
"cbinders (Type t T) = {atom t}"
|
|
|
294 |
| "cbinders (Dty t) = {atom t}"
|
|
|
295 |
| "cbinders (DStru x s) = {atom x}"
|
|
1396
|
296 |
| "cbinders (Val v M) = {atom v}"
|
|
1272
|
297 |
| "Cbinders (Type1 t) = {atom t}"
|
|
|
298 |
| "Cbinders (Type2 t T) = {atom t}"
|
|
|
299 |
| "Cbinders (SStru x S) = {atom x}"
|
|
1396
|
300 |
| "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
|
301 |
|
|
1418
|
302 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv
|
|
|
303 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject
|
|
|
304 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn
|
|
|
305 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm
|
|
|
306 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct
|
|
|
307 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct
|
|
1392
|
308 |
|
|
1312
|
309 |
(* example 3 from Peter Sewell's bestiary *)
|
|
1418
|
310 |
|
|
1312
|
311 |
nominal_datatype exp =
|
|
1340
|
312 |
VarP "name"
|
|
|
313 |
| AppP "exp" "exp"
|
|
|
314 |
| LamP x::"name" e::"exp" bind x in e
|
|
1396
|
315 |
| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp' p" in e1
|
|
1378
|
316 |
and pat3 =
|
1319
d793ce9cd06f
potential problem with the phd-example, where two permutations are generated, but only one is used
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
317 |
PVar "name"
|
|
1312
|
318 |
| PUnit
|
|
1378
|
319 |
| PPair "pat3" "pat3"
|
|
1312
|
320 |
binder
|
|
1396
|
321 |
bp' :: "pat3 \<Rightarrow> atom set"
|
|
1312
|
322 |
where
|
|
1396
|
323 |
"bp' (PVar x) = {atom x}"
|
|
|
324 |
| "bp' (PUnit) = {}"
|
|
|
325 |
| "bp' (PPair p1 p2) = bp' p1 \<union> bp' p2"
|
|
1418
|
326 |
|
|
|
327 |
thm exp_pat3_fv
|
|
|
328 |
thm exp_pat3_inject
|
|
|
329 |
thm exp_pat3_bn
|
|
|
330 |
thm exp_pat3_perm
|
|
|
331 |
thm exp_pat3_induct
|
|
|
332 |
thm exp_pat3_distinct
|
|
1312
|
333 |
|
|
|
334 |
(* example 6 from Peter Sewell's bestiary *)
|
1341
c25f797c7e6e
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
335 |
nominal_datatype exp6 =
|
|
1312
|
336 |
EVar name
|
|
|
337 |
| EPair exp6 exp6
|
|
|
338 |
| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1
|
|
|
339 |
and pat6 =
|
|
1340
|
340 |
PVar' name
|
|
|
341 |
| PUnit'
|
|
|
342 |
| PPair' pat6 pat6
|
|
1312
|
343 |
binder
|
|
|
344 |
bp6 :: "pat6 \<Rightarrow> atom set"
|
|
|
345 |
where
|
|
1340
|
346 |
"bp6 (PVar' x) = {atom x}"
|
|
|
347 |
| "bp6 (PUnit') = {}"
|
1341
c25f797c7e6e
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
348 |
| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2"
|
|
1418
|
349 |
|
|
|
350 |
thm exp6_pat6_fv
|
|
|
351 |
thm exp6_pat6_inject
|
|
|
352 |
thm exp6_pat6_bn
|
|
|
353 |
thm exp6_pat6_perm
|
|
|
354 |
thm exp6_pat6_induct
|
|
|
355 |
thm exp6_pat6_distinct
|
|
1312
|
356 |
|
|
1398
|
357 |
(* THE REST ARE NOT SUPPOSED TO WORK YET *)
|
|
|
358 |
|
|
1312
|
359 |
(* example 7 from Peter Sewell's bestiary *)
|
1341
c25f797c7e6e
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
360 |
nominal_datatype exp7 =
|
|
1312
|
361 |
EVar name
|
|
|
362 |
| EUnit
|
|
|
363 |
| EPair exp7 exp7
|
|
|
364 |
| ELetRec l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
|
|
|
365 |
and lrb =
|
|
|
366 |
Assign name exp7
|
|
|
367 |
and lrbs =
|
|
|
368 |
Single lrb
|
|
|
369 |
| More lrb lrbs
|
|
|
370 |
binder
|
|
|
371 |
b7 :: "lrb \<Rightarrow> atom set" and
|
|
|
372 |
b7s :: "lrbs \<Rightarrow> atom set"
|
|
|
373 |
where
|
|
|
374 |
"b7 (Assign x e) = {atom x}"
|
|
|
375 |
| "b7s (Single a) = b7 a"
|
1341
c25f797c7e6e
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
376 |
| "b7s (More a as) = (b7 a) \<union> (b7s as)"
|
1361
1e811e3424f3
With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
377 |
thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros
|
|
1312
|
378 |
|
|
|
379 |
(* example 8 from Peter Sewell's bestiary *)
|
1341
c25f797c7e6e
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
380 |
nominal_datatype exp8 =
|
|
1312
|
381 |
EVar name
|
|
|
382 |
| EUnit
|
|
|
383 |
| EPair exp8 exp8
|
|
|
384 |
| ELetRec l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
|
|
|
385 |
and fnclause =
|
|
|
386 |
K x::name p::pat8 e::exp8 bind "b_pat p" in e
|
|
|
387 |
and fnclauses =
|
|
|
388 |
S fnclause
|
|
|
389 |
| ORs fnclause fnclauses
|
|
|
390 |
and lrb8 =
|
|
|
391 |
Clause fnclauses
|
|
|
392 |
and lrbs8 =
|
|
|
393 |
Single lrb8
|
|
|
394 |
| More lrb8 lrbs8
|
|
|
395 |
and pat8 =
|
|
|
396 |
PVar name
|
|
|
397 |
| PUnit
|
|
|
398 |
| PPair pat8 pat8
|
|
|
399 |
binder
|
|
|
400 |
b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
|
|
|
401 |
b_pat :: "pat8 \<Rightarrow> atom set" and
|
|
|
402 |
b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
|
|
|
403 |
b_fnclause :: "fnclause \<Rightarrow> atom set" and
|
|
|
404 |
b_lrb8 :: "lrb8 \<Rightarrow> atom set"
|
|
|
405 |
where
|
|
|
406 |
"b_lrbs8 (Single l) = b_lrb8 l"
|
|
|
407 |
| "b_lrbs8 (More l ls) = b_lrb8 l \<union> b_lrbs8 ls"
|
|
|
408 |
| "b_pat (PVar x) = {atom x}"
|
|
|
409 |
| "b_pat (PUnit) = {}"
|
|
|
410 |
| "b_pat (PPair p1 p2) = b_pat p1 \<union> b_pat p2"
|
|
|
411 |
| "b_fnclauses (S fc) = (b_fnclause fc)"
|
|
|
412 |
| "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
|
|
|
413 |
| "b_lrb8 (Clause fcs) = (b_fnclauses fcs)"
|
1341
c25f797c7e6e
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
414 |
| "b_fnclause (K x pat exp8) = {atom x}"
|
1361
1e811e3424f3
With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
415 |
thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros
|
|
1312
|
416 |
|
|
1398
|
417 |
(* example 4 from Terms.thy *)
|
|
|
418 |
(* fv_eqvt does not work, we need to repaire defined permute functions
|
|
|
419 |
defined fv and defined alpha... *)
|
|
|
420 |
nominal_datatype trm4 =
|
|
|
421 |
Vr4 "name"
|
|
|
422 |
| Ap4 "trm4" "trm4 list"
|
|
|
423 |
| Lm4 x::"name" t::"trm4" bind x in t
|
|
|
424 |
|
|
|
425 |
thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
|
|
|
426 |
thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
|
|
|
427 |
|
|
|
428 |
(* core haskell *)
|
|
|
429 |
atom_decl var
|
|
|
430 |
atom_decl tvar
|
|
|
431 |
|
|
|
432 |
(* there are types, coercion types and regular types *)
|
|
|
433 |
nominal_datatype tkind =
|
|
|
434 |
KStar
|
|
|
435 |
| KFun "tkind" "tkind"
|
|
|
436 |
and ckind =
|
|
|
437 |
CKEq "ty" "ty"
|
|
|
438 |
and ty =
|
|
|
439 |
TVar "tvar"
|
|
|
440 |
| TC "string"
|
|
|
441 |
| TApp "ty" "ty"
|
|
|
442 |
| TFun "string" "ty list"
|
|
|
443 |
| TAll tv::"tvar" "tkind" T::"ty" bind tv in T
|
|
|
444 |
| TEq "ty" "ty" "ty"
|
|
|
445 |
and co =
|
|
|
446 |
CC "string"
|
|
|
447 |
| CApp "co" "co"
|
|
|
448 |
| CFun "string" "co list"
|
|
|
449 |
| CAll tv::"tvar" "ckind" C::"co" bind tv in C
|
|
|
450 |
| CEq "co" "co" "co"
|
|
|
451 |
| CSym "co"
|
|
|
452 |
| CCir "co" "co"
|
|
|
453 |
| CLeft "co"
|
|
|
454 |
| CRight "co"
|
|
|
455 |
| CSim "co"
|
|
|
456 |
| CRightc "co"
|
|
|
457 |
| CLeftc "co"
|
|
|
458 |
| CCoe "co" "co"
|
|
|
459 |
|
|
|
460 |
|
|
|
461 |
typedecl ty --"hack since ty is not yet defined"
|
|
|
462 |
typedecl kind
|
|
|
463 |
|
|
|
464 |
instance ty and kind:: pt
|
|
|
465 |
sorry
|
|
|
466 |
|
|
|
467 |
abbreviation
|
|
|
468 |
"atoms A \<equiv> atom ` A"
|
|
|
469 |
|
|
|
470 |
nominal_datatype trm =
|
|
|
471 |
Var "var"
|
|
|
472 |
| C "string"
|
|
|
473 |
| LAM tv::"tvar" "kind" t::"trm" bind tv in t
|
|
|
474 |
| APP "trm" "ty"
|
|
|
475 |
| Lam v::"var" "ty" t::"trm" bind v in t
|
|
|
476 |
| App "trm" "trm"
|
|
|
477 |
| Let x::"var" "ty" "trm" t::"trm" bind x in t
|
|
|
478 |
| Case "trm" "assoc list"
|
|
|
479 |
| Cast "trm" "ty" --"ty is supposed to be a coercion type only"
|
|
|
480 |
and assoc =
|
|
|
481 |
A p::"pat" t::"trm" bind "bv p" in t
|
|
|
482 |
and pat =
|
|
|
483 |
K "string" "(tvar \<times> kind) list" "(var \<times> ty) list"
|
|
|
484 |
binder
|
|
|
485 |
bv :: "pat \<Rightarrow> atom set"
|
|
|
486 |
where
|
|
|
487 |
"bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))"
|
|
|
488 |
|
|
|
489 |
(*
|
|
|
490 |
compat (K s ts vs) pi (K s' ts' vs') ==
|
|
|
491 |
s = s' &
|
|
|
492 |
|
|
|
493 |
*)
|
|
|
494 |
|
|
|
495 |
|
|
|
496 |
|
|
|
497 |
text {* weirdo example from Peter Sewell's bestiary *}
|
|
|
498 |
|
|
|
499 |
nominal_datatype weird =
|
|
|
500 |
WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird"
|
|
|
501 |
bind x in p1, bind x in p2, bind y in p2, bind y in p3
|
|
|
502 |
| WV "name"
|
|
|
503 |
| WP "weird" "weird"
|
|
|
504 |
|
|
|
505 |
thm permute_weird_raw.simps[no_vars]
|
|
|
506 |
thm alpha_weird_raw.intros[no_vars]
|
|
|
507 |
thm fv_weird_raw.simps[no_vars]
|
|
|
508 |
|
|
|
509 |
(* example 6 from Terms.thy *)
|
|
|
510 |
|
|
|
511 |
(* BV is not respectful, needs to fail*)
|
|
|
512 |
nominal_datatype trm6 =
|
|
|
513 |
Vr6 "name"
|
|
|
514 |
| Lm6 x::"name" t::"trm6" bind x in t
|
|
|
515 |
| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right
|
|
|
516 |
binder
|
|
|
517 |
bv6
|
|
|
518 |
where
|
|
|
519 |
"bv6 (Vr6 n) = {}"
|
|
|
520 |
| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
|
|
|
521 |
| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
|
|
|
522 |
(* example 7 from Terms.thy *)
|
|
|
523 |
|
|
|
524 |
(* BV is not respectful, needs to fail*)
|
|
|
525 |
nominal_datatype trm7 =
|
|
|
526 |
Vr7 "name"
|
|
|
527 |
| Lm7 l::"name" r::"trm7" bind l in r
|
|
|
528 |
| Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r
|
|
|
529 |
binder
|
|
|
530 |
bv7
|
|
|
531 |
where
|
|
|
532 |
"bv7 (Vr7 n) = {atom n}"
|
|
|
533 |
| "bv7 (Lm7 n t) = bv7 t - {atom n}"
|
|
|
534 |
| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
|
|
|
535 |
|
|
|
536 |
(* example 8 from Terms.thy *)
|
|
|
537 |
|
|
|
538 |
(* Binding in a term under a bn, needs to fail *)
|
|
|
539 |
nominal_datatype foo8 =
|
|
|
540 |
Foo0 "name"
|
|
|
541 |
| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
|
|
|
542 |
and bar8 =
|
|
|
543 |
Bar0 "name"
|
|
|
544 |
| Bar1 "name" s::"name" b::"bar8" bind s in b
|
|
|
545 |
binder
|
|
|
546 |
bv8
|
|
|
547 |
where
|
|
|
548 |
"bv8 (Bar0 x) = {}"
|
|
|
549 |
| "bv8 (Bar1 v x b) = {atom v}"
|
|
|
550 |
|
|
|
551 |
(* example 9 from Terms.thy *)
|
|
|
552 |
|
|
|
553 |
(* BV is not respectful, needs to fail*)
|
|
|
554 |
nominal_datatype lam9 =
|
|
|
555 |
Var9 "name"
|
|
|
556 |
| Lam9 n::"name" l::"lam9" bind n in l
|
|
|
557 |
and bla9 =
|
|
|
558 |
Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
|
|
|
559 |
binder
|
|
|
560 |
bv9
|
|
|
561 |
where
|
|
|
562 |
"bv9 (Var9 x) = {}"
|
|
|
563 |
| "bv9 (Lam9 x b) = {atom x}"
|
|
|
564 |
|
|
|
565 |
|
|
|
566 |
(* Type schemes with separate datatypes *)
|
|
|
567 |
nominal_datatype t =
|
|
|
568 |
Var "name"
|
|
|
569 |
| Fun "t" "t"
|
|
|
570 |
|
|
|
571 |
nominal_datatype tyS =
|
|
|
572 |
All xs::"name list" ty::"t_raw" bind xs in ty
|
|
|
573 |
|
|
1312
|
574 |
|
|
|
575 |
|
|
|
576 |
|
|
|
577 |
(* example 9 from Peter Sewell's bestiary *)
|
|
|
578 |
(* run out of steam at the moment *)
|
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
579 |
|
|
961
|
580 |
end
|
1223
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
581 |
|
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
582 |
|
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
|
583 |
|