src/HOL/Nitpick_Examples/Typedef_Nits.thy
author wenzelm
Tue Oct 10 19:23:03 2017 +0200 (2017-10-10)
changeset 66831 29ea2b900a05
parent 63167 0909deb8059b
permissions -rw-r--r--
tuned: each session has at most one defining entry;
     1 (*  Title:      HOL/Nitpick_Examples/Typedef_Nits.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2009-2011
     4 
     5 Examples featuring Nitpick applied to typedefs.
     6 *)
     7 
     8 section \<open>Examples Featuring Nitpick Applied to Typedefs\<close>
     9 
    10 theory Typedef_Nits
    11 imports Complex_Main
    12 begin
    13 
    14 nitpick_params [verbose, card = 1-4, sat_solver = MiniSat_JNI, max_threads = 1,
    15                 timeout = 240]
    16 
    17 definition "three = {0::nat, 1, 2}"
    18 typedef three = three
    19 unfolding three_def by blast
    20 
    21 definition A :: three where "A \<equiv> Abs_three 0"
    22 definition B :: three where "B \<equiv> Abs_three 1"
    23 definition C :: three where "C \<equiv> Abs_three 2"
    24 
    25 lemma "x = (y::three)"
    26 nitpick [expect = genuine]
    27 oops
    28 
    29 definition "one_or_two = {undefined False::'a, undefined True}"
    30 
    31 typedef 'a one_or_two = "one_or_two :: 'a set"
    32 unfolding one_or_two_def by auto
    33 
    34 lemma "x = (y::unit one_or_two)"
    35 nitpick [expect = none]
    36 sorry
    37 
    38 lemma "x = (y::bool one_or_two)"
    39 nitpick [expect = genuine]
    40 oops
    41 
    42 lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> x = (y::bool one_or_two)"
    43 nitpick [expect = none]
    44 sorry
    45 
    46 lemma "undefined False \<longleftrightarrow> undefined True \<Longrightarrow> \<exists>x (y::bool one_or_two). x \<noteq> y"
    47 nitpick [card = 1, expect = potential] (* unfortunate *)
    48 oops
    49 
    50 lemma "\<exists>x (y::bool one_or_two). x \<noteq> y"
    51 nitpick [card = 1, expect = potential] (* unfortunate *)
    52 nitpick [card = 2, expect = none]
    53 oops
    54 
    55 definition "bounded = {n::nat. finite (UNIV :: 'a set) \<longrightarrow> n < card (UNIV :: 'a set)}"
    56 
    57 typedef 'a bounded = "bounded(TYPE('a))"
    58 unfolding bounded_def
    59 apply (rule_tac x = 0 in exI)
    60 apply (case_tac "card UNIV = 0")
    61 by auto
    62 
    63 lemma "x = (y::unit bounded)"
    64 nitpick [expect = none]
    65 sorry
    66 
    67 lemma "x = (y::bool bounded)"
    68 nitpick [expect = genuine]
    69 oops
    70 
    71 lemma "x \<noteq> (y::bool bounded) \<Longrightarrow> z = x \<or> z = y"
    72 nitpick [expect = potential] (* unfortunate *)
    73 sorry
    74 
    75 lemma "x \<noteq> (y::(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
    76 nitpick [card = 1-5, expect = genuine]
    77 oops
    78 
    79 lemma "True \<equiv> ((\<lambda>x::bool. x) = (\<lambda>x. x))"
    80 nitpick [expect = none]
    81 by (rule True_def)
    82 
    83 lemma "False \<equiv> \<forall>P. P"
    84 nitpick [expect = none]
    85 by (rule False_def)
    86 
    87 lemma "() = Abs_unit True"
    88 nitpick [expect = none]
    89 by (rule Unity_def)
    90 
    91 lemma "() = Abs_unit False"
    92 nitpick [expect = none]
    93 by simp
    94 
    95 lemma "Rep_unit () = True"
    96 nitpick [expect = none]
    97 by (insert Rep_unit) simp
    98 
    99 lemma "Rep_unit () = False"
   100 nitpick [expect = genuine]
   101 oops
   102 
   103 lemma "Pair a b = Abs_prod (Pair_Rep a b)"
   104 nitpick [card = 1-2, expect = none]
   105 by (rule Pair_def)
   106 
   107 lemma "Pair a b = Abs_prod (Pair_Rep b a)"
   108 nitpick [card = 1-2, expect = none]
   109 nitpick [dont_box, expect = genuine]
   110 oops
   111 
   112 lemma "fst (Abs_prod (Pair_Rep a b)) = a"
   113 nitpick [card = 2, expect = none]
   114 by (simp add: Pair_def [THEN sym])
   115 
   116 lemma "fst (Abs_prod (Pair_Rep a b)) = b"
   117 nitpick [card = 1-2, expect = none]
   118 nitpick [dont_box, expect = genuine]
   119 oops
   120 
   121 lemma "a \<noteq> a' \<Longrightarrow> Pair_Rep a b \<noteq> Pair_Rep a' b"
   122 nitpick [expect = none]
   123 apply (rule ccontr)
   124 apply simp
   125 apply (drule subst [where P = "\<lambda>r. Abs_prod r = Abs_prod (Pair_Rep a b)"])
   126  apply (rule refl)
   127 by (simp add: Pair_def [THEN sym])
   128 
   129 lemma "Abs_prod (Rep_prod a) = a"
   130 nitpick [card = 2, expect = none]
   131 by (rule Rep_prod_inverse)
   132 
   133 lemma "Inl \<equiv> \<lambda>a. Abs_sum (Inl_Rep a)"
   134 nitpick [card = 1, expect = none]
   135 by (simp add: Inl_def o_def)
   136 
   137 lemma "Inl \<equiv> \<lambda>a. Abs_sum (Inr_Rep a)"
   138 nitpick [card = 1, card "'a + 'a" = 2, expect = genuine]
   139 oops
   140 
   141 lemma "Inl_Rep a \<noteq> Inr_Rep a"
   142 nitpick [expect = none]
   143 by (rule Inl_Rep_not_Inr_Rep)
   144 
   145 lemma "Abs_sum (Rep_sum a) = a"
   146 nitpick [card = 1, expect = none]
   147 nitpick [card = 2, expect = none]
   148 by (rule Rep_sum_inverse)
   149 
   150 lemma "0::nat \<equiv> Abs_Nat Zero_Rep"
   151 nitpick [expect = none]
   152 by (rule Zero_nat_def [abs_def])
   153 
   154 lemma "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"
   155 nitpick [expect = none]
   156 by (rule Nat.Suc_def)
   157 
   158 lemma "Suc n = Abs_Nat (Suc_Rep (Suc_Rep (Rep_Nat n)))"
   159 nitpick [expect = genuine]
   160 oops
   161 
   162 lemma "Abs_Nat (Rep_Nat a) = a"
   163 nitpick [expect = none]
   164 by (rule Rep_Nat_inverse)
   165 
   166 lemma "Abs_list (Rep_list a) = a"
   167 (* nitpick [card = 1-2, expect = none] FIXME *)
   168 by (rule Rep_list_inverse)
   169 
   170 record point =
   171   Xcoord :: int
   172   Ycoord :: int
   173 
   174 lemma "Abs_point_ext (Rep_point_ext a) = a"
   175 nitpick [expect = none]
   176 by (fact Rep_point_ext_inverse)
   177 
   178 lemma "Fract a b = of_int a / of_int b"
   179 nitpick [card = 1, expect = none]
   180 by (rule Fract_of_int_quotient)
   181 
   182 lemma "Abs_rat (Rep_rat a) = a"
   183 nitpick [card = 1, expect = none]
   184 by (rule Rep_rat_inverse)
   185 
   186 typedef check = "{x::nat. x < 2}" by (rule exI[of _ 0], auto)
   187 
   188 lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 2"
   189 nitpick [card = 1-3, expect = none]
   190 using Rep_check[of "Abs_check n"] by auto
   191 
   192 lemma "Rep_check (Abs_check n) = n \<Longrightarrow> n < 1"
   193 nitpick [card = 1-3, expect = genuine]
   194 oops
   195 
   196 end