src/HOL/Library/RBT_Set.thy
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 60580 7e741e22d7fc
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Wed Jun 17 10:57:11 2015 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Wed Jun 17 11:03:05 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Ondrej Kuncar
     1.5  *)
     1.6  
     1.7 -section {* Implementation of sets using RBT trees *}
     1.8 +section \<open>Implementation of sets using RBT trees\<close>
     1.9  
    1.10  theory RBT_Set
    1.11  imports RBT Product_Lexorder
    1.12 @@ -16,7 +16,7 @@
    1.13    own equations using RBT trees. 
    1.14  *)
    1.15  
    1.16 -section {* Definition of code datatype constructors *}
    1.17 +section \<open>Definition of code datatype constructors\<close>
    1.18  
    1.19  definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
    1.20    where "Set t = {x . RBT.lookup t x = Some ()}"
    1.21 @@ -25,7 +25,7 @@
    1.22    where [simp]: "Coset t = - Set t"
    1.23  
    1.24  
    1.25 -section {* Deletion of already existing code equations *}
    1.26 +section \<open>Deletion of already existing code equations\<close>
    1.27  
    1.28  lemma [code, code del]:
    1.29    "Set.empty = Set.empty" ..
    1.30 @@ -141,10 +141,10 @@
    1.31  lemma [code, code del]: 
    1.32    "List.Bleast = List.Bleast" ..
    1.33  
    1.34 -section {* Lemmas *}
    1.35 +section \<open>Lemmas\<close>
    1.36  
    1.37  
    1.38 -subsection {* Auxiliary lemmas *}
    1.39 +subsection \<open>Auxiliary lemmas\<close>
    1.40  
    1.41  lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
    1.42  by (auto simp: not_Some_eq[THEN iffD1])
    1.43 @@ -158,7 +158,7 @@
    1.44  lemma set_keys: "Set t = set(RBT.keys t)"
    1.45  by (simp add: Set_set_keys lookup_keys)
    1.46  
    1.47 -subsection {* fold and filter *}
    1.48 +subsection \<open>fold and filter\<close>
    1.49  
    1.50  lemma finite_fold_rbt_fold_eq:
    1.51    assumes "comp_fun_commute f" 
    1.52 @@ -198,7 +198,7 @@
    1.53    finite_fold_fold_keys[OF comp_fun_commute_filter_fold])
    1.54  
    1.55  
    1.56 -subsection {* foldi and Ball *}
    1.57 +subsection \<open>foldi and Ball\<close>
    1.58  
    1.59  lemma Ball_False: "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t False = False"
    1.60  by (induction t) auto
    1.61 @@ -214,7 +214,7 @@
    1.62  unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_conj)
    1.63  
    1.64  
    1.65 -subsection {* foldi and Bex *}
    1.66 +subsection \<open>foldi and Bex\<close>
    1.67  
    1.68  lemma Bex_True: "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t True = True"
    1.69  by (induction t) auto
    1.70 @@ -230,7 +230,7 @@
    1.71  unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_disj)
    1.72  
    1.73  
    1.74 -subsection {* folding over non empty trees and selecting the minimal and maximal element *}
    1.75 +subsection \<open>folding over non empty trees and selecting the minimal and maximal element\<close>
    1.76  
    1.77  (** concrete **)
    1.78  
    1.79 @@ -438,7 +438,7 @@
    1.80    assumes "\<not> RBT.is_empty t"
    1.81    shows "semilattice_set.F f (Set t) = fold1_keys f t"
    1.82  proof -
    1.83 -  from `semilattice f` interpret semilattice_set f by (rule semilattice_set.intro)
    1.84 +  from \<open>semilattice f\<close> interpret semilattice_set f by (rule semilattice_set.intro)
    1.85    show ?thesis using assms 
    1.86      by (auto simp: fold1_keys_def_alt set_keys fold_def_alt non_empty_keys set_eq_fold [symmetric])
    1.87  qed
    1.88 @@ -521,7 +521,7 @@
    1.89  
    1.90  end
    1.91  
    1.92 -section {* Code equations *}
    1.93 +section \<open>Code equations\<close>
    1.94  
    1.95  code_datatype Set Coset
    1.96  
    1.97 @@ -564,7 +564,7 @@
    1.98  proof -
    1.99    interpret comp_fun_idem Set.insert
   1.100      by (fact comp_fun_idem_insert)
   1.101 -  from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`]
   1.102 +  from finite_fold_fold_keys[OF \<open>comp_fun_commute Set.insert\<close>]
   1.103    show ?thesis by (auto simp add: union_fold_insert)
   1.104  qed
   1.105  
   1.106 @@ -577,7 +577,7 @@
   1.107  proof -
   1.108    interpret comp_fun_idem Set.remove
   1.109      by (fact comp_fun_idem_remove)
   1.110 -  from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`]
   1.111 +  from finite_fold_fold_keys[OF \<open>comp_fun_commute Set.remove\<close>]
   1.112    show ?thesis by (auto simp add: minus_fold_remove)
   1.113  qed
   1.114  
   1.115 @@ -648,7 +648,7 @@
   1.116      by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
   1.117  qed
   1.118  
   1.119 -text {* A frequent case -- avoid intermediate sets *}
   1.120 +text \<open>A frequent case -- avoid intermediate sets\<close>
   1.121  lemma [code_unfold]:
   1.122    "Set t1 \<subseteq> Set t2 \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
   1.123  by (simp add: subset_code Ball_Set)