Nominal/Ex/LetPat.thy
author Christian Urban <urbanc@in.tum.de>
Wed, 22 Jun 2011 12:18:22 +0100
changeset 2885 1264f2a21ea9
parent 2648 5d9724ad543d
child 2950 0911cb7bf696
permissions -rw-r--r--
some rudimentary infrastructure for storing data about nominal datatypes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
     1
theory LetPat
2454
9ffee4eb1ae1 renamed NewParser to Nominal2
Christian Urban <urbanc@in.tum.de>
parents: 2436
diff changeset
     2
imports "../Nominal2"
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
begin
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
atom_decl name
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
2026
7f504136149b Another example where only alpha_eqvt fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1773
diff changeset
     7
nominal_datatype trm =
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
  Var "name"
2026
7f504136149b Another example where only alpha_eqvt fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1773
diff changeset
     9
| App "trm" "trm"
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    10
| Lam x::"name" t::"trm"       bind (set) x in t
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    11
| Let p::"pat" "trm" t::"trm"  bind (set) "f p" in t
2026
7f504136149b Another example where only alpha_eqvt fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1773
diff changeset
    12
and pat =
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    13
  PN
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
| PS "name"
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
| PD "name" "name"
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
binder
2026
7f504136149b Another example where only alpha_eqvt fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1773
diff changeset
    17
  f::"pat \<Rightarrow> atom set"
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
where
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
  "f PN = {}"
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
| "f (PD x y) = {atom x, atom y}"
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
| "f (PS x) = {atom x}"
2300
9fb315392493 added FSet to the correct paper
Christian Urban <urbanc@in.tum.de>
parents: 2120
diff changeset
    22
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    23
thm trm_pat.distinct
2026
7f504136149b Another example where only alpha_eqvt fails.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1773
diff changeset
    24
thm trm_pat.induct
2436
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    25
thm trm_pat.exhaust
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    26
thm trm_pat.fv_defs
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    27
thm trm_pat.bn_defs
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    28
thm trm_pat.perm_simps
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    29
thm trm_pat.eq_iff
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    30
thm trm_pat.fv_bn_eqvt
3885dc2669f9 cleaned up (almost completely) the examples
Christian Urban <urbanc@in.tum.de>
parents: 2311
diff changeset
    31
thm trm_pat.size_eqvt
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    32
2082
0854af516f14 cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
parents: 2030
diff changeset
    33
1596
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    34
end
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    35
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    36
c69d9fb16785 Move Ex1 and Ex2 out of Test
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37