src/HOL/Enum.thy
changeset 53015 a1119cf551e8
parent 52435 6646bb548c6b
child 54148 c8cc5ab4a863
     1.1 --- a/src/HOL/Enum.thy	Tue Aug 13 14:20:22 2013 +0200
     1.2 +++ b/src/HOL/Enum.thy	Tue Aug 13 16:25:47 2013 +0200
     1.3 @@ -438,25 +438,25 @@
     1.4  
     1.5  text {* We define small finite types for the use in Quickcheck *}
     1.6  
     1.7 -datatype finite_1 = a\<^isub>1
     1.8 +datatype finite_1 = a\<^sub>1
     1.9  
    1.10 -notation (output) a\<^isub>1  ("a\<^isub>1")
    1.11 +notation (output) a\<^sub>1  ("a\<^sub>1")
    1.12  
    1.13  lemma UNIV_finite_1:
    1.14 -  "UNIV = {a\<^isub>1}"
    1.15 +  "UNIV = {a\<^sub>1}"
    1.16    by (auto intro: finite_1.exhaust)
    1.17  
    1.18  instantiation finite_1 :: enum
    1.19  begin
    1.20  
    1.21  definition
    1.22 -  "enum = [a\<^isub>1]"
    1.23 +  "enum = [a\<^sub>1]"
    1.24  
    1.25  definition
    1.26 -  "enum_all P = P a\<^isub>1"
    1.27 +  "enum_all P = P a\<^sub>1"
    1.28  
    1.29  definition
    1.30 -  "enum_ex P = P a\<^isub>1"
    1.31 +  "enum_ex P = P a\<^sub>1"
    1.32  
    1.33  instance proof
    1.34  qed (simp_all only: enum_finite_1_def enum_all_finite_1_def enum_ex_finite_1_def UNIV_finite_1, simp_all)
    1.35 @@ -482,28 +482,28 @@
    1.36  
    1.37  end
    1.38  
    1.39 -hide_const (open) a\<^isub>1
    1.40 +hide_const (open) a\<^sub>1
    1.41  
    1.42 -datatype finite_2 = a\<^isub>1 | a\<^isub>2
    1.43 +datatype finite_2 = a\<^sub>1 | a\<^sub>2
    1.44  
    1.45 -notation (output) a\<^isub>1  ("a\<^isub>1")
    1.46 -notation (output) a\<^isub>2  ("a\<^isub>2")
    1.47 +notation (output) a\<^sub>1  ("a\<^sub>1")
    1.48 +notation (output) a\<^sub>2  ("a\<^sub>2")
    1.49  
    1.50  lemma UNIV_finite_2:
    1.51 -  "UNIV = {a\<^isub>1, a\<^isub>2}"
    1.52 +  "UNIV = {a\<^sub>1, a\<^sub>2}"
    1.53    by (auto intro: finite_2.exhaust)
    1.54  
    1.55  instantiation finite_2 :: enum
    1.56  begin
    1.57  
    1.58  definition
    1.59 -  "enum = [a\<^isub>1, a\<^isub>2]"
    1.60 +  "enum = [a\<^sub>1, a\<^sub>2]"
    1.61  
    1.62  definition
    1.63 -  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2"
    1.64 +  "enum_all P \<longleftrightarrow> P a\<^sub>1 \<and> P a\<^sub>2"
    1.65  
    1.66  definition
    1.67 -  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2"
    1.68 +  "enum_ex P \<longleftrightarrow> P a\<^sub>1 \<or> P a\<^sub>2"
    1.69  
    1.70  instance proof
    1.71  qed (simp_all only: enum_finite_2_def enum_all_finite_2_def enum_ex_finite_2_def UNIV_finite_2, simp_all)
    1.72 @@ -515,7 +515,7 @@
    1.73  
    1.74  definition less_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
    1.75  where
    1.76 -  "x < y \<longleftrightarrow> x = a\<^isub>1 \<and> y = a\<^isub>2"
    1.77 +  "x < y \<longleftrightarrow> x = a\<^sub>1 \<and> y = a\<^sub>2"
    1.78  
    1.79  definition less_eq_finite_2 :: "finite_2 \<Rightarrow> finite_2 \<Rightarrow> bool"
    1.80  where
    1.81 @@ -529,29 +529,29 @@
    1.82  
    1.83  end
    1.84  
    1.85 -hide_const (open) a\<^isub>1 a\<^isub>2
    1.86 +hide_const (open) a\<^sub>1 a\<^sub>2
    1.87  
    1.88 -datatype finite_3 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3
    1.89 +datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    1.90  
    1.91 -notation (output) a\<^isub>1  ("a\<^isub>1")
    1.92 -notation (output) a\<^isub>2  ("a\<^isub>2")
    1.93 -notation (output) a\<^isub>3  ("a\<^isub>3")
    1.94 +notation (output) a\<^sub>1  ("a\<^sub>1")
    1.95 +notation (output) a\<^sub>2  ("a\<^sub>2")
    1.96 +notation (output) a\<^sub>3  ("a\<^sub>3")
    1.97  
    1.98  lemma UNIV_finite_3:
    1.99 -  "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3}"
   1.100 +  "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3}"
   1.101    by (auto intro: finite_3.exhaust)
   1.102  
   1.103  instantiation finite_3 :: enum
   1.104  begin
   1.105  
   1.106  definition
   1.107 -  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3]"
   1.108 +  "enum = [a\<^sub>1, a\<^sub>2, a\<^sub>3]"
   1.109  
   1.110  definition
   1.111 -  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3"
   1.112 +  "enum_all P \<longleftrightarrow> P a\<^sub>1 \<and> P a\<^sub>2 \<and> P a\<^sub>3"
   1.113  
   1.114  definition
   1.115 -  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3"
   1.116 +  "enum_ex P \<longleftrightarrow> P a\<^sub>1 \<or> P a\<^sub>2 \<or> P a\<^sub>3"
   1.117  
   1.118  instance proof
   1.119  qed (simp_all only: enum_finite_3_def enum_all_finite_3_def enum_ex_finite_3_def UNIV_finite_3, simp_all)
   1.120 @@ -563,7 +563,7 @@
   1.121  
   1.122  definition less_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
   1.123  where
   1.124 -  "x < y = (case x of a\<^isub>1 \<Rightarrow> y \<noteq> a\<^isub>1 | a\<^isub>2 \<Rightarrow> y = a\<^isub>3 | a\<^isub>3 \<Rightarrow> False)"
   1.125 +  "x < y = (case x of a\<^sub>1 \<Rightarrow> y \<noteq> a\<^sub>1 | a\<^sub>2 \<Rightarrow> y = a\<^sub>3 | a\<^sub>3 \<Rightarrow> False)"
   1.126  
   1.127  definition less_eq_finite_3 :: "finite_3 \<Rightarrow> finite_3 \<Rightarrow> bool"
   1.128  where
   1.129 @@ -574,69 +574,69 @@
   1.130  
   1.131  end
   1.132  
   1.133 -hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3
   1.134 +hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
   1.135  
   1.136 -datatype finite_4 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4
   1.137 +datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
   1.138  
   1.139 -notation (output) a\<^isub>1  ("a\<^isub>1")
   1.140 -notation (output) a\<^isub>2  ("a\<^isub>2")
   1.141 -notation (output) a\<^isub>3  ("a\<^isub>3")
   1.142 -notation (output) a\<^isub>4  ("a\<^isub>4")
   1.143 +notation (output) a\<^sub>1  ("a\<^sub>1")
   1.144 +notation (output) a\<^sub>2  ("a\<^sub>2")
   1.145 +notation (output) a\<^sub>3  ("a\<^sub>3")
   1.146 +notation (output) a\<^sub>4  ("a\<^sub>4")
   1.147  
   1.148  lemma UNIV_finite_4:
   1.149 -  "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4}"
   1.150 +  "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4}"
   1.151    by (auto intro: finite_4.exhaust)
   1.152  
   1.153  instantiation finite_4 :: enum
   1.154  begin
   1.155  
   1.156  definition
   1.157 -  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4]"
   1.158 +  "enum = [a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4]"
   1.159  
   1.160  definition
   1.161 -  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4"
   1.162 +  "enum_all P \<longleftrightarrow> P a\<^sub>1 \<and> P a\<^sub>2 \<and> P a\<^sub>3 \<and> P a\<^sub>4"
   1.163  
   1.164  definition
   1.165 -  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4"
   1.166 +  "enum_ex P \<longleftrightarrow> P a\<^sub>1 \<or> P a\<^sub>2 \<or> P a\<^sub>3 \<or> P a\<^sub>4"
   1.167  
   1.168  instance proof
   1.169  qed (simp_all only: enum_finite_4_def enum_all_finite_4_def enum_ex_finite_4_def UNIV_finite_4, simp_all)
   1.170  
   1.171  end
   1.172  
   1.173 -hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4
   1.174 +hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
   1.175  
   1.176  
   1.177 -datatype finite_5 = a\<^isub>1 | a\<^isub>2 | a\<^isub>3 | a\<^isub>4 | a\<^isub>5
   1.178 +datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
   1.179  
   1.180 -notation (output) a\<^isub>1  ("a\<^isub>1")
   1.181 -notation (output) a\<^isub>2  ("a\<^isub>2")
   1.182 -notation (output) a\<^isub>3  ("a\<^isub>3")
   1.183 -notation (output) a\<^isub>4  ("a\<^isub>4")
   1.184 -notation (output) a\<^isub>5  ("a\<^isub>5")
   1.185 +notation (output) a\<^sub>1  ("a\<^sub>1")
   1.186 +notation (output) a\<^sub>2  ("a\<^sub>2")
   1.187 +notation (output) a\<^sub>3  ("a\<^sub>3")
   1.188 +notation (output) a\<^sub>4  ("a\<^sub>4")
   1.189 +notation (output) a\<^sub>5  ("a\<^sub>5")
   1.190  
   1.191  lemma UNIV_finite_5:
   1.192 -  "UNIV = {a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5}"
   1.193 +  "UNIV = {a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4, a\<^sub>5}"
   1.194    by (auto intro: finite_5.exhaust)
   1.195  
   1.196  instantiation finite_5 :: enum
   1.197  begin
   1.198  
   1.199  definition
   1.200 -  "enum = [a\<^isub>1, a\<^isub>2, a\<^isub>3, a\<^isub>4, a\<^isub>5]"
   1.201 +  "enum = [a\<^sub>1, a\<^sub>2, a\<^sub>3, a\<^sub>4, a\<^sub>5]"
   1.202  
   1.203  definition
   1.204 -  "enum_all P \<longleftrightarrow> P a\<^isub>1 \<and> P a\<^isub>2 \<and> P a\<^isub>3 \<and> P a\<^isub>4 \<and> P a\<^isub>5"
   1.205 +  "enum_all P \<longleftrightarrow> P a\<^sub>1 \<and> P a\<^sub>2 \<and> P a\<^sub>3 \<and> P a\<^sub>4 \<and> P a\<^sub>5"
   1.206  
   1.207  definition
   1.208 -  "enum_ex P \<longleftrightarrow> P a\<^isub>1 \<or> P a\<^isub>2 \<or> P a\<^isub>3 \<or> P a\<^isub>4 \<or> P a\<^isub>5"
   1.209 +  "enum_ex P \<longleftrightarrow> P a\<^sub>1 \<or> P a\<^sub>2 \<or> P a\<^sub>3 \<or> P a\<^sub>4 \<or> P a\<^sub>5"
   1.210  
   1.211  instance proof
   1.212  qed (simp_all only: enum_finite_5_def enum_all_finite_5_def enum_ex_finite_5_def UNIV_finite_5, simp_all)
   1.213  
   1.214  end
   1.215  
   1.216 -hide_const (open) a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
   1.217 +hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4 a\<^sub>5
   1.218  
   1.219  
   1.220  subsection {* Closing up *}