equal
deleted
inserted
replaced
871 |
871 |
872 lemma num1_eq1 [simp]: |
872 lemma num1_eq1 [simp]: |
873 fixes a::num1 shows "a = 1" |
873 fixes a::num1 shows "a = 1" |
874 by (rule num1_eqI) |
874 by (rule num1_eqI) |
875 |
875 |
876 instantiation num1 :: cart_one |
|
877 begin |
|
878 |
|
879 instance |
|
880 proof |
|
881 show "CARD(1) = Suc 0" by auto |
|
882 qed |
|
883 |
|
884 end |
|
885 |
|
886 instantiation num1 :: linorder begin |
876 instantiation num1 :: linorder begin |
887 definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b" |
877 definition "a < b \<longleftrightarrow> Rep_num1 a < Rep_num1 b" |
888 definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b" |
878 definition "a \<le> b \<longleftrightarrow> Rep_num1 a \<le> Rep_num1 b" |
889 instance |
879 instance |
890 by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI) |
880 by intro_classes (auto simp: less_eq_num1_def less_num1_def intro: num1_eqI) |