src/HOL/Statespace/DistinctTreeProver.thy

 (*  Title:      HOL/Statespace/DistinctTreeProver.thy
     Author:     Norbert Schirmer, TU Muenchen
 *)
 
-section {* Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}*}
+section \<open>Distinctness of Names in a Binary Tree \label{sec:DistinctTreeProver}\<close>
 
 theory DistinctTreeProver 
 imports Main
 begin
 
-text {* A state space manages a set of (abstract) names and assumes
+text \<open>A state space manages a set of (abstract) names and assumes
 that the names are distinct. The names are stored as parameters of a
 locale and distinctness as an assumption. The most common request is
 to proof distinctness of two given names. We maintain the names in a
 balanced binary tree and formulate a predicate that all nodes in the
 tree have distinct names. This setup leads to logarithmic certificates.
-*}
-
-subsection {* The Binary Tree *}
+\<close>
+
+subsection \<open>The Binary Tree\<close>
 
 datatype 'a tree = Node "'a tree" 'a bool "'a tree" | Tip
 
 
-text {* The boolean flag in the node marks the content of the node as
+text \<open>The boolean flag in the node marks the content of the node as
 deleted, without having to build a new tree. We prefer the boolean
 flag to an option type, so that the ML-layer can still use the node
 content to facilitate binary search in the tree. The ML code keeps the
 nodes sorted using the term order. We do not have to push ordering to
-the HOL level. *}
-
-subsection {* Distinctness of Nodes *}
+the HOL level.\<close>
+
+subsection \<open>Distinctness of Nodes\<close>
 
 
 primrec set_of :: "'a tree \<Rightarrow> 'a set"
 where
   "set_of Tip = {}"

 | "all_distinct (Node l x d r) =
     ((d \<or> (x \<notin> set_of l \<and> x \<notin> set_of r)) \<and> 
       set_of l \<inter> set_of r = {} \<and>
       all_distinct l \<and> all_distinct r)"
 
-text {* Given a binary tree @{term "t"} for which 
+text \<open>Given a binary tree @{term "t"} for which 
 @{const all_distinct} holds, given two different nodes contained in the tree,
 we want to write a ML function that generates a logarithmic
 certificate that the content of the nodes is distinct. We use the
-following lemmas to achieve this.  *} 
+following lemmas to achieve this.\<close> 
 
 lemma all_distinct_left: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct l"
   by simp
 
 lemma all_distinct_right: "all_distinct (Node l x b r) \<Longrightarrow> all_distinct r"

   by blast
 
 lemma neq_to_eq_False: "x\<noteq>y \<Longrightarrow> (x=y)\<equiv>False"
   by simp
 
-subsection {* Containment of Trees *}
-
-text {* When deriving a state space from other ones, we create a new
+subsection \<open>Containment of Trees\<close>
+
+text \<open>When deriving a state space from other ones, we create a new
 name tree which contains all the names of the parent state spaces and
 assume the predicate @{const all_distinct}. We then prove that the new
 locale interprets all parent locales. Hence we have to show that the
 new distinctness assumption on all names implies the distinctness
 assumptions of the parent locales. This proof is implemented in ML. We

 by ``subtraction''.  We subtract the parent tree from the new tree. If
 this succeeds we know that @{const all_distinct} of the new tree
 implies @{const all_distinct} of the parent tree.  The resulting
 certificate is of the order @{term "n * log(m)"} where @{term "n"} is
 the size of the (smaller) parent tree and @{term "m"} the size of the
-(bigger) new tree.  *}
+(bigger) new tree.\<close>
 
 
 primrec delete :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree option"
 where
   "delete x Tip = None"

 by simp
 
 lemma subtract_Tip: "subtract Tip t = Some t"
   by simp
  
-text {* Now we have all the theorems in place that are needed for the
-certificate generating ML functions. *}
+text \<open>Now we have all the theorems in place that are needed for the
+certificate generating ML functions.\<close>
 
 ML_file "distinct_tree_prover.ML"
 
 end