equal
deleted
inserted
replaced
79 quotient TY = ty / aty |
79 quotient TY = ty / aty |
80 and TRM = trm / atrm |
80 and TRM = trm / atrm |
81 by (auto intro: alpha_equivps) |
81 by (auto intro: alpha_equivps) |
82 |
82 |
83 quotient_def |
83 quotient_def |
84 TYP :: "TYP :: KIND" |
84 "TYP :: KIND" |
85 where |
85 as |
86 "Type" |
86 "Type" |
87 |
87 |
88 quotient_def |
88 quotient_def |
89 KPI :: "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
89 "KPI :: TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND" |
90 where |
90 as |
91 "KPi" |
91 "KPi" |
92 |
92 |
93 quotient_def |
93 quotient_def |
94 TCONST :: "TCONST :: ident \<Rightarrow> TY" |
94 "TCONST :: ident \<Rightarrow> TY" |
95 where |
95 as |
96 "TConst" |
96 "TConst" |
97 |
97 |
98 quotient_def |
98 quotient_def |
99 TAPP :: "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY" |
99 "TAPP :: TY \<Rightarrow> TRM \<Rightarrow> TY" |
100 where |
100 as |
101 "TApp" |
101 "TApp" |
102 |
102 |
103 quotient_def |
103 quotient_def |
104 TPI :: "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY" |
104 "TPI :: TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY" |
105 where |
105 as |
106 "TPi" |
106 "TPi" |
107 |
107 |
108 (* FIXME: does not work with CONST *) |
108 (* FIXME: does not work with CONST *) |
109 quotient_def |
109 quotient_def |
110 CONS :: "CONS :: ident \<Rightarrow> TRM" |
110 "CONS :: ident \<Rightarrow> TRM" |
111 where |
111 as |
112 "Const" |
112 "Const" |
113 |
113 |
114 quotient_def |
114 quotient_def |
115 VAR :: "VAR :: name \<Rightarrow> TRM" |
115 "VAR :: name \<Rightarrow> TRM" |
116 where |
116 as |
117 "Var" |
117 "Var" |
118 |
118 |
119 quotient_def |
119 quotient_def |
120 APP :: "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM" |
120 "APP :: TRM \<Rightarrow> TRM \<Rightarrow> TRM" |
121 where |
121 as |
122 "App" |
122 "App" |
123 |
123 |
124 quotient_def |
124 quotient_def |
125 LAM :: "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM" |
125 "LAM :: TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM" |
126 where |
126 as |
127 "Lam" |
127 "Lam" |
128 |
128 |
129 thm TYP_def |
129 thm TYP_def |
130 thm KPI_def |
130 thm KPI_def |
131 thm TCONST_def |
131 thm TCONST_def |
136 thm APP_def |
136 thm APP_def |
137 thm LAM_def |
137 thm LAM_def |
138 |
138 |
139 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *) |
139 (* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *) |
140 quotient_def |
140 quotient_def |
141 FV_kind :: "FV_kind :: KIND \<Rightarrow> name set" |
141 "FV_kind :: KIND \<Rightarrow> name set" |
142 where |
142 as |
143 "fv_kind" |
143 "fv_kind" |
144 |
144 |
145 quotient_def |
145 quotient_def |
146 FV_ty :: "FV_ty :: TY \<Rightarrow> name set" |
146 "FV_ty :: TY \<Rightarrow> name set" |
147 where |
147 as |
148 "fv_ty" |
148 "fv_ty" |
149 |
149 |
150 quotient_def |
150 quotient_def |
151 FV_trm :: "FV_trm :: TRM \<Rightarrow> name set" |
151 "FV_trm :: TRM \<Rightarrow> name set" |
152 where |
152 as |
153 "fv_trm" |
153 "fv_trm" |
154 |
154 |
155 thm FV_kind_def |
155 thm FV_kind_def |
156 thm FV_ty_def |
156 thm FV_ty_def |
157 thm FV_trm_def |
157 thm FV_trm_def |
162 perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked) |
162 perm_ty \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" (unchecked) |
163 perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked) |
163 perm_trm \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" (unchecked) |
164 begin |
164 begin |
165 |
165 |
166 quotient_def |
166 quotient_def |
167 perm_kind :: "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" |
167 "perm_kind :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND" |
168 where |
168 as |
169 "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)" |
169 "(perm::'x prm \<Rightarrow> kind \<Rightarrow> kind)" |
170 |
170 |
171 quotient_def |
171 quotient_def |
172 perm_ty :: "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" |
172 "perm_ty :: 'x prm \<Rightarrow> TY \<Rightarrow> TY" |
173 where |
173 as |
174 "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)" |
174 "(perm::'x prm \<Rightarrow> ty \<Rightarrow> ty)" |
175 |
175 |
176 quotient_def |
176 quotient_def |
177 perm_trm :: "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
177 "perm_trm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
178 where |
178 as |
179 "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
179 "(perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
180 |
180 |
181 end |
181 end |
182 |
182 |
183 (* TODO/FIXME: Think whether these RSP theorems are true. *) |
183 (* TODO/FIXME: Think whether these RSP theorems are true. *) |