equal
deleted
inserted
replaced
43 fun |
43 fun |
44 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
44 my_neg :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
45 where |
45 where |
46 "my_neg (x, y) = (y, x)" |
46 "my_neg (x, y) = (y, x)" |
47 |
47 |
48 local_setup {* |
48 quotient_def (for my_int) |
49 old_make_const_def @{binding NEG} @{term "my_neg"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
49 NEG::"my_int \<Rightarrow> my_int" |
50 *} |
50 where |
|
51 "NEG \<equiv> my_neg" |
51 |
52 |
52 term NEG |
53 term NEG |
53 thm NEG_def |
54 thm NEG_def |
54 |
55 |
55 definition |
56 definition |
60 fun |
61 fun |
61 my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
62 my_mult :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
62 where |
63 where |
63 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
64 "my_mult (x, y) (u, v) = (x*u + y*v, x*v + y*u)" |
64 |
65 |
65 local_setup {* |
66 quotient_def (for my_int) |
66 old_make_const_def @{binding MULT} @{term "my_mult"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
67 MULT::"my_int \<Rightarrow> my_int \<Rightarrow> my_int" |
67 *} |
68 where |
|
69 "MULT \<equiv> my_mult" |
68 |
70 |
69 term MULT |
71 term MULT |
70 thm MULT_def |
72 thm MULT_def |
71 |
73 |
72 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *) |
74 (* NOT SURE WETHER THIS DEFINITION IS CORRECT *) |
73 fun |
75 fun |
74 my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
76 my_le :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
75 where |
77 where |
76 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
78 "my_le (x, y) (u, v) = (x+v \<le> u+y)" |
77 |
79 |
78 local_setup {* |
80 quotient_def (for my_int) |
79 old_make_const_def @{binding LE} @{term "my_le"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd |
81 LE :: "my_int \<Rightarrow> my_int \<Rightarrow> bool" |
80 *} |
82 where |
|
83 "LE \<equiv> my_le" |
81 |
84 |
82 term LE |
85 term LE |
83 thm LE_def |
86 thm LE_def |
84 |
87 |
85 definition |
88 definition |
87 where |
90 where |
88 "LESS z w = (LE z w \<and> z \<noteq> w)" |
91 "LESS z w = (LE z w \<and> z \<noteq> w)" |
89 |
92 |
90 term LESS |
93 term LESS |
91 thm LESS_def |
94 thm LESS_def |
92 |
|
93 |
95 |
94 definition |
96 definition |
95 ABS :: "my_int \<Rightarrow> my_int" |
97 ABS :: "my_int \<Rightarrow> my_int" |
96 where |
98 where |
97 "ABS i = (if (LESS i ZERO) then (NEG i) else i)" |
99 "ABS i = (if (LESS i ZERO) then (NEG i) else i)" |
146 done |
148 done |
147 |
149 |
148 ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *} |
150 ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *} |
149 |
151 |
150 |
152 |
151 |
|
152 |
|
153 |
|
154 |
|
155 |
|
156 |
|
157 text {* Below is the construction site code used if things do now work *} |
153 text {* Below is the construction site code used if things do now work *} |
158 |
154 |
159 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
155 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
160 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
156 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
161 |
157 |