# HG changeset patch
# User blanchet
# Date 1410454476 -7200
# Node ID 30ab8289f0e14bffe8d7f5f0ba828e45c5eaed3a
# Parent  068496644aa15da9af25f69db205b96448ef66b9
took out some datatype tests for Refute -- these yield timeouts on some Isatests after transition to new datatypes, for some reason (and Refute is obsolete anyway)

diff -r 068496644aa1 -r 30ab8289f0e1 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Sep 11 18:54:36 2014 +0200
@@ -806,405 +806,6 @@
 refute [expect = potential]
 oops
 
-datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
-
-lemma "P (x::'a BinTree)"
-refute [expect = potential]
-oops
-
-lemma "\<forall>x::'a BinTree. P x"
-refute [expect = potential]
-oops
-
-lemma "P (Node (Leaf x) (Leaf y))"
-refute [expect = potential]
-oops
-
-lemma "rec_BinTree l n (Leaf x) = l x"
-  refute [maxsize = 1, expect = none]
-  (* The "maxsize = 1" tests are a bit pointless: for some formulae
-     below, refute will find no countermodel simply because this
-     size makes involved terms undefined.  Unfortunately, any
-     larger size already takes too long. *)
-by simp
-
-lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "P (rec_BinTree l n x)"
-refute [expect = potential]
-oops
-
-lemma "P (case x of Leaf a \<Rightarrow> l a | Node a b \<Rightarrow> n a b)"
-refute [expect = potential]
-oops
-
-text {* Mutually recursive datatypes *}
-
-datatype_new
-  'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp" and
-  'a bexp = Equal "'a aexp" "'a aexp"
-
-lemma "P (x::'a aexp)"
-refute [expect = potential]
-oops
-
-lemma "\<forall>x::'a aexp. P x"
-refute [expect = potential]
-oops
-
-lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
-refute [expect = potential]
-oops
-
-lemma "P (x::'a bexp)"
-refute [expect = potential]
-oops
-
-lemma "\<forall>x::'a bexp. P x"
-refute [expect = potential]
-oops
-
-lemma "rec_aexp number ite equal (Number x) = number x"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_bexp number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "P (rec_aexp number ite equal x)"
-refute [expect = potential]
-oops
-
-lemma "P (case x of Number a \<Rightarrow> number a | ITE b a1 a2 \<Rightarrow> ite b a1 a2)"
-refute [expect = potential]
-oops
-
-lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "P (rec_bexp number ite equal x)"
-refute [expect = potential]
-oops
-
-lemma "P (case x of Equal a1 a2 \<Rightarrow> equal a1 a2)"
-refute [expect = potential]
-oops
-
-datatype_new
-  X = A | B X | C Y and
-  Y = D X | E Y | F
-
-lemma "P (x::X)"
-refute [expect = potential]
-oops
-
-lemma "P (y::Y)"
-refute [expect = potential]
-oops
-
-lemma "P (B (B A))"
-refute [expect = potential]
-oops
-
-lemma "P (B (C F))"
-refute [expect = potential]
-oops
-
-lemma "P (C (D A))"
-refute [expect = potential]
-oops
-
-lemma "P (C (E F))"
-refute [expect = potential]
-oops
-
-lemma "P (D (B A))"
-refute [expect = potential]
-oops
-
-lemma "P (D (C F))"
-refute [expect = potential]
-oops
-
-lemma "P (E (D A))"
-refute [expect = potential]
-oops
-
-lemma "P (E (E F))"
-refute [expect = potential]
-oops
-
-lemma "P (C (D (C F)))"
-refute [expect = potential]
-oops
-
-lemma "rec_X a b c d e f A = a"
-refute [maxsize = 2, expect = none]
-by simp
-
-lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_Y a b c d e f F = f"
-refute [maxsize = 2, expect = none]
-by simp
-
-lemma "P (rec_X a b c d e f x)"
-refute [expect = potential]
-oops
-
-lemma "P (rec_Y a b c d e f y)"
-refute [expect = potential]
-oops
-
-text {* Other datatype examples *}
-
-text {* Indirect recursion is implemented via mutual recursion. *}
-
-datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
-
-lemma "P (x::XOpt)"
-refute [expect = potential]
-oops
-
-lemma "P (CX None)"
-refute [expect = potential]
-oops
-
-lemma "P (CX (Some (CX None)))"
-refute [expect = potential]
-oops
-
-lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1"
-refute [maxsize = 2, expect = none]
-by simp
-
-lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2"
-refute [maxsize = 2, expect = none]
-by simp
-
-lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
-refute [expect = potential]
-oops
-
-lemma "P (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
-refute [expect = potential]
-oops
-
-lemma "P (rec_XOpt_3 cx dx n1 s1 n2 s2 x)"
-refute [expect = potential]
-oops
-
-datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
-
-lemma "P (x::'a YOpt)"
-refute [expect = potential]
-oops
-
-lemma "P (CY None)"
-refute [expect = potential]
-oops
-
-lemma "P (CY (Some (\<lambda>a. CY None)))"
-refute [expect = potential]
-oops
-
-lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_YOpt_2 cy n s None = n"
-refute [maxsize = 2, expect = none]
-by simp
-
-lemma "rec_YOpt_2 cy n s (Some x) = s x (\<lambda>a. rec_YOpt_1 cy n s (x a))"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "P (rec_YOpt_1 cy n s x)"
-refute [expect = potential]
-oops
-
-lemma "P (rec_YOpt_2 cy n s x)"
-refute [expect = potential]
-oops
-
-datatype_new Trie = TR "Trie list"
-datatype_compat Trie
-
-abbreviation "rec_Trie_1 \<equiv> compat_Trie.rec_n2m_Trie"
-abbreviation "rec_Trie_2 \<equiv> compat_Trie_list.rec_n2m_Trie_list"
-
-lemma "P (x::Trie)"
-refute [expect = potential]
-oops
-
-lemma "\<forall>x::Trie. P x"
-refute [expect = potential]
-oops
-
-lemma "P (TR [TR []])"
-refute [expect = potential]
-oops
-
-lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_Trie_2 tr nil cons [] = nil"
-refute [maxsize = 3, expect = none]
-by simp
-
-lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "P (rec_Trie_1 tr nil cons x)"
-refute [expect = potential]
-oops
-
-lemma "P (rec_Trie_2 tr nil cons x)"
-refute [expect = potential]
-oops
-
-datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
-
-lemma "P (x::InfTree)"
-refute [expect = potential]
-oops
-
-lemma "\<forall>x::InfTree. P x"
-refute [expect = potential]
-oops
-
-lemma "P (Node (\<lambda>n. Leaf))"
-refute [expect = potential]
-oops
-
-lemma "rec_InfTree leaf node Leaf = leaf"
-refute [maxsize = 2, expect = none]
-by simp
-
-lemma "rec_InfTree leaf node (Node x) = node x (\<lambda>n. rec_InfTree leaf node (x n))"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "P (rec_InfTree leaf node x)"
-refute [expect = potential]
-oops
-
-datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
-
-lemma "P (x::'a lambda)"
-refute [expect = potential]
-oops
-
-lemma "\<forall>x::'a lambda. P x"
-refute [expect = potential]
-oops
-
-lemma "P (Lam (\<lambda>a. Var a))"
-refute [expect = potential]
-oops
-
-lemma "rec_lambda var app lam (Var x) = var x"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_lambda var app lam (Lam x) = lam x (\<lambda>a. rec_lambda var app lam (x a))"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "P (rec_lambda v a l x)"
-refute [expect = potential]
-oops
-
-text {* Taken from "Inductive datatypes in HOL", p.8: *}
-
-datatype ('a, 'b) T = C "'a \<Rightarrow> bool" | D "'b list"
-datatype 'c U = E "('c, 'c U) T"
-
-lemma "P (x::'c U)"
-refute [expect = potential]
-oops
-
-lemma "\<forall>x::'c U. P x"
-refute [expect = potential]
-oops
-
-lemma "P (E (C (\<lambda>a. True)))"
-refute [expect = potential]
-oops
-
-lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_U_2 e c d nil cons (C x) = c x"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "rec_U_3 e c d nil cons [] = nil"
-refute [maxsize = 2, expect = none]
-by simp
-
-lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)"
-refute [maxsize = 1, expect = none]
-by simp
-
-lemma "P (rec_U_1 e c d nil cons x)"
-refute [expect = potential]
-oops
-
-lemma "P (rec_U_2 e c d nil cons x)"
-refute [expect = potential]
-oops
-
-lemma "P (rec_U_3 e c d nil cons x)"
-refute [expect = potential]
-oops
-
 (*****************************************************************************)
 
 subsubsection {* Examples involving special functions *}