equal
deleted
inserted
replaced
11 ("Tools/Domain/domain_take_proofs.ML") |
11 ("Tools/Domain/domain_take_proofs.ML") |
12 ("Tools/Domain/domain_isomorphism.ML") |
12 ("Tools/Domain/domain_isomorphism.ML") |
13 begin |
13 begin |
14 |
14 |
15 subsection {* Preliminaries: Take proofs *} |
15 subsection {* Preliminaries: Take proofs *} |
|
16 |
|
17 text {* |
|
18 This section contains lemmas that are used in a module that supports |
|
19 the domain isomorphism package; the module contains proofs related |
|
20 to take functions and the finiteness predicate. |
|
21 *} |
16 |
22 |
17 lemma deflation_abs_rep: |
23 lemma deflation_abs_rep: |
18 fixes abs and rep and d |
24 fixes abs and rep and d |
19 assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x" |
25 assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x" |
20 assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y" |
26 assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y" |