src/HOL/Quickcheck_Examples/Completeness.thy

 (*  Title:      HOL/Quickcheck_Examples/Completeness.thy
     Author:     Lukas Bulwahn
     Copyright   2012 TU Muenchen
 *)
 
-section {* Proving completeness of exhaustive generators *}
+section \<open>Proving completeness of exhaustive generators\<close>
 
 theory Completeness
 imports Main
 begin
 
-subsection {* Preliminaries *}
+subsection \<open>Preliminaries\<close>
 
 primrec is_some
 where
   "is_some (Some t) = True"
 | "is_some None = False"

   "is_some x \<longleftrightarrow> x \<noteq> None"
   by (cases x) simp_all
 
 setup Exhaustive_Generators.setup_exhaustive_datatype_interpretation
 
-subsection {* Defining the size of values *}
+subsection \<open>Defining the size of values\<close>
 
 hide_const size
 
 class size =
   fixes size :: "'a => nat"

 
 instance ..
 
 end
 
-subsection {* Completeness *}
+subsection \<open>Completeness\<close>
 
 class complete = exhaustive + size +
 assumes
    complete: "(\<exists> v. size v \<le> n \<and> is_some (f v)) \<longleftrightarrow> is_some (exhaustive_class.exhaustive f (natural_of_nat n))"
 

 lemma complete_imp2:
   assumes "is_some (exhaustive_class.exhaustive f (natural_of_nat n))"
   obtains v where "size (v :: 'a :: complete) \<le> n" "is_some (f v)"
 using assms by (metis complete)
 
-subsubsection {* Instance Proofs *}
+subsubsection \<open>Instance Proofs\<close>
 
 declare exhaustive_int'.simps [simp del]
 
 lemma complete_exhaustive':
   "(\<exists> i. j <= i & i <= k & is_some (f i)) \<longleftrightarrow> is_some (Quickcheck_Exhaustive.exhaustive_int' f k j)"