equal
deleted
inserted
replaced
13 apply(auto simp add: mem_def expand_fun_eq) |
13 apply(auto simp add: mem_def expand_fun_eq) |
14 done |
14 done |
15 |
15 |
16 quotient_definition |
16 quotient_definition |
17 "ZERO :: my_int" |
17 "ZERO :: my_int" |
18 as |
18 is |
19 "(0::nat, 0::nat)" |
19 "(0::nat, 0::nat)" |
20 |
20 |
21 quotient_definition |
21 quotient_definition |
22 "ONE :: my_int" |
22 "ONE :: my_int" |
23 as |
23 is |
24 "(1::nat, 0::nat)" |
24 "(1::nat, 0::nat)" |
25 |
25 |
26 fun |
26 fun |
27 my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
27 my_plus :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
28 where |
28 where |
29 "my_plus (x, y) (u, v) = (x + u, y + v)" |
29 "my_plus (x, y) (u, v) = (x + u, y + v)" |
30 |
30 |
31 quotient_definition |
31 quotient_definition |
32 "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
32 "PLUS :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
33 as |
33 is |
34 "my_plus" |
34 "my_plus" |
35 |
35 |
36 fun |
36 fun |
37 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
37 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
38 where |
38 where |
39 "my_neg (x, y) = (y, x)" |
39 "my_neg (x, y) = (y, x)" |
40 |
40 |
41 quotient_definition |
41 quotient_definition |
42 "NEG :: my_int \<Rightarrow> my_int" |
42 "NEG :: my_int \<Rightarrow> my_int" |
43 as |
43 is |
44 "my_neg" |
44 "my_neg" |
45 |
45 |
46 definition |
46 definition |
47 MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
47 MINUS :: "my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
48 where |
48 where |
53 where |
53 where |
54 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
54 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
55 |
55 |
56 quotient_definition |
56 quotient_definition |
57 "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
57 "MULT :: my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
58 as |
58 is |
59 "my_mult" |
59 "my_mult" |
60 |
60 |
61 |
61 |
62 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *) |
62 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *) |
63 fun |
63 fun |
65 where |
65 where |
66 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
66 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
67 |
67 |
68 quotient_definition |
68 quotient_definition |
69 "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool" |
69 "LE :: my_int \<Rightarrow> my_int \<Rightarrow> bool" |
70 as |
70 is |
71 "my_le" |
71 "my_le" |
72 |
72 |
73 term LE |
73 term LE |
74 thm LE_def |
74 thm LE_def |
75 |
75 |