equal
deleted
inserted
replaced
565 |
565 |
566 constdefs |
566 constdefs |
567 Nats :: "'a::comm_semiring_1_cancel set" |
567 Nats :: "'a::comm_semiring_1_cancel set" |
568 "Nats == range of_nat" |
568 "Nats == range of_nat" |
569 |
569 |
570 abbreviation (xsymbols) |
570 const_syntax (xsymbols) |
571 Nats1 ("\<nat>") |
571 Nats ("\<nat>") |
572 "\<nat> == Nats" |
|
573 |
572 |
574 lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats" |
573 lemma of_nat_in_Nats [simp]: "of_nat n \<in> Nats" |
575 by (simp add: Nats_def) |
574 by (simp add: Nats_def) |
576 |
575 |
577 lemma Nats_0 [simp]: "0 \<in> Nats" |
576 lemma Nats_0 [simp]: "0 \<in> Nats" |
699 |
698 |
700 constdefs |
699 constdefs |
701 Ints :: "'a::comm_ring_1 set" |
700 Ints :: "'a::comm_ring_1 set" |
702 "Ints == range of_int" |
701 "Ints == range of_int" |
703 |
702 |
704 abbreviation (xsymbols) |
703 const_syntax (xsymbols) |
705 Ints1 ("\<int>") |
704 Ints ("\<int>") |
706 "\<int> == Ints" |
|
707 |
705 |
708 lemma Ints_0 [simp]: "0 \<in> Ints" |
706 lemma Ints_0 [simp]: "0 \<in> Ints" |
709 apply (simp add: Ints_def) |
707 apply (simp add: Ints_def) |
710 apply (rule range_eqI) |
708 apply (rule range_eqI) |
711 apply (rule of_int_0 [symmetric]) |
709 apply (rule of_int_0 [symmetric]) |