--- a/src/Doc/Implementation/Logic.thy Mon Feb 24 21:43:28 2020 +0100
+++ b/src/Doc/Implementation/Logic.thy Mon Feb 24 21:43:52 2020 +0100
@@ -598,7 +598,7 @@
\begin{mldecls}
@{index_ML Theory.add_deps: "Defs.context -> string ->
Defs.entry -> Defs.entry list -> theory -> theory"} \\
- @{index_ML Thm_Deps.all_oracles: "thm list -> (string * term option) list"} \\
+ @{index_ML Thm_Deps.all_oracles: "thm list -> Proofterm.oracle list"} \\
\end{mldecls}
\<^descr> \<^ML>\<open>Logic.all\<close>~\<open>a B\<close> produces a Pure quantification \<open>\<And>a. B\<close>, where
@@ -676,9 +676,10 @@
\<^descr> \<^ML>\<open>Thm_Deps.all_oracles\<close>~\<open>thms\<close> returns all oracles used in the
internal derivation of the given theorems; this covers the full graph of
- transitive dependencies. The result contains a name, plus the original
- proposition, if @{ML Proofterm.proofs} was at least @{ML 1} during the
- oracle inference. See also the command @{command_ref "thm_oracles"}.
+ transitive dependencies. The result contains an authentic oracle name; if
+ @{ML Proofterm.proofs} was at least @{ML 1} during the oracle inference, it
+ also contains the position of the oracle invocation and its proposition. See
+ also the command @{command_ref "thm_oracles"}.
\<close>
text %mlantiq \<open>
--- a/src/HOL/Fun.thy Mon Feb 24 21:43:28 2020 +0100
+++ b/src/HOL/Fun.thy Mon Feb 24 21:43:52 2020 +0100
@@ -341,6 +341,9 @@
lemma inj_on_imp_bij_betw: "inj_on f A \<Longrightarrow> bij_betw f A (f ` A)"
unfolding bij_betw_def by simp
+lemma bij_betw_apply: "\<lbrakk>bij_betw f A B; a \<in> A\<rbrakk> \<Longrightarrow> f a \<in> B"
+ unfolding bij_betw_def by auto
+
lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
by (rule bij_betw_def)
--- a/src/HOL/Library/Ramsey.thy Mon Feb 24 21:43:28 2020 +0100
+++ b/src/HOL/Library/Ramsey.thy Mon Feb 24 21:43:52 2020 +0100
@@ -27,6 +27,90 @@
lemma doubleton_in_nsets_2 [simp]: "{x,y} \<in> [A]\<^bsup>2\<^esup> \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> x \<noteq> y"
by (auto simp: nsets_2_eq Set.doubleton_eq_iff)
+lemma nsets_3_eq: "nsets A 3 = (\<Union>x\<in>A. \<Union>y\<in>A - {x}. \<Union>z\<in>A - {x,y}. {{x,y,z}})"
+ by (simp add: eval_nat_numeral nsets_def card_Suc_eq) blast
+
+lemma nsets_4_eq: "[A]\<^bsup>4\<^esup> = (\<Union>u\<in>A. \<Union>x\<in>A - {u}. \<Union>y\<in>A - {u,x}. \<Union>z\<in>A - {u,x,y}. {{u,x,y,z}})"
+ (is "_ = ?rhs")
+proof
+ show "[A]\<^bsup>4\<^esup> \<subseteq> ?rhs"
+ by (clarsimp simp add: nsets_def eval_nat_numeral card_Suc_eq) blast
+ show "?rhs \<subseteq> [A]\<^bsup>4\<^esup>"
+ apply (clarsimp simp add: nsets_def eval_nat_numeral card_Suc_eq)
+ by (metis insert_iff singletonD)
+qed
+
+lemma nsets_disjoint_2:
+ "X \<inter> Y = {} \<Longrightarrow> [X \<union> Y]\<^bsup>2\<^esup> = [X]\<^bsup>2\<^esup> \<union> [Y]\<^bsup>2\<^esup> \<union> (\<Union>x\<in>X. \<Union>y\<in>Y. {{x,y}})"
+ by (fastforce simp: nsets_2_eq Set.doubleton_eq_iff)
+
+lemma ordered_nsets_2_eq:
+ fixes A :: "'a::linorder set"
+ shows "nsets A 2 = {{x,y} | x y. x \<in> A \<and> y \<in> A \<and> x<y}"
+ (is "_ = ?rhs")
+proof
+ show "nsets A 2 \<subseteq> ?rhs"
+ unfolding numeral_nat
+ apply (clarsimp simp add: nsets_def card_Suc_eq Set.doubleton_eq_iff not_less)
+ by (metis antisym)
+ show "?rhs \<subseteq> nsets A 2"
+ unfolding numeral_nat by (auto simp: nsets_def card_Suc_eq)
+qed
+
+lemma ordered_nsets_3_eq:
+ fixes A :: "'a::linorder set"
+ shows "nsets A 3 = {{x,y,z} | x y z. x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> x<y \<and> y<z}"
+ (is "_ = ?rhs")
+proof
+ show "nsets A 3 \<subseteq> ?rhs"
+ apply (clarsimp simp add: nsets_def card_Suc_eq eval_nat_numeral)
+ by (metis insert_commute linorder_cases)
+ show "?rhs \<subseteq> nsets A 3"
+ apply (clarsimp simp add: nsets_def card_Suc_eq eval_nat_numeral)
+ by (metis empty_iff insert_iff not_less_iff_gr_or_eq)
+qed
+
+lemma ordered_nsets_4_eq:
+ fixes A :: "'a::linorder set"
+ shows "[A]\<^bsup>4\<^esup> = {U. \<exists>u x y z. U = {u,x,y,z} \<and> u \<in> A \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> u < x \<and> x < y \<and> y < z}"
+ (is "_ = Collect ?RHS")
+proof -
+ { fix U
+ assume "U \<in> [A]\<^bsup>4\<^esup>"
+ then obtain l where "strict_sorted l" "List.set l = U" "length l = 4" "U \<subseteq> A"
+ by (simp add: nsets_def) (metis finite_set_strict_sorted)
+ then have "?RHS U"
+ unfolding numeral_nat length_Suc_conv by auto blast }
+ moreover
+ have "Collect ?RHS \<subseteq> [A]\<^bsup>4\<^esup>"
+ apply (clarsimp simp add: nsets_def eval_nat_numeral)
+ apply (subst card_insert_disjoint, auto)+
+ done
+ ultimately show ?thesis
+ by auto
+qed
+
+lemma ordered_nsets_5_eq:
+ fixes A :: "'a::linorder set"
+ shows "[A]\<^bsup>5\<^esup> = {U. \<exists>u v x y z. U = {u,v,x,y,z} \<and> u \<in> A \<and> v \<in> A \<and> x \<in> A \<and> y \<in> A \<and> z \<in> A \<and> u < v \<and> v < x \<and> x < y \<and> y < z}"
+ (is "_ = Collect ?RHS")
+proof -
+ { fix U
+ assume "U \<in> [A]\<^bsup>5\<^esup>"
+ then obtain l where "strict_sorted l" "List.set l = U" "length l = 5" "U \<subseteq> A"
+ apply (simp add: nsets_def)
+ by (metis finite_set_strict_sorted)
+ then have "?RHS U"
+ unfolding numeral_nat length_Suc_conv by auto blast }
+ moreover
+ have "Collect ?RHS \<subseteq> [A]\<^bsup>5\<^esup>"
+ apply (clarsimp simp add: nsets_def eval_nat_numeral)
+ apply (subst card_insert_disjoint, auto)+
+ done
+ ultimately show ?thesis
+ by auto
+qed
+
lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)"
apply (simp add: binomial_def nsets_def)
by (meson subset_eq_atLeast0_lessThan_finite)
--- a/src/HOL/ex/Iff_Oracle.thy Mon Feb 24 21:43:28 2020 +0100
+++ b/src/HOL/ex/Iff_Oracle.thy Mon Feb 24 21:43:52 2020 +0100
@@ -36,7 +36,7 @@
ML \<open>iff_oracle (\<^theory>, 10)\<close>
ML \<open>
- \<^assert> (map #1 (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
+ \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
\<close>
text \<open>These oracle calls had better fail.\<close>
--- a/src/Pure/General/position.ML Mon Feb 24 21:43:28 2020 +0100
+++ b/src/Pure/General/position.ML Mon Feb 24 21:43:52 2020 +0100
@@ -7,6 +7,7 @@
signature POSITION =
sig
eqtype T
+ val ord: T ord
val make: Thread_Position.T -> T
val dest: T -> Thread_Position.T
val line_of: T -> int option
@@ -52,6 +53,7 @@
val store_reports: report_text list Unsynchronized.ref ->
T list -> ('a -> Markup.T list) -> 'a -> unit
val append_reports: report_text list Unsynchronized.ref -> report list -> unit
+ val here_strs: T -> string * string
val here: T -> string
val here_list: T list -> string
type range = T * T
@@ -73,6 +75,19 @@
datatype T = Pos of (int * int * int) * Properties.T;
+fun ord (pos1 as Pos ((i, j, k), props), pos2 as Pos ((i', j', k'), props')) =
+ if pointer_eq (pos1, pos2) then EQUAL
+ else
+ (case int_ord (i, i') of
+ EQUAL =>
+ (case int_ord (j, j') of
+ EQUAL =>
+ (case int_ord (k, k') of
+ EQUAL => Properties.ord (props, props')
+ | ord => ord)
+ | ord => ord)
+ | ord => ord);
+
fun norm_props (props: Properties.T) =
maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
Markup.position_properties';
@@ -228,15 +243,17 @@
(* here: user output *)
+fun here_strs pos =
+ (case (line_of pos, file_of pos) of
+ (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
+ | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
+ | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
+ | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
+
fun here pos =
let
val props = properties_of pos;
- val (s1, s2) =
- (case (line_of pos, file_of pos) of
- (SOME i, NONE) => (" ", "(line " ^ Value.print_int i ^ ")")
- | (SOME i, SOME name) => (" ", "(line " ^ Value.print_int i ^ " of " ^ quote name ^ ")")
- | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
- | _ => if is_reported pos then ("", "\092<^here>") else ("", ""));
+ val (s1, s2) = here_strs pos;
in
if s2 = "" then ""
else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
--- a/src/Pure/General/pretty.ML Mon Feb 24 21:43:28 2020 +0100
+++ b/src/Pure/General/pretty.ML Mon Feb 24 21:43:52 2020 +0100
@@ -53,6 +53,7 @@
val enclose: string -> string -> T list -> T
val enum: string -> string -> string -> T list -> T
val position: Position.T -> T
+ val here: Position.T -> T list
val list: string -> string -> T list -> T
val str_list: string -> string -> string list -> T
val big_list: string -> T list -> T
@@ -191,6 +192,15 @@
val position =
enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
+fun here pos =
+ let
+ val props = Position.properties_of pos;
+ val (s1, s2) = Position.here_strs pos;
+ in
+ if s2 = "" then []
+ else [str s1, mark_str (Markup.properties props Markup.position, s2)]
+ end;
+
val list = enum ",";
fun str_list lpar rpar strs = list lpar rpar (map str strs);
--- a/src/Pure/General/properties.ML Mon Feb 24 21:43:28 2020 +0100
+++ b/src/Pure/General/properties.ML Mon Feb 24 21:43:52 2020 +0100
@@ -8,6 +8,8 @@
sig
type entry = string * string
type T = entry list
+ val entry_ord: entry ord
+ val ord: T ord
val defined: T -> string -> bool
val get: T -> string -> string option
val put: entry -> T -> T
@@ -21,6 +23,9 @@
type entry = string * string;
type T = entry list;
+val entry_ord = prod_ord string_ord string_ord;
+val ord = list_ord entry_ord;
+
fun defined (props: T) name = AList.defined (op =) props name;
fun get (props: T) name = AList.lookup (op =) props name;
fun put entry (props: T) = AList.update (op =) entry props;
--- a/src/Pure/Proof/extraction.ML Mon Feb 24 21:43:28 2020 +0100
+++ b/src/Pure/Proof/extraction.ML Mon Feb 24 21:43:52 2020 +0100
@@ -177,7 +177,7 @@
let
val (oracles, thms) =
([prf], ([], [])) |-> Proofterm.fold_proof_atoms false
- (fn Oracle (name, prop, _) => apfst (cons (name, SOME prop))
+ (fn Oracle (name, prop, _) => apfst (cons ((name, Position.none), SOME prop))
| PThm (header, thm_body) => apsnd (cons (Proofterm.make_thm header thm_body))
| _ => I);
val body =
--- a/src/Pure/proofterm.ML Mon Feb 24 21:43:28 2020 +0100
+++ b/src/Pure/proofterm.ML Mon Feb 24 21:43:52 2020 +0100
@@ -26,10 +26,10 @@
| Oracle of string * term * typ list option
| PThm of thm_header * thm_body
and proof_body = PBody of
- {oracles: (string * term option) Ord_List.T,
+ {oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
proof: proof}
- type oracle = string * term option
+ type oracle = (string * Position.T) * term option
type thm = serial * thm_node
exception MIN_PROOF of unit
val proof_of: proof_body -> proof
@@ -218,7 +218,7 @@
| Oracle of string * term * typ list option
| PThm of thm_header * thm_body
and proof_body = PBody of
- {oracles: (string * term option) Ord_List.T,
+ {oracles: ((string * Position.T) * term option) Ord_List.T,
thms: (serial * thm_node) Ord_List.T,
proof: proof}
and thm_body =
@@ -227,8 +227,9 @@
Thm_Node of {theory_name: string, name: string, prop: term,
body: proof_body future, export: unit lazy, consolidate: unit lazy};
-type oracle = string * term option;
-val oracle_ord = prod_ord fast_string_ord (option_ord Term_Ord.fast_term_ord);
+type oracle = (string * Position.T) * term option;
+val oracle_ord: oracle ord =
+ prod_ord (prod_ord fast_string_ord Position.ord) (option_ord Term_Ord.fast_term_ord);
type thm = serial * thm_node;
val thm_ord: thm ord = fn ((i, _), (j, _)) => int_ord (j, i);
@@ -374,8 +375,8 @@
pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts)))
(map Position.properties_of pos, (prop, (types, map_proof_of open_proof (Future.join body)))))]
and proof_body consts (PBody {oracles, thms, proof = prf}) =
- triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts)
- (oracles, thms, prf)
+ triple (list (pair (pair string (properties o Position.properties_of))
+ (option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
and thm consts (a, thm_node) =
pair int (pair string (pair string (pair (term consts) (proof_body consts))))
(a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
@@ -439,7 +440,8 @@
and proof_body consts x =
let
val (a, b, c) =
- triple (list (pair string (option (term consts)))) (list (thm consts)) (proof consts) x;
+ triple (list (pair (pair string (Position.of_properties o properties))
+ (option (term consts)))) (list (thm consts)) (proof consts) x;
in PBody {oracles = a, thms = b, proof = c} end
and thm consts x =
let
--- a/src/Pure/thm.ML Mon Feb 24 21:43:28 2020 +0100
+++ b/src/Pure/thm.ML Mon Feb 24 21:43:52 2020 +0100
@@ -1065,9 +1065,9 @@
let
val (oracle, prf) =
(case ! Proofterm.proofs of
- 2 => ((name, SOME prop), Proofterm.oracle_proof name prop)
- | 1 => ((name, SOME prop), MinProof)
- | 0 => ((name, NONE), MinProof)
+ 2 => (((name, Position.thread_data ()), SOME prop), Proofterm.oracle_proof name prop)
+ | 1 => (((name, Position.thread_data ()), SOME prop), MinProof)
+ | 0 => (((name, Position.none), NONE), MinProof)
| i => bad_proofs i);
in
Thm (make_deriv [] [oracle] [] prf,
--- a/src/Pure/thm_deps.ML Mon Feb 24 21:43:28 2020 +0100
+++ b/src/Pure/thm_deps.ML Mon Feb 24 21:43:52 2020 +0100
@@ -33,15 +33,15 @@
in fold collect bodies ([], Inttab.empty) |> #1 |> Proofterm.unions_oracles end;
fun has_skip_proof thms =
- all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\<open>skip_proof\<close>);
+ all_oracles thms |> exists (fn ((name, _), _) => name = \<^oracle_name>\<open>skip_proof\<close>);
fun pretty_thm_oracles ctxt thms =
let
val thy = Proof_Context.theory_of ctxt;
- fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name]
- | prt_oracle (name, SOME prop) =
- [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1,
- Syntax.pretty_term_global thy prop];
+ fun prt_ora (name, pos) = Thm.pretty_oracle ctxt name :: Pretty.here pos;
+ fun prt_oracle (ora, NONE) = prt_ora ora
+ | prt_oracle (ora, SOME prop) =
+ prt_ora ora @ [Pretty.str ":", Pretty.brk 1, Syntax.pretty_term_global thy prop];
in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end;