# HG changeset patch # User desharna # Date 1634715097 -7200 # Node ID 67c4004495f24a760f71c01e2ba815e8fb9905c4 # Parent 3ec9cafab99090715c7c6d285840e4de7471b816# Parent 375e8e1a2139a2466fb86814db2125a18ac5bdc2 merged diff -r 3ec9cafab990 -r 67c4004495f2 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Tue Oct 19 11:48:31 2021 +0200 +++ b/Admin/components/components.sha1 Wed Oct 20 09:31:37 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 diff -r 3ec9cafab990 -r 67c4004495f2 Admin/components/main --- a/Admin/components/main Tue Oct 19 11:48:31 2021 +0200 +++ b/Admin/components/main Wed Oct 20 09:31:37 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 diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Analysis/Metric_Arith.thy --- a/src/HOL/Analysis/Metric_Arith.thy Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Analysis/Metric_Arith.thy Wed Oct 20 09:31:37 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 \Functional Analysis\ @@ -108,7 +108,7 @@ ML_file "metric_arith.ML" method_setup metric = \ - Scan.succeed (SIMPLE_METHOD' o MetricArith.metric_arith_tac) + Scan.succeed (SIMPLE_METHOD' o Metric_Arith.metric_arith_tac) \ "prove simple linear statements in metric spaces (\\\<^sub>p fragment)" -end \ No newline at end of file +end diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Analysis/Simplex_Content.thy --- a/src/HOL/Analysis/Simplex_Content.thy Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Analysis/Simplex_Content.thy Wed Oct 20 09:31:37 2021 +0200 @@ -1,6 +1,6 @@ (* File: Analysis/Simplex_Content.thy - Author: Manuel Eberl + Author: Manuel Eberl The content of an n-dimensional simplex, including the formula for the content of a triangle and Heron's formula. diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Analysis/metric_arith.ML --- a/src/HOL/Analysis/metric_arith.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Analysis/metric_arith.ML Wed Oct 20 09:31:37 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 (\\<^sup>n,dist\<^sub>\) *) -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 (\\<^sup>n,dist\<^sub>\) *) - 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 \\<^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 \\<^sup>n") THEN' top_sweep_rewrs_tac ctxt (eq1 @ eq2))i goal - end + (K (trace_tac ctxt "Embedding into \\<^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 diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Analysis/normarith.ML --- a/src/HOL/Analysis/normarith.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Analysis/normarith.ML Wed Oct 20 09:31:37 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 diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Computational_Algebra/Factorial_Ring.thy --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Wed Oct 20 09:31:37 2021 +0200 @@ -313,7 +313,7 @@ context begin -private lemma prime_elem_powerD: +lemma prime_elem_powerD: assumes "prime_elem (p ^ n)" shows "prime_elem p \ n = 1" proof (cases n) diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Computational_Algebra/Nth_Powers.thy --- a/src/HOL/Computational_Algebra/Nth_Powers.thy Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Computational_Algebra/Nth_Powers.thy Wed Oct 20 09:31:37 2021 +0200 @@ -1,6 +1,6 @@ (* File: HOL/Computational_Algebra/Nth_Powers.thy - Author: Manuel Eberl + Author: Manuel Eberl n-th powers in general and n-th roots of natural numbers *) diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Computational_Algebra/Polynomial_Factorial.thy --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Wed Oct 20 09:31:37 2021 +0200 @@ -525,7 +525,7 @@ qed qed -private lemma irreducible_imp_prime_poly: +lemma irreducible_imp_prime_poly: fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly" assumes "irreducible p" shows "prime_elem p" @@ -615,7 +615,7 @@ subsection \Prime factorisation of polynomials\ -private lemma poly_prime_factorization_exists_content_1: +lemma poly_prime_factorization_exists_content_1: fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide,semiring_gcd_mult_normalize} poly" assumes "p \ 0" "content p = 1" shows "\A. (\p. p \# A \ prime_elem p) \ prod_mset A = normalize p" diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Computational_Algebra/Squarefree.thy --- a/src/HOL/Computational_Algebra/Squarefree.thy Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Computational_Algebra/Squarefree.thy Wed Oct 20 09:31:37 2021 +0200 @@ -1,6 +1,6 @@ (* File: HOL/Computational_Algebra/Squarefree.thy - Author: Manuel Eberl + Author: Manuel Eberl Squarefreeness and decomposition of ring elements into square part and squarefree part *) diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Library/Landau_Symbols.thy --- a/src/HOL/Library/Landau_Symbols.thy Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Library/Landau_Symbols.thy Wed Oct 20 09:31:37 2021 +0200 @@ -1,6 +1,6 @@ (* File: Landau_Symbols_Definition.thy - Author: Manuel Eberl + Author: Manuel Eberl Landau symbols for reasoning about the asymptotic growth of functions. *) diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Library/cconv.ML --- a/src/HOL/Library/cconv.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Library/cconv.ML Wed Oct 20 09:31:37 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 diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Library/conditional_parametricity.ML --- a/src/HOL/Library/conditional_parametricity.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Library/conditional_parametricity.ML Wed Oct 20 09:31:37 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 3ec9cafab990 -r 67c4004495f2 src/HOL/Library/rewrite.ML --- a/src/HOL/Library/rewrite.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Library/rewrite.ML Wed Oct 20 09:31:37 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>\rewrite\ (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 diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Number_Theory/Prime_Powers.thy --- a/src/HOL/Number_Theory/Prime_Powers.thy Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Number_Theory/Prime_Powers.thy Wed Oct 20 09:31:37 2021 +0200 @@ -1,6 +1,6 @@ (* File: HOL/Number_Theory/Prime_Powers.thy - Author: Manuel Eberl + Author: Manuel Eberl Prime powers and the Mangoldt function *) diff -r 3ec9cafab990 -r 67c4004495f2 src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Oct 20 09:31:37 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 3ec9cafab990 -r 67c4004495f2 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Oct 20 09:31:37 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 3ec9cafab990 -r 67c4004495f2 src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Wed Oct 20 09:31:37 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 3ec9cafab990 -r 67c4004495f2 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Wed Oct 20 09:31:37 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 3ec9cafab990 -r 67c4004495f2 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Wed Oct 20 09:31:37 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 3ec9cafab990 -r 67c4004495f2 src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Wed Oct 20 09:31:37 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 3ec9cafab990 -r 67c4004495f2 src/Pure/Admin/build_jedit.scala --- a/src/Pure/Admin/build_jedit.scala Tue Oct 19 11:48:31 2021 +0200 +++ b/src/Pure/Admin/build_jedit.scala Wed Oct 20 09:31:37 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") diff -r 3ec9cafab990 -r 67c4004495f2 src/Pure/conv.ML --- a/src/Pure/conv.ML Tue Oct 19 11:48:31 2021 +0200 +++ b/src/Pure/conv.ML Wed Oct 20 09:31:37 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 *)