src/HOL/ex/Refute_Examples.thy
changeset 58129 3ec65a7f2b50
parent 56851 35ff4ede3409
child 58143 7f7026ae9dc5
     1.1 --- a/src/HOL/ex/Refute_Examples.thy	Mon Sep 01 16:34:40 2014 +0200
     1.2 +++ b/src/HOL/ex/Refute_Examples.thy	Mon Sep 01 17:34:03 2014 +0200
     1.3 @@ -609,7 +609,7 @@
     1.4  
     1.5  text {* Non-recursive datatypes *}
     1.6  
     1.7 -datatype T1 = A | B
     1.8 +datatype_new T1 = A | B
     1.9  
    1.10  lemma "P (x::T1)"
    1.11  refute [expect = genuine]
    1.12 @@ -643,7 +643,7 @@
    1.13  refute [expect = genuine]
    1.14  oops
    1.15  
    1.16 -datatype 'a T2 = C T1 | D 'a
    1.17 +datatype_new 'a T2 = C T1 | D 'a
    1.18  
    1.19  lemma "P (x::'a T2)"
    1.20  refute [expect = genuine]
    1.21 @@ -673,7 +673,7 @@
    1.22  refute [expect = genuine]
    1.23  oops
    1.24  
    1.25 -datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
    1.26 +datatype_new ('a,'b) T3 = E "'a \<Rightarrow> 'b"
    1.27  
    1.28  lemma "P (x::('a,'b) T3)"
    1.29  refute [expect = genuine]
    1.30 @@ -776,7 +776,7 @@
    1.31  refute [expect = potential]
    1.32  oops
    1.33  
    1.34 -datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
    1.35 +datatype_new BitList = BitListNil | Bit0 BitList | Bit1 BitList
    1.36  
    1.37  lemma "P (x::BitList)"
    1.38  refute [expect = potential]
    1.39 @@ -806,7 +806,7 @@
    1.40  refute [expect = potential]
    1.41  oops
    1.42  
    1.43 -datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
    1.44 +datatype_new 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
    1.45  
    1.46  lemma "P (x::'a BinTree)"
    1.47  refute [expect = potential]
    1.48 @@ -842,8 +842,9 @@
    1.49  
    1.50  text {* Mutually recursive datatypes *}
    1.51  
    1.52 -datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
    1.53 -     and 'a bexp = Equal "'a aexp" "'a aexp"
    1.54 +datatype_new
    1.55 +  'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp" and
    1.56 +  'a bexp = Equal "'a aexp" "'a aexp"
    1.57  
    1.58  lemma "P (x::'a aexp)"
    1.59  refute [expect = potential]
    1.60 @@ -865,15 +866,15 @@
    1.61  refute [expect = potential]
    1.62  oops
    1.63  
    1.64 -lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x"
    1.65 +lemma "rec_aexp number ite equal (Number x) = number x"
    1.66  refute [maxsize = 1, expect = none]
    1.67  by simp
    1.68  
    1.69 -lemma "rec_aexp_bexp_1 number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp_bexp_1 number ite equal y) (rec_aexp_bexp_1 number ite equal z)"
    1.70 +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)"
    1.71  refute [maxsize = 1, expect = none]
    1.72  by simp
    1.73  
    1.74 -lemma "P (rec_aexp_bexp_1 number ite equal x)"
    1.75 +lemma "P (rec_aexp number ite equal x)"
    1.76  refute [expect = potential]
    1.77  oops
    1.78  
    1.79 @@ -881,11 +882,11 @@
    1.80  refute [expect = potential]
    1.81  oops
    1.82  
    1.83 -lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp_bexp_1 number ite equal x) (rec_aexp_bexp_1 number ite equal y)"
    1.84 +lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
    1.85  refute [maxsize = 1, expect = none]
    1.86  by simp
    1.87  
    1.88 -lemma "P (rec_aexp_bexp_2 number ite equal x)"
    1.89 +lemma "P (rec_bexp number ite equal x)"
    1.90  refute [expect = potential]
    1.91  oops
    1.92  
    1.93 @@ -893,8 +894,9 @@
    1.94  refute [expect = potential]
    1.95  oops
    1.96  
    1.97 -datatype X = A | B X | C Y
    1.98 -     and Y = D X | E Y | F
    1.99 +datatype_new
   1.100 +  X = A | B X | C Y and
   1.101 +  Y = D X | E Y | F
   1.102  
   1.103  lemma "P (x::X)"
   1.104  refute [expect = potential]
   1.105 @@ -940,35 +942,35 @@
   1.106  refute [expect = potential]
   1.107  oops
   1.108  
   1.109 -lemma "rec_X_Y_1 a b c d e f A = a"
   1.110 +lemma "rec_X a b c d e f A = a"
   1.111  refute [maxsize = 3, expect = none]
   1.112  by simp
   1.113  
   1.114 -lemma "rec_X_Y_1 a b c d e f (B x) = b x (rec_X_Y_1 a b c d e f x)"
   1.115 +lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
   1.116  refute [maxsize = 1, expect = none]
   1.117  by simp
   1.118  
   1.119 -lemma "rec_X_Y_1 a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)"
   1.120 +lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)"
   1.121  refute [maxsize = 1, expect = none]
   1.122  by simp
   1.123  
   1.124 -lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X_Y_1 a b c d e f x)"
   1.125 +lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)"
   1.126  refute [maxsize = 1, expect = none]
   1.127  by simp
   1.128  
   1.129 -lemma "rec_X_Y_2 a b c d e f (E y) = e y (rec_X_Y_2 a b c d e f y)"
   1.130 +lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)"
   1.131  refute [maxsize = 1, expect = none]
   1.132  by simp
   1.133  
   1.134 -lemma "rec_X_Y_2 a b c d e f F = f"
   1.135 +lemma "rec_Y a b c d e f F = f"
   1.136  refute [maxsize = 3, expect = none]
   1.137  by simp
   1.138  
   1.139 -lemma "P (rec_X_Y_1 a b c d e f x)"
   1.140 +lemma "P (rec_X a b c d e f x)"
   1.141  refute [expect = potential]
   1.142  oops
   1.143  
   1.144 -lemma "P (rec_X_Y_2 a b c d e f y)"
   1.145 +lemma "P (rec_Y a b c d e f y)"
   1.146  refute [expect = potential]
   1.147  oops
   1.148  
   1.149 @@ -1060,7 +1062,11 @@
   1.150  refute [expect = potential]
   1.151  oops
   1.152  
   1.153 -datatype Trie = TR "Trie list"
   1.154 +datatype_new Trie = TR "Trie list"
   1.155 +datatype_compat Trie
   1.156 +
   1.157 +abbreviation "rec_Trie_1 \<equiv> compat_Trie.n2m_Trie_rec"
   1.158 +abbreviation "rec_Trie_2 \<equiv> compat_Trie_list.n2m_Trie_list_rec"
   1.159  
   1.160  lemma "P (x::Trie)"
   1.161  refute [expect = potential]
   1.162 @@ -1241,19 +1247,6 @@
   1.163  refute
   1.164  oops
   1.165  
   1.166 -inductive_set
   1.167 -  even :: "nat set"
   1.168 -  and odd  :: "nat set"
   1.169 -where
   1.170 -  "0 : even"
   1.171 -| "n : even \<Longrightarrow> Suc n : odd"
   1.172 -| "n : odd \<Longrightarrow> Suc n : even"
   1.173 -
   1.174 -lemma "n : odd"
   1.175 -(* refute *)  (* TODO: there seems to be an issue here with undefined terms
   1.176 -                       because of the recursive datatype "nat" *)
   1.177 -oops
   1.178 -
   1.179  consts f :: "'a \<Rightarrow> 'a"
   1.180  
   1.181  inductive_set