equal
deleted
inserted
replaced
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_definition |
25 "ZERO :: my_int" |
25 "ZERO :: my_int" |
26 as |
26 as |
27 "(0::nat, 0::nat)" |
27 "(0::nat, 0::nat)" |
28 |
28 |
29 quotient_def |
29 quotient_definition |
30 "ONE :: my_int" |
30 "ONE :: my_int" |
31 as |
31 as |
32 "(1::nat, 0::nat)" |
32 "(1::nat, 0::nat)" |
33 |
33 |
34 fun |
34 fun |
35 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)" |
36 where |
36 where |
37 "my_plus (x, y) (u, v) = (x + u, y + v)" |
37 "my_plus (x, y) (u, v) = (x + u, y + v)" |
38 |
38 |
39 quotient_def |
39 quotient_definition |
40 "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
40 "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
41 as |
41 as |
42 "my_plus" |
42 "my_plus" |
43 |
43 |
44 fun |
44 fun |
45 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
45 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
46 where |
46 where |
47 "my_neg (x, y) = (y, x)" |
47 "my_neg (x, y) = (y, x)" |
48 |
48 |
49 quotient_def |
49 quotient_definition |
50 "NEG :: my_int \<Rightarrow> my_int" |
50 "NEG :: my_int \<Rightarrow> my_int" |
51 as |
51 as |
52 "my_neg" |
52 "my_neg" |
53 |
53 |
54 definition |
54 definition |
59 fun |
59 fun |
60 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)" |
61 where |
61 where |
62 "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)" |
63 |
63 |
64 quotient_def |
64 quotient_definition |
65 "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
65 "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
66 as |
66 as |
67 "my_mult" |
67 "my_mult" |
68 |
68 |
69 |
69 |
71 fun |
71 fun |
72 my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
72 my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
73 where |
73 where |
74 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
74 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
75 |
75 |
76 quotient_def |
76 quotient_definition |
77 "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool" |
77 "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool" |
78 as |
78 as |
79 "my_le" |
79 "my_le" |
80 |
80 |
81 term LE |
81 term LE |