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
|
16 |
\<Omega>
|
|
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
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
| TAll a::tvar kind t::ty binds a in t
|
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
| TEx a::tvar kind t::ty binds a in t
|
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
| TLam a::tvar kind t::ty binds 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
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
| Lam x::var ty t::trm binds 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
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
| LAM a::tvar kind t::trm binds 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
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
| Unpack a::tvar x::var trm t::trm binds 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>
diff
changeset
|
45 |
thm ty_trec.distinct
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
thm ty_trec.induct
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
thm ty_trec.inducts
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
48 |
thm ty_trec.exhaust
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
49 |
thm ty_trec.strong_exhaust
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
50 |
thm ty_trec.fv_defs
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
51 |
thm ty_trec.bn_defs
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
52 |
thm ty_trec.perm_simps
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
thm ty_trec.eq_iff
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
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>
diff
changeset
|
55 |
thm ty_trec.size_eqvt
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
thm ty_trec.supports
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
57 |
thm ty_trec.fsupp
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
thm ty_trec.supp
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
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>
diff
changeset
|
61 |
thm trm_rec.distinct
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
62 |
thm trm_rec.induct
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
63 |
thm trm_rec.inducts
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
64 |
thm trm_rec.exhaust
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
65 |
thm trm_rec.strong_exhaust
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
66 |
thm trm_rec.fv_defs
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
67 |
thm trm_rec.bn_defs
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
68 |
thm trm_rec.perm_simps
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
69 |
thm trm_rec.eq_iff
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
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>
diff
changeset
|
71 |
thm trm_rec.size_eqvt
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
thm trm_rec.supports
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
thm trm_rec.fsupp
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
74 |
thm trm_rec.supp
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
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 |
|