# HG changeset patch # User wenzelm # Date 1634648302 -7200 # Node ID 6c123914883ab4f7b6c827c7f0146df85d627fbe # Parent 9864ab4c20cefc0b0bb2b98db24e9548310a7b53 clarified context; clarified modules; diff -r 9864ab4c20ce -r 6c123914883a src/HOL/Analysis/metric_arith.ML --- a/src/HOL/Analysis/metric_arith.ML Tue Oct 19 14:41:29 2021 +0200 +++ b/src/HOL/Analysis/metric_arith.ML Tue Oct 19 14:58:22 2021 +0200 @@ -214,9 +214,6 @@ in infer_instantiate' ctxt [SOME xct, SOME yct] @{thm zero_le_dist} end in map inst (find_dist metric_ty ct) end -fun top_sweep_rewrs_tac ctxt thms = - CONVERSION (Conv.top_sweep_conv (K (Conv.rewrs_conv thms)) ctxt) - (* apply maxdist_conv and metric_eq_conv to the goal, thereby embedding the goal in (\\<^sup>n,dist\<^sub>\) *) fun embedding_tac ctxt metric_ty i goal = let @@ -228,7 +225,8 @@ (* replace point equality by equality of components in \\<^sup>n *) val eq2 = map (metric_eq_conv ctxt fset_ct) (find_eq metric_ty ct) in - ( K (trace_tac ctxt "Embedding into \\<^sup>n") THEN' top_sweep_rewrs_tac ctxt (eq1 @ eq2))i goal + (K (trace_tac ctxt "Embedding into \\<^sup>n") THEN' + CONVERSION (Conv.top_sweep_rewrs_conv (eq1 @ eq2) ctxt)) i goal end (* decision procedure for linear real arithmetic *) diff -r 9864ab4c20ce -r 6c123914883a src/HOL/Library/conditional_parametricity.ML --- a/src/HOL/Library/conditional_parametricity.ML Tue Oct 19 14:41:29 2021 +0200 +++ b/src/HOL/Library/conditional_parametricity.ML Tue Oct 19 14:58:22 2021 +0200 @@ -384,7 +384,8 @@ fun transfer_rel_conv conv = Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv))); -fun fold_relator_eqs_conv ctxt ct = (Transfer.bottom_rewr_conv (Transfer.get_relator_eq ctxt)) ct; +fun fold_relator_eqs_conv ctxt = + Conv.bottom_rewrs_conv (Transfer.get_relator_eq ctxt) ctxt; fun mk_is_equality t = Const (\<^const_name>\is_equality\, Term.fastype_of t --> HOLogic.boolT) $ t; diff -r 9864ab4c20ce -r 6c123914883a src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Tue Oct 19 14:41:29 2021 +0200 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Tue Oct 19 14:58:22 2021 +0200 @@ -387,8 +387,8 @@ end; fun subst_conv ctxt thm = - Conv.arg_conv (Conv.arg_conv - (Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) ctxt)); + (Conv.arg_conv o Conv.arg_conv) + (Conv.top_sweep_rewrs_conv [safe_mk_meta_eq thm] ctxt); fun mk_rel_eq_onp_tac ctxt pred_def map_id0 rel_Grp = HEADGOAL (EVERY' diff -r 9864ab4c20ce -r 6c123914883a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 19 14:41:29 2021 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 19 14:58:22 2021 +0200 @@ -1341,11 +1341,9 @@ val pred_injects = let - fun top_sweep_rewr_conv rewrs = - Conv.top_sweep_conv (K (Conv.rewrs_conv rewrs)) \<^context>; - - val rel_eq_onp_with_tops_of = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv - (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))); + val rel_eq_onp_with_tops_of = + Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv + (Conv.top_sweep_rewrs_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} lthy))); val eq_onps = map rel_eq_onp_with_tops_of (map rel_eq_onp_of_bnf fp_bnfs @ fp_nesting_rel_eq_onps @ live_nesting_rel_eq_onps @ diff -r 9864ab4c20ce -r 6c123914883a src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Tue Oct 19 14:41:29 2021 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Tue Oct 19 14:58:22 2021 +0200 @@ -27,7 +27,7 @@ val vimage2p_unfolds = o_apply :: @{thms vimage2p_def}; fun unfold_at_most_once_tac ctxt thms = - CONVERSION (Conv.top_sweep_conv (K (Conv.rewrs_conv thms)) ctxt); + CONVERSION (Conv.top_sweep_rewrs_conv thms ctxt); val unfold_once_tac = CHANGED ooo unfold_at_most_once_tac; fun mk_rel_xtor_co_induct_tac fp abs_inverses co_inducts0 rel_defs rel_monos nesting_rel_eqs0 diff -r 9864ab4c20ce -r 6c123914883a src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Tue Oct 19 14:41:29 2021 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Tue Oct 19 14:58:22 2021 +0200 @@ -242,8 +242,9 @@ Const (\<^const_name>\rel_fun\, _) $ _ $ _ => binop_conv2 Conv.all_conv conv ctm | _ => conv ctm - fun R_conv rel_eq_onps = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} - then_conv Transfer.bottom_rewr_conv rel_eq_onps + fun R_conv rel_eq_onps ctxt = + Conv.top_sweep_rewrs_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} ctxt + then_conv Conv.bottom_rewrs_conv rel_eq_onps ctxt val (ret_lift_def, lthy1) = add_lift_def (#lift_config config) var qty rhs rsp_thm par_thms lthy in @@ -282,7 +283,8 @@ val f'_qty = strip_type qty |> fst |> rpair qty_isom |> op ---> val f'_rsp_rel = Lifting_Term.equiv_relation lthy3 (rty, f'_qty); val rsp = rsp_thm_of_lift_def lift_def - val rel_eq_onps_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (ret_rel_conv (R_conv rel_eq_onps))) + val rel_eq_onps_conv = + HOLogic.Trueprop_conv (Conv.fun2_conv (ret_rel_conv (R_conv rel_eq_onps lthy3))) val rsp_norm = Conv.fconv_rule rel_eq_onps_conv rsp val f'_rsp_goal = HOLogic.mk_Trueprop (f'_rsp_rel $ rhs $ rhs); val f'_rsp = Goal.prove_sorry lthy3 [] [] f'_rsp_goal @@ -558,9 +560,11 @@ else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.") val rel_eq_onp = safe_mk_meta_eq (Transfer.rel_eq_onp pred_data); val rel_eq_onps = insert Thm.eq_thm rel_eq_onp rel_eq_onps - val R_conv = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} + fun R_conv ctxt = + Conv.top_sweep_rewrs_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} ctxt then_conv Conv.rewr_conv rel_eq_onp - val quot_thm = Conv.fconv_rule(HOLogic.Trueprop_conv (Quotient_R_conv R_conv)) quot_thm; + val quot_thm = + Conv.fconv_rule (HOLogic.Trueprop_conv (Quotient_R_conv (R_conv lthy0))) quot_thm; in if is_none (code_dt_of lthy0 (rty, qty)) then let @@ -685,7 +689,7 @@ val eq_onp_assms_tac_rules = @{thm left_unique_OO} :: eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw ctxt) val intro_top_rule = @{thm eq_onp_top_eq_eq[symmetric, THEN eq_reflection]} - val kill_tops = Transfer.top_sweep_rewr_conv [@{thm eq_onp_top_eq_eq[THEN eq_reflection]}] + val kill_tops = Conv.top_sweep_rewrs_conv @{thms eq_onp_top_eq_eq[THEN eq_reflection]} ctxt val eq_onp_assms_tac = (CONVERSION kill_tops THEN' TRY o REPEAT_ALL_NEW (resolve_tac ctxt eq_onp_assms_tac_rules) THEN_ALL_NEW (DETERM o Transfer.eq_tac ctxt)) 1 @@ -705,7 +709,7 @@ val unfold_ret_val_invs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) ctxt val unfold_inv_conv = - Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) ctxt + Conv.top_sweep_rewrs_conv @{thms eq_onp_def[THEN eq_reflection]} ctxt val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv) val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]} val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) ctxt diff -r 9864ab4c20ce -r 6c123914883a src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Oct 19 14:41:29 2021 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Oct 19 14:58:22 2021 +0200 @@ -148,7 +148,7 @@ pcr_rel_def |> infer_instantiate args_ctxt args_inst |> Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv - (Transfer.bottom_rewr_conv (Transfer.get_relator_eq args_ctxt)))) + (Conv.bottom_rewrs_conv (Transfer.get_relator_eq args_ctxt) args_ctxt))) in case (Thm.term_of o Thm.rhs_of) pcr_cr_eq of Const (\<^const_name>\relcompp\, _) $ Const (\<^const_name>\HOL.eq\, _) $ _ => diff -r 9864ab4c20ce -r 6c123914883a src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Tue Oct 19 14:41:29 2021 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Tue Oct 19 14:58:22 2021 +0200 @@ -13,11 +13,6 @@ val pred_def: pred_data -> thm val pred_simps: pred_data -> thm list val update_pred_simps: thm list -> pred_data -> pred_data - - val bottom_rewr_conv: thm list -> conv - val top_rewr_conv: thm list -> conv - val top_sweep_rewr_conv: thm list -> conv - val prep_conv: conv val fold_relator_eqs_conv: Proof.context -> conv val unfold_relator_eqs_conv: Proof.context -> conv @@ -57,9 +52,6 @@ structure Transfer : TRANSFER = struct -fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) \<^context> -fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) \<^context> -fun top_sweep_rewr_conv rewrs = Conv.top_sweep_conv (K (Conv.rewrs_conv rewrs)) \<^context> (** Theory Data **) @@ -228,8 +220,8 @@ else_conv Conv.all_conv) ct -fun fold_relator_eqs_conv ctxt ct = (bottom_rewr_conv (get_relator_eq ctxt)) ct; -fun unfold_relator_eqs_conv ctxt ct = (top_rewr_conv (get_sym_relator_eq ctxt)) ct; +fun fold_relator_eqs_conv ctxt = Conv.bottom_rewrs_conv (get_relator_eq ctxt) ctxt +fun unfold_relator_eqs_conv ctxt = Conv.top_rewrs_conv (get_sym_relator_eq ctxt) ctxt (** Replacing explicit equalities with is_equality premises **) diff -r 9864ab4c20ce -r 6c123914883a src/Pure/conv.ML --- a/src/Pure/conv.ML Tue Oct 19 14:41:29 2021 +0200 +++ b/src/Pure/conv.ML Tue Oct 19 14:58:22 2021 +0200 @@ -39,6 +39,9 @@ val implies_concl_conv: conv -> conv val rewr_conv: thm -> conv val rewrs_conv: thm list -> conv + val bottom_rewrs_conv: thm list -> Proof.context -> conv + val top_rewrs_conv: thm list -> Proof.context -> conv + val top_sweep_rewrs_conv: thm list -> Proof.context -> conv val sub_conv: (Proof.context -> conv) -> Proof.context -> conv val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv val top_conv: (Proof.context -> conv) -> Proof.context -> conv @@ -153,8 +156,9 @@ | _ => raise CTERM ("implies_concl_conv", [ct])); -(* single rewrite step, cf. REWR_CONV in HOL *) +(* rewrite steps *) +(*cf. REWR_CONV in HOL*) fun rewr_conv rule ct = let val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule; @@ -172,6 +176,10 @@ fun rewrs_conv rules = first_conv (map rewr_conv rules); +fun bottom_rewrs_conv rewrs = bottom_conv (K (try_conv (rewrs_conv rewrs))); +fun top_rewrs_conv rewrs = top_conv (K (try_conv (rewrs_conv rewrs))); +fun top_sweep_rewrs_conv rewrs = top_sweep_conv (K (rewrs_conv rewrs)); + (* conversions on HHF rules *)