--- 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 (\<real>\<^sup>n,dist\<^sub>\<infinity>) *)
fun embedding_tac ctxt metric_ty i goal =
let
@@ -228,7 +225,8 @@
(* replace point equality by equality of components in \<real>\<^sup>n *)
val eq2 = map (metric_eq_conv ctxt fset_ct) (find_eq metric_ty ct)
in
- ( K (trace_tac ctxt "Embedding into \<real>\<^sup>n") THEN' top_sweep_rewrs_tac ctxt (eq1 @ eq2))i goal
+ (K (trace_tac ctxt "Embedding into \<real>\<^sup>n") THEN'
+ CONVERSION (Conv.top_sweep_rewrs_conv (eq1 @ eq2) ctxt)) i goal
end
(* decision procedure for linear real arithmetic *)
--- 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>\<open>is_equality\<close>, Term.fastype_of t --> HOLogic.boolT) $ t;
--- 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'
--- 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 @
--- 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
--- 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>\<open>rel_fun\<close>, _) $ _ $ _ =>
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
--- 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>\<open>relcompp\<close>, _) $ Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ =>
--- 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 **)
--- 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 *)