142 (* the auxiliary data for the quotient types *) |
142 (* the auxiliary data for the quotient types *) |
143 use "quotient_info.ML" |
143 use "quotient_info.ML" |
144 |
144 |
145 declare [[map "fun" = (fun_map, fun_rel)]] |
145 declare [[map "fun" = (fun_map, fun_rel)]] |
146 |
146 |
147 (* Throws now an exception: *) |
|
148 (* declare [[map "option" = (bla, blu)]] *) |
|
149 |
|
150 lemmas [quot_thm] = fun_quotient |
147 lemmas [quot_thm] = fun_quotient |
151 |
148 |
152 lemmas [quot_respect] = quot_rel_rsp |
149 lemmas [quot_respect] = quot_rel_rsp |
153 |
150 |
154 (* fun_map is not here since equivp is not true *) |
151 (* fun_map is not here since equivp is not true *) |
249 *} |
246 *} |
250 |
247 |
251 section {* Matching of Terms and Types *} |
248 section {* Matching of Terms and Types *} |
252 |
249 |
253 ML {* |
250 ML {* |
254 fun matches_typ (ty, ty') = |
251 fun struct_match_typ (ty, ty') = |
255 case (ty, ty') of |
252 case (ty, ty') of |
256 (_, TVar _) => true |
253 (_, TVar _) => true |
257 | (TFree x, TFree x') => x = x' |
254 | (TFree x, TFree x') => x = x' |
258 | (Type (s, tys), Type (s', tys')) => |
255 | (Type (s, tys), Type (s', tys')) => |
259 s = s' andalso |
256 s = s' andalso |
260 if (length tys = length tys') |
257 if (length tys = length tys') |
261 then (List.all matches_typ (tys ~~ tys')) |
258 then (List.all struct_match_typ (tys ~~ tys')) |
262 else false |
259 else false |
263 | _ => false |
260 | _ => false |
264 |
261 |
265 fun matches_term (trm, trm') = |
262 fun struct_match_term (trm, trm') = |
266 case (trm, trm') of |
263 case (trm, trm') of |
267 (_, Var _) => true |
264 (_, Var _) => true |
268 | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty') |
265 | (Const (s, ty), Const (s', ty')) => s = s' andalso struct_match_typ (ty, ty') |
269 | (Free (x, ty), Free (x', ty')) => x = x' andalso matches_typ (ty, ty') |
266 | (Free (x, ty), Free (x', ty')) => x = x' andalso struct_match_typ (ty, ty') |
270 | (Bound i, Bound j) => i = j |
267 | (Bound i, Bound j) => i = j |
271 | (Abs (_, T, t), Abs (_, T', t')) => matches_typ (T, T') andalso matches_term (t, t') |
268 | (Abs (_, T, t), Abs (_, T', t')) => struct_match_typ (T, T') andalso struct_match_term (t, t') |
272 | (t $ s, t' $ s') => matches_term (t, t') andalso matches_term (s, s') |
269 | (t $ s, t' $ s') => struct_match_term (t, t') andalso struct_match_term (s, s') |
273 | _ => false |
270 | _ => false |
274 *} |
271 *} |
275 |
272 |
276 section {* Computation of the Regularize Goal *} |
273 section {* Computation of the Regularize Goal *} |
277 |
274 |
410 val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)") |
407 val exc1 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") not found)") |
411 val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)") |
408 val exc2 = LIFT_MATCH ("regularize (constant " ^ s ^ "(" ^ st ^ ") mismatch)") |
412 val thy = ProofContext.theory_of lthy |
409 val thy = ProofContext.theory_of lthy |
413 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
410 val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1 |
414 in |
411 in |
415 if matches_term (rtrm, rtrm') then rtrm else |
412 if struct_match_term (rtrm, rtrm') then rtrm else |
416 let |
413 let |
417 val _ = tracing (Syntax.string_of_term @{context} rtrm); |
414 val _ = tracing (Syntax.string_of_term @{context} rtrm); |
418 val _ = tracing (Syntax.string_of_term @{context} rtrm'); |
415 val _ = tracing (Syntax.string_of_term @{context} rtrm'); |
419 in raise exc2 end |
416 in raise exc2 end |
420 end |
417 end |
502 *} |
499 *} |
503 |
500 |
504 lemma eq_imp_rel: |
501 lemma eq_imp_rel: |
505 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
502 shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
506 by (simp add: equivp_reflp) |
503 by (simp add: equivp_reflp) |
507 |
|
508 |
504 |
509 (* Regularize Tactic *) |
505 (* Regularize Tactic *) |
510 |
506 |
511 (* 0. preliminary simplification step according to *) |
507 (* 0. preliminary simplification step according to *) |
512 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *) |
508 thm ball_reg_eqv bex_reg_eqv babs_reg_eqv (* the latter of no use *) |
1183 THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), |
1179 THEN' RANGE_WARN [(regularize_tac ctxt, "Regularize proof failed."), |
1184 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1180 (all_inj_repabs_tac ctxt, "Injection proof failed."), |
1185 (clean_tac ctxt, "Cleaning proof failed.")] |
1181 (clean_tac ctxt, "Cleaning proof failed.")] |
1186 *} |
1182 *} |
1187 |
1183 |
1188 (* methods / interface *) |
1184 section {* methods / interface *} |
1189 ML {* |
1185 ML {* |
1190 (* FIXME: if the argument order changes then this can be just one function *) |
|
1191 fun mk_method1 tac thm ctxt = |
1186 fun mk_method1 tac thm ctxt = |
1192 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
1187 SIMPLE_METHOD (HEADGOAL (tac ctxt thm)) |
1193 |
1188 |
1194 fun mk_method2 tac ctxt = |
1189 fun mk_method2 tac ctxt = |
1195 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |
1190 SIMPLE_METHOD (HEADGOAL (tac ctxt)) |