extending code_int type more; adding narrowing instance for type int; added test case for int instance
authorbulwahn
Fri Mar 18 18:19:42 2011 +0100 (2011-03-18)
changeset 4202152551c0a3374
parent 42020 2da02764d523
child 42022 101ce92333f4
extending code_int type more; adding narrowing instance for type int; added test case for int instance
src/HOL/Library/Quickcheck_Narrowing.thy
src/HOL/ex/Quickcheck_Narrowing_Examples.thy
     1.1 --- a/src/HOL/Library/Quickcheck_Narrowing.thy	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -25,15 +25,67 @@
     1.4  typedef (open) code_int = "UNIV \<Colon> int set"
     1.5    morphisms int_of of_int by rule
     1.6  
     1.7 +lemma of_int_int_of [simp]:
     1.8 +  "of_int (int_of k) = k"
     1.9 +  by (rule int_of_inverse)
    1.10 +
    1.11 +lemma int_of_of_int [simp]:
    1.12 +  "int_of (of_int n) = n"
    1.13 +  by (rule of_int_inverse) (rule UNIV_I)
    1.14 +
    1.15 +lemma code_int:
    1.16 +  "(\<And>n\<Colon>code_int. PROP P n) \<equiv> (\<And>n\<Colon>int. PROP P (of_int n))"
    1.17 +proof
    1.18 +  fix n :: int
    1.19 +  assume "\<And>n\<Colon>code_int. PROP P n"
    1.20 +  then show "PROP P (of_int n)" .
    1.21 +next
    1.22 +  fix n :: code_int
    1.23 +  assume "\<And>n\<Colon>int. PROP P (of_int n)"
    1.24 +  then have "PROP P (of_int (int_of n))" .
    1.25 +  then show "PROP P n" by simp
    1.26 +qed
    1.27 +
    1.28 +
    1.29  lemma int_of_inject [simp]:
    1.30    "int_of k = int_of l \<longleftrightarrow> k = l"
    1.31    by (rule int_of_inject)
    1.32  
    1.33 +lemma of_int_inject [simp]:
    1.34 +  "of_int n = of_int m \<longleftrightarrow> n = m"
    1.35 +  by (rule of_int_inject) (rule UNIV_I)+
    1.36 +
    1.37 +instantiation code_int :: equal
    1.38 +begin
    1.39 +
    1.40 +definition
    1.41 +  "HOL.equal k l \<longleftrightarrow> HOL.equal (int_of k) (int_of l)"
    1.42 +
    1.43 +instance proof
    1.44 +qed (auto simp add: equal_code_int_def equal_int_def eq_int_refl)
    1.45 +
    1.46 +end
    1.47 +
    1.48 +instantiation code_int :: number
    1.49 +begin
    1.50 +
    1.51 +definition
    1.52 +  "number_of = of_int"
    1.53 +
    1.54 +instance ..
    1.55 +
    1.56 +end
    1.57 +
    1.58 +lemma int_of_number [simp]:
    1.59 +  "int_of (number_of k) = number_of k"
    1.60 +  by (simp add: number_of_code_int_def number_of_is_id)
    1.61 +
    1.62 +
    1.63  definition nat_of :: "code_int => nat"
    1.64  where
    1.65    "nat_of i = nat (int_of i)"
    1.66  
    1.67 -instantiation code_int :: "{zero, one, minus, linorder}"
    1.68 +instantiation code_int :: "{minus, linordered_semidom, semiring_div, linorder}"
    1.69  begin
    1.70  
    1.71  definition [simp, code del]:
    1.72 @@ -43,16 +95,29 @@
    1.73    "1 = of_int 1"
    1.74  
    1.75  definition [simp, code del]:
    1.76 +  "n + m = of_int (int_of n + int_of m)"
    1.77 +
    1.78 +definition [simp, code del]:
    1.79    "n - m = of_int (int_of n - int_of m)"
    1.80  
    1.81  definition [simp, code del]:
    1.82 +  "n * m = of_int (int_of n * int_of m)"
    1.83 +
    1.84 +definition [simp, code del]:
    1.85 +  "n div m = of_int (int_of n div int_of m)"
    1.86 +
    1.87 +definition [simp, code del]:
    1.88 +  "n mod m = of_int (int_of n mod int_of m)"
    1.89 +
    1.90 +definition [simp, code del]:
    1.91    "n \<le> m \<longleftrightarrow> int_of n \<le> int_of m"
    1.92  
    1.93  definition [simp, code del]:
    1.94    "n < m \<longleftrightarrow> int_of n < int_of m"
    1.95  
    1.96  
    1.97 -instance proof qed (auto)
    1.98 +instance proof
    1.99 +qed (auto simp add: code_int left_distrib zmult_zless_mono2)
   1.100  
   1.101  end
   1.102  (*
   1.103 @@ -69,6 +134,40 @@
   1.104    using one_code_numeral_code ..
   1.105  *)
   1.106  
   1.107 +definition div_mod_code_int :: "code_int \<Rightarrow> code_int \<Rightarrow> code_int \<times> code_int" where
   1.108 +  [code del]: "div_mod_code_int n m = (n div m, n mod m)"
   1.109 +
   1.110 +lemma [code]:
   1.111 +  "div_mod_code_int n m = (if m = 0 then (0, n) else (n div m, n mod m))"
   1.112 +  unfolding div_mod_code_int_def by auto
   1.113 +
   1.114 +lemma [code]:
   1.115 +  "n div m = fst (div_mod_code_int n m)"
   1.116 +  unfolding div_mod_code_int_def by simp
   1.117 +
   1.118 +lemma [code]:
   1.119 +  "n mod m = snd (div_mod_code_int n m)"
   1.120 +  unfolding div_mod_code_int_def by simp
   1.121 +
   1.122 +lemma int_of_code [code]:
   1.123 +  "int_of k = (if k = 0 then 0
   1.124 +    else (if k mod 2 = 0 then 2 * int_of (k div 2) else 2 * int_of (k div 2) + 1))"
   1.125 +proof -
   1.126 +  have 1: "(int_of k div 2) * 2 + int_of k mod 2 = int_of k" 
   1.127 +    by (rule mod_div_equality)
   1.128 +  have "int_of k mod 2 = 0 \<or> int_of k mod 2 = 1" by auto
   1.129 +  from this show ?thesis
   1.130 +    apply auto
   1.131 +    apply (insert 1) by (auto simp add: mult_ac)
   1.132 +qed
   1.133 +
   1.134 +
   1.135 +code_instance code_numeral :: equal
   1.136 +  (Haskell -)
   1.137 +
   1.138 +setup {* fold (Numeral.add_code @{const_name number_code_int_inst.number_of_code_int}
   1.139 +  false Code_Printer.literal_numeral) ["Haskell"]  *}
   1.140 +
   1.141  code_const "0 \<Colon> code_int"
   1.142    (Haskell "0")
   1.143  
   1.144 @@ -78,6 +177,12 @@
   1.145  code_const "minus \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> code_int"
   1.146    (Haskell "(_/ -/ _)")
   1.147  
   1.148 +code_const div_mod_code_int
   1.149 +  (Haskell "divMod")
   1.150 +
   1.151 +code_const "HOL.equal \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
   1.152 +  (Haskell infix 4 "==")
   1.153 +
   1.154  code_const "op \<le> \<Colon> code_int \<Rightarrow> code_int \<Rightarrow> bool"
   1.155    (Haskell infix 4 "<=")
   1.156  
   1.157 @@ -87,6 +192,8 @@
   1.158  code_type code_int
   1.159    (Haskell "Int")
   1.160  
   1.161 +code_abort of_int
   1.162 +
   1.163  subsubsection {* Narrowing's deep representation of types and terms *}
   1.164  
   1.165  datatype type = SumOfProd "type list list"
   1.166 @@ -207,7 +314,20 @@
   1.167  definition cons2 :: "('a :: narrowing => 'b :: narrowing => 'c) => 'c narrowing"
   1.168  where
   1.169    "cons2 f = apply (apply (cons f) narrowing) narrowing"
   1.170 -  
   1.171 +
   1.172 +definition drawn_from :: "'a list => 'a cons"
   1.173 +where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
   1.174 +
   1.175 +instantiation int :: narrowing
   1.176 +begin
   1.177 +
   1.178 +definition
   1.179 +  "narrowing_int d = (let i = Quickcheck_Narrowing.int_of d in drawn_from [-i .. i])"
   1.180 +
   1.181 +instance ..
   1.182 +
   1.183 +end
   1.184 +
   1.185  instantiation unit :: narrowing
   1.186  begin
   1.187  
     2.1 --- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
     2.2 +++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
     2.3 @@ -10,12 +10,12 @@
     2.4  begin
     2.5  
     2.6  subsection {* Minimalistic examples *}
     2.7 -
     2.8 +(*
     2.9  lemma
    2.10    "x = y"
    2.11 -quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
    2.12 +quickcheck[tester = narrowing, finite_types = false, default_type = int, expect = counterexample]
    2.13  oops
    2.14 -
    2.15 +*)
    2.16  (*
    2.17  lemma
    2.18    "x = y"
    2.19 @@ -30,6 +30,10 @@
    2.20  oops
    2.21  
    2.22  lemma "rev xs = xs"
    2.23 +  quickcheck[tester = narrowing, finite_types = false, default_type = int]
    2.24 +oops
    2.25 +
    2.26 +lemma "rev xs = xs"
    2.27    quickcheck[tester = narrowing, finite_types = true]
    2.28  oops
    2.29