320 Simplifier because it also affects premises in congrence rules, |
320 Simplifier because it also affects premises in congrence rules, |
321 where this can lead to premises of the form @{text "!!a b. ... = |
321 where this can lead to premises of the form @{text "!!a b. ... = |
322 ?P(a, b)"} which cannot be solved by reflexivity. |
322 ?P(a, b)"} which cannot be solved by reflexivity. |
323 *} |
323 *} |
324 |
324 |
325 ML_setup {* |
325 ML {* |
326 (* replace parameters of product type by individual component parameters *) |
326 (* replace parameters of product type by individual component parameters *) |
327 val safe_full_simp_tac = generic_simp_tac true (true, false, false); |
327 val safe_full_simp_tac = generic_simp_tac true (true, false, false); |
328 local (* filtering with exists_paired_all is an essential optimization *) |
328 local (* filtering with exists_paired_all is an essential optimization *) |
329 fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) = |
329 fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) = |
330 can HOLogic.dest_prodT T orelse exists_paired_all t |
330 can HOLogic.dest_prodT T orelse exists_paired_all t |
331 | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u |
331 | exists_paired_all (t $ u) = exists_paired_all t orelse exists_paired_all u |
332 | exists_paired_all (Abs (_, _, t)) = exists_paired_all t |
332 | exists_paired_all (Abs (_, _, t)) = exists_paired_all t |
333 | exists_paired_all _ = false; |
333 | exists_paired_all _ = false; |
334 val ss = HOL_basic_ss |
334 val ss = HOL_basic_ss |
335 addsimps [thm "split_paired_all", thm "unit_all_eq2", thm "unit_abs_eta_conv"] |
335 addsimps [@{thm split_paired_all}, @{thm unit_all_eq2}, @{thm unit_abs_eta_conv}] |
336 addsimprocs [unit_eq_proc]; |
336 addsimprocs [unit_eq_proc]; |
337 in |
337 in |
338 val split_all_tac = SUBGOAL (fn (t, i) => |
338 val split_all_tac = SUBGOAL (fn (t, i) => |
339 if exists_paired_all t then safe_full_simp_tac ss i else no_tac); |
339 if exists_paired_all t then safe_full_simp_tac ss i else no_tac); |
340 val unsafe_split_all_tac = SUBGOAL (fn (t, i) => |
340 val unsafe_split_all_tac = SUBGOAL (fn (t, i) => |
341 if exists_paired_all t then full_simp_tac ss i else no_tac); |
341 if exists_paired_all t then full_simp_tac ss i else no_tac); |
342 fun split_all th = |
342 fun split_all th = |
343 if exists_paired_all (#prop (Thm.rep_thm th)) then full_simplify ss th else th; |
343 if exists_paired_all (Thm.prop_of th) then full_simplify ss th else th; |
344 end; |
344 end; |
345 |
345 *} |
346 change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac)); |
346 |
|
347 declaration {* fn _ => |
|
348 Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac)) |
347 *} |
349 *} |
348 |
350 |
349 lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))" |
351 lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))" |
350 -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *} |
352 -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *} |
351 by fast |
353 by fast |
539 by (rule major [unfolded split_def] cases surjective_pairing)+ |
541 by (rule major [unfolded split_def] cases surjective_pairing)+ |
540 |
542 |
541 declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!] |
543 declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!] |
542 declare mem_splitE [elim!] splitE' [elim!] splitE [elim!] |
544 declare mem_splitE [elim!] splitE' [elim!] splitE [elim!] |
543 |
545 |
544 ML_setup {* |
546 ML {* |
545 local (* filtering with exists_p_split is an essential optimization *) |
547 local (* filtering with exists_p_split is an essential optimization *) |
546 fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true |
548 fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true |
547 | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u |
549 | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u |
548 | exists_p_split (Abs (_, _, t)) = exists_p_split t |
550 | exists_p_split (Abs (_, _, t)) = exists_p_split t |
549 | exists_p_split _ = false; |
551 | exists_p_split _ = false; |
550 val ss = HOL_basic_ss addsimps [thm "split_conv"]; |
552 val ss = HOL_basic_ss addsimps [thm "split_conv"]; |
551 in |
553 in |
552 val split_conv_tac = SUBGOAL (fn (t, i) => |
554 val split_conv_tac = SUBGOAL (fn (t, i) => |
553 if exists_p_split t then safe_full_simp_tac ss i else no_tac); |
555 if exists_p_split t then safe_full_simp_tac ss i else no_tac); |
554 end; |
556 end; |
|
557 *} |
|
558 |
555 (* This prevents applications of splitE for already splitted arguments leading |
559 (* This prevents applications of splitE for already splitted arguments leading |
556 to quite time-consuming computations (in particular for nested tuples) *) |
560 to quite time-consuming computations (in particular for nested tuples) *) |
557 change_claset (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac)); |
561 declaration {* fn _ => |
|
562 Classical.map_cs (fn cs => cs addSbefore ("split_conv_tac", split_conv_tac)) |
558 *} |
563 *} |
559 |
564 |
560 lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P" |
565 lemma split_eta_SetCompr [simp,noatp]: "(%u. EX x y. u = (x, y) & P (x, y)) = P" |
561 by (rule ext) fast |
566 by (rule ext) fast |
562 |
567 |