# HG changeset patch # User blanchet # Date 1420534783 -3600 # Node ID 7ca42387fbf57f242ba0c9e8658f3632d251fb5b # Parent 002d817b4c377152c9080ef743191c20e8a9f3c1 tuning diff -r 002d817b4c37 -r 7ca42387fbf5 src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Mon Jan 05 18:39:32 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_transfer.ML Tue Jan 06 09:59:43 2015 +0100 @@ -18,6 +18,7 @@ open Ctr_Sugar_Util open Ctr_Sugar_Tactics +open BNF_Util open BNF_Def open BNF_FP_Util open BNF_FP_Def_Sugar @@ -27,29 +28,27 @@ val transferN = "transfer"; fun mk_lfp_rec_sugar_transfer_tac ctxt def = - Ctr_Sugar_Tactics.unfold_thms_tac ctxt [def] THEN - HEADGOAL (Transfer.transfer_prover_tac ctxt); + unfold_thms_tac ctxt [def] THEN HEADGOAL (Transfer.transfer_prover_tac ctxt); -fun mk_gfp_rec_sugar_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 = +fun mk_gfp_rec_sugar_transfer_tac ctxt f_def corec_def type_definitions 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 prop as @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, fT) $ _) $ _) = + Thm.prop_of thm; val T = range_type fT; 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); + val lam = Term.lambda cond (mk_If cond then_branch else_branch); in - cterm_instantiate_pos [SOME (certify ctxt lambda)] thm + cterm_instantiate_pos [SOME (certify ctxt lam)] thm end; val transfer_rules = - @{thm Abs_transfer[OF BNF_Composition.type_definition_id_bnf_UNIV - BNF_Composition.type_definition_id_bnf_UNIV]} :: + @{thm Abs_transfer[OF type_definition_id_bnf_UNIV 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; @@ -57,74 +56,63 @@ val case_distribs = map instantiate_with_lambda case_distribs; val simps = case_distribs @ disc_eq_cases @ cases @ @{thms if_True if_False}; - val simp_ctxt = put_simpset (simpset_of (ss_only simps ctxt)) ctxt'; + val ctxt'' = put_simpset (simpset_of (ss_only simps ctxt)) ctxt'; in unfold_thms_tac ctxt ([f_def, corec_def] @ @{thms split_beta if_conn}) THEN - HEADGOAL (simp_tac (fold Simplifier.add_cong case_congs simp_ctxt)) THEN - (if apply_transfer then HEADGOAL (Transfer.transfer_prover_tac ctxt') else all_tac) + HEADGOAL (simp_tac (fold Simplifier.add_cong case_congs ctxt'')) THEN + HEADGOAL (Transfer.transfer_prover_tac ctxt') end; fun massage_simple_notes base = filter_out (null o #2) #> map (fn (thmN, thms, f_attrs) => ((Binding.qualify true base (Binding.name thmN), []), - map_index (fn (i, thm) => ([thm], f_attrs i)) thms)); + map_index (fn (kk, thm) => ([thm], f_attrs kk)) thms)); fun fp_sugar_of_bnf ctxt = fp_sugar_of ctxt o (fn Type (s, _) => s) o T_of_bnf; -fun bnf_depth_first_traverse ctxt f T z = +fun bnf_depth_first_traverse ctxt f T = (case T of - Type (s, innerTs) => + Type (s, Ts) => (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) - -fun if_all_bnfs ctxt Ts f g = - 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; + NONE => I + | SOME bnf => fold (bnf_depth_first_traverse ctxt f) Ts o f bnf) + | _ => I); fun mk_goal lthy f = let val skematic_Ts = Term.add_tvarsT (fastype_of f) []; val ((As, Bs), names_lthy) = lthy - |> Ctr_Sugar_Util.mk_TFrees' (map snd skematic_Ts) - ||>> Ctr_Sugar_Util.mk_TFrees' (map snd skematic_Ts); + |> mk_TFrees' (map snd skematic_Ts) + ||>> 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 (Rs, names_lthy) = mk_Frees "R" (map2 mk_pred2T As Bs) names_lthy; 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) + (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 +fun fp_rec_sugar_transfer_interpretation prove {transfers, fun_names, funs, fun_defs, fpTs} = + fold_index (fn (kk, (((transfer, fun_name), funx), fun_def)) => fn lthy => + if transfer then + (case try (map the) (map (fn Type (s, _) => bnf_of lthy s | _ => NONE) fpTs) of + NONE => error "No transfer rule possible" + | SOME bnfs => + (case try (prove kk bnfs funx fun_def) lthy of + NONE => error "Failed to prove transfer rule" + | SOME thm => + let + val notes = [(transferN, [thm], K @{attributes [transfer_rule]})] + |> massage_simple_notes fun_name; + in + snd (Local_Theory.notes notes lthy) + end)) else - if_all_bnfs lthy fpTs - (fn bnfs => fn () => prove n bnfs f_names f def lthy) - (fn () => error "Function is not parametric" (*FIXME: wording*)) ()) - (transfers ~~ fun_names ~~ funs ~~ fun_defs) lthy; - -fun fp_rec_sugar_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" - | SOME thm => - let - val notes = [(transferN, [thm], K @{attributes [transfer_rule]})] - |> massage_simple_notes f_name; - in - snd (Local_Theory.notes notes lthy) - end)); + lthy) + (transfers ~~ fun_names ~~ funs ~~ fun_defs); val lfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation (fn _ => fn _ => fn f => fn def => fn lthy => @@ -136,28 +124,26 @@ end); val gfp_rec_sugar_transfer_interpretation = fp_rec_sugar_transfer_interpretation - (fn n => fn bnfs => fn f => fn def => fn lthy => + (fn kk => fn bnfs => fn f => fn def => fn lthy => let 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 quad => - let - 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 - Option.map (add_thms quad) (fp_sugar_of_bnf lthy bnf) - |> the_default quad - end) (fastype_of f) ([], [], [], []); + bnf_depth_first_traverse lthy (fn bnf => + (case fp_sugar_of_bnf lthy bnf of + NONE => I + | SOME {fp_ctr_sugar = {ctr_sugar = {disc_eq_cases, case_thms, case_distribs, + case_cong, ...}, ...}, ...} => + (fn (disc_eq_cases0, case_thms0, case_distribs0, case_congs0) => + (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)))) + (fastype_of f) ([], [], [], []); in Goal.prove lthy [] [] goal (fn {context = ctxt, prems = _} => - mk_gfp_rec_sugar_transfer_tac true ctxt def - (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars n))) + mk_gfp_rec_sugar_transfer_tac ctxt def + (#co_rec_def (#fp_co_induct_sugar (nth fp_sugars kk))) (map (#type_definition o #absT_info) fp_sugars) (maps (#xtor_co_rec_transfers o #fp_res) fp_sugars) (map (rel_def_of_bnf o #pre_bnf) fp_sugars)