equal
deleted
inserted
replaced
26 (\<forall>x. Abs (Rep x) = x) \<and> |
26 (\<forall>x. Abs (Rep x) = x) \<and> |
27 (\<forall>y \<in> A. Rep (Abs y) = y)" |
27 (\<forall>y \<in> A. Rep (Abs y) = y)" |
28 -- {* This will be stated as an axiom for each typedef! *} |
28 -- {* This will be stated as an axiom for each typedef! *} |
29 |
29 |
30 lemma type_definitionI [intro]: |
30 lemma type_definitionI [intro]: |
31 "(\<And>x. Rep x \<in> A) \<Longrightarrow> |
31 "(!!x. Rep x \<in> A) ==> |
32 (\<And>x. Abs (Rep x) = x) \<Longrightarrow> |
32 (!!x. Abs (Rep x) = x) ==> |
33 (\<And>y. y \<in> A \<Longrightarrow> Rep (Abs y) = y) \<Longrightarrow> |
33 (!!y. y \<in> A ==> Rep (Abs y) = y) ==> |
34 type_definition Rep Abs A" |
34 type_definition Rep Abs A" |
35 by (unfold type_definition_def) blast |
35 by (unfold type_definition_def) blast |
36 |
36 |
37 theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A" |
37 theorem Rep: "type_definition Rep Abs A ==> Rep x \<in> A" |
38 by (unfold type_definition_def) blast |
38 by (unfold type_definition_def) blast |