# HG changeset patch # User blanchet # Date 1380724180 -7200 # Node ID 732b53d9b7206381c69038e15c4b9bb8315427fc # Parent 4edfd0fd55369eab9ec2303bd41feacc54218dea don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded diff -r 4edfd0fd5536 -r 732b53d9b720 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Oct 02 15:53:20 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Oct 02 16:29:40 2013 +0200 @@ -53,7 +53,7 @@ type gfp_sugar_thms = ((thm list * thm) list * Args.src list) * (thm list list * thm list list * Args.src list) - * (thm list list * thm list list) * (thm list list * thm list list * Args.src list) + * (thm list list * thm list list * Args.src list) * (thm list list * thm list list * Args.src list) * (thm list list list * thm list list list * Args.src list) @@ -397,7 +397,7 @@ type gfp_sugar_thms = ((thm list * thm) list * Args.src list) * (thm list list * thm list list * Args.src list) - * (thm list list * thm list list) * (thm list list * thm list list * Args.src list) + * (thm list list * thm list list * Args.src list) * (thm list list * thm list list * Args.src list) * (thm list list list * thm list list list * Args.src list); @@ -908,7 +908,7 @@ val fcoiterss' as [gunfolds, hcorecs] = map2 (fn (pfss, _) => map (lists_bmoc pfss)) (map fst coiters_args_types) coiterss'; - val (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) = + val (unfold_thmss, corec_thmss) = let fun mk_goal pfss c cps fcoiter n k ctr m cfs' = fold_rev (fold_rev Logic.all) ([c] :: pfss) @@ -956,18 +956,8 @@ val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss |> map (map (unfold_thms lthy @{thms sum_case_if})); - - val unfold_safesss = map2 (map2 (map2 (curry op =))) crgsss' crgsss; - val corec_safesss = map2 (map2 (map2 (curry op =))) cshsss' cshsss; - - val filter_safesss = - map2 (map_filter (fn (safes, thm) => if forall I safes then SOME thm else NONE) oo - curry (op ~~)); - - val safe_unfold_thmss = filter_safesss unfold_safesss unfold_thmss; - val safe_corec_thmss = filter_safesss corec_safesss corec_thmss; in - (unfold_thmss, corec_thmss, safe_unfold_thmss, safe_corec_thmss) + (unfold_thmss, corec_thmss) end; val (disc_unfold_iff_thmss, disc_corec_iff_thmss) = @@ -1035,7 +1025,6 @@ in ((coinduct_thms_pairs, coinduct_case_attrs), (unfold_thmss, corec_thmss, code_nitpick_simp_attrs), - (safe_unfold_thmss, safe_corec_thmss), (disc_unfold_thmss, disc_corec_thmss, []), (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs), (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs)) @@ -1464,7 +1453,6 @@ val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)], coinduct_attrs), (unfold_thmss, corec_thmss, coiter_attrs), - (safe_unfold_thmss, safe_corec_thmss), (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs), (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs), (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) = @@ -1477,21 +1465,14 @@ val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; - fun flat_coiter_thms coiters disc_coiters disc_coiter_iffs sel_coiters = - coiters @ disc_coiters @ disc_coiter_iffs @ sel_coiters; + val flat_coiter_thms = append oo append; val simp_thmss = map7 mk_simp_thms ctr_sugars - (map4 flat_coiter_thms safe_unfold_thmss disc_unfold_thmss disc_unfold_iff_thmss - sel_unfold_thmss) - (map4 flat_coiter_thms safe_corec_thmss disc_corec_thmss disc_corec_iff_thmss - sel_corec_thmss) + (map3 flat_coiter_thms disc_unfold_thmss disc_unfold_iff_thmss sel_unfold_thmss) + (map3 flat_coiter_thms disc_corec_thmss disc_corec_iff_thmss sel_corec_thmss) mapss rel_injects rel_distincts setss; - val anonymous_notes = - [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)] - |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); - val common_notes = (if nn > 1 then [(coinductN, [coinduct_thm], coinduct_attrs), @@ -1521,7 +1502,7 @@ |> Generic_Target.theory_declaration; in lthy - |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd + |> Local_Theory.notes (common_notes @ notes) |> snd |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm] (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss]) diff -r 4edfd0fd5536 -r 732b53d9b720 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Oct 02 15:53:20 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Oct 02 16:29:40 2013 +0200 @@ -157,7 +157,7 @@ derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy - |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, + |> `(fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), (disc_unfold_thmss, disc_corec_thmss, _), _, (sel_unfold_thmsss, sel_corec_thmsss, _)) => (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss, diff -r 4edfd0fd5536 -r 732b53d9b720 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Oct 02 15:53:20 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Oct 02 16:29:40 2013 +0200 @@ -918,20 +918,10 @@ val ctr_thmss = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss (map #ctr_specs corec_specs); - val safess = map (map (not o exists_subterm (member (op =) (map SOME fun_names) o - try (fst o dest_Free)) o snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o - Logic.strip_imp_concl o drop_All o prop_of)) ctr_thmss; - val safe_ctr_thmss = map (map snd o filter fst o (op ~~)) (safess ~~ ctr_thmss); - - val simp_thmss = - map3 (fn x => fn y => fn z => x @ y @ z) disc_thmss sel_thmss safe_ctr_thmss; + val simp_thmss = map2 append disc_thmss sel_thmss val common_name = mk_common_name fun_names; - val anonymous_notes = - [(flat safe_ctr_thmss, simp_attrs)] - |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); - val notes = [(coinductN, map (if n2m then single else K []) coinduct_thms, []), (codeN, ctr_thmss(*FIXME*), code_nitpick_attrs), @@ -953,7 +943,7 @@ |> map (fn (thmN, thms, attrs) => ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])])); in - lthy |> Local_Theory.notes (anonymous_notes @ notes @ common_notes) |> snd + lthy |> Local_Theory.notes (notes @ common_notes) |> snd end; fun after_qed thmss' = fold_map Local_Theory.define defs #-> prove thmss';