src/HOL/Nitpick_Examples/Special_Nits.thy
 author wenzelm Tue Sep 03 01:12:40 2013 +0200 (2013-09-03) changeset 53374 a14d2a854c02 parent 53015 a1119cf551e8 child 54633 86e0b402994c permissions -rw-r--r--
tuned proofs -- clarified flow of facts wrt. calculation;
     1 (*  Title:      HOL/Nitpick_Examples/Special_Nits.thy

     2     Author:     Jasmin Blanchette, TU Muenchen

     3     Copyright   2009-2011

     4

     5 Examples featuring Nitpick's "specialize" optimization.

     6 *)

     7

     8 header {* Examples Featuring Nitpick's \textit{specialize} Optimization *}

     9

    10 theory Special_Nits

    11 imports Main

    12 begin

    13

    14 nitpick_params [verbose, card = 4, sat_solver = MiniSat_JNI, max_threads = 1,

    15                 timeout = 240]

    16

    17 fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where

    18 "f1 a b c d e = a + b + c + d + e"

    19

    20 lemma "f1 0 0 0 0 0 = f1 0 0 0 0 (1 - 1)"

    21 nitpick [expect = none]

    22 nitpick [dont_specialize, expect = none]

    23 sorry

    24

    25 lemma "f1 u v w x y = f1 y x w v u"

    26 nitpick [expect = none]

    27 nitpick [dont_specialize, expect = none]

    28 sorry

    29

    30 fun f2 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where

    31 "f2 a b c d (Suc e) = a + b + c + d + e"

    32

    33 lemma "f2 0 0 0 0 0 = f2 (1 - 1) 0 0 0 0"

    34 nitpick [expect = none]

    35 nitpick [dont_specialize, expect = none]

    36 sorry

    37

    38 lemma "f2 0 (v - v) 0 (x - x) 0 = f2 (u - u) 0 (w - w) 0 (y - y)"

    39 nitpick [expect = none]

    40 nitpick [dont_specialize, expect = none]

    41 sorry

    42

    43 lemma "f2 1 0 0 0 0 = f2 0 1 0 0 0"

    44 nitpick [expect = genuine]

    45 nitpick [dont_specialize, expect = genuine]

    46 oops

    47

    48 lemma "f2 0 0 0 0 0 = f2 0 0 0 0 0"

    49 nitpick [expect = none]

    50 nitpick [dont_specialize, expect = none]

    51 sorry

    52

    53 fun f3 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where

    54 "f3 (Suc a) b 0 d (Suc e) = a + b + d + e" |

    55 "f3 0 b 0 d 0 = b + d"

    56

    57 lemma "f3 a b c d e = f3 e d c b a"

    58 nitpick [expect = genuine]

    59 nitpick [dont_specialize, expect = genuine]

    60 oops

    61

    62 lemma "f3 a b c d a = f3 a d c d a"

    63 nitpick [expect = genuine]

    64 nitpick [dont_specialize, expect = genuine]

    65 oops

    66

    67 lemma "\<lbrakk>c < 1; a \<ge> e; e \<ge> a\<rbrakk> \<Longrightarrow> f3 a b c d a = f3 e d c b e"

    68 nitpick [expect = none]

    69 nitpick [dont_specialize, expect = none]

    70 sorry

    71

    72 lemma "(\<forall>u. a = u \<longrightarrow> f3 a a a a a = f3 u u u u u)

    73        \<and> (\<forall>u. b = u \<longrightarrow> f3 b b u b b = f3 u u b u u)"

    74 nitpick [expect = none]

    75 nitpick [dont_specialize, expect = none]

    76 sorry

    77

    78 function f4 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where

    79 "f4 x x = 1" |

    80 "f4 y z = (if y = z then 1 else 0)"

    81 by auto

    82 termination by lexicographic_order

    83

    84 lemma "f4 a b = f4 b a"

    85 nitpick [expect = none]

    86 nitpick [dont_specialize, expect = none]

    87 sorry

    88

    89 lemma "f4 a (Suc a) = f4 a a"

    90 nitpick [expect = genuine]

    91 nitpick [dont_specialize, expect = genuine]

    92 oops

    93

    94 fun f5 :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where

    95 "f5 f (Suc a) = f a"

    96

    97 lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.

    98        f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"

    99 nitpick [expect = none]

   100 nitpick [dont_specialize, expect = none]

   101 sorry

   102

   103 lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.

   104        f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"

   105 nitpick [expect = none]

   106 nitpick [dont_specialize, expect = none]

   107 sorry

   108

   109 lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.

   110        f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"

   111 nitpick [expect = genuine]

   112 oops

   113

   114 lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.

   115        f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"

   116 nitpick [expect = genuine]

   117 oops

   118

   119 lemma "\<forall>a. g a = a

   120        \<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x =

   121                       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"

   122 nitpick [expect = none]

   123 nitpick [dont_specialize, expect = none]

   124 sorry

   125

   126 lemma "\<forall>a. g a = a

   127        \<Longrightarrow> \<exists>one \<in> {2}. \<exists>two \<in> {1}. f5 g x =

   128                       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"

   129 nitpick [expect = potential]

   130 nitpick [dont_specialize, expect = potential]

   131 sorry

   132

   133 lemma "\<forall>a. g a = a

   134        \<Longrightarrow> \<exists>b\<^sub>1 b\<^sub>2 b\<^sub>3 b\<^sub>4 b\<^sub>5 b\<^sub>6 b\<^sub>7 b\<^sub>8 b\<^sub>9 b\<^sub>10 (b\<^sub>11\<Colon>nat).

   135            b\<^sub>1 < b\<^sub>11 \<and> f5 g x = f5 (\<lambda>a. if b\<^sub>1 < b\<^sub>11 then a else h b\<^sub>2) x"

   136 nitpick [expect = potential]

   137 nitpick [dont_specialize, expect = none]

   138 nitpick [dont_box, expect = none]

   139 nitpick [dont_box, dont_specialize, expect = none]

   140 sorry

   141

   142 lemma "\<forall>a. g a = a

   143        \<Longrightarrow> \<exists>b\<^sub>1 b\<^sub>2 b\<^sub>3 b\<^sub>4 b\<^sub>5 b\<^sub>6 b\<^sub>7 b\<^sub>8 b\<^sub>9 b\<^sub>10 (b\<^sub>11\<Colon>nat).

   144            b\<^sub>1 < b\<^sub>11

   145            \<and> f5 g x = f5 (\<lambda>a. if b\<^sub>1 < b\<^sub>11 then

   146                                 a

   147                               else

   148                                 h b\<^sub>2 + h b\<^sub>3 + h b\<^sub>4 + h b\<^sub>5 + h b\<^sub>6 + h b\<^sub>7 + h b\<^sub>8

   149                                 + h b\<^sub>9 + h b\<^sub>10) x"

   150 nitpick [card nat = 2, card 'a = 1, expect = none]

   151 nitpick [card nat = 2, card 'a = 1, dont_box, expect = none]

   152 nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = none]

   153 nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize, expect = none]

   154 sorry

   155

   156 lemma "\<forall>a. g a = a

   157        \<Longrightarrow> \<exists>b\<^sub>1 b\<^sub>2 b\<^sub>3 b\<^sub>4 b\<^sub>5 b\<^sub>6 b\<^sub>7 b\<^sub>8 b\<^sub>9 b\<^sub>10 (b\<^sub>11\<Colon>nat).

   158            b\<^sub>1 < b\<^sub>11

   159            \<and> f5 g x = f5 (\<lambda>a. if b\<^sub>1 \<ge> b\<^sub>11 then

   160                                 a

   161                               else

   162                                 h b\<^sub>2 + h b\<^sub>3 + h b\<^sub>4 + h b\<^sub>5 + h b\<^sub>6 + h b\<^sub>7 + h b\<^sub>8

   163                                 + h b\<^sub>9 + h b\<^sub>10) x"

   164 nitpick [card nat = 2, card 'a = 1, expect = potential]

   165 nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential]

   166 nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential]

   167 nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize,

   168          expect = potential]

   169 oops

   170

   171 end