simplified fact policies
authorblanchet
Sun Sep 23 14:52:53 2012 +0200 (2012-09-23)
changeset 49538c90818b63599
parent 49537 fe1deee434b6
child 49539 be6cbf960aa7
simplified fact policies
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_lfp.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Sun Sep 23 14:52:53 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Sun Sep 23 14:52:53 2012 +0200
     1.3 @@ -270,7 +270,7 @@
     1.4          (maps wit_thms_of_bnf inners);
     1.5  
     1.6      val (bnf', lthy') =
     1.7 -      bnf_def const_policy (K Derive_Few_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
     1.8 +      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss))
     1.9          (((((b, mapx), sets), bd), wits), SOME rel) lthy;
    1.10    in
    1.11      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.12 @@ -368,7 +368,7 @@
    1.13      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.14  
    1.15      val (bnf', lthy') =
    1.16 -      bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
    1.17 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds))
    1.18          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.19    in
    1.20      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.21 @@ -452,7 +452,7 @@
    1.22      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.23  
    1.24      val (bnf', lthy') =
    1.25 -      bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
    1.26 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds)
    1.27          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.28  
    1.29    in
    1.30 @@ -529,7 +529,7 @@
    1.31      fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
    1.32  
    1.33      val (bnf', lthy') =
    1.34 -      bnf_def Smart_Inline (K Derive_Few_Facts) qualify tacs wit_tac (SOME Ds)
    1.35 +      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds)
    1.36          (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
    1.37    in
    1.38      (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
    1.39 @@ -671,9 +671,7 @@
    1.40  
    1.41      fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
    1.42  
    1.43 -    val policy = user_policy Derive_All_Facts;
    1.44 -
    1.45 -    val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
    1.46 +    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
    1.47        (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
    1.48    in
    1.49      ((bnf', deads), lthy')
     2.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Sun Sep 23 14:52:53 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Sun Sep 23 14:52:53 2012 +0200
     2.3 @@ -82,8 +82,8 @@
     2.4    val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
     2.5  
     2.6    datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
     2.7 -  datatype fact_policy =
     2.8 -    Derive_Few_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms
     2.9 +  datatype fact_policy = Dont_Note | Note_Some | Note_All
    2.10 +
    2.11    val bnf_note_all: bool Config.T
    2.12    val user_policy: fact_policy -> Proof.context -> fact_policy
    2.13  
    2.14 @@ -516,13 +516,11 @@
    2.15  
    2.16  datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline;
    2.17  
    2.18 -datatype fact_policy =
    2.19 -  Derive_Few_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms;
    2.20 +datatype fact_policy = Dont_Note | Note_Some | Note_All;
    2.21  
    2.22  val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
    2.23  
    2.24 -fun user_policy policy ctxt =
    2.25 -  if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else policy;
    2.26 +fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
    2.27  
    2.28  val smart_max_inline_size = 25; (*FUDGE*)
    2.29  
    2.30 @@ -559,7 +557,7 @@
    2.31      fun maybe_define user_specified (b, rhs) lthy =
    2.32        let
    2.33          val inline =
    2.34 -          (user_specified orelse fact_policy = Derive_Few_Facts) andalso
    2.35 +          (user_specified orelse fact_policy = Dont_Note) andalso
    2.36            (case const_policy of
    2.37              Dont_Inline => false
    2.38            | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
    2.39 @@ -904,8 +902,6 @@
    2.40          val bd_Cinfinite = @{thm conjI} OF [#bd_cinfinite axioms, bd_Card_order];
    2.41          val bd_Cnotzero = bd_Cinfinite RS @{thm Cinfinite_Cnotzero};
    2.42  
    2.43 -        fun mk_lazy f = if fact_policy <> Derive_Few_Facts then Lazy.value (f ()) else Lazy.lazy f;
    2.44 -
    2.45          fun mk_collect_set_natural () =
    2.46            let
    2.47              val defT = mk_bnf_T Ts CA --> HOLogic.mk_setT T;
    2.48 @@ -923,7 +919,7 @@
    2.49              |> Thm.close_derivation
    2.50            end;
    2.51  
    2.52 -        val collect_set_natural = mk_lazy mk_collect_set_natural;
    2.53 +        val collect_set_natural = Lazy.lazy mk_collect_set_natural;
    2.54  
    2.55          fun mk_in_mono () =
    2.56            let
    2.57 @@ -937,7 +933,7 @@
    2.58              |> Thm.close_derivation
    2.59            end;
    2.60  
    2.61 -        val in_mono = mk_lazy mk_in_mono;
    2.62 +        val in_mono = Lazy.lazy mk_in_mono;
    2.63  
    2.64          fun mk_in_cong () =
    2.65            let
    2.66 @@ -951,13 +947,13 @@
    2.67              |> Thm.close_derivation
    2.68            end;
    2.69  
    2.70 -        val in_cong = mk_lazy mk_in_cong;
    2.71 +        val in_cong = Lazy.lazy mk_in_cong;
    2.72  
    2.73 -        val map_id' = mk_lazy (fn () => mk_id' (#map_id axioms));
    2.74 -        val map_comp' = mk_lazy (fn () => mk_comp' (#map_comp axioms));
    2.75 +        val map_id' = Lazy.lazy (fn () => mk_id' (#map_id axioms));
    2.76 +        val map_comp' = Lazy.lazy (fn () => mk_comp' (#map_comp axioms));
    2.77  
    2.78          val set_natural' =
    2.79 -          map (fn thm => mk_lazy (fn () => mk_set_natural' thm)) (#set_natural axioms);
    2.80 +          map (fn thm => Lazy.lazy (fn () => mk_set_natural' thm)) (#set_natural axioms);
    2.81  
    2.82          fun mk_map_wppull () =
    2.83            let
    2.84 @@ -997,7 +993,7 @@
    2.85  
    2.86          val srel_O_Grs = no_refl [#srel_O_Gr axioms];
    2.87  
    2.88 -        val map_wppull = mk_lazy mk_map_wppull;
    2.89 +        val map_wppull = Lazy.lazy mk_map_wppull;
    2.90  
    2.91          fun mk_srel_Gr () =
    2.92            let
    2.93 @@ -1011,7 +1007,7 @@
    2.94              |> Thm.close_derivation
    2.95            end;
    2.96  
    2.97 -        val srel_Gr = mk_lazy mk_srel_Gr;
    2.98 +        val srel_Gr = Lazy.lazy mk_srel_Gr;
    2.99  
   2.100          fun mk_srel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
   2.101          fun mk_srel_concl f = HOLogic.mk_Trueprop
   2.102 @@ -1039,8 +1035,8 @@
   2.103              |> Thm.close_derivation
   2.104            end;
   2.105  
   2.106 -        val srel_mono = mk_lazy mk_srel_mono;
   2.107 -        val srel_cong = mk_lazy mk_srel_cong;
   2.108 +        val srel_mono = Lazy.lazy mk_srel_mono;
   2.109 +        val srel_cong = Lazy.lazy mk_srel_cong;
   2.110  
   2.111          fun mk_srel_Id () =
   2.112            let val srelAsAs = mk_bnf_srel self_setRTs CA' CA' in
   2.113 @@ -1051,7 +1047,7 @@
   2.114              |> Thm.close_derivation
   2.115            end;
   2.116  
   2.117 -        val srel_Id = mk_lazy mk_srel_Id;
   2.118 +        val srel_Id = Lazy.lazy mk_srel_Id;
   2.119  
   2.120          fun mk_srel_converse () =
   2.121            let
   2.122 @@ -1069,7 +1065,7 @@
   2.123              |> Thm.close_derivation
   2.124            end;
   2.125  
   2.126 -        val srel_converse = mk_lazy mk_srel_converse;
   2.127 +        val srel_converse = Lazy.lazy mk_srel_converse;
   2.128  
   2.129          fun mk_srel_O () =
   2.130            let
   2.131 @@ -1085,7 +1081,7 @@
   2.132              |> Thm.close_derivation
   2.133            end;
   2.134  
   2.135 -        val srel_O = mk_lazy mk_srel_O;
   2.136 +        val srel_O = Lazy.lazy mk_srel_O;
   2.137  
   2.138          fun mk_in_srel () =
   2.139            let
   2.140 @@ -1105,7 +1101,7 @@
   2.141              |> Thm.close_derivation
   2.142            end;
   2.143  
   2.144 -        val in_srel = mk_lazy mk_in_srel;
   2.145 +        val in_srel = Lazy.lazy mk_in_srel;
   2.146  
   2.147          val eqset_imp_iff_pair = @{thm eqset_imp_iff_pair};
   2.148          val mem_Collect_etc = @{thms mem_Collect_eq fst_conv snd_conv prod.cases};
   2.149 @@ -1116,7 +1112,7 @@
   2.150                 RS eqset_imp_iff_pair RS sym)
   2.151            |> Drule.zero_var_indexes;
   2.152  
   2.153 -        val rel_as_srel = mk_lazy mk_rel_as_srel;
   2.154 +        val rel_as_srel = Lazy.lazy mk_rel_as_srel;
   2.155  
   2.156          fun mk_rel_flip () =
   2.157            let
   2.158 @@ -1130,7 +1126,7 @@
   2.159              |> Drule.zero_var_indexes |> Thm.generalize ([], map fst Qs') 1
   2.160            end;
   2.161  
   2.162 -        val rel_flip = mk_lazy mk_rel_flip;
   2.163 +        val rel_flip = Lazy.lazy mk_rel_flip;
   2.164  
   2.165          val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def;
   2.166  
   2.167 @@ -1149,7 +1145,7 @@
   2.168            wits bnf_rel bnf_srel;
   2.169        in
   2.170          (bnf, lthy
   2.171 -          |> (if fact_policy = Note_All_Facts_and_Axioms then
   2.172 +          |> (if fact_policy = Note_All then
   2.173                  let
   2.174                    val witNs = if length wits = 1 then [witN] else map mk_witN (1 upto length wits);
   2.175                    val notes =
   2.176 @@ -1176,8 +1172,7 @@
   2.177                  end
   2.178                else
   2.179                  I)
   2.180 -          |> (if fact_policy = Note_All_Facts_and_Axioms orelse
   2.181 -                 fact_policy = Derive_All_Facts_Note_Most then
   2.182 +          |> (if fact_policy <> Dont_Note then
   2.183                  let
   2.184                    val notes =
   2.185                      [(map_comp'N, [Lazy.force (#map_comp' facts)]),
   2.186 @@ -1241,7 +1236,7 @@
   2.187    Proof.unfolding ([[(defs, [])]])
   2.188      (Proof.theorem NONE (snd o register_bnf key oo after_qed)
   2.189        (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
   2.190 -  prepare_def Do_Inline (user_policy Derive_All_Facts_Note_Most) I Syntax.read_term NONE;
   2.191 +  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE;
   2.192  
   2.193  fun print_bnfs ctxt =
   2.194    let
     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Sun Sep 23 14:52:53 2012 +0200
     3.3 @@ -2859,11 +2859,9 @@
     3.4  
     3.5          val wit_tac = mk_wit_tac n dtor_ctor_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
     3.6  
     3.7 -        val policy = user_policy Derive_All_Facts_Note_Most;
     3.8 -
     3.9          val (Jbnfs, lthy) =
    3.10            fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn (thms, wits) => fn lthy =>
    3.11 -            bnf_def Dont_Inline policy I tacs (wit_tac thms) (SOME deads)
    3.12 +            bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads)
    3.13                (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
    3.14              |> register_bnf (Local_Theory.full_name lthy b))
    3.15            tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
     4.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 23 14:52:53 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Sun Sep 23 14:52:53 2012 +0200
     4.3 @@ -1703,11 +1703,9 @@
     4.4  
     4.5          fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
     4.6  
     4.7 -        val policy = user_policy Derive_All_Facts_Note_Most;
     4.8 -
     4.9          val (Ibnfs, lthy) =
    4.10            fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn wits => fn lthy =>
    4.11 -            bnf_def Dont_Inline policy I tacs wit_tac (SOME deads)
    4.12 +            bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
    4.13                (((((b, fold_rev Term.absfree fs' mapx), sets), absdummy T bd), wits), NONE) lthy
    4.14              |> register_bnf (Local_Theory.full_name lthy b))
    4.15            tacss bs fs_maps setss_by_bnf Ts ctor_witss lthy;