equal
deleted
inserted
replaced
164 axiomatization |
164 axiomatization |
165 RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" |
165 RR :: "trm \<Rightarrow> trm \<Rightarrow> bool" |
166 where |
166 where |
167 r_eq: "EQUIV RR" |
167 r_eq: "EQUIV RR" |
168 |
168 |
169 quotient qtrm = "trm" / "RR" |
169 quotient qtrm = trm / "RR" |
170 apply(rule r_eq) |
170 apply(rule r_eq) |
171 done |
171 done |
172 |
172 |
173 typ qtrm |
173 typ qtrm |
174 term Rep_qtrm |
174 term Rep_qtrm |
194 | lam' "'a" "'a trm'" |
194 | lam' "'a" "'a trm'" |
195 |
195 |
196 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool" |
196 consts R' :: "'a trm' \<Rightarrow> 'a trm' \<Rightarrow> bool" |
197 axioms r_eq': "EQUIV R'" |
197 axioms r_eq': "EQUIV R'" |
198 |
198 |
199 quotient "'a qtrm'" = "'a trm'" / "R'" |
199 quotient qtrm' = "'a trm'" / "R'" |
200 apply(rule r_eq') |
200 apply(rule r_eq') |
201 done |
201 done |
202 |
202 |
203 print_theorems |
203 print_theorems |
204 |
204 |
216 | lm "string" "t" |
216 | lm "string" "t" |
217 |
217 |
218 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool" |
218 consts Rt :: "t \<Rightarrow> t \<Rightarrow> bool" |
219 axioms t_eq: "EQUIV Rt" |
219 axioms t_eq: "EQUIV Rt" |
220 |
220 |
221 quotient "qt" = "t" / "Rt" |
221 quotient qt = "t" / "Rt" |
222 by (rule t_eq) |
222 by (rule t_eq) |
223 |
223 |
224 section {* lifting of constants *} |
224 section {* lifting of constants *} |
225 |
225 |
226 text {* information about map-functions for type-constructor *} |
226 text {* information about map-functions for type-constructor *} |
406 | lm' "'a" "string \<Rightarrow> ('a t')" |
406 | lm' "'a" "string \<Rightarrow> ('a t')" |
407 |
407 |
408 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool" |
408 consts Rt' :: "('a t') \<Rightarrow> ('a t') \<Rightarrow> bool" |
409 axioms t_eq': "EQUIV Rt'" |
409 axioms t_eq': "EQUIV Rt'" |
410 |
410 |
411 quotient "'a qt'" = "'a t'" / "Rt'" |
411 quotient qt' = "'a t'" / "Rt'" |
412 apply(rule t_eq') |
412 apply(rule t_eq') |
413 done |
413 done |
414 |
414 |
415 print_theorems |
415 print_theorems |
416 |
416 |
451 shows "EQUIV list_eq" |
451 shows "EQUIV list_eq" |
452 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
452 unfolding EQUIV_REFL_SYM_TRANS REFL_def SYM_def TRANS_def |
453 apply(auto intro: list_eq.intros list_eq_refl) |
453 apply(auto intro: list_eq.intros list_eq_refl) |
454 done |
454 done |
455 |
455 |
456 quotient "'a fset" = "'a list" / "list_eq" |
456 quotient fset = "'a list" / "list_eq" |
457 apply(rule equiv_list_eq) |
457 apply(rule equiv_list_eq) |
458 done |
458 done |
459 |
459 |
460 print_theorems |
460 print_theorems |
461 |
461 |