# HG changeset patch # User traytel # Date 1392799850 -3600 # Node ID a6c2379078c84e823477e795aa66fadca6c6e1ff # Parent 315dd59201140f8daa2b03c19f55d85430c4f08a simplifications of internal codatatype construction diff -r 315dd5920114 -r a6c2379078c8 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 19 08:34:34 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 19 09:50:50 2014 +0100 @@ -982,7 +982,6 @@ end; val sbdTs = replicate n sbdT; - val sum_sbd = Library.foldr1 (uncurry mk_csum) (replicate n sbd); val sum_sbdT = mk_sumTN sbdTs; val sum_sbd_listT = HOLogic.listT sum_sbdT; val sum_sbd_list_setT = HOLogic.mk_setT sum_sbd_listT; @@ -1068,8 +1067,6 @@ val isTree = let val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl); - val Field = mk_leq Kl (mk_Field (mk_clists sum_sbd)); - val prefCl = mk_prefCl Kl; val tree = mk_Ball Kl (Term.absfree kl' (HOLogic.mk_conj @@ -1078,12 +1075,8 @@ 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')))); - - val undef = list_all_free [kl] (HOLogic.mk_imp - (HOLogic.mk_not (HOLogic.mk_mem (kl, Kl)), - HOLogic.mk_eq (lab $ kl, mk_undefined sbdFT))); in - Library.foldr1 HOLogic.mk_conj [empty, Field, prefCl, tree, undef] + HOLogic.mk_conj (empty, tree) end; val carT_binds = mk_internal_bs carTN; @@ -1164,7 +1157,6 @@ thm OF [set_sbd, sbd_Card_order]) o drop m) set_sbdss; val to_sbd_inj_thmss = mk_to_sbd_thmss @{thm toCard_inj}; - val to_sbd_thmss = mk_to_sbd_thmss @{thm toCard}; val from_to_sbd_thmss = mk_to_sbd_thmss @{thm fromCard_toCard}; val Lev_bind = mk_internal_b LevN; @@ -1273,10 +1265,8 @@ Term.absfree k' (mk_InN bdFTs (Term.list_comb (to_sbd_map, passive_ids @ map (mk_to_sbd s k i) ks) $ (s $ k)) i); - val Lab = Term.absfree kl' (mk_If - (HOLogic.mk_mem (kl, mk_Lev ss (mk_size kl) i $ z)) - (mk_case_sumN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z)) - (mk_undefined sbdFT)); + val Lab = Term.absfree kl' + (mk_case_sumN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z)); val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT) (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab); @@ -1305,24 +1295,6 @@ Term.list_comb (Const (nth behs (i - 1), behT), ss) end; - val Lev_sbd_thms = - let - fun mk_conjunct i z = mk_leq (mk_Lev ss nat i $ z) (mk_Field (mk_clists sum_sbd)); - val goal = list_all_free zs - (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); - - val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; - - val Lev_sbd = singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) - (K (mk_Lev_sbd_tac lthy cts Lev_0s Lev_Sucs to_sbd_thmss)) - |> Thm.close_derivation); - - val Lev_sbd' = mk_specN n Lev_sbd; - in - map (fn i => Lev_sbd' RS mk_conjunctN n i) ks - end; - val (length_Lev_thms, length_Lev'_thms) = let fun mk_conjunct i z = HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), @@ -1352,26 +1324,6 @@ (length_Levs, length_Levs') end; - val prefCl_Lev_thms = - let - fun mk_conjunct i z = HOLogic.mk_imp - (HOLogic.mk_conj (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z), mk_prefixeq kl_copy kl), - HOLogic.mk_mem (kl_copy, mk_Lev ss (mk_size kl_copy) i $ z)); - val goal = list_all_free (kl :: kl_copy :: zs) - (Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct ks zs)); - - val cts = map (SOME o certify lthy) [Term.absfree nat' goal, nat]; - - val prefCl_Lev = singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal) - (K (mk_prefCl_Lev_tac lthy cts Lev_0s Lev_Sucs))) - |> Thm.close_derivation; - - val prefCl_Lev' = mk_specN (n + 2) prefCl_Lev; - in - map (fn i => prefCl_Lev' RS mk_conjunctN n i RS mp) ks - end; - val rv_last_thmss = let fun mk_conjunct i z i' z_copy = list_exists_free [z_copy] @@ -1479,9 +1431,9 @@ (mk_mor active_UNIVs ss carTAs strTAs (map (mk_beh ss) ks)))) (fn {context = ctxt, prems = _} => mk_mor_beh_tac ctxt m mor_def mor_cong_thm beh_defs carT_defs strT_defs isNode_defs - to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbd_thms - length_Lev_thms length_Lev'_thms prefCl_Lev_thms rv_last_thmss set_Lev_thmsss - set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s map_arg_cong_thms) + to_sbd_inj_thmss from_to_sbd_thmss Lev_0s Lev_Sucs rv_Nils rv_Conss + length_Lev_thms length_Lev'_thms rv_last_thmss set_Lev_thmsss + set_image_Lev_thmsss set_mapss map_comp_id_thms map_cong0s) |> Thm.close_derivation; val timer = time (timer "Behavioral morphism"); diff -r 315dd5920114 -r a6c2379078c8 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Wed Feb 19 08:34:34 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Wed Feb 19 09:50:50 2014 +0100 @@ -9,8 +9,6 @@ signature BNF_GFP_TACTICS = sig - val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list list -> - tactic val mk_bis_Gr_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm list -> tactic val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic @@ -54,8 +52,8 @@ val mk_mor_UNIV_tac: thm list -> thm -> tactic val mk_mor_beh_tac: Proof.context -> int -> thm -> thm -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> - thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> - thm list list list -> thm list list -> thm list -> thm list -> thm list -> tactic + thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> + thm list list -> thm list -> thm list -> tactic val mk_mor_case_sum_tac: 'a list -> thm -> tactic val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic val mk_mor_elim_tac: thm -> tactic @@ -65,7 +63,6 @@ val mk_mor_str_tac: 'a list -> thm -> tactic val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> tactic - val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> thm list -> thm -> thm list -> tactic val mk_rel_coinduct_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list -> @@ -372,9 +369,7 @@ rtac conjI, rtac conjI, etac @{thm empty_Shift}, dtac set_rev_mp, etac equalityD1, etac CollectD, - rtac conjI, etac @{thm Shift_clists}, - rtac conjI, etac @{thm Shift_prefCl}, - rtac conjI, rtac ballI, + 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}, @@ -387,8 +382,6 @@ 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, - rtac allI, rtac impI, REPEAT_DETERM o eresolve_tac [allE, impE], - etac @{thm not_in_Shift}, rtac trans, rtac (@{thm shift_def} RS fun_cong), atac, dtac bspec, atac, dtac conjunct2, dtac (mk_conjunctN n i), dtac bspec, etac @{thm set_mp[OF equalityD1]}, atac, REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, @@ -403,28 +396,6 @@ CONJ_WRAP' coalg_tac (ks ~~ (map (drop m) set_map0ss ~~ strT_defs)) 1 end; -fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss = - let - val n = length Lev_0s; - val ks = 1 upto n; - in - EVERY' [rtac (Drule.instantiate' [] cts nat_induct), - REPEAT_DETERM o rtac allI, - CONJ_WRAP' (fn Lev_0 => - EVERY' (map rtac [ord_eq_le_trans, Lev_0, @{thm Nil_clists}])) Lev_0s, - REPEAT_DETERM o rtac allI, - CONJ_WRAP' (fn (Lev_Suc, to_sbds) => - EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc, - CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) - (fn (i, to_sbd) => EVERY' [rtac subsetI, - REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt, - rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd, - etac set_rev_mp, REPEAT_DETERM o etac allE, - etac (mk_conjunctN n i)]) - (rev (ks ~~ to_sbds))]) - (Lev_Sucs ~~ to_sbdss)] 1 - end; - fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs = let val n = length Lev_0s; @@ -449,37 +420,6 @@ fun mk_length_Lev'_tac length_Lev = EVERY' [ftac length_Lev, etac ssubst, atac] 1; -fun mk_prefCl_Lev_tac ctxt cts Lev_0s Lev_Sucs = - let - val n = length Lev_0s; - val ks = n downto 1; - in - EVERY' [rtac (Drule.instantiate' [] cts nat_induct), - REPEAT_DETERM o rtac allI, - CONJ_WRAP' (fn Lev_0 => - EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp), - etac @{thm singletonE}, hyp_subst_tac ctxt, - dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]}, - hyp_subst_tac ctxt, - rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]}, - rtac Lev_0, rtac @{thm singletonI}]) Lev_0s, - REPEAT_DETERM o rtac allI, - CONJ_WRAP' (fn (Lev_0, Lev_Suc) => - EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp), - CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) - (fn i => - EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt, - dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac ctxt, - rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]}, - rtac Lev_0, rtac @{thm singletonI}, - REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, - rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]}, - rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, - rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), - etac mp, etac conjI, atac]) ks]) - (Lev_0s ~~ Lev_Sucs)] 1 - end; - fun mk_rv_last_tac cTs cts rv_Nils rv_Conss = let val n = length rv_Nils; @@ -610,37 +550,28 @@ ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ to_sbd_injss))] 1 end; -fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs - to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's - prefCl_Levs rv_lastss set_Levsss set_image_Levsss set_map0ss - map_comp_ids map_cong0s map_arg_congs = +fun mk_mor_beh_tac ctxt m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs to_sbd_injss + from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss length_Levs length_Lev's rv_lastss set_Levsss + set_image_Levsss set_map0ss map_comp_ids map_cong0s = let val n = length beh_defs; val ks = 1 upto n; - fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd, - ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_map0s, - (set_Levss, set_image_Levss))))))))))) = + fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, ((length_Lev, length_Lev'), + (rv_lasts, (set_map0s, (set_Levss, set_image_Levss))))))))) = EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI, rtac conjI, rtac @{thm UN_I}, rtac UNIV_I, rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, - rtac conjI, - rtac @{thm UN_least}, rtac Lev_sbd, - rtac conjI, - rtac @{thm prefCl_UN}, rtac ssubst, rtac @{thm PrefCl_def}, REPEAT_DETERM o rtac allI, - rtac impI, etac conjE, rtac exI, rtac conjI, rtac @{thm ord_le_eq_trans}, - etac @{thm prefixeq_length_le}, etac length_Lev, rtac prefCl_Lev, etac conjI, atac, - rtac conjI, + (**) 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 @{thm if_P} THEN' etac length_Lev' - else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN' - etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)), + 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, @@ -657,9 +588,8 @@ REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}], rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS ssubst), rtac exI, rtac conjI, - (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev' - else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN' - etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i)), + 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, @@ -673,12 +603,8 @@ (drop m set_map0s ~~ (set_Levs ~~ set_image_Levs))]) (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_map0ss ~~ (set_Levss ~~ set_image_Levss))))), - (**) - rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI, - etac notE, etac @{thm UN_I[OF UNIV_I]}, (*root isNode*) - rtac (isNode_def RS ssubst), rtac exI, rtac conjI, rtac (@{thm if_P} RS trans), - rtac length_Lev', rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, + rtac (isNode_def RS ssubst), rtac exI, rtac conjI, CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), if n = 1 then rtac refl else rtac (mk_sum_caseN n i), @@ -695,12 +621,9 @@ rtac rv_Nil]) (drop m set_map0s ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))]; - fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)), - ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) = + fun mor_tac (i, (strT_def, ((Lev_Suc, (rv_Nil, rv_Cons)), + ((map_comp_id, map_cong0), (length_Lev', (from_to_sbds, to_sbd_injs)))))) = EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def, - rtac (@{thm if_P} RS (if n = 1 then map_arg_cong else sum_weak_case_cong) RS trans), - rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp), - rtac Lev_0, rtac @{thm singletonI}, CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt), if n = 1 then K all_tac @@ -726,37 +649,22 @@ rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac, rtac trans, rtac @{thm shift_def}, rtac ssubst, rtac @{thm fun_eq_iff}, rtac allI, - rtac @{thm if_cong}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac iffI, - dtac asm_rl, dtac asm_rl, dtac asm_rl, - dtac (Lev_Suc RS equalityD1 RS set_mp), - CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE)) (fn i'' => - EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], - dtac list_inject_iffD1, etac conjE, - if i' = i'' then EVERY' [dtac (mk_InN_inject n i'), - dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)), - atac, atac, hyp_subst_tac ctxt, atac] - else etac (mk_InN_not_InM i' i'' RS notE)]) - (rev ks), - rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI, - REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, etac conjI, atac, CONVERSION (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt), if n = 1 then K all_tac else rtac sum_weak_case_cong THEN' rtac (mk_sum_caseN n i' RS trans), - SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl, - rtac refl]) + SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl]) ks to_sbd_injs from_to_sbds)]; in (rtac mor_cong THEN' EVERY' (map (fn thm => rtac (thm RS ext)) beh_defs) THEN' stac mor_def THEN' rtac conjI THEN' CONJ_WRAP' fbetw_tac - (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~ - ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~ - (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))))) THEN' + (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ ((length_Levs ~~ length_Lev's) ~~ + (rv_lastss ~~ (set_map0ss ~~ (set_Levsss ~~ set_image_Levsss))))))))) THEN' CONJ_WRAP' mor_tac - (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~ - ((map_comp_ids ~~ (map_cong0s ~~ map_arg_congs)) ~~ + (ks ~~ (strT_defs ~~ ((Lev_Sucs ~~ (rv_Nils ~~ rv_Conss)) ~~ + ((map_comp_ids ~~ map_cong0s) ~~ (length_Lev's ~~ (from_to_sbdss ~~ to_sbd_injss))))))) 1 end;