19 thm my_int_equivp |
19 thm my_int_equivp |
20 |
20 |
21 print_theorems |
21 print_theorems |
22 print_quotients |
22 print_quotients |
23 |
23 |
24 quotient_def |
24 quotient_def |
25 ZERO::"my_int" |
25 ZERO::"zero :: my_int" |
26 where |
26 where |
27 "ZERO \<equiv> (0::nat, 0::nat)" |
27 "(0::nat, 0::nat)" |
28 |
28 |
29 ML {* print_qconstinfo @{context} *} |
29 quotient_def |
30 |
30 ONE::"one :: my_int" |
31 term ZERO |
31 where |
32 thm ZERO_def |
32 "(1::nat, 0::nat)" |
33 |
|
34 ML {* prop_of @{thm ZERO_def} *} |
|
35 |
|
36 ML {* separate *} |
|
37 |
|
38 quotient_def |
|
39 ONE::"my_int" |
|
40 where |
|
41 "ONE \<equiv> (1::nat, 0::nat)" |
|
42 |
|
43 ML {* print_qconstinfo @{context} *} |
|
44 |
|
45 term ONE |
|
46 thm ONE_def |
|
47 |
33 |
48 fun |
34 fun |
49 my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
35 my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
50 where |
36 where |
51 "my_plus (x, y) (u, v) = (x + u, y + v)" |
37 "my_plus (x, y) (u, v) = (x + u, y + v)" |
52 |
38 |
53 quotient_def |
39 quotient_def |
54 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
40 PLUS::"PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
55 where |
41 where |
56 "PLUS \<equiv> my_plus" |
42 "my_plus" |
57 |
|
58 term my_plus |
|
59 term PLUS |
|
60 thm PLUS_def |
|
61 |
43 |
62 fun |
44 fun |
63 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
45 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
64 where |
46 where |
65 "my_neg (x, y) = (y, x)" |
47 "my_neg (x, y) = (y, x)" |
66 |
48 |
67 quotient_def |
49 quotient_def |
68 NEG::"my_int \<Rightarrow> my_int" |
50 NEG::"NEG :: my_int \<Rightarrow> my_int" |
69 where |
51 where |
70 "NEG \<equiv> my_neg" |
52 "my_neg" |
71 |
|
72 term NEG |
|
73 thm NEG_def |
|
74 |
53 |
75 definition |
54 definition |
76 MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
55 MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
77 where |
56 where |
78 "MINUS z w = PLUS z (NEG w)" |
57 "MINUS z w = PLUS z (NEG w)" |
80 fun |
59 fun |
81 my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
60 my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
82 where |
61 where |
83 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
62 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
84 |
63 |
85 quotient_def |
64 quotient_def |
86 MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
65 MULT::"MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
87 where |
66 where |
88 "MULT \<equiv> my_mult" |
67 "my_mult" |
89 |
68 |
90 term MULT |
|
91 thm MULT_def |
|
92 |
69 |
93 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *) |
70 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *) |
94 fun |
71 fun |
95 my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
72 my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
96 where |
73 where |
97 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
74 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
98 |
75 |
99 quotient_def |
76 quotient_def |
100 LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool" |
77 LE :: "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool" |
101 where |
78 where |
102 "LE \<equiv> my_le" |
79 "my_le" |
103 |
80 |
104 term LE |
81 term LE |
105 thm LE_def |
82 thm LE_def |
106 |
83 |
107 |
84 |