Quelle  Special_Nits.thy

(*  Title:      HOL/Nitpick_Examples/Special_Nits.thy
  Author: Jasmin Blanchette, TU Muenchen
  Copyright 2009-2011
 
 Examples featuring Nitpick's "specialize" optimization.
*)

section ‹Examples Featuring Nitpick's \textit{specialize} Optimization›

theory Special_Nits
imports Main
begin

nitpick_params [verbose, card = 4, sat_solver = MiniSat, max_threads = 1,
                timeout = 240]

fun f1 :: "nat ==> nat ==> nat ==> nat ==> nat ==> nat" where
"f1 a b c d e = a + b + c + d + e"

lemma "f1 0 0 0 0 0 = f1 0 0 0 0 (1 - 1)"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

lemma "f1 u v w x y = f1 y x w v u"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

fun f2 :: "nat ==> nat ==> nat ==> nat ==> nat ==> nat" where
"f2 a b c d (Suc e) = a + b + c + d + e"

lemma "f2 0 0 0 0 0 = f2 (1 - 1) 0 0 0 0"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

lemma "f2 0 (v - v) 0 (x - x) 0 = f2 (u - u) 0 (w - w) 0 (y - y)"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

lemma "f2 1 0 0 0 0 = f2 0 1 0 0 0"
nitpick [expect = genuine]
nitpick [dont_specialize, expect = genuine]
oops

lemma "f2 0 0 0 0 0 = f2 0 0 0 0 0"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

fun f3 :: "nat ==> nat ==> nat ==> nat ==> nat ==> nat" where
"f3 (Suc a) b 0 d (Suc e) = a + b + d + e" |
"f3 0 b 0 d 0 = b + d"

lemma "f3 a b c d e = f3 e d c b a"
nitpick [expect = genuine]
nitpick [dont_specialize, expect = genuine]
oops

lemma "f3 a b c d a = f3 a d c d a"
nitpick [expect = genuine]
nitpick [dont_specialize, expect = genuine]
oops

lemma "[c < 1; a ≥ e; e ≥ a] ==> f3 a b c d a = f3 e d c b e"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

lemma "(∀u. a = u ⟶ f3 a a a a a = f3 u u u u u)
       ∧ (∀u. b = u ⟶ f3 b b u b b = f3 u u b u u)"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

function f4 :: "nat ==> nat ==> nat" where
"f4 x x = 1" |
"f4 y z = (if y = z then 1 else 0)"
by auto
termination by lexicographic_order

lemma "f4 a b = f4 b a"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

lemma "f4 a (Suc a) = f4 a a"
nitpick [expect = genuine]
nitpick [dont_specialize, expect = genuine]
oops

fun f5 :: "(nat ==> nat) ==> nat ==> nat" where
"f5 f (Suc a) = f a"

lemma "∃one ∈ {1}. ∃two ∈ {2}.
       f5 (λa. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

lemma "∃two ∈ {2}. ∃one ∈ {1}.
       f5 (λa. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

lemma "∃one ∈ {1}. ∃two ∈ {2}.
       f5 (λa. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
nitpick [expect = genuine]
oops

lemma "∃two ∈ {2}. ∃one ∈ {1}.
       f5 (λa. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
nitpick [expect = genuine]
oops

lemma "∀a. g a = a
       ==> ∃one ∈ {1}. ∃two ∈ {2}. f5 g x =
                      f5 (λa. if a = one then 1 else if a = two then 2 else a) x"
nitpick [expect = none]
nitpick [dont_specialize, expect = none]
sorry

lemma "∀a. g a = a
       ==> ∃one ∈ {2}. ∃two ∈ {1}. f5 g x =
                      f5 (λa. if a = one then 1 else if a = two then 2 else a) x"
nitpick [expect = potential]
nitpick [dont_specialize, expect = potential]
sorry

lemma "∀a. g a = a
       ==> ∃b🪙1 b🪙2 b🪙3 b🪙4 b🪙5 b🪙6 b🪙7 b🪙8 b🪙9 b🪙10 (b🪙11::nat).
           b🪙1 < b🪙11 ∧ f5 g x = f5 (λa. if b🪙1 < b🪙11 then a else h b🪙2) x"
nitpick [expect = potential]
nitpick [dont_specialize, expect = none]
nitpick [dont_box, expect = none]
nitpick [dont_box, dont_specialize, expect = none]
sorry

lemma "∀a. g a = a
       ==> ∃b🪙1 b🪙2 b🪙3 b🪙4 b🪙5 b🪙6 b🪙7 b🪙8 b🪙9 b🪙10 (b🪙11::nat).
           b🪙1 < b🪙11
           ∧ f5 g x = f5 (λa. if b🪙1 < b🪙11 then
                                a
                              else
                                h b🪙2 + h b🪙3 + h b🪙4 + h b🪙5 + h b🪙6 + h b🪙7 + h b🪙8
                                + h b🪙9 + h b🪙10) x"
nitpick [card nat = 2, card 'a = 1, expect = none]
nitpick [card nat = 2, card 'a = 1, dont_box, expect = none]
nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = none]
nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize, expect = none]
sorry

lemma "∀a. g a = a
       ==> ∃b🪙1 b🪙2 b🪙3 b🪙4 b🪙5 b🪙6 b🪙7 b🪙8 b🪙9 b🪙10 (b🪙11::nat).
           b🪙1 < b🪙11
           ∧ f5 g x = f5 (λa. if b🪙1 ≥ b🪙11 then
                                a
                              else
                                h b🪙2 + h b🪙3 + h b🪙4 + h b🪙5 + h b🪙6 + h b🪙7 + h b🪙8
                                + h b🪙9 + h b🪙10) x"
nitpick [card nat = 2, card 'a = 1, expect = potential]
nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential]
nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential]
nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize,
         expect = potential]
oops

end