10 quotient my_int = "nat \<times> nat" / intrel |
10 quotient my_int = "nat \<times> nat" / intrel |
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_quotients |
15 quotient_def (for my_int) |
|
16 ZERO::"my_int" |
|
17 where |
|
18 "ZERO \<equiv> (0::nat, 0::nat)" |
16 |
19 |
17 typ my_int |
|
18 |
|
19 local_setup {* |
|
20 make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
|
21 *} |
|
22 |
|
23 term ZERO |
|
24 thm ZERO_def |
20 thm ZERO_def |
25 |
21 |
26 (* |
22 quotient_def (for my_int) |
27 quotient_def (with my_int) |
23 ONE::"my_int" |
28 ZERO :: "my_int" |
|
29 where |
24 where |
30 "ZERO \<equiv> (0::nat, 0::nat)" |
25 "ONE \<equiv> (1::nat, 0::nat)" |
31 *) |
|
32 |
|
33 local_setup {* |
|
34 make_const_def @{binding ONE} @{term "(1::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
|
35 *} |
|
36 |
26 |
37 term ONE |
27 term ONE |
38 thm ONE_def |
28 thm ONE_def |
39 |
29 |
40 fun |
30 fun |
41 my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
31 my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
42 where |
32 where |
43 "my_plus (x, y) (u, v) = (x + u, y + v)" |
33 "my_plus (x, y) (u, v) = (x + u, y + v)" |
44 |
34 |
45 local_setup {* |
35 quotient_def (for my_int) |
46 make_const_def @{binding PLUS} @{term "my_plus"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
36 PLUS::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
47 *} |
37 where |
|
38 "PLUS \<equiv> my_plus" |
48 |
39 |
49 term PLUS |
40 term PLUS |
50 thm PLUS_def |
41 thm PLUS_def |
51 |
42 |
52 fun |
43 fun |
53 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
44 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
54 where |
45 where |
55 "my_neg (x, y) = (y, x)" |
46 "my_neg (x, y) = (y, x)" |
56 |
47 |
57 local_setup {* |
48 local_setup {* |
58 make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
49 old_make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
59 *} |
50 *} |
60 |
51 |
61 term NEG |
52 term NEG |
62 thm NEG_def |
53 thm NEG_def |
63 |
54 |
70 my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
61 my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
71 where |
62 where |
72 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
63 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
73 |
64 |
74 local_setup {* |
65 local_setup {* |
75 make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
66 old_make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
76 *} |
67 *} |
77 |
68 |
78 term MULT |
69 term MULT |
79 thm MULT_def |
70 thm MULT_def |
80 |
71 |