# HG changeset patch # User blanchet # Date 1348404773 -7200 # Node ID c90818b635994df85aee51c6d98bb56e3712578e # Parent fe1deee434b687f44924316ee87eb8cb8927c295 simplified fact policies diff -r fe1deee434b6 -r c90818b63599 src/HOL/BNF/Tools/bnf_comp.ML --- a/src/HOL/BNF/Tools/bnf_comp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_comp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -270,7 +270,7 @@ (maps wit_thms_of_bnf inners); val (bnf', lthy') = - bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss)) + bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) (((((b, mapx), sets), bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) @@ -368,7 +368,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds)) + bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) @@ -452,7 +452,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) + bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; in @@ -529,7 +529,7 @@ fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf); val (bnf', lthy') = - bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds) + bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) @@ -671,9 +671,7 @@ fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf)); - val policy = user_policy Derive_All_Facts; - - val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads) + val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads) (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy; in ((bnf', deads), lthy') diff -r fe1deee434b6 -r c90818b63599 src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Sun Sep 23 14:52:53 2012 +0200 @@ -82,8 +82,8 @@ val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline - datatype fact_policy = - Derive_Few_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms + datatype fact_policy = Dont_Note | Note_Some | Note_All + val bnf_note_all: bool Config.T val user_policy: fact_policy -> Proof.context -> fact_policy @@ -516,13 +516,11 @@ datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline; -datatype fact_policy = - Derive_Few_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms; +datatype fact_policy = Dont_Note | Note_Some | Note_All; val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false); -fun user_policy policy ctxt = - if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else policy; +fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy; val smart_max_inline_size = 25; (*FUDGE*) @@ -559,7 +557,7 @@ fun maybe_define user_specified (b, rhs) lthy = let val inline = - (user_specified orelse fact_policy = Derive_Few_Facts) andalso + (user_specified orelse fact_policy = Dont_Note) andalso (case const_policy of Dont_Inline => false | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs @@ -904,8 +902,6 @@ val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order]; val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero}; - fun mk_lazy f = if fact_policy <> Derive_Few_Facts then Lazy.value (f ()) else Lazy.lazy f; - fun mk_collect_set_natural () = let val defT = mk_bnf_T Ts CA --> HOLogic.mk_setT T; @@ -923,7 +919,7 @@ |> Thm.close_derivation end; - val collect_set_natural = mk_lazy mk_collect_set_natural; + val collect_set_natural = Lazy.lazy mk_collect_set_natural; fun mk_in_mono () = let @@ -937,7 +933,7 @@ |> Thm.close_derivation end; - val in_mono = mk_lazy mk_in_mono; + val in_mono = Lazy.lazy mk_in_mono; fun mk_in_cong () = let @@ -951,13 +947,13 @@ |> Thm.close_derivation end; - val in_cong = mk_lazy mk_in_cong; + val in_cong = Lazy.lazy mk_in_cong; - val map_id' = mk_lazy (fn () => mk_id' (#map_id axioms)); - val map_comp' = mk_lazy (fn () => mk_comp' (#map_comp axioms)); + val map_id' = Lazy.lazy (fn () => mk_id' (#map_id axioms)); + val map_comp' = Lazy.lazy (fn () => mk_comp' (#map_comp axioms)); val set_natural' = - map (fn thm => mk_lazy (fn () => mk_set_natural' thm)) (#set_natural axioms); + map (fn thm => Lazy.lazy (fn () => mk_set_natural' thm)) (#set_natural axioms); fun mk_map_wppull () = let @@ -997,7 +993,7 @@ val srel_O_Grs = no_refl [#srel_O_Gr axioms]; - val map_wppull = mk_lazy mk_map_wppull; + val map_wppull = Lazy.lazy mk_map_wppull; fun mk_srel_Gr () = let @@ -1011,7 +1007,7 @@ |> Thm.close_derivation end; - val srel_Gr = mk_lazy mk_srel_Gr; + val srel_Gr = Lazy.lazy mk_srel_Gr; fun mk_srel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy fun mk_srel_concl f = HOLogic.mk_Trueprop @@ -1039,8 +1035,8 @@ |> Thm.close_derivation end; - val srel_mono = mk_lazy mk_srel_mono; - val srel_cong = mk_lazy mk_srel_cong; + val srel_mono = Lazy.lazy mk_srel_mono; + val srel_cong = Lazy.lazy mk_srel_cong; fun mk_srel_Id () = let val srelAsAs = mk_bnf_srel self_setRTs CA' CA' in @@ -1051,7 +1047,7 @@ |> Thm.close_derivation end; - val srel_Id = mk_lazy mk_srel_Id; + val srel_Id = Lazy.lazy mk_srel_Id; fun mk_srel_converse () = let @@ -1069,7 +1065,7 @@ |> Thm.close_derivation end; - val srel_converse = mk_lazy mk_srel_converse; + val srel_converse = Lazy.lazy mk_srel_converse; fun mk_srel_O () = let @@ -1085,7 +1081,7 @@ |> Thm.close_derivation end; - val srel_O = mk_lazy mk_srel_O; + val srel_O = Lazy.lazy mk_srel_O; fun mk_in_srel () = let @@ -1105,7 +1101,7 @@ |> Thm.close_derivation end; - val in_srel = mk_lazy mk_in_srel; + val in_srel = Lazy.lazy mk_in_srel; val eqset_imp_iff_pair = @{thm eqset_imp_iff_pair}; val mem_Collect_etc = @{thms mem_Collect_eq fst_conv snd_conv prod.cases}; @@ -1116,7 +1112,7 @@ RS eqset_imp_iff_pair RS sym) |> Drule.zero_var_indexes; - val rel_as_srel = mk_lazy mk_rel_as_srel; + val rel_as_srel = Lazy.lazy mk_rel_as_srel; fun mk_rel_flip () = let @@ -1130,7 +1126,7 @@ |> Drule.zero_var_indexes |> Thm.generalize ([], map fst Qs') 1 end; - val rel_flip = mk_lazy mk_rel_flip; + val rel_flip = Lazy.lazy mk_rel_flip; val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def; @@ -1149,7 +1145,7 @@ wits bnf_rel bnf_srel; in (bnf, lthy - |> (if fact_policy = Note_All_Facts_and_Axioms then + |> (if fact_policy = Note_All then let val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits); val notes = @@ -1176,8 +1172,7 @@ end else I) - |> (if fact_policy = Note_All_Facts_and_Axioms orelse - fact_policy = Derive_All_Facts_Note_Most then + |> (if fact_policy <> Dont_Note then let val notes = [(map_comp'N, [Lazy.force (#map_comp' facts)]), @@ -1241,7 +1236,7 @@ Proof.unfolding ([[(defs, [])]]) (Proof.theorem NONE (snd o register_bnf key oo after_qed) (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo - prepare_def Do_Inline (user_policy Derive_All_Facts_Note_Most) I Syntax.read_term NONE; + prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE; fun print_bnfs ctxt = let diff -r fe1deee434b6 -r c90818b63599 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -2859,11 +2859,9 @@ val wit_tac = mk_wit_tac n dtor_ctor_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); - val policy = user_policy Derive_All_Facts_Note_Most; - val (Jbnfs, lthy) = fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn (thms, wits) => fn lthy => - bnf_def Dont_Inline policy I tacs (wit_tac thms) (SOME deads) + bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy |> register_bnf (Local_Theory.full_name lthy b)) tacss bs fs_maps setss_by_bnf Ts all_witss lthy; diff -r fe1deee434b6 -r c90818b63599 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Sun Sep 23 14:52:53 2012 +0200 @@ -1703,11 +1703,9 @@ fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs); - val policy = user_policy Derive_All_Facts_Note_Most; - val (Ibnfs, lthy) = fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn wits => fn lthy => - bnf_def Dont_Inline policy I tacs wit_tac (SOME deads) + bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads) (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy |> register_bnf (Local_Theory.full_name lthy b)) tacss bs fs_maps setss_by_bnf Ts ctor_witss lthy;