equal
deleted
inserted
replaced
12 apply(auto simp add: mem_def expand_fun_eq) |
12 apply(auto simp add: mem_def expand_fun_eq) |
13 done |
13 done |
14 |
14 |
15 print_theorems |
15 print_theorems |
16 |
16 |
17 quotient_def (for my_int) |
17 quotient_def |
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 term ZERO |
|
23 thm ZERO_def |
22 |
24 |
23 quotient_def (for my_int) |
25 quotient_def |
24 ONE::"my_int" |
26 ONE::"my_int" |
25 where |
27 where |
26 "ONE \<equiv> (1::nat, 0::nat)" |
28 "ONE \<equiv> (1::nat, 0::nat)" |
27 |
29 |
28 term ONE |
30 term ONE |
31 fun |
33 fun |
32 my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
34 my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
33 where |
35 where |
34 "my_plus (x, y) (u, v) = (x + u, y + v)" |
36 "my_plus (x, y) (u, v) = (x + u, y + v)" |
35 |
37 |
36 quotient_def (for my_int) |
38 quotient_def |
37 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
39 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
38 where |
40 where |
39 "PLUS \<equiv> my_plus" |
41 "PLUS \<equiv> my_plus" |
40 |
42 |
41 term PLUS |
43 term PLUS |
46 |
48 |
47 term MPLUS |
49 term MPLUS |
48 thm MPLUS_def |
50 thm MPLUS_def |
49 thm MPLUS_def_raw |
51 thm MPLUS_def_raw |
50 |
52 |
51 |
|
52 fun |
53 fun |
53 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
54 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
54 where |
55 where |
55 "my_neg (x, y) = (y, x)" |
56 "my_neg (x, y) = (y, x)" |
56 |
57 |
57 quotient_def (for my_int) |
58 quotient_def |
58 NEG::"my_int \<Rightarrow> my_int" |
59 NEG::"my_int \<Rightarrow> my_int" |
59 where |
60 where |
60 "NEG \<equiv> my_neg" |
61 "NEG \<equiv> my_neg" |
61 |
62 |
62 term NEG |
63 term NEG |
70 fun |
71 fun |
71 my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
72 my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
72 where |
73 where |
73 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
74 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
74 |
75 |
75 quotient_def (for my_int) |
76 quotient_def |
76 MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
77 MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
77 where |
78 where |
78 "MULT \<equiv> my_mult" |
79 "MULT \<equiv> my_mult" |
79 |
80 |
80 term MULT |
81 term MULT |
84 fun |
85 fun |
85 my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
86 my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
86 where |
87 where |
87 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
88 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
88 |
89 |
89 quotient_def (for my_int) |
90 quotient_def |
90 LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool" |
91 LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool" |
91 where |
92 where |
92 "LE \<equiv> my_le" |
93 "LE \<equiv> my_le" |
93 |
94 |
94 term LE |
95 term LE |