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