237 *) |
237 *) |
238 |
238 |
239 text {* tyRel takes a type and builds a relation that a quantifier over this |
239 text {* tyRel takes a type and builds a relation that a quantifier over this |
240 type needs to respect. *} |
240 type needs to respect. *} |
241 ML {* |
241 ML {* |
242 fun matches (ty1, ty2) = |
|
243 Type.raw_instance (ty1, Logic.varifyT ty2); |
|
244 |
|
245 fun tyRel ty rty rel lthy = |
242 fun tyRel ty rty rel lthy = |
246 if matches (rty, ty) |
243 if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty) |
247 then rel |
244 then rel |
248 else (case ty of |
245 else (case ty of |
249 Type (s, tys) => |
246 Type (s, tys) => |
250 let |
247 let |
251 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
248 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
257 | NONE => HOLogic.eq_const ty |
254 | NONE => HOLogic.eq_const ty |
258 ) |
255 ) |
259 end |
256 end |
260 | _ => HOLogic.eq_const ty) |
257 | _ => HOLogic.eq_const ty) |
261 *} |
258 *} |
|
259 |
|
260 (* ML {* cterm_of @{theory} (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) *} *) |
262 |
261 |
263 definition |
262 definition |
264 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
263 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
265 where |
264 where |
266 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
265 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
405 |
404 |
406 (* Needed to have a meta-equality *) |
405 (* Needed to have a meta-equality *) |
407 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id" |
406 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id" |
408 by (simp add: id_def) |
407 by (simp add: id_def) |
409 |
408 |
410 ML {* |
|
411 fun old_exchange_ty rty qty ty = |
|
412 if ty = rty |
|
413 then qty |
|
414 else |
|
415 (case ty of |
|
416 Type (s, tys) => Type (s, map (old_exchange_ty rty qty) tys) |
|
417 | _ => ty |
|
418 ) |
|
419 *} |
|
420 |
|
421 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *) |
409 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *) |
422 ML {* fun exchange_ty rty (qty as (Type (qtys, _))) ty = |
410 ML {* |
423 let val (s, tys) = dest_Type ty in |
411 fun exchange_ty lthy rty qty ty = |
424 if Type.raw_instance (Logic.varifyT ty, rty) |
412 let |
425 then Type (qtys, tys) |
413 val thy = ProofContext.theory_of lthy |
426 else Type (s, map (exchange_ty rty qty) tys) |
414 in |
427 end |
415 if Sign.typ_instance thy (ty, rty) then |
428 handle _ => ty |
416 let |
429 *} |
417 val inst = Sign.typ_match thy (rty, ty) Vartab.empty |
|
418 in |
|
419 Envir.subst_type inst qty |
|
420 end |
|
421 else |
|
422 let |
|
423 val (s, tys) = dest_Type ty |
|
424 in |
|
425 Type (s, map (exchange_ty lthy rty qty) tys) |
|
426 end |
|
427 end |
|
428 handle _ => ty (* for dest_Type *) |
|
429 *} |
|
430 |
|
431 (*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
432 axioms Rl_eq: "EQUIV Rl" |
|
433 |
|
434 quotient ql = "'a list" / "Rl" |
|
435 by (rule Rl_eq) |
|
436 ML {* |
|
437 ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"}); |
|
438 ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"}) |
|
439 *} |
|
440 *) |
|
441 |
430 |
442 |
431 ML {* |
443 ML {* |
432 fun negF absF = repF |
444 fun negF absF = repF |
433 | negF repF = absF |
445 | negF repF = absF |
434 |
446 |
456 val ftys = map (op -->) tys |
468 val ftys = map (op -->) tys |
457 in |
469 in |
458 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
470 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
459 end |
471 end |
460 |
472 |
|
473 val thy = ProofContext.theory_of lthy |
|
474 |
461 fun get_const flag (rty, qty) = |
475 fun get_const flag (rty, qty) = |
462 let |
476 let |
463 val thy = ProofContext.theory_of lthy |
|
464 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
477 val qty_name = Long_Name.base_name (fst (dest_Type qty)) |
465 in |
478 in |
466 case flag of |
479 case flag of |
467 absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) |
480 absF => (Const (Sign.full_bname thy ("ABS_" ^ qty_name), rty --> qty), (rty, qty)) |
468 | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) |
481 | repF => (Const (Sign.full_bname thy ("REP_" ^ qty_name), qty --> rty), (qty, rty)) |
469 end |
482 end |
470 |
483 |
471 fun mk_identity ty = Abs ("", ty, Bound 0) |
484 fun mk_identity ty = Abs ("", ty, Bound 0) |
472 |
485 |
473 in |
486 in |
474 if (Type.raw_instance (Logic.varifyT ty, rty)) |
487 if (Sign.typ_instance thy (ty, rty)) |
475 then (get_const flag (ty, (exchange_ty rty qty ty))) |
488 then (get_const flag (ty, (exchange_ty lthy rty qty ty))) |
476 else (case ty of |
489 else (case ty of |
477 TFree _ => (mk_identity ty, (ty, ty)) |
490 TFree _ => (mk_identity ty, (ty, ty)) |
478 | Type (_, []) => (mk_identity ty, (ty, ty)) |
491 | Type (_, []) => (mk_identity ty, (ty, ty)) |
479 | Type ("fun" , [ty1, ty2]) => |
492 | Type ("fun" , [ty1, ty2]) => |
480 get_fun_fun [get_fun_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2] |
493 get_fun_fun [get_fun_noexchange (negF flag) (rty,qty) lthy ty1, get_fun_noexchange flag (rty,qty) lthy ty2] |
499 |
512 |
500 ML {* |
513 ML {* |
501 fun get_fun_new flag rty qty lthy ty = |
514 fun get_fun_new flag rty qty lthy ty = |
502 let |
515 let |
503 val tys = find_matching_types rty ty; |
516 val tys = find_matching_types rty ty; |
504 val qenv = map (fn t => (exchange_ty rty qty t, t)) tys; |
517 val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys; |
505 val xchg_ty = exchange_ty rty qty ty |
518 val xchg_ty = exchange_ty lthy rty qty ty |
506 in |
519 in |
507 get_fun flag qenv lthy xchg_ty |
520 get_fun flag qenv lthy xchg_ty |
508 end |
521 end |
509 *} |
522 *} |
510 |
523 |
873 val (a2, e2) = findallex_all rty qty a; |
886 val (a2, e2) = findallex_all rty qty a; |
874 in (a1 @ a2, e1 @ e2) end |
887 in (a1 @ a2, e1 @ e2) end |
875 | _ => ([], []); |
888 | _ => ([], []); |
876 *} |
889 *} |
877 ML {* |
890 ML {* |
878 fun findallex rty qty tm = |
891 fun findallex lthy rty qty tm = |
879 let |
892 let |
880 val (a, e) = findallex_all rty qty tm; |
893 val (a, e) = findallex_all rty qty tm; |
881 val (ad, ed) = (map domain_type a, map domain_type e); |
894 val (ad, ed) = (map domain_type a, map domain_type e); |
882 val (au, eu) = (distinct (op =) ad, distinct (op =) ed) |
895 val (au, eu) = (distinct (op =) ad, distinct (op =) ed); |
|
896 val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty) |
883 in |
897 in |
884 (map (old_exchange_ty rty qty) au, map (old_exchange_ty rty qty) eu) |
898 (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu) |
885 end |
899 end |
886 *} |
900 *} |
887 |
901 |
888 ML {* |
902 ML {* |
889 fun make_allex_prs_thm lthy quot_thm thm typ = |
903 fun make_allex_prs_thm lthy quot_thm thm typ = |
910 fun applic_prs lthy rty qty absrep ty = |
924 fun applic_prs lthy rty qty absrep ty = |
911 let |
925 let |
912 val rty = Logic.varifyT rty; |
926 val rty = Logic.varifyT rty; |
913 val qty = Logic.varifyT qty; |
927 val qty = Logic.varifyT qty; |
914 fun absty ty = |
928 fun absty ty = |
915 exchange_ty rty qty ty |
929 exchange_ty lthy rty qty ty |
916 fun mk_rep tm = |
930 fun mk_rep tm = |
917 let |
931 let |
918 val ty = exchange_ty qty rty (fastype_of tm) |
932 val ty = exchange_ty lthy qty rty (fastype_of tm) |
919 in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ tm end; |
933 in fst (get_fun_noexchange repF (rty, qty) lthy ty) $ tm end; |
920 fun mk_abs tm = |
934 fun mk_abs tm = |
921 let |
935 let |
922 val ty = fastype_of tm |
936 val ty = fastype_of tm |
923 in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end |
937 in fst (get_fun_noexchange absF (rty, qty) lthy ty) $ tm end |
939 singleton (ProofContext.export lthy' lthy) t_id |
953 singleton (ProofContext.export lthy' lthy) t_id |
940 end |
954 end |
941 *} |
955 *} |
942 |
956 |
943 ML {* |
957 ML {* |
|
958 fun matches (ty1, ty2) = |
|
959 Type.raw_instance (ty1, Logic.varifyT ty2); |
|
960 |
944 fun lookup_quot_data lthy qty = |
961 fun lookup_quot_data lthy qty = |
945 let |
962 let |
946 val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) |
963 val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy) |
947 val rty = Logic.unvarifyT (#rtyp quotdata) |
964 val rty = Logic.unvarifyT (#rtyp quotdata) |
948 val rel = #rel quotdata |
965 val rel = #rel quotdata |
984 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; |
1001 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; |
985 val consts = lookup_quot_consts defs; |
1002 val consts = lookup_quot_consts defs; |
986 val t_a = atomize_thm t; |
1003 val t_a = atomize_thm t; |
987 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
1004 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
988 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
1005 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
989 val (alls, exs) = findallex rty qty (prop_of t_a); |
1006 val (alls, exs) = findallex lthy rty qty (prop_of t_a); |
990 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
1007 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
991 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
1008 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
992 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
1009 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
993 val abs = findabs rty (prop_of t_a); |
1010 val abs = findabs rty (prop_of t_a); |
994 val aps = findaps rty (prop_of t_a); |
1011 val aps = findaps rty (prop_of t_a); |
998 val defs_sym = add_lower_defs lthy defs; |
1015 val defs_sym = add_lower_defs lthy defs; |
999 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
1016 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
1000 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; |
1017 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; |
1001 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
1018 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
1002 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
1019 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
|
1020 val t_rv = ObjectLogic.rulify t_r |
1003 in |
1021 in |
1004 ObjectLogic.rulify t_r |
1022 Thm.varifyT t_rv |
1005 end |
1023 end |
1006 *} |
1024 *} |
|
1025 |
1007 |
1026 |
1008 ML {* |
1027 ML {* |
1009 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = |
1028 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = |
1010 let |
1029 let |
1011 val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; |
1030 val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; |