140 section {* type definition for the quotient type *} |
140 section {* type definition for the quotient type *} |
141 |
141 |
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 |
|
146 declare [[map "fun" = (fun_map, fun_rel)]] |
145 declare [[map "fun" = (fun_map, fun_rel)]] |
147 |
146 |
148 (* Throws now an exception: *) |
147 (* Throws now an exception: *) |
149 (* declare [[map "option" = (bla, blu)]] *) |
148 (* declare [[map "option" = (bla, blu)]] *) |
150 |
149 |
209 @{thm equal_elim_rule1} OF [thm'', thm'] |
208 @{thm equal_elim_rule1} OF [thm'', thm'] |
210 end |
209 end |
211 *} |
210 *} |
212 |
211 |
213 section {* Infrastructure about id *} |
212 section {* Infrastructure about id *} |
214 |
|
215 print_attributes |
|
216 |
213 |
217 (* TODO: think where should this be *) |
214 (* TODO: think where should this be *) |
218 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
215 lemma prod_fun_id: "prod_fun id id \<equiv> id" |
219 by (rule eq_reflection) (simp add: prod_fun_def) |
216 by (rule eq_reflection) (simp add: prod_fun_def) |
220 |
217 |
373 |
370 |
374 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
371 | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') => |
375 let |
372 let |
376 val subtrm = apply_subt (regularize_trm lthy) t t' |
373 val subtrm = apply_subt (regularize_trm lthy) t t' |
377 in |
374 in |
378 if ty = ty' |
375 if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm |
379 then Const (@{const_name "All"}, ty) $ subtrm |
|
380 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
376 else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
381 end |
377 end |
382 |
378 |
383 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
379 | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') => |
384 let |
380 let |
385 val subtrm = apply_subt (regularize_trm lthy) t t' |
381 val subtrm = apply_subt (regularize_trm lthy) t t' |
386 in |
382 in |
387 if ty = ty' |
383 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm |
388 then Const (@{const_name "Ex"}, ty) $ subtrm |
|
389 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
384 else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm |
390 end |
385 end |
391 |
386 |
392 | (* equalities need to be replaced by appropriate equivalence relations *) |
387 | (* equalities need to be replaced by appropriate equivalence relations *) |
393 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
388 (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) => |
399 let |
394 let |
400 val exc = LIFT_MATCH "regularise (relation mismatch)" |
395 val exc = LIFT_MATCH "regularise (relation mismatch)" |
401 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
396 val rel_ty = (fastype_of rel) handle TERM _ => raise exc |
402 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
397 val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') |
403 in |
398 in |
404 if rel' = rel |
399 if rel' = rel then rtrm else raise exc |
405 then rtrm else raise exc |
|
406 end |
400 end |
407 | (_, Const (s, _)) => |
401 | (_, Const (s, _)) => |
408 let |
402 let |
409 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
403 fun same_name (Const (s, _)) (Const (s', _)) = (s = s') |
410 | same_name _ _ = false |
404 | same_name _ _ = false |
416 fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)") |
410 fun exc1 s = LIFT_MATCH ("regularize (constant " ^ s ^ " not found)") |
417 val exc2 = LIFT_MATCH ("regularize (constant mismatch)") |
411 val exc2 = LIFT_MATCH ("regularize (constant mismatch)") |
418 val thy = ProofContext.theory_of lthy |
412 val thy = ProofContext.theory_of lthy |
419 val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) |
413 val rtrm' = (#rconst (qconsts_lookup thy s)) handle NotFound => raise (exc1 s) |
420 in |
414 in |
421 if matches_term (rtrm, rtrm') |
415 if matches_term (rtrm, rtrm') then rtrm else raise exc2 |
422 then rtrm |
|
423 else raise exc2 |
|
424 end |
416 end |
425 end |
417 end |
426 |
418 |
427 | (t1 $ t2, t1' $ t2') => |
419 | (t1 $ t2, t1' $ t2') => |
428 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
420 (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2') |
441 |
433 |
442 section {* Regularize Tactic *} |
434 section {* Regularize Tactic *} |
443 |
435 |
444 ML {* |
436 ML {* |
445 fun equiv_tac ctxt = |
437 fun equiv_tac ctxt = |
446 (K (print_tac "equiv tac")) THEN' |
|
447 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
438 REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt)) |
448 |
439 |
449 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
440 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
450 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
441 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
451 *} |
442 *} |
717 lemma quot_true_dests: |
708 lemma quot_true_dests: |
718 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
709 shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P" |
719 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
710 and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P" |
720 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
711 and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))" |
721 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
712 and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)" |
722 apply(simp_all add: QUOT_TRUE_def ext) |
713 by (simp_all add: QUOT_TRUE_def ext) |
723 done |
|
724 |
714 |
725 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P" |
715 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P" |
726 by (simp add: QUOT_TRUE_def) |
716 by (simp add: QUOT_TRUE_def) |
727 |
717 |
728 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
718 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
1045 thm all_prs ex_prs |
1035 thm all_prs ex_prs |
1046 (* 3. simplification with *) |
1036 (* 3. simplification with *) |
1047 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps |
1037 thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps |
1048 (* 4. Test for refl *) |
1038 (* 4. Test for refl *) |
1049 |
1039 |
1050 thm fun_map.simps |
|
1051 |
|
1052 ML {* Conv.abs_conv; term_of *} |
|
1053 |
|
1054 thm fun_map.simps[THEN eq_reflection] |
|
1055 |
|
1056 ML {* |
1040 ML {* |
1057 fun fun_map_conv xs ctxt ctrm = |
1041 fun fun_map_conv xs ctxt ctrm = |
1058 case (term_of ctrm) of |
1042 case (term_of ctrm) of |
1059 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
1043 ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) => |
1060 (Conv.binop_conv (fun_map_conv xs ctxt) then_conv |
1044 (Conv.binop_conv (fun_map_conv xs ctxt) then_conv |
1062 then Conv.all_conv |
1046 then Conv.all_conv |
1063 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]})) ctrm |
1047 else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]})) ctrm |
1064 | _ $ _ => Conv.comb_conv (fun_map_conv xs ctxt) ctrm |
1048 | _ $ _ => Conv.comb_conv (fun_map_conv xs ctxt) ctrm |
1065 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
1049 | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm |
1066 | _ => Conv.all_conv ctrm |
1050 | _ => Conv.all_conv ctrm |
1067 *} |
1051 |
1068 |
|
1069 ML {* |
|
1070 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
1052 fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt) |
1071 *} |
1053 *} |
1072 |
1054 |
1073 ML {* |
1055 ML {* |
1074 fun clean_tac lthy = |
1056 fun clean_tac lthy = |