src/HOL/Nitpick_Examples/Mini_Nits.thy
changeset 42415 10accf397ab6
parent 42414 9465651c0db7
child 42417 574393cb3d9d
child 42418 508acf776ebf
     1.1 --- a/src/HOL/Nitpick_Examples/Mini_Nits.thy	Tue Apr 19 12:22:59 2011 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,108 +0,0 @@
     1.4 -(*  Title:      HOL/Nitpick_Examples/Mini_Nits.thy
     1.5 -    Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2009, 2010
     1.7 -
     1.8 -Examples featuring Minipick, the minimalistic version of Nitpick.
     1.9 -*)
    1.10 -
    1.11 -header {* Examples Featuring Minipick, the Minimalistic Version of Nitpick *}
    1.12 -
    1.13 -theory Mini_Nits
    1.14 -imports Main
    1.15 -begin
    1.16 -
    1.17 -ML {*
    1.18 -exception FAIL
    1.19 -
    1.20 -val has_kodkodi = (getenv "KODKODI" <> "")
    1.21 -
    1.22 -fun minipick n t =
    1.23 -  map (fn k => Minipick.kodkod_problem_from_term @{context} (K k) t) (1 upto n)
    1.24 -  |> Minipick.solve_any_kodkod_problem @{theory}
    1.25 -fun minipick_expect expect n t =
    1.26 -  if has_kodkodi then
    1.27 -    if minipick n t = expect then () else raise FAIL
    1.28 -  else
    1.29 -    ()
    1.30 -val none = minipick_expect "none"
    1.31 -val genuine = minipick_expect "genuine"
    1.32 -val unknown = minipick_expect "unknown"
    1.33 -*}
    1.34 -
    1.35 -ML {* genuine 1 @{prop "x = Not"} *}
    1.36 -ML {* none 1 @{prop "\<exists>x. x = Not"} *}
    1.37 -ML {* none 1 @{prop "\<not> False"} *}
    1.38 -ML {* genuine 1 @{prop "\<not> True"} *}
    1.39 -ML {* none 1 @{prop "\<not> \<not> b \<longleftrightarrow> b"} *}
    1.40 -ML {* none 1 @{prop True} *}
    1.41 -ML {* genuine 1 @{prop False} *}
    1.42 -ML {* genuine 1 @{prop "True \<longleftrightarrow> False"} *}
    1.43 -ML {* none 1 @{prop "True \<longleftrightarrow> \<not> False"} *}
    1.44 -ML {* none 5 @{prop "\<forall>x. x = x"} *}
    1.45 -ML {* none 5 @{prop "\<exists>x. x = x"} *}
    1.46 -ML {* none 1 @{prop "\<forall>x. x = y"} *}
    1.47 -ML {* genuine 2 @{prop "\<forall>x. x = y"} *}
    1.48 -ML {* none 1 @{prop "\<exists>x. x = y"} *}
    1.49 -ML {* none 2 @{prop "\<exists>x. x = y"} *}
    1.50 -ML {* none 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = x"} *}
    1.51 -ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
    1.52 -ML {* genuine 2 @{prop "\<forall>x\<Colon>'a \<times> 'a. x = y"} *}
    1.53 -ML {* none 2 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y"} *}
    1.54 -ML {* none 1 @{prop "All = Ex"} *}
    1.55 -ML {* genuine 2 @{prop "All = Ex"} *}
    1.56 -ML {* none 1 @{prop "All P = Ex P"} *}
    1.57 -ML {* genuine 2 @{prop "All P = Ex P"} *}
    1.58 -ML {* none 5 @{prop "x = y \<longrightarrow> P x = P y"} *}
    1.59 -ML {* none 5 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x = P y"} *}
    1.60 -ML {* none 2 @{prop "(x\<Colon>'a \<times> 'a) = y \<longrightarrow> P x y = P y x"} *}
    1.61 -ML {* none 5 @{prop "\<exists>x\<Colon>'a \<times> 'a. x = y \<longrightarrow> P x = P y"} *}
    1.62 -ML {* none 2 @{prop "(x\<Colon>'a \<Rightarrow> 'a) = y \<longrightarrow> P x = P y"} *}
    1.63 -ML {* none 2 @{prop "\<exists>x\<Colon>'a \<Rightarrow> 'a. x = y \<longrightarrow> P x = P y"} *}
    1.64 -ML {* genuine 1 @{prop "(op =) X = Ex"} *}
    1.65 -ML {* none 2 @{prop "\<forall>x::'a \<Rightarrow> 'a. x = x"} *}
    1.66 -ML {* none 1 @{prop "x = y"} *}
    1.67 -ML {* genuine 1 @{prop "x \<longleftrightarrow> y"} *}
    1.68 -ML {* genuine 2 @{prop "x = y"} *}
    1.69 -ML {* genuine 1 @{prop "X \<subseteq> Y"} *}
    1.70 -ML {* none 1 @{prop "P \<and> Q \<longleftrightarrow> Q \<and> P"} *}
    1.71 -ML {* none 1 @{prop "P \<and> Q \<longrightarrow> P"} *}
    1.72 -ML {* none 1 @{prop "P \<or> Q \<longleftrightarrow> Q \<or> P"} *}
    1.73 -ML {* genuine 1 @{prop "P \<or> Q \<longrightarrow> P"} *}
    1.74 -ML {* none 1 @{prop "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"} *}
    1.75 -ML {* none 5 @{prop "{a} = {a, a}"} *}
    1.76 -ML {* genuine 2 @{prop "{a} = {a, b}"} *}
    1.77 -ML {* genuine 1 @{prop "{a} \<noteq> {a, b}"} *}
    1.78 -ML {* none 5 @{prop "{}\<^sup>+ = {}"} *}
    1.79 -ML {* none 1 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.80 -ML {* genuine 2 @{prop "{(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.81 -ML {* none 5 @{prop "a \<noteq> c \<Longrightarrow> {(a, b), (b, c)}\<^sup>+ = {(a, b), (a, c), (b, c)}"} *}
    1.82 -ML {* none 5 @{prop "A \<union> B = (\<lambda>x. A x \<or> B x)"} *}
    1.83 -ML {* none 5 @{prop "A \<inter> B = (\<lambda>x. A x \<and> B x)"} *}
    1.84 -ML {* none 5 @{prop "A - B = (\<lambda>x. A x \<and> \<not> B x)"} *}
    1.85 -ML {* none 5 @{prop "\<exists>a b. (a, b) = (b, a)"} *}
    1.86 -ML {* genuine 2 @{prop "(a, b) = (b, a)"} *}
    1.87 -ML {* genuine 2 @{prop "(a, b) \<noteq> (b, a)"} *}
    1.88 -ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a. (a, b) = (b, a)"} *}
    1.89 -ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a, b) = (b, a)"} *}
    1.90 -ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<times> 'a \<times> 'a. (a, b) = (b, a)"} *}
    1.91 -ML {* genuine 2 @{prop "(a\<Colon>'a \<times> 'a \<times> 'a, b) \<noteq> (b, a)"} *}
    1.92 -ML {* none 5 @{prop "\<exists>a b\<Colon>'a \<Rightarrow> 'a. (a, b) = (b, a)"} *}
    1.93 -ML {* genuine 1 @{prop "(a\<Colon>'a \<Rightarrow> 'a, b) \<noteq> (b, a)"} *}
    1.94 -ML {* none 5 @{prop "fst (a, b) = a"} *}
    1.95 -ML {* none 1 @{prop "fst (a, b) = b"} *}
    1.96 -ML {* genuine 2 @{prop "fst (a, b) = b"} *}
    1.97 -ML {* genuine 2 @{prop "fst (a, b) \<noteq> b"} *}
    1.98 -ML {* none 5 @{prop "snd (a, b) = b"} *}
    1.99 -ML {* none 1 @{prop "snd (a, b) = a"} *}
   1.100 -ML {* genuine 2 @{prop "snd (a, b) = a"} *}
   1.101 -ML {* genuine 2 @{prop "snd (a, b) \<noteq> a"} *}
   1.102 -ML {* genuine 1 @{prop P} *}
   1.103 -ML {* genuine 1 @{prop "(\<lambda>x. P) a"} *}
   1.104 -ML {* genuine 1 @{prop "(\<lambda>x y z. P y x z) a b c"} *}
   1.105 -ML {* none 5 @{prop "\<exists>f. f = (\<lambda>x. x) \<and> f y = y"} *}
   1.106 -ML {* genuine 1 @{prop "\<exists>f. f p \<noteq> p \<and> (\<forall>a b. f (a, b) = (a, b))"} *}
   1.107 -ML {* none 2 @{prop "\<exists>f. \<forall>a b. f (a, b) = (a, b)"} *}
   1.108 -ML {* none 3 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (y, x)"} *}
   1.109 -ML {* genuine 2 @{prop "f = (\<lambda>a b. (b, a)) \<longrightarrow> f x y = (x, y)"} *}
   1.110 -
   1.111 -end