equal
deleted
inserted
replaced
395 in |
395 in |
396 case redex of |
396 case redex of |
397 (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ |
397 (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ |
398 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
398 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
399 calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 |
399 calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2 |
|
400 |
400 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ |
401 | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ |
401 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
402 (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) => |
402 calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 |
403 calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2 |
403 | _ => NONE |
404 | _ => NONE |
404 end |
405 end |
549 |
550 |
550 | _ => raise (LIFT_MATCH "injection") |
551 | _ => raise (LIFT_MATCH "injection") |
551 *} |
552 *} |
552 |
553 |
553 section {* Injection Tactic *} |
554 section {* Injection Tactic *} |
554 |
|
555 |
|
556 |
555 |
557 definition |
556 definition |
558 "QUOT_TRUE x \<equiv> True" |
557 "QUOT_TRUE x \<equiv> True" |
559 |
558 |
560 ML {* |
559 ML {* |
713 (let |
712 (let |
714 val thy = ProofContext.theory_of ctxt; |
713 val thy = ProofContext.theory_of ctxt; |
715 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
714 val (ty_a, ty_b) = dest_fun_type (fastype_of abs); |
716 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
715 val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b]; |
717 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
716 val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep]; |
718 val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
717 val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp} |
719 in |
718 in |
720 (rtac thm THEN' quotient_tac ctxt) i |
719 (rtac inst_thm THEN' quotient_tac ctxt) i |
721 end |
720 end |
722 handle _ => no_tac) (* what is the catch for ? Should go away, no? *) |
721 handle _ => no_tac) (* FIXME / TODO what is the catch for ? Should go away, no? *) |
723 | _ => no_tac) |
722 | _ => no_tac) |
724 *} |
723 *} |
725 |
724 |
726 ML {* |
725 ML {* |
727 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
726 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) => |
869 (f, Abs ("x", T, mk_abs u 0 g)) |
868 (f, Abs ("x", T, mk_abs u 0 g)) |
870 end |
869 end |
871 *} |
870 *} |
872 |
871 |
873 ML {* |
872 ML {* |
|
873 (* FIXME / TODO this needs to be clarified *) |
|
874 |
874 fun lambda_prs_simple_conv ctxt ctrm = |
875 fun lambda_prs_simple_conv ctxt ctrm = |
875 case (term_of ctrm) of |
876 case (term_of ctrm) of |
876 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
877 (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) => |
877 (let |
878 (let |
878 val thy = ProofContext.theory_of ctxt |
879 val thy = ProofContext.theory_of ctxt |
1000 (* *) |
1001 (* *) |
1001 (* the QUOT_TRUE premise in 2 records the lifted theorem *) |
1002 (* the QUOT_TRUE premise in 2 records the lifted theorem *) |
1002 |
1003 |
1003 ML {* |
1004 ML {* |
1004 val lifting_procedure = |
1005 val lifting_procedure = |
1005 @{lemma "\<lbrakk>A; A \<longrightarrow> B; QUOT_TRUE D \<Longrightarrow> B = C; C = D\<rbrakk> \<Longrightarrow> D" by (simp add: QUOT_TRUE_def)} |
1006 @{lemma "\<lbrakk>A; |
|
1007 A \<longrightarrow> B; |
|
1008 QUOT_TRUE D \<Longrightarrow> B = C; |
|
1009 C = D\<rbrakk> \<Longrightarrow> D" |
|
1010 by (simp add: QUOT_TRUE_def)} |
1006 *} |
1011 *} |
1007 |
1012 |
1008 ML {* |
1013 ML {* |
1009 fun lift_match_error ctxt fun_str rtrm qtrm = |
1014 fun lift_match_error ctxt fun_str rtrm qtrm = |
1010 let |
1015 let |