1493 ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN |
1493 ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN |
1494 ALLGOALS (TRY o |
1494 ALLGOALS (TRY o |
1495 FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) |
1495 FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) |
1496 |
1496 |
1497 fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor |
1497 fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets dtor_inject dtor_ctor |
1498 set_naturals set_incls set_set_inclss = |
1498 set_naturals dtor_set_incls dtor_set_set_inclss = |
1499 let |
1499 let |
1500 val m = length set_incls; |
1500 val m = length dtor_set_incls; |
1501 val n = length set_set_inclss; |
1501 val n = length dtor_set_set_inclss; |
1502 val (passive_set_naturals, active_set_naturals) = chop m set_naturals; |
1502 val (passive_set_naturals, active_set_naturals) = chop m set_naturals; |
1503 val in_Jsrel = nth in_Jsrels (i - 1); |
1503 val in_Jsrel = nth in_Jsrels (i - 1); |
1504 val if_tac = |
1504 val if_tac = |
1505 EVERY' [dtac (in_Jsrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], |
1505 EVERY' [dtac (in_Jsrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], |
1506 rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
1506 rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
1507 EVERY' (map2 (fn set_natural => fn set_incl => |
1507 EVERY' (map2 (fn set_natural => fn set_incl => |
1508 EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural, |
1508 EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural, |
1509 rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, |
1509 rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply, |
1510 etac (set_incl RS @{thm subset_trans})]) |
1510 etac (set_incl RS @{thm subset_trans})]) |
1511 passive_set_naturals set_incls), |
1511 passive_set_naturals dtor_set_incls), |
1512 CONJ_WRAP' (fn (in_Jsrel, (set_natural, set_set_incls)) => |
1512 CONJ_WRAP' (fn (in_Jsrel, (set_natural, dtor_set_set_incls)) => |
1513 EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI}, |
1513 EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI}, |
1514 rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
1514 rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI, |
1515 CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) set_set_incls, |
1515 CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls, |
1516 rtac conjI, rtac refl, rtac refl]) |
1516 rtac conjI, rtac refl, rtac refl]) |
1517 (in_Jsrels ~~ (active_set_naturals ~~ set_set_inclss)), |
1517 (in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)), |
1518 CONJ_WRAP' (fn conv => |
1518 CONJ_WRAP' (fn conv => |
1519 EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong, |
1519 EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong, |
1520 REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, |
1520 REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]}, |
1521 REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), |
1521 REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]), |
1522 rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac]) |
1522 rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac]) |