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.7 -section {* Implementation of sets using RBT trees *}
1.8 +section \<open>Implementation of sets using RBT trees\<close>
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.16 -section {* Definition of code datatype constructors *}
1.17 +section \<open>Definition of code datatype constructors\<close>
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.25 -section {* Deletion of already existing code equations *}
1.26 +section \<open>Deletion of already existing code equations\<close>
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.34 -section {* Lemmas *}
1.35 +section \<open>Lemmas\<close>
1.38 -subsection {* Auxiliary lemmas *}
1.39 +subsection \<open>Auxiliary lemmas\<close>
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.47 -subsection {* fold and filter *}
1.48 +subsection \<open>fold and filter\<close>
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.56 -subsection {* foldi and Ball *}
1.57 +subsection \<open>foldi and Ball\<close>
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.65 -subsection {* foldi and Bex *}
1.66 +subsection \<open>foldi and Bex\<close>
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.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.77  (** concrete **)
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.90  end
1.92 -section {* Code equations *}
1.93 +section \<open>Code equations\<close>
1.95  code_datatype Set Coset
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.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.115 @@ -648,7 +648,7 @@
1.116      by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split)
1.117  qed
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)