# HG changeset patch # User blanchet # Date 1409822459 -7200 # Node ID 82478e6c60cb4b4e3c02177be8b2590915fdb469 # Parent 6d527272f7b2e39f50b3e06e6a8263c5f9539c64 tweaked setup for datatype realizer diff -r 6d527272f7b2 -r 82478e6c60cb src/HOL/BNF_Least_Fixpoint.thy --- 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\bool) = 0" by (cases b) auto diff -r 6d527272f7b2 -r 82478e6c60cb src/HOL/Old_Datatype.thy --- 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 diff -r 6d527272f7b2 -r 82478e6c60cb src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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", diff -r 6d527272f7b2 -r 82478e6c60cb src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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 = diff -r 6d527272f7b2 -r 82478e6c60cb src/HOL/Tools/Ctr_Sugar/local_interpretation.ML --- 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 = diff -r 6d527272f7b2 -r 82478e6c60cb src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML --- 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; diff -r 6d527272f7b2 -r 82478e6c60cb src/HOL/Transfer.thy --- 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 \ bool) \ 'a \ 'a \ bool" +definition eq_onp :: "('a \ bool) \ 'a \ 'a \ bool" where "eq_onp R = (\x y. R x \ 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=) (\R S x z. \y\Collect (Domainp B). R x y \ 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 \ ((A ===> A ===> op=) ===> op=) reflp reflp" "right_total A \ ((A ===> A ===> implies) ===> implies) reflp reflp" "right_total A \ ((A ===> A ===> op=) ===> implies) reflp reflp" "bi_total A \ ((A ===> A ===> rev_implies) ===> rev_implies) reflp reflp" "bi_total A \ ((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]: