adding another narrowing strategy for integers
authorbulwahn
Fri Jun 10 15:42:21 2011 +0200 (2011-06-10)
changeset 433562dee03f192b7
parent 43355 00db2eed7189
child 43357 07889e32bc58
adding another narrowing strategy for integers
src/HOL/Quickcheck_Narrowing.thy
src/HOL/ex/Quickcheck_Narrowing_Examples.thy
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jun 10 15:03:29 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jun 10 15:42:21 2011 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Author: Lukas Bulwahn, TU Muenchen *)
     1.5  
     1.6 -header {* Counterexample generator preforming narrowing-based testing *}
     1.7 +header {* Counterexample generator performing narrowing-based testing *}
     1.8  
     1.9  theory Quickcheck_Narrowing
    1.10  imports Quickcheck_Exhaustive
    1.11 @@ -218,6 +218,10 @@
    1.12  datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
    1.13  datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
    1.14  
    1.15 +primrec map_cons :: "('a => 'b) => 'a cons => 'b cons"
    1.16 +where
    1.17 +  "map_cons f (C ty cs) = C ty (map (%c. f o c) cs)"
    1.18 +
    1.19  subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
    1.20  
    1.21  class partial_term_of = typerep +
    1.22 @@ -225,8 +229,7 @@
    1.23  
    1.24  lemma partial_term_of_anything: "partial_term_of x nt \<equiv> t"
    1.25    by (rule eq_reflection) (cases "partial_term_of x nt", cases t, simp)
    1.26 -
    1.27 -
    1.28 + 
    1.29  subsubsection {* Auxilary functions for Narrowing *}
    1.30  
    1.31  consts nth :: "'a list => code_int => 'a"
    1.32 @@ -308,19 +311,6 @@
    1.33  class narrowing =
    1.34    fixes narrowing :: "code_int => 'a cons"
    1.35  
    1.36 -definition drawn_from :: "'a list => 'a cons"
    1.37 -where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
    1.38 -
    1.39 -instantiation int :: narrowing
    1.40 -begin
    1.41 -
    1.42 -definition
    1.43 -  "narrowing_int d = (let i = Quickcheck_Narrowing.int_of d in drawn_from [-i .. i])"
    1.44 -
    1.45 -instance ..
    1.46 -
    1.47 -end
    1.48 -
    1.49  datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
    1.50  
    1.51  (* FIXME: hard-wired maximal depth of 100 here *)
    1.52 @@ -376,9 +366,122 @@
    1.53  
    1.54  setup {* Narrowing_Generators.setup *}
    1.55  
    1.56 +subsection {* Narrowing for integers *}
    1.57 +
    1.58 +
    1.59 +definition drawn_from :: "'a list => 'a cons"
    1.60 +where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
    1.61 +
    1.62 +function around_zero :: "int => int list"
    1.63 +where
    1.64 +  "around_zero i = (if i < 0 then [] else (if i = 0 then [0] else around_zero (i - 1) @ [i, -i]))"
    1.65 +by pat_completeness auto
    1.66 +termination by (relation "measure nat") auto
    1.67 +
    1.68 +declare around_zero.simps[simp del]
    1.69 +
    1.70 +lemma length_around_zero:
    1.71 +  assumes "i >= 0" 
    1.72 +  shows "length (around_zero i) = 2 * nat i + 1"
    1.73 +proof (induct rule: int_ge_induct[OF assms])
    1.74 +  case 1
    1.75 +  from 1 show ?case by (simp add: around_zero.simps)
    1.76 +next
    1.77 +  case (2 i)
    1.78 +  from 2 show ?case
    1.79 +    by (simp add: around_zero.simps[of "i + 1"])
    1.80 +qed
    1.81 +
    1.82 +lemma
    1.83 +  assumes "int n <= 2 * i"
    1.84 +  shows "(n mod 2 = 1 --> around_zero i ! n = (int n + 1) div 2) &
    1.85 +    (n mod 2 = 0 --> around_zero i ! n = (- (int n)) div 2)"
    1.86 +using assms
    1.87 +proof (cases "i >= 0")
    1.88 +  case False
    1.89 +  with assms show ?thesis by (simp add: around_zero.simps[of i])
    1.90 +next
    1.91 +  case True
    1.92 +  from assms show ?thesis
    1.93 +  proof (induct rule:  int_ge_induct[OF True])
    1.94 +    case (2 i)
    1.95 +    have i: "n < Suc (2 * nat i) \<or> n = Suc (2 * nat i) \<or> n = (2 * nat i) + 2 \<or> n > (2 * nat i) + 2"
    1.96 +      by arith
    1.97 +    show ?case    
    1.98 +    proof -
    1.99 +      {
   1.100 +        assume "n mod 2 = 1"
   1.101 +        from 2 length_around_zero[OF 2(1)] this i have "around_zero (i + 1) ! n = (int n + 1) div 2"
   1.102 +          unfolding around_zero.simps[of "i + 1"]
   1.103 +          by (auto simp add: nth_append)
   1.104 +      } moreover
   1.105 +      {
   1.106 +        assume a: "n mod 2 = 0"
   1.107 +        have "\<forall> q q'. 2 * q \<noteq> Suc (2 * q')" by arith
   1.108 +        from a 2 length_around_zero[OF 2(1)] this i have "around_zero (i + 1) ! n = - int n div 2"
   1.109 +          unfolding around_zero.simps[of "i + 1"]
   1.110 +          by (auto simp add: nth_append)
   1.111 +      }
   1.112 +      ultimately show ?thesis by auto
   1.113 +    qed
   1.114 +   next
   1.115 +     case 1
   1.116 +     from 1 show ?case by (auto simp add: around_zero.simps[of 0])
   1.117 +  qed
   1.118 +qed
   1.119 +
   1.120 +instantiation int :: narrowing
   1.121 +begin
   1.122 +
   1.123 +definition
   1.124 +  "narrowing_int d = (let (u :: _ => _ => unit) = conv; i = Quickcheck_Narrowing.int_of d in drawn_from (around_zero i))"
   1.125 +
   1.126 +instance ..
   1.127 +
   1.128 +end
   1.129 +
   1.130 +lemma [code, code del]: "partial_term_of (ty :: int itself) t == undefined"
   1.131 +by (rule partial_term_of_anything)+
   1.132 +
   1.133 +lemma [code]:
   1.134 +  "partial_term_of (ty :: int itself) (Var p t) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
   1.135 +  "partial_term_of (ty :: int itself) (Ctr i []) == (if i mod 2 = 0 then
   1.136 +     Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))"
   1.137 +by (rule partial_term_of_anything)+
   1.138 +
   1.139 +text {* Defining integers by positive and negative copy of naturals *}
   1.140 +(*
   1.141 +datatype simple_int = Positive nat | Negative nat
   1.142 +
   1.143 +primrec int_of_simple_int :: "simple_int => int"
   1.144 +where
   1.145 +  "int_of_simple_int (Positive n) = int n"
   1.146 +| "int_of_simple_int (Negative n) = (-1 - int n)"
   1.147 +
   1.148 +instantiation int :: narrowing
   1.149 +begin
   1.150 +
   1.151 +definition narrowing_int :: "code_int => int cons"
   1.152 +where
   1.153 +  "narrowing_int d = map_cons int_of_simple_int ((narrowing :: simple_int narrowing) d)"
   1.154 +
   1.155 +instance ..
   1.156 +
   1.157 +end
   1.158 +
   1.159 +text {* printing the partial terms *}
   1.160 +
   1.161 +lemma [code]:
   1.162 +  "partial_term_of (ty :: int itself) t == Code_Evaluation.App (Code_Evaluation.Const (STR ''Quickcheck_Narrowing.int_of_simple_int'')
   1.163 +     (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Quickcheck_Narrowing.simple_int'') [], Typerep.Typerep (STR ''Int.int'') []])) (partial_term_of (TYPE(simple_int)) t)"
   1.164 +by (rule partial_term_of_anything)
   1.165 +
   1.166 +*)
   1.167 +
   1.168  hide_type code_int narrowing_type narrowing_term cons property
   1.169  hide_const int_of of_int nth error toEnum marker empty
   1.170    C cons conv nonEmpty "apply" sum ensure_testable all exists 
   1.171  hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
   1.172  
   1.173 +
   1.174  end
   1.175 \ No newline at end of file
     2.1 --- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Jun 10 15:03:29 2011 +0200
     2.2 +++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Jun 10 15:42:21 2011 +0200
     2.3 @@ -10,27 +10,29 @@
     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 = int, expect = counterexample]
    2.12  oops
    2.13 -*)
    2.14 -(*
    2.15 +
    2.16  lemma
    2.17    "x = y"
    2.18 -quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
    2.19 +quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
    2.20  oops
    2.21 -*)
    2.22  
    2.23 -(*declare [[quickcheck_narrowing_overlord]]*)
    2.24  subsection {* Simple examples with existentials *}
    2.25  
    2.26  lemma
    2.27    "\<exists> y :: nat. \<forall> x. x = y"
    2.28  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]
    2.29  oops
    2.30 -
    2.31 +(*
    2.32 +lemma
    2.33 +  "\<exists> y :: int. \<forall> x. x = y"
    2.34 +quickcheck[tester = narrowing, size = 2]
    2.35 +oops
    2.36 +*)
    2.37  lemma
    2.38    "x > 1 --> (\<exists>y :: nat. x < y & y <= 1)"
    2.39  quickcheck[tester = narrowing, finite_types = false, expect = counterexample]