6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
7 where |
7 where |
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
9 |
9 |
10 quotient my_int = "nat \<times> nat" / intrel |
10 quotient my_int = "nat \<times> nat" / intrel |
|
11 and my_int' = "nat \<times> nat" / intrel |
11 apply(unfold EQUIV_def) |
12 apply(unfold EQUIV_def) |
12 apply(auto simp add: mem_def expand_fun_eq) |
13 apply(auto simp add: mem_def expand_fun_eq) |
13 done |
14 done |
14 |
15 |
|
16 thm my_int_equiv |
|
17 |
15 print_theorems |
18 print_theorems |
16 print_quotients |
19 print_quotients |
17 |
20 |
18 quotient_def |
21 quotient_def |
19 ZERO::"my_int" |
22 ZERO::"my_int" |
147 |
151 |
148 ML {* |
152 ML {* |
149 val test = lift_thm_my_int @{context} @{thm plus_sym_pre} |
153 val test = lift_thm_my_int @{context} @{thm plus_sym_pre} |
150 *} |
154 *} |
151 |
155 |
152 |
156 ML {* |
153 ML {* |
157 val aqtrm = (prop_of (atomize_thm test)) |
154 val aqtrm = HOLogic.dest_Trueprop (prop_of (atomize_thm test)) |
158 val artrm = (prop_of (atomize_thm @{thm plus_sym_pre})) |
155 val artrm = HOLogic.dest_Trueprop (prop_of (atomize_thm @{thm plus_sym_pre})) |
159 val reg_artm = mk_REGULARIZE_goal @{context} artrm aqtrm |
156 *} |
160 *} |
157 |
161 |
|
162 prove {* reg_artm *} |
|
163 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
164 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) |
|
165 done |
|
166 |
|
167 (* |
|
168 ML {* |
|
169 fun inj_REPABS lthy rtrm qtrm = |
|
170 case (rtrm, qtrm) of |
|
171 (Abs (x, T, t), Abs (x', T', t')) => |
|
172 if T = T' |
|
173 then Abs (x, T, inj_REPABS lthy t t') |
|
174 else |
|
175 let |
|
176 |
|
177 in |
|
178 |
|
179 end |
|
180 | _ => rtrm |
|
181 *} |
|
182 *) |
158 |
183 |
159 lemma plus_assoc_pre: |
184 lemma plus_assoc_pre: |
160 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
185 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
161 apply (cases i) |
186 apply (cases i) |
162 apply (cases j) |
187 apply (cases j) |
163 apply (cases k) |
188 apply (cases k) |
164 apply (simp) |
189 apply (simp) |
165 done |
190 done |
166 |
191 |
167 ML {* lift_thm_my_int @{context} @{thm plus_assoc_pre} *} |
192 ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *} |
168 |
193 |
|
194 ML {* |
|
195 val aqtrm = (prop_of (atomize_thm test2)) |
|
196 val artrm = (prop_of (atomize_thm @{thm plus_assoc_pre})) |
|
197 *} |
|
198 |
|
199 prove {* mk_REGULARIZE_goal @{context} artrm aqtrm *} |
|
200 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
201 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) |
|
202 done |
169 |
203 |
170 |
204 |
171 |
205 |
172 |
206 |
173 |
207 |