translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
authorbulwahn
Fri Mar 18 18:19:42 2011 +0100 (2011-03-18)
changeset 420202da02764d523
parent 42019 a9445d87bc3e
child 42021 52551c0a3374
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/HOL/ex/Quickcheck_Narrowing_Examples.thy
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -147,6 +147,7 @@
     1.4      val result = Isabelle_System.with_tmp_dir tmp_prefix run
     1.5      val output_value = the_default "NONE"
     1.6        (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
     1.7 +      |> translate_string (fn s => if s = "\\" then "\\\\" else s)
     1.8      val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
     1.9        ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
    1.10      val ctxt' = ctxt
     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 @@ -9,19 +9,31 @@
     2.4  imports "~~/src/HOL/Library/Quickcheck_Narrowing"
     2.5  begin
     2.6  
     2.7 -subsection {* Simple list examples *}
     2.8 +subsection {* Minimalistic examples *}
     2.9  
    2.10 -lemma "rev xs = xs"
    2.11 +lemma
    2.12 +  "x = y"
    2.13  quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
    2.14  oops
    2.15  
    2.16 -text {* Example fails due to some strange thing... *}
    2.17  (*
    2.18 -lemma "rev xs = xs"
    2.19 -quickcheck[tester = lazy_exhaustive, finite_types = true]
    2.20 +lemma
    2.21 +  "x = y"
    2.22 +quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
    2.23  oops
    2.24  *)
    2.25  
    2.26 +subsection {* Simple list examples *}
    2.27 +
    2.28 +lemma "rev xs = xs"
    2.29 +  quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
    2.30 +oops
    2.31 +
    2.32 +lemma "rev xs = xs"
    2.33 +  quickcheck[tester = narrowing, finite_types = true]
    2.34 +oops
    2.35 +
    2.36 +
    2.37  subsection {* AVL Trees *}
    2.38  
    2.39  datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
    2.40 @@ -117,7 +129,7 @@
    2.41  
    2.42  lemma is_ord_l_bal:
    2.43   "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
    2.44 -quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 1, timeout = 100, expect = counterexample]
    2.45 +quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, timeout = 100, expect = counterexample]
    2.46  oops
    2.47  
    2.48