439 14) simplifying (= ===> =) for simpler respectfullness |
439 14) simplifying (= ===> =) for simpler respectfullness |
440 |
440 |
441 *) |
441 *) |
442 |
442 |
443 |
443 |
444 (* Needed to have a meta-equality *) |
|
445 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id" |
|
446 by (simp add: id_def) |
|
447 |
|
448 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *) |
444 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *) |
449 ML {* |
445 ML {* |
450 fun exchange_ty lthy rty qty ty = |
446 fun exchange_ty lthy rty qty ty = |
451 let |
447 let |
452 val thy = ProofContext.theory_of lthy |
448 val thy = ProofContext.theory_of lthy |
462 val (s, tys) = dest_Type ty |
458 val (s, tys) = dest_Type ty |
463 in |
459 in |
464 Type (s, map (exchange_ty lthy rty qty) tys) |
460 Type (s, map (exchange_ty lthy rty qty) tys) |
465 end |
461 end |
466 end |
462 end |
467 handle _ => ty (* for dest_Type *) |
463 handle TYPE _ => ty (* for dest_Type *) |
468 *} |
464 *} |
469 |
465 |
470 (*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
466 (*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
471 axioms Rl_eq: "EQUIV Rl" |
467 axioms Rl_eq: "EQUIV Rl" |
472 |
468 |
473 quotient ql = "'a list" / "Rl" |
469 quotient ql = "'a list" / "Rl" |
474 by (rule Rl_eq) |
470 by (rule Rl_eq) |
475 ML {* |
471 ML {* |
476 ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"}); |
472 ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"}); |
477 ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"}) |
473 ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"}) |
478 *} |
474 *} |
479 *) |
475 *) |
480 |
476 |
616 val goalstate = Goal.init (Thm.cprop_of thm) |
612 val goalstate = Goal.init (Thm.cprop_of thm) |
617 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
613 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
618 NONE => error "eqsubst_thm" |
614 NONE => error "eqsubst_thm" |
619 | SOME th => cprem_of th 1 |
615 | SOME th => cprem_of th 1 |
620 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
616 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
621 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
617 val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a'); |
622 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
618 val cgoal = cterm_of (ProofContext.theory_of ctxt) goal |
|
619 val rt = Goal.prove_internal [] cgoal (fn _ => tac); |
623 in |
620 in |
624 @{thm Pure.equal_elim_rule1} OF [rt, thm] |
621 @{thm Pure.equal_elim_rule1} OF [rt, thm] |
625 end |
622 end |
626 *} |
623 *} |
627 |
624 |
628 ML {* |
625 ML {* |
629 fun repeat_eqsubst_thm ctxt thms thm = |
626 fun repeat_eqsubst_thm ctxt thms thm = |
630 repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) |
627 repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) |
631 handle _ => thm |
628 handle _ => thm |
632 *} |
629 *} |
|
630 |
|
631 (* Needed to have a meta-equality *) |
|
632 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id" |
|
633 by (simp add: id_def) |
633 |
634 |
634 ML {* |
635 ML {* |
635 fun build_repabs_term lthy thm consts rty qty = |
636 fun build_repabs_term lthy thm consts rty qty = |
636 let |
637 let |
637 val rty = Logic.varifyT rty; |
638 val rty = Logic.varifyT rty; |
760 val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
761 val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
761 let |
762 let |
762 val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ |
763 val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ |
763 (Const (@{const_name Ball}, _) $ _)) = term_of concl |
764 (Const (@{const_name Ball}, _) $ _)) = term_of concl |
764 in |
765 in |
765 ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
766 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
766 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
767 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
767 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
768 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
768 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1 |
769 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
769 end |
770 end |
770 handle _ => no_tac |
771 handle _ => no_tac |
771 ) |
772 ) |
772 *} |
773 *} |
773 |
774 |
775 val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
776 val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
776 let |
777 let |
777 val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ |
778 val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ |
778 (Const (@{const_name Bex}, _) $ _)) = term_of concl |
779 (Const (@{const_name Bex}, _) $ _)) = term_of concl |
779 in |
780 in |
780 ((simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
781 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
781 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
782 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
782 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
783 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
783 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1 |
784 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
784 end |
785 end |
785 handle _ => no_tac |
786 handle _ => no_tac |
786 ) |
787 ) |
787 *} |
788 *} |
788 |
789 |
801 Cong_Tac.cong_tac @{thm cong}, |
802 Cong_Tac.cong_tac @{thm cong}, |
802 rtac @{thm ext}, |
803 rtac @{thm ext}, |
803 rtac reflex_thm, |
804 rtac reflex_thm, |
804 atac, |
805 atac, |
805 ( |
806 ( |
806 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
807 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
807 THEN_ALL_NEW (fn _ => no_tac) |
808 THEN_ALL_NEW (fn _ => no_tac) |
808 ), |
809 ), |
809 WEAK_LAMBDA_RES_TAC ctxt, |
810 WEAK_LAMBDA_RES_TAC ctxt, |
810 (fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i)) |
811 (fn i => CHANGED (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}) i)) |
811 ]) |
812 ]) |
993 val rargs = map mk_rep args; |
994 val rargs = map mk_rep args; |
994 val f = Free (fname, nl ---> ltl); |
995 val f = Free (fname, nl ---> ltl); |
995 val rhs = mk_abs (list_comb((mk_rep f), rargs)); |
996 val rhs = mk_abs (list_comb((mk_rep f), rargs)); |
996 val eq = Logic.mk_equals (rhs, lhs); |
997 val eq = Logic.mk_equals (rhs, lhs); |
997 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
998 val ceq = cterm_of (ProofContext.theory_of lthy') eq; |
998 val sctxt = (Simplifier.context lthy' HOL_ss) addsimps (absrep :: @{thms fun_map.simps}); |
999 val sctxt = HOL_ss addsimps (absrep :: @{thms fun_map.simps}); |
999 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
1000 val t = Goal.prove_internal [] ceq (fn _ => simp_tac sctxt 1) |
1000 val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t; |
1001 val t_id = MetaSimplifier.rewrite_rule @{thms id_def_sym} t; |
1001 in |
1002 in |
1002 singleton (ProofContext.export lthy' lthy) t_id |
1003 singleton (ProofContext.export lthy' lthy) t_id |
1003 end |
1004 end |