src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 50058 bb1fadeba35e
parent 49684 1cf810b8f600
child 51070 6ca703425c01
equal deleted inserted replaced
50057:57209cfbf16b 50058:bb1fadeba35e
   656   in
   656   in
   657     EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   657     EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
   658       REPEAT_DETERM o rtac allI,
   658       REPEAT_DETERM o rtac allI,
   659       CONJ_WRAP' (fn Lev_0 =>
   659       CONJ_WRAP' (fn Lev_0 =>
   660         EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
   660         EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
   661           etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefix_Nil[THEN subst, of "%x. x"]},
   661           etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
   662           hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   662           hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   663           rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
   663           rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
   664       REPEAT_DETERM o rtac allI,
   664       REPEAT_DETERM o rtac allI,
   665       CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
   665       CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
   666         EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
   666         EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
   667           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   667           CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   668             (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   668             (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   669               dtac @{thm prefix_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
   669               dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
   670               rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   670               rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   671               rtac Lev_0, rtac @{thm singletonI},
   671               rtac Lev_0, rtac @{thm singletonI},
   672               REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
   672               REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
   673               rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
   673               rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
   674               rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
   674               rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
   855         rtac conjI,
   855         rtac conjI,
   856           rtac @{thm UN_least}, rtac Lev_sbd,
   856           rtac @{thm UN_least}, rtac Lev_sbd,
   857         rtac conjI,
   857         rtac conjI,
   858           rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,
   858           rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI,
   859           rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},
   859           rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans},
   860           etac @{thm prefix_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
   860           etac @{thm prefixeq_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac,
   861         rtac conjI,
   861         rtac conjI,
   862           rtac ballI, etac @{thm UN_E}, rtac conjI,
   862           rtac ballI, etac @{thm UN_E}, rtac conjI,
   863           if n = 1 then K all_tac else rtac (mk_sumEN n),
   863           if n = 1 then K all_tac else rtac (mk_sumEN n),
   864           EVERY' (map6 (fn i => fn isNode_def => fn set_naturals =>
   864           EVERY' (map6 (fn i => fn isNode_def => fn set_naturals =>
   865             fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
   865             fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>