--- a/src/HOL/Ctr_Sugar.thy Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Ctr_Sugar.thy Fri Sep 05 00:41:01 2014 +0200
@@ -30,12 +30,12 @@
ML_file "Tools/Ctr_Sugar/case_translation.ML"
lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
-by (erule iffI) (erule contrapos_pn)
+ by (erule iffI) (erule contrapos_pn)
lemma iff_contradict:
-"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
-"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
-by blast+
+ "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
+ "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
+ by blast+
ML_file "Tools/Ctr_Sugar/local_interpretation.ML"
ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
--- a/src/HOL/Library/bnf_axiomatization.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Library/bnf_axiomatization.ML Fri Sep 05 00:41:01 2014 +0200
@@ -91,7 +91,7 @@
val (bnf, lthy') = after_qed mk_wit_thms thms lthy
in
- (bnf, BNF_Def.register_bnf key bnf lthy')
+ (bnf, BNF_Def.register_bnf (K true) key bnf lthy')
end;
val bnf_axiomatization = prepare_decl (K I) (K I);
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 05 00:41:01 2014 +0200
@@ -19,9 +19,9 @@
val bnf_of_global: theory -> string -> bnf option
val bnf_interpretation: string -> (bnf -> theory -> theory) ->
(bnf -> local_theory -> local_theory) -> theory -> theory
- val interpret_bnf: bnf -> local_theory -> local_theory
+ val interpret_bnf: (string -> bool) -> bnf -> local_theory -> local_theory
val register_bnf_raw: string -> bnf -> local_theory -> local_theory
- val register_bnf: string -> bnf -> local_theory -> local_theory
+ val register_bnf: (string -> bool) -> string -> bnf -> local_theory -> local_theory
val name_of_bnf: bnf -> binding
val T_of_bnf: bnf -> typ
@@ -1532,8 +1532,8 @@
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
-fun register_bnf key bnf =
- register_bnf_raw key bnf #> interpret_bnf bnf;
+fun register_bnf keep key bnf =
+ register_bnf_raw key bnf #> interpret_bnf keep bnf;
fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
(fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
@@ -1572,7 +1572,7 @@
| SOME tac => (mk_triv_wit_thms tac, []));
in
Proof.unfolding ([[(defs, [])]])
- (Proof.theorem NONE (uncurry (register_bnf key) oo after_qed mk_wit_thms)
+ (Proof.theorem NONE (uncurry (register_bnf (K true) key) oo after_qed mk_wit_thms)
(map (single o rpair []) goals @ nontriv_wit_goals) lthy)
end) oo prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
NONE Binding.empty Binding.empty [];
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 05 00:41:01 2014 +0200
@@ -41,9 +41,9 @@
val fp_sugars_of_global: theory -> fp_sugar list
val fp_sugars_interpretation: string -> (fp_sugar list -> theory -> theory) ->
(fp_sugar list -> local_theory -> local_theory)-> theory -> theory
- val interpret_fp_sugars: fp_sugar list -> local_theory -> local_theory
+ val interpret_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
val register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
- val register_fp_sugars: fp_sugar list -> local_theory -> local_theory
+ val register_fp_sugars: (string -> bool) -> fp_sugar list -> local_theory -> local_theory
val co_induct_of: 'a list -> 'a
val strong_co_induct_of: 'a list -> 'a
@@ -236,8 +236,8 @@
(fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
fp_sugars;
-fun register_fp_sugars fp_sugars =
- register_fp_sugars_raw fp_sugars #> interpret_fp_sugars fp_sugars;
+fun register_fp_sugars keep fp_sugars =
+ register_fp_sugars_raw fp_sugars #> interpret_fp_sugars keep fp_sugars;
fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss
@@ -258,8 +258,8 @@
|> morph_fp_sugar (substitute_noted_thm noted)) Ts;
in
register_fp_sugars_raw fp_sugars
- #> fold interpret_bnf (#bnfs fp_res)
- #> interpret_fp_sugars fp_sugars
+ #> fold (interpret_bnf (K true)) (#bnfs fp_res)
+ #> interpret_fp_sugars (K true) fp_sugars
end;
(* This function could produce (fairly harmless) clashes in contrived examples (e.g., "x.A",
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 05 00:41:01 2014 +0200
@@ -46,10 +46,10 @@
val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
val ctr_sugar_interpretation: string -> (ctr_sugar -> theory -> theory) ->
(ctr_sugar -> local_theory -> local_theory) -> theory -> theory
- val interpret_ctr_sugar: ctr_sugar -> local_theory -> local_theory
+ val interpret_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory
- val register_ctr_sugar: ctr_sugar -> local_theory -> local_theory
- val default_register_ctr_sugar_global: ctr_sugar -> theory -> theory
+ val register_ctr_sugar: (string -> bool) -> ctr_sugar -> local_theory -> local_theory
+ val default_register_ctr_sugar_global: (string -> bool) -> ctr_sugar -> theory -> theory
val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
@@ -193,17 +193,17 @@
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.update (s, morph_ctr_sugar phi ctr_sugar)));
-fun register_ctr_sugar ctr_sugar =
- register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar ctr_sugar;
+fun register_ctr_sugar keep ctr_sugar =
+ register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar keep ctr_sugar;
-fun default_register_ctr_sugar_global (ctr_sugar as {T = Type (s, _), ...}) thy =
+fun default_register_ctr_sugar_global keep (ctr_sugar as {T = Type (s, _), ...}) thy =
let val tab = Data.get (Context.Theory thy) in
if Symtab.defined tab s then
thy
else
thy
|> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
- |> Ctr_Sugar_Interpretation.data_global ctr_sugar
+ |> Ctr_Sugar_Interpretation.data_global keep ctr_sugar
end;
val isN = "is_";
@@ -1045,7 +1045,7 @@
case_eq_ifs = case_eq_if_thms}
|> morph_ctr_sugar (substitute_noted_thm noted);
in
- (ctr_sugar, lthy' |> register_ctr_sugar ctr_sugar)
+ (ctr_sugar, lthy' |> register_ctr_sugar (K true) ctr_sugar)
end;
in
(goalss, after_qed, lthy')
--- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML Fri Sep 05 00:41:01 2014 +0200
@@ -13,8 +13,8 @@
val result: theory -> T list
val interpretation: string -> (T -> theory -> theory) -> (T -> local_theory -> local_theory) ->
theory -> theory
- val data: T -> local_theory -> local_theory
- val data_global: T -> theory -> theory
+ val data: (string -> bool) -> T -> local_theory -> local_theory
+ val data_global: (string -> bool) -> T -> theory -> theory
val init: theory -> theory
end;
@@ -26,9 +26,9 @@
structure Interp = Theory_Data
(
type T =
- (Name_Space.naming * T) list
+ ((Name_Space.naming * (string -> bool)) * T) list
* ((((T -> theory -> theory) * (T -> local_theory -> local_theory)) * (string * stamp))
- * (Name_Space.naming * T) list) list;
+ * ((Name_Space.naming * (string -> bool)) * T) list) list;
val empty = ([], []);
val extend = I;
fun merge ((data1, interps1), (data2, interps2)) : T =
@@ -41,10 +41,17 @@
fun consolidate_common g_or_f lift_lthy thy thy_or_lthy =
let
val (data, interps) = Interp.get thy;
- val unfinished = interps |> map (fn ((gf, _), data') =>
+
+ fun unfinished_of ((gf, (name, _)), data') =
(g_or_f gf,
- if eq_list (eq_snd eq) (data', data) then [] else subtract (eq_snd eq) data' data));
- val finished = interps |> map (apsnd (K data));
+ if eq_list (eq_snd eq) (data', data) then
+ []
+ else
+ subtract (eq_snd eq) data' data
+ |> map_filter (fn ((naming, keep), x) => if keep name then SOME (naming, x) else NONE));
+
+ val unfinished = map unfinished_of interps;
+ val finished = map (apsnd (K data)) interps;
in
if forall (null o #2) unfinished then
NONE
@@ -64,12 +71,13 @@
fun interpretation name g f =
Interp.map (apsnd (cons (((g, f), (name, stamp ())), []))) #> perhaps consolidate_global;
-fun data x =
- Local_Theory.background_theory (fn thy => Interp.map (apfst (cons (Sign.naming_of thy, x))) thy)
+fun data keep x =
+ Local_Theory.background_theory
+ (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
#> perhaps consolidate;
-fun data_global x =
- (fn thy => Interp.map (apfst (cons (Sign.naming_of thy, x))) thy)
+fun data_global keep x =
+ (fn thy => Interp.map (apfst (cons ((Sign.naming_of thy, keep), x))) thy)
#> perhaps consolidate_global;
val init = Theory.at_begin consolidate_global;
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Fri Sep 05 00:41:01 2014 +0200
@@ -135,7 +135,7 @@
map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos),
cases = cases |> fold Symtab.update
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #>
- fold (Ctr_Sugar.default_register_ctr_sugar_global o ctr_sugar_of_info o snd) dt_infos;
+ fold (Ctr_Sugar.default_register_ctr_sugar_global (K true) o ctr_sugar_of_info o snd) dt_infos;
(* complex queries *)
--- a/src/HOL/Tools/record.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/record.ML Fri Sep 05 00:41:01 2014 +0200
@@ -1782,7 +1782,7 @@
else thy;
fun add_ctr_sugar ctr sels exhaust inject sel_defs sel_thms =
- Ctr_Sugar.default_register_ctr_sugar_global
+ Ctr_Sugar.default_register_ctr_sugar_global (K true)
{T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels],
exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject], distincts = [],
case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,