# HG changeset patch # User traytel # Date 1392807861 -3600 # Node ID d1c228753d76d889f47869daa219575a585d4b02 # Parent d12a13713cb44da4efc09928deeab4ce000c8185 another simplification of internal codatatype construction diff -r d12a13713cb4 -r d1c228753d76 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 19 11:11:07 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 19 12:04:21 2014 +0100 @@ -1069,12 +1069,10 @@ val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl); val tree = mk_Ball Kl (Term.absfree kl' - (HOLogic.mk_conj - (Library.foldr1 HOLogic.mk_disj (map (mk_isNode kl) ks), - Library.foldr1 HOLogic.mk_conj (map4 (fn Succ => fn i => fn k => fn k' => - mk_Ball Succ (Term.absfree k' (mk_isNode - (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i))) - Succs ks kks kks')))); + (Library.foldr1 HOLogic.mk_conj (map4 (fn Succ => fn i => fn k => fn k' => + mk_Ball Succ (Term.absfree k' (mk_isNode + (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i))) + Succs ks kks kks'))); in HOLogic.mk_conj (empty, tree) end; diff -r d12a13713cb4 -r d1c228753d76 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Wed Feb 19 11:11:07 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Wed Feb 19 12:04:21 2014 +0100 @@ -370,11 +370,8 @@ rtac conjI, etac @{thm empty_Shift}, dtac set_rev_mp, etac equalityD1, etac CollectD, rtac ballI, - rtac conjI, dtac @{thm iffD1[OF ball_conj_distrib]}, dtac conjunct1, - SELECT_GOAL (unfold_thms_tac ctxt @{thms Succ_Shift shift_def}), - etac bspec, etac @{thm ShiftD}, CONJ_WRAP' (fn i => EVERY' [rtac ballI, etac CollectE, dtac @{thm ShiftD}, - dtac bspec, etac thin_rl, atac, dtac conjunct2, dtac (mk_conjunctN n i), + dtac bspec, etac thin_rl, atac, dtac (mk_conjunctN n i), dtac bspec, rtac CollectI, etac @{thm set_mp[OF equalityD1[OF Succ_Shift]]}, REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans), @@ -382,7 +379,7 @@ CONJ_WRAP' (K (EVERY' [etac trans, rtac @{thm Collect_cong}, rtac @{thm eqset_imp_iff}, rtac sym, rtac trans, rtac @{thm Succ_Shift}, rtac (@{thm append_Cons} RS sym RS arg_cong)])) ks]) ks, - dtac bspec, atac, dtac conjunct2, dtac (mk_conjunctN n i), dtac bspec, + dtac bspec, atac, dtac (mk_conjunctN n i), dtac bspec, etac @{thm set_mp[OF equalityD1]}, atac, REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI, rtac (@{thm shift_def} RS fun_cong RS trans), @@ -565,23 +562,7 @@ rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, (**) - rtac ballI, etac @{thm UN_E}, rtac conjI, - if n = 1 then K all_tac else rtac (mk_sumEN n), - EVERY' (map5 (fn i => fn isNode_def => fn set_map0s => fn set_Levs => fn set_image_Levs => - EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst), - rtac exI, rtac conjI, - if n = 1 then rtac refl - else etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i), - CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) => - EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI}, - rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev, - if n = 1 then rtac refl else atac, atac, rtac subsetI, - REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], - rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev', - etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]}, - if n = 1 then rtac refl else atac]) - (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))]) - ks isNode_defs set_map0ss set_Levss set_image_Levss), + rtac ballI, etac @{thm UN_E}, CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_map0s, (set_Levs, set_image_Levs))))) => EVERY' [rtac ballI,