QuotMain.thy
changeset 485 4efb104514f7
parent 482 767baada01dc
child 486 7c26b31d2371
equal deleted inserted replaced
483:74348dc2f8bb 485:4efb104514f7
   785 fun quotient_tac ctxt quot_thms =
   785 fun quotient_tac ctxt quot_thms =
   786   REPEAT_ALL_NEW (FIRST'
   786   REPEAT_ALL_NEW (FIRST'
   787     [rtac @{thm FUN_QUOTIENT},
   787     [rtac @{thm FUN_QUOTIENT},
   788      resolve_tac quot_thms,
   788      resolve_tac quot_thms,
   789      rtac @{thm IDENTITY_QUOTIENT},
   789      rtac @{thm IDENTITY_QUOTIENT},
       
   790      rtac @{thm LIST_QUOTIENT},
   790      (* For functional identity quotients, (op = ---> op =) *)
   791      (* For functional identity quotients, (op = ---> op =) *)
   791      (* TODO: think about the other way around, if we need to shorten the relation *)
   792      (* TODO: think about the other way around, if we need to shorten the relation *)
   792      CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
   793      CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
   793 *}
   794 *}
   794 
   795 
  1220     val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
  1221     val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
  1221     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
  1222     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
  1222     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
  1223     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
  1223       (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
  1224       (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
  1224   in
  1225   in
  1225     EVERY' [lambda_prs_tac lthy quot,
  1226     EVERY' [TRY o lambda_prs_tac lthy quot,
  1226             TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
  1227             TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
  1227             TRY o simp_tac simp_ctxt,
  1228             TRY o simp_tac simp_ctxt,
  1228             TRY o rtac refl]
  1229             TRY o rtac refl]
  1229   end
  1230   end
  1230 *}
  1231 *}