161 prove {* reg_artm *} |
161 prove {* reg_artm *} |
162 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
162 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
163 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) |
163 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) |
164 done |
164 done |
165 |
165 |
166 (* |
166 ML {* |
167 ML {* |
167 fun mk_repabs lthy (T, T') trm = |
168 fun inj_REPABS lthy rtrm qtrm = |
168 Quotient_Def.get_fun repF lthy (T, T') |
|
169 $ (Quotient_Def.get_fun absF lthy (T, T') $ trm) |
|
170 *} |
|
171 |
|
172 ML {* |
|
173 fun replace_bnd0 (trm, Abs (x, T, t)) = |
|
174 Abs (x, T, subst_bound (trm, t)) |
|
175 *} |
|
176 |
|
177 ML {* |
|
178 fun inj_REPABS_aux lthy (rtrm, qtrm) = |
|
179 let |
|
180 val rty = fastype_of rtrm |
|
181 val qty = fastype_of qtrm |
|
182 in |
169 case (rtrm, qtrm) of |
183 case (rtrm, qtrm) of |
170 (Abs (x, T, t), Abs (x', T', t')) => |
184 (Abs (x, T, t), Abs (x', T', t')) => |
171 if T = T' |
185 let |
172 then Abs (x, T, inj_REPABS lthy t t') |
186 val (y, s) = Term.dest_abs (x, T, t) |
173 else |
187 val (y', s') = Term.dest_abs (x', T', t') |
174 let |
188 val yvar = Free (y, T) |
175 |
189 val res = lambda yvar (inj_REPABS_aux lthy (s, s')) |
176 in |
190 in |
177 |
191 if T = T' |
178 end |
192 then res |
|
193 else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res)) |
|
194 end |
|
195 (* FIXME: Does one havae to look at the abstraction or go under the lambda. *) |
|
196 | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') => |
|
197 Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS_aux lthy (t, t')) |
|
198 | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') => |
|
199 Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS_aux lthy (t, t')) |
|
200 | (rtrm as _ $ _, qtrm as _ $ _) => |
|
201 let |
|
202 val (rhead, rargs) = Term.strip_comb rtrm |
|
203 val (qhead, qargs) = Term.strip_comb qtrm |
|
204 val rhead' = inj_REPABS_aux lthy (rhead, qhead) |
|
205 val rargs' = map (inj_REPABS_aux lthy) (rargs ~~ qargs) |
|
206 val res = list_comb (rhead', rargs') |
|
207 in |
|
208 if rty = qty |
|
209 then res |
|
210 else mk_repabs lthy (rty, qty) res |
|
211 end |
|
212 (* FIXME: cases for frees and vars *) |
179 | _ => rtrm |
213 | _ => rtrm |
180 *} |
214 end |
181 *) |
215 *} |
|
216 |
|
217 |
|
218 ML {* |
|
219 fun inj_REPABS lthy (rtrm, qtrm) = |
|
220 inj_REPABS_aux lthy (rtrm, qtrm) |
|
221 |> Syntax.check_term lthy |
|
222 *} |
182 |
223 |
183 lemma plus_assoc_pre: |
224 lemma plus_assoc_pre: |
184 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
225 shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)" |
185 apply (cases i) |
226 apply (cases i) |
186 apply (cases j) |
227 apply (cases j) |
189 done |
230 done |
190 |
231 |
191 ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *} |
232 ML {* val test2 = lift_thm_my_int @{context} @{thm plus_assoc_pre} *} |
192 |
233 |
193 ML {* |
234 ML {* |
194 val aqtrm = (prop_of (atomize_thm test2)) |
235 val arthm = atomize_thm @{thm plus_assoc_pre} |
195 val artrm = (prop_of (atomize_thm @{thm plus_assoc_pre})) |
236 val aqthm = atomize_thm test2 |
196 *} |
237 |
197 |
238 val aqtrm = prop_of aqthm |
198 prove {* mk_REGULARIZE_goal @{context} artrm aqtrm *} |
239 val artrm = prop_of arthm |
|
240 *} |
|
241 |
|
242 prove testtest: {* mk_REGULARIZE_goal @{context} artrm aqtrm *} |
199 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
243 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
200 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) |
244 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *}) |
201 done |
245 done |
|
246 |
|
247 ML {* @{thm testtest} OF [arthm] *} |
|
248 |
|
249 ML {* |
|
250 val reg_atrm = prop_of (@{thm testtest} OF [arthm]); |
|
251 *} |
|
252 |
|
253 ML {* |
|
254 inj_REPABS @{context} (reg_atrm, aqtrm) |
|
255 |> Syntax.string_of_term @{context} |
|
256 |> writeln |
|
257 *} |
|
258 |
202 |
259 |
203 |
260 |
204 |
261 |
205 |
262 |
206 |
263 |