continuation of Nitpick's integration into Isabelle;
authorblanchet
Fri Oct 23 18:59:24 2009 +0200 (2009-10-23)
changeset 33197de6285ebcc05
parent 33196 5fe67e108651
child 33198 bfb9a790d1e7
continuation of Nitpick's integration into Isabelle;
added examples, and integrated non-Main theories better.
src/HOL/GCD.thy
src/HOL/Induct/LList.thy
src/HOL/IsaMakefile
src/HOL/Library/Coinductive_List.thy
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nitpick_Examples/Datatype_Nits.thy
src/HOL/Nitpick_Examples/Induct_Nits.thy
src/HOL/Nitpick_Examples/Manual_Nits.thy
src/HOL/Nitpick_Examples/Mini_Nits.thy
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/Nitpick_Examples/Nitpick_Examples.thy
src/HOL/Nitpick_Examples/Pattern_Nits.thy
src/HOL/Nitpick_Examples/ROOT.ML
src/HOL/Nitpick_Examples/Record_Nits.thy
src/HOL/Nitpick_Examples/Refute_Nits.thy
src/HOL/Nitpick_Examples/Special_Nits.thy
src/HOL/Nitpick_Examples/Tests_Nits.thy
src/HOL/Nitpick_Examples/Typedef_Nits.thy
src/HOL/Rational.thy
src/HOL/RealDef.thy
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_isar.ML
     1.1 --- a/src/HOL/GCD.thy	Fri Oct 23 18:57:35 2009 +0200
     1.2 +++ b/src/HOL/GCD.thy	Fri Oct 23 18:59:24 2009 +0200
     1.3 @@ -1702,4 +1702,12 @@
     1.4    show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
     1.5  qed
     1.6  
     1.7 +lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
     1.8 +apply (rule eq_reflection)
     1.9 +apply (induct x y rule: nat_gcd.induct)
    1.10 +by (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
    1.11 +
    1.12 +lemma lcm_eq_nitpick_lcm [nitpick_def]: "lcm x y \<equiv> Nitpick.nat_lcm x y"
    1.13 +by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
    1.14 +
    1.15  end
     2.1 --- a/src/HOL/Induct/LList.thy	Fri Oct 23 18:57:35 2009 +0200
     2.2 +++ b/src/HOL/Induct/LList.thy	Fri Oct 23 18:59:24 2009 +0200
     2.3 @@ -905,4 +905,9 @@
     2.4  lemma lappend_assoc': "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
     2.5  by (rule_tac l = l1 in llist_fun_equalityI, auto)
     2.6  
     2.7 +setup {*
     2.8 +Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
     2.9 +                            (map dest_Const [@{term LNil}, @{term LCons}])
    2.10 +*}
    2.11 +
    2.12  end
     3.1 --- a/src/HOL/IsaMakefile	Fri Oct 23 18:57:35 2009 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Fri Oct 23 18:59:24 2009 +0200
     3.3 @@ -34,6 +34,7 @@
     3.4    HOL-Mirabelle \
     3.5    HOL-Modelcheck \
     3.6    HOL-NanoJava \
     3.7 +  HOL-Nitpick_Examples \
     3.8    HOL-Nominal-Examples \
     3.9    HOL-Number_Theory \
    3.10    HOL-Old_Number_Theory \
    3.11 @@ -43,9 +44,9 @@
    3.12    HOL-SMT-Examples \
    3.13    HOL-Statespace \
    3.14    HOL-Subst \
    3.15 -      TLA-Buffer \
    3.16 -      TLA-Inc \
    3.17 -      TLA-Memory \
    3.18 +  TLA-Buffer \
    3.19 +  TLA-Inc \
    3.20 +  TLA-Memory \
    3.21    HOL-UNITY \
    3.22    HOL-Unix \
    3.23    HOL-W0 \
    3.24 @@ -584,6 +585,21 @@
    3.25  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Metis_Examples
    3.26  
    3.27  
    3.28 +## HOL-Nitpick_Examples
    3.29 +
    3.30 +HOL-Nitpick_Examples: HOL $(LOG)/HOL-Nitpick_Examples.gz
    3.31 +
    3.32 +$(LOG)/HOL-Nitpick_Examples.gz: $(OUT)/HOL Nitpick_Examples/ROOT.ML \
    3.33 +  Nitpick_Examples/Core_Nits.thy Nitpick_Examples/Datatype_Nits.thy \
    3.34 +  Nitpick_Examples/Induct_Nits.thy Nitpick_Examples/Manual_Nits.thy \
    3.35 +  Nitpick_Examples/Mini_Nits.thy Nitpick_Examples/Mono_Nits.thy \
    3.36 +  Nitpick_Examples/Nitpick_Examples.thy Nitpick_Examples/Pattern_Nits.thy \
    3.37 +  Nitpick_Examples/Record_Nits.thy Nitpick_Examples/Refute_Nits.thy \
    3.38 +  Nitpick_Examples/Special_Nits.thy Nitpick_Examples/Tests_Nits.thy \
    3.39 +  Nitpick_Examples/Typedef_Nits.thy
    3.40 +	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Nitpick_Examples
    3.41 +
    3.42 +
    3.43  ## HOL-Algebra
    3.44  
    3.45  HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
     4.1 --- a/src/HOL/Library/Coinductive_List.thy	Fri Oct 23 18:57:35 2009 +0200
     4.2 +++ b/src/HOL/Library/Coinductive_List.thy	Fri Oct 23 18:59:24 2009 +0200
     4.3 @@ -200,6 +200,7 @@
     4.4    [code del]: "llist_case c d l =
     4.5      List_case c (\<lambda>x y. d (inv Datatype.Leaf x) (Abs_llist y)) (Rep_llist l)"
     4.6  
     4.7 +
     4.8  syntax  (* FIXME? *)
     4.9    LNil :: logic
    4.10    LCons :: logic
    4.11 @@ -848,4 +849,9 @@
    4.12    qed
    4.13  qed
    4.14  
    4.15 +setup {*
    4.16 +Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
    4.17 +                            (map dest_Const [@{term LNil}, @{term LCons}])
    4.18 +*}
    4.19 +
    4.20  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
     5.3 @@ -0,0 +1,1123 @@
     5.4 +(*  Title:      HOL/Nitpick_Examples/Core_Nits.thy
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Copyright   2009
     5.7 +
     5.8 +Examples featuring Nitpick's functional core.
     5.9 +*)
    5.10 +
    5.11 +header {* Examples Featuring Nitpick's Functional Core *}
    5.12 +
    5.13 +theory Core_Nits
    5.14 +imports Main
    5.15 +begin
    5.16 +
    5.17 +subsection {* Curry in a Hurry *}
    5.18 +
    5.19 +lemma "(\<lambda>f x y. (curry o split) f x y) = (\<lambda>f x y. (\<lambda>x. x) f x y)"
    5.20 +nitpick [card = 1\<midarrow>4, expect = none]
    5.21 +nitpick [card = 100, expect = none, timeout = none]
    5.22 +by auto
    5.23 +
    5.24 +lemma "(\<lambda>f p. (split o curry) f p) = (\<lambda>f p. (\<lambda>x. x) f p)"
    5.25 +nitpick [card = 2]
    5.26 +nitpick [card = 1\<midarrow>4, expect = none]
    5.27 +nitpick [card = 10, expect = none]
    5.28 +by auto
    5.29 +
    5.30 +lemma "split (curry f) = f"
    5.31 +nitpick [card = 1\<midarrow>4, expect = none]
    5.32 +nitpick [card = 10, expect = none]
    5.33 +nitpick [card = 40, expect = none]
    5.34 +by auto
    5.35 +
    5.36 +lemma "curry (split f) = f"
    5.37 +nitpick [card = 1\<midarrow>4, expect = none]
    5.38 +nitpick [card = 40, expect = none]
    5.39 +by auto
    5.40 +
    5.41 +lemma "(split o curry) f = f"
    5.42 +nitpick [card = 1\<midarrow>4, expect = none]
    5.43 +nitpick [card = 40, expect = none]
    5.44 +by auto
    5.45 +
    5.46 +lemma "(curry o split) f = f"
    5.47 +nitpick [card = 1\<midarrow>4, expect = none]
    5.48 +nitpick [card = 1000, expect = none]
    5.49 +by auto
    5.50 +
    5.51 +lemma "(split o curry) f = (\<lambda>x. x) f"
    5.52 +nitpick [card = 1\<midarrow>4, expect = none]
    5.53 +nitpick [card = 40, expect = none]
    5.54 +by auto
    5.55 +
    5.56 +lemma "(curry o split) f = (\<lambda>x. x) f"
    5.57 +nitpick [card = 1\<midarrow>4, expect = none]
    5.58 +nitpick [card = 40, expect = none]
    5.59 +by auto
    5.60 +
    5.61 +lemma "((split o curry) f) p = ((\<lambda>x. x) f) p"
    5.62 +nitpick [card = 1\<midarrow>4, expect = none]
    5.63 +nitpick [card = 40, expect = none]
    5.64 +by auto
    5.65 +
    5.66 +lemma "((curry o split) f) x = ((\<lambda>x. x) f) x"
    5.67 +nitpick [card = 1\<midarrow>4, expect = none]
    5.68 +nitpick [card = 1000, expect = none]
    5.69 +by auto
    5.70 +
    5.71 +lemma "((curry o split) f) x y = ((\<lambda>x. x) f) x y"
    5.72 +nitpick [card = 1\<midarrow>4, expect = none]
    5.73 +nitpick [card = 1000, expect = none]
    5.74 +by auto
    5.75 +
    5.76 +lemma "split o curry = (\<lambda>x. x)"
    5.77 +nitpick [card = 1\<midarrow>4, expect = none]
    5.78 +nitpick [card = 40, expect = none]
    5.79 +apply (rule ext)+
    5.80 +by auto
    5.81 +
    5.82 +lemma "curry o split = (\<lambda>x. x)"
    5.83 +nitpick [card = 1\<midarrow>4, expect = none]
    5.84 +nitpick [card = 100, expect = none]
    5.85 +apply (rule ext)+
    5.86 +by auto
    5.87 +
    5.88 +lemma "split (\<lambda>x y. f (x, y)) = f"
    5.89 +nitpick [card = 1\<midarrow>4, expect = none]
    5.90 +nitpick [card = 40, expect = none]
    5.91 +by auto
    5.92 +
    5.93 +subsection {* Representations *}
    5.94 +
    5.95 +lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"
    5.96 +nitpick [expect = none]
    5.97 +by auto
    5.98 +
    5.99 +lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
   5.100 +nitpick [card 'a = 35, card 'b = 34, expect = genuine]
   5.101 +nitpick [card = 1\<midarrow>15, mono, expect = none]
   5.102 +oops
   5.103 +
   5.104 +lemma "\<exists>f. f = (\<lambda>x. x) \<and> f y \<noteq> y"
   5.105 +nitpick [card = 1, expect = genuine]
   5.106 +nitpick [card = 2, expect = genuine]
   5.107 +nitpick [card = 5, expect = genuine]
   5.108 +oops
   5.109 +
   5.110 +lemma "P (\<lambda>x. x)"
   5.111 +nitpick [card = 1, expect = genuine]
   5.112 +nitpick [card = 5, expect = genuine]
   5.113 +oops
   5.114 +
   5.115 +lemma "{(a\<Colon>'a\<times>'a, b\<Colon>'b)}^-1 = {(b, a)}"
   5.116 +nitpick [card = 1\<midarrow>6, expect = none]
   5.117 +nitpick [card = 20, expect = none]
   5.118 +by auto
   5.119 +
   5.120 +lemma "fst (a, b) = a"
   5.121 +nitpick [card = 1\<midarrow>20, expect = none]
   5.122 +by auto
   5.123 +
   5.124 +lemma "\<exists>P. P = Id"
   5.125 +nitpick [card = 1\<midarrow>4, expect = none]
   5.126 +by auto
   5.127 +
   5.128 +lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
   5.129 +nitpick [card = 1\<midarrow>3, expect = none]
   5.130 +by auto
   5.131 +
   5.132 +lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
   5.133 +nitpick [card = 1\<midarrow>6, expect = none]
   5.134 +by auto
   5.135 +
   5.136 +lemma "Id (a, a)"
   5.137 +nitpick [card = 1\<midarrow>100, expect = none]
   5.138 +by (auto simp: Id_def Collect_def)
   5.139 +
   5.140 +lemma "Id ((a\<Colon>'a, b\<Colon>'a), (a, b))"
   5.141 +nitpick [card = 1\<midarrow>20, expect = none]
   5.142 +by (auto simp: Id_def Collect_def)
   5.143 +
   5.144 +lemma "UNIV (x\<Colon>'a\<times>'a)"
   5.145 +nitpick [card = 1\<midarrow>50, expect = none]
   5.146 +sorry
   5.147 +
   5.148 +lemma "{} = A - A"
   5.149 +nitpick [card = 1\<midarrow>100, expect = none]
   5.150 +by auto
   5.151 +
   5.152 +lemma "g = Let (A \<or> B)"
   5.153 +nitpick [card = 1, expect = none]
   5.154 +nitpick [card = 2, expect = genuine]
   5.155 +nitpick [card = 20, expect = genuine]
   5.156 +oops
   5.157 +
   5.158 +lemma "(let a_or_b = A \<or> B in a_or_b \<or> \<not> a_or_b)"
   5.159 +nitpick [expect = none]
   5.160 +by auto
   5.161 +
   5.162 +lemma "A \<subseteq> B"
   5.163 +nitpick [card = 100, expect = genuine]
   5.164 +oops
   5.165 +
   5.166 +lemma "A = {b}"
   5.167 +nitpick [card = 100, expect = genuine]
   5.168 +oops
   5.169 +
   5.170 +lemma "{a, b} = {b}"
   5.171 +nitpick [card = 100, expect = genuine]
   5.172 +oops
   5.173 +
   5.174 +lemma "(a\<Colon>'a\<times>'a, a\<Colon>'a\<times>'a) \<in> R"
   5.175 +nitpick [card = 1, expect = genuine]
   5.176 +nitpick [card = 2, expect = genuine]
   5.177 +nitpick [card = 4, expect = genuine]
   5.178 +nitpick [card = 20, expect = genuine]
   5.179 +nitpick [card = 10, dont_box, expect = genuine]
   5.180 +oops
   5.181 +
   5.182 +lemma "f (g\<Colon>'a\<Rightarrow>'a) = x"
   5.183 +nitpick [card = 3, expect = genuine]
   5.184 +nitpick [card = 3, dont_box, expect = genuine]
   5.185 +nitpick [card = 5, expect = genuine]
   5.186 +nitpick [card = 10, expect = genuine]
   5.187 +oops
   5.188 +
   5.189 +lemma "f (a, b) = x"
   5.190 +nitpick [card = 3, expect = genuine]
   5.191 +nitpick [card = 10, expect = genuine]
   5.192 +nitpick [card = 16, expect = genuine]
   5.193 +nitpick [card = 30, expect = genuine]
   5.194 +oops
   5.195 +
   5.196 +lemma "f (a, a) = f (c, d)"
   5.197 +nitpick [card = 4, expect = genuine]
   5.198 +nitpick [card = 20, expect = genuine]
   5.199 +oops
   5.200 +
   5.201 +lemma "(x\<Colon>'a) = (\<lambda>a. \<lambda>b. \<lambda>c. if c then a else b) x x True"
   5.202 +nitpick [card = 2, expect = none]
   5.203 +by auto
   5.204 +
   5.205 +lemma "\<exists>F. F a b = G a b"
   5.206 +nitpick [card = 3, expect = none]
   5.207 +by auto
   5.208 +
   5.209 +lemma "f = split"
   5.210 +nitpick [card = 1, expect = none]
   5.211 +nitpick [card = 2, expect = genuine]
   5.212 +oops
   5.213 +
   5.214 +lemma "(A\<Colon>'a\<times>'a, B\<Colon>'a\<times>'a) \<in> R \<Longrightarrow> (A, B) \<in> R"
   5.215 +nitpick [card = 20, expect = none]
   5.216 +by auto
   5.217 +
   5.218 +lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
   5.219 +       A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
   5.220 +nitpick [card = 1\<midarrow>50, expect = none]
   5.221 +by auto
   5.222 +
   5.223 +lemma "f = (\<lambda>x\<Colon>'a\<times>'b. x)"
   5.224 +nitpick [card = 3, expect = genuine]
   5.225 +nitpick [card = 4, expect = genuine]
   5.226 +nitpick [card = 8, expect = genuine]
   5.227 +oops
   5.228 +
   5.229 +subsection {* Quantifiers *}
   5.230 +
   5.231 +lemma "x = y"
   5.232 +nitpick [card 'a = 1, expect = none]
   5.233 +nitpick [card 'a = 2, expect = genuine]
   5.234 +nitpick [card 'a = 100, expect = genuine]
   5.235 +nitpick [card 'a = 1000, expect = genuine]
   5.236 +oops
   5.237 +
   5.238 +lemma "\<forall>x. x = y"
   5.239 +nitpick [card 'a = 1, expect = none]
   5.240 +nitpick [card 'a = 2, expect = genuine]
   5.241 +nitpick [card 'a = 100, expect = genuine]
   5.242 +nitpick [card 'a = 1000, expect = genuine]
   5.243 +oops
   5.244 +
   5.245 +lemma "\<forall>x\<Colon>'a \<Rightarrow> bool. x = y"
   5.246 +nitpick [card 'a = 1, expect = genuine]
   5.247 +nitpick [card 'a = 2, expect = genuine]
   5.248 +nitpick [card 'a = 100, expect = genuine]
   5.249 +nitpick [card 'a = 1000, expect = genuine]
   5.250 +oops
   5.251 +
   5.252 +lemma "\<exists>x\<Colon>'a \<Rightarrow> bool. x = y"
   5.253 +nitpick [card 'a = 1\<midarrow>10, expect = none]
   5.254 +by auto
   5.255 +
   5.256 +lemma "\<exists>x y\<Colon>'a \<Rightarrow> bool. x = y"
   5.257 +nitpick [card = 1\<midarrow>40, expect = none]
   5.258 +by auto
   5.259 +
   5.260 +lemma "\<forall>x. \<exists>y. f x y = f x (g x)"
   5.261 +nitpick [card = 1\<midarrow>5, expect = none]
   5.262 +by auto
   5.263 +
   5.264 +lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u) w (h u w)"
   5.265 +nitpick [card = 1\<midarrow>5, expect = none]
   5.266 +by auto
   5.267 +
   5.268 +lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. f u v w x = f u (g u w) w (h u)"
   5.269 +nitpick [card = 1\<midarrow>2, expect = genuine]
   5.270 +nitpick [card = 3, expect = genuine]
   5.271 +oops
   5.272 +
   5.273 +lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   5.274 +       f u v w x y z = f u (g u) w (h u w) y (k u w y)"
   5.275 +nitpick [card = 1\<midarrow>2, expect = none]
   5.276 +nitpick [card = 3, expect = none]
   5.277 +nitpick [card = 4, expect = none]
   5.278 +sorry
   5.279 +
   5.280 +lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   5.281 +       f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
   5.282 +nitpick [card = 1\<midarrow>2, expect = genuine]
   5.283 +oops
   5.284 +
   5.285 +lemma "\<forall>u. \<exists>v. \<forall>w. \<exists>x. \<forall>y. \<exists>z.
   5.286 +       f u v w x y z = f u (g u w) w (h u w) y (k u w y)"
   5.287 +nitpick [card = 1\<midarrow>2, expect = genuine]
   5.288 +oops
   5.289 +
   5.290 +lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
   5.291 +       f u v w x = f u (g u) w (h u w)"
   5.292 +nitpick [card = 1\<midarrow>2, expect = none]
   5.293 +sorry
   5.294 +
   5.295 +lemma "\<forall>u\<Colon>'a \<times> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<times> 'f.
   5.296 +       f u v w x = f u (g u w) w (h u)"
   5.297 +nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
   5.298 +oops
   5.299 +
   5.300 +lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
   5.301 +       f u v w x = f u (g u) w (h u w)"
   5.302 +nitpick [card = 1\<midarrow>2, dont_box, expect = none]
   5.303 +sorry
   5.304 +
   5.305 +lemma "\<forall>u\<Colon>'a \<Rightarrow> 'b. \<exists>v\<Colon>'c. \<forall>w\<Colon>'d. \<exists>x\<Colon>'e \<Rightarrow> 'f.
   5.306 +       f u v w x = f u (g u w) w (h u)"
   5.307 +nitpick [card = 1\<midarrow>2, dont_box, expect = genuine]
   5.308 +oops
   5.309 +
   5.310 +lemma "\<forall>x. if (\<forall>y. x = y) then False else True"
   5.311 +nitpick [card = 1, expect = genuine]
   5.312 +nitpick [card = 2\<midarrow>5, expect = none]
   5.313 +oops
   5.314 +
   5.315 +lemma "\<forall>x\<Colon>'a\<times>'b. if (\<forall>y. x = y) then False else True"
   5.316 +nitpick [card = 1, expect = genuine]
   5.317 +nitpick [card = 2, expect = none]
   5.318 +oops
   5.319 +
   5.320 +lemma "\<forall>x. if (\<exists>y. x = y) then True else False"
   5.321 +nitpick [expect = none]
   5.322 +sorry
   5.323 +
   5.324 +lemma "\<forall>x\<Colon>'a\<times>'b. if (\<exists>y. x = y) then True else False"
   5.325 +nitpick [expect = none]
   5.326 +sorry
   5.327 +
   5.328 +lemma "(\<not> (\<exists>x. P x)) \<longleftrightarrow> (\<forall>x. \<not> P x)"
   5.329 +nitpick [expect = none]
   5.330 +by auto
   5.331 +
   5.332 +lemma "(\<not> \<not> (\<exists>x. P x)) \<longleftrightarrow> (\<not> (\<forall>x. \<not> P x))"
   5.333 +nitpick [expect = none]
   5.334 +by auto
   5.335 +
   5.336 +lemma "(\<exists>x\<Colon>'a. \<forall>y. P x y) \<or> (\<exists>x\<Colon>'a \<times> 'a. \<forall>y. P y x)"
   5.337 +nitpick [card 'a = 1, expect = genuine]
   5.338 +nitpick [card 'a = 2, expect = genuine]
   5.339 +nitpick [card 'a = 3, expect = genuine]
   5.340 +nitpick [card 'a = 4, expect = genuine]
   5.341 +nitpick [card 'a = 5, expect = genuine]
   5.342 +oops
   5.343 +
   5.344 +lemma "\<exists>x. if x = y then (\<forall>y. y = x \<or> y \<noteq> x)
   5.345 +           else (\<forall>y. y = (x, x) \<or> y \<noteq> (x, x))"
   5.346 +nitpick [expect = none]
   5.347 +by auto
   5.348 +
   5.349 +lemma "\<exists>x. if x = y then (\<exists>y. y = x \<or> y \<noteq> x)
   5.350 +           else (\<exists>y. y = (x, x) \<or> y \<noteq> (x, x))"
   5.351 +nitpick [expect = none]
   5.352 +by auto
   5.353 +
   5.354 +lemma "let x = (\<forall>x. P x) in if x then x else \<not> x"
   5.355 +nitpick [expect = none]
   5.356 +by auto
   5.357 +
   5.358 +lemma "let x = (\<forall>x\<Colon>'a \<times> 'b. P x) in if x then x else \<not> x"
   5.359 +nitpick [expect = none]
   5.360 +by auto
   5.361 +
   5.362 +subsection {* Schematic Variables *}
   5.363 +
   5.364 +lemma "x = ?x"
   5.365 +nitpick [expect = none]
   5.366 +by auto
   5.367 +
   5.368 +lemma "\<forall>x. x = ?x"
   5.369 +nitpick [expect = genuine]
   5.370 +oops
   5.371 +
   5.372 +lemma "\<exists>x. x = ?x"
   5.373 +nitpick [expect = none]
   5.374 +by auto
   5.375 +
   5.376 +lemma "\<exists>x\<Colon>'a \<Rightarrow> 'b. x = ?x"
   5.377 +nitpick [expect = none]
   5.378 +by auto
   5.379 +
   5.380 +lemma "\<forall>x. ?x = ?y"
   5.381 +nitpick [expect = none]
   5.382 +by auto
   5.383 +
   5.384 +lemma "\<exists>x. ?x = ?y"
   5.385 +nitpick [expect = none]
   5.386 +by auto
   5.387 +
   5.388 +subsection {* Known Constants *}
   5.389 +
   5.390 +lemma "x \<equiv> all \<Longrightarrow> False"
   5.391 +nitpick [card = 1, expect = genuine]
   5.392 +nitpick [card = 1, box "('a \<Rightarrow> prop) \<Rightarrow> prop", expect = genuine]
   5.393 +nitpick [card = 2, expect = genuine]
   5.394 +nitpick [card = 8, expect = genuine]
   5.395 +nitpick [card = 10, expect = unknown]
   5.396 +oops
   5.397 +
   5.398 +lemma "\<And>x. f x y = f x y"
   5.399 +nitpick [expect = none]
   5.400 +oops
   5.401 +
   5.402 +lemma "\<And>x. f x y = f y x"
   5.403 +nitpick [expect = genuine]
   5.404 +oops
   5.405 +
   5.406 +lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop True"
   5.407 +nitpick [expect = none]
   5.408 +by auto
   5.409 +
   5.410 +lemma "all (\<lambda>x. Trueprop (f x y = f x y)) \<equiv> Trueprop False"
   5.411 +nitpick [expect = genuine]
   5.412 +oops
   5.413 +
   5.414 +lemma "I = (\<lambda>x. x) \<Longrightarrow> all P \<equiv> all (\<lambda>x. P (I x))"
   5.415 +nitpick [expect = none]
   5.416 +by auto
   5.417 +
   5.418 +lemma "x \<equiv> (op \<equiv>) \<Longrightarrow> False"
   5.419 +nitpick [card = 1, expect = genuine]
   5.420 +nitpick [card = 2, expect = genuine]
   5.421 +nitpick [card = 3, expect = genuine]
   5.422 +nitpick [card = 4, expect = genuine]
   5.423 +nitpick [card = 5, expect = genuine]
   5.424 +nitpick [card = 100, expect = genuine]
   5.425 +oops
   5.426 +
   5.427 +lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<equiv> x) \<equiv> (\<lambda>y. (x \<equiv> I y))"
   5.428 +nitpick [expect = none]
   5.429 +by auto
   5.430 +
   5.431 +lemma "P x \<equiv> P x"
   5.432 +nitpick [card = 1\<midarrow>10, expect = none]
   5.433 +by auto
   5.434 +
   5.435 +lemma "P x \<equiv> Q x \<Longrightarrow> P x = Q x"
   5.436 +nitpick [card = 1\<midarrow>10, expect = none]
   5.437 +by auto
   5.438 +
   5.439 +lemma "P x = Q x \<Longrightarrow> P x \<equiv> Q x"
   5.440 +nitpick [card = 1\<midarrow>10, expect = none]
   5.441 +by auto
   5.442 +
   5.443 +lemma "x \<equiv> (op \<Longrightarrow>) \<Longrightarrow> False"
   5.444 +nitpick [expect = genuine]
   5.445 +oops
   5.446 +
   5.447 +lemma "I \<equiv> (\<lambda>x. x) \<Longrightarrow> (op \<Longrightarrow> x) \<equiv> (\<lambda>y. (op \<Longrightarrow> x (I y)))"
   5.448 +nitpick [expect = none]
   5.449 +by auto
   5.450 +
   5.451 +lemma "P x \<Longrightarrow> P x"
   5.452 +nitpick [card = 1\<midarrow>10, expect = none]
   5.453 +by auto
   5.454 +
   5.455 +lemma "True \<Longrightarrow> True" "False \<Longrightarrow> True" "False \<Longrightarrow> False"
   5.456 +nitpick [expect = none]
   5.457 +by auto
   5.458 +
   5.459 +lemma "True \<Longrightarrow> False"
   5.460 +nitpick [expect = genuine]
   5.461 +oops
   5.462 +
   5.463 +lemma "x = Not"
   5.464 +nitpick [expect = genuine]
   5.465 +oops
   5.466 +
   5.467 +lemma "I = (\<lambda>x. x) \<Longrightarrow> Not = (\<lambda>x. Not (I x))"
   5.468 +nitpick [expect = none]
   5.469 +by auto
   5.470 +
   5.471 +lemma "x = True"
   5.472 +nitpick [expect = genuine]
   5.473 +oops
   5.474 +
   5.475 +lemma "x = False"
   5.476 +nitpick [expect = genuine]
   5.477 +oops
   5.478 +
   5.479 +lemma "x = undefined"
   5.480 +nitpick [expect = genuine]
   5.481 +oops
   5.482 +
   5.483 +lemma "(False, ()) = undefined \<Longrightarrow> ((), False) = undefined"
   5.484 +nitpick [expect = genuine]
   5.485 +oops
   5.486 +
   5.487 +lemma "undefined = undefined"
   5.488 +nitpick [expect = none]
   5.489 +by auto
   5.490 +
   5.491 +lemma "f undefined = f undefined"
   5.492 +nitpick [expect = none]
   5.493 +by auto
   5.494 +
   5.495 +lemma "f undefined = g undefined"
   5.496 +nitpick [card = 33, expect = genuine]
   5.497 +oops
   5.498 +
   5.499 +lemma "\<exists>!x. x = undefined"
   5.500 +nitpick [card = 30, expect = none]
   5.501 +by auto
   5.502 +
   5.503 +lemma "x = All \<Longrightarrow> False"
   5.504 +nitpick [card = 1, dont_box, expect = genuine]
   5.505 +nitpick [card = 2, dont_box, expect = genuine]
   5.506 +nitpick [card = 8, dont_box, expect = genuine]
   5.507 +nitpick [card = 10, dont_box, expect = unknown]
   5.508 +oops
   5.509 +
   5.510 +lemma "\<forall>x. f x y = f x y"
   5.511 +nitpick [expect = none]
   5.512 +oops
   5.513 +
   5.514 +lemma "\<forall>x. f x y = f y x"
   5.515 +nitpick [expect = genuine]
   5.516 +oops
   5.517 +
   5.518 +lemma "All (\<lambda>x. f x y = f x y) = True"
   5.519 +nitpick [expect = none]
   5.520 +by auto
   5.521 +
   5.522 +lemma "All (\<lambda>x. f x y = f x y) = False"
   5.523 +nitpick [expect = genuine]
   5.524 +oops
   5.525 +
   5.526 +lemma "I = (\<lambda>x. x) \<Longrightarrow> All P = All (\<lambda>x. P (I x))"
   5.527 +nitpick [expect = none]
   5.528 +by auto
   5.529 +
   5.530 +lemma "x = Ex \<Longrightarrow> False"
   5.531 +nitpick [card = 1, dont_box, expect = genuine]
   5.532 +nitpick [card = 2, dont_box, expect = genuine]
   5.533 +nitpick [card = 8, dont_box, expect = genuine]
   5.534 +nitpick [card = 10, dont_box, expect = unknown]
   5.535 +oops
   5.536 +
   5.537 +lemma "\<exists>x. f x y = f x y"
   5.538 +nitpick [expect = none]
   5.539 +oops
   5.540 +
   5.541 +lemma "\<exists>x. f x y = f y x"
   5.542 +nitpick [expect = none]
   5.543 +oops
   5.544 +
   5.545 +lemma "Ex (\<lambda>x. f x y = f x y) = True"
   5.546 +nitpick [expect = none]
   5.547 +by auto
   5.548 +
   5.549 +lemma "Ex (\<lambda>x. f x y = f y x) = True"
   5.550 +nitpick [expect = none]
   5.551 +by auto
   5.552 +
   5.553 +lemma "Ex (\<lambda>x. f x y = f x y) = False"
   5.554 +nitpick [expect = genuine]
   5.555 +oops
   5.556 +
   5.557 +lemma "Ex (\<lambda>x. f x y = f y x) = False"
   5.558 +nitpick [expect = genuine]
   5.559 +oops
   5.560 +
   5.561 +lemma "Ex (\<lambda>x. f x y \<noteq> f x y) = False"
   5.562 +nitpick [expect = none]
   5.563 +by auto
   5.564 +
   5.565 +lemma "I = (\<lambda>x. x) \<Longrightarrow> Ex P = Ex (\<lambda>x. P (I x))"
   5.566 +nitpick [expect = none]
   5.567 +by auto
   5.568 +
   5.569 +lemma "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x. (op= (I x)))"
   5.570 +      "I = (\<lambda>x. x) \<Longrightarrow> (op =) = (\<lambda>x y. x = (I y))"
   5.571 +nitpick [expect = none]
   5.572 +by auto
   5.573 +
   5.574 +lemma "x = y \<Longrightarrow> y = x"
   5.575 +nitpick [expect = none]
   5.576 +by auto
   5.577 +
   5.578 +lemma "x = y \<Longrightarrow> f x = f y"
   5.579 +nitpick [expect = none]
   5.580 +by auto
   5.581 +
   5.582 +lemma "x = y \<and> y = z \<Longrightarrow> x = z"
   5.583 +nitpick [expect = none]
   5.584 +by auto
   5.585 +
   5.586 +lemma "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x. op & (I x))"
   5.587 +      "I = (\<lambda>x. x) \<Longrightarrow> (op &) = (\<lambda>x y. x & (I y))"
   5.588 +nitpick [expect = none]
   5.589 +by auto
   5.590 +
   5.591 +lemma "(a \<and> b) = (\<not> (\<not> a \<or> \<not> b))"
   5.592 +nitpick [expect = none]
   5.593 +by auto
   5.594 +
   5.595 +lemma "a \<and> b \<Longrightarrow> a" "a \<and> b \<Longrightarrow> b"
   5.596 +nitpick [expect = none]
   5.597 +by auto
   5.598 +
   5.599 +lemma "\<not> a \<Longrightarrow> \<not> (a \<and> b)" "\<not> b \<Longrightarrow> \<not> (a \<and> b)"
   5.600 +nitpick [expect = none]
   5.601 +by auto
   5.602 +
   5.603 +lemma "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x. op \<or> (I x))"
   5.604 +      "I = (\<lambda>x. x) \<Longrightarrow> (op \<or>) = (\<lambda>x y. x \<or> (I y))"
   5.605 +nitpick [expect = none]
   5.606 +by auto
   5.607 +
   5.608 +lemma "a \<Longrightarrow> a \<or> b" "b \<Longrightarrow> a \<or> b"
   5.609 +nitpick [expect = none]
   5.610 +by auto
   5.611 +
   5.612 +lemma "\<not> (a \<or> b) \<Longrightarrow> \<not> a" "\<not> (a \<or> b) \<Longrightarrow> \<not> b"
   5.613 +nitpick [expect = none]
   5.614 +by auto
   5.615 +
   5.616 +lemma "(op \<longrightarrow>) = (\<lambda>x. op\<longrightarrow> x)" "(op\<longrightarrow> ) = (\<lambda>x y. x \<longrightarrow> y)"
   5.617 +nitpick [expect = none]
   5.618 +by auto
   5.619 +
   5.620 +lemma "\<not>a \<Longrightarrow> a \<longrightarrow> b" "b \<Longrightarrow> a \<longrightarrow> b"
   5.621 +nitpick [expect = none]
   5.622 +by auto
   5.623 +
   5.624 +lemma "\<lbrakk>a; \<not> b\<rbrakk> \<Longrightarrow> \<not> (a \<longrightarrow> b)"
   5.625 +nitpick [expect = none]
   5.626 +by auto
   5.627 +
   5.628 +lemma "((if a then b else c) = d) = ((a \<longrightarrow> (b = d)) \<and> (\<not> a \<longrightarrow> (c = d)))"
   5.629 +nitpick [expect = none]
   5.630 +by auto
   5.631 +
   5.632 +lemma "(if a then b else c) = (THE d. (a \<longrightarrow> (d = b)) \<and> (\<not> a \<longrightarrow> (d = c)))"
   5.633 +nitpick [expect = none]
   5.634 +by auto
   5.635 +
   5.636 +lemma "I = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x. If (I x))"
   5.637 +      "J = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y. If x (J y))"
   5.638 +      "K = (\<lambda>x. x) \<Longrightarrow> If = (\<lambda>x y z. If x y (K z))"
   5.639 +nitpick [expect = none]
   5.640 +by auto
   5.641 +
   5.642 +lemma "fst (x, y) = x"
   5.643 +nitpick [expect = none]
   5.644 +by (simp add: fst_def)
   5.645 +
   5.646 +lemma "snd (x, y) = y"
   5.647 +nitpick [expect = none]
   5.648 +by (simp add: snd_def)
   5.649 +
   5.650 +lemma "fst (x\<Colon>'a\<Rightarrow>'b, y) = x"
   5.651 +nitpick [expect = none]
   5.652 +by (simp add: fst_def)
   5.653 +
   5.654 +lemma "snd (x\<Colon>'a\<Rightarrow>'b, y) = y"
   5.655 +nitpick [expect = none]
   5.656 +by (simp add: snd_def)
   5.657 +
   5.658 +lemma "fst (x, y\<Colon>'a\<Rightarrow>'b) = x"
   5.659 +nitpick [expect = none]
   5.660 +by (simp add: fst_def)
   5.661 +
   5.662 +lemma "snd (x, y\<Colon>'a\<Rightarrow>'b) = y"
   5.663 +nitpick [expect = none]
   5.664 +by (simp add: snd_def)
   5.665 +
   5.666 +lemma "fst (x\<Colon>'a\<times>'b, y) = x"
   5.667 +nitpick [expect = none]
   5.668 +by (simp add: fst_def)
   5.669 +
   5.670 +lemma "snd (x\<Colon>'a\<times>'b, y) = y"
   5.671 +nitpick [expect = none]
   5.672 +by (simp add: snd_def)
   5.673 +
   5.674 +lemma "fst (x, y\<Colon>'a\<times>'b) = x"
   5.675 +nitpick [expect = none]
   5.676 +by (simp add: fst_def)
   5.677 +
   5.678 +lemma "snd (x, y\<Colon>'a\<times>'b) = y"
   5.679 +nitpick [expect = none]
   5.680 +by (simp add: snd_def)
   5.681 +
   5.682 +lemma "fst p = (THE a. \<exists>b. p = Pair a b)"
   5.683 +nitpick [expect = none]
   5.684 +by (simp add: fst_def)
   5.685 +
   5.686 +lemma "snd p = (THE b. \<exists>a. p = Pair a b)"
   5.687 +nitpick [expect = none]
   5.688 +by (simp add: snd_def)
   5.689 +
   5.690 +lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))"
   5.691 +nitpick [expect = none]
   5.692 +by auto
   5.693 +
   5.694 +lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))"
   5.695 +nitpick [expect = none]
   5.696 +by auto
   5.697 +
   5.698 +lemma "fst (x, y) = snd (y, x)"
   5.699 +nitpick [expect = none]
   5.700 +by auto
   5.701 +
   5.702 +lemma "(x, x) \<in> Id"
   5.703 +nitpick [expect = none]
   5.704 +by auto
   5.705 +
   5.706 +lemma "(x, y) \<in> Id \<Longrightarrow> x = y"
   5.707 +nitpick [expect = none]
   5.708 +by auto
   5.709 +
   5.710 +lemma "I = (\<lambda>x. x) \<Longrightarrow> Id = (\<lambda>x. Id (I x))"
   5.711 +nitpick [expect = none]
   5.712 +by auto
   5.713 +
   5.714 +lemma "I = (\<lambda>x. x) \<Longrightarrow> curry Id = (\<lambda>x y. Id (x, I y))"
   5.715 +nitpick [expect = none]
   5.716 +by (simp add: curry_def)
   5.717 +
   5.718 +lemma "{} = (\<lambda>x. False)"
   5.719 +nitpick [expect = none]
   5.720 +by (metis Collect_def bot_set_eq empty_def)
   5.721 +
   5.722 +lemma "x \<in> {}"
   5.723 +nitpick [expect = genuine]
   5.724 +oops
   5.725 +
   5.726 +lemma "{a, b} = {b}"
   5.727 +nitpick [expect = genuine]
   5.728 +oops
   5.729 +
   5.730 +lemma "{a, b} \<noteq> {b}"
   5.731 +nitpick [expect = genuine]
   5.732 +oops
   5.733 +
   5.734 +lemma "{a} = {b}"
   5.735 +nitpick [expect = genuine]
   5.736 +oops
   5.737 +
   5.738 +lemma "{a} \<noteq> {b}"
   5.739 +nitpick [expect = genuine]
   5.740 +oops
   5.741 +
   5.742 +lemma "{a, b, c} = {c, b, a}"
   5.743 +nitpick [expect = none]
   5.744 +by auto
   5.745 +
   5.746 +lemma "UNIV = (\<lambda>x. True)"
   5.747 +nitpick [expect = none]
   5.748 +by (simp only: UNIV_def Collect_def)
   5.749 +
   5.750 +lemma "UNIV x = True"
   5.751 +nitpick [expect = none]
   5.752 +by (simp only: UNIV_def Collect_def)
   5.753 +
   5.754 +lemma "x \<notin> UNIV"
   5.755 +nitpick [expect = genuine]
   5.756 +oops
   5.757 +
   5.758 +lemma "op \<in> = (\<lambda>x P. P x)"
   5.759 +nitpick [expect = none]
   5.760 +apply (rule ext)
   5.761 +apply (rule ext)
   5.762 +by (simp add: mem_def)
   5.763 +
   5.764 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<in> = (\<lambda>x. (op \<in> (I x)))"
   5.765 +nitpick [expect = none]
   5.766 +apply (rule ext)
   5.767 +apply (rule ext)
   5.768 +by (simp add: mem_def)
   5.769 +
   5.770 +lemma "P x = (x \<in> P)"
   5.771 +nitpick [expect = none]
   5.772 +by (simp add: mem_def)
   5.773 +
   5.774 +lemma "I = (\<lambda>x. x) \<Longrightarrow> insert = (\<lambda>x. insert (I x))"
   5.775 +nitpick [expect = none]
   5.776 +by simp
   5.777 +
   5.778 +lemma "insert = (\<lambda>x y. insert x (y \<union> y))"
   5.779 +nitpick [expect = none]
   5.780 +by simp
   5.781 +
   5.782 +lemma "I = (\<lambda>x. x) \<Longrightarrow> trancl = (\<lambda>x. trancl (I x))"
   5.783 +nitpick [card = 1\<midarrow>2, expect = none]
   5.784 +by auto
   5.785 +
   5.786 +lemma "rtrancl = (\<lambda>x. rtrancl x \<union> {(y, y)})"
   5.787 +nitpick [card = 1\<midarrow>3, expect = none]
   5.788 +apply (rule ext)
   5.789 +by auto
   5.790 +
   5.791 +lemma "(x, x) \<in> rtrancl {(y, y)}"
   5.792 +nitpick [expect = none]
   5.793 +by auto
   5.794 +
   5.795 +lemma "I = (\<lambda>x. x) \<Longrightarrow> rtrancl = (\<lambda>x. rtrancl (I x))"
   5.796 +nitpick [card = 1\<midarrow>2, expect = none]
   5.797 +by auto
   5.798 +
   5.799 +lemma "((x, x), (x, x)) \<in> rtrancl {}"
   5.800 +nitpick [expect = none]
   5.801 +by auto
   5.802 +
   5.803 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x. op \<union> (I x))"
   5.804 +nitpick [card = 1\<midarrow>5, expect = none]
   5.805 +by auto
   5.806 +
   5.807 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<union> = (\<lambda>x y. op \<union> x (I y))"
   5.808 +nitpick [card = 1\<midarrow>5, expect = none]
   5.809 +by auto
   5.810 +
   5.811 +lemma "a \<in> A \<Longrightarrow> a \<in> (A \<union> B)" "b \<in> B \<Longrightarrow> b \<in> (A \<union> B)"
   5.812 +nitpick [expect = none]
   5.813 +by auto
   5.814 +
   5.815 +lemma "a \<in> (A \<union> B) \<Longrightarrow> a \<in> A \<or> a \<in> B"
   5.816 +nitpick [expect = none]
   5.817 +by auto
   5.818 +
   5.819 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x. op \<inter> (I x))"
   5.820 +nitpick [card = 1\<midarrow>5, expect = none]
   5.821 +by auto
   5.822 +
   5.823 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<inter> = (\<lambda>x y. op \<inter> x (I y))"
   5.824 +nitpick [card = 1\<midarrow>5, expect = none]
   5.825 +by auto
   5.826 +
   5.827 +lemma "a \<notin> A \<Longrightarrow> a \<notin> (A \<inter> B)" "b \<notin> B \<Longrightarrow> b \<notin> (A \<inter> B)"
   5.828 +nitpick [card = 1\<midarrow>5, expect = none]
   5.829 +by auto
   5.830 +
   5.831 +lemma "a \<notin> (A \<inter> B) \<Longrightarrow> a \<notin> A \<or> a \<notin> B"
   5.832 +nitpick [expect = none]
   5.833 +by auto
   5.834 +
   5.835 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x\<Colon>'a set. op - (I x))"
   5.836 +nitpick [card = 1\<midarrow>5, expect = none]
   5.837 +by auto
   5.838 +
   5.839 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op - = (\<lambda>x y\<Colon>'a set. op - x (I y))"
   5.840 +nitpick [card = 1\<midarrow>5, expect = none]
   5.841 +by auto
   5.842 +
   5.843 +lemma "x \<in> ((A\<Colon>'a set) - B) \<longleftrightarrow> x \<in> A \<and> x \<notin> B"
   5.844 +nitpick [card = 1\<midarrow>5, expect = none]
   5.845 +by auto
   5.846 +
   5.847 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x. op \<subset> (I x))"
   5.848 +nitpick [card = 1\<midarrow>5, expect = none]
   5.849 +by auto
   5.850 +
   5.851 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subset> = (\<lambda>x y. op \<subset> x (I y))"
   5.852 +nitpick [card = 1\<midarrow>5, expect = none]
   5.853 +by auto
   5.854 +
   5.855 +lemma "A \<subset> B \<Longrightarrow> (\<forall>a \<in> A. a \<in> B) \<and> (\<exists>b \<in> B. b \<notin> A)"
   5.856 +nitpick [card = 1\<midarrow>5, expect = none]
   5.857 +by auto
   5.858 +
   5.859 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x. op \<subseteq> (I x))"
   5.860 +nitpick [card = 1\<midarrow>5, expect = none]
   5.861 +by auto
   5.862 +
   5.863 +lemma "I = (\<lambda>x. x) \<Longrightarrow> op \<subseteq> = (\<lambda>x y. op \<subseteq> x (I y))"
   5.864 +nitpick [card = 1\<midarrow>5, expect = none]
   5.865 +by auto
   5.866 +
   5.867 +lemma "A \<subseteq> B \<Longrightarrow> \<forall>a \<in> A. a \<in> B"
   5.868 +nitpick [card = 1\<midarrow>5, expect = none]
   5.869 +by auto
   5.870 +
   5.871 +lemma "A \<subseteq> B \<Longrightarrow> A \<subset> B"
   5.872 +nitpick [card = 5, expect = genuine]
   5.873 +oops
   5.874 +
   5.875 +lemma "A \<subset> B \<Longrightarrow> A \<subseteq> B"
   5.876 +nitpick [expect = none]
   5.877 +by auto
   5.878 +
   5.879 +lemma "I = (\<lambda>x\<Colon>'a set. x) \<Longrightarrow> uminus = (\<lambda>x. uminus (I x))"
   5.880 +nitpick [expect = none]
   5.881 +by auto
   5.882 +
   5.883 +lemma "A \<union> - A = UNIV"
   5.884 +nitpick [expect = none]
   5.885 +by auto
   5.886 +
   5.887 +lemma "A \<inter> - A = {}"
   5.888 +nitpick [expect = none]
   5.889 +by auto
   5.890 +
   5.891 +lemma "A = -(A\<Colon>'a set)"
   5.892 +nitpick [card 'a = 10, expect = genuine]
   5.893 +oops
   5.894 +
   5.895 +lemma "I = (\<lambda>x. x) \<Longrightarrow> finite = (\<lambda>x. finite (I x))"
   5.896 +nitpick [expect = none]
   5.897 +oops
   5.898 +
   5.899 +lemma "finite A"
   5.900 +nitpick [expect = none]
   5.901 +oops
   5.902 +
   5.903 +lemma "finite A \<Longrightarrow> finite B"
   5.904 +nitpick [expect = none]
   5.905 +oops
   5.906 +
   5.907 +lemma "All finite"
   5.908 +nitpick [expect = none]
   5.909 +oops
   5.910 +
   5.911 +subsection {* The and Eps *}
   5.912 +
   5.913 +lemma "x = The"
   5.914 +nitpick [card = 5, expect = genuine]
   5.915 +oops
   5.916 +
   5.917 +lemma "\<exists>x. x = The"
   5.918 +nitpick [card = 1\<midarrow>3]
   5.919 +by auto
   5.920 +
   5.921 +lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> The P = x"
   5.922 +nitpick [expect = none]
   5.923 +by auto
   5.924 +
   5.925 +lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = z"
   5.926 +nitpick [expect = genuine]
   5.927 +oops
   5.928 +
   5.929 +lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> The P = x \<or> The P = y"
   5.930 +nitpick [card = 2, expect = none]
   5.931 +nitpick [card = 3\<midarrow>5, expect = genuine]
   5.932 +oops
   5.933 +
   5.934 +lemma "P x \<Longrightarrow> P (The P)"
   5.935 +nitpick [card = 1, expect = none]
   5.936 +nitpick [card = 1\<midarrow>2, expect = none]
   5.937 +nitpick [card = 3\<midarrow>5, expect = genuine]
   5.938 +nitpick [card = 8, expect = genuine]
   5.939 +oops
   5.940 +
   5.941 +lemma "(\<forall>x. \<not> P x) \<longrightarrow> The P = y"
   5.942 +nitpick [expect = genuine]
   5.943 +oops
   5.944 +
   5.945 +lemma "I = (\<lambda>x. x) \<Longrightarrow> The = (\<lambda>x. The (I x))"
   5.946 +nitpick [card = 1\<midarrow>5, expect = none]
   5.947 +by auto
   5.948 +
   5.949 +lemma "x = Eps"
   5.950 +nitpick [card = 5, expect = genuine]
   5.951 +oops
   5.952 +
   5.953 +lemma "\<exists>x. x = Eps"
   5.954 +nitpick [card = 1\<midarrow>3, expect = none]
   5.955 +by auto
   5.956 +
   5.957 +lemma "P x \<and> (\<forall>y. P y \<longrightarrow> y = x) \<longrightarrow> Eps P = x"
   5.958 +nitpick [expect = none]
   5.959 +by auto
   5.960 +
   5.961 +lemma "P x \<and> P y \<and> x \<noteq> y \<longrightarrow> Eps P = z"
   5.962 +nitpick [expect = genuine]
   5.963 +apply auto
   5.964 +oops
   5.965 +
   5.966 +lemma "P x \<Longrightarrow> P (Eps P)"
   5.967 +nitpick [card = 1\<midarrow>8, expect = none]
   5.968 +by (metis exE_some)
   5.969 +
   5.970 +lemma "\<forall>x. \<not> P x \<longrightarrow> Eps P = y"
   5.971 +nitpick [expect = genuine]
   5.972 +oops
   5.973 +
   5.974 +lemma "P (Eps P)"
   5.975 +nitpick [expect = genuine]
   5.976 +oops
   5.977 +
   5.978 +lemma "(P\<Colon>nat set) (Eps P)"
   5.979 +nitpick [expect = genuine]
   5.980 +oops
   5.981 +
   5.982 +lemma "\<not> P (Eps P)"
   5.983 +nitpick [expect = genuine]
   5.984 +oops
   5.985 +
   5.986 +lemma "\<not> (P\<Colon>nat set) (Eps P)"
   5.987 +nitpick [expect = genuine]
   5.988 +oops
   5.989 +
   5.990 +lemma "P \<noteq> {} \<Longrightarrow> P (Eps P)"
   5.991 +nitpick [expect = none]
   5.992 +sorry
   5.993 +
   5.994 +lemma "(P\<Colon>nat set) \<noteq> {} \<Longrightarrow> P (Eps P)"
   5.995 +nitpick [expect = none]
   5.996 +sorry
   5.997 +
   5.998 +lemma "P (The P)"
   5.999 +nitpick [expect = genuine]
  5.1000 +oops
  5.1001 +
  5.1002 +lemma "(P\<Colon>nat set) (The P)"
  5.1003 +nitpick [expect = genuine]
  5.1004 +oops
  5.1005 +
  5.1006 +lemma "\<not> P (The P)"
  5.1007 +nitpick [expect = genuine]
  5.1008 +oops
  5.1009 +
  5.1010 +lemma "\<not> (P\<Colon>nat set) (The P)"
  5.1011 +nitpick [expect = genuine]
  5.1012 +oops
  5.1013 +
  5.1014 +lemma "The P \<noteq> x"
  5.1015 +nitpick [expect = genuine]
  5.1016 +oops
  5.1017 +
  5.1018 +lemma "The P \<noteq> (x\<Colon>nat)"
  5.1019 +nitpick [expect = genuine]
  5.1020 +oops
  5.1021 +
  5.1022 +lemma "P x \<Longrightarrow> P (The P)"
  5.1023 +nitpick [expect = genuine]
  5.1024 +oops
  5.1025 +
  5.1026 +lemma "P (x\<Colon>nat) \<Longrightarrow> P (The P)"
  5.1027 +nitpick [expect = genuine]
  5.1028 +oops
  5.1029 +
  5.1030 +lemma "P = {x} \<Longrightarrow> P (The P)"
  5.1031 +nitpick [expect = none]
  5.1032 +oops
  5.1033 +
  5.1034 +lemma "P = {x\<Colon>nat} \<Longrightarrow> P (The P)"
  5.1035 +nitpick [expect = none]
  5.1036 +oops
  5.1037 +
  5.1038 +consts Q :: 'a
  5.1039 +
  5.1040 +lemma "Q (Eps Q)"
  5.1041 +nitpick [expect = genuine]
  5.1042 +oops
  5.1043 +
  5.1044 +lemma "(Q\<Colon>nat set) (Eps Q)"
  5.1045 +nitpick [expect = none]
  5.1046 +oops
  5.1047 +
  5.1048 +lemma "\<not> Q (Eps Q)"
  5.1049 +nitpick [expect = genuine]
  5.1050 +oops
  5.1051 +
  5.1052 +lemma "\<not> (Q\<Colon>nat set) (Eps Q)"
  5.1053 +nitpick [expect = genuine]
  5.1054 +oops
  5.1055 +
  5.1056 +lemma "(Q\<Colon>'a set) \<noteq> {} \<Longrightarrow> (Q\<Colon>'a set) (Eps Q)"
  5.1057 +nitpick [expect = none]
  5.1058 +sorry
  5.1059 +
  5.1060 +lemma "(Q\<Colon>nat set) \<noteq> {} \<Longrightarrow> (Q\<Colon>nat set) (Eps Q)"
  5.1061 +nitpick [expect = none]
  5.1062 +sorry
  5.1063 +
  5.1064 +lemma "Q (The Q)"
  5.1065 +nitpick [expect = genuine]
  5.1066 +oops
  5.1067 +
  5.1068 +lemma "(Q\<Colon>nat set) (The Q)"
  5.1069 +nitpick [expect = genuine]
  5.1070 +oops
  5.1071 +
  5.1072 +lemma "\<not> Q (The Q)"
  5.1073 +nitpick [expect = genuine]
  5.1074 +oops
  5.1075 +
  5.1076 +lemma "\<not> (Q\<Colon>nat set) (The Q)"
  5.1077 +nitpick [expect = genuine]
  5.1078 +oops
  5.1079 +
  5.1080 +lemma "The Q \<noteq> x"
  5.1081 +nitpick [expect = genuine]
  5.1082 +oops
  5.1083 +
  5.1084 +lemma "The Q \<noteq> (x\<Colon>nat)"
  5.1085 +nitpick [expect = genuine]
  5.1086 +oops
  5.1087 +
  5.1088 +lemma "Q x \<Longrightarrow> Q (The Q)"
  5.1089 +nitpick [expect = genuine]
  5.1090 +oops
  5.1091 +
  5.1092 +lemma "Q (x\<Colon>nat) \<Longrightarrow> Q (The Q)"
  5.1093 +nitpick [expect = genuine]
  5.1094 +oops
  5.1095 +
  5.1096 +lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"
  5.1097 +nitpick [expect = none]
  5.1098 +oops
  5.1099 +
  5.1100 +lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"
  5.1101 +nitpick [expect = none]
  5.1102 +oops
  5.1103 +
  5.1104 +subsection {* Destructors and Recursors *}
  5.1105 +
  5.1106 +lemma "(x\<Colon>'a) = (case True of True \<Rightarrow> x | False \<Rightarrow> x)"
  5.1107 +nitpick [card = 2, expect = none]
  5.1108 +by auto
  5.1109 +
  5.1110 +lemma "bool_rec x y True = x"
  5.1111 +nitpick [card = 2, expect = none]
  5.1112 +by auto
  5.1113 +
  5.1114 +lemma "bool_rec x y False = y"
  5.1115 +nitpick [card = 2, expect = none]
  5.1116 +by auto
  5.1117 +
  5.1118 +lemma "(x\<Colon>bool) = bool_rec x x True"
  5.1119 +nitpick [card = 2, expect = none]
  5.1120 +by auto
  5.1121 +
  5.1122 +lemma "x = (case (x, y) of (x', y') \<Rightarrow> x')"
  5.1123 +nitpick [expect = none]
  5.1124 +sorry
  5.1125 +
  5.1126 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
     6.3 @@ -0,0 +1,104 @@
     6.4 +(*  Title:      HOL/Nitpick_Examples/Datatype_Nits.thy
     6.5 +    Author:     Jasmin Blanchette, TU Muenchen
     6.6 +    Copyright   2009
     6.7 +
     6.8 +Examples featuring Nitpick applied to datatypes.
     6.9 +*)
    6.10 +
    6.11 +header {* Examples Featuring Nitpick Applied to Datatypes *}
    6.12 +
    6.13 +theory Datatype_Nits
    6.14 +imports Main
    6.15 +begin
    6.16 +
    6.17 +primrec rot where
    6.18 +"rot Nibble0 = Nibble1" |
    6.19 +"rot Nibble1 = Nibble2" |
    6.20 +"rot Nibble2 = Nibble3" |
    6.21 +"rot Nibble3 = Nibble4" |
    6.22 +"rot Nibble4 = Nibble5" |
    6.23 +"rot Nibble5 = Nibble6" |
    6.24 +"rot Nibble6 = Nibble7" |
    6.25 +"rot Nibble7 = Nibble8" |
    6.26 +"rot Nibble8 = Nibble9" |
    6.27 +"rot Nibble9 = NibbleA" |
    6.28 +"rot NibbleA = NibbleB" |
    6.29 +"rot NibbleB = NibbleC" |
    6.30 +"rot NibbleC = NibbleD" |
    6.31 +"rot NibbleD = NibbleE" |
    6.32 +"rot NibbleE = NibbleF" |
    6.33 +"rot NibbleF = Nibble0"
    6.34 +
    6.35 +lemma "rot n \<noteq> n"
    6.36 +nitpick [card = 1\<midarrow>16, expect = none]
    6.37 +sorry
    6.38 +
    6.39 +lemma "rot Nibble2 \<noteq> Nibble3"
    6.40 +nitpick [card = 1, expect = none]
    6.41 +nitpick [card = 2, expect = genuine]
    6.42 +nitpick [card = 2, max Nibble2 = 0, expect = none]
    6.43 +nitpick [card = 2, max Nibble3 = 0, expect = none]
    6.44 +oops
    6.45 +
    6.46 +lemma "fun_pow 15 rot n \<noteq> n"
    6.47 +nitpick [card = 17, expect = none]
    6.48 +sorry
    6.49 +
    6.50 +lemma "fun_pow 15 rot n = n"
    6.51 +nitpick [card = 17, expect = genuine]
    6.52 +oops
    6.53 +
    6.54 +lemma "fun_pow 16 rot n = n"
    6.55 +nitpick [card = 17, expect = none]
    6.56 +oops
    6.57 +
    6.58 +datatype ('a, 'b) pd = Pd "'a \<times> 'b"
    6.59 +
    6.60 +fun fs where
    6.61 +"fs (Pd (a, _)) = a"
    6.62 +
    6.63 +fun sn where
    6.64 +"sn (Pd (_, b)) = b"
    6.65 +
    6.66 +lemma "fs (Pd p) = fst p"
    6.67 +nitpick [card = 20, expect = none]
    6.68 +sorry
    6.69 +
    6.70 +lemma "fs (Pd p) = snd p"
    6.71 +nitpick [expect = genuine]
    6.72 +oops
    6.73 +
    6.74 +lemma "sn (Pd p) = snd p"
    6.75 +nitpick [card = 20, expect = none]
    6.76 +sorry
    6.77 +
    6.78 +lemma "sn (Pd p) = fst p"
    6.79 +nitpick [expect = genuine]
    6.80 +oops
    6.81 +
    6.82 +lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
    6.83 +nitpick [card = 1\<midarrow>12, expect = none]
    6.84 +sorry
    6.85 +
    6.86 +lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
    6.87 +nitpick [expect = genuine]
    6.88 +oops
    6.89 +
    6.90 +datatype ('a, 'b) fn = Fn "'a \<Rightarrow> 'b"
    6.91 +
    6.92 +fun app where
    6.93 +"app (Fn f) x = f x"
    6.94 +
    6.95 +lemma "app (Fn g) y = g y"
    6.96 +nitpick [card = 1\<midarrow>12, expect = none]
    6.97 +sorry
    6.98 +
    6.99 +lemma "app (Fn g) y = g' y"
   6.100 +nitpick [expect = genuine]
   6.101 +oops
   6.102 +
   6.103 +lemma "app (Fn g) y = g y'"
   6.104 +nitpick [expect = genuine]
   6.105 +oops
   6.106 +
   6.107 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Nitpick_Examples/Induct_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
     7.3 @@ -0,0 +1,171 @@
     7.4 +(*  Title:      HOL/Nitpick_Examples/Induct_Nits.thy
     7.5 +    Author:     Jasmin Blanchette, TU Muenchen
     7.6 +    Copyright   2009
     7.7 +
     7.8 +Examples featuring Nitpick applied to (co)inductive definitions.
     7.9 +*)
    7.10 +
    7.11 +header {* Examples Featuring Nitpick Applied to (Co)inductive Definitions *}
    7.12 +
    7.13 +theory Induct_Nits
    7.14 +imports Main
    7.15 +begin
    7.16 +
    7.17 +nitpick_params [show_all]
    7.18 +
    7.19 +inductive p1 :: "nat \<Rightarrow> bool" where
    7.20 +"p1 0" |
    7.21 +"p1 n \<Longrightarrow> p1 (n + 2)"
    7.22 +
    7.23 +coinductive q1 :: "nat \<Rightarrow> bool" where
    7.24 +"q1 0" |
    7.25 +"q1 n \<Longrightarrow> q1 (n + 2)"
    7.26 +
    7.27 +lemma "p1 = q1"
    7.28 +nitpick [expect = none]
    7.29 +nitpick [wf, expect = none]
    7.30 +nitpick [non_wf, expect = none]
    7.31 +nitpick [non_wf, dont_star_linear_preds, expect = none]
    7.32 +oops
    7.33 +
    7.34 +lemma "p1 \<noteq> q1"
    7.35 +nitpick [expect = potential]
    7.36 +nitpick [wf, expect = potential]
    7.37 +nitpick [non_wf, expect = potential]
    7.38 +nitpick [non_wf, dont_star_linear_preds, expect = potential]
    7.39 +oops
    7.40 +
    7.41 +lemma "p1 (n - 2) \<Longrightarrow> p1 n"
    7.42 +nitpick [expect = genuine]
    7.43 +nitpick [non_wf, expect = genuine]
    7.44 +nitpick [non_wf, dont_star_linear_preds, expect = genuine]
    7.45 +oops
    7.46 +
    7.47 +lemma "q1 (n - 2) \<Longrightarrow> q1 n"
    7.48 +nitpick [expect = genuine]
    7.49 +nitpick [non_wf, expect = genuine]
    7.50 +nitpick [non_wf, dont_star_linear_preds, expect = genuine]
    7.51 +oops
    7.52 +
    7.53 +inductive p2 :: "nat \<Rightarrow> bool" where
    7.54 +"p2 n \<Longrightarrow> p2 n"
    7.55 +
    7.56 +coinductive q2 :: "nat \<Rightarrow> bool" where
    7.57 +"q2 n \<Longrightarrow> q2 n"
    7.58 +
    7.59 +lemma "p2 = {}"
    7.60 +nitpick [expect = none]
    7.61 +nitpick [dont_star_linear_preds, expect = none]
    7.62 +sorry
    7.63 +
    7.64 +lemma "q2 = {}"
    7.65 +nitpick [expect = genuine]
    7.66 +nitpick [dont_star_linear_preds, expect = genuine]
    7.67 +nitpick [wf, expect = likely_genuine]
    7.68 +oops
    7.69 +
    7.70 +lemma "p2 = UNIV"
    7.71 +nitpick [expect = genuine]
    7.72 +nitpick [dont_star_linear_preds, expect = genuine]
    7.73 +oops
    7.74 +
    7.75 +lemma "q2 = UNIV"
    7.76 +nitpick [expect = none]
    7.77 +nitpick [dont_star_linear_preds, expect = none]
    7.78 +nitpick [wf, expect = likely_genuine]
    7.79 +sorry
    7.80 +
    7.81 +lemma "p2 = q2"
    7.82 +nitpick [expect = genuine]
    7.83 +nitpick [dont_star_linear_preds, expect = genuine]
    7.84 +oops
    7.85 +
    7.86 +lemma "p2 n"
    7.87 +nitpick [expect = genuine]
    7.88 +nitpick [dont_star_linear_preds, expect = genuine]
    7.89 +nitpick [dont_specialize, expect = genuine]
    7.90 +oops
    7.91 +
    7.92 +lemma "q2 n"
    7.93 +nitpick [expect = none]
    7.94 +nitpick [dont_star_linear_preds, expect = none]
    7.95 +sorry
    7.96 +
    7.97 +lemma "\<not> p2 n"
    7.98 +nitpick [expect = none]
    7.99 +nitpick [dont_star_linear_preds, expect = none]
   7.100 +sorry
   7.101 +
   7.102 +lemma "\<not> q2 n"
   7.103 +nitpick [expect = genuine]
   7.104 +nitpick [dont_star_linear_preds, expect = genuine]
   7.105 +nitpick [dont_specialize, expect = genuine]
   7.106 +oops
   7.107 +
   7.108 +inductive p3 and p4 where
   7.109 +"p3 0" |
   7.110 +"p3 n \<Longrightarrow> p4 (Suc n)" |
   7.111 +"p4 n \<Longrightarrow> p3 (Suc n)"
   7.112 +
   7.113 +coinductive q3 and q4 where
   7.114 +"q3 0" |
   7.115 +"q3 n \<Longrightarrow> q4 (Suc n)" |
   7.116 +"q4 n \<Longrightarrow> q3 (Suc n)"
   7.117 +
   7.118 +lemma "p3 = q3"
   7.119 +nitpick [expect = none]
   7.120 +nitpick [dont_star_linear_preds, expect = none]
   7.121 +nitpick [non_wf, expect = potential]
   7.122 +nitpick [non_wf, dont_box, expect = none]
   7.123 +nitpick [non_wf, dont_star_linear_preds, expect = none]
   7.124 +sorry
   7.125 +
   7.126 +lemma "p4 = q4"
   7.127 +nitpick [expect = none]
   7.128 +nitpick [dont_star_linear_preds, expect = none]
   7.129 +nitpick [non_wf, expect = potential]
   7.130 +nitpick [non_wf, dont_box, expect = none]
   7.131 +nitpick [non_wf, dont_star_linear_preds, expect = none]
   7.132 +sorry
   7.133 +
   7.134 +lemma "p3 = UNIV - p4"
   7.135 +nitpick [expect = none]
   7.136 +nitpick [dont_star_linear_preds, expect = none]
   7.137 +nitpick [non_wf, expect = potential]
   7.138 +nitpick [non_wf, dont_box, expect = none]
   7.139 +nitpick [non_wf, dont_star_linear_preds, expect = none]
   7.140 +sorry
   7.141 +
   7.142 +lemma "q3 = UNIV - q4"
   7.143 +nitpick [expect = none]
   7.144 +nitpick [dont_star_linear_preds, expect = none]
   7.145 +nitpick [non_wf, expect = none]
   7.146 +nitpick [non_wf, dont_box, expect = none]
   7.147 +nitpick [non_wf, dont_star_linear_preds, expect = none]
   7.148 +sorry
   7.149 +
   7.150 +lemma "p3 \<inter> q4 \<noteq> {}"
   7.151 +nitpick [expect = potential]
   7.152 +nitpick [non_wf, expect = potential]
   7.153 +nitpick [non_wf, dont_star_linear_preds, expect = potential]
   7.154 +sorry
   7.155 +
   7.156 +lemma "q3 \<inter> p4 \<noteq> {}"
   7.157 +nitpick [expect = potential]
   7.158 +nitpick [non_wf, expect = potential]
   7.159 +nitpick [non_wf, dont_star_linear_preds, expect = potential]
   7.160 +sorry
   7.161 +
   7.162 +lemma "p3 \<union> q4 \<noteq> UNIV"
   7.163 +nitpick [expect = potential]
   7.164 +nitpick [non_wf, expect = potential]
   7.165 +nitpick [non_wf, dont_star_linear_preds, expect = potential]
   7.166 +sorry
   7.167 +
   7.168 +lemma "q3 \<union> p4 \<noteq> UNIV"
   7.169 +nitpick [expect = potential]
   7.170 +nitpick [non_wf, expect = potential]
   7.171 +nitpick [non_wf, dont_star_linear_preds, expect = potential]
   7.172 +sorry
   7.173 +
   7.174 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
     8.3 @@ -0,0 +1,389 @@
     8.4 +(*  Title:      HOL/Nitpick_Examples/Manual_Nits.thy
     8.5 +    Author:     Jasmin Blanchette, TU Muenchen
     8.6 +    Copyright   2009
     8.7 +
     8.8 +Examples from the Nitpick manual.
     8.9 +*)
    8.10 +
    8.11 +header {* Examples from the Nitpick Manual *}
    8.12 +
    8.13 +theory Manual_Nits
    8.14 +imports Main Coinductive_List RealDef
    8.15 +begin
    8.16 +
    8.17 +chapter {* 3. First Steps *}
    8.18 +
    8.19 +nitpick_params [sat_solver = MiniSatJNI, max_threads = 1]
    8.20 +
    8.21 +subsection {* 3.1. Propositional Logic *}
    8.22 +
    8.23 +lemma "P \<longleftrightarrow> Q"
    8.24 +nitpick
    8.25 +apply auto
    8.26 +nitpick 1
    8.27 +nitpick 2
    8.28 +oops
    8.29 +
    8.30 +subsection {* 3.2. Type Variables *}
    8.31 +
    8.32 +lemma "P x \<Longrightarrow> P (THE y. P y)"
    8.33 +nitpick [verbose]
    8.34 +oops
    8.35 +
    8.36 +subsection {* 3.3. Constants *}
    8.37 +
    8.38 +lemma "P x \<Longrightarrow> P (THE y. P y)"
    8.39 +nitpick [show_consts]
    8.40 +nitpick [full_descrs, show_consts]
    8.41 +nitpick [dont_specialize, full_descrs, show_consts]
    8.42 +oops
    8.43 +
    8.44 +lemma "\<exists>!x. P x \<Longrightarrow> P (THE y. P y)"
    8.45 +nitpick
    8.46 +nitpick [card 'a = 1-50]
    8.47 +(* sledgehammer *)
    8.48 +apply (metis the_equality)
    8.49 +done
    8.50 +
    8.51 +subsection {* 3.4. Skolemization *}
    8.52 +
    8.53 +lemma "\<exists>g. \<forall>x. g (f x) = x \<Longrightarrow> \<forall>y. \<exists>x. y = f x"
    8.54 +nitpick
    8.55 +oops
    8.56 +
    8.57 +lemma "\<exists>x. \<forall>f. f x = x"
    8.58 +nitpick
    8.59 +oops
    8.60 +
    8.61 +lemma "refl r \<Longrightarrow> sym r"
    8.62 +nitpick
    8.63 +oops
    8.64 +
    8.65 +subsection {* 3.5. Numbers *}
    8.66 +
    8.67 +lemma "\<lbrakk>i \<le> j; n \<le> (m\<Colon>int)\<rbrakk> \<Longrightarrow> i * n + j * m \<le> i * m + j * n"
    8.68 +nitpick
    8.69 +oops
    8.70 +
    8.71 +lemma "\<forall>n. Suc n \<noteq> n \<Longrightarrow> P"
    8.72 +nitpick [card nat = 100, check_potential]
    8.73 +oops
    8.74 +
    8.75 +lemma "P Suc"
    8.76 +nitpick [card = 1-6]
    8.77 +oops
    8.78 +
    8.79 +lemma "P (op +\<Colon>nat\<Rightarrow>nat\<Rightarrow>nat)"
    8.80 +nitpick [card nat = 1]
    8.81 +nitpick [card nat = 2]
    8.82 +oops
    8.83 +
    8.84 +subsection {* 3.6. Inductive Datatypes *}
    8.85 +
    8.86 +lemma "hd (xs @ [y, y]) = hd xs"
    8.87 +nitpick
    8.88 +nitpick [show_consts, show_datatypes]
    8.89 +oops
    8.90 +
    8.91 +lemma "\<lbrakk>length xs = 1; length ys = 1\<rbrakk> \<Longrightarrow> xs = ys"
    8.92 +nitpick [show_datatypes]
    8.93 +oops
    8.94 +
    8.95 +subsection {* 3.7. Typedefs, Records, Rationals, and Reals *}
    8.96 +
    8.97 +typedef three = "{0\<Colon>nat, 1, 2}"
    8.98 +by blast
    8.99 +
   8.100 +definition A :: three where "A \<equiv> Abs_three 0"
   8.101 +definition B :: three where "B \<equiv> Abs_three 1"
   8.102 +definition C :: three where "C \<equiv> Abs_three 2"
   8.103 +
   8.104 +lemma "\<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P x"
   8.105 +nitpick [show_datatypes]
   8.106 +oops
   8.107 +
   8.108 +record point =
   8.109 +  Xcoord :: int
   8.110 +  Ycoord :: int
   8.111 +
   8.112 +lemma "Xcoord (p\<Colon>point) = Xcoord (q\<Colon>point)"
   8.113 +nitpick [show_datatypes]
   8.114 +oops
   8.115 +
   8.116 +lemma "4 * x + 3 * (y\<Colon>real) \<noteq> 1 / 2"
   8.117 +nitpick [show_datatypes]
   8.118 +oops
   8.119 +
   8.120 +subsection {* 3.8. Inductive and Coinductive Predicates *}
   8.121 +
   8.122 +inductive even where
   8.123 +"even 0" |
   8.124 +"even n \<Longrightarrow> even (Suc (Suc n))"
   8.125 +
   8.126 +lemma "\<exists>n. even n \<and> even (Suc n)"
   8.127 +nitpick [card nat = 100, verbose]
   8.128 +oops
   8.129 +
   8.130 +lemma "\<exists>n \<le> 99. even n \<and> even (Suc n)"
   8.131 +nitpick [card nat = 100]
   8.132 +oops
   8.133 +
   8.134 +inductive even' where
   8.135 +"even' (0\<Colon>nat)" |
   8.136 +"even' 2" |
   8.137 +"\<lbrakk>even' m; even' n\<rbrakk> \<Longrightarrow> even' (m + n)"
   8.138 +
   8.139 +lemma "\<exists>n \<in> {0, 2, 4, 6, 8}. \<not> even' n"
   8.140 +nitpick [card nat = 10, verbose, show_consts]
   8.141 +oops
   8.142 +
   8.143 +lemma "even' (n - 2) \<Longrightarrow> even' n"
   8.144 +nitpick [card nat = 10, show_consts]
   8.145 +oops
   8.146 +
   8.147 +coinductive nats where
   8.148 +"nats (x\<Colon>nat) \<Longrightarrow> nats x"
   8.149 +
   8.150 +lemma "nats = {0, 1, 2, 3, 4}"
   8.151 +nitpick [card nat = 10, show_consts]
   8.152 +oops
   8.153 +
   8.154 +inductive odd where
   8.155 +"odd 1" |
   8.156 +"\<lbrakk>odd m; even n\<rbrakk> \<Longrightarrow> odd (m + n)"
   8.157 +
   8.158 +lemma "odd n \<Longrightarrow> odd (n - 2)"
   8.159 +nitpick [card nat = 10, show_consts]
   8.160 +oops
   8.161 +
   8.162 +subsection {* 3.9. Coinductive Datatypes *}
   8.163 +
   8.164 +lemma "xs \<noteq> LCons a xs"
   8.165 +nitpick
   8.166 +oops
   8.167 +
   8.168 +lemma "\<lbrakk>xs = LCons a xs; ys = iterates (\<lambda>b. a) b\<rbrakk> \<Longrightarrow> xs = ys"
   8.169 +nitpick [verbose]
   8.170 +nitpick [bisim_depth = -1, verbose]
   8.171 +oops
   8.172 +
   8.173 +lemma "\<lbrakk>xs = LCons a xs; ys = LCons a ys\<rbrakk> \<Longrightarrow> xs = ys"
   8.174 +nitpick [bisim_depth = -1, show_datatypes]
   8.175 +nitpick
   8.176 +sorry
   8.177 +
   8.178 +subsection {* 3.10. Boxing *}
   8.179 +
   8.180 +datatype tm = Var nat | Lam tm | App tm tm
   8.181 +
   8.182 +primrec lift where
   8.183 +"lift (Var j) k = Var (if j < k then j else j + 1)" |
   8.184 +"lift (Lam t) k = Lam (lift t (k + 1))" |
   8.185 +"lift (App t u) k = App (lift t k) (lift u k)"
   8.186 +
   8.187 +primrec loose where
   8.188 +"loose (Var j) k = (j \<ge> k)" |
   8.189 +"loose (Lam t) k = loose t (Suc k)" |
   8.190 +"loose (App t u) k = (loose t k \<or> loose u k)"
   8.191 +
   8.192 +primrec subst\<^isub>1 where
   8.193 +"subst\<^isub>1 \<sigma> (Var j) = \<sigma> j" |
   8.194 +"subst\<^isub>1 \<sigma> (Lam t) =
   8.195 + Lam (subst\<^isub>1 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 1) t)" |
   8.196 +"subst\<^isub>1 \<sigma> (App t u) = App (subst\<^isub>1 \<sigma> t) (subst\<^isub>1 \<sigma> u)"
   8.197 +
   8.198 +lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>1 \<sigma> t = t"
   8.199 +nitpick [verbose]
   8.200 +nitpick [eval = "subst\<^isub>1 \<sigma> t"]
   8.201 +nitpick [dont_box]
   8.202 +oops
   8.203 +
   8.204 +primrec subst\<^isub>2 where
   8.205 +"subst\<^isub>2 \<sigma> (Var j) = \<sigma> j" |
   8.206 +"subst\<^isub>2 \<sigma> (Lam t) =
   8.207 + Lam (subst\<^isub>2 (\<lambda>n. case n of 0 \<Rightarrow> Var 0 | Suc m \<Rightarrow> lift (\<sigma> m) 0) t)" |
   8.208 +"subst\<^isub>2 \<sigma> (App t u) = App (subst\<^isub>2 \<sigma> t) (subst\<^isub>2 \<sigma> u)"
   8.209 +
   8.210 +lemma "\<not> loose t 0 \<Longrightarrow> subst\<^isub>2 \<sigma> t = t"
   8.211 +nitpick
   8.212 +sorry
   8.213 +
   8.214 +subsection {* 3.11. Scope Monotonicity *}
   8.215 +
   8.216 +lemma "length xs = length ys \<Longrightarrow> rev (zip xs ys) = zip xs (rev ys)"
   8.217 +nitpick [verbose]
   8.218 +nitpick [card = 8, verbose]
   8.219 +oops
   8.220 +
   8.221 +lemma "\<exists>g. \<forall>x\<Colon>'b. g (f x) = x \<Longrightarrow> \<forall>y\<Colon>'a. \<exists>x. y = f x"
   8.222 +nitpick [mono]
   8.223 +nitpick
   8.224 +oops
   8.225 +
   8.226 +section {* 4. Case Studies *}
   8.227 +
   8.228 +nitpick_params [max_potential = 0, max_threads = 2]
   8.229 +
   8.230 +subsection {* 4.1. A Context-Free Grammar *}
   8.231 +
   8.232 +datatype alphabet = a | b
   8.233 +
   8.234 +inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
   8.235 +  "[] \<in> S\<^isub>1"
   8.236 +| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
   8.237 +| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
   8.238 +| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
   8.239 +| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
   8.240 +| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
   8.241 +
   8.242 +theorem S\<^isub>1_sound:
   8.243 +"w \<in> S\<^isub>1 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   8.244 +nitpick
   8.245 +oops
   8.246 +
   8.247 +inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
   8.248 +  "[] \<in> S\<^isub>2"
   8.249 +| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
   8.250 +| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
   8.251 +| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
   8.252 +| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
   8.253 +| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
   8.254 +
   8.255 +theorem S\<^isub>2_sound:
   8.256 +"w \<in> S\<^isub>2 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   8.257 +nitpick
   8.258 +oops
   8.259 +
   8.260 +inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
   8.261 +  "[] \<in> S\<^isub>3"
   8.262 +| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
   8.263 +| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
   8.264 +| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
   8.265 +| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
   8.266 +| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
   8.267 +
   8.268 +theorem S\<^isub>3_sound:
   8.269 +"w \<in> S\<^isub>3 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   8.270 +nitpick
   8.271 +sorry
   8.272 +
   8.273 +theorem S\<^isub>3_complete:
   8.274 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>3"
   8.275 +nitpick
   8.276 +oops
   8.277 +
   8.278 +inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
   8.279 +  "[] \<in> S\<^isub>4"
   8.280 +| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
   8.281 +| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
   8.282 +| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
   8.283 +| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
   8.284 +| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
   8.285 +| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
   8.286 +
   8.287 +theorem S\<^isub>4_sound:
   8.288 +"w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   8.289 +nitpick
   8.290 +sorry
   8.291 +
   8.292 +theorem S\<^isub>4_complete:
   8.293 +"length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
   8.294 +nitpick
   8.295 +sorry
   8.296 +
   8.297 +theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
   8.298 +"w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
   8.299 +"w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
   8.300 +"w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
   8.301 +nitpick
   8.302 +sorry
   8.303 +
   8.304 +subsection {* 4.2. AA Trees *}
   8.305 +
   8.306 +datatype 'a tree = \<Lambda> | N "'a\<Colon>linorder" nat "'a tree" "'a tree"
   8.307 +
   8.308 +primrec data where
   8.309 +"data \<Lambda> = undefined" |
   8.310 +"data (N x _ _ _) = x"
   8.311 +
   8.312 +primrec dataset where
   8.313 +"dataset \<Lambda> = {}" |
   8.314 +"dataset (N x _ t u) = {x} \<union> dataset t \<union> dataset u"
   8.315 +
   8.316 +primrec level where
   8.317 +"level \<Lambda> = 0" |
   8.318 +"level (N _ k _ _) = k"
   8.319 +
   8.320 +primrec left where
   8.321 +"left \<Lambda> = \<Lambda>" |
   8.322 +"left (N _ _ t\<^isub>1 _) = t\<^isub>1"
   8.323 +
   8.324 +primrec right where
   8.325 +"right \<Lambda> = \<Lambda>" |
   8.326 +"right (N _ _ _ t\<^isub>2) = t\<^isub>2"
   8.327 +
   8.328 +fun wf where
   8.329 +"wf \<Lambda> = True" |
   8.330 +"wf (N _ k t u) =
   8.331 + (if t = \<Lambda> then
   8.332 +    k = 1 \<and> (u = \<Lambda> \<or> (level u = 1 \<and> left u = \<Lambda> \<and> right u = \<Lambda>))
   8.333 +  else
   8.334 +    wf t \<and> wf u \<and> u \<noteq> \<Lambda> \<and> level t < k \<and> level u \<le> k \<and> level (right u) < k)"
   8.335 +
   8.336 +fun skew where
   8.337 +"skew \<Lambda> = \<Lambda>" |
   8.338 +"skew (N x k t u) =
   8.339 + (if t \<noteq> \<Lambda> \<and> k = level t then
   8.340 +    N (data t) k (left t) (N x k (right t) u)
   8.341 +  else
   8.342 +    N x k t u)"
   8.343 +
   8.344 +fun split where
   8.345 +"split \<Lambda> = \<Lambda>" |
   8.346 +"split (N x k t u) =
   8.347 + (if u \<noteq> \<Lambda> \<and> k = level (right u) then
   8.348 +    N (data u) (Suc k) (N x k t (left u)) (right u)
   8.349 +  else
   8.350 +    N x k t u)"
   8.351 +
   8.352 +theorem dataset_skew_split:
   8.353 +"dataset (skew t) = dataset t"
   8.354 +"dataset (split t) = dataset t"
   8.355 +nitpick
   8.356 +sorry
   8.357 +
   8.358 +theorem wf_skew_split:
   8.359 +"wf t \<Longrightarrow> skew t = t"
   8.360 +"wf t \<Longrightarrow> split t = t"
   8.361 +nitpick
   8.362 +sorry
   8.363 +
   8.364 +primrec insort\<^isub>1 where
   8.365 +"insort\<^isub>1 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
   8.366 +"insort\<^isub>1 (N y k t u) x =
   8.367 + (* (split \<circ> skew) *) (N y k (if x < y then insort\<^isub>1 t x else t)
   8.368 +                             (if x > y then insort\<^isub>1 u x else u))"
   8.369 +
   8.370 +theorem wf_insort\<^isub>1: "wf t \<Longrightarrow> wf (insort\<^isub>1 t x)"
   8.371 +nitpick
   8.372 +oops
   8.373 +
   8.374 +theorem wf_insort\<^isub>1_nat: "wf t \<Longrightarrow> wf (insort\<^isub>1 t (x\<Colon>nat))"
   8.375 +nitpick [eval = "insort\<^isub>1 t x"]
   8.376 +oops
   8.377 +
   8.378 +primrec insort\<^isub>2 where
   8.379 +"insort\<^isub>2 \<Lambda> x = N x 1 \<Lambda> \<Lambda>" |
   8.380 +"insort\<^isub>2 (N y k t u) x =
   8.381 + (split \<circ> skew) (N y k (if x < y then insort\<^isub>2 t x else t)
   8.382 +                       (if x > y then insort\<^isub>2 u x else u))"
   8.383 +
   8.384 +theorem wf_insort\<^isub>2: "wf t \<Longrightarrow> wf (insort\<^isub>2 t x)"
   8.385 +nitpick
   8.386 +sorry
   8.387 +
   8.388 +theorem dataset_insort\<^isub>2: "dataset (insort\<^isub>2 t x) = {x} \<union> dataset t"
   8.389 +nitpick
   8.390 +sorry
   8.391 +
   8.392 +end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Nitpick_Examples/Mini_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
     9.3 @@ -0,0 +1,107 @@
     9.4 +(*  Title:      HOL/Nitpick_Examples/Mini_Nits.thy
     9.5 +    Author:     Jasmin Blanchette, TU Muenchen
     9.6 +    Copyright   2009
     9.7 +
     9.8 +Examples featuring Minipick, the minimalistic version of Nitpick.
     9.9 +*)
    9.10 +
    9.11 +header {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *}
    9.12 +
    9.13 +theory Mini_Nits
    9.14 +imports Main
    9.15 +begin
    9.16 +
    9.17 +ML {*
    9.18 +exception FAIL
    9.19 +
    9.20 +(* int -> term -> string *)
    9.21 +fun minipick 0 _ = "none"
    9.22 +  | minipick n t =
    9.23 +    case minipick (n - 1) t of
    9.24 +      "none" => Minipick.pick_nits_in_term @{context} (K n) t
    9.25 +    | outcome_code => outcome_code
    9.26 +(* int -> term -> bool *)
    9.27 +fun none n t = (minipick n t = "none" orelse raise FAIL)
    9.28 +fun genuine n t = (minipick n t = "genuine" orelse raise FAIL)
    9.29 +fun unknown n t = (minipick n t = "unknown" orelse raise FAIL)
    9.30 +*}
    9.31 +
    9.32 +ML {* minipick 1 @{prop "\<forall>x\<Colon>'a. \<exists>y\<Colon>'b. f x = y"} *}
    9.33 +
    9.34 +ML {* genuine 1 @{prop "x = Not"} *}
    9.35 +ML {* none 1 @{prop "\<exists>x. x = Not"} *}
    9.36 +ML {* none 1 @{prop "\<not> False"} *}
    9.37 +ML {* genuine 1 @{prop "\<not> True"} *}
    9.38 +ML {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
    9.39 +ML {* none 1 @{prop True} *}
    9.40 +ML {* genuine 1 @{prop False} *}
    9.41 +ML {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
    9.42 +ML {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
    9.43 +ML {* none 5 @{prop "\<forall>x. x = x"} *}
    9.44 +ML {* none 5 @{prop "\<exists>x. x = x"} *}
    9.45 +ML {* none 1 @{prop "\<forall>x. x = y"} *}
    9.46 +ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
    9.47 +ML {* none 1 @{prop "\<exists>x. x = y"} *}
    9.48 +ML {* none 2 @{prop "\<exists>x. x = y"} *}
    9.49 +ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
    9.50 +ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
    9.51 +ML {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
    9.52 +ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
    9.53 +ML {* none 1 @{prop "All = Ex"} *}
    9.54 +ML {* genuine 2 @{prop "All = Ex"} *}
    9.55 +ML {* none 1 @{prop "All P = Ex P"} *}
    9.56 +ML {* genuine 2 @{prop "All P = Ex P"} *}
    9.57 +ML {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
    9.58 +ML {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
    9.59 +ML {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
    9.60 +ML {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
    9.61 +ML {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
    9.62 +ML {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
    9.63 +ML {* genuine 1 @{prop "(op =) X = Ex"} *}
    9.64 +ML {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
    9.65 +ML {* none 1 @{prop "x = y"} *}
    9.66 +ML {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
    9.67 +ML {* genuine 2 @{prop "x = y"} *}
    9.68 +ML {* genuine 1 @{prop "X \<subseteq> Y"} *}
    9.69 +ML {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
    9.70 +ML {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
    9.71 +ML {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
    9.72 +ML {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
    9.73 +ML {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
    9.74 +ML {* none 5 @{prop "{a} = {a, a}"} *}
    9.75 +ML {* genuine 2 @{prop "{a} = {a, b}"} *}
    9.76 +ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
    9.77 +ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
    9.78 +ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    9.79 +ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    9.80 +ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    9.81 +ML {* none 5 @{prop "A \<union> B = (\<lambda>x. A x \<or> B x)"} *}
    9.82 +ML {* none 5 @{prop "A \<inter> B = (\<lambda>x. A x \<and> B x)"} *}
    9.83 +ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
    9.84 +ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
    9.85 +ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
    9.86 +ML {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
    9.87 +ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
    9.88 +ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
    9.89 +ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
    9.90 +ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
    9.91 +ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
    9.92 +ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
    9.93 +ML {* none 8 @{prop "fst (a, b) = a"} *}
    9.94 +ML {* none 1 @{prop "fst (a, b) = b"} *}
    9.95 +ML {* genuine 2 @{prop "fst (a, b) = b"} *}
    9.96 +ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
    9.97 +ML {* none 8 @{prop "snd (a, b) = b"} *}
    9.98 +ML {* none 1 @{prop "snd (a, b) = a"} *}
    9.99 +ML {* genuine 2 @{prop "snd (a, b) = a"} *}
   9.100 +ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
   9.101 +ML {* genuine 1 @{prop P} *}
   9.102 +ML {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
   9.103 +ML {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
   9.104 +ML {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
   9.105 +ML {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
   9.106 +ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
   9.107 +ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
   9.108 +ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
   9.109 +
   9.110 +end
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
    10.3 @@ -0,0 +1,98 @@
    10.4 +(*  Title:      HOL/Nitpick_Examples/Mono_Nits.thy
    10.5 +    Author:     Jasmin Blanchette, TU Muenchen
    10.6 +    Copyright   2009
    10.7 +
    10.8 +Examples featuring Nitpick's monotonicity check.
    10.9 +*)
   10.10 +
   10.11 +header {* Examples Featuring Nitpick's Monotonicity Check *}
   10.12 +
   10.13 +theory Mono_Nits
   10.14 +imports Main
   10.15 +begin
   10.16 +
   10.17 +ML {*
   10.18 +exception FAIL
   10.19 +
   10.20 +val defs = NitpickHOL.all_axioms_of @{theory} |> #1
   10.21 +val def_table = NitpickHOL.const_def_table @{context} defs
   10.22 +val ext_ctxt =
   10.23 +  {thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
   10.24 +   user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false,
   10.25 +   specialize = false, skolemize = false, star_linear_preds = false,
   10.26 +   uncurry = false, fast_descrs = false, tac_timeout = NONE, evals = [],
   10.27 +   case_names = [], def_table = def_table, nondef_table = Symtab.empty,
   10.28 +   user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty,
   10.29 +   psimp_table = Symtab.empty, intro_table = Symtab.empty,
   10.30 +   ground_thm_table = Inttab.empty, ersatz_table = [],
   10.31 +   skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
   10.32 +   unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref []}
   10.33 +(* term -> bool *)
   10.34 +val is_mono = NitpickMono.formulas_monotonic ext_ctxt @{typ 'a} [] []
   10.35 +fun is_const t =
   10.36 +  let val T = fastype_of t in
   10.37 +    is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
   10.38 +                               @{const False}))
   10.39 +  end
   10.40 +fun mono t = is_mono t orelse raise FAIL
   10.41 +fun nonmono t = not (is_mono t) orelse raise FAIL
   10.42 +fun const t = is_const t orelse raise FAIL
   10.43 +fun nonconst t = not (is_const t) orelse raise FAIL
   10.44 +*}
   10.45 +
   10.46 +ML {* const @{term "A::('a\<Rightarrow>'b)"} *}
   10.47 +ML {* const @{term "(A::'a set) = A"} *}
   10.48 +ML {* const @{term "(A::'a set set) = A"} *}
   10.49 +ML {* const @{term "(\<lambda>x::'a set. x a)"} *}
   10.50 +ML {* const @{term "{{a}} = C"} *}
   10.51 +ML {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *}
   10.52 +ML {* const @{term "A \<union> B"} *}
   10.53 +ML {* const @{term "P (a::'a)"} *}
   10.54 +ML {* const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *}
   10.55 +ML {* const @{term "\<forall>A::'a set. A a"} *}
   10.56 +ML {* const @{term "\<forall>A::'a set. P A"} *}
   10.57 +ML {* const @{term "P \<or> Q"} *}
   10.58 +ML {* const @{term "A \<union> B = C"} *}
   10.59 +ML {* const @{term "(if P then (A::'a set) else B) = C"} *}
   10.60 +ML {* const @{term "let A = C in A \<union> B"} *}
   10.61 +ML {* const @{term "THE x::'b. P x"} *}
   10.62 +ML {* const @{term "{}::'a set"} *}
   10.63 +ML {* const @{term "(\<lambda>x::'a. True)"} *}
   10.64 +ML {* const @{term "Let a A"} *}
   10.65 +ML {* const @{term "A (a::'a)"} *}
   10.66 +ML {* const @{term "insert a A = B"} *}
   10.67 +ML {* const @{term "- (A::'a set)"} *}
   10.68 +ML {* const @{term "finite A"} *}
   10.69 +ML {* const @{term "\<not> finite A"} *}
   10.70 +ML {* const @{term "finite (A::'a set set)"} *}
   10.71 +ML {* const @{term "\<lambda>a::'a. A a \<and> \<not> B a"} *}
   10.72 +ML {* const @{term "A < (B::'a set)"} *}
   10.73 +ML {* const @{term "A \<le> (B::'a set)"} *}
   10.74 +ML {* const @{term "[a::'a]"} *}
   10.75 +ML {* const @{term "[a::'a set]"} *}
   10.76 +ML {* const @{term "[A \<union> (B::'a set)]"} *}
   10.77 +ML {* const @{term "[A \<union> (B::'a set)] = [C]"} *}
   10.78 +ML {* const @{term "\<forall>P. P a"} *}
   10.79 +
   10.80 +ML {* nonconst @{term "{%x. True}"} *}
   10.81 +ML {* nonconst @{term "{(%x. x = a)} = C"} *}
   10.82 +ML {* nonconst @{term "\<forall>P (a::'a). P a"} *}
   10.83 +ML {* nonconst @{term "\<forall>a::'a. P a"} *}
   10.84 +ML {* nonconst @{term "(\<lambda>a::'a. \<not> A a) = B"} *}
   10.85 +ML {* nonconst @{term "THE x. P x"} *}
   10.86 +ML {* nonconst @{term "SOME x. P x"} *}
   10.87 +
   10.88 +ML {* mono @{prop "Q (\<forall>x::'a set. P x)"} *}
   10.89 +ML {* mono @{prop "P (a::'a)"} *}
   10.90 +ML {* mono @{prop "{a} = {b}"} *}
   10.91 +ML {* mono @{prop "P (a::'a) \<and> P \<union> P = P"} *}
   10.92 +ML {* mono @{prop "\<forall>F::'a set set. P"} *}
   10.93 +ML {* mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h)"} *}
   10.94 +ML {* mono @{prop "\<not> Q (\<forall>x::'a set. P x)"} *}
   10.95 +ML {* mono @{prop "\<not> (\<forall>x. P x)"} *}
   10.96 +
   10.97 +ML {* nonmono @{prop "\<forall>x. P x"} *}
   10.98 +ML {* nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
   10.99 +ML {* nonmono @{prop "myall P = (P = (\<lambda>x. True))"} *}
  10.100 +
  10.101 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Nitpick_Examples/Nitpick_Examples.thy	Fri Oct 23 18:59:24 2009 +0200
    11.3 @@ -0,0 +1,14 @@
    11.4 +(*  Title:      HOL/Nitpick_Examples/Nitpick_Examples.thy
    11.5 +    Author:     Jasmin Blanchette, TU Muenchen
    11.6 +    Copyright   2009
    11.7 +
    11.8 +Nitpick examples.
    11.9 +*)
   11.10 +
   11.11 +theory Nitpick_Examples
   11.12 +imports Core_Nits Datatype_Nits Induct_Nits Manual_Nits Mini_Nits Mono_Nits
   11.13 +        Pattern_Nits Record_Nits Refute_Nits Special_Nits Tests_Nits
   11.14 +        Typedef_Nits
   11.15 +begin
   11.16 +
   11.17 +end
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Nitpick_Examples/Pattern_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
    12.3 @@ -0,0 +1,138 @@
    12.4 +(*  Title:      HOL/Nitpick_Examples/Pattern_Nits.thy
    12.5 +    Author:     Jasmin Blanchette, TU Muenchen
    12.6 +    Copyright   2009
    12.7 +
    12.8 +Examples featuring Nitpick's "destroy_constrs" optimization.
    12.9 +*)
   12.10 +
   12.11 +header {* Examples Featuring Nitpick's \textit{destroy\_constrs} Optimization *}
   12.12 +
   12.13 +theory Pattern_Nits
   12.14 +imports Main
   12.15 +begin
   12.16 +
   12.17 +nitpick_params [card = 14]
   12.18 +
   12.19 +lemma "x = (case u of () \<Rightarrow> y)"
   12.20 +nitpick [expect = genuine]
   12.21 +oops
   12.22 +
   12.23 +lemma "x = (case b of True \<Rightarrow> x | False \<Rightarrow> y)"
   12.24 +nitpick [expect = genuine]
   12.25 +oops
   12.26 +
   12.27 +lemma "x = (case p of (x, y) \<Rightarrow> y)"
   12.28 +nitpick [expect = genuine]
   12.29 +oops
   12.30 +
   12.31 +lemma "x = (case n of 0 \<Rightarrow> x | Suc n \<Rightarrow> n)"
   12.32 +nitpick [expect = genuine]
   12.33 +oops
   12.34 +
   12.35 +lemma "x = (case opt of None \<Rightarrow> x | Some y \<Rightarrow> y)"
   12.36 +nitpick [expect = genuine]
   12.37 +oops
   12.38 +
   12.39 +lemma "x = (case xs of [] \<Rightarrow> x | y # ys \<Rightarrow> y)"
   12.40 +nitpick [expect = genuine]
   12.41 +oops
   12.42 +
   12.43 +lemma "x = (case xs of
   12.44 +              [] \<Rightarrow> x
   12.45 +            | y # ys \<Rightarrow>
   12.46 +              (case ys of
   12.47 +                 [] \<Rightarrow> x
   12.48 +               | z # zs \<Rightarrow>
   12.49 +                 (case z of
   12.50 +                    None \<Rightarrow> x
   12.51 +                  | Some p \<Rightarrow>
   12.52 +                    (case p of
   12.53 +                       (a, b) \<Rightarrow> b))))"
   12.54 +nitpick [expect = genuine]
   12.55 +oops
   12.56 +
   12.57 +fun f1 where
   12.58 +"f1 x () = x"
   12.59 +
   12.60 +lemma "x = f1 y u"
   12.61 +nitpick [expect = genuine]
   12.62 +oops
   12.63 +
   12.64 +fun f2 where
   12.65 +"f2 x _ True = x" |
   12.66 +"f2 _ y False = y"
   12.67 +
   12.68 +lemma "x = f2 x y b"
   12.69 +nitpick [expect = genuine]
   12.70 +oops
   12.71 +
   12.72 +fun f3 where
   12.73 +"f3 (_, y) = y"
   12.74 +
   12.75 +lemma "x = f3 p"
   12.76 +nitpick [expect = genuine]
   12.77 +oops
   12.78 +
   12.79 +fun f4 where
   12.80 +"f4 x 0 = x" |
   12.81 +"f4 _ (Suc n) = n"
   12.82 +
   12.83 +lemma "x = f4 x n"
   12.84 +nitpick [expect = genuine]
   12.85 +oops
   12.86 +
   12.87 +fun f5 where
   12.88 +"f5 x None = x" |
   12.89 +"f5 _ (Some y) = y"
   12.90 +
   12.91 +lemma "x = f5 x opt"
   12.92 +nitpick [expect = genuine]
   12.93 +oops
   12.94 +
   12.95 +fun f6 where
   12.96 +"f6 x [] = x" |
   12.97 +"f6 _ (y # ys) = y"
   12.98 +
   12.99 +lemma "x = f6 x xs"
  12.100 +nitpick [expect = genuine]
  12.101 +oops
  12.102 +
  12.103 +fun f7 where
  12.104 +"f7 _ (y # Some (a, b) # zs) = b" |
  12.105 +"f7 x (y # None # zs) = x" |
  12.106 +"f7 x [y] = x" |
  12.107 +"f7 x [] = x"
  12.108 +
  12.109 +lemma "x = f7 x xs"
  12.110 +nitpick [expect = genuine]
  12.111 +oops
  12.112 +
  12.113 +lemma "u = ()"
  12.114 +nitpick [expect = none]
  12.115 +sorry
  12.116 +
  12.117 +lemma "\<exists>y. (b::bool) = y"
  12.118 +nitpick [expect = none]
  12.119 +sorry
  12.120 +
  12.121 +lemma "\<exists>x y. p = (x, y)"
  12.122 +nitpick [expect = none]
  12.123 +sorry
  12.124 +
  12.125 +lemma "\<exists>x. n = Suc x"
  12.126 +nitpick [expect = genuine]
  12.127 +oops
  12.128 +
  12.129 +lemma "\<exists>y. x = Some y"
  12.130 +nitpick [expect = genuine]
  12.131 +oops
  12.132 +
  12.133 +lemma "\<exists>y ys. xs = y # ys"
  12.134 +nitpick [expect = genuine]
  12.135 +oops
  12.136 +
  12.137 +lemma "\<exists>y a b zs. x = (y # Some (a, b) # zs)"
  12.138 +nitpick [expect = genuine]
  12.139 +oops
  12.140 +
  12.141 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Nitpick_Examples/ROOT.ML	Fri Oct 23 18:59:24 2009 +0200
    13.3 @@ -0,0 +1,8 @@
    13.4 +(*  Title:      HOL/Nitpick_Examples/ROOT.ML
    13.5 +    Author:     Jasmin Blanchette, TU Muenchen
    13.6 +    Copyright   2009
    13.7 +
    13.8 +Nitpick examples.
    13.9 +*)
   13.10 +
   13.11 +setmp_noncritical quick_and_dirty true (try use_thy) "Nitpick_Examples";
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Nitpick_Examples/Record_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
    14.3 @@ -0,0 +1,84 @@
    14.4 +(*  Title:      HOL/Nitpick_Examples/Record_Nits.thy
    14.5 +    Author:     Jasmin Blanchette, TU Muenchen
    14.6 +    Copyright   2009
    14.7 +
    14.8 +Examples featuring Nitpick applied to records.
    14.9 +*)
   14.10 +
   14.11 +header {* Examples Featuring Nitpick Applied to Records *}
   14.12 +
   14.13 +theory Record_Nits
   14.14 +imports Main
   14.15 +begin
   14.16 +
   14.17 +record point2d =
   14.18 +  xc :: int
   14.19 +  yc :: int
   14.20 +
   14.21 +lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x, yc := y\<rparr>"
   14.22 +nitpick [expect = none]
   14.23 +sorry
   14.24 +
   14.25 +lemma "\<lparr>xc = x, yc = y\<rparr> = p\<lparr>xc := x\<rparr>"
   14.26 +nitpick [expect = genuine]
   14.27 +oops
   14.28 +
   14.29 +lemma "p\<lparr>xc := x, yc := y\<rparr> \<noteq> p"
   14.30 +nitpick [expect = genuine]
   14.31 +oops
   14.32 +
   14.33 +lemma "p\<lparr>xc := x, yc := y\<rparr> = p"
   14.34 +nitpick [expect = genuine]
   14.35 +oops
   14.36 +
   14.37 +record point3d = point2d +
   14.38 +  zc :: int
   14.39 +
   14.40 +lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x, yc := y, zc := z\<rparr>"
   14.41 +nitpick [expect = none]
   14.42 +sorry
   14.43 +
   14.44 +lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>xc := x\<rparr>"
   14.45 +nitpick [expect = genuine]
   14.46 +oops
   14.47 +
   14.48 +lemma "\<lparr>xc = x, yc = y, zc = z\<rparr> = p\<lparr>zc := z\<rparr>"
   14.49 +nitpick [expect = genuine]
   14.50 +oops
   14.51 +
   14.52 +lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> \<noteq> p"
   14.53 +nitpick [expect = genuine]
   14.54 +oops
   14.55 +
   14.56 +lemma "p\<lparr>xc := x, yc := y, zc := z\<rparr> = p"
   14.57 +nitpick [expect = genuine]
   14.58 +oops
   14.59 +
   14.60 +record point4d = point3d +
   14.61 +  wc :: int
   14.62 +
   14.63 +lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr>"
   14.64 +nitpick [expect = none]
   14.65 +sorry
   14.66 +
   14.67 +lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>xc := x\<rparr>"
   14.68 +nitpick [expect = genuine]
   14.69 +oops
   14.70 +
   14.71 +lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>zc := z\<rparr>"
   14.72 +nitpick [expect = genuine]
   14.73 +oops
   14.74 +
   14.75 +lemma "\<lparr>xc = x, yc = y, zc = z, wc = w\<rparr> = p\<lparr>wc := w\<rparr>"
   14.76 +nitpick [expect = genuine]
   14.77 +oops
   14.78 +
   14.79 +lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> \<noteq> p"
   14.80 +nitpick [expect = genuine]
   14.81 +oops
   14.82 +
   14.83 +lemma "p\<lparr>xc := x, yc := y, zc := z, wc := w\<rparr> = p"
   14.84 +nitpick [expect = genuine]
   14.85 +oops
   14.86 +
   14.87 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
    15.3 @@ -0,0 +1,1476 @@
    15.4 +(*  Title:      HOL/Nitpick_Examples/Refute_Nits.thy
    15.5 +    Author:     Jasmin Blanchette, TU Muenchen
    15.6 +    Copyright   2009
    15.7 +
    15.8 +Refute examples adapted to Nitpick.
    15.9 +*)
   15.10 +
   15.11 +header {* Refute Examples Adapted to Nitpick *}
   15.12 +
   15.13 +theory Refute_Nits
   15.14 +imports Main
   15.15 +begin
   15.16 +
   15.17 +lemma "P \<and> Q"
   15.18 +apply (rule conjI)
   15.19 +nitpick [expect = genuine] 1
   15.20 +nitpick [expect = genuine] 2
   15.21 +nitpick [expect = genuine]
   15.22 +nitpick [card = 5, expect = genuine]
   15.23 +nitpick [sat_solver = MiniSat, expect = genuine] 2
   15.24 +oops
   15.25 +
   15.26 +subsection {* Examples and Test Cases *}
   15.27 +
   15.28 +subsubsection {* Propositional logic *}
   15.29 +
   15.30 +lemma "True"
   15.31 +nitpick [expect = none]
   15.32 +apply auto
   15.33 +done
   15.34 +
   15.35 +lemma "False"
   15.36 +nitpick [expect = genuine]
   15.37 +oops
   15.38 +
   15.39 +lemma "P"
   15.40 +nitpick [expect = genuine]
   15.41 +oops
   15.42 +
   15.43 +lemma "\<not> P"
   15.44 +nitpick [expect = genuine]
   15.45 +oops
   15.46 +
   15.47 +lemma "P \<and> Q"
   15.48 +nitpick [expect = genuine]
   15.49 +oops
   15.50 +
   15.51 +lemma "P \<or> Q"
   15.52 +nitpick [expect = genuine]
   15.53 +oops
   15.54 +
   15.55 +lemma "P \<longrightarrow> Q"
   15.56 +nitpick [expect = genuine]
   15.57 +oops
   15.58 +
   15.59 +lemma "(P\<Colon>bool) = Q"
   15.60 +nitpick [expect = genuine]
   15.61 +oops
   15.62 +
   15.63 +lemma "(P \<or> Q) \<longrightarrow> (P \<and> Q)"
   15.64 +nitpick [expect = genuine]
   15.65 +oops
   15.66 +
   15.67 +subsubsection {* Predicate logic *}
   15.68 +
   15.69 +lemma "P x y z"
   15.70 +nitpick [expect = genuine]
   15.71 +oops
   15.72 +
   15.73 +lemma "P x y \<longrightarrow> P y x"
   15.74 +nitpick [expect = genuine]
   15.75 +oops
   15.76 +
   15.77 +lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
   15.78 +nitpick [expect = genuine]
   15.79 +oops
   15.80 +
   15.81 +subsubsection {* Equality *}
   15.82 +
   15.83 +lemma "P = True"
   15.84 +nitpick [expect = genuine]
   15.85 +oops
   15.86 +
   15.87 +lemma "P = False"
   15.88 +nitpick [expect = genuine]
   15.89 +oops
   15.90 +
   15.91 +lemma "x = y"
   15.92 +nitpick [expect = genuine]
   15.93 +oops
   15.94 +
   15.95 +lemma "f x = g x"
   15.96 +nitpick [expect = genuine]
   15.97 +oops
   15.98 +
   15.99 +lemma "(f\<Colon>'a\<Rightarrow>'b) = g"
  15.100 +nitpick [expect = genuine]
  15.101 +oops
  15.102 +
  15.103 +lemma "(f\<Colon>('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
  15.104 +nitpick [expect = genuine]
  15.105 +oops
  15.106 +
  15.107 +lemma "distinct [a, b]"
  15.108 +nitpick [expect = genuine]
  15.109 +apply simp
  15.110 +nitpick [expect = genuine]
  15.111 +oops
  15.112 +
  15.113 +subsubsection {* First-Order Logic *}
  15.114 +
  15.115 +lemma "\<exists>x. P x"
  15.116 +nitpick [expect = genuine]
  15.117 +oops
  15.118 +
  15.119 +lemma "\<forall>x. P x"
  15.120 +nitpick [expect = genuine]
  15.121 +oops
  15.122 +
  15.123 +lemma "\<exists>!x. P x"
  15.124 +nitpick [expect = genuine]
  15.125 +oops
  15.126 +
  15.127 +lemma "Ex P"
  15.128 +nitpick [expect = genuine]
  15.129 +oops
  15.130 +
  15.131 +lemma "All P"
  15.132 +nitpick [expect = genuine]
  15.133 +oops
  15.134 +
  15.135 +lemma "Ex1 P"
  15.136 +nitpick [expect = genuine]
  15.137 +oops
  15.138 +
  15.139 +lemma "(\<exists>x. P x) \<longrightarrow> (\<forall>x. P x)"
  15.140 +nitpick [expect = genuine]
  15.141 +oops
  15.142 +
  15.143 +lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"
  15.144 +nitpick [expect = genuine]
  15.145 +oops
  15.146 +
  15.147 +lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
  15.148 +nitpick [expect = genuine]
  15.149 +oops
  15.150 +
  15.151 +text {* A true statement (also testing names of free and bound variables being identical) *}
  15.152 +
  15.153 +lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
  15.154 +nitpick [expect = none]
  15.155 +apply fast
  15.156 +done
  15.157 +
  15.158 +text {* "A type has at most 4 elements." *}
  15.159 +
  15.160 +lemma "\<not> distinct [a, b, c, d, e]"
  15.161 +nitpick [expect = genuine]
  15.162 +apply simp
  15.163 +nitpick [expect = genuine]
  15.164 +oops
  15.165 +
  15.166 +lemma "distinct [a, b, c, d]"
  15.167 +nitpick [expect = genuine]
  15.168 +apply simp
  15.169 +nitpick [expect = genuine]
  15.170 +oops
  15.171 +
  15.172 +text {* "Every reflexive and symmetric relation is transitive." *}
  15.173 +
  15.174 +lemma "\<lbrakk>\<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x\<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z"
  15.175 +nitpick [expect = genuine]
  15.176 +oops
  15.177 +
  15.178 +text {* The "Drinker's theorem" ... *}
  15.179 +
  15.180 +lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
  15.181 +nitpick [expect = none]
  15.182 +apply (auto simp add: ext)
  15.183 +done
  15.184 +
  15.185 +text {* ... and an incorrect version of it *}
  15.186 +
  15.187 +lemma "(\<exists>x. f x = g x) \<longrightarrow> f = g"
  15.188 +nitpick [expect = genuine]
  15.189 +oops
  15.190 +
  15.191 +text {* "Every function has a fixed point." *}
  15.192 +
  15.193 +lemma "\<exists>x. f x = x"
  15.194 +nitpick [expect = genuine]
  15.195 +oops
  15.196 +
  15.197 +text {* "Function composition is commutative." *}
  15.198 +
  15.199 +lemma "f (g x) = g (f x)"
  15.200 +nitpick [expect = genuine]
  15.201 +oops
  15.202 +
  15.203 +text {* "Two functions that are equivalent wrt.\ the same predicate 'P' are equal." *}
  15.204 +
  15.205 +lemma "((P\<Colon>('a\<Rightarrow>'b)\<Rightarrow>bool) f = P g) \<longrightarrow> (f x = g x)"
  15.206 +nitpick [expect = genuine]
  15.207 +oops
  15.208 +
  15.209 +subsubsection {* Higher-Order Logic *}
  15.210 +
  15.211 +lemma "\<exists>P. P"
  15.212 +nitpick [expect = none]
  15.213 +apply auto
  15.214 +done
  15.215 +
  15.216 +lemma "\<forall>P. P"
  15.217 +nitpick [expect = genuine]
  15.218 +oops
  15.219 +
  15.220 +lemma "\<exists>!P. P"
  15.221 +nitpick [expect = none]
  15.222 +apply auto
  15.223 +done
  15.224 +
  15.225 +lemma "\<exists>!P. P x"
  15.226 +nitpick [expect = genuine]
  15.227 +oops
  15.228 +
  15.229 +lemma "P Q \<or> Q x"
  15.230 +nitpick [expect = genuine]
  15.231 +oops
  15.232 +
  15.233 +lemma "x \<noteq> All"
  15.234 +nitpick [expect = genuine]
  15.235 +oops
  15.236 +
  15.237 +lemma "x \<noteq> Ex"
  15.238 +nitpick [expect = genuine]
  15.239 +oops
  15.240 +
  15.241 +lemma "x \<noteq> Ex1"
  15.242 +nitpick [expect = genuine]
  15.243 +oops
  15.244 +
  15.245 +text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
  15.246 +
  15.247 +constdefs
  15.248 +"trans" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
  15.249 +"trans P \<equiv> (ALL x y z. P x y \<longrightarrow> P y z \<longrightarrow> P x z)"
  15.250 +"subset" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
  15.251 +"subset P Q \<equiv> (ALL x y. P x y \<longrightarrow> Q x y)"
  15.252 +"trans_closure" :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
  15.253 +"trans_closure P Q \<equiv> (subset Q P) \<and> (trans P) \<and> (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
  15.254 +
  15.255 +lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
  15.256 +nitpick [expect = genuine]
  15.257 +oops
  15.258 +
  15.259 +text {* "The union of transitive closures is equal to the transitive closure of unions." *}
  15.260 +
  15.261 +lemma "(\<forall>x y. (P x y \<or> R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y \<or> R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
  15.262 + \<longrightarrow> trans_closure TP P
  15.263 + \<longrightarrow> trans_closure TR R
  15.264 + \<longrightarrow> (T x y = (TP x y \<or> TR x y))"
  15.265 +nitpick [expect = genuine]
  15.266 +oops
  15.267 +
  15.268 +text {* "Every surjective function is invertible." *}
  15.269 +
  15.270 +lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"
  15.271 +nitpick [expect = genuine]
  15.272 +oops
  15.273 +
  15.274 +text {* "Every invertible function is surjective." *}
  15.275 +
  15.276 +lemma "(\<exists>g. \<forall>x. g (f x) = x) \<longrightarrow> (\<forall>y. \<exists>x. y = f x)"
  15.277 +nitpick [expect = genuine]
  15.278 +oops
  15.279 +
  15.280 +text {* Every point is a fixed point of some function. *}
  15.281 +
  15.282 +lemma "\<exists>f. f x = x"
  15.283 +nitpick [card = 1\<midarrow>7, expect = none]
  15.284 +apply (rule_tac x = "\<lambda>x. x" in exI)
  15.285 +apply simp
  15.286 +done
  15.287 +
  15.288 +text {* Axiom of Choice: first an incorrect version ... *}
  15.289 +
  15.290 +lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
  15.291 +nitpick [expect = genuine]
  15.292 +oops
  15.293 +
  15.294 +text {* ... and now two correct ones *}
  15.295 +
  15.296 +lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
  15.297 +nitpick [card = 1-5, expect = none]
  15.298 +apply (simp add: choice)
  15.299 +done
  15.300 +
  15.301 +lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
  15.302 +nitpick [card = 1-4, expect = none]
  15.303 +apply auto
  15.304 + apply (simp add: ex1_implies_ex choice)
  15.305 +apply (fast intro: ext)
  15.306 +done
  15.307 +
  15.308 +subsubsection {* Metalogic *}
  15.309 +
  15.310 +lemma "\<And>x. P x"
  15.311 +nitpick [expect = genuine]
  15.312 +oops
  15.313 +
  15.314 +lemma "f x \<equiv> g x"
  15.315 +nitpick [expect = genuine]
  15.316 +oops
  15.317 +
  15.318 +lemma "P \<Longrightarrow> Q"
  15.319 +nitpick [expect = genuine]
  15.320 +oops
  15.321 +
  15.322 +lemma "\<lbrakk>P; Q; R\<rbrakk> \<Longrightarrow> S"
  15.323 +nitpick [expect = genuine]
  15.324 +oops
  15.325 +
  15.326 +lemma "(x \<equiv> all) \<Longrightarrow> False"
  15.327 +nitpick [expect = genuine]
  15.328 +oops
  15.329 +
  15.330 +lemma "(x \<equiv> (op \<equiv>)) \<Longrightarrow> False"
  15.331 +nitpick [expect = genuine]
  15.332 +oops
  15.333 +
  15.334 +lemma "(x \<equiv> (op \<Longrightarrow>)) \<Longrightarrow> False"
  15.335 +nitpick [expect = genuine]
  15.336 +oops
  15.337 +
  15.338 +subsubsection {* Schematic Variables *}
  15.339 +
  15.340 +lemma "?P"
  15.341 +nitpick [expect = none]
  15.342 +apply auto
  15.343 +done
  15.344 +
  15.345 +lemma "x = ?y"
  15.346 +nitpick [expect = none]
  15.347 +apply auto
  15.348 +done
  15.349 +
  15.350 +subsubsection {* Abstractions *}
  15.351 +
  15.352 +lemma "(\<lambda>x. x) = (\<lambda>x. y)"
  15.353 +nitpick [expect = genuine]
  15.354 +oops
  15.355 +
  15.356 +lemma "(\<lambda>f. f x) = (\<lambda>f. True)"
  15.357 +nitpick [expect = genuine]
  15.358 +oops
  15.359 +
  15.360 +lemma "(\<lambda>x. x) = (\<lambda>y. y)"
  15.361 +nitpick [expect = none]
  15.362 +apply simp
  15.363 +done
  15.364 +
  15.365 +subsubsection {* Sets *}
  15.366 +
  15.367 +lemma "P (A\<Colon>'a set)"
  15.368 +nitpick [expect = genuine]
  15.369 +oops
  15.370 +
  15.371 +lemma "P (A\<Colon>'a set set)"
  15.372 +nitpick [expect = genuine]
  15.373 +oops
  15.374 +
  15.375 +lemma "{x. P x} = {y. P y}"
  15.376 +nitpick [expect = none]
  15.377 +apply simp
  15.378 +done
  15.379 +
  15.380 +lemma "x \<in> {x. P x}"
  15.381 +nitpick [expect = genuine]
  15.382 +oops
  15.383 +
  15.384 +lemma "P (op \<in>)"
  15.385 +nitpick [expect = genuine]
  15.386 +oops
  15.387 +
  15.388 +lemma "P (op \<in> x)"
  15.389 +nitpick [expect = genuine]
  15.390 +oops
  15.391 +
  15.392 +lemma "P Collect"
  15.393 +nitpick [expect = genuine]
  15.394 +oops
  15.395 +
  15.396 +lemma "A Un B = A Int B"
  15.397 +nitpick [expect = genuine]
  15.398 +oops
  15.399 +
  15.400 +lemma "(A Int B) Un C = (A Un C) Int B"
  15.401 +nitpick [expect = genuine]
  15.402 +oops
  15.403 +
  15.404 +lemma "Ball A P \<longrightarrow> Bex A P"
  15.405 +nitpick [expect = genuine]
  15.406 +oops
  15.407 +
  15.408 +subsubsection {* @{const undefined} *}
  15.409 +
  15.410 +lemma "undefined"
  15.411 +nitpick [expect = genuine]
  15.412 +oops
  15.413 +
  15.414 +lemma "P undefined"
  15.415 +nitpick [expect = genuine]
  15.416 +oops
  15.417 +
  15.418 +lemma "undefined x"
  15.419 +nitpick [expect = genuine]
  15.420 +oops
  15.421 +
  15.422 +lemma "undefined undefined"
  15.423 +nitpick [expect = genuine]
  15.424 +oops
  15.425 +
  15.426 +subsubsection {* @{const The} *}
  15.427 +
  15.428 +lemma "The P"
  15.429 +nitpick [expect = genuine]
  15.430 +oops
  15.431 +
  15.432 +lemma "P The"
  15.433 +nitpick [expect = genuine]
  15.434 +oops
  15.435 +
  15.436 +lemma "P (The P)"
  15.437 +nitpick [expect = genuine]
  15.438 +oops
  15.439 +
  15.440 +lemma "(THE x. x=y) = z"
  15.441 +nitpick [expect = genuine]
  15.442 +oops
  15.443 +
  15.444 +lemma "Ex P \<longrightarrow> P (The P)"
  15.445 +nitpick [expect = genuine]
  15.446 +oops
  15.447 +
  15.448 +subsubsection {* @{const Eps} *}
  15.449 +
  15.450 +lemma "Eps P"
  15.451 +nitpick [expect = genuine]
  15.452 +oops
  15.453 +
  15.454 +lemma "P Eps"
  15.455 +nitpick [expect = genuine]
  15.456 +oops
  15.457 +
  15.458 +lemma "P (Eps P)"
  15.459 +nitpick [expect = genuine]
  15.460 +oops
  15.461 +
  15.462 +lemma "(SOME x. x=y) = z"
  15.463 +nitpick [expect = genuine]
  15.464 +oops
  15.465 +
  15.466 +lemma "Ex P \<longrightarrow> P (Eps P)"
  15.467 +nitpick [expect = none]
  15.468 +apply (auto simp add: someI)
  15.469 +done
  15.470 +
  15.471 +subsubsection {* Operations on Natural Numbers *}
  15.472 +
  15.473 +lemma "(x\<Colon>nat) + y = 0"
  15.474 +nitpick [expect = genuine]
  15.475 +oops
  15.476 +
  15.477 +lemma "(x\<Colon>nat) = x + x"
  15.478 +nitpick [expect = genuine]
  15.479 +oops
  15.480 +
  15.481 +lemma "(x\<Colon>nat) - y + y = x"
  15.482 +nitpick [expect = genuine]
  15.483 +oops
  15.484 +
  15.485 +lemma "(x\<Colon>nat) = x * x"
  15.486 +nitpick [expect = genuine]
  15.487 +oops
  15.488 +
  15.489 +lemma "(x\<Colon>nat) < x + y"
  15.490 +nitpick [card = 1, expect = genuine]
  15.491 +nitpick [card = 2-5, expect = genuine]
  15.492 +oops
  15.493 +
  15.494 +text {* \<times> *}
  15.495 +
  15.496 +lemma "P (x\<Colon>'a\<times>'b)"
  15.497 +nitpick [expect = genuine]
  15.498 +oops
  15.499 +
  15.500 +lemma "\<forall>x\<Colon>'a\<times>'b. P x"
  15.501 +nitpick [expect = genuine]
  15.502 +oops
  15.503 +
  15.504 +lemma "P (x, y)"
  15.505 +nitpick [expect = genuine]
  15.506 +oops
  15.507 +
  15.508 +lemma "P (fst x)"
  15.509 +nitpick [expect = genuine]
  15.510 +oops
  15.511 +
  15.512 +lemma "P (snd x)"
  15.513 +nitpick [expect = genuine]
  15.514 +oops
  15.515 +
  15.516 +lemma "P Pair"
  15.517 +nitpick [expect = genuine]
  15.518 +oops
  15.519 +
  15.520 +lemma "prod_rec f p = f (fst p) (snd p)"
  15.521 +nitpick [expect = none]
  15.522 +by (case_tac p) auto
  15.523 +
  15.524 +lemma "prod_rec f (a, b) = f a b"
  15.525 +nitpick [expect = none]
  15.526 +by auto
  15.527 +
  15.528 +lemma "P (prod_rec f x)"
  15.529 +nitpick [expect = genuine]
  15.530 +oops
  15.531 +
  15.532 +lemma "P (case x of Pair a b \<Rightarrow> f a b)"
  15.533 +nitpick [expect = genuine]
  15.534 +oops
  15.535 +
  15.536 +subsubsection {* Subtypes (typedef), typedecl *}
  15.537 +
  15.538 +text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
  15.539 +
  15.540 +typedef 'a myTdef = "insert (undefined\<Colon>'a) (undefined\<Colon>'a set)"
  15.541 +by auto
  15.542 +
  15.543 +lemma "(x\<Colon>'a myTdef) = y"
  15.544 +nitpick [expect = genuine]
  15.545 +oops
  15.546 +
  15.547 +typedecl myTdecl
  15.548 +
  15.549 +typedef 'a T_bij = "{(f\<Colon>'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
  15.550 +by auto
  15.551 +
  15.552 +lemma "P (f\<Colon>(myTdecl myTdef) T_bij)"
  15.553 +nitpick [expect = genuine]
  15.554 +oops
  15.555 +
  15.556 +subsubsection {* Inductive Datatypes *}
  15.557 +
  15.558 +text {* unit *}
  15.559 +
  15.560 +lemma "P (x\<Colon>unit)"
  15.561 +nitpick [expect = genuine]
  15.562 +oops
  15.563 +
  15.564 +lemma "\<forall>x\<Colon>unit. P x"
  15.565 +nitpick [expect = genuine]
  15.566 +oops
  15.567 +
  15.568 +lemma "P ()"
  15.569 +nitpick [expect = genuine]
  15.570 +oops
  15.571 +
  15.572 +lemma "unit_rec u x = u"
  15.573 +nitpick [expect = none]
  15.574 +apply simp
  15.575 +done
  15.576 +
  15.577 +lemma "P (unit_rec u x)"
  15.578 +nitpick [expect = genuine]
  15.579 +oops
  15.580 +
  15.581 +lemma "P (case x of () \<Rightarrow> u)"
  15.582 +nitpick [expect = genuine]
  15.583 +oops
  15.584 +
  15.585 +text {* option *}
  15.586 +
  15.587 +lemma "P (x\<Colon>'a option)"
  15.588 +nitpick [expect = genuine]
  15.589 +oops
  15.590 +
  15.591 +lemma "\<forall>x\<Colon>'a option. P x"
  15.592 +nitpick [expect = genuine]
  15.593 +oops
  15.594 +
  15.595 +lemma "P None"
  15.596 +nitpick [expect = genuine]
  15.597 +oops
  15.598 +
  15.599 +lemma "P (Some x)"
  15.600 +nitpick [expect = genuine]
  15.601 +oops
  15.602 +
  15.603 +lemma "option_rec n s None = n"
  15.604 +nitpick [expect = none]
  15.605 +apply simp
  15.606 +done
  15.607 +
  15.608 +lemma "option_rec n s (Some x) = s x"
  15.609 +nitpick [expect = none]
  15.610 +apply simp
  15.611 +done
  15.612 +
  15.613 +lemma "P (option_rec n s x)"
  15.614 +nitpick [expect = genuine]
  15.615 +oops
  15.616 +
  15.617 +lemma "P (case x of None \<Rightarrow> n | Some u \<Rightarrow> s u)"
  15.618 +nitpick [expect = genuine]
  15.619 +oops
  15.620 +
  15.621 +text {* + *}
  15.622 +
  15.623 +lemma "P (x\<Colon>'a+'b)"
  15.624 +nitpick [expect = genuine]
  15.625 +oops
  15.626 +
  15.627 +lemma "\<forall>x\<Colon>'a+'b. P x"
  15.628 +nitpick [expect = genuine]
  15.629 +oops
  15.630 +
  15.631 +lemma "P (Inl x)"
  15.632 +nitpick [expect = genuine]
  15.633 +oops
  15.634 +
  15.635 +lemma "P (Inr x)"
  15.636 +nitpick [expect = genuine]
  15.637 +oops
  15.638 +
  15.639 +lemma "P Inl"
  15.640 +nitpick [expect = genuine]
  15.641 +oops
  15.642 +
  15.643 +lemma "sum_rec l r (Inl x) = l x"
  15.644 +nitpick [expect = none]
  15.645 +apply simp
  15.646 +done
  15.647 +
  15.648 +lemma "sum_rec l r (Inr x) = r x"
  15.649 +nitpick [expect = none]
  15.650 +apply simp
  15.651 +done
  15.652 +
  15.653 +lemma "P (sum_rec l r x)"
  15.654 +nitpick [expect = genuine]
  15.655 +oops
  15.656 +
  15.657 +lemma "P (case x of Inl a \<Rightarrow> l a | Inr b \<Rightarrow> r b)"
  15.658 +nitpick [expect = genuine]
  15.659 +oops
  15.660 +
  15.661 +text {* Non-recursive datatypes *}
  15.662 +
  15.663 +datatype T1 = A | B
  15.664 +
  15.665 +lemma "P (x\<Colon>T1)"
  15.666 +nitpick [expect = genuine]
  15.667 +oops
  15.668 +
  15.669 +lemma "\<forall>x\<Colon>T1. P x"
  15.670 +nitpick [expect = genuine]
  15.671 +oops
  15.672 +
  15.673 +lemma "P A"
  15.674 +nitpick [expect = genuine]
  15.675 +oops
  15.676 +
  15.677 +lemma "P B"
  15.678 +nitpick [expect = genuine]
  15.679 +oops
  15.680 +
  15.681 +lemma "T1_rec a b A = a"
  15.682 +nitpick [expect = none]
  15.683 +apply simp
  15.684 +done
  15.685 +
  15.686 +lemma "T1_rec a b B = b"
  15.687 +nitpick [expect = none]
  15.688 +apply simp
  15.689 +done
  15.690 +
  15.691 +lemma "P (T1_rec a b x)"
  15.692 +nitpick [expect = genuine]
  15.693 +oops
  15.694 +
  15.695 +lemma "P (case x of A \<Rightarrow> a | B \<Rightarrow> b)"
  15.696 +nitpick [expect = genuine]
  15.697 +oops
  15.698 +
  15.699 +datatype 'a T2 = C T1 | D 'a
  15.700 +
  15.701 +lemma "P (x\<Colon>'a T2)"
  15.702 +nitpick [expect = genuine]
  15.703 +oops
  15.704 +
  15.705 +lemma "\<forall>x\<Colon>'a T2. P x"
  15.706 +nitpick [expect = genuine]
  15.707 +oops
  15.708 +
  15.709 +lemma "P D"
  15.710 +nitpick [expect = genuine]
  15.711 +oops
  15.712 +
  15.713 +lemma "T2_rec c d (C x) = c x"
  15.714 +nitpick [expect = none]
  15.715 +apply simp
  15.716 +done
  15.717 +
  15.718 +lemma "T2_rec c d (D x) = d x"
  15.719 +nitpick [expect = none]
  15.720 +apply simp
  15.721 +done
  15.722 +
  15.723 +lemma "P (T2_rec c d x)"
  15.724 +nitpick [expect = genuine]
  15.725 +oops
  15.726 +
  15.727 +lemma "P (case x of C u \<Rightarrow> c u | D v \<Rightarrow> d v)"
  15.728 +nitpick [expect = genuine]
  15.729 +oops
  15.730 +
  15.731 +datatype ('a, 'b) T3 = E "'a \<Rightarrow> 'b"
  15.732 +
  15.733 +lemma "P (x\<Colon>('a, 'b) T3)"
  15.734 +nitpick [expect = genuine]
  15.735 +oops
  15.736 +
  15.737 +lemma "\<forall>x\<Colon>('a, 'b) T3. P x"
  15.738 +nitpick [expect = genuine]
  15.739 +oops
  15.740 +
  15.741 +lemma "P E"
  15.742 +nitpick [expect = genuine]
  15.743 +oops
  15.744 +
  15.745 +lemma "T3_rec e (E x) = e x"
  15.746 +nitpick [card = 1\<midarrow>4, expect = none]
  15.747 +apply simp
  15.748 +done
  15.749 +
  15.750 +lemma "P (T3_rec e x)"
  15.751 +nitpick [expect = genuine]
  15.752 +oops
  15.753 +
  15.754 +lemma "P (case x of E f \<Rightarrow> e f)"
  15.755 +nitpick [expect = genuine]
  15.756 +oops
  15.757 +
  15.758 +text {* Recursive datatypes *}
  15.759 +
  15.760 +text {* nat *}
  15.761 +
  15.762 +lemma "P (x\<Colon>nat)"
  15.763 +nitpick [expect = genuine]
  15.764 +oops
  15.765 +
  15.766 +lemma "\<forall>x\<Colon>nat. P x"
  15.767 +nitpick [expect = genuine]
  15.768 +oops
  15.769 +
  15.770 +lemma "P (Suc 0)"
  15.771 +nitpick [expect = genuine]
  15.772 +oops
  15.773 +
  15.774 +lemma "P Suc"
  15.775 +nitpick [card = 1\<midarrow>7, expect = none]
  15.776 +oops
  15.777 +
  15.778 +lemma "nat_rec zero suc 0 = zero"
  15.779 +nitpick [expect = none]
  15.780 +apply simp
  15.781 +done
  15.782 +
  15.783 +lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
  15.784 +nitpick [expect = none]
  15.785 +apply simp
  15.786 +done
  15.787 +
  15.788 +lemma "P (nat_rec zero suc x)"
  15.789 +nitpick [expect = genuine]
  15.790 +oops
  15.791 +
  15.792 +lemma "P (case x of 0 \<Rightarrow> zero | Suc n \<Rightarrow> suc n)"
  15.793 +nitpick [expect = genuine]
  15.794 +oops
  15.795 +
  15.796 +text {* 'a list *}
  15.797 +
  15.798 +lemma "P (xs\<Colon>'a list)"
  15.799 +nitpick [expect = genuine]
  15.800 +oops
  15.801 +
  15.802 +lemma "\<forall>xs\<Colon>'a list. P xs"
  15.803 +nitpick [expect = genuine]
  15.804 +oops
  15.805 +
  15.806 +lemma "P [x, y]"
  15.807 +nitpick [expect = genuine]
  15.808 +oops
  15.809 +
  15.810 +lemma "list_rec nil cons [] = nil"
  15.811 +nitpick [expect = none]
  15.812 +apply simp
  15.813 +done
  15.814 +
  15.815 +lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
  15.816 +nitpick [expect = none]
  15.817 +apply simp
  15.818 +done
  15.819 +
  15.820 +lemma "P (list_rec nil cons xs)"
  15.821 +nitpick [expect = genuine]
  15.822 +oops
  15.823 +
  15.824 +lemma "P (case x of Nil \<Rightarrow> nil | Cons a b \<Rightarrow> cons a b)"
  15.825 +nitpick [expect = genuine]
  15.826 +oops
  15.827 +
  15.828 +lemma "(xs\<Colon>'a list) = ys"
  15.829 +nitpick [expect = genuine]
  15.830 +oops
  15.831 +
  15.832 +lemma "a # xs = b # xs"
  15.833 +nitpick [expect = genuine]
  15.834 +oops
  15.835 +
  15.836 +datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
  15.837 +
  15.838 +lemma "P (x\<Colon>BitList)"
  15.839 +nitpick [expect = genuine]
  15.840 +oops
  15.841 +
  15.842 +lemma "\<forall>x\<Colon>BitList. P x"
  15.843 +nitpick [expect = genuine]
  15.844 +oops
  15.845 +
  15.846 +lemma "P (Bit0 (Bit1 BitListNil))"
  15.847 +nitpick [expect = genuine]
  15.848 +oops
  15.849 +
  15.850 +lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
  15.851 +nitpick [expect = none]
  15.852 +apply simp
  15.853 +done
  15.854 +
  15.855 +lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
  15.856 +nitpick [expect = none]
  15.857 +apply simp
  15.858 +done
  15.859 +
  15.860 +lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
  15.861 +nitpick [expect = none]
  15.862 +apply simp
  15.863 +done
  15.864 +
  15.865 +lemma "P (BitList_rec nil bit0 bit1 x)"
  15.866 +nitpick [expect = genuine]
  15.867 +oops
  15.868 +
  15.869 +datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
  15.870 +
  15.871 +lemma "P (x\<Colon>'a BinTree)"
  15.872 +nitpick [expect = genuine]
  15.873 +oops
  15.874 +
  15.875 +lemma "\<forall>x\<Colon>'a BinTree. P x"
  15.876 +nitpick [expect = genuine]
  15.877 +oops
  15.878 +
  15.879 +lemma "P (Node (Leaf x) (Leaf y))"
  15.880 +nitpick [expect = genuine]
  15.881 +oops
  15.882 +
  15.883 +lemma "BinTree_rec l n (Leaf x) = l x"
  15.884 +nitpick [expect = none]
  15.885 +apply simp
  15.886 +done
  15.887 +
  15.888 +lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
  15.889 +nitpick [card = 1\<midarrow>6, expect = none]
  15.890 +apply simp
  15.891 +done
  15.892 +
  15.893 +lemma "P (BinTree_rec l n x)"
  15.894 +nitpick [expect = genuine]
  15.895 +oops
  15.896 +
  15.897 +lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
  15.898 +nitpick [expect = genuine]
  15.899 +oops
  15.900 +
  15.901 +text {* Mutually recursive datatypes *}
  15.902 +
  15.903 +datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
  15.904 + and 'a bexp = Equal "'a aexp" "'a aexp"
  15.905 +
  15.906 +lemma "P (x\<Colon>'a aexp)"
  15.907 +nitpick [expect = genuine]
  15.908 +oops
  15.909 +
  15.910 +lemma "\<forall>x\<Colon>'a aexp. P x"
  15.911 +nitpick [expect = genuine]
  15.912 +oops
  15.913 +
  15.914 +lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
  15.915 +nitpick [expect = genuine]
  15.916 +oops
  15.917 +
  15.918 +lemma "P (x\<Colon>'a bexp)"
  15.919 +nitpick [expect = genuine]
  15.920 +oops
  15.921 +
  15.922 +lemma "\<forall>x\<Colon>'a bexp. P x"
  15.923 +nitpick [expect = genuine]
  15.924 +oops
  15.925 +
  15.926 +lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
  15.927 +nitpick [card = 1\<midarrow>4, expect = none]
  15.928 +apply simp
  15.929 +done
  15.930 +
  15.931 +lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"
  15.932 +nitpick [card = 1\<midarrow>4, expect = none]
  15.933 +apply simp
  15.934 +done
  15.935 +
  15.936 +lemma "P (aexp_bexp_rec_1 number ite equal x)"
  15.937 +nitpick [expect = genuine]
  15.938 +oops
  15.939 +
  15.940 +lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
  15.941 +nitpick [expect = genuine]
  15.942 +oops
  15.943 +
  15.944 +lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"
  15.945 +nitpick [card = 1\<midarrow>4, expect = none]
  15.946 +apply simp
  15.947 +done
  15.948 +
  15.949 +lemma "P (aexp_bexp_rec_2 number ite equal x)"
  15.950 +nitpick [expect = genuine]
  15.951 +oops
  15.952 +
  15.953 +lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
  15.954 +nitpick [expect = genuine]
  15.955 +oops
  15.956 +
  15.957 +datatype X = A | B X | C Y
  15.958 +     and Y = D X | E Y | F
  15.959 +
  15.960 +lemma "P (x\<Colon>X)"
  15.961 +nitpick [expect = genuine]
  15.962 +oops
  15.963 +
  15.964 +lemma "P (y\<Colon>Y)"
  15.965 +nitpick [expect = genuine]
  15.966 +oops
  15.967 +
  15.968 +lemma "P (B (B A))"
  15.969 +nitpick [expect = genuine]
  15.970 +oops
  15.971 +
  15.972 +lemma "P (B (C F))"
  15.973 +nitpick [expect = genuine]
  15.974 +oops
  15.975 +
  15.976 +lemma "P (C (D A))"
  15.977 +nitpick [expect = genuine]
  15.978 +oops
  15.979 +
  15.980 +lemma "P (C (E F))"
  15.981 +nitpick [expect = genuine]
  15.982 +oops
  15.983 +
  15.984 +lemma "P (D (B A))"
  15.985 +nitpick [expect = genuine]
  15.986 +oops
  15.987 +
  15.988 +lemma "P (D (C F))"
  15.989 +nitpick [expect = genuine]
  15.990 +oops
  15.991 +
  15.992 +lemma "P (E (D A))"
  15.993 +nitpick [expect = genuine]
  15.994 +oops
  15.995 +
  15.996 +lemma "P (E (E F))"
  15.997 +nitpick [expect = genuine]
  15.998 +oops
  15.999 +
 15.1000 +lemma "P (C (D (C F)))"
 15.1001 +nitpick [expect = genuine]
 15.1002 +oops
 15.1003 +
 15.1004 +lemma "X_Y_rec_1 a b c d e f A = a"
 15.1005 +nitpick [expect = none]
 15.1006 +apply simp
 15.1007 +done
 15.1008 +
 15.1009 +lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"
 15.1010 +nitpick [expect = none]
 15.1011 +apply simp
 15.1012 +done
 15.1013 +
 15.1014 +lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"
 15.1015 +nitpick [expect = none]
 15.1016 +apply simp
 15.1017 +done
 15.1018 +
 15.1019 +lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"
 15.1020 +nitpick [expect = none]
 15.1021 +apply simp
 15.1022 +done
 15.1023 +
 15.1024 +lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"
 15.1025 +nitpick [expect = none]
 15.1026 +apply simp
 15.1027 +done
 15.1028 +
 15.1029 +lemma "X_Y_rec_2 a b c d e f F = f"
 15.1030 +nitpick [expect = none]
 15.1031 +apply simp
 15.1032 +done
 15.1033 +
 15.1034 +lemma "P (X_Y_rec_1 a b c d e f x)"
 15.1035 +nitpick [expect = genuine]
 15.1036 +oops
 15.1037 +
 15.1038 +lemma "P (X_Y_rec_2 a b c d e f y)"
 15.1039 +nitpick [expect = genuine]
 15.1040 +oops
 15.1041 +
 15.1042 +text {* Other datatype examples *}
 15.1043 +
 15.1044 +text {* Indirect recursion is implemented via mutual recursion. *}
 15.1045 +
 15.1046 +datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
 15.1047 +
 15.1048 +lemma "P (x\<Colon>XOpt)"
 15.1049 +nitpick [expect = genuine]
 15.1050 +oops
 15.1051 +
 15.1052 +lemma "P (CX None)"
 15.1053 +nitpick [expect = genuine]
 15.1054 +oops
 15.1055 +
 15.1056 +lemma "P (CX (Some (CX None)))"
 15.1057 +nitpick [expect = genuine]
 15.1058 +oops
 15.1059 +
 15.1060 +lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
 15.1061 +nitpick [card = 1\<midarrow>6, expect = none]
 15.1062 +apply simp
 15.1063 +done
 15.1064 +
 15.1065 +lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"
 15.1066 +nitpick [card = 1\<midarrow>4, expect = none]
 15.1067 +apply simp
 15.1068 +done
 15.1069 +
 15.1070 +lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
 15.1071 +nitpick [card = 1\<midarrow>4, expect = none]
 15.1072 +apply simp
 15.1073 +done
 15.1074 +
 15.1075 +lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
 15.1076 +nitpick [card = 1\<midarrow>4, expect = none]
 15.1077 +apply simp
 15.1078 +done
 15.1079 +
 15.1080 +lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
 15.1081 +nitpick [card = 1\<midarrow>4, expect = none]
 15.1082 +apply simp
 15.1083 +done
 15.1084 +
 15.1085 +lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
 15.1086 +nitpick [card = 1\<midarrow>4, expect = none]
 15.1087 +apply simp
 15.1088 +done
 15.1089 +
 15.1090 +lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
 15.1091 +nitpick [expect = genuine]
 15.1092 +oops
 15.1093 +
 15.1094 +lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
 15.1095 +nitpick [expect = genuine]
 15.1096 +oops
 15.1097 +
 15.1098 +lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
 15.1099 +nitpick [expect = genuine]
 15.1100 +oops
 15.1101 +
 15.1102 +datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
 15.1103 +
 15.1104 +lemma "P (x\<Colon>'a YOpt)"
 15.1105 +nitpick [expect = genuine]
 15.1106 +oops
 15.1107 +
 15.1108 +lemma "P (CY None)"
 15.1109 +nitpick [expect = genuine]
 15.1110 +oops
 15.1111 +
 15.1112 +lemma "P (CY (Some (\<lambda>a. CY None)))"
 15.1113 +nitpick [expect = genuine]
 15.1114 +oops
 15.1115 +
 15.1116 +lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
 15.1117 +nitpick [card = 1\<midarrow>2, expect = none]
 15.1118 +apply simp
 15.1119 +done
 15.1120 +
 15.1121 +lemma "YOpt_rec_2 cy n s None = n"
 15.1122 +nitpick [card = 1\<midarrow>2, expect = none]
 15.1123 +apply simp
 15.1124 +done
 15.1125 +
 15.1126 +lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
 15.1127 +nitpick [card = 1\<midarrow>2, expect = none]
 15.1128 +apply simp
 15.1129 +done
 15.1130 +
 15.1131 +lemma "P (YOpt_rec_1 cy n s x)"
 15.1132 +nitpick [expect = genuine]
 15.1133 +oops
 15.1134 +
 15.1135 +lemma "P (YOpt_rec_2 cy n s x)"
 15.1136 +nitpick [expect = genuine]
 15.1137 +oops
 15.1138 +
 15.1139 +datatype Trie = TR "Trie list"
 15.1140 +
 15.1141 +lemma "P (x\<Colon>Trie)"
 15.1142 +nitpick [expect = genuine]
 15.1143 +oops
 15.1144 +
 15.1145 +lemma "\<forall>x\<Colon>Trie. P x"
 15.1146 +nitpick [expect = genuine]
 15.1147 +oops
 15.1148 +
 15.1149 +lemma "P (TR [TR []])"
 15.1150 +nitpick [expect = genuine]
 15.1151 +oops
 15.1152 +
 15.1153 +lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
 15.1154 +nitpick [card = 1\<midarrow>6, expect = none]
 15.1155 +apply simp
 15.1156 +done
 15.1157 +
 15.1158 +lemma "Trie_rec_2 tr nil cons [] = nil"
 15.1159 +nitpick [card = 1\<midarrow>6, expect = none]
 15.1160 +apply simp
 15.1161 +done
 15.1162 +
 15.1163 +lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"
 15.1164 +nitpick [card = 1\<midarrow>6, expect = none]
 15.1165 +apply simp
 15.1166 +done
 15.1167 +
 15.1168 +lemma "P (Trie_rec_1 tr nil cons x)"
 15.1169 +nitpick [card = 1, expect = genuine]
 15.1170 +oops
 15.1171 +
 15.1172 +lemma "P (Trie_rec_2 tr nil cons x)"
 15.1173 +nitpick [card = 1, expect = genuine]
 15.1174 +oops
 15.1175 +
 15.1176 +datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
 15.1177 +
 15.1178 +lemma "P (x\<Colon>InfTree)"
 15.1179 +nitpick [expect = genuine]
 15.1180 +oops
 15.1181 +
 15.1182 +lemma "\<forall>x\<Colon>InfTree. P x"
 15.1183 +nitpick [expect = genuine]
 15.1184 +oops
 15.1185 +
 15.1186 +lemma "P (Node (\<lambda>n. Leaf))"
 15.1187 +nitpick [expect = genuine]
 15.1188 +oops
 15.1189 +
 15.1190 +lemma "InfTree_rec leaf node Leaf = leaf"
 15.1191 +nitpick [card = 1\<midarrow>3, expect = none]
 15.1192 +apply simp
 15.1193 +done
 15.1194 +
 15.1195 +lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
 15.1196 +nitpick [card = 1\<midarrow>3, expect = none]
 15.1197 +apply simp
 15.1198 +done
 15.1199 +
 15.1200 +lemma "P (InfTree_rec leaf node x)"
 15.1201 +nitpick [expect = genuine]
 15.1202 +oops
 15.1203 +
 15.1204 +datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
 15.1205 +
 15.1206 +lemma "P (x\<Colon>'a lambda)"
 15.1207 +nitpick [expect = genuine]
 15.1208 +oops
 15.1209 +
 15.1210 +lemma "\<forall>x\<Colon>'a lambda. P x"
 15.1211 +nitpick [expect = genuine]
 15.1212 +oops
 15.1213 +
 15.1214 +lemma "P (Lam (\<lambda>a. Var a))"
 15.1215 +nitpick [card = 1\<midarrow>5, expect = none]
 15.1216 +nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
 15.1217 +oops
 15.1218 +
 15.1219 +lemma "lambda_rec var app lam (Var x) = var x"
 15.1220 +nitpick [card = 1\<midarrow>3, expect = none]
 15.1221 +apply simp
 15.1222 +done
 15.1223 +
 15.1224 +lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
 15.1225 +nitpick [card = 1\<midarrow>3, expect = none]
 15.1226 +apply simp
 15.1227 +done
 15.1228 +
 15.1229 +lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
 15.1230 +nitpick [card = 1\<midarrow>3, expect = none]
 15.1231 +apply simp
 15.1232 +done
 15.1233 +
 15.1234 +lemma "P (lambda_rec v a l x)"
 15.1235 +nitpick [expect = genuine]
 15.1236 +oops
 15.1237 +
 15.1238 +text {* Taken from "Inductive datatypes in HOL", p. 8: *}
 15.1239 +
 15.1240 +datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
 15.1241 +datatype 'c U = E "('c, 'c U) T"
 15.1242 +
 15.1243 +lemma "P (x\<Colon>'c U)"
 15.1244 +nitpick [expect = genuine]
 15.1245 +oops
 15.1246 +
 15.1247 +lemma "\<forall>x\<Colon>'c U. P x"
 15.1248 +nitpick [expect = genuine]
 15.1249 +oops
 15.1250 +
 15.1251 +lemma "P (E (C (\<lambda>a. True)))"
 15.1252 +nitpick [expect = genuine]
 15.1253 +oops
 15.1254 +
 15.1255 +lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
 15.1256 +nitpick [card = 1\<midarrow>3, expect = none]
 15.1257 +apply simp
 15.1258 +done
 15.1259 +
 15.1260 +lemma "U_rec_2 e c d nil cons (C x) = c x"
 15.1261 +nitpick [card = 1\<midarrow>3, expect = none]
 15.1262 +apply simp
 15.1263 +done
 15.1264 +
 15.1265 +lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
 15.1266 +nitpick [card = 1\<midarrow>3, expect = none]
 15.1267 +apply simp
 15.1268 +done
 15.1269 +
 15.1270 +lemma "U_rec_3 e c d nil cons [] = nil"
 15.1271 +nitpick [card = 1\<midarrow>3, expect = none]
 15.1272 +apply simp
 15.1273 +done
 15.1274 +
 15.1275 +lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)"
 15.1276 +nitpick [card = 1\<midarrow>3, expect = none]
 15.1277 +apply simp
 15.1278 +done
 15.1279 +
 15.1280 +lemma "P (U_rec_1 e c d nil cons x)"
 15.1281 +nitpick [expect = genuine]
 15.1282 +oops
 15.1283 +
 15.1284 +lemma "P (U_rec_2 e c d nil cons x)"
 15.1285 +nitpick [card = 1, expect = genuine]
 15.1286 +oops
 15.1287 +
 15.1288 +lemma "P (U_rec_3 e c d nil cons x)"
 15.1289 +nitpick [card = 1, expect = genuine]
 15.1290 +oops
 15.1291 +
 15.1292 +subsubsection {* Records *}
 15.1293 +
 15.1294 +record ('a, 'b) point =
 15.1295 +  xpos :: 'a
 15.1296 +  ypos :: 'b
 15.1297 +
 15.1298 +lemma "(x\<Colon>('a, 'b) point) = y"
 15.1299 +nitpick [expect = genuine]
 15.1300 +oops
 15.1301 +
 15.1302 +record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
 15.1303 +  ext :: 'c
 15.1304 +
 15.1305 +lemma "(x\<Colon>('a, 'b, 'c) extpoint) = y"
 15.1306 +nitpick [expect = genuine]
 15.1307 +oops
 15.1308 +
 15.1309 +subsubsection {* Inductively Defined Sets *}
 15.1310 +
 15.1311 +inductive_set undefinedSet :: "'a set" where
 15.1312 +"undefined \<in> undefinedSet"
 15.1313 +
 15.1314 +lemma "x \<in> undefinedSet"
 15.1315 +nitpick [expect = genuine]
 15.1316 +oops
 15.1317 +
 15.1318 +inductive_set evenCard :: "'a set set"
 15.1319 +where
 15.1320 +"{} \<in> evenCard" |
 15.1321 +"\<lbrakk>S \<in> evenCard; x \<notin> S; y \<notin> S; x \<noteq> y\<rbrakk> \<Longrightarrow> S \<union> {x, y} \<in> evenCard"
 15.1322 +
 15.1323 +lemma "S \<in> evenCard"
 15.1324 +nitpick [expect = genuine]
 15.1325 +oops
 15.1326 +
 15.1327 +inductive_set
 15.1328 +even :: "nat set"
 15.1329 +and odd :: "nat set"
 15.1330 +where
 15.1331 +"0 \<in> even" |
 15.1332 +"n \<in> even \<Longrightarrow> Suc n \<in> odd" |
 15.1333 +"n \<in> odd \<Longrightarrow> Suc n \<in> even"
 15.1334 +
 15.1335 +lemma "n \<in> odd"
 15.1336 +nitpick [expect = genuine]
 15.1337 +oops
 15.1338 +
 15.1339 +consts f :: "'a \<Rightarrow> 'a"
 15.1340 +
 15.1341 +inductive_set a_even :: "'a set" and a_odd :: "'a set" where
 15.1342 +"undefined \<in> a_even" |
 15.1343 +"x \<in> a_even \<Longrightarrow> f x \<in> a_odd" |
 15.1344 +"x \<in> a_odd \<Longrightarrow> f x \<in> a_even"
 15.1345 +
 15.1346 +lemma "x \<in> a_odd"
 15.1347 +nitpick [expect = genuine]
 15.1348 +oops
 15.1349 +
 15.1350 +subsubsection {* Examples Involving Special Functions *}
 15.1351 +
 15.1352 +lemma "card x = 0"
 15.1353 +nitpick [expect = genuine]
 15.1354 +oops
 15.1355 +
 15.1356 +lemma "finite x"
 15.1357 +nitpick [expect = none]
 15.1358 +oops
 15.1359 +
 15.1360 +lemma "xs @ [] = ys @ []"
 15.1361 +nitpick [expect = genuine]
 15.1362 +oops
 15.1363 +
 15.1364 +lemma "xs @ ys = ys @ xs"
 15.1365 +nitpick [expect = genuine]
 15.1366 +oops
 15.1367 +
 15.1368 +lemma "f (lfp f) = lfp f"
 15.1369 +nitpick [expect = genuine]
 15.1370 +oops
 15.1371 +
 15.1372 +lemma "f (gfp f) = gfp f"
 15.1373 +nitpick [expect = genuine]
 15.1374 +oops
 15.1375 +
 15.1376 +lemma "lfp f = gfp f"
 15.1377 +nitpick [expect = genuine]
 15.1378 +oops
 15.1379 +
 15.1380 +subsubsection {* Axiomatic Type Classes and Overloading *}
 15.1381 +
 15.1382 +text {* A type class without axioms: *}
 15.1383 +
 15.1384 +axclass classA
 15.1385 +
 15.1386 +lemma "P (x\<Colon>'a\<Colon>classA)"
 15.1387 +nitpick [expect = genuine]
 15.1388 +oops
 15.1389 +
 15.1390 +text {* The axiom of this type class does not contain any type variables: *}
 15.1391 +
 15.1392 +axclass classB
 15.1393 +classB_ax: "P \<or> \<not> P"
 15.1394 +
 15.1395 +lemma "P (x\<Colon>'a\<Colon>classB)"
 15.1396 +nitpick [expect = genuine]
 15.1397 +oops
 15.1398 +
 15.1399 +text {* An axiom with a type variable (denoting types which have at least two elements): *}
 15.1400 +
 15.1401 +axclass classC < type
 15.1402 +classC_ax: "\<exists>x y. x \<noteq> y"
 15.1403 +
 15.1404 +lemma "P (x\<Colon>'a\<Colon>classC)"
 15.1405 +nitpick [expect = genuine]
 15.1406 +oops
 15.1407 +
 15.1408 +lemma "\<exists>x y. (x\<Colon>'a\<Colon>classC) \<noteq> y"
 15.1409 +nitpick [expect = none]
 15.1410 +sorry
 15.1411 +
 15.1412 +text {* A type class for which a constant is defined: *}
 15.1413 +
 15.1414 +consts
 15.1415 +classD_const :: "'a \<Rightarrow> 'a"
 15.1416 +
 15.1417 +axclass classD < type
 15.1418 +classD_ax: "classD_const (classD_const x) = classD_const x"
 15.1419 +
 15.1420 +lemma "P (x\<Colon>'a\<Colon>classD)"
 15.1421 +nitpick [expect = genuine]
 15.1422 +oops
 15.1423 +
 15.1424 +text {* A type class with multiple superclasses: *}
 15.1425 +
 15.1426 +axclass classE < classC, classD
 15.1427 +
 15.1428 +lemma "P (x\<Colon>'a\<Colon>classE)"
 15.1429 +nitpick [expect = genuine]
 15.1430 +oops
 15.1431 +
 15.1432 +lemma "P (x\<Colon>'a\<Colon>{classB, classE})"
 15.1433 +nitpick [expect = genuine]
 15.1434 +oops
 15.1435 +
 15.1436 +text {* OFCLASS: *}
 15.1437 +
 15.1438 +lemma "OFCLASS('a\<Colon>type, type_class)"
 15.1439 +nitpick [expect = none]
 15.1440 +apply intro_classes
 15.1441 +done
 15.1442 +
 15.1443 +lemma "OFCLASS('a\<Colon>classC, type_class)"
 15.1444 +nitpick [expect = none]
 15.1445 +apply intro_classes
 15.1446 +done
 15.1447 +
 15.1448 +lemma "OFCLASS('a, classB_class)"
 15.1449 +nitpick [expect = none]
 15.1450 +apply intro_classes
 15.1451 +apply simp
 15.1452 +done
 15.1453 +
 15.1454 +lemma "OFCLASS('a\<Colon>type, classC_class)"
 15.1455 +nitpick [expect = genuine]
 15.1456 +oops
 15.1457 +
 15.1458 +text {* Overloading: *}
 15.1459 +
 15.1460 +consts inverse :: "'a \<Rightarrow> 'a"
 15.1461 +
 15.1462 +defs (overloaded)
 15.1463 +inverse_bool: "inverse (b\<Colon>bool) \<equiv> \<not> b"
 15.1464 +inverse_set: "inverse (S\<Colon>'a set) \<equiv> -S"
 15.1465 +inverse_pair: "inverse p \<equiv> (inverse (fst p), inverse (snd p))"
 15.1466 +
 15.1467 +lemma "inverse b"
 15.1468 +nitpick [expect = genuine]
 15.1469 +oops
 15.1470 +
 15.1471 +lemma "P (inverse (S\<Colon>'a set))"
 15.1472 +nitpick [expect = genuine]
 15.1473 +oops
 15.1474 +
 15.1475 +lemma "P (inverse (p\<Colon>'a\<times>'b))"
 15.1476 +nitpick [expect = genuine]
 15.1477 +oops
 15.1478 +
 15.1479 +end
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Nitpick_Examples/Special_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
    16.3 @@ -0,0 +1,172 @@
    16.4 +(*  Title:      HOL/Nitpick_Examples/Special_Nits.thy
    16.5 +    Author:     Jasmin Blanchette, TU Muenchen
    16.6 +    Copyright   2009
    16.7 +
    16.8 +Examples featuring Nitpick's "specialize" optimization.
    16.9 +*)
   16.10 +
   16.11 +header {* Examples Featuring Nitpick's \textit{specialize} Optimization *}
   16.12 +
   16.13 +theory Special_Nits
   16.14 +imports Main
   16.15 +begin
   16.16 +
   16.17 +nitpick_params [card = 4, debug, show_consts, timeout = 10 s]
   16.18 +
   16.19 +fun f1 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   16.20 +"f1 a b c d e = a + b + c + d + e"
   16.21 +
   16.22 +lemma "f1 0 0 0 0 0 = f1 0 0 0 0 (1 - 1)"
   16.23 +nitpick [expect = none]
   16.24 +nitpick [dont_specialize, expect = none]
   16.25 +sorry
   16.26 +
   16.27 +lemma "f1 u v w x y = f1 y x w v u"
   16.28 +nitpick [expect = none]
   16.29 +nitpick [dont_specialize, expect = none]
   16.30 +sorry
   16.31 +
   16.32 +fun f2 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   16.33 +"f2 a b c d (Suc e) = a + b + c + d + e"
   16.34 +
   16.35 +lemma "f2 0 0 0 0 0 = f2 (1 - 1) 0 0 0 0"
   16.36 +nitpick [expect = none]
   16.37 +nitpick [dont_specialize, expect = none]
   16.38 +sorry
   16.39 +
   16.40 +lemma "f2 0 (v - v) 0 (x - x) 0 = f2 (u - u) 0 (w - w) 0 (y - y)"
   16.41 +nitpick [expect = none]
   16.42 +nitpick [dont_specialize, expect = none]
   16.43 +sorry
   16.44 +
   16.45 +lemma "f2 1 0 0 0 0 = f2 0 1 0 0 0"
   16.46 +nitpick [expect = genuine]
   16.47 +nitpick [dont_specialize, expect = genuine]
   16.48 +oops
   16.49 +
   16.50 +lemma "f2 0 0 0 0 0 = f2 0 0 0 0 0"
   16.51 +nitpick [expect = none]
   16.52 +nitpick [dont_specialize, expect = none]
   16.53 +sorry
   16.54 +
   16.55 +fun f3 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   16.56 +"f3 (Suc a) b 0 d (Suc e) = a + b + d + e" |
   16.57 +"f3 0 b 0 d 0 = b + d"
   16.58 +
   16.59 +lemma "f3 a b c d e = f3 e d c b a"
   16.60 +nitpick [expect = genuine]
   16.61 +nitpick [dont_specialize, expect = genuine]
   16.62 +oops
   16.63 +
   16.64 +lemma "f3 a b c d a = f3 a d c d a"
   16.65 +nitpick [expect = genuine]
   16.66 +nitpick [dont_specialize, expect = genuine]
   16.67 +oops
   16.68 +
   16.69 +lemma "\<lbrakk>c < 1; a \<ge> e; e \<ge> a\<rbrakk> \<Longrightarrow> f3 a b c d a = f3 e d c b e"
   16.70 +nitpick [expect = none]
   16.71 +nitpick [dont_specialize, expect = none]
   16.72 +sorry
   16.73 +
   16.74 +lemma "(\<forall>u. a = u \<longrightarrow> f3 a a a a a = f3 u u u u u)
   16.75 +       \<and> (\<forall>u. b = u \<longrightarrow> f3 b b u b b = f3 u u b u u)"
   16.76 +nitpick [expect = none]
   16.77 +nitpick [dont_specialize, expect = none]
   16.78 +nitpick [dont_skolemize, expect = none]
   16.79 +nitpick [dont_specialize, dont_skolemize, expect = none]
   16.80 +sorry
   16.81 +
   16.82 +function f4 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
   16.83 +"f4 x x = 1" |
   16.84 +"f4 y z = (if y = z then 1 else 0)"
   16.85 +by auto
   16.86 +termination by lexicographic_order
   16.87 +
   16.88 +lemma "f4 a b = f4 b a"
   16.89 +nitpick [expect = none]
   16.90 +nitpick [dont_specialize, expect = none]
   16.91 +sorry
   16.92 +
   16.93 +lemma "f4 a (Suc a) = f4 a a"
   16.94 +nitpick [expect = genuine]
   16.95 +nitpick [dont_specialize, expect = genuine]
   16.96 +oops
   16.97 +
   16.98 +fun f5 :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" where
   16.99 +"f5 f (Suc a) = f a"
  16.100 +
  16.101 +lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
  16.102 +       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"
  16.103 +nitpick [expect = none]
  16.104 +nitpick [dont_specialize, expect = none]
  16.105 +sorry
  16.106 +
  16.107 +lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
  16.108 +       f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) (Suc x) = x"
  16.109 +nitpick [expect = none]
  16.110 +nitpick [dont_specialize, expect = none]
  16.111 +sorry
  16.112 +
  16.113 +lemma "\<exists>one \<in> {1}. \<exists>two \<in> {2}.
  16.114 +       f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
  16.115 +nitpick [expect = genuine]
  16.116 +sorry
  16.117 +
  16.118 +lemma "\<exists>two \<in> {2}. \<exists>one \<in> {1}.
  16.119 +       f5 (\<lambda>a. if a = one then 2 else if a = two then 1 else a) (Suc x) = x"
  16.120 +nitpick [expect = genuine]
  16.121 +sorry
  16.122 +
  16.123 +lemma "\<forall>a. g a = a
  16.124 +       \<Longrightarrow> \<exists>one \<in> {1}. \<exists>two \<in> {2}. f5 g x =
  16.125 +                      f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"
  16.126 +nitpick [expect = none]
  16.127 +nitpick [dont_specialize, expect = none]
  16.128 +sorry
  16.129 +
  16.130 +lemma "\<forall>a. g a = a
  16.131 +       \<Longrightarrow> \<exists>one \<in> {2}. \<exists>two \<in> {1}. f5 g x =
  16.132 +                      f5 (\<lambda>a. if a = one then 1 else if a = two then 2 else a) x"
  16.133 +nitpick [expect = potential]
  16.134 +nitpick [dont_specialize, expect = potential]
  16.135 +sorry
  16.136 +
  16.137 +lemma "\<forall>a. g a = a
  16.138 +       \<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
  16.139 +           b\<^isub>1 < b\<^isub>11 \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then a else h b\<^isub>2) x"
  16.140 +nitpick [expect = potential]
  16.141 +nitpick [dont_specialize, expect = none]
  16.142 +nitpick [dont_box, expect = none]
  16.143 +nitpick [dont_box, dont_specialize, expect = none]
  16.144 +sorry
  16.145 +
  16.146 +lemma "\<forall>a. g a = a
  16.147 +       \<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
  16.148 +           b\<^isub>1 < b\<^isub>11
  16.149 +           \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then
  16.150 +                                a
  16.151 +                              else
  16.152 +                                h b\<^isub>2 + h b\<^isub>3 + h b\<^isub>4 + h b\<^isub>5 + h b\<^isub>6 + h b\<^isub>7 + h b\<^isub>8
  16.153 +                                + h b\<^isub>9 + h b\<^isub>10) x"
  16.154 +nitpick [card nat = 2, card 'a = 1, expect = none]
  16.155 +nitpick [card nat = 2, card 'a = 1, dont_box, expect = none]
  16.156 +nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = none]
  16.157 +nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize, expect = none]
  16.158 +sorry
  16.159 +
  16.160 +lemma "\<forall>a. g a = a
  16.161 +       \<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
  16.162 +           b\<^isub>1 < b\<^isub>11
  16.163 +           \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 \<ge> b\<^isub>11 then
  16.164 +                                a
  16.165 +                              else
  16.166 +                                h b\<^isub>2 + h b\<^isub>3 + h b\<^isub>4 + h b\<^isub>5 + h b\<^isub>6 + h b\<^isub>7 + h b\<^isub>8
  16.167 +                                + h b\<^isub>9 + h b\<^isub>10) x"
  16.168 +nitpick [card nat = 2, card 'a = 1, expect = none]
  16.169 +nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential]
  16.170 +nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential]
  16.171 +nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize,
  16.172 +         expect = potential]
  16.173 +oops
  16.174 +
  16.175 +end
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/Nitpick_Examples/Tests_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
    17.3 @@ -0,0 +1,16 @@
    17.4 +(*  Title:      HOL/Nitpick_Examples/Tests_Nits.thy
    17.5 +    Author:     Jasmin Blanchette, TU Muenchen
    17.6 +    Copyright   2009
    17.7 +
    17.8 +Nitpick tests.
    17.9 +*)
   17.10 +
   17.11 +header {* Nitpick Tests *}
   17.12 +
   17.13 +theory Tests_Nits
   17.14 +imports Main
   17.15 +begin
   17.16 +
   17.17 +ML {* NitpickTests.run_all_tests () *}
   17.18 +
   17.19 +end
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy	Fri Oct 23 18:59:24 2009 +0200
    18.3 @@ -0,0 +1,187 @@
    18.4 +(*  Title:      HOL/Nitpick_Examples/Typedef_Nits.thy
    18.5 +    Author:     Jasmin Blanchette, TU Muenchen
    18.6 +    Copyright   2009
    18.7 +
    18.8 +Examples featuring Nitpick applied to typedefs.
    18.9 +*)
   18.10 +
   18.11 +header {* Examples Featuring Nitpick Applied to Typedefs *}
   18.12 +
   18.13 +theory Typedef_Nits
   18.14 +imports Main Rational
   18.15 +begin
   18.16 +
   18.17 +nitpick_params [card = 1\<midarrow>4, timeout = 5 s]
   18.18 +
   18.19 +typedef three = "{0\<Colon>nat, 1, 2}"
   18.20 +by blast
   18.21 +
   18.22 +definition A :: three where "A \<equiv> Abs_three 0"
   18.23 +definition B :: three where "B \<equiv> Abs_three 1"
   18.24 +definition C :: three where "C \<equiv> Abs_three 2"
   18.25 +
   18.26 +lemma "x = (y\<Colon>three)"
   18.27 +nitpick [expect = genuine]
   18.28 +oops
   18.29 +
   18.30 +typedef 'a one_or_two = "{undefined False\<Colon>'a, undefined True}"
   18.31 +by auto
   18.32 +
   18.33 +lemma "x = (y\<Colon>unit one_or_two)"
   18.34 +nitpick [expect = none]
   18.35 +sorry
   18.36 +
   18.37 +lemma "x = (y\<Colon>bool one_or_two)"
   18.38 +nitpick [expect = genuine]
   18.39 +oops
   18.40 +
   18.41 +lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> x = (y\<Colon>bool one_or_two)"
   18.42 +nitpick [expect = none]
   18.43 +sorry
   18.44 +
   18.45 +lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> \<exists>x (y\<Colon>bool one_or_two). x \<noteq> y"
   18.46 +nitpick [card = 1, expect = potential] (* unfortunate *)
   18.47 +oops
   18.48 +
   18.49 +lemma "\<exists>x (y\<Colon>bool one_or_two). x \<noteq> y"
   18.50 +nitpick [card = 1, expect = potential] (* unfortunate *)
   18.51 +nitpick [card = 2, expect = none]
   18.52 +oops
   18.53 +
   18.54 +typedef 'a bounded =
   18.55 +        "{n\<Colon>nat. finite (UNIV\<Colon>'a \<Rightarrow> bool) \<longrightarrow> n < card (UNIV\<Colon>'a \<Rightarrow> bool)}"
   18.56 +apply (rule_tac x = 0 in exI)
   18.57 +apply (case_tac "card UNIV = 0")
   18.58 +by auto
   18.59 +
   18.60 +lemma "x = (y\<Colon>unit bounded)"
   18.61 +nitpick [expect = none]
   18.62 +sorry
   18.63 +
   18.64 +lemma "x = (y\<Colon>bool bounded)"
   18.65 +nitpick [expect = genuine]
   18.66 +oops
   18.67 +
   18.68 +lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
   18.69 +nitpick [expect = none]
   18.70 +sorry
   18.71 +
   18.72 +lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
   18.73 +nitpick [card = 1\<midarrow>5, timeout = 10 s, expect = genuine]
   18.74 +oops
   18.75 +
   18.76 +lemma "True \<equiv> ((\<lambda>x\<Colon>bool. x) = (\<lambda>x. x))"
   18.77 +nitpick [expect = none]
   18.78 +by (rule True_def)
   18.79 +
   18.80 +lemma "False \<equiv> \<forall>P. P"
   18.81 +nitpick [expect = none]
   18.82 +by (rule False_def)
   18.83 +
   18.84 +lemma "() = Abs_unit True"
   18.85 +nitpick [expect = none]
   18.86 +by (rule Unity_def)
   18.87 +
   18.88 +lemma "() = Abs_unit False"
   18.89 +nitpick [expect = none]
   18.90 +by simp
   18.91 +
   18.92 +lemma "Rep_unit () = True"
   18.93 +nitpick [expect = none]
   18.94 +by (insert Rep_unit) (simp add: unit_def)
   18.95 +
   18.96 +lemma "Rep_unit () = False"
   18.97 +nitpick [expect = genuine]
   18.98 +oops
   18.99 +
  18.100 +lemma "Pair a b \<equiv> Abs_Prod (Pair_Rep a b)"
  18.101 +nitpick [card = 1\<midarrow>2, expect = none]
  18.102 +by (rule Pair_def)
  18.103 +
  18.104 +lemma "Pair a b \<equiv> Abs_Prod (Pair_Rep b a)"
  18.105 +nitpick [card = 1\<midarrow>2, expect = none]
  18.106 +nitpick [dont_box, expect = genuine]
  18.107 +oops
  18.108 +
  18.109 +lemma "fst (Abs_Prod (Pair_Rep a b)) = a"
  18.110 +nitpick [card = 2, expect = none]
  18.111 +by (simp add: Pair_def [THEN symmetric])
  18.112 +
  18.113 +lemma "fst (Abs_Prod (Pair_Rep a b)) = b"
  18.114 +nitpick [card = 1\<midarrow>2, expect = none]
  18.115 +nitpick [dont_box, expect = genuine]
  18.116 +oops
  18.117 +
  18.118 +lemma "a \<noteq> a' \<Longrightarrow> Pair_Rep a b \<noteq> Pair_Rep a' b"
  18.119 +nitpick [expect = none]
  18.120 +apply (rule ccontr)
  18.121 +apply simp
  18.122 +apply (drule subst [where P = "\<lambda>r. Abs_Prod r = Abs_Prod (Pair_Rep a b)"])
  18.123 + apply (rule refl)
  18.124 +by (simp add: Pair_def [THEN symmetric])
  18.125 +
  18.126 +lemma "Abs_Prod (Rep_Prod a) = a"
  18.127 +nitpick [card = 2, expect = none]
  18.128 +by (rule Rep_Prod_inverse)
  18.129 +
  18.130 +lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inl_Rep a)"
  18.131 +nitpick [card = 1, expect = none]
  18.132 +by (rule Inl_def)
  18.133 +
  18.134 +lemma "Inl \<equiv> \<lambda>a. Abs_Sum (Inr_Rep a)"
  18.135 +nitpick [card = 1, card "'a + 'a" = 2, expect = genuine]
  18.136 +oops
  18.137 +
  18.138 +lemma "Inl_Rep a \<noteq> Inr_Rep a"
  18.139 +nitpick [expect = none]
  18.140 +by (rule Inl_Rep_not_Inr_Rep)
  18.141 +
  18.142 +lemma "Abs_Sum (Rep_Sum a) = a"
  18.143 +nitpick [card = 1\<midarrow>2, timeout = 30 s, expect = none]
  18.144 +by (rule Rep_Sum_inverse)
  18.145 +
  18.146 +lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
  18.147 +nitpick [expect = none]
  18.148 +by (rule Zero_nat_def_raw)
  18.149 +
  18.150 +lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Rep_Nat n))"
  18.151 +nitpick [expect = none]
  18.152 +by (rule Suc_def)
  18.153 +
  18.154 +lemma "Suc \<equiv> \<lambda>n. Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
  18.155 +nitpick [expect = genuine]
  18.156 +oops
  18.157 +
  18.158 +lemma "Abs_Nat (Rep_Nat a) = a"
  18.159 +nitpick [expect = none]
  18.160 +by (rule Rep_Nat_inverse)
  18.161 +
  18.162 +lemma "0 \<equiv> Abs_Integ (intrel `` {(0, 0)})"
  18.163 +nitpick [card = 1\<midarrow>2, timeout = 30 s, max_potential = 0, expect = unknown]
  18.164 +by (rule Zero_int_def_raw)
  18.165 +
  18.166 +lemma "Abs_Integ (Rep_Integ a) = a"
  18.167 +nitpick [card = 1\<midarrow>2, timeout = 30 s, max_potential = 0, expect = none]
  18.168 +by (rule Rep_Integ_inverse)
  18.169 +
  18.170 +lemma "Abs_list (Rep_list a) = a"
  18.171 +nitpick [card = 1\<midarrow>2, timeout = 30 s, expect = none]
  18.172 +by (rule Rep_list_inverse)
  18.173 +
  18.174 +record point =
  18.175 +  Xcoord :: int
  18.176 +  Ycoord :: int
  18.177 +
  18.178 +lemma "Abs_point_ext_type (Rep_point_ext_type a) = a"
  18.179 +nitpick [expect = none]
  18.180 +by (rule Rep_point_ext_type_inverse)
  18.181 +
  18.182 +lemma "Fract a b = of_int a / of_int b"
  18.183 +nitpick [card = 1\<midarrow>2, expect = potential]
  18.184 +by (rule Fract_of_int_quotient)
  18.185 +
  18.186 +lemma "Abs_Rat (Rep_Rat a) = a"
  18.187 +nitpick [card = 1\<midarrow>2, expect = none]
  18.188 +by (rule Rep_Rat_inverse)
  18.189 +
  18.190 +end
    19.1 --- a/src/HOL/Rational.thy	Fri Oct 23 18:57:35 2009 +0200
    19.2 +++ b/src/HOL/Rational.thy	Fri Oct 23 18:59:24 2009 +0200
    19.3 @@ -1063,4 +1063,23 @@
    19.4  fun rat_of_int i = (i, 1);
    19.5  *}
    19.6  
    19.7 +setup {*
    19.8 +Nitpick.register_frac_type @{type_name rat}
    19.9 +    [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
   19.10 +     (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
   19.11 +     (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
   19.12 +     (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
   19.13 +     (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
   19.14 +     (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
   19.15 +     (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
   19.16 +     (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
   19.17 +     (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
   19.18 +     (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
   19.19 +*}
   19.20 +
   19.21 +lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
   19.22 +    number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
   19.23 +    plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
   19.24 +    zero_rat_inst.zero_rat
   19.25 +
   19.26  end
    20.1 --- a/src/HOL/RealDef.thy	Fri Oct 23 18:57:35 2009 +0200
    20.2 +++ b/src/HOL/RealDef.thy	Fri Oct 23 18:59:24 2009 +0200
    20.3 @@ -1185,4 +1185,22 @@
    20.4  fun real_of_int i = (i, 1);
    20.5  *}
    20.6  
    20.7 +setup {*
    20.8 +Nitpick.register_frac_type @{type_name real}
    20.9 +    [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
   20.10 +     (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
   20.11 +     (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
   20.12 +     (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
   20.13 +     (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
   20.14 +     (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
   20.15 +     (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
   20.16 +     (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
   20.17 +*}
   20.18 +
   20.19 +lemmas [nitpick_def] = inverse_real_inst.inverse_real
   20.20 +    number_real_inst.number_of_real one_real_inst.one_real
   20.21 +    ord_real_inst.less_eq_real plus_real_inst.plus_real
   20.22 +    times_real_inst.times_real uminus_real_inst.uminus_real
   20.23 +    zero_real_inst.zero_real
   20.24 +
   20.25  end
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Fri Oct 23 18:59:24 2009 +0200
    21.3 @@ -0,0 +1,155 @@
    21.4 +Version 2010
    21.5 +
    21.6 +  * Moved into Isabelle/HOL "Main"
    21.7 +  * Renamed "nitpick_const_def" to "nitpick_def", "nitpick_const_simp" to
    21.8 +    "nitpick_simp", "nitpick_const_psimp" to "nitpick_psimp", and
    21.9 +    "nitpick_ind_intro" to "nitpick_intro"
   21.10 +  * Replaced "special_depth" and "skolemize_depth" options by "specialize"
   21.11 +    and "skolemize"
   21.12 +  * Fixed monotonicity check
   21.13 +
   21.14 +Version 1.2.2 (16 Oct 2009)
   21.15 +
   21.16 +  * Added and implemented "star_linear_preds" option
   21.17 +  * Added and implemented "format" option
   21.18 +  * Added and implemented "coalesce_type_vars" option
   21.19 +  * Added and implemented "max_genuine" option
   21.20 +  * Fixed soundness issues related to "set", "distinct", "image", "Sigma",
   21.21 +    "-1::nat", subset, constructors, sort axioms, and partially applied
   21.22 +    interpreted constants
   21.23 +  * Fixed error in "show_consts" for boxed specialized constants
   21.24 +  * Fixed errors in Kodkod encoding of "The", "Eps", and "ind"
   21.25 +  * Fixed display of Skolem constants
   21.26 +  * Fixed error in "check_potential" and "check_genuine"
   21.27 +  * Added boxing support for higher-order constructor parameters
   21.28 +  * Changed notation used for coinductive datatypes
   21.29 +  * Optimized Kodkod encoding of "If", "card", and "setsum"
   21.30 +  * Improved the monotonicity check
   21.31 +
   21.32 +Version 1.2.1 (25 Sep 2009)
   21.33 +
   21.34 +  * Added explicit support for coinductive datatypes
   21.35 +  * Added and implemented "box" option
   21.36 +  * Added and implemented "fast_descrs" option
   21.37 +  * Added and implemented "uncurry" option
   21.38 +  * Renamed and generalized "sync_cards" and "inductive_mood" to "mono" and "wf"
   21.39 +  * Fixed soundness issue related to nullary constructors
   21.40 +  * Fixed soundness issue related to higher-order quantifiers
   21.41 +  * Fixed soundness issue related to the "destroy_constrs" optimization
   21.42 +  * Fixed soundness issues related to the "special_depth" optimization
   21.43 +  * Added support for PicoSAT and incorporated it with the Nitpick package
   21.44 +  * Added automatic detection of installed SAT solvers based on naming
   21.45 +    convention
   21.46 +  * Optimized handling of quantifiers by moving them inward whenever possible
   21.47 +  * Optimized and improved precision of "wf" and "wfrec"
   21.48 +  * Improved handling of definitions made in locales
   21.49 +  * Fixed checked scope count in message shown upon interruption and timeout
   21.50 +  * Added minimalistic Nitpick-like tool called Minipick
   21.51 +
   21.52 +Version 1.2.0 (27 Jul 2009)
   21.53 +
   21.54 +  * Optimized Kodkod encoding of datatypes and records
   21.55 +  * Optimized coinductive definitions
   21.56 +  * Fixed soundness issues related to pairs of functions
   21.57 +  * Fixed soundness issue in the peephole optimizer
   21.58 +  * Improved precision of non-well-founded predicates occurring positively in
   21.59 +    the formula to falsify
   21.60 +  * Added and implemented "destroy_constrs" option
   21.61 +  * Changed semantics of "inductive_mood" option to ensure soundness
   21.62 +  * Fixed semantics of "lockstep" option (broken in 1.1.1) and renamed it
   21.63 +    "sync_cards"
   21.64 +  * Improved precision of "trancl" and "rtrancl"
   21.65 +  * Optimized Kodkod encoding of "tranclp" and "rtranclp"
   21.66 +  * Made detection of inconsistent scope specifications more robust
   21.67 +  * Fixed a few Kodkod generation bugs that resulted in exceptions
   21.68 +
   21.69 +Version 1.1.1 (24 Jun 2009)
   21.70 +
   21.71 +  * Added "show_all" option
   21.72 +  * Fixed soundness issues related to type classes
   21.73 +  * Improved precision of some set constructs
   21.74 +  * Fiddled with the automatic monotonicity check
   21.75 +  * Fixed performance issues related to scope enumeration
   21.76 +  * Fixed a few Kodkod generation bugs that resulted in exceptions or stack
   21.77 +    overflows
   21.78 +
   21.79 +Version 1.1.0 (16 Jun 2009)
   21.80 +
   21.81 +  * Redesigned handling of datatypes to provide an interface baded on "card" and
   21.82 +    "max", obsoleting "mult"
   21.83 +  * Redesigned handling of typedefs, "rat", and "real"
   21.84 +  * Made "lockstep" option a three-state option and added an automatic
   21.85 +    monotonicity check
   21.86 +  * Made "batch_size" a (n + 1)-state option whose default depends on whether
   21.87 +    "debug" is enabled
   21.88 +  * Made "debug" automatically enable "verbose"
   21.89 +  * Added "destroy_equals" option
   21.90 +  * Added "no_assms" option
   21.91 +  * Fixed bug in computation of ground type 
   21.92 +  * Fixed performance issue related to datatype acyclicity constraint generation
   21.93 +  * Fixed performance issue related to axiom selection
   21.94 +  * Improved precision of some well-founded inductive predicates
   21.95 +  * Added more checks to guard against very large cardinalities
   21.96 +  * Improved hit rate of potential counterexamples
   21.97 +  * Fixed several soundness issues
   21.98 +  * Optimized the Kodkod encoding to benefit more from symmetry breaking
   21.99 +  * Optimized relational composition, cartesian product, and converse
  21.100 +  * Added support for HaifaSat
  21.101 +
  21.102 +Version 1.0.3 (17 Mar 2009)
  21.103 +
  21.104 +  * Added "HOL-Nominal-Nitpick" as a target in addition to "HOL-Nitpick"
  21.105 +  * Added "overlord" option to assist debugging
  21.106 +  * Increased default value of "special_depth" option
  21.107 +  * Fixed a bug that effectively disabled the "nitpick_const_def" attribute
  21.108 +  * Ensured that no scopes are skipped when multithreading is enabled
  21.109 +  * Fixed soundness issue in handling of "The", "Eps", and partial functions
  21.110 +    defined using Isabelle's function package
  21.111 +  * Fixed soundness issue in handling of non-definitional axioms
  21.112 +  * Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
  21.113 +    "nat", "int", and "*"
  21.114 +  * Fixed a few Kodkod generation bugs that resulted in exceptions
  21.115 +  * Optimized "div", "mod", and "dvd" on "nat" and "int"
  21.116 +
  21.117 +Version 1.0.2 (12 Mar 2009)
  21.118 +
  21.119 +  * Added support for non-definitional axioms
  21.120 +  * Improved Isar integration
  21.121 +  * Added support for multiplicities of 0
  21.122 +  * Added "max_threads" option and support for multithreaded Kodkodi
  21.123 +  * Added "blocking" option to control whether Nitpick should be run
  21.124 +    synchronously or asynchronously
  21.125 +  * Merged "auto_timeout" and "wellfounded_timeout" into "tac_timeout"
  21.126 +  * Added "auto" option to run Nitpick automatically (like Auto Quickcheck)
  21.127 +  * Introduced "auto_timeout" to specify Auto Nitpick's time limit
  21.128 +  * Renamed the possible values for the "expect" option
  21.129 +  * Renamed the "peephole" option to "peephole_optim"
  21.130 +  * Added negative versions of all Boolean options and made "= true" optional
  21.131 +  * Altered order of automatic SAT solver selection
  21.132 +
  21.133 +Version 1.0.1 (6 Mar 2009)
  21.134 +
  21.135 +  * Eliminated the need to import "Nitpick" to use "nitpick"
  21.136 +  * Added "debug" option
  21.137 +  * Replaced "specialize_funs" with the more general "special_depth" option
  21.138 +  * Renamed "watch" option to "eval"
  21.139 +  * Improved parsing of "card", "mult", and "iter" options
  21.140 +  * Fixed a soundness bug in the "specialize_funs" optimization
  21.141 +  * Increased the scope of the "specialize_funs" optimization
  21.142 +  * Fixed a soundness bug in the treatment of "<" and "<=" on type "int"
  21.143 +  * Fixed a soundness bug in the "subterm property" optimization for types of
  21.144 +    cardinality 1
  21.145 +  * Improved the axiom selection for overloaded constants, which led to an
  21.146 +    infinite loop for "Nominal.perm"
  21.147 +  * Added support for multiple instantiations of non-well-founded inductive
  21.148 +    predicates, which previously raised an exception
  21.149 +  * Fixed a Kodkod generation bug that resulted in an exception
  21.150 +  * Altered order of scope enumeration and automatic SAT solver selection
  21.151 +  * Optimized "Eps", "nat_case", and "list_case"
  21.152 +  * Improved output formatting
  21.153 +  * Added checks to prevent infinite loops in axiom selector and constant
  21.154 +    unfolding
  21.155 +
  21.156 +Version 1.0.0 (27 Feb 2009)
  21.157 +
  21.158 +  * First release
    22.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 23 18:57:35 2009 +0200
    22.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 23 18:59:24 2009 +0200
    22.3 @@ -970,15 +970,14 @@
    22.4                           $ Const (@{const_name TYPE}, _)) = true
    22.5    | is_arity_type_axiom _ = false
    22.6  (* theory -> bool -> term -> bool *)
    22.7 -fun is_typedef_axiom thy only_boring (@{const "==>"} $ _ $ t2) =
    22.8 -    is_typedef_axiom thy only_boring t2
    22.9 -  | is_typedef_axiom thy only_boring
   22.10 +fun is_typedef_axiom thy boring (@{const "==>"} $ _ $ t2) =
   22.11 +    is_typedef_axiom thy boring t2
   22.12 +  | is_typedef_axiom thy boring
   22.13          (@{const Trueprop} $ (Const (@{const_name Typedef.type_definition}, _)
   22.14 -         $ Const (_, Type ("fun", [T as Type (s, _), _])) $ Const _ $ _)) =
   22.15 -    is_typedef thy s
   22.16 -    andalso not (only_boring andalso
   22.17 -                 (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]
   22.18 -                  orelse is_frac_type thy T))
   22.19 +         $ Const (_, Type ("fun", [Type (s, _), _])) $ Const _ $ _)) =
   22.20 +    boring <> (s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"}]
   22.21 +               orelse is_frac_type thy (Type (s, [])))
   22.22 +    andalso is_typedef thy s
   22.23    | is_typedef_axiom _ _ _ = false
   22.24  
   22.25  (* Distinguishes between (1) constant definition axioms, (2) type arity and
   22.26 @@ -995,8 +994,8 @@
   22.27        |> filter_out ((is_arity_type_axiom orf is_typedef_axiom thy true) o snd)
   22.28    in pairself (map snd) (defs, nondefs) end
   22.29  
   22.30 -(* Ideally we would check against "Complex_Main", not "Quickcheck", but any
   22.31 -   theory will do as long as it contains all the "axioms" and "axiomatization"
   22.32 +(* Ideally we would check against "Complex_Main", not "Refute", but any theory
   22.33 +   will do as long as it contains all the "axioms" and "axiomatization"
   22.34     commands. *)
   22.35  (* theory -> bool *)
   22.36  fun is_built_in_theory thy = Theory.subthy (thy, @{theory Refute})
   22.37 @@ -1040,18 +1039,20 @@
   22.38      (* theory list -> term list *)
   22.39      val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
   22.40      val specs = Defs.all_specifications_of (Theory.defs_of thy)
   22.41 -    val def_names =
   22.42 -      specs |> maps snd
   22.43 -      |> filter #is_def |> map #name |> OrdList.make fast_string_ord
   22.44 +    val def_names = specs |> maps snd |> filter #is_def |> map #name
   22.45 +                    |> OrdList.make fast_string_ord
   22.46      val thys = thy :: Theory.ancestors_of thy
   22.47      val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
   22.48      val built_in_axioms = axioms_of_thys built_in_thys
   22.49      val user_axioms = axioms_of_thys user_thys
   22.50      val (built_in_defs, built_in_nondefs) =
   22.51        partition_axioms_by_definitionality thy built_in_axioms def_names
   22.52 -      |> apsnd (filter (is_typedef_axiom thy false))
   22.53 +      ||> filter (is_typedef_axiom thy false)
   22.54      val (user_defs, user_nondefs) =
   22.55        partition_axioms_by_definitionality thy user_axioms def_names
   22.56 +    val (built_in_nondefs, user_nondefs) =
   22.57 +      List.partition (is_typedef_axiom thy false) user_nondefs
   22.58 +      |>> append built_in_nondefs
   22.59      val defs = built_in_built_in_defs @
   22.60                 (thy |> PureThy.all_thms_of
   22.61                      |> filter (equal Thm.definitionK o Thm.get_kind o snd)
   22.62 @@ -1230,30 +1231,31 @@
   22.63  (* Similar to "Refute.specialize_type" but returns all matches rather than only
   22.64     the first (preorder) match. *)
   22.65  (* theory -> styp -> term -> term list *)
   22.66 -fun multi_specialize_type thy (x as (s, T)) t =
   22.67 +fun multi_specialize_type thy slack (x as (s, T)) t =
   22.68    let
   22.69      (* term -> (typ * term) list -> (typ * term) list *)
   22.70      fun aux (Const (s', T')) ys =
   22.71          if s = s' then
   22.72 -          (if AList.defined (op =) ys T' then
   22.73 -             I
   22.74 -           else if T = T' then
   22.75 -             cons (T, t)
   22.76 -           else
   22.77 -             cons (T', Refute.monomorphic_term
   22.78 -                           (Sign.typ_match thy (T', T) Vartab.empty) t)
   22.79 -             handle Type.TYPE_MATCH => I) ys
   22.80 +          ys |> (if AList.defined (op =) ys T' then
   22.81 +                   I
   22.82 +                else
   22.83 +                  cons (T', Refute.monomorphic_term
   22.84 +                                (Sign.typ_match thy (T', T) Vartab.empty) t)
   22.85 +                  handle Type.TYPE_MATCH => I
   22.86 +                       | Refute.REFUTE _ =>
   22.87 +                         if slack then
   22.88 +                           I
   22.89 +                         else
   22.90 +                           raise NOT_SUPPORTED ("too much polymorphism in \
   22.91 +                                                \axiom involving " ^ quote s))
   22.92          else
   22.93            ys
   22.94        | aux _ ys = ys
   22.95    in map snd (fold_aterms aux t []) end
   22.96  
   22.97 -(* theory -> const_table -> styp -> term list *)
   22.98 -fun nondef_props_for_const thy table (x as (s, _)) =
   22.99 -  these (Symtab.lookup table s) |> maps (multi_specialize_type thy x)
  22.100 -  handle Refute.REFUTE _ =>
  22.101 -         raise NOT_SUPPORTED ("too much polymorphism in axiom involving " ^
  22.102 -                              quote s)
  22.103 +(* theory -> bool -> const_table -> styp -> term list *)
  22.104 +fun nondef_props_for_const thy slack table (x as (s, _)) =
  22.105 +  these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
  22.106  
  22.107  (* theory -> styp list -> term list *)
  22.108  fun optimized_typedef_axioms thy (abs_s, abs_Ts) =
  22.109 @@ -1680,7 +1682,7 @@
  22.110          (x as (s, _)) =
  22.111    case triple_lookup (const_match thy) wfs x of
  22.112      SOME (SOME b) => b
  22.113 -  | _ => s = @{const_name fold_graph'}
  22.114 +  | _ => s mem [@{const_name Nats}, @{const_name fold_graph'}]
  22.115           orelse case AList.lookup (op =) (!wf_cache) x of
  22.116                    SOME (_, wf) => wf
  22.117                  | NONE =>
  22.118 @@ -3025,15 +3027,15 @@
  22.119                      accum
  22.120               else if is_abs_fun thy x then
  22.121                 accum |> fold (add_nondef_axiom depth)
  22.122 -                             (nondef_props_for_const thy nondef_table x)
  22.123 +                             (nondef_props_for_const thy false nondef_table x)
  22.124                       |> fold (add_def_axiom depth)
  22.125 -                             (nondef_props_for_const thy
  22.126 +                             (nondef_props_for_const thy true
  22.127                                                      (extra_table def_table s) x)
  22.128               else if is_rep_fun thy x then
  22.129                 accum |> fold (add_nondef_axiom depth)
  22.130 -                             (nondef_props_for_const thy nondef_table x)
  22.131 +                             (nondef_props_for_const thy false nondef_table x)
  22.132                       |> fold (add_def_axiom depth)
  22.133 -                             (nondef_props_for_const thy
  22.134 +                             (nondef_props_for_const thy true
  22.135                                                      (extra_table def_table s) x)
  22.136                       |> add_axioms_for_term depth
  22.137                                              (Const (mate_of_rep_fun thy x))
  22.138 @@ -3041,7 +3043,7 @@
  22.139               else
  22.140                 accum |> user_axioms <> SOME false
  22.141                          ? fold (add_nondef_axiom depth)
  22.142 -                               (nondef_props_for_const thy nondef_table x)
  22.143 +                               (nondef_props_for_const thy false nondef_table x)
  22.144             end)
  22.145          |> add_axioms_for_type depth T
  22.146        | Free (_, T) => add_axioms_for_type depth T accum
    23.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Oct 23 18:57:35 2009 +0200
    23.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Oct 23 18:59:24 2009 +0200
    23.3 @@ -55,11 +55,7 @@
    23.4     ("max_threads", ["0"]),
    23.5     ("verbose", ["false"]),
    23.6     ("debug", ["false"]),
    23.7 -   ("overlord", [if exists (fn s => String.isSuffix s (getenv "HOME"))
    23.8 -                           ["blanchet", "blanchette"] then
    23.9 -                   "true"
   23.10 -                 else
   23.11 -                   "false"]),
   23.12 +   ("overlord", ["false"]),
   23.13     ("show_all", ["false"]),
   23.14     ("show_skolems", ["true"]),
   23.15     ("show_datatypes", ["false"]),