update for Isabelle2025.

Author: yutakang

Abduction/Abduction.thy

@@ -90,12 +90,7 @@ val long_keyword =
 val long_statement =
   Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts --
   Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
-    >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl))
-: Token.T list ->
-  (bool * Attrib.binding * (xstring * Position.T) list *
-   Element.context list * Element.statement)
-  *
-  Token.T list;
+    >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));
 
 val short_statement =
   Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes

PSL/Subtool.ML

@@ -43,7 +43,7 @@ fun nontac (timeout:real) (state:Proof.state) =
     fun trace_cexm _    = show_trace "Quickcheck.quickcheck found a  counterexample";
     fun trace_scexn _   = show_trace ("Quickcheck.quickcheck found a potentially spurious " ^
                                       "counterexample due to underspecified functions");
-    fun trace_to to     = show_trace ("Quickcheck timed out after " ^ Timeout.print to);
+    fun trace_to to     = show_trace ("Quickcheck timed out after " ^ Timeout.message to);
     val timeout         = Isabelle_Utils.timeout_apply (seconds timeout);
     fun get_result _    =  (case timeout (quickcheck [] 1) state of
       NONE => (trace_no_cexm (); single)
@@ -69,7 +69,7 @@ fun state_stttac (timeout:real) (state:Proof.state) (log:Dynamic_Utils.log) =
     val timeout            = Isabelle_Utils.timeout_apply (seconds timeout);
     val do_trace           = false;
     fun show_trace text    = if do_trace then tracing text else ();
-    fun trace_to to        = show_trace ("Nitpick timed out after " ^ Timeout.print to);
+    fun trace_to to        = show_trace ("Nitpick timed out after " ^ Timeout.message to);
     fun nitpick_result' _  = Nitpick.pick_nits_in_subgoal state params Nitpick.Normal 1 1;
     val nitpick_result     = timeout nitpick_result' () handle Timeout.TIMEOUT to => (trace_to to; ("timeout", []));
     (*"genuine" means "genuine counter-example".*)
@@ -198,13 +198,13 @@ fun hammer_logtac (timeout:real) (pstate:Proof.state): (Dynamic_Utils.log * Proo
     fun did_smt_timeout (out::timed::_) = (Utils.are_same ("out)", out)) andalso
                                           (Utils.are_same ("timed", timed))
      |  did_smt_timeout _  = error "Something went wrong in Subtool.ML";
-    val one_line_apply     = orig_string <$> space_explode " "
+    val one_line_apply     = orig_string <$> Isabelle_Utils.YXML_content_of <$> space_explode " "
                             <$> drop 2                           (* drop "Try this:"*)
                             <$> rev <$> (fn tokens =>
                                 if did_smt_timeout tokens then drop 5 tokens else drop 2 tokens)
                             <$> rev           (* drop "(0.1 ms)." and such.*)
                             <$> String.concatWith " "            : string option;
-    val apply_script_cntnt = omap YXML.content_of one_line_apply : string option;
+    val apply_script_cntnt = omap Isabelle_Utils.YXML_content_of one_line_apply : string option;
     val sh_returned        = if is_some apply_script_cntnt
                              then valOf result |> fst else false : bool;
   in

README.md

@@ -1,10 +1,5 @@
-# Note on Isabelle2024 and its Sledgehammer
-This repository has been updated to Isabelle2024. However, we have received reports that the integration of Sledgehammer with this repository is now less stable under Isabelle2024. Therefore, although we have confirmed that the Abduction Prover works in some cases, its performance may currently be suboptimal. We are working to resolve this issue as quickly as possible. 🙇
-
-For users seeking the best performance, we recommend using Isabelle2023 and [this version of the Abduction Prover (v0.2.7-alpha)](https://github.com/data61/PSL/releases/tag/v0.2.7-alpha), which was developed specifically for Isabelle2023."
-
 # News
-- We updated this repository to Isabelle2024.
+- We updated this repository to Isabelle2025.
 - _NEW_: The introduction of **Abduction Prover**. You can watch a demo of Abduction Prover in [our YouTube channel](https://youtu.be/d7IXk0vB2p0).
 - LiFtEr and Smart_Induct are no-longer supported, since their successors, SeLFiE and sem_ind, have shown superior performance.
 - _PaMpeR is currently not supported either,_ since we want to minimise the cost necessary to maintain this repository. 
@@ -15,7 +10,7 @@ For users seeking the best performance, we recommend using Isabelle2023 and [thi
 
 This repository contains various tools to support interactive theorem proving in Isabelle/HOL using artificial intelligence.
 This repository contains the implementation of *proof strategy language (PSL)* and its default strategy,
-**try_hard**, for [Isabelle2024](https://isabelle.in.tum.de). Past versions of Isabelle, such as Isabelle2022-1, are no longer supported.
+**try_hard**, for [Isabelle2025](https://isabelle.in.tum.de). Past versions of Isabelle, such as Isabelle2022-1, are no longer supported.
 
 ## YouTube
 
@@ -25,19 +20,19 @@ We opened [a YouTube channel](https://www.youtube.com/channel/UCjnY6hIaryOEgG92u
 
 
 ## Installation (of SeLFiE, PSL, and sem_ind in one go) (for MacOS/Lunux users)
-1. Install [Isabelle2024](https://isabelle.in.tum.de).
+1. Install [Isabelle2025](https://isabelle.in.tum.de).
 2. Download or clone this repository (git clone https://github.com/data61/PSL.git).
 3. Open Isabelle/jEdit with PSL and all that. You can do this by opening Isabelle/jEdit as following:
    * `(path to the Isabelle binary)isabelle jedit -d (path to the directory that contains this README file) -l Smart_Isabelle`
    * If you are a MacOS user and your current directory is this one with this README.md, probably you should type something like this in Terminal:
-   * `/Applications/Isabelle2024.app/bin/isabelle jedit -d . -l Smart_Isabelle`
+   * `/Applications/Isabelle2025.app/bin/isabelle jedit -d . -l Smart_Isabelle`
 4. Then, You can use SeLFiE/PSL/sem_ind to your theory files
    with the Isabelle keyword, **imports** as ``imports "Smart_Isabelle.Smart_Isabelle"``.
 5. Open `Example/Example.thy` to see if the installation is successful.
 
 ### Note on installation for Windows users
 The basic steps are the same as MacOS and Linux. 
-However, instead of using the binary file directly, use `Isabelle2024\Cygwin-Terminal` in Command Prompt. Once you start `Isabelle2024\Cygwin-Terminal`, you can install our tools by typing `isabelle jedit -d (path to the directory that contains this README file) -l Smart_Isabelle`. Note that once you started `Isabelle2024\Cygwin-Terminal`, you should not specify the path to the Isabelle binary file. Therefore, the command you need after starting `Isabelle2024\Cygwin-Terminal` is something like `isabelle jedit -d . -l Smart_Isabelle`, assuming that your current directory is this one with this README.md/
+However, instead of using the binary file directly, use `Isabelle2025\Cygwin-Terminal` in Command Prompt. Once you start `Isabelle2025\Cygwin-Terminal`, you can install our tools by typing `isabelle jedit -d (path to the directory that contains this README file) -l Smart_Isabelle`. Note that once you started `Isabelle2025\Cygwin-Terminal`, you should not specify the path to the Isabelle binary file. Therefore, the command you need after starting `Isabelle2025\Cygwin-Terminal` is something like `isabelle jedit -d . -l Smart_Isabelle`, assuming that your current directory is this one with this README.md/
 
 ![Screenshot](./image/screen_shot_import.png)
 

SeLFiE/Util.ML

@@ -488,6 +488,7 @@ sig
   val strip_atyp                                  : term -> term;
   val takes_n_arguments                           : term -> int -> bool;
   val read_term_then_check_term                   : Proof.context -> string -> (term -> bool) -> bool;
+  val YXML_content_of                             : string -> string;
 end;
 
 (*** Isabelle_Utils : Utility functions specific to Isabelle/HOL. ***)
@@ -707,7 +708,7 @@ fun is_in_Main (ctxt:Proof.context) (thm:thm) =
     val thy_names_in_main = Context.get_theory {long=false} this_thy "Main"
       |> Theory.ancestors_of
       |> map (Context.theory_name {long=true}):strings;
-    fun get_theory_name (thm:thm) = thm |> Thm.get_name_hint |> fst_qualifier;
+    fun get_theory_name (thm:thm) = thm |> Thm.get_name_hint |> Thm_Name.short |> fst_qualifier;
     val thy_name = get_theory_name thm;
     val result = exists (equal thy_name) thy_names_in_main;
   in
@@ -926,14 +927,18 @@ fun normalize_trm_as_string (ctxt:Proof.context) (trm_as_string:string) =
     Syntax.read_term ctxt trm_as_string |> trm_to_string ctxt: string;
 
 (*This contract_abbrevs is a modified version of contract_abbrevs in Pure/Isar/proof_context.ML.*)
-fun contract_abbrevs (ctxt:Proof.context) (t:term) =
+fun contract_abbrevs ctxt tm =
   let
-    val thy            = Proof_Context.theory_of ctxt;
-    val consts         = Proof_Context.consts_of ctxt;
-    val retrieve       = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
-    fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
+    val thy = Proof_Context.theory_of ctxt;
+    val consts = Proof_Context.consts_of ctxt;
+    val inst = #1 (Variable.import_inst true [tm] ctxt);
+    val nets = Consts.revert_abbrevs consts (print_mode_value () @ [""]);
+    val rew = Option.map #1 oo Pattern.match_rew thy;
+    fun match_abbrev t = get_first (fn net => get_first (rew t) (Item_Net.retrieve net t)) nets;
   in
-    Pattern.rewrite_term_top thy [] [match_abbrev] t
+    Term_Subst.instantiate inst tm
+    |> Pattern.rewrite_term_yoyo thy [] [match_abbrev]
+    |> Term_Subst.instantiate_frees (Variable.import_inst_revert inst)
   end;
 
 val strip_atyp = Term.map_types (map_atyps (K dummyT)): term -> term;
@@ -945,6 +950,8 @@ fun read_term_then_check_term (ctxt:Proof.context) (print:string) (checker: term
 <$> checker
  |> Utils.is_some_true
 
+val YXML_content_of = YXML.parse_body #> XML.content_of;
+
 end;
 
 (*** FIND_THEOREMS2: provides an interface of find_theorem for PSL. ***)
@@ -956,8 +963,7 @@ signature FIND_THEOREMS2 =
 sig
   include FIND_THEOREMS;
   type context;
-  type ref;
-  type get_rules           = context -> thm -> (ref * thm) list;
+  type get_rules           = context -> thm -> (string * thm) list;
   type get_rule_names      = context -> thm -> strings;
   type pstate_to_thms      = Proof.state -> thms;
   type pstate_to_thm_names = Proof.state -> strings;
@@ -997,8 +1003,8 @@ fun (m liftM f) = Option.map f m;
 open Find_Theorems;
 
 type context = Proof.context;
-type ref = Facts.ref;
-type get_rules = context -> thm -> (ref * thm) list;
+type fact_name = string;
+type get_rules = context -> thm -> (fact_name * thm) list;
 type get_rule_names = context -> thm -> strings;
 type pstate_to_thms      = Proof.state -> thms;
 type pstate_to_thm_names = Proof.state -> strings;
@@ -1007,17 +1013,18 @@ fun get_criterion kind_name ([]:strings) = [(true, Name kind_name)]
   | get_criterion kind_name (name::names:strings) = (true, Name name)::get_criterion kind_name names;
 
 fun all_names_to_rules kind_name (names:strings) ctxt (_(*just for type checking*):thm) =
-  try (find_theorems ctxt NONE NONE true) (get_criterion kind_name names) liftM snd |> Utils.is_some_null;
+  try (find_theorems ctxt NONE NONE true) (get_criterion kind_name names) liftM snd |> Utils.is_some_null
+|> map (apfst Thm_Name.print);
 
-fun some_names_to_rules kind_name names ctxt goal = names
-  |> map (fn name:string => all_names_to_rules kind_name [name] ctxt goal)
+fun some_names_to_rules kind_name names ctxt goal: (string * thm) list = names
+  |> map (fn name:string => all_names_to_rules kind_name [name] ctxt goal: (string * thm) list)
   |> flat
   |> distinct (Thm.eq_thm o Utils.map_pair snd);
 
-fun get_rule_names (get_rules:context -> thm -> (ref * thm) list) ctxt goal =
+fun get_rule_names (get_rules:context -> thm -> (string * thm) list) ctxt goal =
   let
     val related_rules          = get_rules ctxt goal;
-    val related_rule_names     = map (Facts.string_of_ref o fst) related_rules;
+    val related_rule_names     = map fst related_rules;
     fun get_thm  thm_nm        = SOME (Proof_Context.get_thm  ctxt thm_nm) handle ERROR _ => NONE;
     fun get_thms thm_nm        = SOME (Proof_Context.get_thms ctxt
       (Utils.rm_parentheses_with_contents_in_the_end thm_nm)) handle ERROR _ => NONE;
@@ -1032,12 +1039,12 @@ fun get_rule_names (get_rules:context -> thm -> (ref * thm) list) ctxt goal =
 fun get_simp_rules (ctxt:context) (goal:thm) =
   let
     val cnames   = Isabelle_Utils.get_cnames_in_1st_subg goal;
-    val related_rules = some_names_to_rules "" cnames ctxt goal;
+    val related_rules = some_names_to_rules "" cnames ctxt goal: (string * thm) list;
     val simpset_thms  = ctxt |> simpset_of |> Raw_Simplifier.dest_ss |> #simps |> map snd;
     fun eq_test (thm1, (_, thm2)) = Thm.eq_thm (thm1, thm2);
     val unique_rules  = subtract eq_test simpset_thms related_rules;
   in
-    unique_rules : (Facts.ref * thm) list
+    unique_rules : (string * thm) list
   end;
 
 fun get_simp_rule_names ctxt goal = get_rule_names get_simp_rules ctxt goal : strings;
@@ -1047,7 +1054,7 @@ fun get_induct_rules (ctxt:context) (goal:thm) =
     val cnames  = Isabelle_Utils.get_cnames_in_1st_subg goal         : strings;
     val induct_rules = some_names_to_rules ".induct" cnames ctxt goal;
   in
-    induct_rules : (Facts.ref * thm) list
+    induct_rules : (string * thm) list
   end;
 
 fun get_induct_rule_names ctxt goal = get_rule_names get_induct_rules ctxt goal : strings;
@@ -1101,14 +1108,16 @@ fun get_coinduction_rules (ctxt:context) (goal:thm) =
     val coinduct_rules1 = get_coinduct_rules ".coinduct";
     val coinduct_rules2 = get_coinduct_rules ".coinduct_strong";
   in
-    coinduct_rules1 @ coinduct_rules2: (Facts.ref * thm) list
+    coinduct_rules1 @ coinduct_rules2: (string * thm) list
   end;
 
 fun get_coinduction_rule_names ctxt goal = get_rule_names get_coinduction_rules ctxt goal : strings;
 
-fun get_elim_rules  ctxt goal = find_theorems ctxt (SOME goal) NONE true [(true, Elim)] |> snd;
-fun get_intro_rules ctxt goal = find_theorems ctxt (SOME goal) (SOME 100) true [(true, Intro)] |> snd;
-fun get_dest_rules  ctxt goal = find_theorems ctxt (SOME goal) (SOME 100) true [(true, Dest)] |> snd;
+fun post_proc (_, pairs: (Thm_Name.T * thm) list) = map (apfst Thm_Name.print) pairs: (string * thm) list;
+
+fun get_elim_rules  ctxt goal = find_theorems ctxt (SOME goal) NONE true [(true, Elim)] |> post_proc;
+fun get_intro_rules ctxt goal = find_theorems ctxt (SOME goal) (SOME 100) true [(true, Intro)] |> post_proc;
+fun get_dest_rules  ctxt goal = find_theorems ctxt (SOME goal) (SOME 100) true [(true, Dest)] |> post_proc;
 
 fun get_elim_rule_names  ctxt goal = get_rule_names get_elim_rules  ctxt goal : strings;
 fun get_intro_rule_names ctxt goal = get_rule_names get_intro_rules ctxt goal : strings;
@@ -1120,7 +1129,7 @@ fun get_split_rules ctxt goal =
     val used_typ_names = Isabelle_Utils.get_typ_names_in_1st_subg goal;
     val related_rules  = some_names_to_rules "split" used_typ_names ctxt goal
   in
-    related_rules : (Facts.ref * thm) list
+    related_rules : (string * thm) list
   end;
 
 fun get_split_rule_names ctxt goal = get_rule_names get_split_rules ctxt goal;

TBC/TBC.thy

@@ -175,16 +175,18 @@ type pnodes = pnode list;
 val proof_id_counter = Unsynchronized.ref 0: int Unsynchronized.ref;
 
 fun statement_to_conjecture (pst:Proof.state) (Element.Shows [((binding, _), [(stmt:string, _(*assumptions_maybe*))])]) =
+(tracing ("TBC.thy stmt is: " ^ stmt);
+ tracing ("TBC.thy content is: " ^ Isabelle_Utils.YXML_content_of stmt);
       {
         is_final_goal = true,
         lemma_name = mk_lemma_name (Proof.context_of pst) Original_Goal "": string,
-        lemma_stmt = stmt |> YXML.content_of |> String.explode |> Utils.init |> tl |> String.implode,
+        lemma_stmt = stmt |> Isabelle_Utils.YXML_content_of |> String.explode |> Utils.init |> tl |> String.implode,
         proof = NONE,
         proof_id = NONE,
         refuted = false,(*we assume the final goal is a true statement.*)
         proved_wo_assmng_cnjctr = false,
         proved_in_nth_round = NONE
-      }: pnode
+      }): pnode
   | statement_to_conjecture _ _ = error "statement_to_conjecture failed for the final goal.";
 
 fun sort_pnodes (pnodes:pnodes): pnodes =
@@ -2065,12 +2067,7 @@ val long_keyword =
 val long_statement =
   Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead long_keyword) Binding.empty_atts --
   Scan.optional Parse_Spec.includes [] -- Parse_Spec.long_statement
-    >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl))
-: Token.T list ->
-  (bool * Attrib.binding * (xstring * Position.T) list *
-   Element.context list * Element.statement)
-  *
-  Token.T list;
+    >> (fn ((binding, includes), (elems, concl)) => (true, binding, includes, elems, concl));
 
 val short_statement =
   Parse_Spec.statement -- Parse_Spec.if_statement -- Parse.for_fixes