--- a/Admin/components/components.sha1 Tue Oct 19 16:10:36 2021 +0200
+++ b/Admin/components/components.sha1 Tue Oct 19 18:24:33 2021 +0200
@@ -192,6 +192,7 @@
beb99f2cb0bd4e595c5c597d3970c46aa21616e4 jedit-20210717.tar.gz
33dd96cd83f2c6a26c035b7a0ee57624655224c5 jedit-20210724.tar.gz
0e4fd4d66388ddc760fa5fbd8d4a9a3b77cf59c7 jedit-20210802.tar.gz
+258d527819583d740a3aa52dfef630eed389f8c6 jedit-20211019.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Tue Oct 19 16:10:36 2021 +0200
+++ b/Admin/components/main Tue Oct 19 18:24:33 2021 +0200
@@ -10,7 +10,7 @@
isabelle_fonts-20211004
isabelle_setup-20210922
jdk-17+35
-jedit-20210802
+jedit-20211019
jfreechart-1.5.3
jortho-1.0-2
kodkodi-1.5.7
--- a/src/HOL/Analysis/Metric_Arith.thy Tue Oct 19 16:10:36 2021 +0200
+++ b/src/HOL/Analysis/Metric_Arith.thy Tue Oct 19 18:24:33 2021 +0200
@@ -1,5 +1,5 @@
-(* Title: Metric_Arith.thy
- Author: Maximilian Schäffeler (port from HOL Light)
+(* Title: HOL/Analysis/Metric_Arith.thy
+ Author: Maximilian Schäffeler (port from HOL Light)
*)
chapter \<open>Functional Analysis\<close>
@@ -108,7 +108,7 @@
ML_file "metric_arith.ML"
method_setup metric = \<open>
- Scan.succeed (SIMPLE_METHOD' o MetricArith.metric_arith_tac)
+ Scan.succeed (SIMPLE_METHOD' o Metric_Arith.metric_arith_tac)
\<close> "prove simple linear statements in metric spaces (\<forall>\<exists>\<^sub>p fragment)"
-end
\ No newline at end of file
+end
--- a/src/HOL/Analysis/metric_arith.ML Tue Oct 19 16:10:36 2021 +0200
+++ b/src/HOL/Analysis/metric_arith.ML Tue Oct 19 18:24:33 2021 +0200
@@ -1,9 +1,17 @@
-signature METRIC_ARITH = sig
+(* Title: HOL/Analysis/metric_arith.ML
+ Author: Maximilian Schäffeler (port from HOL Light)
+
+A decision procedure for metric spaces.
+*)
+
+signature METRIC_ARITH =
+sig
+ val trace: bool Config.T
val metric_arith_tac : Proof.context -> int -> tactic
- val trace: bool Config.T
end
-structure MetricArith : METRIC_ARITH = struct
+structure Metric_Arith : METRIC_ARITH =
+struct
fun default d x = case x of SOME y => SOME y | NONE => d
@@ -214,22 +222,19 @@
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 =
+fun embedding_tac ctxt metric_ty = CSUBGOAL (fn (goal, i) =>
let
- val ct = (Thm.cprem_of goal 1)
- val points = find_points ctxt metric_ty ct
+ val points = find_points ctxt metric_ty goal
val fset_ct = mk_ct_set ctxt metric_ty points
(* embed all subterms of the form "dist x y" in (\<real>\<^sup>n,dist\<^sub>\<infinity>) *)
- val eq1 = map (maxdist_conv ctxt fset_ct) (find_dist metric_ty ct)
+ val eq1 = map (maxdist_conv ctxt fset_ct) (find_dist metric_ty goal)
(* 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)
+ val eq2 = map (metric_eq_conv ctxt fset_ct) (find_eq metric_ty goal)
in
- ( K (trace_tac ctxt "Embedding into \<real>\<^sup>n") THEN' top_sweep_rewrs_tac ctxt (eq1 @ eq2))i goal
- end
+ (K (trace_tac ctxt "Embedding into \<real>\<^sup>n") THEN'
+ CONVERSION (Conv.top_sweep_rewrs_conv (eq1 @ eq2) ctxt)) i
+ end)
(* decision procedure for linear real arithmetic *)
fun lin_real_arith_tac ctxt metric_ty i goal =
@@ -320,4 +325,5 @@
IF_UNSOLVED' (SUBPROOF (fn {context=ctxt', ...} =>
trace_tac ctxt' "Focused on subgoal" THEN
elim_exists ctxt') ctxt)
+
end
--- a/src/HOL/Analysis/normarith.ML Tue Oct 19 16:10:36 2021 +0200
+++ b/src/HOL/Analysis/normarith.ML Tue Oct 19 18:24:33 2021 +0200
@@ -325,9 +325,9 @@
(map (fn t =>
Drule.instantiate_normalize (TVars.make [(tv_n, Thm.ctyp_of_cterm t)], Vars.empty) pth_zero)
zerodests,
- map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
+ map (fconv_rule (try_conv (Conv.top_sweep_conv norm_canon_conv ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) ges',
- map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
+ map (fconv_rule (try_conv (Conv.top_sweep_conv norm_canon_conv ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) gts))
end
in val real_vector_combo_prover = real_vector_combo_prover
--- a/src/HOL/Library/cconv.ML Tue Oct 19 16:10:36 2021 +0200
+++ b/src/HOL/Library/cconv.ML Tue Oct 19 18:24:33 2021 +0200
@@ -1,16 +1,15 @@
(* Title: HOL/Library/cconv.ML
Author: Christoph Traut, Lars Noschinski, TU Muenchen
-FIXME!?
+Conditional conversions.
*)
infix 1 then_cconv
infix 0 else_cconv
-type cconv = conv
-
signature BASIC_CCONV =
sig
+ type cconv = conv
val then_cconv: cconv * cconv -> cconv
val else_cconv: cconv * cconv -> cconv
val CCONVERSION: cconv -> int -> tactic
@@ -42,6 +41,8 @@
structure CConv : CCONV =
struct
+type cconv = conv
+
val concl_lhs_of = Thm.cprop_of #> Drule.strip_imp_concl #> Thm.dest_equals_lhs
val concl_rhs_of = Thm.cprop_of #> Drule.strip_imp_concl #> Thm.dest_equals_rhs
@@ -69,13 +70,7 @@
val no_cconv = Conv.no_conv
val all_cconv = Conv.all_conv
-
-fun (cv1 else_cconv cv2) ct =
- (cv1 ct
- handle THM _ => cv2 ct
- | CTERM _ => cv2 ct
- | TERM _ => cv2 ct
- | TYPE _ => cv2 ct)
+val op else_cconv = Conv.else_conv
fun (cv1 then_cconv cv2) ct =
let
--- a/src/HOL/Library/conditional_parametricity.ML Tue Oct 19 16:10:36 2021 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML Tue Oct 19 18:24:33 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/Library/rewrite.ML Tue Oct 19 16:10:36 2021 +0200
+++ b/src/HOL/Library/rewrite.ML Tue Oct 19 18:24:33 2021 +0200
@@ -263,7 +263,7 @@
fun rewrs_pconv to thms ctxt (tyenv, env_ts) =
let
- fun instantiate_normalize_env ctxt env thm =
+ fun instantiate_normalize_env env thm =
let
val prop = Thm.prop_of thm
val norm_type = Envir.norm_type o Envir.type_env
@@ -274,28 +274,28 @@
|> map (fn x => (x, Thm.ctyp_of ctxt (norm_type env (TVar x))))
in Drule.instantiate_normalize (TVars.make tyinsts, Vars.make insts) thm end
- fun unify_with_rhs context to env thm =
+ fun unify_with_rhs to env thm =
let
val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals
- val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env
+ val env' = Pattern.unify (Context.Proof ctxt) (Logic.mk_term to, Logic.mk_term rhs) env
handle Pattern.Unif => raise NO_TO_MATCH
in env' end
- fun inst_thm_to _ (NONE, _) thm = thm
- | inst_thm_to (ctxt : Proof.context) (SOME to, env) thm =
- instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm
+ fun inst_thm_to (NONE, _) thm = thm
+ | inst_thm_to (SOME to, env) thm =
+ instantiate_normalize_env (unify_with_rhs to env thm) thm
- fun inst_thm ctxt idents (to, tyenv) thm =
+ fun inst_thm idents (to, tyenv) thm =
let
(* Replace any identifiers with their corresponding bound variables. *)
val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0
val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv}
val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to)
val thm' = Thm.incr_indexes (maxidx + 1) thm
- in SOME (inst_thm_to ctxt (Option.map (replace_idents idents) to, env) thm') end
+ in SOME (inst_thm_to (Option.map (replace_idents idents) to, env) thm') end
handle NO_TO_MATCH => NONE
- in CConv.rewrs_cconv (map_filter (inst_thm ctxt env_ts (to, tyenv)) thms) end
+ in CConv.rewrs_cconv (map_filter (inst_thm env_ts (to, tyenv)) thms) end
fun rewrite_conv ctxt (pattern, to) thms ct =
let
@@ -320,7 +320,7 @@
let
val export = case pat_ctxt of
NONE => I
- | SOME inner => singleton (Proof_Context.export inner ctxt)
+ | SOME ctxt' => singleton (Proof_Context.export ctxt' ctxt)
in CCONVERSION (export o rewrite_conv ctxt pat thms) end
val _ =
@@ -349,7 +349,7 @@
let
val (r, toks') = scan toks
val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context
- in (r', (context', toks' : Token.T list)) end
+ in (r', (context', toks')) end
fun read_fixes fixes ctxt =
let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
@@ -448,6 +448,6 @@
Method.setup \<^binding>\<open>rewrite\<close> (subst_parser >>
(fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt =>
SIMPLE_METHOD' (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))
- "single-step rewriting, allowing subterm selection via patterns."
+ "single-step rewriting, allowing subterm selection via patterns"
end
end
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Tue Oct 19 16:10:36 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Tue Oct 19 18:24:33 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 16:10:36 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 19 18:24:33 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 16:10:36 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Tue Oct 19 18:24:33 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 16:10:36 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Tue Oct 19 18:24:33 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 16:10:36 2021 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Tue Oct 19 18:24:33 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 16:10:36 2021 +0200
+++ b/src/HOL/Tools/Transfer/transfer.ML Tue Oct 19 18:24:33 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/Admin/build_jedit.scala Tue Oct 19 16:10:36 2021 +0200
+++ b/src/Pure/Admin/build_jedit.scala Tue Oct 19 18:24:33 2021 +0200
@@ -98,7 +98,7 @@
"CommonControls" -> "1.7.4",
"Console" -> "5.1.4",
"ErrorList" -> "2.4.0",
- "Highlight" -> "2.2",
+ "Highlight" -> "2.5",
"Navigator" -> "2.7",
"SideKick" -> "1.8")
--- a/src/Pure/conv.ML Tue Oct 19 16:10:36 2021 +0200
+++ b/src/Pure/conv.ML Tue Oct 19 18:24:33 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 *)