src/HOL/Quickcheck_Examples/Quickcheck_Nesting_Example.thy
author haftmann
Thu, 08 Nov 2018 09:11:52 +0100
changeset 69260 0a9688695a1b
parent 63731 9f906a2eb0e7
permissions -rw-r--r--
removed relics of ASCII syntax for indexed big operators
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63731
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
     1
theory Quickcheck_Nesting_Example
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
     2
imports Quickcheck_Nesting
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
     3
begin
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
     4
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
     5
datatype x = X "x list"
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
     6
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
     7
lemma "X a = X b"
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
     8
quickcheck[exhaustive, size = 4, expect = counterexample]
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
     9
oops
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
    10
9f906a2eb0e7 added theory to provide workaround to support nested datatypes in quickcheck (until quickcheck is generalized to support it with new datatypes)
blanchet
parents:
diff changeset
    11
end