src/HOL/Nitpick_Examples/Manual_Nits.thy

     Copyright   2009-2014
 
 Examples from the Nitpick manual.
 *)
 
-section {* Examples from the Nitpick Manual *}
+section \<open>Examples from the Nitpick Manual\<close>
 
 (* The "expect" arguments to Nitpick in this theory and the other example
    theories are there so that the example can also serve as a regression test
    suite. *)
 
 theory Manual_Nits
 imports Real "~~/src/HOL/Library/Quotient_Product"
 begin
 
-section {* 2. First Steps *}
+section \<open>2. First Steps\<close>
 
 nitpick_params [sat_solver = MiniSat_JNI, max_threads = 1, timeout = 240]
 
 
-subsection {* 2.1. Propositional Logic *}
+subsection \<open>2.1. Propositional Logic\<close>
 
 lemma "P \<longleftrightarrow> Q"
 nitpick [expect = genuine]
 apply auto
 nitpick [expect = genuine] 1
 nitpick [expect = genuine] 2
 oops
 
 
-subsection {* 2.2. Type Variables *}
+subsection \<open>2.2. Type Variables\<close>
 
 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [verbose, expect = genuine]
 oops
 
 
-subsection {* 2.3. Constants *}
+subsection \<open>2.3. Constants\<close>
 
 lemma "x \<in> A \<Longrightarrow> (THE y. y \<in> A) \<in> A"
 nitpick [show_consts, expect = genuine]
 nitpick [dont_specialize, show_consts, expect = genuine]
 oops

 nitpick [card 'a = 1-50, expect = none]
 (* sledgehammer *)
 by (metis the_equality)
 
 
-subsection {* 2.4. Skolemization *}
+subsection \<open>2.4. Skolemization\<close>
 
 lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
 nitpick [expect = genuine]
 oops
 

 lemma "refl r \<Longrightarrow> sym r"
 nitpick [expect = genuine]
 oops
 
 
-subsection {* 2.5. Natural Numbers and Integers *}
+subsection \<open>2.5. Natural Numbers and Integers\<close>
 
 lemma "\<lbrakk>i \<le> j; n \<le> (m::int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
 nitpick [expect = genuine]
 nitpick [binary_ints, bits = 16, expect = genuine]
 oops

 nitpick [card nat = 1, expect = genuine]
 nitpick [card nat = 2, expect = none]
 oops
 
 
-subsection {* 2.6. Inductive Datatypes *}
+subsection \<open>2.6. Inductive Datatypes\<close>
 
 lemma "hd (xs @ [y, y]) = hd xs"
 nitpick [expect = genuine]
 nitpick [show_consts, show_types, expect = genuine]
 oops

 lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
 nitpick [show_types, expect = genuine]
 oops
 
 
-subsection {* 2.7. Typedefs, Records, Rationals, and Reals *}
+subsection \<open>2.7. Typedefs, Records, Rationals, and Reals\<close>
 
 definition "three = {0::nat, 1, 2}"
 typedef three = three
   unfolding three_def by blast
 

 
 lemma "add x y = add x x"
 nitpick [show_types, expect = genuine]
 oops
 
-ML {*
+ML \<open>
 fun my_int_postproc _ _ _ T (Const _ $ (Const _ $ t1 $ t2)) =
     HOLogic.mk_number T (snd (HOLogic.dest_number t1)
                          - snd (HOLogic.dest_number t2))
   | my_int_postproc _ _ _ _ t = t
-*}
-
-declaration {*
+\<close>
+
+declaration \<open>
 Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
-*}
+\<close>
 
 lemma "add x y = add x x"
 nitpick [show_types]
 oops
 

 lemma "4 * x + 3 * (y::real) \<noteq> 1 / 2"
 nitpick [show_types, expect = genuine]
 oops
 
 
-subsection {* 2.8. Inductive and Coinductive Predicates *}
+subsection \<open>2.8. Inductive and Coinductive Predicates\<close>
 
 inductive even where
 "even 0" |
 "even n \<Longrightarrow> even (Suc (Suc n))"
 

 lemma "odd n \<Longrightarrow> odd (n - 2)"
 nitpick [card nat = 4, show_consts, expect = genuine]
 oops
 
 
-subsection {* 2.9. Coinductive Datatypes *}
+subsection \<open>2.9. Coinductive Datatypes\<close>
 
 codatatype 'a llist = LNil | LCons 'a "'a llist"
 
 primcorec iterates where
 "iterates f a = LCons a (iterates f (f a))"

 nitpick [bisim_depth = -1, show_types, expect = quasi_genuine]
 nitpick [card = 1-5, expect = none]
 sorry
 
 
-subsection {* 2.10. Boxing *}
+subsection \<open>2.10. Boxing\<close>
 
 datatype tm = Var nat | Lam tm | App tm tm
 
 primrec lift where
 "lift (Var j) k = Var (if j < k then j else j + 1)" |

 lemma "\<not> loose t 0 \<Longrightarrow> subst\<^sub>2 \<sigma> t = t"
 nitpick [card = 1-5, expect = none]
 sorry
 
 
-subsection {* 2.11. Scope Monotonicity *}
+subsection \<open>2.11. Scope Monotonicity\<close>
 
 lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
 nitpick [verbose, expect = genuine]
 oops
 

 nitpick [mono, expect = none]
 nitpick [expect = genuine]
 oops
 
 
-subsection {* 2.12. Inductive Properties *}
+subsection \<open>2.12. Inductive Properties\<close>
 
 inductive_set reach where
 "(4::nat) \<in> reach" |
 "n \<in> reach \<Longrightarrow> n < 4 \<Longrightarrow> 3 * n + 1 \<in> reach" |
 "n \<in> reach \<Longrightarrow> n + 2 \<in> reach"

 
 lemma "n \<in> reach \<Longrightarrow> 2 dvd n \<and> n \<ge> 4"
 by (induct set: reach) arith+
 
 
-section {* 3. Case Studies *}
+section \<open>3. Case Studies\<close>
 
 nitpick_params [max_potential = 0]
 
 
-subsection {* 3.1. A Context-Free Grammar *}
+subsection \<open>3.1. A Context-Free Grammar\<close>
 
 datatype alphabet = a | b
 
 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
   "[] \<in> S\<^sub>1"

 "w \<in> B\<^sub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
 nitpick [card = 1-5, expect = none]
 sorry
 
 
-subsection {* 3.2. AA Trees *}
+subsection \<open>3.2. AA Trees\<close>
 
 datatype 'a aa_tree = \<Lambda> | N "'a::linorder" nat "'a aa_tree" "'a aa_tree"
 
 primrec data where
 "data \<Lambda> = undefined" |