QuotMain.thy
changeset 410 e3eb88d79ad7
parent 409 6b59a3844055
child 411 c10e314761fa
equal deleted inserted replaced
409:6b59a3844055 410:e3eb88d79ad7
   723     rtac (Drule.instantiate insts thm) 1
   723     rtac (Drule.instantiate insts thm) 1
   724   end
   724   end
   725   handle _ => no_tac)
   725   handle _ => no_tac)
   726 *}
   726 *}
   727 
   727 
   728 ML {*
       
   729 fun CHANGED' tac = (fn i => CHANGED (tac i))
       
   730 *}
       
   731 
   728 
   732 ML {*
   729 ML {*
   733 fun quotient_tac quot_thm =
   730 fun quotient_tac quot_thm =
   734   REPEAT_ALL_NEW (FIRST' [
   731   REPEAT_ALL_NEW (FIRST' [
   735     rtac @{thm FUN_QUOTIENT},
   732     rtac @{thm FUN_QUOTIENT},
   736     rtac quot_thm,
   733     rtac quot_thm,
   737     rtac @{thm IDENTITY_QUOTIENT},
   734     rtac @{thm IDENTITY_QUOTIENT},
   738     (* For functional identity quotients, (op = ---> op =) *)
   735     (* For functional identity quotients, (op = ---> op =) *)
   739     CHANGED' (simp_tac (HOL_ss addsimps @{thms id_simps}))
   736     CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))
   740   ])
   737   ])
   741 *}
   738 *}
   742 
   739 
   743 ML {*
   740 ML {*
   744 fun LAMBDA_RES_TAC ctxt i st =
   741 fun LAMBDA_RES_TAC ctxt i st =
   831     rtac @{thm ext},
   828     rtac @{thm ext},
   832     rtac reflex_thm,
   829     rtac reflex_thm,
   833     atac,
   830     atac,
   834     SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
   831     SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
   835     WEAK_LAMBDA_RES_TAC ctxt,
   832     WEAK_LAMBDA_RES_TAC ctxt,
   836     CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
   833     CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
   837     ])
   834     ])
   838 *}
   835 *}
   839 
   836 
   840 (*
   837 (*
   841 To prove that the regularised theorem implies the abs/rep injected, 
   838 To prove that the regularised theorem implies the abs/rep injected, 
   880     DT ctxt "C" (rtac @{thm ext}),
   877     DT ctxt "C" (rtac @{thm ext}),
   881     DT ctxt "D" (rtac reflex_thm),
   878     DT ctxt "D" (rtac reflex_thm),
   882     DT ctxt "E" (atac),
   879     DT ctxt "E" (atac),
   883     DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
   880     DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
   884     DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
   881     DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
   885     DT ctxt "H" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
   882     DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
   886     ])
   883     ])
   887 *}
   884 *}
   888 
   885 
   889 
   886 
   890 
   887