Nominal/Test.thy
author Christian Urban <urbanc@in.tum.de>
Wed, 24 Mar 2010 12:53:39 +0100
changeset 1629 a0ca7d9f6781
parent 1600 e33e37fd4c7d
child 1655 9cec4269b7f9
permissions -rw-r--r--
some tuning; possible fix for strange paper generation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1629
a0ca7d9f6781 some tuning; possible fix for strange paper generation
Christian Urban <urbanc@in.tum.de>
parents: 1600
diff changeset
     1
(*<*)
954
c009d2535896 very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
theory Test
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1595
diff changeset
     3
imports "Parser"
954
c009d2535896 very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
begin
c009d2535896 very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
1600
e33e37fd4c7d More reorganization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1599
diff changeset
     6
(* This file contains only the examples that are not supposed to work yet. *)
e33e37fd4c7d More reorganization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1599
diff changeset
     7
e33e37fd4c7d More reorganization.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1599
diff changeset
     8
1428
4029105011ca Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1418
diff changeset
     9
atom_decl name
4029105011ca Show that the new types are in finite support typeclass.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1418
diff changeset
    10
1465
4de35639fef0 added another supp-proof for the non-recursive case
Christian Urban <urbanc@in.tum.de>
parents: 1461
diff changeset
    11
ML {* val _ = recursive := false  *}
1367
9bbf56cdeb88 added compat definitions to some examples
Christian Urban <urbanc@in.tum.de>
parents: 1365
diff changeset
    12
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    13
(* example 7 from Peter Sewell's bestiary *)
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    14
(* dest_Const raised
1341
c25f797c7e6e Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1340
diff changeset
    15
nominal_datatype exp7 =
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    16
  EVar' name
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    17
| EUnit'
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    18
| EPair' exp7 exp7
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    19
| 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
    20
and lrb =
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    21
  Assign' name exp7
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    22
and lrbs =
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    23
  Single' lrb
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    24
| More' lrb lrbs
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    25
binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    26
  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
    27
  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
    28
where
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    29
  "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
    30
| "b7s (Single a) = b7 a"
1341
c25f797c7e6e Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1340
diff changeset
    31
| "b7s (More a as) = (b7 a) \<union> (b7s as)"
1361
1e811e3424f3 With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1355
diff changeset
    32
thm alpha_exp7_raw_alpha_lrb_raw_alpha_lrbs_raw.intros
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    33
*)
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    34
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    35
(* example 8 from Peter Sewell's bestiary *)
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    36
(*
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    37
*** fv_bn: recursive argument, but wrong datatype.
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    38
*** At command "nominal_datatype".
1341
c25f797c7e6e Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1340
diff changeset
    39
nominal_datatype exp8 =
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    40
  EVar' name
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    41
| EUnit'
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    42
| EPair' exp8 exp8
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    43
| 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
    44
and fnclause =
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    45
  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
    46
and fnclauses =
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    47
  S' fnclause
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    48
| ORs' fnclause fnclauses
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    49
and lrb8 =
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    50
  Clause' fnclauses
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    51
and lrbs8 =
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    52
  Single' lrb8
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    53
| More' lrb8 lrbs8
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    54
and pat8 =
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    55
  PVar'' name
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    56
| PUnit''
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    57
| PPair'' pat8 pat8
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    58
binder
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
    59
  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
    60
  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
    61
  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
    62
  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
    63
  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
    64
where
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    65
  "b_lrbs8 (Single' l) = b_lrb8 l"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    66
| "b_lrbs8 (More' l ls) = b_lrb8 l \<union> b_lrbs8 ls"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    67
| "b_pat (PVar'' x) = {atom x}"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    68
| "b_pat (PUnit'') = {}"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    69
| "b_pat (PPair'' p1 p2) = b_pat p1 \<union> b_pat p2"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    70
| "b_fnclauses (S' fc) = (b_fnclause fc)"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    71
| "b_fnclauses (ORs' fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    72
| "b_lrb8 (Clause' fcs) = (b_fnclauses fcs)"
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    73
| "b_fnclause (K' x pat exp8) = {atom x}"
1361
1e811e3424f3 With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1355
diff changeset
    74
thm alpha_exp8_raw_alpha_fnclause_raw_alpha_fnclauses_raw_alpha_lrb8_raw_alpha_lrbs8_raw_alpha_pat8_raw.intros
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    75
*)
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    76
(* example 4 from Terms.thy *)
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    77
(* 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
    78
   defined fv and defined alpha... *)
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    79
(* lists-datastructure does not work yet
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    80
nominal_datatype trm4 =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    81
  Vr4 "name"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    82
| Ap4 "trm4" "trm4 list"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    83
| Lm4 x::"name" t::"trm4"  bind x in t
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    84
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    85
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
    86
thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    87
*)
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    88
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    89
(* example 8 from Terms.thy *)
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    90
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    91
(* Binding in a term under a bn, needs to fail *)
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
    92
(*
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    93
nominal_datatype foo8 =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    94
  Foo0 "name"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    95
| 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
    96
and bar8 =
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    97
  Bar0 "name"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
    98
| 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
    99
binder
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   100
  bv8
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   101
where
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   102
  "bv8 (Bar0 x) = {}"
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   103
| "bv8 (Bar1 v x b) = {atom v}"
1466
d18defacda25 commented out examples that should not work; but for example type-scheme example should work
Christian Urban <urbanc@in.tum.de>
parents: 1465
diff changeset
   104
*)
1398
1f3c01345c9e Reordered examples in Test.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1396
diff changeset
   105
1312
b0eae8c93314 added some more examples from Peter Sewell's bestiary
Christian Urban <urbanc@in.tum.de>
parents: 1304
diff changeset
   106
(* 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
   107
(* run out of steam at the moment *)
1265
fc8f5897b00a first attempt to make sense out of the core-haskell definition
Christian Urban <urbanc@in.tum.de>
parents: 1261
diff changeset
   108
961
0f88e04eb486 Variable takes a 'name'.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 954
diff changeset
   109
end
1629
a0ca7d9f6781 some tuning; possible fix for strange paper generation
Christian Urban <urbanc@in.tum.de>
parents: 1600
diff changeset
   110
(*>*)
1223
160343d86a6f "raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
parents: 1194
diff changeset
   111
160343d86a6f "raw"-ified the term-constructors and types given in the specification
Christian Urban <urbanc@in.tum.de>
parents: 1194
diff changeset
   112