2436
+ − 1
theory TypeVarsTest
2454
+ − 2
imports "../Nominal2"
2436
+ − 3
begin
+ − 4
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 5
(* a nominal datatype with type variables and sorts *)
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 6
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 7
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 8
(* the sort constraints need to be attached to the *)
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 9
(* first occurence of the type variables on the *)
2622
+ − 10
(* right-hand side *)
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 11
2436
+ − 12
atom_decl name
+ − 13
+ − 14
class s1
+ − 15
class s2
+ − 16
2571
+ − 17
instance nat :: s1 ..
+ − 18
instance int :: s2 ..
+ − 19
3091
578e0265b235
the default sort for type-variables in nominal specifications is fs; it is automatically addded
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 20
nominal_datatype ('a::s1, 'b::s2, 'c::at) lam =
2436
+ − 21
Var "name"
3065
+ − 22
| App "('a, 'b, 'c) lam" "('a, 'b, 'c) lam"
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 23
| Lam x::"name" l::"('a, 'b, 'c) lam" binds x in l
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24
| Foo "'a" "'b"
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 25
| Bar x::"'c" l::"('a, 'b, 'c) lam" binds x in l (* Bar binds a polymorphic atom *)
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 26
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 27
term Foo
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 28
term Bar
2436
+ − 29
+ − 30
thm lam.distinct
+ − 31
thm lam.induct
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 32
thm lam.exhaust
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 33
thm lam.strong_exhaust
2436
+ − 34
thm lam.fv_defs
+ − 35
thm lam.bn_defs
+ − 36
thm lam.perm_simps
+ − 37
thm lam.eq_iff
+ − 38
thm lam.fv_bn_eqvt
+ − 39
thm lam.size_eqvt
2557
781fbc8c0591
fixed locally the problem with the function package; all tests work again
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 40
2730
+ − 41
2888
eda5aeb056a6
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 42
nominal_datatype ('alpha, 'beta, 'gamma) psi =
2730
+ − 43
PsiNil
3091
578e0265b235
the default sort for type-variables in nominal specifications is fs; it is automatically addded
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 44
| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi"
2730
+ − 45
2436
+ − 46
3029
+ − 47
nominal_datatype 'a foo =
3091
578e0265b235
the default sort for type-variables in nominal specifications is fs; it is automatically addded
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 48
Node x::"name" f::"'a foo" binds x in f
3029
+ − 49
| Leaf "'a"
+ − 50
+ − 51
term "Leaf"
+ − 52
+ − 53
+ − 54
+ − 55
2436
+ − 56
end
+ − 57
+ − 58
+ − 59