Nominal/Test.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 23 Mar 2010 08:42:02 +0100
changeset 1596 c69d9fb16785
parent 1595 aeed597d2043
child 1597 af34dd3418fe
permissions -rw-r--r--
Move Ex1 and Ex2 out of Test
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1595
diff changeset
     2
imports "Parser"
954
c009d2535896 very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
c009d2535896 very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
1428
4029105011ca Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1418
diff changeset
     5
atom_decl name
4029105011ca Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1418
diff changeset
     6
1465
4de35639fef0 added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents: 1461
diff changeset
     7
ML {* val _ = recursive := false  *}
1367
9bbf56cdeb88 added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents: 1365
diff changeset
     8
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
     9
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
    10
  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
    11
| App0 "trm0" "trm0"
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    12
| 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
    13
| 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
    14
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
    15
  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
    16
| 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
    17
| 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
    18
binder
1299
cbcd4997dac5 most tests work - the ones that do not I commented out
Christian Urban <urbanc@in.tum.de>
parents: 1298
diff changeset
    19
  f0::"pat0 \<Rightarrow> atom set"
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    20
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
    21
  "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
    22
| "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
    23
| "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
    24
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    25
thm trm0_pat0.fv
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    26
thm trm0_pat0.eq_iff
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    27
thm trm0_pat0.bn
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    28
thm trm0_pat0.perm
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    29
thm trm0_pat0.induct
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    30
thm trm0_pat0.distinct
1553
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1549
diff changeset
    31
thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
954
c009d2535896 very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
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
    33
(* 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
    34
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents: 1232
diff changeset
    35
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
    36
  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
    37
| Ap1 "trm1" "trm1"
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    38
| Lm1 x::"name" t::"trm1"       bind x in t
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    39
| 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
    40
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
    41
  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
    42
| 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
    43
| 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
    44
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
    45
  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
    46
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
    47
  "bv1 (BUnit1) = {}"
1392
baa67b07f436 parser produces ordered bn-fun information
Christian Urban <urbanc@in.tum.de>
parents: 1380
diff changeset
    48
| "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
    49
| "bv1 (BV1 x) = {atom x}"
1392
baa67b07f436 parser produces ordered bn-fun information
Christian Urban <urbanc@in.tum.de>
parents: 1380
diff changeset
    50
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    51
thm trm1_bp1.fv
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    52
thm trm1_bp1.eq_iff
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    53
thm trm1_bp1.bn
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    54
thm trm1_bp1.perm
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    55
thm trm1_bp1.induct
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    56
thm trm1_bp1.distinct
1553
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1549
diff changeset
    57
thm trm1_bp1.fv[simplified trm1_bp1.supp]
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
    58
1367
9bbf56cdeb88 added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents: 1365
diff changeset
    59
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
    60
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents: 1232
diff changeset
    61
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
    62
  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
    63
| 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
    64
| 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
    65
| 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
    66
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
    67
  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
    68
| 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
    69
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
    70
  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
    71
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
    72
  "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
    73
| "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
    74
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    75
thm trm3_rassigns3.fv
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    76
thm trm3_rassigns3.eq_iff
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    77
thm trm3_rassigns3.bn
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    78
thm trm3_rassigns3.perm
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    79
thm trm3_rassigns3.induct
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    80
thm trm3_rassigns3.distinct
1553
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1549
diff changeset
    81
thm trm3_rassigns3.fv[simplified trm3_rassigns3.supp]
1367
9bbf56cdeb88 added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents: 1365
diff changeset
    82
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
    83
(* 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
    84
11b8798dea5d parsing and definition of raw datatype and bv-function work (not very beautiful)
Christian Urban <urbanc@in.tum.de>
parents: 1232
diff changeset
    85
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
    86
  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
    87
| 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
    88
| 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
    89
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
    90
  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
    91
| 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
    92
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
    93
  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
    94
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
    95
  "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
    96
| "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
    97
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    98
thm trm5_lts.fv
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
    99
thm trm5_lts.eq_iff
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   100
thm trm5_lts.bn
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   101
thm trm5_lts.perm
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   102
thm trm5_lts.induct
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   103
thm trm5_lts.distinct
1553
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1549
diff changeset
   104
thm trm5_lts.fv[simplified trm5_lts.supp]
1285
e3ac56d3b7af added example from my phd
Christian Urban <urbanc@in.tum.de>
parents: 1284
diff changeset
   105
e3ac56d3b7af added example from my phd
Christian Urban <urbanc@in.tum.de>
parents: 1284
diff changeset
   106
(* example form Leroy 96 about modules; OTT *)
1284
212f3ab40cc2 streamlined parser
Christian Urban <urbanc@in.tum.de>
parents: 1283
diff changeset
   107
1272
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   108
nominal_datatype mexp =
1296
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   109
  Acc "path"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   110
| Stru "body"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   111
| Funct x::"name" "sexp" m::"mexp"    bind x in m
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   112
| FApp "mexp" "path"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   113
| Ascr "mexp" "sexp"
1272
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   114
and body =
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   115
  Empty
1296
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   116
| 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
   117
and defn =
1296
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   118
  Type "name" "tyty"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   119
| Dty "name"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   120
| DStru "name" "mexp"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   121
| Val "name" "trmtrm"
1272
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   122
and sexp =
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   123
  Sig sbody
1296
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   124
| SFunc "name" "sexp" "sexp"
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   125
and sbody =
1272
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   126
  SEmpty
1296
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   127
| 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
   128
and spec =
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   129
  Type1 "name"
1296
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   130
| Type2 "name" "tyty"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   131
| SStru "name" "sexp"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   132
| SVal "name" "tyty"
1272
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   133
and tyty =
1296
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   134
  Tyref1 "name"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   135
| Tyref2 "path" "tyty"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   136
| Fun "tyty" "tyty"
1272
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   137
and path =
1296
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   138
  Sref1 "name"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   139
| Sref2 "path" "name"
1272
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   140
and trmtrm =
1296
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   141
  Tref1 "name"
790940e90db2 some tuning
Christian Urban <urbanc@in.tum.de>
parents: 1295
diff changeset
   142
| Tref2 "path" "name"
1340
f201eb6acafc Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1338
diff changeset
   143
| 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
   144
| App' "trmtrm" "trmtrm"
f201eb6acafc Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1338
diff changeset
   145
| Let' "body" "trmtrm"
1272
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   146
binder
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   147
    cbinders :: "defn \<Rightarrow> atom set"
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   148
and Cbinders :: "spec \<Rightarrow> atom set"
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   149
where
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   150
  "cbinders (Type t T) = {atom t}"
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   151
| "cbinders (Dty t) = {atom t}"
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   152
| "cbinders (DStru x s) = {atom x}"
1396
08294f4d6c08 Linked parser to fv and alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1392
diff changeset
   153
| "cbinders (Val v M) = {atom v}"
1272
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   154
| "Cbinders (Type1 t) = {atom t}"
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   155
| "Cbinders (Type2 t T) = {atom t}"
6d140b2c751f added ott-example about Leroy96
Christian Urban <urbanc@in.tum.de>
parents: 1265
diff changeset
   156
| "Cbinders (SStru x S) = {atom x}"
1396
08294f4d6c08 Linked parser to fv and alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1392
diff changeset
   157
| "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
   158
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   159
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   160
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.eq_iff
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   161
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.bn
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   162
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.perm
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   163
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   164
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   165
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
1553
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1549
diff changeset
   166
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1549
diff changeset
   167
thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
1392
baa67b07f436 parser produces ordered bn-fun information
Christian Urban <urbanc@in.tum.de>
parents: 1380
diff changeset
   168
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   169
(* 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
   170
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   171
nominal_datatype exp =
1340
f201eb6acafc Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1338
diff changeset
   172
  VarP "name"
f201eb6acafc Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1338
diff changeset
   173
| AppP "exp" "exp"
f201eb6acafc Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1338
diff changeset
   174
| 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
   175
| 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
   176
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
   177
  PVar "name"
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   178
| PUnit
1378
5c6c950812b1 All examples should work.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1368
diff changeset
   179
| PPair "pat3" "pat3"
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   180
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
   181
  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
   182
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
   183
  "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
   184
| "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
   185
| "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
   186
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   187
thm exp_pat3.fv
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   188
thm exp_pat3.eq_iff
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   189
thm exp_pat3.bn
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   190
thm exp_pat3.perm
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   191
thm exp_pat3.induct
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   192
thm exp_pat3.distinct
1553
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1549
diff changeset
   193
thm exp_pat3.fv[simplified exp_pat3.supp]
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   194
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   195
(* 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
   196
nominal_datatype exp6 =
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   197
  EVar name
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   198
| EPair exp6 exp6
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   199
| 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
   200
and pat6 =
1340
f201eb6acafc Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1338
diff changeset
   201
  PVar' name
f201eb6acafc Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1338
diff changeset
   202
| PUnit'
f201eb6acafc Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1338
diff changeset
   203
| PPair' pat6 pat6
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   204
binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   205
  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
   206
where
1340
f201eb6acafc Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1338
diff changeset
   207
  "bp6 (PVar' x) = {atom x}"
f201eb6acafc Lift BV,FV,Permutations and injection :).
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1338
diff changeset
   208
| "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
   209
| "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
   210
1515
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   211
thm exp6_pat6.fv
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   212
thm exp6_pat6.eq_iff
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   213
thm exp6_pat6.bn
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   214
thm exp6_pat6.perm
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   215
thm exp6_pat6.induct
76fa21f27f22 Rename "_property" to ".property"
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1510
diff changeset
   216
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
   217
1553
4355eb3b7161 Automatically derive support for datatypes with at-most one binding per constructor.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1549
diff changeset
   218
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   219
(* THE REST ARE NOT SUPPOSED TO WORK YET *)
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   220
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   221
(* 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
   222
(* 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
   223
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
   224
  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
   225
| 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
   226
| 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
   227
| 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
   228
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
   229
  Assign' name exp7
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   230
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
   231
  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
   232
| More' lrb lrbs
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   233
binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   234
  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
   235
  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
   236
where
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   237
  "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
   238
| "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
   239
| "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
   240
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
   241
*)
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   242
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   243
(* 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
   244
(*
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
   245
*** 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
   246
*** 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
   247
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
   248
  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
   249
| 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
   250
| 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
   251
| 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
   252
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
   253
  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
   254
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
   255
  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
   256
| ORs' fnclause fnclauses
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   257
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
   258
  Clause' fnclauses
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   259
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
   260
  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
   261
| More' lrb8 lrbs8
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   262
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
   263
  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
   264
| 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
   265
| PPair'' pat8 pat8
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   266
binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   267
  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
   268
  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
   269
  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
   270
  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
   271
  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
   272
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
   273
  "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
   274
| "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
   275
| "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
   276
| "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
   277
| "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
   278
| "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
   279
| "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
   280
| "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
   281
| "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
   282
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
   283
*)
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   284
(* example 4 from Terms.thy *)
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   285
(* 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
   286
   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
   287
(* lists-datastructure does not work yet
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   288
nominal_datatype trm4 =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   289
  Vr4 "name"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   290
| Ap4 "trm4" "trm4 list"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   291
| Lm4 x::"name" t::"trm4"  bind x in t
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   292
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   293
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
   294
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
   295
*)
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   296
(* core haskell *)
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   297
atom_decl var
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   298
atom_decl tvar
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   299
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   300
(* 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
   301
(* list-data-structure
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   302
nominal_datatype tkind =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   303
  KStar
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   304
| KFun "tkind" "tkind"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   305
and ckind =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   306
  CKEq "ty" "ty"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   307
and ty =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   308
  TVar "tvar"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   309
| TC "string"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   310
| TApp "ty" "ty"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   311
| TFun "string" "ty list"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   312
| 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
   313
| TEq "ty" "ty" "ty"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   314
and co =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   315
  CC "string"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   316
| CApp "co" "co"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   317
| CFun "string" "co list"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   318
| 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
   319
| CEq "co" "co" "co"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   320
| CSym "co"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   321
| CCir "co" "co"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   322
| CLeft "co"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   323
| CRight "co"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   324
| CSim "co"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   325
| CRightc "co"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   326
| CLeftc "co"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   327
| CCoe "co" "co"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   328
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   329
abbreviation
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   330
  "atoms A \<equiv> atom ` A"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   331
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   332
nominal_datatype trm =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   333
  Var "var"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   334
| C "string"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   335
| 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
   336
| APP "trm" "ty"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   337
| 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
   338
| App "trm" "trm"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   339
| 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
   340
| Case "trm" "assoc list"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   341
| 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
   342
and assoc =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   343
  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
   344
and pat =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   345
  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
   346
binder
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   347
 bv :: "pat \<Rightarrow> atom set"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   348
where
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   349
 "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
   350
*)
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   351
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   352
(* example 8 from Terms.thy *)
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   353
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   354
(* 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
   355
(*
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   356
nominal_datatype foo8 =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   357
  Foo0 "name"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   358
| 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
   359
and bar8 =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   360
  Bar0 "name"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   361
| 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
   362
binder
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   363
  bv8
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   364
where
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   365
  "bv8 (Bar0 x) = {}"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   366
| "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
   367
*)
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   368
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   369
(* 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
   370
(* 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
   371
961
0f88e04eb486 Variable takes a 'name'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 954
diff changeset
   372
end
1223
160343d86a6f "raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
parents: 1194
diff changeset
   373
160343d86a6f "raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
parents: 1194
diff changeset
   374
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
   375