1629
|
1 |
(*<*)
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
theory Test
|
1596
|
3 |
imports "Parser"
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
begin
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
|
1600
|
6 |
(* This file contains only the examples that are not supposed to work yet. *)
|
|
7 |
|
|
8 |
|
1428
|
9 |
atom_decl name
|
|
10 |
|
1465
|
11 |
ML {* val _ = recursive := false *}
|
1367
|
12 |
|
1312
|
13 |
(* example 7 from Peter Sewell's bestiary *)
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
14 |
(* dest_Const raised
|
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
|
15 |
nominal_datatype exp7 =
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
EVar' name
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
| EUnit'
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
| EPair' exp7 exp7
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
| ELetRec' l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l
|
1312
|
20 |
and lrb =
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
Assign' name exp7
|
1312
|
22 |
and lrbs =
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
Single' lrb
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
| More' lrb lrbs
|
1312
|
25 |
binder
|
|
26 |
b7 :: "lrb \<Rightarrow> atom set" and
|
|
27 |
b7s :: "lrbs \<Rightarrow> atom set"
|
|
28 |
where
|
|
29 |
"b7 (Assign x e) = {atom x}"
|
|
30 |
| "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
|
31 |
| "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
|
32 |
thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
*)
|
1312
|
34 |
|
|
35 |
(* example 8 from Peter Sewell's bestiary *)
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
(*
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
37 |
*** fv_bn: recursive argument, but wrong datatype.
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
38 |
*** At command "nominal_datatype".
|
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
|
39 |
nominal_datatype exp8 =
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
EVar' name
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
| EUnit'
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
| EPair' exp8 exp8
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
| ELetRec' l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l
|
1312
|
44 |
and fnclause =
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
45 |
K' x::name p::pat8 e::exp8 bind "b_pat p" in e
|
1312
|
46 |
and fnclauses =
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
S' fnclause
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
| ORs' fnclause fnclauses
|
1312
|
49 |
and lrb8 =
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
Clause' fnclauses
|
1312
|
51 |
and lrbs8 =
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
52 |
Single' lrb8
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
| More' lrb8 lrbs8
|
1312
|
54 |
and pat8 =
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
PVar'' name
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
| PUnit''
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
57 |
| PPair'' pat8 pat8
|
1312
|
58 |
binder
|
|
59 |
b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and
|
|
60 |
b_pat :: "pat8 \<Rightarrow> atom set" and
|
|
61 |
b_fnclauses :: "fnclauses \<Rightarrow> atom set" and
|
|
62 |
b_fnclause :: "fnclause \<Rightarrow> atom set" and
|
|
63 |
b_lrb8 :: "lrb8 \<Rightarrow> atom set"
|
|
64 |
where
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
"b_lrbs8 (Single' l) = b_lrb8 l"
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
| "b_lrbs8 (More' l ls) = b_lrb8 l \<union> b_lrbs8 ls"
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
| "b_pat (PVar'' x) = {atom x}"
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
| "b_pat (PUnit'') = {}"
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
69 |
| "b_pat (PPair'' p1 p2) = b_pat p1 \<union> b_pat p2"
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
70 |
| "b_fnclauses (S' fc) = (b_fnclause fc)"
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
71 |
| "b_fnclauses (ORs' fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
| "b_lrb8 (Clause' fcs) = (b_fnclauses fcs)"
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
| "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
|
74 |
thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
75 |
*)
|
1398
|
76 |
(* example 4 from Terms.thy *)
|
|
77 |
(* fv_eqvt does not work, we need to repaire defined permute functions
|
|
78 |
defined fv and defined alpha... *)
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
79 |
(* lists-datastructure does not work yet
|
1398
|
80 |
nominal_datatype trm4 =
|
|
81 |
Vr4 "name"
|
|
82 |
| Ap4 "trm4" "trm4 list"
|
|
83 |
| Lm4 x::"name" t::"trm4" bind x in t
|
|
84 |
|
|
85 |
thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
|
|
86 |
thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
87 |
*)
|
1398
|
88 |
|
|
89 |
(* example 8 from Terms.thy *)
|
|
90 |
|
|
91 |
(* Binding in a term under a bn, needs to fail *)
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
92 |
(*
|
1398
|
93 |
nominal_datatype foo8 =
|
|
94 |
Foo0 "name"
|
|
95 |
| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
|
|
96 |
and bar8 =
|
|
97 |
Bar0 "name"
|
|
98 |
| Bar1 "name" s::"name" b::"bar8" bind s in b
|
|
99 |
binder
|
|
100 |
bv8
|
|
101 |
where
|
|
102 |
"bv8 (Bar0 x) = {}"
|
|
103 |
| "bv8 (Bar1 v x b) = {atom v}"
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
104 |
*)
|
1398
|
105 |
|
1312
|
106 |
(* example 9 from Peter Sewell's bestiary *)
|
|
107 |
(* 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
|
108 |
|
961
|
109 |
end
|
1629
|
110 |
(*>*)
|
1223
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
111 |
|
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
112 |
|