278 val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") |
278 val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same") |
279 val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") |
279 val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10") |
280 val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name) |
280 val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name) |
281 in |
281 in |
282 (trans2, reps_same, absrep, quot) |
282 (trans2, reps_same, absrep, quot) |
283 end |
|
284 *} |
|
285 |
|
286 ML {* |
|
287 fun lookup_quot_consts defs = |
|
288 let |
|
289 fun dest_term (a $ b) = (a, b); |
|
290 val def_terms = map (snd o Logic.dest_equals o concl_of) defs; |
|
291 in |
|
292 map (fst o dest_Const o snd o dest_term) def_terms |
|
293 end |
283 end |
294 *} |
284 *} |
295 |
285 |
296 section {* Regularization *} |
286 section {* Regularization *} |
297 |
287 |
935 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
925 fun dest_fun_type (Type("fun", [T, S])) = (T, S) |
936 | dest_fun_type _ = error "dest_fun_type" |
926 | dest_fun_type _ = error "dest_fun_type" |
937 *} |
927 *} |
938 |
928 |
939 ML {* |
929 ML {* |
|
930 val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl |
|
931 *} |
|
932 |
|
933 ML {* |
940 fun rep_abs_rsp_tac ctxt = |
934 fun rep_abs_rsp_tac ctxt = |
941 SUBGOAL (fn (goal, i) => |
935 SUBGOAL (fn (goal, i) => |
942 case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of (rel $ _ $ (rep $ (abs $ _))) => |
936 case (bare_concl goal) of |
943 (let |
937 (rel $ _ $ (rep $ (abs $ _))) => |
944 val thy = ProofContext.theory_of ctxt; |
938 (let |
945 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
939 val thy = ProofContext.theory_of ctxt; |
946 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
940 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
947 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
941 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
948 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
942 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
949 val te = solve_quotient_assums ctxt thm |
943 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
950 in |
944 val te = solve_quotient_assums ctxt thm |
951 rtac te i |
945 in |
952 end |
946 rtac te i |
953 handle _ => no_tac) |
947 end |
954 | _ => no_tac) |
948 handle _ => no_tac) |
|
949 | _ => no_tac) |
955 *} |
950 *} |
956 |
951 |
957 lemma fun_rel_id: |
952 lemma fun_rel_id: |
958 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
953 assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)" |
959 shows "(R1 ===> R2) f g" |
954 shows "(R1 ===> R2) f g" |
960 using a by simp |
955 using a by simp |
961 |
956 |
962 |
957 |
963 ML {* |
958 ML {* |
964 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
959 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) => |
965 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of |
960 (case (bare_concl goal) of |
966 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
961 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
967 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
962 ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)) |
968 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
963 => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam |
969 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
964 (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *) |
970 | (Const (@{const_name "op ="},_) $ |
965 | (Const (@{const_name "op ="},_) $ |