equal
deleted
inserted
replaced
12 fixes Rep and Abs and A |
12 fixes Rep and Abs and A |
13 assumes Rep: "Rep x \<in> A" |
13 assumes Rep: "Rep x \<in> A" |
14 and Rep_inverse: "Abs (Rep x) = x" |
14 and Rep_inverse: "Abs (Rep x) = x" |
15 and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y" |
15 and Abs_inverse: "y \<in> A ==> Rep (Abs y) = y" |
16 -- {* This will be axiomatized for each typedef! *} |
16 -- {* This will be axiomatized for each typedef! *} |
17 |
|
18 lemmas type_definitionI [intro] = |
|
19 type_definition.intro [OF type_definition_axioms.intro] |
|
20 |
17 |
21 lemma (in type_definition) Rep_inject: |
18 lemma (in type_definition) Rep_inject: |
22 "(Rep x = Rep y) = (x = y)" |
19 "(Rep x = Rep y) = (x = y)" |
23 proof |
20 proof |
24 assume "Rep x = Rep y" |
21 assume "Rep x = Rep y" |