equal
deleted
inserted
replaced
11 apply(unfold EQUIV_def) |
11 apply(unfold EQUIV_def) |
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 print_quotients |
16 |
17 |
17 quotient_def |
18 quotient_def |
18 ZERO::"my_int" |
19 ZERO::"my_int" |
19 where |
20 where |
20 "ZERO \<equiv> (0::nat, 0::nat)" |
21 "ZERO \<equiv> (0::nat, 0::nat)" |
36 "my_plus (x, y) (u, v) = (x + u, y + v)" |
37 "my_plus (x, y) (u, v) = (x + u, y + v)" |
37 |
38 |
38 quotient_def |
39 quotient_def |
39 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
40 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
40 where |
41 where |
41 "PLUS \<equiv> my_plus" |
42 "PLUS x y \<equiv> my_plus x y" |
42 |
43 |
43 term PLUS |
44 term PLUS |
44 thm PLUS_def |
45 thm PLUS_def |
45 |
|
46 definition |
|
47 "MPLUS x y \<equiv> my_plus x y" |
|
48 |
|
49 term MPLUS |
|
50 thm MPLUS_def |
|
51 thm MPLUS_def_raw |
|
52 |
46 |
53 fun |
47 fun |
54 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
48 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
55 where |
49 where |
56 "my_neg (x, y) = (y, x)" |
50 "my_neg (x, y) = (y, x)" |