# HG changeset patch
# User bulwahn
# Date 1300468782 -3600
# Node ID 2da02764d523ca0b0a2a629533c2222b60f0ce7c
# Parent  a9445d87bc3e7d6e0b5a5e30ffaa290252510c3e
translating bash output in quickcheck_narrowing to handle special characters; adding simple test cases

diff -r a9445d87bc3e -r 2da02764d523 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
@@ -147,6 +147,7 @@
     val result = Isabelle_System.with_tmp_dir tmp_prefix run
     val output_value = the_default "NONE"
       (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
+      |> translate_string (fn s => if s = "\\" then "\\\\" else s)
     val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
       ^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
     val ctxt' = ctxt
diff -r a9445d87bc3e -r 2da02764d523 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Fri Mar 18 18:19:42 2011 +0100
@@ -9,19 +9,31 @@
 imports "~~/src/HOL/Library/Quickcheck_Narrowing"
 begin
 
-subsection {* Simple list examples *}
+subsection {* Minimalistic examples *}
 
-lemma "rev xs = xs"
+lemma
+  "x = y"
 quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
 oops
 
-text {* Example fails due to some strange thing... *}
 (*
-lemma "rev xs = xs"
-quickcheck[tester = lazy_exhaustive, finite_types = true]
+lemma
+  "x = y"
+quickcheck[tester = narrowing, finite_types = true, expect = counterexample]
 oops
 *)
 
+subsection {* Simple list examples *}
+
+lemma "rev xs = xs"
+  quickcheck[tester = narrowing, finite_types = false, default_type = nat, expect = counterexample]
+oops
+
+lemma "rev xs = xs"
+  quickcheck[tester = narrowing, finite_types = true]
+oops
+
+
 subsection {* AVL Trees *}
 
 datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat
@@ -117,7 +129,7 @@
 
 lemma is_ord_l_bal:
  "\<lbrakk> is_ord(MKT (x :: nat) l r h); height l = height r + 2 \<rbrakk> \<Longrightarrow> is_ord(l_bal(x,l,r))"
-quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 1, timeout = 100, expect = counterexample]
+quickcheck[tester = narrowing, finite_types = false, default_type = nat, size = 6, timeout = 100, expect = counterexample]
 oops