equal
deleted
inserted
replaced
17 quotient_def (for my_int) |
17 quotient_def (for my_int) |
18 ZERO::"my_int" |
18 ZERO::"my_int" |
19 where |
19 where |
20 "ZERO \<equiv> (0::nat, 0::nat)" |
20 "ZERO \<equiv> (0::nat, 0::nat)" |
21 |
21 |
22 thm ZERO_def |
|
23 |
22 |
24 quotient_def (for my_int) |
23 quotient_def (for my_int) |
25 ONE::"my_int" |
24 ONE::"my_int" |
26 where |
25 where |
27 "ONE \<equiv> (1::nat, 0::nat)" |
26 "ONE \<equiv> (1::nat, 0::nat)" |
39 where |
38 where |
40 "PLUS \<equiv> my_plus" |
39 "PLUS \<equiv> my_plus" |
41 |
40 |
42 term PLUS |
41 term PLUS |
43 thm PLUS_def |
42 thm PLUS_def |
|
43 |
|
44 definition |
|
45 "MPLUS x y \<equiv> my_plus x y" |
|
46 |
|
47 term MPLUS |
|
48 thm MPLUS_def |
|
49 thm MPLUS_def_raw |
|
50 |
44 |
51 |
45 fun |
52 fun |
46 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
53 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
47 where |
54 where |
48 "my_neg (x, y) = (y, x)" |
55 "my_neg (x, y) = (y, x)" |