introduced mechanism to filter interpretations
authorblanchet
Fri Sep 05 00:41:01 2014 +0200 (2014-09-05)
changeset 58188cc71d2be4f0a
parent 58187 d2ddd401d74d
child 58189 9d714be4f028
introduced mechanism to filter interpretations
src/HOL/Ctr_Sugar.thy
src/HOL/Library/bnf_axiomatization.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/local_interpretation.ML
src/HOL/Tools/Old_Datatype/old_datatype_data.ML
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Ctr_Sugar.thy	Fri Sep 05 00:41:01 2014 +0200
     1.2 +++ b/src/HOL/Ctr_Sugar.thy	Fri Sep 05 00:41:01 2014 +0200
     1.3 @@ -30,12 +30,12 @@
     1.4  ML_file "Tools/Ctr_Sugar/case_translation.ML"
     1.5  
     1.6  lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
     1.7 -by (erule iffI) (erule contrapos_pn)
     1.8 +  by (erule iffI) (erule contrapos_pn)
     1.9  
    1.10  lemma iff_contradict:
    1.11 -"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    1.12 -"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    1.13 -by blast+
    1.14 +  "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    1.15 +  "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    1.16 +  by blast+
    1.17  
    1.18  ML_file "Tools/Ctr_Sugar/local_interpretation.ML"
    1.19  ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
     2.1 --- a/src/HOL/Library/bnf_axiomatization.ML	Fri Sep 05 00:41:01 2014 +0200
     2.2 +++ b/src/HOL/Library/bnf_axiomatization.ML	Fri Sep 05 00:41:01 2014 +0200
     2.3 @@ -91,7 +91,7 @@
     2.4  
     2.5      val (bnf, lthy') = after_qed mk_wit_thms thms lthy
     2.6    in
     2.7 -    (bnf, BNF_Def.register_bnf key bnf lthy')
     2.8 +    (bnf, BNF_Def.register_bnf (K true) key bnf lthy')
     2.9    end;
    2.10  
    2.11  val bnf_axiomatization = prepare_decl (K I) (K I);
     3.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:01 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:01 2014 +0200
     3.3 @@ -19,9 +19,9 @@
     3.4    val bnf_of_global: theory -> string -> bnf option
     3.5    val bnf_interpretation: string -> (bnf -> theory -> theory) ->
     3.6      (bnf -> local_theory -> local_theory) -> theory -> theory
     3.7 -  val interpret_bnf: bnf -> local_theory -> local_theory
     3.8 +  val interpret_bnf: (string -> bool) -> bnf -> local_theory -> local_theory
     3.9    val register_bnf_raw: string -> bnf -> local_theory -> local_theory
    3.10 -  val register_bnf: string -> bnf -> local_theory -> local_theory
    3.11 +  val register_bnf: (string -> bool) -> string -> bnf -> local_theory -> local_theory
    3.12  
    3.13    val name_of_bnf: bnf -> binding
    3.14    val T_of_bnf: bnf -> typ
    3.15 @@ -1532,8 +1532,8 @@
    3.16    Local_Theory.declaration {syntax = false, pervasive = true}
    3.17      (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
    3.18  
    3.19 -fun register_bnf key bnf =
    3.20 -  register_bnf_raw key bnf #> interpret_bnf bnf;
    3.21 +fun register_bnf keep key bnf =
    3.22 +  register_bnf_raw key bnf #> interpret_bnf keep bnf;
    3.23  
    3.24  fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
    3.25    (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
    3.26 @@ -1572,7 +1572,7 @@
    3.27        | SOME tac => (mk_triv_wit_thms tac, []));
    3.28    in
    3.29      Proof.unfolding ([[(defs, [])]])
    3.30 -      (Proof.theorem NONE (uncurry (register_bnf key) oo after_qed mk_wit_thms)
    3.31 +      (Proof.theorem NONE (uncurry (register_bnf (K true) key) oo after_qed mk_wit_thms)
    3.32          (map (single o rpair []) goals @ nontriv_wit_goals) lthy)
    3.33    end) oo prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
    3.34      NONE Binding.empty Binding.empty [];
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     4.3 @@ -41,9 +41,9 @@
     4.4    val fp_sugars_of_global: theory -> fp_sugar list
     4.5    val fp_sugars_interpretation: string -> (fp_sugar list -> theory -> theory) ->
     4.6      (fp_sugar list -> local_theory -> local_theory)-> theory -> theory
     4.7 -  val interpret_fp_sugars: fp_sugar list -> local_theory -> local_theory
     4.8 +  val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
     4.9    val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
    4.10 -  val register_fp_sugars: fp_sugar list -> local_theory -> local_theory
    4.11 +  val register_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
    4.12  
    4.13    val co_induct_of: 'a list -> 'a
    4.14    val strong_co_induct_of: 'a list -> 'a
    4.15 @@ -236,8 +236,8 @@
    4.16          (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
    4.17      fp_sugars;
    4.18  
    4.19 -fun register_fp_sugars fp_sugars =
    4.20 -  register_fp_sugars_raw fp_sugars #> interpret_fp_sugars fp_sugars;
    4.21 +fun register_fp_sugars keep fp_sugars =
    4.22 +  register_fp_sugars_raw fp_sugars #> interpret_fp_sugars keep fp_sugars;
    4.23  
    4.24  fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
    4.25      live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss
    4.26 @@ -258,8 +258,8 @@
    4.27          |> morph_fp_sugar (substitute_noted_thm noted)) Ts;
    4.28    in
    4.29      register_fp_sugars_raw fp_sugars
    4.30 -    #> fold interpret_bnf (#bnfs fp_res)
    4.31 -    #> interpret_fp_sugars fp_sugars
    4.32 +    #> fold (interpret_bnf (K true)) (#bnfs fp_res)
    4.33 +    #> interpret_fp_sugars (K true) fp_sugars
    4.34    end;
    4.35  
    4.36  (* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A",
     5.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     5.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     5.3 @@ -46,10 +46,10 @@
     5.4    val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
     5.5    val ctr_sugar_interpretation: string -> (ctr_sugar -> theory -> theory) ->
     5.6      (ctr_sugar -> local_theory -> local_theory) -> theory -> theory
     5.7 -  val interpret_ctr_sugar: ctr_sugar -> local_theory -> local_theory
     5.8 +  val interpret_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
     5.9    val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory
    5.10 -  val register_ctr_sugar: ctr_sugar -> local_theory -> local_theory
    5.11 -  val default_register_ctr_sugar_global: ctr_sugar -> theory -> theory
    5.12 +  val register_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
    5.13 +  val default_register_ctr_sugar_global: (string -> bool) -> ctr_sugar -> theory -> theory
    5.14  
    5.15    val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
    5.16    val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
    5.17 @@ -193,17 +193,17 @@
    5.18    Local_Theory.declaration {syntax = false, pervasive = true}
    5.19      (fn phi => Data.map (Symtab.update (s, morph_ctr_sugar phi ctr_sugar)));
    5.20  
    5.21 -fun register_ctr_sugar ctr_sugar =
    5.22 -  register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar ctr_sugar;
    5.23 +fun register_ctr_sugar keep ctr_sugar =
    5.24 +  register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar keep ctr_sugar;
    5.25  
    5.26 -fun default_register_ctr_sugar_global (ctr_sugar as {T = Type (s, _), ...}) thy =
    5.27 +fun default_register_ctr_sugar_global keep (ctr_sugar as {T = Type (s, _), ...}) thy =
    5.28    let val tab = Data.get (Context.Theory thy) in
    5.29      if Symtab.defined tab s then
    5.30        thy
    5.31      else
    5.32        thy
    5.33        |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
    5.34 -      |> Ctr_Sugar_Interpretation.data_global ctr_sugar
    5.35 +      |> Ctr_Sugar_Interpretation.data_global keep ctr_sugar
    5.36    end;
    5.37  
    5.38  val isN = "is_";
    5.39 @@ -1045,7 +1045,7 @@
    5.40             case_eq_ifs = case_eq_if_thms}
    5.41            |> morph_ctr_sugar (substitute_noted_thm noted);
    5.42        in
    5.43 -        (ctr_sugar, lthy' |> register_ctr_sugar ctr_sugar)
    5.44 +        (ctr_sugar, lthy' |> register_ctr_sugar (K true) ctr_sugar)
    5.45        end;
    5.46    in
    5.47      (goalss, after_qed, lthy')
     6.1 --- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Fri Sep 05 00:41:01 2014 +0200
     6.2 +++ b/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML	Fri Sep 05 00:41:01 2014 +0200
     6.3 @@ -13,8 +13,8 @@
     6.4    val result: theory -> T list
     6.5    val interpretation: string -> (T -> theory -> theory) -> (T -> local_theory -> local_theory) ->
     6.6      theory -> theory
     6.7 -  val data: T -> local_theory -> local_theory
     6.8 -  val data_global: T -> theory -> theory
     6.9 +  val data: (string -> bool) -> T -> local_theory -> local_theory
    6.10 +  val data_global: (string -> bool) -> T -> theory -> theory
    6.11    val init: theory -> theory
    6.12  end;
    6.13  
    6.14 @@ -26,9 +26,9 @@
    6.15  structure Interp = Theory_Data
    6.16  (
    6.17    type T =
    6.18 -    (Name_Space.naming * T) list
    6.19 +    ((Name_Space.naming * (string -> bool)) * T) list
    6.20      * ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * (string * stamp))
    6.21 -       * (Name_Space.naming * T) list) list;
    6.22 +       * ((Name_Space.naming * (string -> bool)) * T) list) list;
    6.23    val empty = ([], []);
    6.24    val extend = I;
    6.25    fun merge ((data1, interps1), (data2, interps2)) : T =
    6.26 @@ -41,10 +41,17 @@
    6.27  fun consolidate_common g_or_f lift_lthy thy thy_or_lthy =
    6.28    let
    6.29      val (data, interps) = Interp.get thy;
    6.30 -    val unfinished = interps |> map (fn ((gf, _), data') =>
    6.31 +
    6.32 +    fun unfinished_of ((gf, (name, _)), data') =
    6.33        (g_or_f gf,
    6.34 -       if eq_list (eq_snd eq) (data', data) then [] else subtract (eq_snd eq) data' data));
    6.35 -    val finished = interps |> map (apsnd (K data));
    6.36 +       if eq_list (eq_snd eq) (data', data) then
    6.37 +         []
    6.38 +       else
    6.39 +         subtract (eq_snd eq) data' data
    6.40 +         |> map_filter (fn ((naming, keep), x) => if keep name then SOME (naming, x) else NONE));
    6.41 +
    6.42 +    val unfinished = map unfinished_of interps;
    6.43 +    val finished = map (apsnd (K data)) interps;
    6.44    in
    6.45      if forall (null o #2) unfinished then
    6.46        NONE
    6.47 @@ -64,12 +71,13 @@
    6.48  fun interpretation name g f =
    6.49    Interp.map (apsnd (cons (((g, f), (name, stamp ())), []))) #> perhaps consolidate_global;
    6.50  
    6.51 -fun data x =
    6.52 -  Local_Theory.background_theory (fn thy => Interp.map (apfst (cons (Sign.naming_of thy, x))) thy)
    6.53 +fun data keep x =
    6.54 +  Local_Theory.background_theory
    6.55 +    (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
    6.56    #> perhaps consolidate;
    6.57  
    6.58 -fun data_global x =
    6.59 -  (fn thy => Interp.map (apfst (cons (Sign.naming_of thy, x))) thy)
    6.60 +fun data_global keep x =
    6.61 +  (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
    6.62    #> perhaps consolidate_global;
    6.63  
    6.64  val init = Theory.at_begin consolidate_global;
     7.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Fri Sep 05 00:41:01 2014 +0200
     7.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Fri Sep 05 00:41:01 2014 +0200
     7.3 @@ -135,7 +135,7 @@
     7.4            map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos),
     7.5       cases = cases |> fold Symtab.update
     7.6         (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #>
     7.7 -  fold (Ctr_Sugar.default_register_ctr_sugar_global o ctr_sugar_of_info o snd) dt_infos;
     7.8 +  fold (Ctr_Sugar.default_register_ctr_sugar_global (K true) o ctr_sugar_of_info o snd) dt_infos;
     7.9  
    7.10  
    7.11  (* complex queries *)
     8.1 --- a/src/HOL/Tools/record.ML	Fri Sep 05 00:41:01 2014 +0200
     8.2 +++ b/src/HOL/Tools/record.ML	Fri Sep 05 00:41:01 2014 +0200
     8.3 @@ -1782,7 +1782,7 @@
     8.4    else thy;
     8.5  
     8.6  fun add_ctr_sugar ctr sels exhaust inject sel_defs sel_thms =
     8.7 -  Ctr_Sugar.default_register_ctr_sugar_global
     8.8 +  Ctr_Sugar.default_register_ctr_sugar_global (K true)
     8.9      {T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels],
    8.10       exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject], distincts = [],
    8.11       case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,