--- a/src/HOL/Data_Structures/Binomial_Heap.thy Wed Dec 06 21:28:12 2023 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Wed Dec 06 21:28:40 2023 +0100
@@ -476,20 +476,16 @@
estimations of their complexity.
\<close>
definition T_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
-[simp]: "T_link _ _ = 1"
+[simp]: "T_link _ _ = 0"
-text \<open>This function is non-canonical: we omitted a \<open>+1\<close> in the \<open>else\<close>-part,
- to keep the following analysis simpler and more to the point.
-\<close>
fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a trees \<Rightarrow> nat" where
"T_ins_tree t [] = 1"
-| "T_ins_tree t\<^sub>1 (t\<^sub>2 # ts) = (
- (if rank t\<^sub>1 < rank t\<^sub>2 then 1
- else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) ts)
- )"
+| "T_ins_tree t\<^sub>1 (t\<^sub>2 # ts) = 1 +
+ (if rank t\<^sub>1 < rank t\<^sub>2 then 0
+ else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) ts)"
definition T_insert :: "'a::linorder \<Rightarrow> 'a trees \<Rightarrow> nat" where
-"T_insert x ts = T_ins_tree (Node 0 x []) ts + 1"
+"T_insert x ts = T_ins_tree (Node 0 x []) ts"
lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1"
by (induction t ts rule: T_ins_tree.induct) auto
@@ -498,11 +494,11 @@
lemma T_insert_bound:
assumes "invar ts"
- shows "T_insert x ts \<le> log 2 (size (mset_trees ts) + 1) + 2"
+ shows "T_insert x ts \<le> log 2 (size (mset_trees ts) + 1) + 1"
proof -
- have "real (T_insert x ts) \<le> real (length ts) + 2"
- unfolding T_insert_def using T_ins_tree_simple_bound
- using of_nat_mono by fastforce
+ have "real (T_insert x ts) \<le> real (length ts) + 1"
+ unfolding T_insert_def using T_ins_tree_simple_bound
+ by (metis of_nat_1 of_nat_add of_nat_mono)
also note size_mset_trees[OF \<open>invar ts\<close>]
finally show ?thesis by simp
qed
@@ -605,14 +601,13 @@
definition T_del_min :: "'a::linorder trees \<Rightarrow> nat" where
"T_del_min ts = T_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
- \<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2
- ) + 1"
+ \<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2)"
lemma T_del_min_bound:
fixes ts
defines "n \<equiv> size (mset_trees ts)"
assumes "invar ts" and "ts\<noteq>[]"
- shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
+ shows "T_del_min ts \<le> 6 * log 2 (n+1) + 2"
proof -
obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
by (metis surj_pair tree.exhaust_sel)
@@ -628,7 +623,7 @@
using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
by (auto simp: mset_trees_def)
- have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2) + 1"
+ have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2)"
unfolding T_del_min_def GM
by simp
also have "T_get_min_rest ts \<le> log 2 (n+1)"
@@ -637,7 +632,7 @@
unfolding T_rev_def n\<^sub>1_def using size_mset_trees[OF I1] by simp
also have "T_merge (rev ts\<^sub>1) ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1"
unfolding n\<^sub>1_def n\<^sub>2_def using T_merge_bound[OF I1 I2] by (simp add: algebra_simps)
- finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 3"
+ finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 2"
by (simp add: algebra_simps)
also note \<open>n\<^sub>1 + n\<^sub>2 \<le> n\<close>
also note \<open>n\<^sub>1 \<le> n\<close>
--- a/src/HOL/Data_Structures/Queue_2Lists.thy Wed Dec 06 21:28:12 2023 +0100
+++ b/src/HOL/Data_Structures/Queue_2Lists.thy Wed Dec 06 21:28:40 2023 +0100
@@ -60,29 +60,23 @@
text \<open>Running times:\<close>
fun T_norm :: "'a queue \<Rightarrow> nat" where
-"T_norm (fs,rs) = (if fs = [] then T_itrev rs [] else 0) + 1"
+"T_norm (fs,rs) = (if fs = [] then T_itrev rs [] else 0)"
fun T_enq :: "'a \<Rightarrow> 'a queue \<Rightarrow> nat" where
-"T_enq a (fs,rs) = T_norm(fs, a # rs) + 1"
+"T_enq a (fs,rs) = T_norm(fs, a # rs)"
fun T_deq :: "'a queue \<Rightarrow> nat" where
-"T_deq (fs,rs) = (if fs = [] then 0 else T_norm(tl fs,rs)) + 1"
-
-fun T_first :: "'a queue \<Rightarrow> nat" where
-"T_first (a # fs,rs) = 1"
-
-fun T_is_empty :: "'a queue \<Rightarrow> nat" where
-"T_is_empty (fs,rs) = 1"
+"T_deq (fs,rs) = (if fs = [] then 0 else T_norm(tl fs,rs))"
text \<open>Amortized running times:\<close>
fun \<Phi> :: "'a queue \<Rightarrow> nat" where
"\<Phi>(fs,rs) = length rs"
-lemma a_enq: "T_enq a (fs,rs) + \<Phi>(enq a (fs,rs)) - \<Phi>(fs,rs) \<le> 4"
+lemma a_enq: "T_enq a (fs,rs) + \<Phi>(enq a (fs,rs)) - \<Phi>(fs,rs) \<le> 2"
by(auto simp: T_itrev)
-lemma a_deq: "T_deq (fs,rs) + \<Phi>(deq (fs,rs)) - \<Phi>(fs,rs) \<le> 3"
+lemma a_deq: "T_deq (fs,rs) + \<Phi>(deq (fs,rs)) - \<Phi>(fs,rs) \<le> 1"
by(auto simp: T_itrev)
end
--- a/src/HOL/Data_Structures/Tree23_of_List.thy Wed Dec 06 21:28:12 2023 +0100
+++ b/src/HOL/Data_Structures/Tree23_of_List.thy Wed Dec 06 21:28:40 2023 +0100
@@ -130,7 +130,7 @@
"T_leaves (a # as) = T_leaves as + 1"
definition T_tree23_of_list :: "'a list \<Rightarrow> nat" where
-"T_tree23_of_list as = T_leaves as + T_join_all(leaves as) + 1"
+"T_tree23_of_list as = T_leaves as + T_join_all(leaves as)"
lemma T_join_adj: "not_T ts \<Longrightarrow> T_join_adj ts \<le> len ts div 2"
by(induction ts rule: T_join_adj.induct) auto
@@ -162,7 +162,7 @@
lemma len_leaves: "len(leaves as) = length as + 1"
by(induction as) auto
-lemma T_tree23_of_list: "T_tree23_of_list as \<le> 3*(length as) + 4"
+lemma T_tree23_of_list: "T_tree23_of_list as \<le> 3*(length as) + 3"
using T_join_all[of "leaves as"] by(simp add: T_tree23_of_list_def T_leaves len_leaves)
end
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 06 21:28:12 2023 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 06 21:28:40 2023 +0100
@@ -1428,23 +1428,6 @@
((lam_fact_prefix ^ Int.toString (j + 1), (Global, Non_Rec_Def)), (Axiom, t)))
in (facts, lam_facts) end
-(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate this in Sledgehammer to
- prevent the discovery of unreplayable proofs. *)
-fun freeze_term t =
- let
- (* Freshness is desirable for completeness, but not for soundness. *)
- fun indexed_name (s, i) = s ^ "_" ^ string_of_int i ^ atp_weak_suffix
- fun freeze (t $ u) = freeze t $ freeze u
- | freeze (Abs (s, T, t)) = Abs (s, T, freeze t)
- | freeze (Var (x, T)) = Free (indexed_name x, T)
- | freeze t = t
- fun freeze_tvar (x, S) = TFree (indexed_name x, S)
- in
- t |> exists_subterm is_Var t ? freeze
- |> exists_type (exists_subtype is_TVar) t
- ? map_types (map_type_tvar freeze_tvar)
- end
-
fun presimp_prop simp_options ctxt type_enc t =
let
val t =
@@ -2080,8 +2063,6 @@
performance (for some reason). *)
val hyp_ts = hyp_ts |> map (fn t => if member (op aconv) fact_ts t then \<^prop>\<open>True\<close> else t)
- val hyp_ts = map freeze_term hyp_ts;
- val concl_t = freeze_term concl_t;
val maybe_presimp_prop = presimp ? presimp_prop simp_options ctxt type_enc
val facts = facts |> map (apsnd (pair Axiom o maybe_presimp_prop))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Dec 06 21:28:12 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Wed Dec 06 21:28:40 2023 +0100
@@ -293,23 +293,7 @@
fun hammer_away override_params writeln_result subcommand opt_i fact_override state0 =
let
- (* We generally want chained facts to be picked up by the relevance filter, because it can then
- give it a proper name, which is useful for a variety of reasons (minimization, Isar proofs,
- verbose output, machine learning). However, if the fact is available by no other means (not
- even backticks), as "f" would be in "using f unfolding f'" after unfolding, we have no choice
- but to insert it into the state as an additional hypothesis. *)
- val {facts = chained0, ...} = Proof.goal state0
- val (inserts, keep_chained) =
- if null chained0 orelse #only fact_override then
- (chained0, [])
- else
- let val ctxt0 = Proof.context_of state0 in
- List.partition (is_useful_unnamed_local_fact ctxt0) chained0
- end
- val state = state0
- |> (if null inserts then I else Proof.refine_insert inserts #> Proof.set_facts keep_chained)
- |> silence_state
-
+ val state = silence_state state0
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
@@ -329,7 +313,7 @@
(if subcommand = relearn_isarN orelse subcommand = relearn_proverN then mash_unlearn ctxt
else ();
mash_learn ctxt
- (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
+ (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params". *)
(get_params Normal thy
([("timeout", [string_of_real default_learn_prover_timeout]),
("slice", ["false"])] @
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Dec 06 21:28:12 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed Dec 06 21:28:40 2023 +0100
@@ -32,7 +32,6 @@
val instantiate_inducts : Proof.context -> term list -> term ->
(((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list
val fact_of_lazy_fact : lazy_fact -> fact
- val is_useful_unnamed_local_fact : Proof.context -> thm -> bool
val all_facts : Proof.context -> bool -> Keyword.keywords -> thm list -> thm list ->
status Termtab.table -> lazy_fact list
@@ -465,8 +464,7 @@
val assms = Assumption.all_assms_of ctxt
val named_locals = Facts.dest_static true [global_facts] local_facts
val unnamed_locals =
- Facts.props local_facts
- |> map #1
+ chained @ map #1 (Facts.props local_facts)
|> filter (is_useful_unnamed_local_fact ctxt)
|> map (pair "" o single)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Dec 06 21:28:12 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Dec 06 21:28:40 2023 +0100
@@ -477,8 +477,8 @@
one_line_proof_text ctxt 0
(if is_less (play_outcome_ord (play_outcome, one_line_play)) then
(case isar_proof of
- Proof {steps = [Prove {facts = (_, gfs), proof_methods = meth :: _, ...}],
- ...} =>
+ Proof {steps = [Prove {qualifiers = [Show], facts = (_, gfs),
+ proof_methods = meth :: _, ...}], ...} =>
let
val used_facts' =
map_filter (fn s =>
@@ -489,7 +489,8 @@
SOME (s, (Global, General))) gfs
in
((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count)
- end)
+ end
+ | _ => one_line_params)
else
one_line_params) ^
(if isar_proofs = SOME true then "\n(No Isar proof available)" else "")