equal
deleted
inserted
replaced
98 end |
98 end |
99 |
99 |
100 lemma identity_quotient: "Quotient (op =) id id (op =)" |
100 lemma identity_quotient: "Quotient (op =) id id (op =)" |
101 unfolding Quotient_def by simp |
101 unfolding Quotient_def by simp |
102 |
102 |
|
103 lemma reflp_equality: "reflp (op =)" |
|
104 by (auto intro: reflpI) |
|
105 |
103 text {* TODO: Use one of these alternatives as the real definition. *} |
106 text {* TODO: Use one of these alternatives as the real definition. *} |
104 |
107 |
105 lemma Quotient_alt_def: |
108 lemma Quotient_alt_def: |
106 "Quotient R Abs Rep T \<longleftrightarrow> |
109 "Quotient R Abs Rep T \<longleftrightarrow> |
107 (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> |
110 (\<forall>a b. T a b \<longrightarrow> Abs a = b) \<and> |
362 |
365 |
363 use "Tools/Lifting/lifting_info.ML" |
366 use "Tools/Lifting/lifting_info.ML" |
364 setup Lifting_Info.setup |
367 setup Lifting_Info.setup |
365 |
368 |
366 declare fun_quotient[quot_map] |
369 declare fun_quotient[quot_map] |
|
370 declare reflp_equality[reflp_preserve] |
367 |
371 |
368 use "Tools/Lifting/lifting_term.ML" |
372 use "Tools/Lifting/lifting_term.ML" |
369 |
373 |
370 use "Tools/Lifting/lifting_def.ML" |
374 use "Tools/Lifting/lifting_def.ML" |
371 |
375 |