--- a/NEWS Mon Oct 28 18:48:14 2024 +0100
+++ b/NEWS Mon Oct 28 18:48:28 2024 +0100
@@ -56,19 +56,19 @@
manner, but more complex translations may require manual changes: rare
INCOMPATIBILITY.
-* Printing term abbreviations now uses a different rewrite strategy:
-alternate top-down, bottom-up, top-down etc. until a normal form is
-reached. This is more efficient than the former top-down strategy. It
-also conforms to AST rewriting (command 'translations'). Rare
-INCOMPATIBILITY, slightly different results could be printed (often
-slightly "better" ones).
-
-* Blocks for pretty-printing now support properties "open_block" (bool)
-and "notation" (string as cartouche). When "open_block" is enabled, the
-block has no impact on formatting, but it may carry markup information
-via "notation". The latter uses formal kinds (e.g. "mixfix", "infix",
-"binder") together with informal words to describe the notation. This
-markup affects both input and output of inner syntax --- it can be
+* Printing term abbreviations now uses more efficient matching and
+rewrite strategy: alternate top-down, bottom-up, top-down etc. until a
+normal form is reached. This usually works better than the former
+top-down strategy, it also conforms to AST rewriting (command
+'translations'). Rare INCOMPATIBILITY, slightly different results could
+be printed.
+
+* Blocks in mixfix annotations now support properties "open_block"
+(bool) and "notation" (string as cartouche). When "open_block" is
+enabled, the block has no impact on formatting, but it may carry markup
+information via "notation". The latter uses formal kinds (e.g. "mixfix",
+"infix", "binder") together with informal words to describe the
+notation. This markup affects both parsing and printing --- it can be
explored via mouse hovering in the Prover IDE, or programmatically by
Isabelle/Scala tools. Markup for "infix" and "binder" declarations are
automatic, but general mixfix forms require manual annotations in the
--- a/src/HOL/Bali/State.thy Mon Oct 28 18:48:14 2024 +0100
+++ b/src/HOL/Bali/State.thy Mon Oct 28 18:48:28 2024 +0100
@@ -131,19 +131,15 @@
subsubsection "object references"
type_synonym oref = "loc + qtname" \<comment> \<open>generalized object reference\<close>
-syntax
- Heap :: "loc \<Rightarrow> oref"
- Stat :: "qtname \<Rightarrow> oref"
-
-syntax_consts
- Heap == Inl and
- Stat == Inr
translations
- "Heap" => "CONST Inl"
- "Stat" => "CONST Inr"
(type) "oref" <= (type) "loc + qtname"
+abbreviation (input)
+ Heap :: "loc \<Rightarrow> oref" where "Heap \<equiv> Inl"
+abbreviation (input)
+ Stat :: "qtname \<Rightarrow> oref" where "Stat \<equiv> Inr"
+
definition
fields_table :: "prog \<Rightarrow> qtname \<Rightarrow> (fspec \<Rightarrow> field \<Rightarrow> bool) \<Rightarrow> (fspec, ty) table" where
"fields_table G C P =
--- a/src/HOL/Library/Cardinality.thy Mon Oct 28 18:48:14 2024 +0100
+++ b/src/HOL/Library/Cardinality.thy Mon Oct 28 18:48:28 2024 +0100
@@ -74,8 +74,9 @@
lemma card_fun: "CARD('a \<Rightarrow> 'b) = (if CARD('a) \<noteq> 0 \<and> CARD('b) \<noteq> 0 \<or> CARD('b) = 1 then CARD('b) ^ CARD('a) else 0)"
proof -
- { assume "0 < CARD('a)" and "0 < CARD('b)"
- hence fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
+ have "CARD('a \<Rightarrow> 'b) = CARD('b) ^ CARD('a)" if "0 < CARD('a)" and "0 < CARD('b)"
+ proof -
+ from that have fina: "finite (UNIV :: 'a set)" and finb: "finite (UNIV :: 'b set)"
by(simp_all only: card_ge_0_finite)
from finite_distinct_list[OF finb] obtain bs
where bs: "set bs = (UNIV :: 'b set)" and distb: "distinct bs" by blast
@@ -113,19 +114,23 @@
qed
hence "card (set ?xs) = length ?xs" by(simp only: distinct_card)
moreover have "length ?xs = length bs ^ length as" by(simp add: length_n_lists)
- ultimately have "CARD('a \<Rightarrow> 'b) = CARD('b) ^ CARD('a)" using cb ca by simp }
- moreover {
- assume cb: "CARD('b) = 1"
- then obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
+ ultimately show ?thesis using cb ca by simp
+ qed
+ moreover have "CARD('a \<Rightarrow> 'b) = 1" if "CARD('b) = 1"
+ proof -
+ from that obtain b where b: "UNIV = {b :: 'b}" by(auto simp add: card_Suc_eq)
have eq: "UNIV = {\<lambda>x :: 'a. b ::'b}"
proof(rule UNIV_eq_I)
fix x :: "'a \<Rightarrow> 'b"
- { fix y
+ have "x y = b" for y
+ proof -
have "x y \<in> UNIV" ..
- hence "x y = b" unfolding b by simp }
+ thus ?thesis unfolding b by simp
+ qed
thus "x \<in> {\<lambda>x. b}" by(auto)
qed
- have "CARD('a \<Rightarrow> 'b) = 1" unfolding eq by simp }
+ show ?thesis unfolding eq by simp
+ qed
ultimately show ?thesis
by(auto simp del: One_nat_def)(auto simp add: card_eq_0_iff dest: finite_fun_UNIVD2 finite_fun_UNIVD1)
qed
--- a/src/HOL/Library/Complete_Partial_Order2.thy Mon Oct 28 18:48:14 2024 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Mon Oct 28 18:48:28 2024 +0100
@@ -4,8 +4,8 @@
section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
-theory Complete_Partial_Order2 imports
- Main
+theory Complete_Partial_Order2
+ imports Main
begin
unbundle lattice_syntax
@@ -604,7 +604,7 @@
and mcont: "\<And>f. mcont lub (\<sqsubseteq>) Sup (\<le>) f \<Longrightarrow> mcont lub (\<sqsubseteq>) Sup (\<le>) (F f)"
shows "mcont lub (\<sqsubseteq>) Sup (\<le>) (ccpo.fixp (fun_lub Sup) (fun_ord (\<le>)) F)"
(is "mcont _ _ _ _ ?fixp")
-unfolding mcont_def
+ unfolding mcont_def
proof(intro conjI monotoneI contI)
have mono: "monotone (fun_ord (\<le>)) (fun_ord (\<le>)) F"
by(rule monotoneI)(auto simp add: fun_ord_def intro: monotoneD[OF mono])
@@ -612,36 +612,33 @@
have chain: "\<And>x. Complete_Partial_Order.chain (\<le>) ((\<lambda>f. f x) ` ?iter)"
by(rule chain_imageI[OF ccpo.chain_iterates[OF ccpo_fun mono]])(simp add: fun_ord_def)
- {
- fix x y
- assume "x \<sqsubseteq> y"
- show "?fixp x \<le> ?fixp y"
- apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
- using chain
- proof(rule ccpo_Sup_least)
- fix x'
- assume "x' \<in> (\<lambda>f. f x) ` ?iter"
- then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
- also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
- by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
- also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
- by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
- finally show "x' \<le> \<dots>" .
- qed
- next
- fix Y
- assume chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
- and Y: "Y \<noteq> {}"
- { fix f
- assume "f \<in> ?iter"
- hence "f (\<Or>Y) = \<Squnion>(f ` Y)"
- using mcont chain Y by(rule mcont_contD[OF iterates_mcont]) }
+ show "?fixp x \<le> ?fixp y" if "x \<sqsubseteq> y" for x y
+ apply (simp only: ccpo.fixp_def[OF ccpo_fun] fun_lub_apply)
+ using chain
+ proof(rule ccpo_Sup_least)
+ fix x'
+ assume "x' \<in> (\<lambda>f. f x) ` ?iter"
+ then obtain f where "f \<in> ?iter" "x' = f x" by blast note this(2)
+ also from _ \<open>x \<sqsubseteq> y\<close> have "f x \<le> f y"
+ by(rule mcont_monoD[OF iterates_mcont[OF \<open>f \<in> ?iter\<close> mcont]])
+ also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` ?iter)" using chain
+ by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> ?iter\<close>)
+ finally show "x' \<le> \<dots>" .
+ qed
+
+ show "?fixp (\<Or>Y) = \<Squnion>(?fixp ` Y)"
+ if chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y" and Y: "Y \<noteq> {}" for Y
+ proof -
+ have "f (\<Or>Y) = \<Squnion>(f ` Y)" if "f \<in> ?iter" for f
+ using that mcont chain Y
+ by (rule mcont_contD[OF iterates_mcont])
moreover have "\<Squnion>((\<lambda>f. \<Squnion>(f ` Y)) ` ?iter) = \<Squnion>((\<lambda>x. \<Squnion>((\<lambda>f. f x) ` ?iter)) ` Y)"
using chain ccpo.chain_iterates[OF ccpo_fun mono]
- by(rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]])
- ultimately show "?fixp (\<Or>Y) = \<Squnion>(?fixp ` Y)" unfolding ccpo.fixp_def[OF ccpo_fun]
- by(simp add: fun_lub_apply cong: image_cong)
- }
+ by (rule swap_Sup)(rule mcont_mono[OF iterates_mcont[OF _ mcont]])
+ ultimately show ?thesis
+ unfolding ccpo.fixp_def[OF ccpo_fun]
+ by (simp add: fun_lub_apply cong: image_cong)
+ qed
qed
end
@@ -1753,12 +1750,14 @@
from A obtain z where "z \<in> A" by blast
with * have z: "\<not> flat_ord x y z" ..
hence y: "x \<noteq> y" "y \<noteq> z" by(auto simp add: flat_ord_def)
- { assume "\<not> A \<subseteq> {x}"
- then obtain z' where "z' \<in> A" "z' \<noteq> x" by auto
+ have "y \<noteq> (THE z. z \<in> A - {x})" if "\<not> A \<subseteq> {x}"
+ proof -
+ from that obtain z' where "z' \<in> A" "z' \<noteq> x" by auto
then have "(THE z. z \<in> A - {x}) = z'"
by(intro the_equality)(auto dest: chainD[OF chain] simp add: flat_ord_def)
moreover have "z' \<noteq> y" using \<open>z' \<in> A\<close> * by(auto simp add: flat_ord_def)
- ultimately have "y \<noteq> (THE z. z \<in> A - {x})" by simp }
+ ultimately show ?thesis by simp
+ qed
with z show "\<not> flat_ord x y (flat_lub x A)" by(simp add: flat_ord_def flat_lub_def)
qed
--- a/src/Pure/Isar/auto_bind.ML Mon Oct 28 18:48:14 2024 +0100
+++ b/src/Pure/Isar/auto_bind.ML Mon Oct 28 18:48:28 2024 +0100
@@ -12,7 +12,9 @@
val assmsN: string
val abs_params: term -> term -> term
val goal: Proof.context -> term list -> (indexname * term option) list
- val dddot: indexname
+ val dddot_name: string
+ val dddot_indexname: indexname
+ val dddot_vname: string
val facts: Proof.context -> term list -> (indexname * term option) list
val no_facts: indexname list
end;
@@ -43,11 +45,9 @@
(* dddot *)
-val dddot = ("dddot", 0);
-
-val _ =
- Theory.setup (Sign.parse_translation
- [("_DDDOT", fn _ => fn ts => Term.list_comb (Syntax.var dddot, ts))]);
+val dddot_name = "dddot";
+val dddot_indexname = (dddot_name, 0);
+val dddot_vname = Term.string_of_vname dddot_indexname;
(* facts *)
@@ -60,8 +60,8 @@
fun facts ctxt props =
(case try List.last props of
NONE => []
- | SOME prop => [(dddot, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
+ | SOME prop => [(dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
-val no_facts = [dddot, (thisN, 0)];
+val no_facts = [dddot_indexname, (thisN, 0)];
end;
--- a/src/Pure/Syntax/syntax_phases.ML Mon Oct 28 18:48:14 2024 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Oct 28 18:48:28 2024 +0100
@@ -202,6 +202,8 @@
|>> dest_Type_name;
val _ = append_reports rs;
in [Ast.Constant (Lexicon.mark_type c)] end
+ | asts_of (Parser.Node ({const = "_DDDOT", ...}, [Parser.Tip tok])) =
+ [Ast.constrain (Ast.Variable Auto_Bind.dddot_vname) (ast_of_position tok)]
| asts_of (Parser.Node ({const = "_position", ...}, [Parser.Tip tok])) =
asts_of_position "_constrain" tok
| asts_of (Parser.Node ({const = "_position_sort", ...}, [Parser.Tip tok])) =
@@ -662,7 +664,7 @@
else Syntax.const "_free" $ t
end
| mark (t as Var (xi, T)) =
- if xi = Auto_Bind.dddot then Const ("_DDDOT", T)
+ if xi = Auto_Bind.dddot_indexname then Const ("_DDDOT", T)
else Syntax.const "_var" $ t
| mark a = a;
in mark tm end;