equal
deleted
inserted
replaced
621 qed |
621 qed |
622 |
622 |
623 |
623 |
624 subsection {* Embedding integers *} |
624 subsection {* Embedding integers *} |
625 |
625 |
626 constdefs (* FIXME generalize int to any numeric subtype *) |
626 constdefs |
627 rat :: "int => rat" |
627 rat :: "int => rat" (* FIXME generalize int to any numeric subtype *) |
628 "rat z == Fract z #1" |
628 "rat z == Fract z #1" |
629 int_set :: "rat set" ("\<int>") |
629 int_set :: "rat set" ("\<int>") (* FIXME generalize rat to any numeric supertype *) |
630 "\<int> == range rat" |
630 "\<int> == range rat" |
631 |
631 |
632 lemma rat_inject: "(rat z = rat w) = (z = w)" |
632 lemma rat_inject: "(rat z = rat w) = (z = w)" |
633 proof |
633 proof |
634 assume "rat z = rat w" |
634 assume "rat z = rat w" |