# HG changeset patch
# User blanchet
# Date 1411126024 -7200
# Node ID 00f5b1efc741e9678c26d1ad15549a567154f9ff
# Parent  fe0fc8aee49aecf9d70f5ed5bc2c1e7809da69f3
added a few tests for 'old_datatype'

diff -r fe0fc8aee49a -r 00f5b1efc741 src/HOL/Datatype_Examples/Compat.thy
--- a/src/HOL/Datatype_Examples/Compat.thy	Fri Sep 19 13:27:04 2014 +0200
+++ b/src/HOL/Datatype_Examples/Compat.thy	Fri Sep 19 13:27:04 2014 +0200
@@ -29,6 +29,26 @@
 
 old_datatype 'a old_lst = Old_Nl | Old_Cns 'a "'a old_lst"
 
+text {*
+A few tests to make sure that @{text old_datatype} works as expected:
+*}
+
+primrec old_len :: "'a old_lst \<Rightarrow> nat" where
+  "old_len Old_Nl = 0"
+| "old_len (Old_Cns _ xs) = Suc (old_len xs)"
+
+export_code old_len checking SML OCaml? Haskell? Scala
+
+lemma "Old_Nl = Old_Cns x xs"
+  nitpick [expect = genuine]
+  quickcheck [exhaustive, expect = counterexample]
+  quickcheck [random, expect = counterexample]
+  quickcheck [narrowing, expect = counterexample]
+  oops
+
+lemma "old_len xs = size xs"
+  by (induct xs) auto
+
 ML {* get_descrs @{theory} (1, 1, 1) @{type_name old_lst} *}
 
 datatype 'a lst = Nl | Cns 'a "'a lst"