src/HOL/Library/ExecutableSet.thy

 
 theory ExecutableSet
 imports Main
 begin
 
-section {* Definitional rewrites *}
+subsection {* Definitional rewrites *}
 
 instance set :: (eq) eq ..
 
 lemma [code target: Set]:
   "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"

   "filter_set P xs = {x\<in>xs. P x}"
 
 lemmas [symmetric, code inline] = filter_set_def
 
 
-section {* Operations on lists *}
-
-subsection {* Basic definitions *}
+subsection {* Operations on lists *}
+
+subsubsection {* Basic definitions *}
 
 definition
   flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
   "flip f a b = f b a"
 

 lemma foldr_remove1_empty [simp]:
   "foldr remove1 xs [] = []"
   by (induct xs) simp_all
 
 
-subsection {* Derived definitions *}
+subsubsection {* Derived definitions *}
 
 function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "unionl [] ys = ys"
 | "unionl xs ys = foldr insertl xs ys"

 definition
   map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   "map_inter xs f = intersects (map f xs)"
 
 
-section {* Isomorphism proofs *}
+subsection {* Isomorphism proofs *}
 
 lemma iso_member:
   "member xs x \<longleftrightarrow> x \<in> set xs"
   unfolding member_def mem_iff ..
 

 
 lemma iso_filter:
   "set (filter P xs) = filter_set P (set xs)"
   unfolding filter_set_def by (induct xs) auto
 
-section {* code generator setup *}
+subsection {* code generator setup *}
 
 ML {*
 nonfix inter;
 nonfix union;
 nonfix subset;

   Ball \<equiv> Blall
   Bex \<equiv> Blex
   filter_set \<equiv> filter
 
 
-subsection {* type serializations *}
+subsubsection {* type serializations *}
 
 types_code
   set ("_ list")
 attach (term_of) {*
 fun term_of_set f T [] = Const ("{}", Type ("set", [T]))

   [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] ()
 and gen_set aG i = gen_set' aG i i;
 *}
 
 
-subsection {* const serializations *}
+subsubsection {* const serializations *}
 
 consts_code
   "{}"      ("[]")
   "insert"  ("{*insertl*}")
   "op Un"   ("{*unionl*}")