# HG changeset patch # User traytel # Date 1373891031 -7200 # Node ID 58b87aa4dc3bc47a050c879f7c49d91d0fd5642e # Parent 1e7896c7f781f6649d7b44e0d30e5633e4a4dbb9 eliminate duplicated theorems (thanks to "Auto solve_direct" in jEdit) diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/BNF_Def.thy --- a/src/HOL/BNF/BNF_Def.thy Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/BNF_Def.thy Mon Jul 15 14:23:51 2013 +0200 @@ -171,9 +171,6 @@ lemma flip_pred: "A \ Collect (split (R ^--1)) \ (%(x, y). (y, x)) ` A \ Collect (split R)" by auto -lemma pointfreeE: "f o g = f' o g' \ f (g x) = f' (g' x)" -unfolding o_def fun_eq_iff by simp - lemma Collect_split_mono: "A \ B \ Collect (split A) \ Collect (split B)" by auto diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/BNF_FP_Basic.thy --- a/src/HOL/BNF/BNF_FP_Basic.thy Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/BNF_FP_Basic.thy Mon Jul 15 14:23:51 2013 +0200 @@ -35,18 +35,6 @@ lemma prod_all_impI_step: "(\x. \y. P (x, y) \ Q (x, y)) \ \x. P x \ Q x" by auto -lemma all_unit_eq: "(\x. PROP P x) \ PROP P ()" -by simp - -lemma all_prod_eq: "(\x. PROP P x) \ (\a b. PROP P (a, b))" -by clarsimp - -lemma rev_bspec: "a \ A \ \z \ A. P z \ P a" -by simp - -lemma Un_cong: "\A = B; C = D\ \ A \ C = B \ D" -by simp - lemma pointfree_idE: "f \ g = id \ f (g x) = x" unfolding o_def fun_eq_iff by simp diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Mon Jul 15 14:23:51 2013 +0200 @@ -247,11 +247,6 @@ lemma cpow_clists_czero: "\A \ Field (cpow (clists r)) - {{}}; |A| =o czero\ \ False" unfolding cpow_def clists_def card_of_ordIso_czero_iff_empty by auto -lemma incl_UNION_I: -assumes "i \ I" and "A \ F i" -shows "A \ UNION I F" -using assms by auto - lemma Nil_clists: "{[]} \ Field (clists r)" unfolding clists_def Field_card_of by auto diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/Countable_Type.thy --- a/src/HOL/BNF/Countable_Type.thy Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Countable_Type.thy Mon Jul 15 14:23:51 2013 +0200 @@ -92,10 +92,6 @@ "countable (rcset C)" using Rep_cset by simp -lemma rcset_inj[simp]: -"rcset C = rcset D \ C = D" -by (metis acset_rcset) - lemma rcset_surj: assumes "countable A" shows "\ C. rcset C = A" diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/More_BNFs.thy Mon Jul 15 14:23:51 2013 +0200 @@ -297,7 +297,7 @@ lemma rcset_to_rcset: "countable A \ rcset (the_inv rcset A) = A" apply (rule f_the_inv_into_f) -unfolding inj_on_def rcset_inj using rcset_surj by auto +unfolding inj_on_def Rep_cset_inject using rcset_surj by auto lemma Collect_Int_Times: "{(x, y). R x y} \ A \ B = {(x, y). R x y \ x \ A \ y \ B}" diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/Tools/bnf_comp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Mon Jul 15 14:23:51 2013 +0200 @@ -78,7 +78,7 @@ [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply, rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply, rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans), - rtac @{thm trans[OF pointfreeE[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, + rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union, rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]}, rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @ [REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]}, diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Mon Jul 15 14:23:51 2013 +0200 @@ -45,7 +45,7 @@ fun mk_map_cong_tac ctxt cong0 = (hyp_subst_tac ctxt THEN' rtac cong0 THEN' REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1; -fun mk_set_map' set_map = set_map RS @{thm pointfreeE}; +fun mk_set_map' set_map = set_map RS @{thm comp_eq_dest}; fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1 else (rtac subsetI THEN' rtac CollectI) 1 THEN diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Jul 15 14:23:51 2013 +0200 @@ -1174,7 +1174,7 @@ end; val sumEN_thm' = - unfold_thms lthy @{thms all_unit_eq} + unfold_thms lthy @{thms unit_all_eq1} (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) [] (mk_sumEN_balanced n)) |> Morphism.thm phi; diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Jul 15 14:23:51 2013 +0200 @@ -78,7 +78,7 @@ fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' = unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN - unfold_thms_tac ctxt @{thms all_prod_eq} THEN + unfold_thms_tac ctxt @{thms split_paired_all} THEN HEADGOAL (EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac meta_spec, etac meta_mp, atac]) (1 upto n))); diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Mon Jul 15 14:23:51 2013 +0200 @@ -2219,7 +2219,7 @@ |> Thm.close_derivation) goals cTs dtor_unfold_thms map_comp's map_cong0s; in - map_split (fn thm => (thm RS @{thm pointfreeE}, thm)) maps + map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps end; val map_comp_thms = diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Mon Jul 15 14:23:51 2013 +0200 @@ -140,12 +140,14 @@ val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym; val sum_case_weak_cong = @{thm sum_case_weak_cong}; val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]}; -val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]} +val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]}; +val rev_bspec = Drule.rotate_prems 1 bspec; +val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \"]} fun mk_coalg_set_tac coalg_def = dtac (coalg_def RS iffD1) 1 THEN REPEAT_DETERM (etac conjE 1) THEN - EVERY' [dtac @{thm rev_bspec}, atac] 1 THEN + EVERY' [dtac rev_bspec, atac] 1 THEN REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN atac 1; fun mk_mor_elim_tac mor_def = @@ -183,7 +185,7 @@ EVERY' [rtac iffI, CONJ_WRAP' mor_tac morEs, stac mor_def, rtac conjI, CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) morEs, CONJ_WRAP' (fn i => - EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm pointfreeE}]) (1 upto n)] 1 + EVERY' [dtac (mk_conjunctN n i), rtac ballI, etac @{thm comp_eq_dest}]) (1 upto n)] 1 end; fun mk_mor_str_tac ks mor_UNIV = @@ -194,7 +196,7 @@ fun mk_set_incl_hset_tac def rec_Suc = EVERY' (stac def :: - map rtac [@{thm incl_UNION_I}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, + map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym, rec_Suc]) 1; fun mk_set_hset_incl_hset_tac n defs rec_Suc i = @@ -238,10 +240,10 @@ (fn (rec_Suc, (morE, ((passive_set_maps, active_set_maps), coalg_sets))) => EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym), if m = 0 then K all_tac - else EVERY' [rtac @{thm Un_cong}, rtac box_equals, + else EVERY' [rtac Un_cong, rtac box_equals, rtac (nth passive_set_maps (j - 1) RS sym), rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac], - CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong})) + CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong)) (fn (i, (set_map, coalg_set)) => EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})), etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map, @@ -360,7 +362,7 @@ EVERY' [rtac allI, rtac allI, rtac impI, etac @{thm UN_E}, dtac bspec, atac, dtac conjunct2, dtac (mk_conjunctN n i), etac allE, etac allE, dtac mp, atac, etac bexE, rtac bexI, atac, rtac in_mono, - REPEAT_DETERM_N n o etac @{thm incl_UNION_I[OF _ subset_refl]}, + REPEAT_DETERM_N n o etac @{thm SUP_upper2[OF _ subset_refl]}, atac]) (ks ~~ in_monos)] 1 end; @@ -374,7 +376,7 @@ end; fun mk_incl_lsbis_tac n i lsbis_def = - EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm incl_UNION_I}, rtac CollectI, + EVERY' [rtac @{thm xt1(3)}, rtac lsbis_def, rtac @{thm SUP_upper2}, rtac CollectI, REPEAT_DETERM_N n o rtac exI, rtac conjI, rtac refl, atac, rtac equalityD2, rtac (mk_nth_conv n i)] 1; @@ -1122,8 +1124,8 @@ CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY' [SELECT_GOAL (unfold_thms_tac ctxt (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})), - rtac @{thm Un_cong}, rtac refl, - CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong})) + rtac Un_cong, rtac refl, + CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong)) (fn i => EVERY' [rtac @{thm UN_cong[OF refl]}, REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)]) (rec_Sucs ~~ (dtor_maps ~~ set_mapss))] 1 diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Mon Jul 15 14:23:51 2013 +0200 @@ -1451,7 +1451,7 @@ |> Thm.close_derivation) goals ctor_fold_thms map_comp_id_thms map_cong0s; in - map (fn thm => thm RS @{thm pointfreeE}) maps + map (fn thm => thm RS @{thm comp_eq_dest}) maps end; val (ctor_map_unique_thms, ctor_map_unique_thm) = diff -r 1e7896c7f781 -r 58b87aa4dc3b src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Mon Jul 15 11:29:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Mon Jul 15 14:23:51 2013 +0200 @@ -87,6 +87,8 @@ val ord_eq_le_trans = @{thm ord_eq_le_trans}; val subset_trans = @{thm subset_trans}; val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]}; +val rev_bspec = Drule.rotate_prems 1 bspec; +val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \"]} fun mk_alg_set_tac alg_def = dtac (alg_def RS iffD1) 1 THEN @@ -123,7 +125,7 @@ val fbetw_tac = EVERY' [rtac ballI, stac o_apply, etac bspec, etac bspec, atac]; fun mor_tac (set_map', map_comp_id) = EVERY' [rtac ballI, stac o_apply, rtac trans, - rtac trans, dtac @{thm rev_bspec}, atac, etac arg_cong, + rtac trans, dtac rev_bspec, atac, etac arg_cong, REPEAT o eresolve_tac [CollectE, conjE], etac bspec, rtac CollectI] THEN' CONJ_WRAP' (fn thm => FIRST' [rtac subset_UNIV, @@ -147,7 +149,7 @@ (EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans, etac @{thm image_mono}, atac])]) set_map'; fun mor_tac (set_map', ((morE, map_comp_id), map_cong0L)) = - EVERY' [rtac ballI, ftac @{thm rev_bspec}, atac, + EVERY' [rtac ballI, ftac rev_bspec, atac, REPEAT o eresolve_tac [CollectE, conjE], rtac sym, rtac trans, rtac sym, etac @{thm inverE}, etac bspec, rtac CollectI, Collect_tac set_map', rtac trans, etac (morE RS arg_cong), rtac CollectI, Collect_tac set_map', @@ -270,7 +272,7 @@ let val minG_tac = EVERY' [rtac @{thm UN_cong}, rtac refl, dtac bspec, atac, etac arg_cong]; fun minH_tac thm = - EVERY' [rtac @{thm Un_cong}, minG_tac, rtac @{thm image_cong}, rtac thm, + EVERY' [rtac Un_cong, minG_tac, rtac @{thm image_cong}, rtac thm, REPEAT_DETERM_N (length in_congs) o minG_tac, rtac refl]; in (rtac (worel RS (@{thm wo_rel.worec_fixpoint} RS fun_cong)) THEN' rtac ssubst THEN' @@ -391,7 +393,7 @@ let val n = length alg_sets; val fbetw_tac = - CONJ_WRAP' (K (EVERY' [rtac ballI, etac @{thm rev_bspec}, etac CollectE, atac])) alg_sets; + CONJ_WRAP' (K (EVERY' [rtac ballI, etac rev_bspec, etac CollectE, atac])) alg_sets; val mor_tac = CONJ_WRAP' (fn thm => EVERY' [rtac ballI, rtac thm]) str_init_defs; fun alg_epi_tac ((alg_set, str_init_def), set_map') = @@ -583,7 +585,7 @@ fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_cong0s = let val n = length map_cong0s; - fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm pointfreeE}, + fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm comp_eq_dest}, rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong), rtac (cong RS arg_cong), REPEAT_DETERM_N m o rtac refl, @@ -603,9 +605,9 @@ fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN' rtac @{thm Union_image_eq}; in - EVERY' [rtac (set RS @{thm pointfreeE} RS trans), rtac @{thm Un_cong}, + EVERY' [rtac (set RS @{thm comp_eq_dest} RS trans), rtac Un_cong, rtac (trans OF [set_map', trans_fun_cong_image_id_id_apply]), - REPEAT_DETERM_N (n - 1) o rtac @{thm Un_cong}, + REPEAT_DETERM_N (n - 1) o rtac Un_cong, EVERY' (map mk_UN set_map's)] 1 end; @@ -621,9 +623,9 @@ fun mk_set_nat cset ctor_map ctor_set set_nats = EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl, rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, ctor_set RS trans]), - rtac sym, EVERY' (map rtac (trans :: @{thms image_Un Un_cong})), + rtac sym, EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]), rtac sym, rtac (nth set_nats (i - 1)), - REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})), + REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]), EVERY' (map useIH (drop m set_nats))]; in (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_map'ss)) 1