--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 04 11:20:59 2014 +0200
@@ -188,6 +188,7 @@
ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
ML_file "Tools/BNF/bnf_lfp_size.ML"
ML_file "Tools/Function/old_size.ML"
+ML_file "Tools/Old_Datatype/old_datatype_realizer.ML"
lemma size_bool[code]: "size (b\<Colon>bool) = 0"
by (cases b) auto
--- a/src/HOL/Old_Datatype.thy Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/Old_Datatype.thy Thu Sep 04 11:20:59 2014 +0200
@@ -526,7 +526,4 @@
ML_file "Tools/inductive_realizer.ML"
setup InductiveRealizer.setup
-ML_file "Tools/Old_Datatype/old_datatype_realizer.ML"
-setup Old_Datatype_Realizer.setup
-
end
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 04 11:20:59 2014 +0200
@@ -41,6 +41,8 @@
val fp_sugars_of_global: theory -> fp_sugar list
val fp_sugar_interpretation: (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 register_fp_sugars_raw: fp_sugar list -> local_theory -> local_theory
val register_fp_sugars: fp_sugar list -> local_theory -> local_theory
val co_induct_of: 'a list -> 'a
@@ -229,13 +231,16 @@
|> Sign.restore_naming thy;
val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
+val interpret_fp_sugars = FP_Sugar_Interpretation.data;
-fun register_fp_sugars fp_sugars =
+fun register_fp_sugars_raw fp_sugars =
fold (fn fp_sugar as {T = Type (s, _), ...} =>
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
- fp_sugars
- #> FP_Sugar_Interpretation.data fp_sugars;
+ fp_sugars;
+
+fun register_fp_sugars fp_sugars =
+ register_fp_sugars fp_sugars #> interpret_fp_sugars 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
@@ -255,8 +260,9 @@
rel_distincts = nth rel_distinctss kk}
|> morph_fp_sugar (substitute_noted_thm noted)) Ts;
in
- fold interpret_bnf (#bnfs fp_res)
- #> register_fp_sugars fp_sugars
+ register_fp_sugars_raw fp_sugars
+ #> fold interpret_bnf (#bnfs fp_res)
+ #> interpret_fp_sugars 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 Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Thu Sep 04 11:20:59 2014 +0200
@@ -1025,7 +1025,7 @@
(Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
I)
|> Local_Theory.notes (anonymous_notes @ notes)
- (* for "datatype_realizer.ML": *)
+ (* for "old_datatype_realizer.ML": *)
|>> name_noted_thms fcT_name exhaustN;
val ctr_sugar =
--- a/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/local_interpretation.ML Thu Sep 04 11:20:59 2014 +0200
@@ -42,11 +42,13 @@
val (data, interps) = Interp.get thy;
val unfinished = interps |> map (fn ((gf, _), xs) =>
(g_or_f gf, if eq_list eq (xs, data) then [] else subtract eq xs data));
- val finished = interps |> map (fn (interp, _) => (interp, data));
+ val finished = interps |> map (apsnd (K data));
in
- if forall (null o #2) unfinished then NONE
- else SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
- |> lift_lthy (Interp.put (data, finished)))
+ if forall (null o #2) unfinished then
+ NONE
+ else
+ SOME (thy_or_lthy |> fold_rev (uncurry fold_rev) unfinished
+ |> lift_lthy (Interp.put (data, finished)))
end;
fun consolidate lthy =
--- a/src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML Thu Sep 04 11:20:59 2014 +0200
@@ -8,7 +8,6 @@
signature OLD_DATATYPE_REALIZER =
sig
val add_dt_realizers: Old_Datatype_Aux.config -> string list -> theory -> theory
- val setup: theory -> theory
end;
structure Old_Datatype_Realizer : OLD_DATATYPE_REALIZER =
@@ -158,9 +157,7 @@
in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
-
-fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info)
- thy =
+fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Old_Datatype_Aux.info) thy =
let
val ctxt = Proof_Context.init_global thy;
val cert = cterm_of thy;
@@ -241,6 +238,6 @@
|> fold_rev make_casedists infos
end;
-val setup = Old_Datatype_Data.interpretation add_dt_realizers;
+val _ = Theory.setup (Old_Datatype_Data.interpretation add_dt_realizers);
end;
--- a/src/HOL/Transfer.thy Thu Sep 04 09:02:43 2014 +0200
+++ b/src/HOL/Transfer.thy Thu Sep 04 11:20:59 2014 +0200
@@ -9,8 +9,8 @@
imports Hilbert_Choice Metis Option
begin
-(* We include Option here although it's not needed here.
- By doing this, we avoid a diamond problem for BNF and
+(* We import Option here although it's not needed here.
+ By doing this, we avoid a diamond problem for BNF and
FP sugar interpretation defined in this file. *)
subsection {* Relator for function space *}
@@ -227,18 +227,18 @@
subsection {* Equality restricted by a predicate *}
-definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
-lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id"
-unfolding eq_onp_def Grp_def by auto
+lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id"
+unfolding eq_onp_def Grp_def by auto
lemma eq_onp_to_eq:
assumes "eq_onp P x y"
shows "x = y"
using assms by (simp add: eq_onp_def)
-lemma eq_onp_top_eq_eq: "eq_onp top = op="
+lemma eq_onp_top_eq_eq: "eq_onp top = op="
by (simp add: eq_onp_def)
lemma eq_onp_same_args:
@@ -298,10 +298,10 @@
subsection {* Properties of relators *}
-lemma left_total_eq[transfer_rule]: "left_total op="
+lemma left_total_eq[transfer_rule]: "left_total op="
unfolding left_total_def by blast
-lemma left_unique_eq[transfer_rule]: "left_unique op="
+lemma left_unique_eq[transfer_rule]: "left_unique op="
unfolding left_unique_def by blast
lemma right_total_eq [transfer_rule]: "right_total op="
@@ -366,7 +366,7 @@
end
-ML_file "Tools/Transfer/transfer_bnf.ML"
+ML_file "Tools/Transfer/transfer_bnf.ML"
declare pred_fun_def [simp]
declare rel_fun_eq [relator_eq]
@@ -486,13 +486,13 @@
shows "((A ===> B) ===> op=) mono mono"
unfolding mono_def[abs_def] by transfer_prover
-lemma right_total_relcompp_transfer[transfer_rule]:
+lemma right_total_relcompp_transfer[transfer_rule]:
assumes [transfer_rule]: "right_total B"
- shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=)
+ shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=)
(\<lambda>R S x z. \<exists>y\<in>Collect (Domainp B). R x y \<and> S y z) op OO"
unfolding OO_def[abs_def] by transfer_prover
-lemma relcompp_transfer[transfer_rule]:
+lemma relcompp_transfer[transfer_rule]:
assumes [transfer_rule]: "bi_total B"
shows "((A ===> B ===> op=) ===> (B ===> C ===> op=) ===> A ===> C ===> op=) op OO op OO"
unfolding OO_def[abs_def] by transfer_prover
@@ -507,13 +507,13 @@
shows "((A ===> B ===> op=) ===> A ===> op=) Domainp Domainp"
unfolding Domainp_iff[abs_def] by transfer_prover
-lemma reflp_transfer[transfer_rule]:
+lemma reflp_transfer[transfer_rule]:
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> op=) reflp reflp"
"right_total A \<Longrightarrow> ((A ===> A ===> implies) ===> implies) reflp reflp"
"right_total A \<Longrightarrow> ((A ===> A ===> op=) ===> implies) reflp reflp"
"bi_total A \<Longrightarrow> ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp"
"bi_total A \<Longrightarrow> ((A ===> A ===> op=) ===> rev_implies) reflp reflp"
-using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
+using assms unfolding reflp_def[abs_def] rev_implies_def bi_total_def right_total_def rel_fun_def
by fast+
lemma right_unique_transfer [transfer_rule]: