--- a/NEWS Fri Jul 19 22:29:16 2024 +0100
+++ b/NEWS Fri Jul 19 22:29:32 2024 +0100
@@ -32,6 +32,9 @@
wfP_trancl ~> wfp_tranclp
wfP_wf_eq ~> wfp_wf_eq
wf_acc_iff ~> wf_iff_acc
+ - Added lemmas.
+ wf_on_antimono_stronger
+ wfp_on_antimono_stronger
* Theory "HOL-Library.Multiset":
- Renamed lemmas. Minor INCOMPATIBILITY.
--- a/src/Doc/Implementation/Logic.thy Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Doc/Implementation/Logic.thy Fri Jul 19 22:29:32 2024 +0100
@@ -1293,7 +1293,7 @@
@{define_ML Proofterm.reconstruct_proof:
"theory -> term -> proof -> proof"} \\
@{define_ML Proofterm.expand_proof: "theory ->
- (Proofterm.thm_header -> Thm_Name.T option) -> proof -> proof"} \\
+ (Proofterm.thm_header -> Thm_Name.P option) -> proof -> proof"} \\
@{define_ML Proof_Checker.thm_of_proof: "theory -> proof -> thm"} \\
@{define_ML Proof_Syntax.read_proof: "theory -> bool -> bool -> string -> proof"} \\
@{define_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy Fri Jul 19 22:29:32 2024 +0100
@@ -67,13 +67,13 @@
GT \<Rightarrow> let r' = insert x r in if incr r r' then balR l a b r' else Node l (a,b) r')"
fun decr where
-"decr t t' = (t \<noteq> Leaf \<and> (t' = Leaf \<or> \<not> is_bal t \<and> is_bal t'))"
+"decr t t' = (t \<noteq> Leaf \<and> incr t' t)"
fun split_max :: "'a tree_bal \<Rightarrow> 'a tree_bal * 'a" where
"split_max (Node l (a, ba) r) =
(if r = Leaf then (l,a)
else let (r',a') = split_max r;
- t' = if decr r r' then balL l a ba r' else Node l (a,ba) r'
+ t' = if incr r' r then balL l a ba r' else Node l (a,ba) r'
in (t', a'))"
fun delete :: "'a::linorder \<Rightarrow> 'a tree_bal \<Rightarrow> 'a tree_bal" where
@@ -82,7 +82,7 @@
(case cmp x a of
EQ \<Rightarrow> if l = Leaf then r
else let (l', a') = split_max l in
- if decr l l' then balR l' a' ba r else Node l' (a',ba) r |
+ if incr l' l then balR l' a' ba r else Node l' (a',ba) r |
LT \<Rightarrow> let l' = delete x l in if decr l l' then balR l' a ba r else Node l' (a,ba) r |
GT \<Rightarrow> let r' = delete x r in if decr r r' then balL l a ba r' else Node l (a,ba) r')"
@@ -136,7 +136,7 @@
lemma avl_split_max:
"\<lbrakk> split_max t = (t',a); avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow>
- avl t' \<and> height t = height t' + (if decr t t' then 1 else 0)"
+ avl t' \<and> height t = height t' + (if incr t' t then 1 else 0)"
apply(induction t arbitrary: t' a rule: split_max_induct)
apply(auto simp: max_absorb1 max_absorb2 height_1_iff split!: splits prod.splits)
done
--- a/src/HOL/Data_Structures/RBT_Set.thy Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy Fri Jul 19 22:29:32 2024 +0100
@@ -307,10 +307,13 @@
lemma bheight_size_bound: "invc t \<Longrightarrow> invh t \<Longrightarrow> 2 ^ (bheight t) \<le> size1 t"
by (induction t) auto
+lemma bheight_le_min_height: "invh t \<Longrightarrow> bheight t \<le> min_height t"
+by (induction t) auto
+
lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
proof -
have "2 powr (height t / 2) \<le> 2 powr bheight t"
- using rbt_height_bheight[OF assms] by (simp)
+ using rbt_height_bheight[OF assms] by simp
also have "\<dots> \<le> size1 t" using assms
by (simp add: powr_realpow bheight_size_bound rbt_def)
finally have "2 powr (height t / 2) \<le> size1 t" .
@@ -319,4 +322,15 @@
thus ?thesis by simp
qed
+lemma rbt_height_le2: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
+proof -
+ have "height t \<le> 2 * bheight t"
+ using rbt_height_bheight_if assms[simplified rbt_def] by fastforce
+ also have "\<dots> \<le> 2 * min_height t"
+ using bheight_le_min_height assms[simplified rbt_def] by auto
+ also have "\<dots> \<le> 2 * log 2 (size1 t)"
+ using le_log2_of_power min_height_size1 by auto
+ finally show ?thesis by simp
+qed
+
end
--- a/src/HOL/Proofs/ex/XML_Data.thy Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Proofs/ex/XML_Data.thy Fri Jul 19 22:29:32 2024 +0100
@@ -14,11 +14,11 @@
ML \<open>
fun export_proof thy thm = thm
|> Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
- |> Proofterm.encode (Sign.consts_of thy);
+ |> Proofterm.encode thy;
fun import_proof thy xml =
let
- val prf = Proofterm.decode (Sign.consts_of thy) xml;
+ val prf = Proofterm.decode thy xml;
val (prf', _) = Proofterm.freeze_thaw_prf prf;
in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end;
\<close>
--- a/src/HOL/Tools/inductive_realizer.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Jul 19 22:29:32 2024 +0100
@@ -16,7 +16,7 @@
fun thm_name_of thm =
(case Proofterm.fold_proof_atoms false (fn PThm ({thm_name, ...}, _) => cons thm_name | _ => I)
[Thm.proof_of thm] [] of
- [thm_name] => thm_name
+ [(thm_name, _)] => thm_name
| _ => raise THM ("thm_name_of: bad proof of theorem", 0, [thm]));
val short_name_of = Thm_Name.short o thm_name_of;
--- a/src/HOL/Tools/rewrite_hol_proof.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Fri Jul 19 22:29:32 2024 +0100
@@ -305,9 +305,9 @@
(** Replace congruence rules by substitution rules **)
-fun strip_cong ps (PThm ({thm_name = ("HOL.cong", 0), ...}, _) % _ % _ % SOME x % SOME y %%
+fun strip_cong ps (PThm ({thm_name = (("HOL.cong", 0), _), ...}, _) % _ % _ % SOME x % SOME y %%
prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1
- | strip_cong ps (PThm ({thm_name = ("HOL.refl", 0), ...}, _) % SOME f %% _) = SOME (f, ps)
+ | strip_cong ps (PThm ({thm_name = (("HOL.refl", 0), _), ...}, _) % SOME f %% _) = SOME (f, ps)
| strip_cong _ _ = NONE;
val subst_prf = Proofterm.any_head_of (Thm.proof_of @{thm subst});
@@ -330,15 +330,15 @@
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
-fun elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
+fun elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD1", 0), _), ...}, _) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
- | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD1", 0), ...}, _) % P % _ %% prf) =
+ | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD1", 0), _), ...}, _) % P % _ %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
(strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
- | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % _ %% prf1 %% prf2) =
+ | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD2", 0), _), ...}, _) % _ % _ %% prf1 %% prf2) =
Option.map (make_subst Ts prf2 [] o
apsnd (map (make_sym Ts))) (strip_cong [] prf1)
- | elim_cong_aux Ts (PThm ({thm_name = ("HOL.iffD2", 0), ...}, _) % _ % P %% prf) =
+ | elim_cong_aux Ts (PThm ({thm_name = (("HOL.iffD2", 0), _), ...}, _) % _ % P %% prf) =
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_boundvars 1 0 prf))
| elim_cong_aux _ _ = NONE;
--- a/src/HOL/Wellfounded.thy Fri Jul 19 22:29:16 2024 +0100
+++ b/src/HOL/Wellfounded.thy Fri Jul 19 22:29:32 2024 +0100
@@ -309,18 +309,45 @@
subsubsection \<open>Antimonotonicity\<close>
+
+lemma wfp_on_antimono_stronger:
+ fixes
+ A :: "'a set" and B :: "'b set" and
+ f :: "'a \<Rightarrow> 'b" and
+ R :: "'b \<Rightarrow> 'b \<Rightarrow> bool" and Q :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ assumes
+ wf: "wfp_on B R" and
+ sub: "f ` A \<subseteq> B" and
+ mono: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> Q x y \<Longrightarrow> R (f x) (f y)"
+ shows "wfp_on A Q"
+ unfolding wfp_on_iff_ex_minimal
+proof (intro allI impI)
+ fix A' :: "'a set"
+ assume "A' \<subseteq> A" and "A' \<noteq> {}"
+ have "f ` A' \<subseteq> B"
+ using \<open>A' \<subseteq> A\<close> sub by blast
+ moreover have "f ` A' \<noteq> {}"
+ using \<open>A' \<noteq> {}\<close> by blast
+ ultimately have "\<exists>z\<in>f ` A'. \<forall>y. R y z \<longrightarrow> y \<notin> f ` A'"
+ using wf wfp_on_iff_ex_minimal by blast
+ hence "\<exists>z\<in>A'. \<forall>y. R (f y) (f z) \<longrightarrow> y \<notin> A'"
+ by blast
+ thus "\<exists>z\<in>A'. \<forall>y. Q y z \<longrightarrow> y \<notin> A'"
+ using \<open>A' \<subseteq> A\<close> mono by blast
+qed
+
+lemma wf_on_antimono_stronger:
+ assumes
+ "wf_on B r" and
+ "f ` A \<subseteq> B" and
+ "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> q \<Longrightarrow> (f x, f y) \<in> r)"
+ shows "wf_on A q"
+ using assms wfp_on_antimono_stronger[to_set, of B r f A q] by blast
+
lemma wf_on_antimono_strong:
assumes "wf_on B r" and "A \<subseteq> B" and "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> q \<Longrightarrow> (x, y) \<in> r)"
shows "wf_on A q"
- unfolding wf_on_iff_ex_minimal
-proof (intro allI impI)
- fix AA assume "AA \<subseteq> A" and "AA \<noteq> {}"
- hence "\<exists>z\<in>AA. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> AA"
- using \<open>wf_on B r\<close> \<open>A \<subseteq> B\<close>
- by (simp add: wf_on_iff_ex_minimal)
- then show "\<exists>z\<in>AA. \<forall>y. (y, z) \<in> q \<longrightarrow> y \<notin> AA"
- using \<open>AA \<subseteq> A\<close> assms(3) by blast
-qed
+ using assms wf_on_antimono_stronger[of B r "\<lambda>x. x" A q] by blast
lemma wfp_on_antimono_strong:
"wfp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> Q x y \<Longrightarrow> R x y) \<Longrightarrow> wfp_on A Q"
--- a/src/Pure/Build/build_manager.scala Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Build/build_manager.scala Fri Jul 19 22:29:32 2024 +0100
@@ -980,8 +980,7 @@
/* repository poller */
object Poller {
- case class Versions(isabelle: String, components: List[Component])
- case class State(current: Versions, next: Future[Versions])
+ case class State(current: List[Component], next: Future[List[Component]])
}
class Poller(
@@ -994,11 +993,11 @@
override def delay = options.seconds("build_manager_poll_delay")
- private def current: Poller.Versions =
- Poller.Versions(isabelle_repository.id("default"), sync_dirs.map(dir =>
- Component(dir.name, dir.hg.id("default"))))
+ private def current: List[Component] =
+ Component.isabelle(isabelle_repository.id("default")) ::
+ sync_dirs.map(dir => Component(dir.name, dir.hg.id("default")))
- private def poll: Future[Poller.Versions] = Future.fork {
+ private def poll: Future[List[Component]] = Future.fork {
Par_List.map((repo: Mercurial.Repository) => repo.pull(),
isabelle_repository :: sync_dirs.map(_.hg))
@@ -1007,17 +1006,24 @@
val init: Poller.State = Poller.State(current, poll)
- private def add_tasks(current: Poller.Versions, next: Poller.Versions): Unit = {
- val isabelle_updated = current.isabelle != next.isabelle
- val updated_components =
- next.components.zip(current.components).filter(_ != _).map(_._1.name).toSet
+ private def add_tasks(current: List[Component], next: List[Component]): Unit = {
+ val next_rev = next.map(component => component.name -> component.rev).toMap
+
+ def is_unchanged(components: List[Component]): Boolean =
+ components.forall(component => next_rev.get(component.name).contains(component.rev))
+
+ def is_changed(component_names: List[String]): Boolean =
+ !is_unchanged(current.filter(component => component_names.contains(component.name)))
+
+ def is_current(job: Job): Boolean = is_unchanged(job.components)
synchronized_database("add_tasks") {
for {
ci_job <- ci_jobs
if ci_job.trigger == Build_CI.On_Commit
- if isabelle_updated || ci_job.components.exists(updated_components.contains)
+ if is_changed(Component.Isabelle :: ci_job.components)
if !_state.pending.values.exists(_.kind == ci_job.name)
+ if !_state.running.values.filter(_.kind == ci_job.name).exists(is_current)
} _state = _state.add_pending(CI_Build.task(ci_job))
}
}
--- a/src/Pure/Build/export_theory.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Build/export_theory.ML Fri Jul 19 22:29:32 2024 +0100
@@ -283,8 +283,8 @@
val lookup_thm_id = Global_Theory.lookup_thm_id thy;
fun expand_name thm_id (header: Proofterm.thm_header) =
- if #serial header = #serial thm_id then Thm_Name.empty
- else the_default Thm_Name.empty (lookup_thm_id (Proofterm.thm_header_id header));
+ if #serial header = #serial thm_id then Thm_Name.none
+ else the_default Thm_Name.none (lookup_thm_id (Proofterm.thm_header_id header));
fun entity_markup_thm (serial, (name, i)) =
let
@@ -310,11 +310,11 @@
(prop, deps, proof) |>
let
open XML.Encode Term_XML.Encode;
- val encode_proof = Proofterm.encode_standard_proof consts;
+ val encode_proof = Proofterm.encode_standard_proof thy;
in triple encode_prop (list Thm_Name.encode) encode_proof end
end;
- fun export_thm (thm_id, thm_name) =
+ fun export_thm (thm_id, (thm_name, _)) =
let
val markup = entity_markup_thm (#serial thm_id, thm_name);
val body =
--- a/src/Pure/General/table.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/General/table.ML Fri Jul 19 22:29:32 2024 +0100
@@ -66,7 +66,8 @@
val insert_set: key -> set -> set
val remove_set: key -> set -> set
val make_set: key list -> set
- val unsynchronized_cache: (key -> 'a) -> key -> 'a
+ type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}
+ val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
end;
functor Table(Key: KEY): TABLE =
@@ -591,12 +592,13 @@
(* cache *)
+type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
+
fun unsynchronized_cache f =
let
val cache1 = Unsynchronized.ref empty;
val cache2 = Unsynchronized.ref empty;
- in
- fn x =>
+ fun apply x =
(case lookup (! cache1) x of
SOME y => y
| NONE =>
@@ -604,9 +606,11 @@
SOME exn => Exn.reraise exn
| NONE =>
(case Exn.result f x of
- Exn.Res y => (Unsynchronized.change cache1 (update (x, y)); y)
- | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))))
- end;
+ Exn.Res y => (Unsynchronized.change cache1 (default (x, y)); y)
+ | Exn.Exn exn => (Unsynchronized.change cache2 (default (x, exn)); Exn.reraise exn))));
+ fun reset () = (cache2 := empty; cache1 := empty);
+ fun total_size () = size (! cache1) + size (! cache2);
+ in {apply = apply, reset = reset, size = total_size} end;
(* ML pretty-printing *)
--- a/src/Pure/Proof/extraction.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Jul 19 22:29:32 2024 +0100
@@ -511,9 +511,9 @@
val procs = maps (rev o fst o snd) types;
val rtypes = map fst types;
val typroc = typeof_proc [];
- fun expand_name ({thm_name, ...}: Proofterm.thm_header) =
+ fun expand_name ({thm_name = (thm_name, _), ...}: Proofterm.thm_header) =
if Thm_Name.is_empty thm_name orelse member (op =) expand thm_name
- then SOME Thm_Name.empty else NONE;
+ then SOME Thm_Name.none else NONE;
val prep = the_default (K I) prep thy' o
Proof_Rewrite_Rules.elim_defs thy' false (map (Thm.transfer thy) defs) o
Proofterm.expand_proof thy' expand_name;
@@ -623,7 +623,7 @@
| corr d vs ts Ts hs cs _ (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) _ defs =
let
- val {pos, theory_name, thm_name, prop, ...} = thm_header;
+ val {command_pos, theory_name, thm_name = (thm_name, thm_pos), prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
@@ -650,8 +650,8 @@
val corr_prf = mkabsp shyps corr_prf0;
val corr_prop = Proofterm.prop_of corr_prf;
val corr_header =
- Proofterm.thm_header (serial ()) pos theory_name
- (corr_name thm_name vs', 0) corr_prop
+ Proofterm.thm_header (serial ()) command_pos theory_name
+ ((corr_name thm_name vs', 0), thm_pos) corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_prf' =
Proofterm.proof_combP
@@ -727,7 +727,7 @@
| extr d vs ts Ts hs (prf0 as PThm (thm_header as {types = SOME Ts', ...}, thm_body)) defs =
let
- val {pos, theory_name, thm_name, prop, ...} = thm_header;
+ val {command_pos, theory_name, thm_name = (thm_name, thm_pos), prop, ...} = thm_header;
val prf = Proofterm.thm_body_proof_open thm_body;
val (vs', tye) = find_inst prop Ts ts vs;
val shyps = mk_shyps tye;
@@ -772,8 +772,8 @@
SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
val corr_prop = Proofterm.prop_of corr_prf';
val corr_header =
- Proofterm.thm_header (serial ()) pos theory_name
- (corr_name thm_name vs', 0) corr_prop
+ Proofterm.thm_header (serial ()) command_pos theory_name
+ ((corr_name thm_name vs', 0), thm_pos) corr_prop
(SOME (map TVar (Term.add_tvars corr_prop [] |> rev)));
val corr_prf'' =
Proofterm.proof_combP (Proofterm.proof_combt
--- a/src/Pure/Proof/proof_checker.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Proof/proof_checker.ML Fri Jul 19 22:29:32 2024 +0100
@@ -88,7 +88,7 @@
(Thm.forall_intr_vars (Thm.forall_intr_frees thm'))
end;
- fun thm_of _ _ (PThm ({thm_name, prop = prop', types = SOME Ts, ...}, _)) =
+ fun thm_of _ _ (PThm ({thm_name = (thm_name, thm_pos), prop = prop', types = SOME Ts, ...}, _)) =
let
val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup thm_name));
val prop = Thm.prop_of thm;
@@ -96,9 +96,9 @@
if is_equal prop prop' then ()
else
error ("Duplicate use of theorem name " ^
- quote (Global_Theory.print_thm_name thy thm_name) ^ "\n" ^
- Syntax.string_of_term_global thy prop ^ "\n\n" ^
- Syntax.string_of_term_global thy prop');
+ quote (Global_Theory.print_thm_name thy thm_name) ^ Position.here thm_pos
+ ^ "\n" ^ Syntax.string_of_term_global thy prop
+ ^ "\n\n" ^ Syntax.string_of_term_global thy prop');
in thm_of_atom thm Ts end
| thm_of _ _ (PAxm (name, _, SOME Ts)) =
--- a/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Fri Jul 19 22:29:32 2024 +0100
@@ -39,12 +39,12 @@
val equal_elim_axm = ax Proofterm.equal_elim_axm [];
val symmetric_axm = ax Proofterm.symmetric_axm [propT];
- fun rew' (PThm ({thm_name = ("Pure.protectD", 0), ...}, _) % _ %%
- (PThm ({thm_name = ("Pure.protectI", 0), ...}, _) % _ %% prf)) = SOME prf
- | rew' (PThm ({thm_name = ("Pure.conjunctionD1", 0), ...}, _) % _ % _ %%
- (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% prf %% _)) = SOME prf
- | rew' (PThm ({thm_name = ("Pure.conjunctionD2", 0), ...}, _) % _ % _ %%
- (PThm ({thm_name = ("Pure.conjunctionI", 0), ...}, _) % _ % _ %% _ %% prf)) = SOME prf
+ fun rew' (PThm ({thm_name = (("Pure.protectD", 0), _), ...}, _) % _ %%
+ (PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _) % _ %% prf)) = SOME prf
+ | rew' (PThm ({thm_name = (("Pure.conjunctionD1", 0), _), ...}, _) % _ % _ %%
+ (PThm ({thm_name = (("Pure.conjunctionI", 0), _), ...}, _) % _ % _ %% prf %% _)) = SOME prf
+ | rew' (PThm ({thm_name = (("Pure.conjunctionD2", 0), _), ...}, _) % _ % _ %%
+ (PThm ({thm_name = (("Pure.conjunctionI", 0), _), ...}, _) % _ % _ %% _ %% prf)) = SOME prf
| rew' (PAxm ("Pure.equal_elim", _, _) % _ % _ %%
(PAxm ("Pure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
| rew' (PAxm ("Pure.symmetric", _, _) % _ % _ %%
@@ -54,14 +54,14 @@
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
(PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
_ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1) %%
- ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
+ ((tg as PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _)) % _ %% prf2)) =
SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
| rew' (PAxm ("Pure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
(PAxm ("Pure.symmetric", _, _) % _ % _ %%
(PAxm ("Pure.combination", _, _) % SOME (Const ("Pure.prop", _)) %
_ % _ % _ %% (PAxm ("Pure.reflexive", _, _) % _) %% prf1)) %%
- ((tg as PThm ({thm_name = ("Pure.protectI", 0), ...}, _)) % _ %% prf2)) =
+ ((tg as PThm ({thm_name = (("Pure.protectI", 0), _), ...}, _)) % _ %% prf2)) =
SOME (tg %> B %% (equal_elim_axm %> A %> B %%
(symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
@@ -245,7 +245,7 @@
(AbsP (s, t, fst (insert_refl defs Ts prf)), false)
| insert_refl defs Ts prf =
(case Proofterm.strip_combt prf of
- (PThm ({thm_name, prop, types = SOME Ts, ...}, _), ts) =>
+ (PThm ({thm_name = (thm_name, _), prop, types = SOME Ts, ...}, _), ts) =>
if member (op =) defs thm_name then
let
val vs = vars_of prop;
@@ -271,11 +271,11 @@
let
val cnames = map (fst o dest_Const o fst) defs';
val expand = Proofterm.fold_proof_atoms true
- (fn PThm ({serial, thm_name, prop, ...}, _) =>
+ (fn PThm ({serial, thm_name = (thm_name, _), prop, ...}, _) =>
if member (op =) defnames thm_name orelse
not (exists_Const (member (op =) cnames o #1) prop)
then I
- else Inttab.update (serial, Thm_Name.empty)
+ else Inttab.update (serial, Thm_Name.none)
| _ => I) [prf] Inttab.empty;
in Proofterm.expand_proof thy (Inttab.lookup expand o #serial) prf end
else prf;
--- a/src/Pure/Proof/proof_syntax.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/Proof/proof_syntax.ML Fri Jul 19 22:29:32 2024 +0100
@@ -16,7 +16,7 @@
val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
val pretty_proof_boxes_of: Proof.context ->
{full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T
- val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.T option} ->
+ val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> Thm_Name.P option} ->
thm -> Proofterm.proof
val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
end;
@@ -104,7 +104,7 @@
let val U = Term.itselfT T --> propT
in Const ("Pure.PClass", U --> proofT) $ Const (Logic.const_of_class c, U) end;
-fun term_of _ (PThm ({serial = i, thm_name = a, types = Ts, ...}, _)) =
+fun term_of _ (PThm ({serial = i, thm_name = (a, _), types = Ts, ...}, _)) =
fold AppT (these Ts)
(Const
(Long_Name.append "thm"
@@ -227,7 +227,7 @@
fun proof_syntax prf =
let
val thm_names = Symset.dest (Proofterm.fold_proof_atoms true
- (fn PThm ({thm_name, ...}, _) =>
+ (fn PThm ({thm_name = (thm_name, _), ...}, _) =>
if Thm_Name.is_empty thm_name then I else Symset.insert (Thm_Name.short thm_name)
| _ => I) [prf] Symset.empty);
val axm_names = Symset.dest (Proofterm.fold_proof_atoms true
@@ -264,7 +264,7 @@
excluded = is_some o Global_Theory.lookup_thm_id thy}
in
Proofterm.proof_boxes selection [Thm.proof_of thm]
- |> map (fn ({serial = i, pos, prop, ...}, proof) =>
+ |> map (fn ({serial = i, command_pos, prop, thm_name = (_, thm_pos), ...}, proof) =>
let
val proof' = proof
|> Proofterm.reconstruct_proof thy prop
@@ -276,7 +276,7 @@
val name = Long_Name.append "thm" (string_of_int i);
in
Pretty.item
- [Pretty.str (name ^ Position.here_list pos ^ ":"), Pretty.brk 1,
+ [Pretty.str (name ^ Position.here_list [command_pos, thm_pos] ^ ":"), Pretty.brk 1,
Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof']
end)
|> Pretty.chunks
--- a/src/Pure/global_theory.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/global_theory.ML Fri Jul 19 22:29:32 2024 +0100
@@ -13,13 +13,13 @@
val defined_fact: theory -> string -> bool
val alias_fact: binding -> string -> theory -> theory
val hide_fact: bool -> string -> theory -> theory
- val dest_thms: bool -> theory list -> theory -> (Thm_Name.T * thm) list
+ val dest_thms: bool -> theory list -> theory -> (Thm_Name.P * thm) list
val pretty_thm_name: theory -> Thm_Name.T -> Pretty.T
val print_thm_name: theory -> Thm_Name.T -> string
- val get_thm_names: theory -> Thm_Name.T Inttab.table
- val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.T) list
- val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.T option
- val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) option
+ val get_thm_names: theory -> Thm_Name.P Inttab.table
+ val dest_thm_names: theory -> (Proofterm.thm_id * Thm_Name.P) list
+ val lookup_thm_id: theory -> Proofterm.thm_id -> Thm_Name.P option
+ val lookup_thm: theory -> thm -> (Proofterm.thm_id * Thm_Name.P) option
val get_thms: theory -> xstring -> thm list
val get_thm: theory -> xstring -> thm
val transfer_theories: theory -> thm -> thm
@@ -63,7 +63,7 @@
structure Data = Theory_Data
(
- type T = Facts.T * Thm_Name.T Inttab.table lazy option;
+ type T = Facts.T * Thm_Name.P Inttab.table lazy option;
val empty: T = (Facts.empty, NONE);
fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), NONE);
);
@@ -86,7 +86,7 @@
fun dest_thms verbose prev_thys thy =
Facts.dest_static verbose (map facts_of prev_thys) (facts_of thy)
- |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms |> map (apfst fst));
+ |> maps (fn (name, thms) => Thm_Name.list (name, Position.none) thms);
fun pretty_thm_name thy = Facts.pretty_thm_name (Context.Theory thy) (facts_of thy);
val print_thm_name = Pretty.string_of oo pretty_thm_name;
@@ -99,7 +99,7 @@
fun make_thm_names thy =
(dest_thms true (Theory.parents_of thy) thy, Inttab.empty)
- |-> fold (fn (thm_name, thm) => fn thm_names =>
+ |-> fold (fn ((thm_name, thm_pos), thm) => fn thm_names =>
(case Thm.derivation_id (Thm.transfer thy thm) of
NONE => thm_names
| SOME {serial, theory_name} =>
@@ -107,11 +107,11 @@
raise THM ("Bad theory name for derivation", 0, [thm])
else
(case Inttab.lookup thm_names serial of
- SOME thm_name' =>
+ SOME (thm_name', thm_pos') =>
raise THM ("Duplicate use of derivation identity for " ^
- print_thm_name thy thm_name ^ " vs. " ^
- print_thm_name thy thm_name', 0, [thm])
- | NONE => Inttab.update (serial, thm_name) thm_names)));
+ print_thm_name thy thm_name ^ Position.here thm_pos ^ " vs. " ^
+ print_thm_name thy thm_name' ^ Position.here thm_pos', 0, [thm])
+ | NONE => Inttab.update (serial, (thm_name, thm_pos)) thm_names)));
fun lazy_thm_names thy =
(case thm_names_of thy of
@@ -256,7 +256,7 @@
No_Name_Flags => thm
| Name_Flags {post, official} =>
thm
- |> (official andalso (post orelse Thm_Name.is_empty (Thm.raw_derivation_name thm))) ?
+ |> (official andalso (post orelse Thm_Name.is_empty (#1 (Thm.raw_derivation_name thm)))) ?
Thm.name_derivation (name, pos)
|> (not (Thm_Name.is_empty name) andalso (post orelse not (Thm.has_name_hint thm))) ?
Thm.put_name_hint name));
--- a/src/Pure/proofterm.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/proofterm.ML Fri Jul 19 22:29:32 2024 +0100
@@ -9,7 +9,7 @@
signature PROOFTERM =
sig
type thm_header =
- {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
+ {serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P,
prop: term, types: typ list option}
type thm_body
type thm_node
@@ -38,7 +38,7 @@
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
val map_proof_of: (proof -> proof) -> proof_body -> proof_body
- val thm_header: serial -> Position.T list -> string -> Thm_Name.T -> term -> typ list option ->
+ val thm_header: serial -> Position.T -> string -> Thm_Name.P -> term -> typ list option ->
thm_header
val thm_body: proof_body -> thm_body
val thm_body_proof_raw: thm_body -> proof
@@ -65,12 +65,13 @@
val no_thm_proofs: proof -> proof
val no_body_proofs: proof -> proof
- val encode: Consts.T -> proof XML.Encode.T
- val encode_body: Consts.T -> proof_body XML.Encode.T
- val encode_standard_term: Consts.T -> term XML.Encode.T
- val encode_standard_proof: Consts.T -> proof XML.Encode.T
- val decode: Consts.T -> proof XML.Decode.T
- val decode_body: Consts.T -> proof_body XML.Decode.T
+ val proof_to_zproof: theory -> proof -> zproof
+ val encode_standard_term: theory -> term XML.Encode.T
+ val encode_standard_proof: theory -> proof XML.Encode.T
+ val encode: theory -> proof XML.Encode.T
+ val encode_body: theory -> proof_body XML.Encode.T
+ val decode: theory -> proof XML.Decode.T
+ val decode_body: theory -> proof_body XML.Decode.T
val %> : proof * term -> proof
@@ -170,8 +171,8 @@
val reconstruct_proof: theory -> term -> proof -> proof
val prop_of': term list -> proof -> term
val prop_of: proof -> term
- val expand_name_empty: thm_header -> Thm_Name.T option
- val expand_proof: theory -> (thm_header -> Thm_Name.T option) -> proof -> proof
+ val expand_name_empty: thm_header -> Thm_Name.P option
+ val expand_proof: theory -> (thm_header -> Thm_Name.P option) -> proof -> proof
val standard_vars: Name.context -> term * proof option -> term * proof option
val standard_vars_term: Name.context -> term -> term
@@ -188,8 +189,8 @@
val unconstrain_thm_proof: theory -> sorts_proof -> sort list ->
term -> (serial * proof_body future) list -> proof_body -> term * proof_body
val get_identity: sort list -> term list -> term -> proof ->
- {serial: serial, theory_name: string, thm_name: Thm_Name.T} option
- val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.T
+ {serial: serial, theory_name: string, thm_name: Thm_Name.P} option
+ val get_approximative_name: sort list -> term list -> term -> proof -> Thm_Name.P
type thm_id = {serial: serial, theory_name: string}
val make_thm_id: serial * string -> thm_id
val thm_header_id: thm_header -> thm_id
@@ -205,8 +206,10 @@
(** datatype proof **)
+val proof_serial = Counter.make ();
+
type thm_header =
- {serial: serial, pos: Position.T list, theory_name: string, thm_name: Thm_Name.T,
+ {serial: serial, command_pos: Position.T, theory_name: string, thm_name: Thm_Name.P,
prop: term, types: typ list option};
datatype proof =
@@ -253,8 +256,8 @@
fun no_proof (PBody {oracles, thms, zboxes, zproof, ...}) =
PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = MinProof};
-fun thm_header serial pos theory_name thm_name prop types : thm_header =
- {serial = serial, pos = pos, theory_name = theory_name, thm_name = thm_name,
+fun thm_header serial command_pos theory_name thm_name prop types : thm_header =
+ {serial = serial, command_pos = command_pos, theory_name = theory_name, thm_name = thm_name,
prop = prop, types = types};
fun thm_body body = Thm_Body {open_proof = I, body = Future.value body};
@@ -290,7 +293,9 @@
val no_export = Lazy.value ();
-fun make_thm ({serial, theory_name, thm_name, prop, ...}: thm_header) (Thm_Body {body, ...}) =
+fun make_thm
+ ({serial, theory_name, thm_name = (thm_name, _), prop, ...}: thm_header)
+ (Thm_Body {body, ...}) =
(serial, make_thm_node theory_name thm_name prop body no_export);
@@ -342,8 +347,8 @@
| no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf)
| no_thm_names (prf % t) = no_thm_names prf % t
| no_thm_names (prf1 %% prf2) = no_thm_names prf1 %% no_thm_names prf2
- | no_thm_names (PThm ({serial, pos, theory_name, thm_name = _, prop, types}, thm_body)) =
- PThm (thm_header serial pos theory_name Thm_Name.empty prop types, thm_body)
+ | no_thm_names (PThm ({serial, command_pos, theory_name, thm_name = _, prop, types}, thm_body)) =
+ PThm (thm_header serial command_pos theory_name Thm_Name.none prop types, thm_body)
| no_thm_names a = a;
fun no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
@@ -369,6 +374,39 @@
(** XML data representation **)
+(* encode as zterm/zproof *)
+
+fun proof_to_zproof thy =
+ let
+ val {ztyp, zterm} = ZTerm.zterm_cache thy;
+ val ztvar = ztyp #> (fn ZTVar v => v);
+
+ fun zproof_const name prop typargs =
+ let
+ val vs = rev ((fold_types o fold_atyps) (insert (op =) o ztvar) prop []);
+ val Ts = map ztyp typargs
+ in ZConstp ((name, zterm prop), (ZTVars.make (vs ~~ Ts), ZVars.empty)) end;
+
+ fun zproof MinProof = ZNop
+ | zproof (PBound i) = ZBoundp i
+ | zproof (Abst (a, SOME T, p)) = ZAbst (a, ztyp T, zproof p)
+ | zproof (AbsP (a, SOME t, p)) = ZAbsp (a, zterm t, zproof p)
+ | zproof (p % SOME t) = ZAppt (zproof p, zterm t)
+ | zproof (p %% q) = ZAppp (zproof p, zproof q)
+ | zproof (Hyp t) = ZHyp (zterm t)
+ | zproof (PAxm (a, prop, SOME Ts)) = zproof_const (ZAxiom a) prop Ts
+ | zproof (PClass (T, c)) = OFCLASSp (ztyp T, c)
+ | zproof (Oracle (a, prop, SOME Ts)) = zproof_const (ZOracle a) prop Ts
+ | zproof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts, ...}, _)) =
+ let val proof_name =
+ ZThm {theory_name = theory_name, thm_name = thm_name, serial = serial};
+ in zproof_const proof_name prop Ts end;
+ in zproof end;
+
+fun encode_standard_term thy = ZTerm.zterm_of thy #> ZTerm.encode_zterm {typed_vars = false};
+fun encode_standard_proof thy = proof_to_zproof thy #> ZTerm.encode_zproof {typed_vars = false};
+
+
(* encode *)
local
@@ -386,11 +424,13 @@
fn PAxm (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
fn PClass (a, b) => ([b], typ a),
fn Oracle (a, b, c) => ([a], pair (term consts) (option (list typ)) (b, c)),
- fn PThm ({serial, pos, theory_name, thm_name, prop, types}, Thm_Body {open_proof, body, ...}) =>
- ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)],
- 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)))))]
+ fn PThm ({serial, command_pos, theory_name, thm_name, prop, types}, Thm_Body {open_proof, body, ...}) =>
+ ([int_atom serial, theory_name],
+ pair (properties o Position.properties_of)
+ (pair Thm_Name.encode_pos
+ (pair (term consts)
+ (pair (option (list typ)) (proof_body consts))))
+ (command_pos, (thm_name, (prop, (types, map_proof_of open_proof (Future.join body))))))]
and proof_body consts (PBody {oracles, thms, zboxes = _, zproof = _, proof = prf}) =
triple (list (pair (pair string (properties o Position.properties_of))
(option (term consts)))) (list (thm consts)) (proof consts) (oracles, thms, prf)
@@ -399,39 +439,10 @@
(a, (thm_node_theory_name thm_node, (thm_node_name thm_node, (thm_node_prop thm_node,
(Future.join (thm_node_body thm_node))))));
-fun standard_term consts t = t |> variant
- [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
- fn Free (a, _) => ([a], []),
- fn Var (a, _) => (indexname a, []),
- fn Bound a => ([], int a),
- fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)),
- fn t as op $ a =>
- if can Logic.match_of_class t then raise Match
- else ([], pair (standard_term consts) (standard_term consts) a),
- fn t =>
- let val (T, c) = Logic.match_of_class t
- in ([c], typ T) end];
-
-fun standard_proof consts prf = prf |> variant
- [fn MinProof => ([], []),
- fn PBound a => ([], int a),
- fn Abst (a, SOME b, c) => ([a], pair typ (standard_proof consts) (b, c)),
- fn AbsP (a, SOME b, c) => ([a], pair (standard_term consts) (standard_proof consts) (b, c)),
- fn a % SOME b => ([], pair (standard_proof consts) (standard_term consts) (a, b)),
- fn a %% b => ([], pair (standard_proof consts) (standard_proof consts) (a, b)),
- fn Hyp a => ([], standard_term consts a),
- fn PAxm (name, _, SOME Ts) => ([name], list typ Ts),
- fn PClass (T, c) => ([c], typ T),
- fn Oracle (name, prop, SOME Ts) => ([name], pair (standard_term consts) (list typ) (prop, Ts)),
- fn PThm ({serial, theory_name, thm_name, types = SOME Ts, ...}, _) =>
- ([int_atom serial, theory_name, #1 thm_name, int_atom (#2 thm_name)], list typ Ts)];
-
in
-val encode = proof;
-val encode_body = proof_body;
-val encode_standard_term = standard_term;
-val encode_standard_proof = standard_proof;
+val encode = proof o Sign.consts_of;
+val encode_body = proof_body o Sign.consts_of;
end;
@@ -453,12 +464,14 @@
fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in PAxm (a, c, d) end,
fn ([b], a) => PClass (typ a, b),
fn ([a], b) => let val (c, d) = pair (term consts) (option (list typ)) b in Oracle (a, c, d) end,
- fn ([a, b, c, d], e) =>
+ fn ([ser, theory_name], b) =>
let
- val ((x, (y, (z, w)))) =
- pair (list properties) (pair (term consts) (pair (option (list typ)) (proof_body consts))) e;
- val header = thm_header (int_atom a) (map Position.of_properties x) b (c, int_atom d) y z;
- in PThm (header, thm_body w) end]
+ val ((command_pos, (thm_name, (prop, (types, body))))) =
+ pair (Position.of_properties o properties)
+ (pair Thm_Name.decode_pos
+ (pair (term consts) (pair (option (list typ)) (proof_body consts)))) b;
+ val header = thm_header (int_atom ser) command_pos theory_name thm_name prop types;
+ in PThm (header, thm_body body) end]
and proof_body consts x =
let
val (a, b, c) =
@@ -473,8 +486,8 @@
in
-val decode = proof;
-val decode_body = proof_body;
+val decode = proof o Sign.consts_of;
+val decode_body = proof_body o Sign.consts_of;
end;
@@ -562,8 +575,8 @@
| proof (PAxm (a, prop, SOME Ts)) = PAxm (a, prop, SOME (typs Ts))
| proof (PClass C) = ofclass C
| proof (Oracle (a, prop, SOME Ts)) = Oracle (a, prop, SOME (typs Ts))
- | proof (PThm ({serial, pos, theory_name, thm_name, prop, types = SOME Ts}, thm_body)) =
- PThm (thm_header serial pos theory_name thm_name prop (SOME (typs Ts)), thm_body)
+ | proof (PThm ({serial, command_pos, theory_name, thm_name, prop, types = SOME Ts}, thm_body)) =
+ PThm (thm_header serial command_pos theory_name thm_name prop (SOME (typs Ts)), thm_body)
| proof _ = raise Same.SAME;
in proof end;
@@ -603,8 +616,8 @@
fun change_types types (PAxm (name, prop, _)) = PAxm (name, prop, types)
| change_types (SOME [T]) (PClass (_, c)) = PClass (T, c)
| change_types types (Oracle (name, prop, _)) = Oracle (name, prop, types)
- | change_types types (PThm ({serial, pos, theory_name, thm_name, prop, types = _}, thm_body)) =
- PThm (thm_header serial pos theory_name thm_name prop types, thm_body)
+ | change_types types (PThm ({serial, command_pos, theory_name, thm_name, prop, types = _}, thm_body)) =
+ PThm (thm_header serial command_pos theory_name thm_name prop types, thm_body)
| change_types _ prf = prf;
@@ -768,7 +781,7 @@
PClass (norm_type_same T, c)
| norm (Oracle (a, prop, Ts)) =
Oracle (a, prop, Same.map_option norm_types_same Ts)
- | norm (PThm ({serial = i, pos = p, theory_name, thm_name, prop = t, types = Ts}, thm_body)) =
+ | norm (PThm ({serial = i, command_pos = p, theory_name, thm_name, prop = t, types = Ts}, thm_body)) =
PThm (thm_header i p theory_name thm_name t
(Same.map_option norm_types_same Ts), thm_body)
| norm _ = raise Same.SAME;
@@ -1029,8 +1042,8 @@
| proof _ _ (PAxm (a, prop, Ts)) = PAxm (a, prop, typs Ts)
| proof _ _ (PClass (T, c)) = PClass (typ T, c)
| proof _ _ (Oracle (a, prop, Ts)) = Oracle (a, prop, typs Ts)
- | proof _ _ (PThm ({serial, pos, theory_name, thm_name, prop, types}, thm_body)) =
- PThm (thm_header serial pos theory_name thm_name prop (typs types), thm_body)
+ | proof _ _ (PThm ({serial, command_pos, theory_name, thm_name, prop, types}, thm_body)) =
+ PThm (thm_header serial command_pos theory_name thm_name prop (typs types), thm_body)
| proof _ _ _ = raise Same.SAME;
val k = length prems;
@@ -1452,7 +1465,7 @@
| subst _ _ (PAxm (id, prop, Ts)) = PAxm (id, prop, Same.map_option substTs Ts)
| subst _ _ (PClass (T, c)) = PClass (substT T, c)
| subst _ _ (Oracle (id, prop, Ts)) = Oracle (id, prop, Same.map_option substTs Ts)
- | subst _ _ (PThm ({serial = i, pos = p, theory_name, thm_name, prop, types}, thm_body)) =
+ | subst _ _ (PThm ({serial = i, command_pos = p, theory_name, thm_name, prop, types}, thm_body)) =
PThm (thm_header i p theory_name thm_name prop (Same.map_option substTs types), thm_body)
| subst _ _ _ = raise Same.SAME;
in fn t => subst 0 0 t handle Same.SAME => t end;
@@ -1627,7 +1640,7 @@
| guess_name (prf %% PClass _) = guess_name prf
| guess_name (prf % NONE) = guess_name prf
| guess_name (prf % SOME (Var _)) = guess_name prf
- | guess_name _ = Thm_Name.empty;
+ | guess_name _ = Thm_Name.none;
(* generate constraints for proof term *)
@@ -1739,7 +1752,8 @@
| SOME Ts => (Ts, env));
val prop' = subst_atomic_types (prop_types ~~ Ts)
(forall_intr_variables_term prop) handle ListPair.UnequalLengths =>
- error ("Wrong number of type arguments for " ^ quote (Thm_Name.print (guess_name prf)))
+ error ("Wrong number of type arguments for " ^
+ quote (Thm_Name.print_pos (guess_name prf)))
in (prop', change_types (SOME Ts) prf, [], env', vTs) end;
fun head_norm (prop, prf, cnstrts, env, vTs) =
@@ -1927,7 +1941,7 @@
(* expand and reconstruct subproofs *)
fun expand_name_empty (header: thm_header) =
- if Thm_Name.is_empty (#thm_name header) then SOME Thm_Name.empty else NONE;
+ if Thm_Name.is_empty (#1 (#thm_name header)) then SOME Thm_Name.none else NONE;
fun expand_proof thy expand_name prf =
let
@@ -1946,10 +1960,10 @@
let val (seen', maxidx', prf') = expand seen maxidx prf
in (seen', maxidx', prf' % t) end
| expand seen maxidx (prf as PThm (header, thm_body)) =
- let val {serial, pos, theory_name, thm_name, prop, types} = header in
+ let val {serial, command_pos, theory_name, thm_name, prop, types} = header in
(case expand_name header of
SOME thm_name' =>
- if #1 thm_name' = "" andalso is_some types then
+ if #1 (#1 thm_name') = "" andalso is_some types then
let
val (seen', maxidx', prf') =
(case Inttab.lookup seen serial of
@@ -1968,7 +1982,7 @@
in (seen', maxidx' + maxidx + 1, prf'') end
else if thm_name' <> thm_name then
(seen, maxidx,
- PThm (thm_header serial pos theory_name thm_name' prop types, thm_body))
+ PThm (thm_header serial command_pos theory_name thm_name' prop types, thm_body))
else (seen, maxidx, prf)
| NONE => (seen, maxidx, prf))
end
@@ -2160,13 +2174,12 @@
val args = [] |> add_standard_vars_term prop' |> add_standard_vars prf' |> rev;
val typargs = [] |> Term.add_tfrees prop' |> fold_proof_terms Term.add_tfrees prf' |> rev;
- val consts = Sign.consts_of thy;
val xml = (typargs, (args, (prop', no_thm_names prf'))) |>
let
open XML.Encode Term_XML.Encode;
val encode_vars = list (pair string typ);
- val encode_term = encode_standard_term consts;
- val encode_proof = encode_standard_proof consts;
+ val encode_term = encode_standard_term thy;
+ val encode_proof = encode_standard_proof thy;
in pair (list (pair string sort)) (pair encode_vars (pair encode_term encode_proof)) end;
in
Export.export_params (Context.Theory thy)
@@ -2199,7 +2212,7 @@
fun new_prf () =
let
- val i = serial ();
+ val i = proof_serial ();
val unconstrainT = unconstrainT_proof (Sign.classes_of thy) sorts_proof ucontext;
val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy);
val body1 =
@@ -2211,11 +2224,11 @@
if export_enabled () then new_prf ()
else
(case strip_combt (proof_head_of proof0) of
- (PThm ({serial = ser, thm_name = a, prop = prop', types = NONE, ...}, thm_body'), args') =>
+ (PThm ({serial = ser, thm_name = (a, _), prop = prop', types = NONE, ...}, thm_body'), args') =>
if (#1 a = "" orelse a = name) andalso prop' = prop1 andalso args' = args then
let
val Thm_Body {body = body', ...} = thm_body';
- val i = if #1 a = "" andalso named then serial () else ser;
+ val i = if #1 a = "" andalso named then proof_serial () else ser;
in (i, body' |> ser <> i ? Future.map (map_proof_of (rew_proof thy))) end
else new_prf ()
| _ => new_prf ());
@@ -2244,7 +2257,7 @@
val theory_name = Context.theory_long_name thy;
val thm = (i, make_thm_node theory_name name prop1 thm_body export);
- val header = thm_header i ([pos, Position.thread_data ()]) theory_name name prop1 NONE;
+ val header = thm_header i (Position.thread_data ()) theory_name (name, pos) prop1 NONE;
val head = PThm (header, Thm_Body {open_proof = open_proof, body = thm_body});
val argst =
if unconstrain then
@@ -2283,7 +2296,7 @@
end;
fun get_approximative_name shyps hyps prop prf =
- Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.empty;
+ Option.map #thm_name (get_identity shyps hyps prop prf) |> the_default Thm_Name.none;
(* thm_id *)
@@ -2302,7 +2315,7 @@
fun get_id shyps hyps prop prf : thm_id option =
(case get_identity shyps hyps prop prf of
NONE => NONE
- | SOME {serial, theory_name, thm_name, ...} =>
+ | SOME {serial, theory_name, thm_name = (thm_name, _), ...} =>
if Thm_Name.is_empty thm_name then NONE else SOME (make_thm_id (serial, theory_name)));
fun this_id NONE _ = false
--- a/src/Pure/term_items.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/term_items.ML Fri Jul 19 22:29:32 2024 +0100
@@ -34,7 +34,8 @@
val make1: key * 'a -> 'a table
val make2: key * 'a -> key * 'a -> 'a table
val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
- val unsynchronized_cache: (key -> 'a) -> key -> 'a
+ type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
+ val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
type set = int table
val add_set: key -> set -> set
val make_set: key list -> set
@@ -86,6 +87,7 @@
fun make2 e1 e2 = build (add e1 #> add e2);
fun make3 e1 e2 e3 = build (add e1 #> add e2 #> add e3);
+type 'a cache_ops = 'a Table.cache_ops;
val unsynchronized_cache = Table.unsynchronized_cache;
--- a/src/Pure/term_xml.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/term_xml.ML Fri Jul 19 22:29:32 2024 +0100
@@ -12,7 +12,6 @@
val sort: sort T
val typ: typ T
val term_raw: term T
- val typ_body: typ T
val term: Consts.T -> term T
end
@@ -47,12 +46,12 @@
fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
fn op $ a => ([], pair term_raw term_raw a)];
-fun typ_body T = if T = dummyT then [] else typ T;
+fun var_type T = if T = dummyT then [] else typ T;
fun term consts t = t |> variant
[fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
- fn Free (a, b) => ([a], typ_body b),
- fn Var (a, b) => (indexname a, typ_body b),
+ fn Free (a, b) => ([a], var_type b),
+ fn Var (a, b) => (indexname a, var_type b),
fn Bound a => ([], int a),
fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
fn t as op $ a =>
@@ -87,13 +86,13 @@
fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end,
fn ([], a) => op $ (pair term_raw term_raw a)];
-fun typ_body [] = dummyT
- | typ_body body = typ body;
+fun var_type [] = dummyT
+ | var_type body = typ body;
fun term consts body = body |> variant
[fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)),
- fn ([a], b) => Free (a, typ_body b),
- fn (a, b) => Var (indexname a, typ_body b),
+ fn ([a], b) => Free (a, var_type b),
+ fn (a, b) => Var (indexname a, var_type b),
fn ([], a) => Bound (int a),
fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
fn ([], a) => op $ (pair (term consts) (term consts) a),
--- a/src/Pure/term_xml.scala Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/term_xml.scala Fri Jul 19 22:29:32 2024 +0100
@@ -25,13 +25,13 @@
{ case TFree(a, b) => (List(a), sort(b)) },
{ case TVar(a, b) => (indexname(a), sort(b)) }))
- val typ_body: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t)
+ private val var_type: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t)
def term: T[Term] =
variant[Term](List(
{ case Const(a, b) => (List(a), list(typ)(b)) },
- { case Free(a, b) => (List(a), typ_body(b)) },
- { case Var(a, b) => (indexname(a), typ_body(b)) },
+ { case Free(a, b) => (List(a), var_type(b)) },
+ { case Var(a, b) => (indexname(a), var_type(b)) },
{ case Bound(a) => (Nil, int(a)) },
{ case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
{ case App(a, b) => (Nil, pair(term, term)(a, b)) },
@@ -53,13 +53,13 @@
{ case (List(a), b) => TFree(a, sort(b)) },
{ case (a, b) => TVar(indexname(a), sort(b)) }))
- val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) }
+ private val var_type: T[Typ] = { case Nil => dummyT case body => typ(body) }
def term: T[Term] =
variant[Term](List(
{ case (List(a), b) => Const(a, list(typ)(b)) },
- { case (List(a), b) => Free(a, typ_body(b)) },
- { case (a, b) => Var(indexname(a), typ_body(b)) },
+ { case (List(a), b) => Free(a, var_type(b)) },
+ { case (a, b) => Var(indexname(a), var_type(b)) },
{ case (Nil, a) => Bound(int(a)) },
{ case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
{ case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) },
@@ -72,8 +72,8 @@
def term: T[Term] =
variant[Term](List(
{ case (List(a), b) => Const(a, list(typ)(b)) },
- { case (List(a), b) => Free(a, env_type(a, typ_body(b))) },
- { case (a, b) => Var(indexname(a), typ_body(b)) },
+ { case (List(a), b) => Free(a, env_type(a, var_type(b))) },
+ { case (a, b) => Var(indexname(a), var_type(b)) },
{ case (Nil, a) => Bound(int(a)) },
{ case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
{ case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) },
--- a/src/Pure/thm.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/thm.ML Fri Jul 19 22:29:32 2024 +0100
@@ -120,8 +120,8 @@
val derivation_closed: thm -> bool
val derivation_name: thm -> Thm_Name.T
val derivation_id: thm -> Proofterm.thm_id option
- val raw_derivation_name: thm -> Thm_Name.T
- val expand_name: thm -> Proofterm.thm_header -> Thm_Name.T option
+ val raw_derivation_name: thm -> Thm_Name.P
+ val expand_name: thm -> Proofterm.thm_header -> Thm_Name.P option
val name_derivation: Thm_Name.P -> thm -> thm
val close_derivation: Position.T -> thm -> thm
val trim_context: thm -> thm
@@ -1100,8 +1100,8 @@
SOME T' => T'
| NONE => raise Fail "strip_shyps: bad type variable in proof term"));
val map_ztyp =
- ZTypes.unsynchronized_cache
- (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar));
+ #apply (ZTypes.unsynchronized_cache
+ (ZTerm.subst_type_same (ZTerm.ztyp_of o map_atyp o ZTerm.typ_of o ZTVar)));
val zproof' = ZTerm.map_proof_types {hyps = true} map_ztyp zproof;
val proof' = Proofterm.map_proof_types (Term.map_atyps_same map_atyp) proof;
@@ -1131,13 +1131,13 @@
NONE => K false
| SOME {serial, ...} => fn (header: Proofterm.thm_header) => serial = #serial header);
fun expand header =
- if self_id header orelse Thm_Name.is_empty (#thm_name header)
- then SOME Thm_Name.empty else NONE;
+ if self_id header orelse Thm_Name.is_empty (#1 (#thm_name header))
+ then SOME Thm_Name.none else NONE;
in expand end;
(*deterministic name of finished proof*)
fun derivation_name (thm as Thm (_, {shyps, hyps, prop, ...})) =
- Proofterm.get_approximative_name shyps hyps prop (proof_of thm);
+ #1 (Proofterm.get_approximative_name shyps hyps prop (proof_of thm));
(*identified PThm node*)
fun derivation_id (thm as Thm (_, {shyps, hyps, prop, ...})) =
--- a/src/Pure/thm_deps.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/thm_deps.ML Fri Jul 19 22:29:32 2024 +0100
@@ -59,7 +59,7 @@
else
let val thm_id = Proofterm.thm_id (i, thm_node) in
(case lookup thm_id of
- SOME thm_name =>
+ SOME (thm_name, _) =>
Inttab.update (i, SOME (thm_id, thm_name)) res
| NONE =>
Inttab.update (i, NONE) res
--- a/src/Pure/thm_name.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/thm_name.ML Fri Jul 19 22:29:32 2024 +0100
@@ -26,9 +26,12 @@
val print_prefix: Context.generic -> Name_Space.T -> T -> Markup.T * string
val print_suffix: T -> string
val print: T -> string
+ val print_pos: P -> string
val short: T -> string
val encode: T XML.Encode.T
val decode: T XML.Decode.T
+ val encode_pos: P XML.Encode.T
+ val decode_pos: P XML.Decode.T
end;
structure Thm_Name: THM_NAME =
@@ -106,6 +109,8 @@
fun print (name, index) = name ^ print_suffix (name, index);
+fun print_pos (thm_name, pos) = print thm_name ^ Position.here pos;
+
fun short (name, index) =
if name = "" orelse index = 0 then name
else name ^ "_" ^ string_of_int index;
@@ -116,4 +121,7 @@
val encode = let open XML.Encode in pair string int end;
val decode = let open XML.Decode in pair string int end;
+val encode_pos = let open XML.Encode in pair encode (properties o Position.properties_of) end;
+val decode_pos = let open XML.Decode in pair decode (Position.of_properties o properties) end;
+
end;
--- a/src/Pure/zterm.ML Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Pure/zterm.ML Fri Jul 19 22:29:32 2024 +0100
@@ -251,10 +251,15 @@
val map_proof_types: {hyps: bool} -> ztyp Same.operation -> zproof -> zproof
val map_class_proof: (ztyp * class, zproof) Same.function -> zproof -> zproof
val ztyp_of: typ -> ztyp
+ val ztyp_dummy: ztyp
+ val typ_of_tvar: indexname * sort -> typ
+ val typ_of: ztyp -> typ
+ val reset_cache: theory -> theory
+ val check_cache: theory -> {ztyp: int, typ: int} option
+ val ztyp_cache: theory -> typ -> ztyp
+ val typ_cache: theory -> ztyp -> typ
val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp}
val zterm_of: theory -> term -> zterm
- val typ_of_tvar: indexname * sort -> typ
- val typ_of: ztyp -> typ
val term_of: theory -> zterm -> term
val beta_norm_term_same: zterm Same.operation
val beta_norm_proof_same: zproof Same.operation
@@ -262,7 +267,7 @@
val beta_norm_term: zterm -> zterm
val beta_norm_proof: zproof -> zproof
val beta_norm_prooft: zproof -> zproof
- val norm_type: Type.tyenv -> ztyp -> ztyp
+ val norm_type: theory -> Type.tyenv -> ztyp -> ztyp
val norm_term: theory -> Envir.env -> zterm -> zterm
val norm_proof: theory -> Envir.env -> term list -> zproof -> zproof
val zproof_const_typargs: zproof_const -> ((indexname * sort) * ztyp) list
@@ -310,6 +315,9 @@
val of_sort_proof: Sorts.algebra -> sorts_proof -> (typ * class -> zproof) ->
typ * sort -> zproof list
val unconstrainT_proof: theory -> sorts_proof -> Logic.unconstrain_context -> zproof -> zproof
+ val encode_ztyp: ztyp XML.Encode.T
+ val encode_zterm: {typed_vars: bool} -> zterm XML.Encode.T
+ val encode_zproof: {typed_vars: bool} -> zproof XML.Encode.T
end;
structure ZTerm: ZTERM =
@@ -470,7 +478,7 @@
fun instantiate_type_same instT =
if ZTVars.is_empty instT then Same.same
- else ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT)));
+ else #apply (ZTypes.unsynchronized_cache (subst_type_same (Same.function (ZTVars.lookup instT))));
fun instantiate_term_same typ inst =
subst_term_same typ (Same.function (ZVars.lookup inst));
@@ -577,7 +585,7 @@
in Same.commit proof end;
-(* convert ztyp / zterm vs. regular typ / term *)
+(* convert ztyp vs. regular typ *)
fun ztyp_of (TFree (a, S)) = ZTVar ((a, ~1), S)
| ztyp_of (TVar v) = ZTVar v
@@ -587,13 +595,75 @@
| ztyp_of (Type (c, [T])) = ZType1 (c, ztyp_of T)
| ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts);
-fun ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
+val ztyp_dummy = ztyp_of dummyT;
+
+fun typ_of_tvar ((a, ~1), S) = TFree (a, S)
+ | typ_of_tvar v = TVar v;
+
+fun typ_of (ZTVar v) = typ_of_tvar v
+ | typ_of (ZFun (T, U)) = typ_of T --> typ_of U
+ | typ_of ZProp = propT
+ | typ_of (ZType0 c) = Type (c, [])
+ | typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
+ | typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
+
+
+(* cache within theory context *)
+
+local
+
+structure Data = Theory_Data
+(
+ type T = (ztyp Typtab.cache_ops * typ ZTypes.cache_ops) option;
+ val empty = NONE;
+ val merge = K NONE;
+);
+
+fun make_ztyp_cache () = Typtab.unsynchronized_cache ztyp_of;
+fun make_typ_cache () = ZTypes.unsynchronized_cache typ_of;
+
+fun init_cache thy =
+ if is_some (Data.get thy) then NONE
+ else SOME (Data.put (SOME (make_ztyp_cache (), make_typ_cache ())) thy);
+
+fun exit_cache thy =
+ (case Data.get thy of
+ SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); SOME (Data.put NONE thy))
+ | NONE => NONE);
+
+in
+
+val _ = Theory.setup (Theory.at_begin init_cache #> Theory.at_end exit_cache);
+
+fun reset_cache thy =
+ (case Data.get thy of
+ SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); thy)
+ | NONE => thy);
+
+fun check_cache thy =
+ Data.get thy
+ |> Option.map (fn (cache1, cache2) => {ztyp = #size cache1 (), typ = #size cache2 ()});
+
+fun ztyp_cache thy =
+ (case Data.get thy of
+ SOME (cache, _) => cache
+ | NONE => make_ztyp_cache ()) |> #apply;
+
+fun typ_cache thy =
+ (case Data.get thy of
+ SOME (_, cache) => cache
+ | NONE => make_typ_cache ()) |> #apply;
+
+end;
+
+
+(* convert zterm vs. regular term *)
fun zterm_cache thy =
let
val typargs = Consts.typargs (Sign.consts_of thy);
- val ztyp = ztyp_cache ();
+ val ztyp = ztyp_cache thy;
fun zterm (Free (x, T)) = ZVar ((x, ~1), ztyp T)
| zterm (Var (xi, T)) = ZVar (xi, ztyp T)
@@ -612,18 +682,6 @@
val zterm_of = #zterm o zterm_cache;
-fun typ_of_tvar ((a, ~1), S) = TFree (a, S)
- | typ_of_tvar v = TVar v;
-
-fun typ_of (ZTVar v) = typ_of_tvar v
- | typ_of (ZFun (T, U)) = typ_of T --> typ_of U
- | typ_of ZProp = propT
- | typ_of (ZType0 c) = Type (c, [])
- | typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
- | typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
-
-fun typ_cache () = ZTypes.unsynchronized_cache typ_of;
-
fun term_of thy =
let
val instance = Consts.instance (Sign.consts_of thy);
@@ -717,11 +775,13 @@
| norm (ZType (a, Ts)) = ZType (a, Same.map norm Ts);
in norm end;
-fun norm_term_same {ztyp, zterm, typ} (envir as Envir.Envir {tyenv, tenv, ...}) =
+fun norm_term_same {ztyp, zterm} (envir as Envir.Envir {tyenv, tenv, ...}) =
let
val lookup =
if Vartab.is_empty tenv then K NONE
- else ZVars.unsynchronized_cache (apsnd typ #> Envir.lookup envir #> Option.map zterm);
+ else
+ #apply (ZVars.unsynchronized_cache
+ (apsnd typ_of #> Envir.lookup envir #> Option.map zterm));
val normT = norm_type_same ztyp tyenv;
@@ -776,15 +836,9 @@
in beta_norm_prooft (map_proof {hyps = false} inst_typ norm_term prf) end
end;
-fun norm_cache thy =
- let
- val {ztyp, zterm} = zterm_cache thy;
- val typ = typ_cache ();
- in {ztyp = ztyp, zterm = zterm, typ = typ} end;
-
-fun norm_type tyenv = Same.commit (norm_type_same (ztyp_cache ()) tyenv);
-fun norm_term thy envir = Same.commit (norm_term_same (norm_cache thy) envir);
-fun norm_proof thy envir = norm_proof_cache (norm_cache thy) envir;
+fun norm_type thy tyenv = Same.commit (norm_type_same (ztyp_cache thy) tyenv);
+fun norm_term thy envir = Same.commit (norm_term_same (zterm_cache thy) envir);
+fun norm_proof thy envir = norm_proof_cache (zterm_cache thy) envir;
@@ -870,7 +924,8 @@
val typ_operation = #typ_operation ucontext {strip_sorts = true};
val unconstrain_typ = Same.commit typ_operation;
val unconstrain_ztyp =
- ZTypes.unsynchronized_cache (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of));
+ #apply (ZTypes.unsynchronized_cache
+ (Same.function_eq (op =) (typ_of #> unconstrain_typ #> ztyp_of)));
val unconstrain_zterm = zterm o Term.map_types typ_operation;
val unconstrain_proof = Same.commit (map_proof_types {hyps = true} unconstrain_ztyp);
@@ -1087,10 +1142,10 @@
val typ =
if Names.is_empty tfrees then Same.same
else
- ZTypes.unsynchronized_cache
+ #apply (ZTypes.unsynchronized_cache
(subst_type_same (fn ((a, i), S) =>
if i = ~1 andalso Names.defined tfrees a then ZTVar ((a, idx), S)
- else raise Same.SAME));
+ else raise Same.SAME)));
val term =
subst_term_same typ (fn ((x, i), T) =>
if i = ~1 andalso Names.defined frees x then ZVar ((x, idx), T)
@@ -1112,10 +1167,10 @@
let
val tab = ZTVars.build (names |> fold (fn ((a, S), b) => ZTVars.add (((a, ~1), S), b)));
val typ =
- ZTypes.unsynchronized_cache (subst_type_same (fn v =>
+ #apply (ZTypes.unsynchronized_cache (subst_type_same (fn v =>
(case ZTVars.lookup tab v of
NONE => raise Same.SAME
- | SOME w => ZTVar w)));
+ | SOME w => ZTVar w))));
in map_proof_types {hyps = false} typ prf end;
fun legacy_freezeT_proof t prf =
@@ -1124,7 +1179,7 @@
| SOME f =>
let
val tvar = ztyp_of o Same.function f;
- val typ = ZTypes.unsynchronized_cache (subst_type_same tvar);
+ val typ = #apply (ZTypes.unsynchronized_cache (subst_type_same tvar));
in map_proof_types {hyps = false} typ prf end);
@@ -1158,7 +1213,7 @@
if inc = 0 then Same.same
else
let fun tvar ((a, i), S) = if i >= 0 then ZTVar ((a, i + inc), S) else raise Same.SAME
- in ZTypes.unsynchronized_cache (subst_type_same tvar) end;
+ in #apply (ZTypes.unsynchronized_cache (subst_type_same tvar)) end;
fun incr_indexes_proof inc prf =
let
@@ -1240,7 +1295,7 @@
fun assumption_proof thy envir Bs Bi n visible prf =
let
- val cache as {zterm, ...} = norm_cache thy;
+ val cache as {zterm, ...} = zterm_cache thy;
val normt = zterm #> Same.commit (norm_term_same cache envir);
in
ZAbsps (map normt Bs)
@@ -1258,7 +1313,7 @@
fun bicompose_proof thy env smax flatten Bs As A oldAs n m visible rprf sprf =
let
- val cache as {zterm, ...} = norm_cache thy;
+ val cache as {zterm, ...} = zterm_cache thy;
val normt = zterm #> Same.commit (norm_term_same cache env);
val normp = norm_proof_cache cache env visible;
@@ -1292,12 +1347,14 @@
fun unconstrainT_proof thy sorts_proof (ucontext: Logic.unconstrain_context) =
let
- val cache = norm_cache thy;
val algebra = Sign.classes_of thy;
+ val cache = zterm_cache thy;
+ val typ_cache = typ_cache thy;
+
val typ =
- ZTypes.unsynchronized_cache
- (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of);
+ #apply (ZTypes.unsynchronized_cache
+ (typ_of #> #typ_operation ucontext {strip_sorts = true} #> ztyp_of));
val typ_sort = #typ_operation ucontext {strip_sorts = false};
@@ -1307,11 +1364,67 @@
| NONE => raise Fail "unconstrainT_proof: missing constraint");
fun class (T, c) =
- let val T' = Same.commit typ_sort (#typ cache T)
+ let val T' = Same.commit typ_sort (typ_cache T)
in the_single (of_sort_proof algebra sorts_proof hyps (T', [c])) end;
in
map_proof_types {hyps = false} typ #> map_class_proof class #> beta_norm_prooft
#> fold_rev (implies_intr_proof' o #zterm cache o #2) (#constraints ucontext)
end;
+
+
+(** XML data representation **)
+
+(* encode *)
+
+local
+
+open XML.Encode Term_XML.Encode;
+
+fun ztyp T = T |> variant
+ [fn ZFun args => (["fun"], pair ztyp ztyp args)
+ | ZProp => (["prop"], [])
+ | ZType0 a => ([a], [])
+ | ZType1 (a, b) => ([a], list ztyp [b])
+ | ZType (a, b) => ([a], list ztyp b),
+ fn ZTVar ((a, ~1), b) => ([a], sort b),
+ fn ZTVar (a, b) => (indexname a, sort b)];
+
+fun zvar_type {typed_vars} T =
+ if typed_vars andalso T <> ztyp_dummy then ztyp T else [];
+
+fun zterm flag t = t |> variant
+ [fn ZConst0 a => ([a], [])
+ | ZConst1 (a, b) => ([a], list ztyp [b])
+ | ZConst (a, b) => ([a], list ztyp b),
+ fn ZVar ((a, ~1), b) => ([a], zvar_type flag b),
+ fn ZVar (a, b) => (indexname a, zvar_type flag b),
+ fn ZBound a => ([], int a),
+ fn ZAbs (a, b, c) => ([a], pair ztyp (zterm flag) (b, c)),
+ fn ZApp a => ([], pair (zterm flag) (zterm flag) a),
+ fn OFCLASS (a, b) => ([b], ztyp a)];
+
+fun zproof flag prf = prf |> variant
+ [fn ZNop => ([], []),
+ fn ZBoundp a => ([], int a),
+ fn ZAbst (a, b, c) => ([a], pair ztyp (zproof flag) (b, c)),
+ fn ZAbsp (a, b, c) => ([a], pair (zterm flag) (zproof flag) (b, c)),
+ fn ZAppt a => ([], pair (zproof flag) (zterm flag) a),
+ fn ZAppp a => ([], pair (zproof flag) (zproof flag) a),
+ fn ZHyp a => ([], zterm flag a),
+ fn ZConstp (c as ((ZAxiom a, b), _)) => ([a], list (ztyp o #2) (zproof_const_typargs c)),
+ fn OFCLASSp (a, b) => ([b], ztyp a),
+ fn ZConstp (c as ((ZOracle a, b), _)) => ([a], list (ztyp o #2) (zproof_const_typargs c)),
+ fn ZConstp (c as ((ZThm {theory_name, thm_name = (name, _), serial}, b), _)) =>
+ ([int_atom serial, theory_name, #1 name, int_atom (#2 name)],
+ list (ztyp o #2) (zproof_const_typargs c))];
+
+in
+
+val encode_ztyp = ztyp;
+val encode_zterm = zterm;
+val encode_zproof = zproof;
+
end;
+
+end;
--- a/src/Tools/Haskell/Haskell.thy Fri Jul 19 22:29:16 2024 +0100
+++ b/src/Tools/Haskell/Haskell.thy Fri Jul 19 22:29:32 2024 +0100
@@ -2651,7 +2651,7 @@
{-# LANGUAGE LambdaCase #-}
-module Isabelle.Term_XML.Encode (indexname, sort, typ, typ_body, term)
+module Isabelle.Term_XML.Encode (indexname, sort, typ, term)
where
import Isabelle.Library
@@ -2671,15 +2671,15 @@
\case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
\case { TVar (a, b) -> Just (indexname a, sort b); _ -> Nothing }]
-typ_body :: T Typ
-typ_body ty = if is_dummyT ty then [] else typ ty
+var_type :: T Typ
+var_type ty = if is_dummyT ty then [] else typ ty
term :: T Term
term t =
t |> variant
[\case { Const (a, b) -> Just ([a], list typ b); _ -> Nothing },
- \case { Free (a, b) -> Just ([a], typ_body b); _ -> Nothing },
- \case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing },
+ \case { Free (a, b) -> Just ([a], var_type b); _ -> Nothing },
+ \case { Var (a, b) -> Just (indexname a, var_type b); _ -> Nothing },
\case { Bound a -> Just ([], int a); _ -> Nothing },
\case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
\case { App a -> Just ([], pair term term a); _ -> Nothing },
@@ -2698,7 +2698,7 @@
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
-module Isabelle.Term_XML.Decode (indexname, sort, typ, typ_body, term)
+module Isabelle.Term_XML.Decode (indexname, sort, typ, term)
where
import Isabelle.Library
@@ -2720,16 +2720,16 @@
\([a], b) -> TFree (a, sort b),
\(a, b) -> TVar (indexname a, sort b)]
-typ_body :: T Typ
-typ_body [] = dummyT
-typ_body body = typ body
+var_type :: T Typ
+var_type [] = dummyT
+var_type body = typ body
term :: T Term
term t =
t |> variant
[\([a], b) -> Const (a, list typ b),
- \([a], b) -> Free (a, typ_body b),
- \(a, b) -> Var (indexname a, typ_body b),
+ \([a], b) -> Free (a, var_type b),
+ \(a, b) -> Var (indexname a, var_type b),
\([], a) -> Bound (int a),
\([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
\([], a) -> App (pair term term a),