# HG changeset patch # User blanchet # Date 1420437375 -3600 # Node ID d207455817e861f58c7f2411f7355f1f6c042e0f # Parent 77cd4992edcd7012f55cea63d12d4002e5cff84c tuning diff -r 77cd4992edcd -r d207455817e8 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Dec 19 14:06:13 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jan 05 06:56:15 2015 +0100 @@ -64,6 +64,9 @@ fp_bnf_sugar: fp_bnf_sugar, fp_co_induct_sugar: fp_co_induct_sugar}; + val co_induct_of: 'a list -> 'a + val strong_co_induct_of: 'a list -> 'a + val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar val transfer_fp_sugar: theory -> fp_sugar -> fp_sugar val fp_sugar_of: Proof.context -> string -> fp_sugar option @@ -76,8 +79,7 @@ val register_fp_sugars_raw: 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 + val mk_parametricity_goal: Proof.context -> term list -> term -> term -> term val flat_corec_preds_predsss_gettersss: 'a list -> 'a list list list -> 'a list list list -> 'a list @@ -154,8 +156,6 @@ BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> BNF_FP_Util.fp_result * local_theory) -> (local_theory -> local_theory) parser - - val mk_parametricity_goal: Proof.context -> term list -> term -> term -> term end; structure BNF_FP_Def_Sugar : BNF_FP_DEF_SUGAR = @@ -243,6 +243,9 @@ fp_bnf_sugar: fp_bnf_sugar, fp_co_induct_sugar: fp_co_induct_sugar}; +fun co_induct_of (i :: _) = i; +fun strong_co_induct_of [_, s] = s; + fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases} : fp_bnf_sugar) = @@ -328,9 +331,6 @@ val fp_sugars_of = fp_sugars_of_generic o Context.Proof; val fp_sugars_of_global = fp_sugars_of_generic o Context.Theory; -fun co_induct_of (i :: _) = i; -fun strong_co_induct_of [_, s] = s; - structure FP_Sugar_Plugin = Plugin(type T = fp_sugar list); fun fp_sugars_interpretation name f = diff -r 77cd4992edcd -r d207455817e8 src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Fri Dec 19 14:06:13 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Mon Jan 05 06:56:15 2015 +0100 @@ -5,65 +5,54 @@ Parametricity of primitively (co)recursive functions. *) -(* DO NOT FORGET TO DOCUMENT THIS NEW PLUGIN!!! *) - signature BNF_FP_REC_SUGAR_TRANSFER = sig - -val primrec_transfer_pluginN : string -val primcorec_transfer_pluginN : string - -val primrec_transfer_interpretation: - BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context -> Proof.context -val primcorec_transfer_interpretation: - BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context -> Proof.context - + val primrec_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context -> + Proof.context + val primcorec_transfer_interpretation: BNF_FP_Rec_Sugar_Util.fp_rec_sugar -> Proof.context -> + Proof.context end; structure BNF_FP_Rec_Sugar_Transfer : BNF_FP_REC_SUGAR_TRANSFER = struct +open Ctr_Sugar_Util +open Ctr_Sugar_Tactics open BNF_Def +open BNF_FP_Util open BNF_FP_Def_Sugar open BNF_FP_Rec_Sugar_Util -open BNF_FP_Util -open Ctr_Sugar_Tactics -open Ctr_Sugar_Util -val primrec_transfer_pluginN = Plugin_Name.declare_setup @{binding primrec_transfer}; -val primcorec_transfer_pluginN = Plugin_Name.declare_setup @{binding primcorec_transfer}; +val transferN = "transfer"; fun mk_primrec_transfer_tac ctxt def = Ctr_Sugar_Tactics.unfold_thms_tac ctxt [def] THEN HEADGOAL (Transfer.transfer_prover_tac ctxt); fun mk_primcorec_transfer_tac apply_transfer ctxt f_def corec_def type_definitions - dtor_corec_transfers rel_pre_defs disc_eq_cases cases case_distribs case_congs = + dtor_corec_transfers rel_pre_defs disc_eq_cases cases case_distribs case_congs = let fun instantiate_with_lambda thm = let val prop = Thm.prop_of thm; - val @{const Trueprop} $ - (Const (@{const_name HOL.eq}, _) $ - (Var (_, fT) $ _) $ _) = prop; + val @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, fT) $ _) $ _) = prop; val T = range_type fT; - val idx = Term.maxidx_of_term prop + 1; - val bool_expr = Var (("x", idx), HOLogic.boolT); - val then_expr = Var (("t", idx), T); - val else_expr = Var (("e", idx), T); - val lambda = Term.lambda bool_expr (mk_If bool_expr then_expr else_expr); + val j = Term.maxidx_of_term prop + 1; + val cond = Var (("x", j), HOLogic.boolT); + val then_branch = Var (("t", j), T); + val else_branch = Var (("e", j), T); + val lambda = Term.lambda cond (mk_If cond then_branch else_branch); in cterm_instantiate_pos [SOME (certify ctxt lambda)] thm end; val transfer_rules = - @{thm Abs_transfer[OF - BNF_Composition.type_definition_id_bnf_UNIV + @{thm Abs_transfer[OF BNF_Composition.type_definition_id_bnf_UNIV BNF_Composition.type_definition_id_bnf_UNIV]} :: map (fn thm => @{thm Abs_transfer} OF [thm, thm]) type_definitions @ map (Local_Defs.unfold ctxt rel_pre_defs) dtor_corec_transfers; - val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add - val ctxt' = Context.proof_map (fold add_transfer_rule transfer_rules) ctxt + val add_transfer_rule = Thm.attribute_declaration Transfer.transfer_add; + val ctxt' = Context.proof_map (fold add_transfer_rule transfer_rules) ctxt; val case_distribs = map instantiate_with_lambda case_distribs; val simps = case_distribs @ disc_eq_cases @ cases @ @{thms if_True if_False}; @@ -82,71 +71,63 @@ fun fp_sugar_of_bnf ctxt = fp_sugar_of ctxt o (fn Type (s, _) => s) o T_of_bnf; -val cat_somes = map the o filter is_some -fun maybe_apply z = the_default z oo Option.map - fun bnf_depth_first_traverse ctxt f T z = - case T of + (case T of Type (s, innerTs) => (case bnf_of ctxt s of NONE => z | SOME bnf => let val z' = f bnf z in fold (bnf_depth_first_traverse ctxt f) innerTs z' end) - | _ => z + | _ => z) fun if_all_bnfs ctxt Ts f g = - let - val bnfs = cat_somes (map (fn T => - case T of Type (s, _) => BNF_Def.bnf_of ctxt s | _ => NONE) Ts); - in + let val bnfs = map_filter (fn Type (s, _) => BNF_Def.bnf_of ctxt s | _ => NONE) Ts in if length bnfs = length Ts then f bnfs else g end; fun mk_goal lthy f = let - val skematicTs = Term.add_tvarsT (fastype_of f) []; + val skematic_Ts = Term.add_tvarsT (fastype_of f) []; val ((As, Bs), names_lthy) = lthy - |> Ctr_Sugar_Util.mk_TFrees' (map snd skematicTs) - ||>> Ctr_Sugar_Util.mk_TFrees' (map snd skematicTs); + |> Ctr_Sugar_Util.mk_TFrees' (map snd skematic_Ts) + ||>> Ctr_Sugar_Util.mk_TFrees' (map snd skematic_Ts); val (Rs, names_lthy) = Ctr_Sugar_Util.mk_Frees "R" (map2 BNF_Util.mk_pred2T As Bs) names_lthy; - val fA = Term.subst_TVars (map fst skematicTs ~~ As) f; - val fB = Term.subst_TVars (map fst skematicTs ~~ Bs) f; + val fA = Term.subst_TVars (map fst skematic_Ts ~~ As) f; + val fB = Term.subst_TVars (map fst skematic_Ts ~~ Bs) f; in (BNF_FP_Def_Sugar.mk_parametricity_goal lthy Rs fA fB, names_lthy) end; fun prove_parametricity_if_bnf prove {transfers, fun_names, funs, fun_defs, fpTs} lthy = fold_index (fn (n, (((transfer, f_names), f), def)) => fn lthy => - if not transfer then lthy + if not transfer then + lthy else if_all_bnfs lthy fpTs (fn bnfs => fn () => prove n bnfs f_names f def lthy) - (fn () => let val _ = error "Function is not parametric." in lthy end) ()) + (fn () => error "Function is not parametric" (*FIXME: wording*)) ()) (transfers ~~ fun_names ~~ funs ~~ fun_defs) lthy; fun prim_co_rec_transfer_interpretation prove = prove_parametricity_if_bnf (fn n => fn bnfs => fn f_name => fn f => fn def => fn lthy => - case try (prove n bnfs f def) lthy of - NONE => error "Failed to prove parametricity." + (case try (prove n bnfs f def) lthy of + NONE => error "Failed to prove parametricity" | SOME thm => let - val notes = - [("transfer", [thm], K @{attributes [transfer_rule]})] + val notes = [(transferN, [thm], K @{attributes [transfer_rule]})] |> massage_simple_notes f_name; in snd (Local_Theory.notes notes lthy) - end); + end)); val primrec_transfer_interpretation = prim_co_rec_transfer_interpretation - (fn n => fn bnfs => fn f => fn def => fn lthy => - let - val (goal, names_lthy) = mk_goal lthy f; - in + (fn _ => fn _ => fn f => fn def => fn lthy => + let val (goal, names_lthy) = mk_goal lthy f in Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} => mk_primrec_transfer_tac ctxt def) |> singleton (Proof_Context.export names_lthy lthy) @@ -159,33 +140,32 @@ val fp_sugars = map (the o fp_sugar_of_bnf lthy) bnfs; val (goal, names_lthy) = mk_goal lthy f; val (disc_eq_cases, case_thms, case_distribs, case_congs) = - bnf_depth_first_traverse lthy (fn bnf => fn xs => + bnf_depth_first_traverse lthy (fn bnf => fn quad => let - fun add_thms (xs, ys, zs, ws) (fp_sugar : fp_sugar) = - let - val ctr_sugar = #ctr_sugar (#fp_ctr_sugar fp_sugar); - val xs' = #disc_eq_cases ctr_sugar; - val ys' = #case_thms ctr_sugar; - val zs' = #case_distribs ctr_sugar; - val w = #case_cong ctr_sugar; - val union' = union Thm.eq_thm; - val insert' = insert Thm.eq_thm; - in - (union' xs' xs, union' ys' ys, union' zs' zs, insert' w ws) - end; + fun add_thms (disc_eq_cases0, case_thms0, case_distribs0, case_congs0) + {fp_ctr_sugar = {ctr_sugar = {disc_eq_cases, case_thms, case_distribs, case_cong, + ...}, ...}, ...} = + (union Thm.eq_thm disc_eq_cases disc_eq_cases0, + union Thm.eq_thm case_thms case_thms0, + union Thm.eq_thm case_distribs case_distribs0, + insert Thm.eq_thm case_cong case_congs0); in - maybe_apply xs (add_thms xs) (fp_sugar_of_bnf lthy bnf) + Option.map (add_thms quad) (fp_sugar_of_bnf lthy bnf) + |> the_default quad end) (fastype_of f) ([], [], [], []); in Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} => mk_primcorec_transfer_tac true ctxt def (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars n))) (map (#type_definition o #absT_info) fp_sugars) - (flat (map (#xtor_co_rec_transfers o #fp_res) fp_sugars)) + (maps (#xtor_co_rec_transfers o #fp_res) fp_sugars) (map (rel_def_of_bnf o #pre_bnf) fp_sugars) disc_eq_cases case_thms case_distribs case_congs) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation end); -end +val _ = Theory.setup (BNF_LFP_Rec_Sugar.primrec_interpretation Transfer_BNF.transfer_plugin + primrec_transfer_interpretation); + +end; diff -r 77cd4992edcd -r d207455817e8 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Dec 19 14:06:13 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Jan 05 06:56:15 2015 +0100 @@ -68,6 +68,7 @@ open BNF_FP_Def_Sugar open BNF_FP_N2M_Sugar open BNF_FP_Rec_Sugar_Util +open BNF_FP_Rec_Sugar_Transfer open BNF_GFP_Rec_Sugar_Tactics val codeN = "code"; @@ -951,7 +952,7 @@ val prems = maps (s_not_conj o #prems) disc_eqns; val ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE; val code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE; - val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (* FIXME *); + val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000; (* FIXME *) val extra_disc_eqn = {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = n, @@ -1504,8 +1505,7 @@ Parse.!!! (Parse.list1 primcorec_option_parser) --| @{keyword ")"}) []) -- (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd); -val _ = Theory.setup (primcorec_interpretation - BNF_FP_Rec_Sugar_Transfer.primcorec_transfer_pluginN - BNF_FP_Rec_Sugar_Transfer.primcorec_transfer_interpretation) +val _ = Theory.setup (primcorec_interpretation Transfer_BNF.transfer_plugin + primcorec_transfer_interpretation); end; diff -r 77cd4992edcd -r d207455817e8 src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Dec 19 14:06:13 2014 +0100 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Mon Jan 05 06:56:15 2015 +0100 @@ -6,6 +6,7 @@ signature TRANSFER_BNF = sig + val transfer_plugin: string val base_name_of_bnf: BNF_Def.bnf -> binding val type_name_of_bnf: BNF_Def.bnf -> string val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data @@ -20,6 +21,8 @@ open BNF_FP_Util open BNF_FP_Def_Sugar +val transfer_plugin = Plugin_Name.declare_setup @{binding transfer} + (* util functions *) fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf)) @@ -293,8 +296,6 @@ (* BNF interpretation *) -val transfer_plugin = Plugin_Name.declare_setup @{binding transfer} - fun transfer_bnf_interpretation bnf lthy = let val dead = dead_of_bnf bnf diff -r 77cd4992edcd -r d207455817e8 src/HOL/Transfer.thy --- a/src/HOL/Transfer.thy Fri Dec 19 14:06:13 2014 +0100 +++ b/src/HOL/Transfer.thy Mon Jan 05 06:56:15 2015 +0100 @@ -371,12 +371,6 @@ ML_file "Tools/Transfer/transfer_bnf.ML" ML_file "Tools/BNF/bnf_fp_rec_sugar_transfer.ML" -ML {* -val _ = Theory.setup (BNF_LFP_Rec_Sugar.primrec_interpretation - BNF_FP_Rec_Sugar_Transfer.primrec_transfer_pluginN - BNF_FP_Rec_Sugar_Transfer.primrec_transfer_interpretation) -*} - declare pred_fun_def [simp] declare rel_fun_eq [relator_eq]