Nominal/Ex/SystemFOmega.thy
author Christian Urban <urbanc@in.tum.de>
Fri, 07 Jan 2011 02:30:00 +0000
changeset 2650 e5fa8de0e4bd
parent 2622 e6e6a3da81aa
child 2950 0911cb7bf696
permissions -rw-r--r--
derived equivariance for the function graph and function relation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2581
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory SystemFOmega
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
imports "../Nominal2"
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
text {*
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
  System from the F-ing paper by Rossberg, Russo and 
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
  Dreyer, TLDI'10
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
*}
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
atom_decl var
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
atom_decl tvar
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
atom_decl label
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    15
nominal_datatype kind =
2622
e6e6a3da81aa tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2617
diff changeset
    16
  \<Omega> 
e6e6a3da81aa tuned examples
Christian Urban <urbanc@in.tum.de>
parents: 2617
diff changeset
    17
| KFun kind kind
2581
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
nominal_datatype ty =
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
  TVar tvar
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    21
| TFun ty ty
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    22
| TAll a::tvar kind t::ty  bind a in t
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    23
| TEx  a::tvar kind t::ty  bind a in t
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    24
| TLam a::tvar kind t::ty  bind a in t
2581
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
| TApp ty ty
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
| TRec trec
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
and trec =
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    28
  TRNil
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
| TRCons label ty trec 
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
nominal_datatype trm =
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
  Var var
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    33
| Lam x::var ty t::trm  bind x in t
2581
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
| App trm trm
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
| Dot trm label
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    36
| LAM a::tvar kind t::trm  bind a in t
2581
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    37
| APP trm ty
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
| Pack ty trm
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    39
| Unpack a::tvar x::var trm t::trm  bind a x in t
2581
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
| Rec rec 
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
and rec =
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
  RNil
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
| RCons label trm rec
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    45
thm ty_trec.distinct
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    46
thm ty_trec.induct
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    47
thm ty_trec.inducts
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    48
thm ty_trec.exhaust 
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    49
thm ty_trec.strong_exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    50
thm ty_trec.fv_defs
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    51
thm ty_trec.bn_defs
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    52
thm ty_trec.perm_simps
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    53
thm ty_trec.eq_iff
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    54
thm ty_trec.fv_bn_eqvt
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    55
thm ty_trec.size_eqvt
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    56
thm ty_trec.supports
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    57
thm ty_trec.fsupp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    58
thm ty_trec.supp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    59
thm ty_trec.fresh
2581
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    60
2617
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    61
thm trm_rec.distinct
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    62
thm trm_rec.induct
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    63
thm trm_rec.inducts
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    64
thm trm_rec.exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    65
thm trm_rec.strong_exhaust
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    66
thm trm_rec.fv_defs
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    67
thm trm_rec.bn_defs
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    68
thm trm_rec.perm_simps
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    69
thm trm_rec.eq_iff
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    70
thm trm_rec.fv_bn_eqvt
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    71
thm trm_rec.size_eqvt
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    72
thm trm_rec.supports
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    73
thm trm_rec.fsupp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    74
thm trm_rec.supp
e44551d067e6 properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
parents: 2581
diff changeset
    75
thm trm_rec.fresh
2581
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
end
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    79
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    80
3696659358c8 added example from the F-ing paper by Rossberg, Russo and Dreyer
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    81