--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy Sat Jan 05 17:24:33 2019 +0100
@@ -12,7 +12,7 @@
text \<open>
Function \<open>joinL\<close> joins two trees (and an element).
-Precondition: @{prop "bheight l \<le> bheight r"}.
+Precondition: \<^prop>\<open>bheight l \<le> bheight r\<close>.
Method:
Descend along the left spine of \<open>r\<close>
until you find a subtree with the same \<open>bheight\<close> as \<open>l\<close>,
@@ -44,29 +44,29 @@
declare joinR.simps[simp del]
text \<open>
-One would expect @{const joinR} to be be completely dual to @{const joinL}.
-Thus the condition should be @{prop"bheight l = bheight r"}. What we have done
-is totalize the function. On the intended domain (@{prop "bheight l \<ge> bheight r"})
+One would expect \<^const>\<open>joinR\<close> to be be completely dual to \<^const>\<open>joinL\<close>.
+Thus the condition should be \<^prop>\<open>bheight l = bheight r\<close>. What we have done
+is totalize the function. On the intended domain (\<^prop>\<open>bheight l \<ge> bheight r\<close>)
the two versions behave exactly the same, including complexity. Thus from a programmer's
perspective they are equivalent. However, not from a verifier's perspective:
-the total version of @{const joinR} is easier
+the total version of \<^const>\<open>joinR\<close> is easier
to reason about because lemmas about it may not require preconditions. In particular
-@{prop"set_tree (joinR l x r) = set_tree l \<union> {x} \<union> set_tree r"}
+\<^prop>\<open>set_tree (joinR l x r) = set_tree l \<union> {x} \<union> set_tree r\<close>
is provable outright and hence also
-@{prop"set_tree (join l x r) = set_tree l \<union> {x} \<union> set_tree r"}.
-This is necessary because locale @{locale Set2_Join} unconditionally assumes
+\<^prop>\<open>set_tree (join l x r) = set_tree l \<union> {x} \<union> set_tree r\<close>.
+This is necessary because locale \<^locale>\<open>Set2_Join\<close> unconditionally assumes
exactly that. Adding preconditions to this assumptions significantly complicates
-the proofs within @{locale Set2_Join}, which we want to avoid.
+the proofs within \<^locale>\<open>Set2_Join\<close>, which we want to avoid.
-Why not work with the partial version of @{const joinR} and add the precondition
-@{prop "bheight l \<ge> bheight r"} to lemmas about @{const joinR}? After all, that is how
-we worked with @{const joinL}, and @{const join} ensures that @{const joinL} and @{const joinR}
-are only called under the respective precondition. But function @{const bheight}
-makes the difference: it descends along the left spine, just like @{const joinL}.
-Function @{const joinR}, however, descends along the right spine and thus @{const bheight}
-may change all the time. Thus we would need the further precondition @{prop "invh l"}.
+Why not work with the partial version of \<^const>\<open>joinR\<close> and add the precondition
+\<^prop>\<open>bheight l \<ge> bheight r\<close> to lemmas about \<^const>\<open>joinR\<close>? After all, that is how
+we worked with \<^const>\<open>joinL\<close>, and \<^const>\<open>join\<close> ensures that \<^const>\<open>joinL\<close> and \<^const>\<open>joinR\<close>
+are only called under the respective precondition. But function \<^const>\<open>bheight\<close>
+makes the difference: it descends along the left spine, just like \<^const>\<open>joinL\<close>.
+Function \<^const>\<open>joinR\<close>, however, descends along the right spine and thus \<^const>\<open>bheight\<close>
+may change all the time. Thus we would need the further precondition \<^prop>\<open>invh l\<close>.
This is what we really wanted to avoid in order to satisfy the unconditional assumption
-in @{locale Set2_Join}.
+in \<^locale>\<open>Set2_Join\<close>.
\<close>
subsection "Properties"
@@ -142,7 +142,7 @@
subsubsection "Inorder properties"
-text "Currently unused. Instead @{const set_tree} and @{const bst} properties are proved directly."
+text "Currently unused. Instead \<^const>\<open>set_tree\<close> and \<^const>\<open>bst\<close> properties are proved directly."
lemma inorder_joinL: "bheight l \<le> bheight r \<Longrightarrow> inorder(joinL l x r) = inorder l @ x # inorder r"
proof(induction l x r rule: joinL.induct)
@@ -231,7 +231,7 @@
by(auto simp: bst_paint bst_joinL bst_joinR)
-subsubsection "Interpretation of @{locale Set2_Join} with Red-Black Tree"
+subsubsection "Interpretation of \<^locale>\<open>Set2_Join\<close> with Red-Black Tree"
global_interpretation RBT: Set2_Join
where join = join and inv = "\<lambda>t. invc t \<and> invh t"