| author | Christian Urban <urbanc@in.tum.de> |
| Wed, 17 Mar 2010 08:07:25 +0100 | |
| changeset 1466 | d18defacda25 |
| parent 1465 | 4de35639fef0 |
| child 1471 | 7fe643ad19e4 |
| permissions | -rw-r--r-- |
|
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
c3dfd4193b42
Experiments with proving weird transp
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1331
diff
changeset
|
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
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
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>
parents:
1309
diff
changeset
|
6 |
|
|
1428
4029105011ca
Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1418
diff
changeset
|
7 |
atom_decl name |
|
4029105011ca
Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1418
diff
changeset
|
8 |
|
|
1454
7c8cd6eae8e2
FV_bn generated for recursive functions as well, and used in main fv for bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1453
diff
changeset
|
9 |
ML {* val _ = cheat_alpha_eqvt := false *}
|
|
7c8cd6eae8e2
FV_bn generated for recursive functions as well, and used in main fv for bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1453
diff
changeset
|
10 |
ML {* val _ = cheat_fv_eqvt := false *}
|
|
7c8cd6eae8e2
FV_bn generated for recursive functions as well, and used in main fv for bindings.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1453
diff
changeset
|
11 |
ML {* val _ = recursive := false *}
|
|
1445
3246c5e1a9d7
cheat_alpha_eqvt no longer needed; the proofs work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1441
diff
changeset
|
12 |
|
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
nominal_datatype lam = |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
VAR "name" |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
| APP "lam" "lam" |
|
1449
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
16 |
| LAM x::"name" t::"lam" bind x in t |
|
1287
8557af71724e
slight simplification of the raw-decl generation
Christian Urban <urbanc@in.tum.de>
parents:
1285
diff
changeset
|
17 |
| LET bp::"bp" t::"lam" bind "bi bp" in t |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
18 |
and bp = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
19 |
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
|
20 |
binder |
|
1295
0ecc775e5fce
Link calls to Raw permutations, FV definition and alpha_definition into the parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1290
diff
changeset
|
21 |
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
|
22 |
where |
|
1295
0ecc775e5fce
Link calls to Raw permutations, FV definition and alpha_definition into the parser.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1290
diff
changeset
|
23 |
"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>
parents:
1223
diff
changeset
|
24 |
|
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
25 |
thm lam_bp_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
26 |
thm lam_bp_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
27 |
thm lam_bp_bn |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
28 |
thm lam_bp_perm |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
29 |
thm lam_bp_induct |
|
1447
378b8c791de8
derive "inducts" from "induct" instead of lifting again is much faster.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1445
diff
changeset
|
30 |
thm lam_bp_inducts |
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
31 |
thm lam_bp_distinct |
|
1428
4029105011ca
Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1418
diff
changeset
|
32 |
ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
|
|
4029105011ca
Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1418
diff
changeset
|
33 |
|
|
4029105011ca
Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1418
diff
changeset
|
34 |
term "supp (x :: lam)" |
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
35 |
|
|
1439
bdd73f8bb63b
added an eqvt-proof for bi
Christian Urban <urbanc@in.tum.de>
parents:
1436
diff
changeset
|
36 |
(* maybe should be added to Infinite.thy *) |
|
1436
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
37 |
lemma infinite_Un: |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
38 |
shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T" |
|
1439
bdd73f8bb63b
added an eqvt-proof for bi
Christian Urban <urbanc@in.tum.de>
parents:
1436
diff
changeset
|
39 |
by simp |
|
1436
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
40 |
|
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
41 |
lemma bi_eqvt: |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
42 |
shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)" |
| 1441 | 43 |
by (rule eqvts) |
|
1436
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
44 |
|
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
45 |
lemma supp_fv: |
|
1461
c79bcbe1983d
added the final unfolded result
Christian Urban <urbanc@in.tum.de>
parents:
1460
diff
changeset
|
46 |
shows "supp t = fv_lam t" |
|
c79bcbe1983d
added the final unfolded result
Christian Urban <urbanc@in.tum.de>
parents:
1460
diff
changeset
|
47 |
and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
|
|
1460
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
48 |
apply(induct t and bp rule: lam_bp_inducts) |
|
1436
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
49 |
apply(simp_all add: lam_bp_fv) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
50 |
(* VAR case *) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
51 |
apply(simp only: supp_def) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
52 |
apply(simp only: lam_bp_perm) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
53 |
apply(simp only: lam_bp_inject) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
54 |
apply(simp only: supp_def[symmetric]) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
55 |
apply(simp only: supp_at_base) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
56 |
(* APP case *) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
57 |
apply(simp only: supp_def) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
58 |
apply(simp only: lam_bp_perm) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
59 |
apply(simp only: lam_bp_inject) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
60 |
apply(simp only: de_Morgan_conj) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
61 |
apply(simp only: Collect_disj_eq) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
62 |
apply(simp only: infinite_Un) |
|
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
63 |
apply(simp only: Collect_disj_eq) |
|
1449
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
64 |
(* LAM case *) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
65 |
apply(rule_tac t="supp (LAM name lam_raw)" and s="supp (Abs {atom name} lam_raw)" in subst)
|
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
66 |
apply(simp (no_asm) only: supp_def) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
67 |
apply(simp only: lam_bp_perm) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
68 |
apply(simp only: permute_ABS) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
69 |
apply(simp only: lam_bp_inject) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
70 |
apply(simp only: Abs_eq_iff) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
71 |
apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
72 |
apply(simp only: alpha_gen) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
73 |
apply(simp only: supp_eqvt[symmetric]) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
74 |
apply(simp only: eqvts) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
75 |
apply(simp only: supp_Abs) |
|
1436
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
76 |
(* LET case *) |
|
1460
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
77 |
apply(rule_tac t="supp (LET bp_raw lam_raw)" and s="supp (Abs (bi bp_raw) lam_raw) \<union> fv_bi bp_raw" in subst) |
|
1449
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
78 |
apply(simp (no_asm) only: supp_def) |
|
1436
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
79 |
apply(simp only: lam_bp_perm) |
|
1460
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
80 |
apply(simp only: permute_ABS) |
|
1436
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
81 |
apply(simp only: lam_bp_inject) |
|
1460
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
82 |
apply(simp only: eqvts) |
|
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
83 |
apply(simp only: Abs_eq_iff) |
|
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
84 |
apply(simp only: ex_simps) |
|
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
85 |
apply(simp only: de_Morgan_conj) |
|
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
86 |
apply(simp only: Collect_disj_eq) |
|
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
87 |
apply(simp only: infinite_Un) |
|
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
88 |
apply(simp only: Collect_disj_eq) |
|
1436
04dad9b0136d
started supp-fv proofs (is going to work)
Christian Urban <urbanc@in.tum.de>
parents:
1428
diff
changeset
|
89 |
apply(simp only: alpha_gen) |
|
1449
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
90 |
apply(simp only: supp_eqvt[symmetric]) |
|
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
91 |
apply(simp only: eqvts) |
|
1460
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
92 |
apply(blast) |
|
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
93 |
apply(simp add: supp_Abs) |
|
0fd03936dedb
merge and proof of support for non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1457
diff
changeset
|
94 |
apply(blast) |
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
95 |
(* BP case *) |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
96 |
apply(simp only: supp_def) |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
97 |
apply(simp only: lam_bp_perm) |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
98 |
apply(simp only: lam_bp_inject) |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
99 |
apply(simp only: de_Morgan_conj) |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
100 |
apply(simp only: Collect_disj_eq) |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
101 |
apply(simp only: infinite_Un) |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
102 |
apply(simp only: Collect_disj_eq) |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
103 |
apply(simp only: supp_def[symmetric]) |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
104 |
apply(simp only: supp_at_base) |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
105 |
apply(simp) |
|
1449
b66d754bf1c2
proof for support when bn-function is present, but fb_function is empty
Christian Urban <urbanc@in.tum.de>
parents:
1439
diff
changeset
|
106 |
done |
|
1367
9bbf56cdeb88
added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents:
1365
diff
changeset
|
107 |
|
|
1461
c79bcbe1983d
added the final unfolded result
Christian Urban <urbanc@in.tum.de>
parents:
1460
diff
changeset
|
108 |
thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
|
c79bcbe1983d
added the final unfolded result
Christian Urban <urbanc@in.tum.de>
parents:
1460
diff
changeset
|
109 |
|
|
1465
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
110 |
ML {* val _ = recursive := true *}
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
111 |
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
112 |
nominal_datatype lam' = |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
113 |
VAR' "name" |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
114 |
| APP' "lam'" "lam'" |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
115 |
| LAM' x::"name" t::"lam'" bind x in t |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
116 |
| LET' bp::"bp'" t::"lam'" bind "bi' bp" in t |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
117 |
and bp' = |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
118 |
BP' "name" "lam'" |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
119 |
binder |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
120 |
bi'::"bp' \<Rightarrow> atom set" |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
121 |
where |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
122 |
"bi' (BP' x t) = {atom x}"
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
123 |
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
124 |
thm lam'_bp'_fv |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
125 |
thm lam'_bp'_inject[no_vars] |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
126 |
thm lam'_bp'_bn |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
127 |
thm lam'_bp'_perm |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
128 |
thm lam'_bp'_induct |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
129 |
thm lam'_bp'_inducts |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
130 |
thm lam'_bp'_distinct |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
131 |
ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
132 |
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
133 |
lemma supp_fv: |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
134 |
shows "supp t = fv_lam' t" |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
135 |
and "supp bp = fv_bp' bp" |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
136 |
apply(induct t and bp rule: lam'_bp'_inducts) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
137 |
apply(simp_all add: lam'_bp'_fv) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
138 |
(* VAR case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
139 |
apply(simp only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
140 |
apply(simp only: lam'_bp'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
141 |
apply(simp only: lam'_bp'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
142 |
apply(simp only: supp_def[symmetric]) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
143 |
apply(simp only: supp_at_base) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
144 |
(* APP case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
145 |
apply(simp only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
146 |
apply(simp only: lam'_bp'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
147 |
apply(simp only: lam'_bp'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
148 |
apply(simp only: de_Morgan_conj) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
149 |
apply(simp only: Collect_disj_eq) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
150 |
apply(simp only: infinite_Un) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
151 |
apply(simp only: Collect_disj_eq) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
152 |
(* LAM case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
153 |
apply(rule_tac t="supp (LAM' name lam'_raw)" and s="supp (Abs {atom name} lam'_raw)" in subst)
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
154 |
apply(simp (no_asm) only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
155 |
apply(simp only: lam'_bp'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
156 |
apply(simp only: permute_ABS) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
157 |
apply(simp only: lam'_bp'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
158 |
apply(simp only: Abs_eq_iff) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
159 |
apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
160 |
apply(simp only: alpha_gen) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
161 |
apply(simp only: supp_eqvt[symmetric]) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
162 |
apply(simp only: eqvts) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
163 |
apply(simp only: supp_Abs) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
164 |
(* LET case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
165 |
apply(rule_tac t="supp (LET' bp'_raw lam'_raw)" and |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
166 |
s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
167 |
apply(simp (no_asm) only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
168 |
apply(simp only: lam'_bp'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
169 |
apply(simp only: permute_ABS) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
170 |
apply(simp only: lam'_bp'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
171 |
apply(simp only: eqvts) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
172 |
apply(simp only: Abs_eq_iff) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
173 |
apply(rule Collect_cong) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
174 |
apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
175 |
apply(simp) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
176 |
apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
177 |
apply(simp) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
178 |
apply(rule Collect_cong) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
179 |
apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
180 |
apply(simp) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
181 |
apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
182 |
apply(simp) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
183 |
apply(rule ext) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
184 |
apply(rule sym) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
185 |
apply(subgoal_tac "fv_bp' = supp") |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
186 |
apply(subgoal_tac "fv_lam' = supp") |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
187 |
apply(simp) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
188 |
apply(rule trans) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
189 |
apply(rule alpha_abs_Pair[symmetric]) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
190 |
apply(simp add: alpha_gen supp_Pair) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
191 |
oops |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
192 |
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
193 |
thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
194 |
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
195 |
|
|
1261
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
1258
diff
changeset
|
196 |
text {* example 2 *}
|
|
853abc14c5c6
added IsaMakefile...but so far included only a test for the parser
Christian Urban <urbanc@in.tum.de>
parents:
1258
diff
changeset
|
197 |
|
|
1465
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
198 |
ML {* val _ = recursive := false *}
|
|
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
parents:
1261
diff
changeset
|
199 |
nominal_datatype trm' = |
|
961
0f88e04eb486
Variable takes a 'name'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
954
diff
changeset
|
200 |
Var "name" |
|
1265
fc8f5897b00a
first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
parents:
1261
diff
changeset
|
201 |
| App "trm'" "trm'" |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
202 |
| 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>
parents:
1261
diff
changeset
|
203 |
| 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>
parents:
1261
diff
changeset
|
204 |
and pat' = |
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
205 |
PN |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
206 |
| PS "name" |
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
207 |
| 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
|
208 |
binder |
|
1299
cbcd4997dac5
most tests work - the ones that do not I commented out
Christian Urban <urbanc@in.tum.de>
parents:
1298
diff
changeset
|
209 |
f::"pat' \<Rightarrow> atom set" |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
210 |
where |
|
978
b44592adf235
Improper interface for datatype and function packages and proper interface lateron.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
973
diff
changeset
|
211 |
"f PN = {}"
|
|
1380
dab8d99b37c1
added bn-information, but it is not yet ordered according to the dts
Christian Urban <urbanc@in.tum.de>
parents:
1378
diff
changeset
|
212 |
| "f (PD x y) = {atom x, atom y}"
|
|
1299
cbcd4997dac5
most tests work - the ones that do not I commented out
Christian Urban <urbanc@in.tum.de>
parents:
1298
diff
changeset
|
213 |
| "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>
parents:
1378
diff
changeset
|
214 |
|
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
215 |
thm trm'_pat'_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
216 |
thm trm'_pat'_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
217 |
thm trm'_pat'_bn |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
218 |
thm trm'_pat'_perm |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
219 |
thm trm'_pat'_induct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
220 |
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>
parents:
1232
diff
changeset
|
221 |
|
|
1465
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
222 |
lemma supp_fv_trm'_pat': |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
223 |
shows "supp t = fv_trm' t" |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
224 |
and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
225 |
apply(induct t and bp rule: trm'_pat'_inducts) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
226 |
apply(simp_all add: trm'_pat'_fv) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
227 |
(* VAR case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
228 |
apply(simp only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
229 |
apply(simp only: trm'_pat'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
230 |
apply(simp only: trm'_pat'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
231 |
apply(simp only: supp_def[symmetric]) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
232 |
apply(simp only: supp_at_base) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
233 |
(* APP case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
234 |
apply(simp only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
235 |
apply(simp only: trm'_pat'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
236 |
apply(simp only: trm'_pat'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
237 |
apply(simp only: de_Morgan_conj) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
238 |
apply(simp only: Collect_disj_eq) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
239 |
apply(simp only: infinite_Un) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
240 |
apply(simp only: Collect_disj_eq) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
241 |
(* LAM case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
242 |
apply(rule_tac t="supp (Lam name trm'_raw)" and s="supp (Abs {atom name} trm'_raw)" in subst)
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
243 |
apply(simp (no_asm) only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
244 |
apply(simp only: trm'_pat'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
245 |
apply(simp only: permute_ABS) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
246 |
apply(simp only: trm'_pat'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
247 |
apply(simp only: Abs_eq_iff) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
248 |
apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
249 |
apply(simp only: alpha_gen) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
250 |
apply(simp only: supp_eqvt[symmetric]) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
251 |
apply(simp only: eqvts) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
252 |
apply(simp only: supp_Abs) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
253 |
(* LET case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
254 |
apply(rule_tac t="supp (Let pat'_raw trm'_raw1 trm'_raw2)" |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
255 |
and s="supp (Abs (f pat'_raw) trm'_raw2) \<union> supp trm'_raw1 \<union> fv_f pat'_raw" in subst) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
256 |
apply(simp (no_asm) only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
257 |
apply(simp only: trm'_pat'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
258 |
apply(simp only: permute_ABS) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
259 |
apply(simp only: trm'_pat'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
260 |
apply(simp only: eqvts) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
261 |
apply(simp only: Abs_eq_iff) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
262 |
apply(simp only: ex_simps) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
263 |
apply(simp only: de_Morgan_conj) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
264 |
apply(simp only: Collect_disj_eq) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
265 |
apply(simp only: infinite_Un) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
266 |
apply(simp only: Collect_disj_eq) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
267 |
apply(simp only: alpha_gen) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
268 |
apply(simp only: supp_eqvt[symmetric]) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
269 |
apply(simp only: eqvts) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
270 |
apply(blast) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
271 |
apply(simp add: supp_Abs) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
272 |
apply(blast) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
273 |
(* PN case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
274 |
apply(simp only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
275 |
apply(simp only: trm'_pat'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
276 |
apply(simp only: trm'_pat'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
277 |
apply(simp) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
278 |
(* PS case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
279 |
apply(simp only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
280 |
apply(simp only: trm'_pat'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
281 |
apply(simp only: trm'_pat'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
282 |
apply(simp only: supp_def[symmetric]) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
283 |
apply(simp only: supp_at_base) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
284 |
apply(simp) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
285 |
(* PD case *) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
286 |
apply(simp only: supp_def) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
287 |
apply(simp only: trm'_pat'_perm) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
288 |
apply(simp only: trm'_pat'_inject) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
289 |
apply(simp only: de_Morgan_conj) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
290 |
apply(simp only: Collect_disj_eq) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
291 |
apply(simp only: infinite_Un) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
292 |
apply(simp only: Collect_disj_eq) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
293 |
apply(simp only: supp_def[symmetric]) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
294 |
apply(simp add: supp_at_base) |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
295 |
done |
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
296 |
|
|
4de35639fef0
added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents:
1461
diff
changeset
|
297 |
thm trm'_pat'_fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]] |
|
1367
9bbf56cdeb88
added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents:
1365
diff
changeset
|
298 |
|
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
299 |
nominal_datatype trm0 = |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
300 |
Var0 "name" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
301 |
| App0 "trm0" "trm0" |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
302 |
| 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>
parents:
1232
diff
changeset
|
303 |
| 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>
parents:
1232
diff
changeset
|
304 |
and pat0 = |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
305 |
PN0 |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
306 |
| PS0 "name" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
307 |
| 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
|
308 |
binder |
|
1299
cbcd4997dac5
most tests work - the ones that do not I commented out
Christian Urban <urbanc@in.tum.de>
parents:
1298
diff
changeset
|
309 |
f0::"pat0 \<Rightarrow> atom set" |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
310 |
where |
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
311 |
"f0 PN0 = {}"
|
|
1299
cbcd4997dac5
most tests work - the ones that do not I commented out
Christian Urban <urbanc@in.tum.de>
parents:
1298
diff
changeset
|
312 |
| "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>
parents:
1232
diff
changeset
|
313 |
| "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>
parents:
1232
diff
changeset
|
314 |
|
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
315 |
thm trm0_pat0_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
316 |
thm trm0_pat0_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
317 |
thm trm0_pat0_bn |
|
1340
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
318 |
thm trm0_pat0_perm |
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
319 |
thm trm0_pat0_induct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
320 |
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
|
321 |
|
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
322 |
text {* example type schemes *}
|
|
1285
e3ac56d3b7af
added example from my phd
Christian Urban <urbanc@in.tum.de>
parents:
1284
diff
changeset
|
323 |
|
|
1302
d3101a5b9c4d
Length fix for nested recursions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1299
diff
changeset
|
324 |
nominal_datatype t = |
| 1416 | 325 |
VarTS "name" |
326 |
| FunTS "t" "t" |
|
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
327 |
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>
parents:
1340
diff
changeset
|
328 |
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
|
329 |
|
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
330 |
thm t_tyS_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
331 |
thm t_tyS_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
332 |
thm t_tyS_bn |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
333 |
thm t_tyS_perm |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
334 |
thm t_tyS_induct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
335 |
thm t_tyS_distinct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
336 |
|
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
337 |
(* 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>
parents:
1232
diff
changeset
|
338 |
|
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
339 |
nominal_datatype trm1 = |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
340 |
Vr1 "name" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
341 |
| Ap1 "trm1" "trm1" |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
342 |
| Lm1 x::"name" t::"trm1" bind x in t |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
343 |
| 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>
parents:
1232
diff
changeset
|
344 |
and bp1 = |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
345 |
BUnit1 |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
346 |
| BV1 "name" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
347 |
| BP1 "bp1" "bp1" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
348 |
binder |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
349 |
bv1 |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
350 |
where |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
351 |
"bv1 (BUnit1) = {}"
|
|
1392
baa67b07f436
parser produces ordered bn-fun information
Christian Urban <urbanc@in.tum.de>
parents:
1380
diff
changeset
|
352 |
| "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>
parents:
1232
diff
changeset
|
353 |
| "bv1 (BV1 x) = {atom x}"
|
|
1392
baa67b07f436
parser produces ordered bn-fun information
Christian Urban <urbanc@in.tum.de>
parents:
1380
diff
changeset
|
354 |
|
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
355 |
thm trm1_bp1_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
356 |
thm trm1_bp1_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
357 |
thm trm1_bp1_bn |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
358 |
thm trm1_bp1_perm |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
359 |
thm trm1_bp1_induct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
360 |
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>
parents:
1232
diff
changeset
|
361 |
|
|
1367
9bbf56cdeb88
added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents:
1365
diff
changeset
|
362 |
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>
parents:
1232
diff
changeset
|
363 |
|
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
364 |
nominal_datatype trm3 = |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
365 |
Vr3 "name" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
366 |
| Ap3 "trm3" "trm3" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
367 |
| 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>
parents:
1232
diff
changeset
|
368 |
| 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>
parents:
1232
diff
changeset
|
369 |
and rassigns3 = |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
370 |
ANil |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
371 |
| ACons "name" "trm3" "rassigns3" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
372 |
binder |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
373 |
bv3 |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
374 |
where |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
375 |
"bv3 ANil = {}"
|
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
376 |
| "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>
parents:
1232
diff
changeset
|
377 |
|
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
378 |
thm trm3_rassigns3_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
379 |
thm trm3_rassigns3_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
380 |
thm trm3_rassigns3_bn |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
381 |
thm trm3_rassigns3_perm |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
382 |
thm trm3_rassigns3_induct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
383 |
thm trm3_rassigns3_distinct |
|
1367
9bbf56cdeb88
added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents:
1365
diff
changeset
|
384 |
|
|
9bbf56cdeb88
added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents:
1365
diff
changeset
|
385 |
(* compat should be |
|
9bbf56cdeb88
added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents:
1365
diff
changeset
|
386 |
compat (ANil) pi (PNil) \<equiv> TRue |
|
9bbf56cdeb88
added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents:
1365
diff
changeset
|
387 |
compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts' |
|
9bbf56cdeb88
added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents:
1365
diff
changeset
|
388 |
*) |
|
9bbf56cdeb88
added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents:
1365
diff
changeset
|
389 |
|
|
1251
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
390 |
(* 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>
parents:
1232
diff
changeset
|
391 |
|
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
392 |
nominal_datatype trm5 = |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
393 |
Vr5 "name" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
394 |
| Ap5 "trm5" "trm5" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
395 |
| 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>
parents:
1232
diff
changeset
|
396 |
and lts = |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
397 |
Lnil |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
398 |
| Lcons "name" "trm5" "lts" |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
399 |
binder |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
400 |
bv5 |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
401 |
where |
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
402 |
"bv5 Lnil = {}"
|
|
11b8798dea5d
parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents:
1232
diff
changeset
|
403 |
| "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>
parents:
1232
diff
changeset
|
404 |
|
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
405 |
thm trm5_lts_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
406 |
thm trm5_lts_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
407 |
thm trm5_lts_bn |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
408 |
thm trm5_lts_perm |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
409 |
thm trm5_lts_induct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
410 |
thm trm5_lts_distinct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
411 |
|
|
1285
e3ac56d3b7af
added example from my phd
Christian Urban <urbanc@in.tum.de>
parents:
1284
diff
changeset
|
412 |
(* example from my PHD *) |
|
e3ac56d3b7af
added example from my phd
Christian Urban <urbanc@in.tum.de>
parents:
1284
diff
changeset
|
413 |
|
|
e3ac56d3b7af
added example from my phd
Christian Urban <urbanc@in.tum.de>
parents:
1284
diff
changeset
|
414 |
atom_decl coname |
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
415 |
|
|
1341
c25f797c7e6e
Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1340
diff
changeset
|
416 |
nominal_datatype phd = |
|
1290
a7e7ffb7f362
modified for new binding format - hope it is the intended one
Christian Urban <urbanc@in.tum.de>
parents:
1287
diff
changeset
|
417 |
Ax "name" "coname" |
|
a7e7ffb7f362
modified for new binding format - hope it is the intended one
Christian Urban <urbanc@in.tum.de>
parents:
1287
diff
changeset
|
418 |
| Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 |
|
a7e7ffb7f362
modified for new binding format - hope it is the intended one
Christian Urban <urbanc@in.tum.de>
parents:
1287
diff
changeset
|
419 |
| AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 |
|
a7e7ffb7f362
modified for new binding format - hope it is the intended one
Christian Urban <urbanc@in.tum.de>
parents:
1287
diff
changeset
|
420 |
| AndL1 n::"name" t::"phd" "name" bind n in t |
|
a7e7ffb7f362
modified for new binding format - hope it is the intended one
Christian Urban <urbanc@in.tum.de>
parents:
1287
diff
changeset
|
421 |
| AndL2 n::"name" t::"phd" "name" bind n in t |
|
a7e7ffb7f362
modified for new binding format - hope it is the intended one
Christian Urban <urbanc@in.tum.de>
parents:
1287
diff
changeset
|
422 |
| 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>
parents:
1313
diff
changeset
|
423 |
| 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>
parents:
1313
diff
changeset
|
424 |
|
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
425 |
thm phd_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
426 |
thm phd_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
427 |
thm phd_bn |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
428 |
thm phd_perm |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
429 |
thm phd_induct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
430 |
thm phd_distinct |
|
1285
e3ac56d3b7af
added example from my phd
Christian Urban <urbanc@in.tum.de>
parents:
1284
diff
changeset
|
431 |
|
|
e3ac56d3b7af
added example from my phd
Christian Urban <urbanc@in.tum.de>
parents:
1284
diff
changeset
|
432 |
(* example form Leroy 96 about modules; OTT *) |
| 1284 | 433 |
|
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
434 |
nominal_datatype mexp = |
| 1296 | 435 |
Acc "path" |
436 |
| Stru "body" |
|
437 |
| Funct x::"name" "sexp" m::"mexp" bind x in m |
|
438 |
| FApp "mexp" "path" |
|
439 |
| Ascr "mexp" "sexp" |
|
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
440 |
and body = |
|
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
441 |
Empty |
| 1296 | 442 |
| Seq c::defn d::"body" bind "cbinders c" in d |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
443 |
and defn = |
| 1296 | 444 |
Type "name" "tyty" |
445 |
| Dty "name" |
|
446 |
| DStru "name" "mexp" |
|
447 |
| Val "name" "trmtrm" |
|
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
448 |
and sexp = |
|
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
449 |
Sig sbody |
| 1296 | 450 |
| SFunc "name" "sexp" "sexp" |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
451 |
and sbody = |
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
452 |
SEmpty |
| 1296 | 453 |
| SSeq C::spec D::sbody bind "Cbinders C" in D |
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
454 |
and spec = |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
455 |
Type1 "name" |
| 1296 | 456 |
| Type2 "name" "tyty" |
457 |
| SStru "name" "sexp" |
|
458 |
| SVal "name" "tyty" |
|
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
459 |
and tyty = |
| 1296 | 460 |
Tyref1 "name" |
461 |
| Tyref2 "path" "tyty" |
|
462 |
| Fun "tyty" "tyty" |
|
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
463 |
and path = |
| 1296 | 464 |
Sref1 "name" |
465 |
| Sref2 "path" "name" |
|
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
466 |
and trmtrm = |
| 1296 | 467 |
Tref1 "name" |
468 |
| Tref2 "path" "name" |
|
|
1340
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
469 |
| Lam' v::"name" "tyty" M::"trmtrm" bind v in M |
|
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
470 |
| App' "trmtrm" "trmtrm" |
|
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
471 |
| Let' "body" "trmtrm" |
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
472 |
binder |
|
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
473 |
cbinders :: "defn \<Rightarrow> atom set" |
|
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
474 |
and Cbinders :: "spec \<Rightarrow> atom set" |
|
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
475 |
where |
|
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
476 |
"cbinders (Type t T) = {atom t}"
|
|
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
477 |
| "cbinders (Dty t) = {atom t}"
|
|
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
478 |
| "cbinders (DStru x s) = {atom x}"
|
|
1396
08294f4d6c08
Linked parser to fv and alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1392
diff
changeset
|
479 |
| "cbinders (Val v M) = {atom v}"
|
|
1272
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
480 |
| "Cbinders (Type1 t) = {atom t}"
|
|
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
481 |
| "Cbinders (Type2 t T) = {atom t}"
|
|
6d140b2c751f
added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents:
1265
diff
changeset
|
482 |
| "Cbinders (SStru x S) = {atom x}"
|
|
1396
08294f4d6c08
Linked parser to fv and alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1392
diff
changeset
|
483 |
| "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>
parents:
1261
diff
changeset
|
484 |
|
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
485 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
486 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
487 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
488 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
489 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct |
|
1447
378b8c791de8
derive "inducts" from "induct" instead of lifting again is much faster.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1445
diff
changeset
|
490 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inducts |
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
491 |
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct |
|
1392
baa67b07f436
parser produces ordered bn-fun information
Christian Urban <urbanc@in.tum.de>
parents:
1380
diff
changeset
|
492 |
|
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
493 |
(* example 3 from Peter Sewell's bestiary *) |
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
494 |
|
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
495 |
nominal_datatype exp = |
|
1340
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
496 |
VarP "name" |
|
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
497 |
| AppP "exp" "exp" |
|
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
498 |
| LamP x::"name" e::"exp" bind x in e |
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
499 |
| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp'' p" in e1 |
|
1378
5c6c950812b1
All examples should work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1368
diff
changeset
|
500 |
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>
parents:
1313
diff
changeset
|
501 |
PVar "name" |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
502 |
| PUnit |
|
1378
5c6c950812b1
All examples should work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1368
diff
changeset
|
503 |
| PPair "pat3" "pat3" |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
504 |
binder |
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
505 |
bp'' :: "pat3 \<Rightarrow> atom set" |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
506 |
where |
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
507 |
"bp'' (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>
parents:
1465
diff
changeset
|
508 |
| "bp'' (PUnit) = {}"
|
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
509 |
| "bp'' (PPair p1 p2) = bp'' p1 \<union> bp'' p2" |
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
510 |
|
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
511 |
thm exp_pat3_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
512 |
thm exp_pat3_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
513 |
thm exp_pat3_bn |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
514 |
thm exp_pat3_perm |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
515 |
thm exp_pat3_induct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
516 |
thm exp_pat3_distinct |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
517 |
|
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
518 |
(* 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>
parents:
1340
diff
changeset
|
519 |
nominal_datatype exp6 = |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
520 |
EVar name |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
521 |
| EPair exp6 exp6 |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
522 |
| ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
523 |
and pat6 = |
|
1340
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
524 |
PVar' name |
|
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
525 |
| PUnit' |
|
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
526 |
| PPair' pat6 pat6 |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
527 |
binder |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
528 |
bp6 :: "pat6 \<Rightarrow> atom set" |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
529 |
where |
|
1340
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
530 |
"bp6 (PVar' x) = {atom x}"
|
|
f201eb6acafc
Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1338
diff
changeset
|
531 |
| "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>
parents:
1340
diff
changeset
|
532 |
| "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
|
1418
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
533 |
|
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
534 |
thm exp6_pat6_fv |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
535 |
thm exp6_pat6_inject |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
536 |
thm exp6_pat6_bn |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
537 |
thm exp6_pat6_perm |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
538 |
thm exp6_pat6_induct |
|
632b08744613
With the 4 cheats, all examples fully lift.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1416
diff
changeset
|
539 |
thm exp6_pat6_distinct |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
540 |
|
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
541 |
(* THE REST ARE NOT SUPPOSED TO WORK YET *) |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
542 |
|
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
543 |
(* 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>
parents:
1465
diff
changeset
|
544 |
(* 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>
parents:
1340
diff
changeset
|
545 |
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>
parents:
1465
diff
changeset
|
546 |
EVar' name |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
547 |
| EUnit' |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
548 |
| 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>
parents:
1465
diff
changeset
|
549 |
| ELetRec' l::lrbs e::exp7 bind "b7s l" in e, bind "b7s l" in l |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
550 |
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>
parents:
1465
diff
changeset
|
551 |
Assign' name exp7 |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
552 |
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>
parents:
1465
diff
changeset
|
553 |
Single' lrb |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
554 |
| More' lrb lrbs |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
555 |
binder |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
556 |
b7 :: "lrb \<Rightarrow> atom set" and |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
557 |
b7s :: "lrbs \<Rightarrow> atom set" |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
558 |
where |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
559 |
"b7 (Assign x e) = {atom x}"
|
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
560 |
| "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>
parents:
1340
diff
changeset
|
561 |
| "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>
parents:
1355
diff
changeset
|
562 |
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>
parents:
1465
diff
changeset
|
563 |
*) |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
564 |
|
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
565 |
(* 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>
parents:
1465
diff
changeset
|
566 |
(* |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
567 |
*** 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>
parents:
1465
diff
changeset
|
568 |
*** 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>
parents:
1340
diff
changeset
|
569 |
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>
parents:
1465
diff
changeset
|
570 |
EVar' name |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
571 |
| EUnit' |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
572 |
| 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>
parents:
1465
diff
changeset
|
573 |
| ELetRec' l::lrbs8 e::exp8 bind "b_lrbs8 l" in e, bind "b_lrbs8 l" in l |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
574 |
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>
parents:
1465
diff
changeset
|
575 |
K' x::name p::pat8 e::exp8 bind "b_pat p" in e |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
576 |
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>
parents:
1465
diff
changeset
|
577 |
S' fnclause |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
578 |
| ORs' fnclause fnclauses |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
579 |
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>
parents:
1465
diff
changeset
|
580 |
Clause' fnclauses |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
581 |
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>
parents:
1465
diff
changeset
|
582 |
Single' lrb8 |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
583 |
| More' lrb8 lrbs8 |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
584 |
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>
parents:
1465
diff
changeset
|
585 |
PVar'' name |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
586 |
| PUnit'' |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
587 |
| PPair'' pat8 pat8 |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
588 |
binder |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
589 |
b_lrbs8 :: "lrbs8 \<Rightarrow> atom set" and |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
590 |
b_pat :: "pat8 \<Rightarrow> atom set" and |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
591 |
b_fnclauses :: "fnclauses \<Rightarrow> atom set" and |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
592 |
b_fnclause :: "fnclause \<Rightarrow> atom set" and |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
593 |
b_lrb8 :: "lrb8 \<Rightarrow> atom set" |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
594 |
where |
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
595 |
"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>
parents:
1465
diff
changeset
|
596 |
| "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>
parents:
1465
diff
changeset
|
597 |
| "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>
parents:
1465
diff
changeset
|
598 |
| "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>
parents:
1465
diff
changeset
|
599 |
| "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>
parents:
1465
diff
changeset
|
600 |
| "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>
parents:
1465
diff
changeset
|
601 |
| "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>
parents:
1465
diff
changeset
|
602 |
| "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>
parents:
1465
diff
changeset
|
603 |
| "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>
parents:
1355
diff
changeset
|
604 |
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>
parents:
1465
diff
changeset
|
605 |
*) |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
606 |
(* example 4 from Terms.thy *) |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
607 |
(* fv_eqvt does not work, we need to repaire defined permute functions |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
608 |
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>
parents:
1465
diff
changeset
|
609 |
(* lists-datastructure does not work yet |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
610 |
nominal_datatype trm4 = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
611 |
Vr4 "name" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
612 |
| Ap4 "trm4" "trm4 list" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
613 |
| Lm4 x::"name" t::"trm4" bind x in t |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
614 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
615 |
thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
616 |
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>
parents:
1465
diff
changeset
|
617 |
*) |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
618 |
(* core haskell *) |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
619 |
atom_decl var |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
620 |
atom_decl tvar |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
621 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
622 |
(* there are types, coercion types and regular types *) |
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
623 |
(* list-data-structure |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
624 |
nominal_datatype tkind = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
625 |
KStar |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
626 |
| KFun "tkind" "tkind" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
627 |
and ckind = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
628 |
CKEq "ty" "ty" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
629 |
and ty = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
630 |
TVar "tvar" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
631 |
| TC "string" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
632 |
| TApp "ty" "ty" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
633 |
| TFun "string" "ty list" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
634 |
| TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
635 |
| TEq "ty" "ty" "ty" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
636 |
and co = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
637 |
CC "string" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
638 |
| CApp "co" "co" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
639 |
| CFun "string" "co list" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
640 |
| CAll tv::"tvar" "ckind" C::"co" bind tv in C |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
641 |
| CEq "co" "co" "co" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
642 |
| CSym "co" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
643 |
| CCir "co" "co" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
644 |
| CLeft "co" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
645 |
| CRight "co" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
646 |
| CSim "co" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
647 |
| CRightc "co" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
648 |
| CLeftc "co" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
649 |
| CCoe "co" "co" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
650 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
651 |
abbreviation |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
652 |
"atoms A \<equiv> atom ` A" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
653 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
654 |
nominal_datatype trm = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
655 |
Var "var" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
656 |
| C "string" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
657 |
| LAM tv::"tvar" "kind" t::"trm" bind tv in t |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
658 |
| APP "trm" "ty" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
659 |
| Lam v::"var" "ty" t::"trm" bind v in t |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
660 |
| App "trm" "trm" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
661 |
| Let x::"var" "ty" "trm" t::"trm" bind x in t |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
662 |
| Case "trm" "assoc list" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
663 |
| Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
664 |
and assoc = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
665 |
A p::"pat" t::"trm" bind "bv p" in t |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
666 |
and pat = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
667 |
K "string" "(tvar \<times> kind) list" "(var \<times> ty) list" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
668 |
binder |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
669 |
bv :: "pat \<Rightarrow> atom set" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
670 |
where |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
671 |
"bv (K s ts vs) = (atoms (set (map fst ts))) \<union> (atoms (set (map fst vs)))" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
672 |
*) |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
673 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
674 |
text {* weirdo example from Peter Sewell's bestiary *}
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
675 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
676 |
nominal_datatype weird = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
677 |
WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
678 |
bind x in p1, bind x in p2, bind y in p2, bind y in p3 |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
679 |
| WV "name" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
680 |
| WP "weird" "weird" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
681 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
682 |
thm permute_weird_raw.simps[no_vars] |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
683 |
thm alpha_weird_raw.intros[no_vars] |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
684 |
thm fv_weird_raw.simps[no_vars] |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
685 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
686 |
(* example 6 from Terms.thy *) |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
687 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
688 |
(* BV is not respectful, 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>
parents:
1465
diff
changeset
|
689 |
(* |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
690 |
nominal_datatype trm6 = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
691 |
Vr6 "name" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
692 |
| Lm6 x::"name" t::"trm6" bind x in t |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
693 |
| Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
694 |
binder |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
695 |
bv6 |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
696 |
where |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
697 |
"bv6 (Vr6 n) = {}"
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
698 |
| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
699 |
| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r" |
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
700 |
*) |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
701 |
|
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
702 |
(* example 7 from Terms.thy *) |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
703 |
(* BV is not respectful, 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>
parents:
1465
diff
changeset
|
704 |
(* |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
705 |
nominal_datatype trm7 = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
706 |
Vr7 "name" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
707 |
| Lm7 l::"name" r::"trm7" bind l in r |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
708 |
| Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
709 |
binder |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
710 |
bv7 |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
711 |
where |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
712 |
"bv7 (Vr7 n) = {atom n}"
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
713 |
| "bv7 (Lm7 n t) = bv7 t - {atom n}"
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
714 |
| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r" |
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
715 |
*) |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
716 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
717 |
(* example 8 from Terms.thy *) |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
718 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
719 |
(* 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>
parents:
1465
diff
changeset
|
720 |
(* |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
721 |
nominal_datatype foo8 = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
722 |
Foo0 "name" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
723 |
| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
724 |
and bar8 = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
725 |
Bar0 "name" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
726 |
| Bar1 "name" s::"name" b::"bar8" bind s in b |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
727 |
binder |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
728 |
bv8 |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
729 |
where |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
730 |
"bv8 (Bar0 x) = {}"
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
731 |
| "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>
parents:
1465
diff
changeset
|
732 |
*) |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
733 |
(* example 9 from Terms.thy *) |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
734 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
735 |
(* BV is not respectful, 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>
parents:
1465
diff
changeset
|
736 |
(* |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
737 |
nominal_datatype lam9 = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
738 |
Var9 "name" |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
739 |
| Lam9 n::"name" l::"lam9" bind n in l |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
740 |
and bla9 = |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
741 |
Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
742 |
binder |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
743 |
bv9 |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
744 |
where |
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
745 |
"bv9 (Var9 x) = {}"
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
746 |
| "bv9 (Lam9 x b) = {atom x}"
|
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
747 |
*) |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
748 |
|
|
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
749 |
(* Type schemes with separate datatypes *) |
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
750 |
nominal_datatype T = |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
751 |
TVar "name" |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
752 |
| TFun "T" "T" |
|
1398
1f3c01345c9e
Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1396
diff
changeset
|
753 |
|
|
1466
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
754 |
(* PROBLEM: |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
755 |
*** exception Datatype raised |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
756 |
*** (line 218 of "/usr/local/src/Isabelle_16-Mar-2010/src/HOL/Tools/Datatype/datatype_aux.ML") |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
757 |
*** At command "nominal_datatype". |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
758 |
nominal_datatype TyS = |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
759 |
TAll xs::"name list" ty::"T" bind xs in ty |
|
d18defacda25
commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents:
1465
diff
changeset
|
760 |
*) |
|
1312
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
761 |
|
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
762 |
(* example 9 from Peter Sewell's bestiary *) |
|
b0eae8c93314
added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents:
1304
diff
changeset
|
763 |
(* 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>
parents:
1261
diff
changeset
|
764 |
|
|
961
0f88e04eb486
Variable takes a 'name'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
954
diff
changeset
|
765 |
end |
|
1223
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
parents:
1194
diff
changeset
|
766 |
|
|
160343d86a6f
"raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
parents:
1194
diff
changeset
|
767 |
|
|
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>
parents:
1223
diff
changeset
|
768 |