Tuning the quotient examples
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Thu Apr 29 09:06:35 2010 +0200 (2010-04-29)
changeset 365243909002beca5
parent 36523 a294e4ebe0a3
child 36525 2584289edbb0
child 36529 11c750bc7acf
Tuning the quotient examples
src/HOL/IsaMakefile
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/LarryDatatype.thy
src/HOL/Quotient_Examples/LarryInt.thy
src/HOL/Quotient_Examples/Quotient_Int.thy
src/HOL/Quotient_Examples/Quotient_Message.thy
src/HOL/Quotient_Examples/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Apr 28 17:42:37 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Apr 29 09:06:35 2010 +0200
     1.3 @@ -1295,8 +1295,8 @@
     1.4  HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
     1.5  
     1.6  $(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL				\
     1.7 -  Quotient_Examples/FSet.thy                                            \
     1.8 -  Quotient_Examples/LarryInt.thy Quotient_Examples/LarryDatatype.thy
     1.9 +  Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy         \
    1.10 +  Quotient_Examples/Quotient_Message.thy
    1.11  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
    1.12  
    1.13  
     2.1 --- a/src/HOL/Quotient_Examples/FSet.thy	Wed Apr 28 17:42:37 2010 +0200
     2.2 +++ b/src/HOL/Quotient_Examples/FSet.thy	Thu Apr 29 09:06:35 2010 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/Quotient_Examples/Quotient.thy
     2.5 +(*  Title:      HOL/Quotient_Examples/FSet.thy
     2.6      Author:     Cezary Kaliszyk, TU Munich
     2.7      Author:     Christian Urban, TU Munich
     2.8  
     3.1 --- a/src/HOL/Quotient_Examples/LarryDatatype.thy	Wed Apr 28 17:42:37 2010 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,394 +0,0 @@
     3.4 -theory LarryDatatype
     3.5 -imports Main Quotient_Syntax
     3.6 -begin
     3.7 -
     3.8 -subsection{*Defining the Free Algebra*}
     3.9 -
    3.10 -datatype
    3.11 -  freemsg = NONCE  nat
    3.12 -        | MPAIR  freemsg freemsg
    3.13 -        | CRYPT  nat freemsg  
    3.14 -        | DECRYPT  nat freemsg
    3.15 -
    3.16 -inductive 
    3.17 -  msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
    3.18 -where 
    3.19 -  CD:    "CRYPT K (DECRYPT K X) \<sim> X"
    3.20 -| DC:    "DECRYPT K (CRYPT K X) \<sim> X"
    3.21 -| NONCE: "NONCE N \<sim> NONCE N"
    3.22 -| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
    3.23 -| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
    3.24 -| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
    3.25 -| SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
    3.26 -| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
    3.27 -
    3.28 -lemmas msgrel.intros[intro]
    3.29 -
    3.30 -text{*Proving that it is an equivalence relation*}
    3.31 -
    3.32 -lemma msgrel_refl: "X \<sim> X"
    3.33 -by (induct X, (blast intro: msgrel.intros)+)
    3.34 -
    3.35 -theorem equiv_msgrel: "equivp msgrel"
    3.36 -proof (rule equivpI)
    3.37 -  show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
    3.38 -  show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
    3.39 -  show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
    3.40 -qed
    3.41 -
    3.42 -subsection{*Some Functions on the Free Algebra*}
    3.43 -
    3.44 -subsubsection{*The Set of Nonces*}
    3.45 -
    3.46 -fun
    3.47 -  freenonces :: "freemsg \<Rightarrow> nat set"
    3.48 -where
    3.49 -  "freenonces (NONCE N) = {N}"
    3.50 -| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
    3.51 -| "freenonces (CRYPT K X) = freenonces X"
    3.52 -| "freenonces (DECRYPT K X) = freenonces X"
    3.53 -
    3.54 -theorem msgrel_imp_eq_freenonces: 
    3.55 -  assumes a: "U \<sim> V"
    3.56 -  shows "freenonces U = freenonces V"
    3.57 -  using a by (induct) (auto) 
    3.58 -
    3.59 -subsubsection{*The Left Projection*}
    3.60 -
    3.61 -text{*A function to return the left part of the top pair in a message.  It will
    3.62 -be lifted to the initial algrebra, to serve as an example of that process.*}
    3.63 -fun
    3.64 -  freeleft :: "freemsg \<Rightarrow> freemsg"
    3.65 -where
    3.66 -  "freeleft (NONCE N) = NONCE N"
    3.67 -| "freeleft (MPAIR X Y) = X"
    3.68 -| "freeleft (CRYPT K X) = freeleft X"
    3.69 -| "freeleft (DECRYPT K X) = freeleft X"
    3.70 -
    3.71 -text{*This theorem lets us prove that the left function respects the
    3.72 -equivalence relation.  It also helps us prove that MPair
    3.73 -  (the abstract constructor) is injective*}
    3.74 -lemma msgrel_imp_eqv_freeleft_aux:
    3.75 -  shows "freeleft U \<sim> freeleft U"
    3.76 -  by (induct rule: freeleft.induct) (auto)
    3.77 -
    3.78 -theorem msgrel_imp_eqv_freeleft:
    3.79 -  assumes a: "U \<sim> V" 
    3.80 -  shows "freeleft U \<sim> freeleft V"
    3.81 -  using a
    3.82 -  by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
    3.83 -
    3.84 -subsubsection{*The Right Projection*}
    3.85 -
    3.86 -text{*A function to return the right part of the top pair in a message.*}
    3.87 -fun
    3.88 -  freeright :: "freemsg \<Rightarrow> freemsg"
    3.89 -where
    3.90 -  "freeright (NONCE N) = NONCE N"
    3.91 -| "freeright (MPAIR X Y) = Y"
    3.92 -| "freeright (CRYPT K X) = freeright X"
    3.93 -| "freeright (DECRYPT K X) = freeright X"
    3.94 -
    3.95 -text{*This theorem lets us prove that the right function respects the
    3.96 -equivalence relation.  It also helps us prove that MPair
    3.97 -  (the abstract constructor) is injective*}
    3.98 -lemma msgrel_imp_eqv_freeright_aux:
    3.99 -  shows "freeright U \<sim> freeright U"
   3.100 -  by (induct rule: freeright.induct) (auto)
   3.101 -
   3.102 -theorem msgrel_imp_eqv_freeright:
   3.103 -  assumes a: "U \<sim> V" 
   3.104 -  shows "freeright U \<sim> freeright V"
   3.105 -  using a
   3.106 -  by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
   3.107 -
   3.108 -subsubsection{*The Discriminator for Constructors*}
   3.109 -
   3.110 -text{*A function to distinguish nonces, mpairs and encryptions*}
   3.111 -fun 
   3.112 -  freediscrim :: "freemsg \<Rightarrow> int"
   3.113 -where
   3.114 -   "freediscrim (NONCE N) = 0"
   3.115 - | "freediscrim (MPAIR X Y) = 1"
   3.116 - | "freediscrim (CRYPT K X) = freediscrim X + 2"
   3.117 - | "freediscrim (DECRYPT K X) = freediscrim X - 2"
   3.118 -
   3.119 -text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
   3.120 -theorem msgrel_imp_eq_freediscrim:
   3.121 -  assumes a: "U \<sim> V"
   3.122 -  shows "freediscrim U = freediscrim V"
   3.123 -  using a by (induct) (auto)
   3.124 -
   3.125 -subsection{*The Initial Algebra: A Quotiented Message Type*}
   3.126 -
   3.127 -quotient_type msg = freemsg / msgrel
   3.128 -  by (rule equiv_msgrel)
   3.129 -
   3.130 -text{*The abstract message constructors*}
   3.131 -
   3.132 -quotient_definition
   3.133 -  "Nonce :: nat \<Rightarrow> msg"
   3.134 -is
   3.135 -  "NONCE"
   3.136 -
   3.137 -quotient_definition
   3.138 -  "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
   3.139 -is
   3.140 -  "MPAIR"
   3.141 -
   3.142 -quotient_definition
   3.143 -  "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
   3.144 -is
   3.145 -  "CRYPT"
   3.146 -
   3.147 -quotient_definition
   3.148 -  "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
   3.149 -is
   3.150 -  "DECRYPT"
   3.151 -
   3.152 -lemma [quot_respect]:
   3.153 -  shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
   3.154 -by (auto intro: CRYPT)
   3.155 -
   3.156 -lemma [quot_respect]:
   3.157 -  shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
   3.158 -by (auto intro: DECRYPT)
   3.159 -
   3.160 -text{*Establishing these two equations is the point of the whole exercise*}
   3.161 -theorem CD_eq [simp]: 
   3.162 -  shows "Crypt K (Decrypt K X) = X"
   3.163 -  by (lifting CD)
   3.164 -
   3.165 -theorem DC_eq [simp]: 
   3.166 -  shows "Decrypt K (Crypt K X) = X"
   3.167 -  by (lifting DC)
   3.168 -
   3.169 -subsection{*The Abstract Function to Return the Set of Nonces*}
   3.170 -
   3.171 -quotient_definition
   3.172 -   "nonces:: msg \<Rightarrow> nat set"
   3.173 -is
   3.174 -  "freenonces"
   3.175 -
   3.176 -text{*Now prove the four equations for @{term nonces}*}
   3.177 -
   3.178 -lemma [quot_respect]:
   3.179 -  shows "(op \<sim> ===> op =) freenonces freenonces"
   3.180 -  by (simp add: msgrel_imp_eq_freenonces)
   3.181 -
   3.182 -lemma [quot_respect]:
   3.183 -  shows "(op = ===> op \<sim>) NONCE NONCE"
   3.184 -  by (simp add: NONCE)
   3.185 -
   3.186 -lemma nonces_Nonce [simp]: 
   3.187 -  shows "nonces (Nonce N) = {N}"
   3.188 -  by (lifting freenonces.simps(1))
   3.189 - 
   3.190 -lemma [quot_respect]:
   3.191 -  shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
   3.192 -  by (simp add: MPAIR)
   3.193 -
   3.194 -lemma nonces_MPair [simp]: 
   3.195 -  shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
   3.196 -  by (lifting freenonces.simps(2))
   3.197 -
   3.198 -lemma nonces_Crypt [simp]: 
   3.199 -  shows "nonces (Crypt K X) = nonces X"
   3.200 -  by (lifting freenonces.simps(3))
   3.201 -
   3.202 -lemma nonces_Decrypt [simp]: 
   3.203 -  shows "nonces (Decrypt K X) = nonces X"
   3.204 -  by (lifting freenonces.simps(4))
   3.205 -
   3.206 -subsection{*The Abstract Function to Return the Left Part*}
   3.207 -
   3.208 -quotient_definition
   3.209 -  "left:: msg \<Rightarrow> msg"
   3.210 -is
   3.211 -  "freeleft"
   3.212 -
   3.213 -lemma [quot_respect]:
   3.214 -  shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
   3.215 -  by (simp add: msgrel_imp_eqv_freeleft)
   3.216 -
   3.217 -lemma left_Nonce [simp]: 
   3.218 -  shows "left (Nonce N) = Nonce N"
   3.219 -  by (lifting freeleft.simps(1))
   3.220 -
   3.221 -lemma left_MPair [simp]: 
   3.222 -  shows "left (MPair X Y) = X"
   3.223 -  by (lifting freeleft.simps(2))
   3.224 -
   3.225 -lemma left_Crypt [simp]: 
   3.226 -  shows "left (Crypt K X) = left X"
   3.227 -  by (lifting freeleft.simps(3))
   3.228 -
   3.229 -lemma left_Decrypt [simp]: 
   3.230 -  shows "left (Decrypt K X) = left X"
   3.231 -  by (lifting freeleft.simps(4))
   3.232 -
   3.233 -subsection{*The Abstract Function to Return the Right Part*}
   3.234 -
   3.235 -quotient_definition
   3.236 -  "right:: msg \<Rightarrow> msg"
   3.237 -is
   3.238 -  "freeright"
   3.239 -
   3.240 -text{*Now prove the four equations for @{term right}*}
   3.241 -
   3.242 -lemma [quot_respect]:
   3.243 -  shows "(op \<sim> ===> op \<sim>) freeright freeright"
   3.244 -  by (simp add: msgrel_imp_eqv_freeright)
   3.245 -
   3.246 -lemma right_Nonce [simp]: 
   3.247 -  shows "right (Nonce N) = Nonce N"
   3.248 -  by (lifting freeright.simps(1))
   3.249 -
   3.250 -lemma right_MPair [simp]: 
   3.251 -  shows "right (MPair X Y) = Y"
   3.252 -  by (lifting freeright.simps(2))
   3.253 -
   3.254 -lemma right_Crypt [simp]: 
   3.255 -  shows "right (Crypt K X) = right X"
   3.256 -  by (lifting freeright.simps(3))
   3.257 -
   3.258 -lemma right_Decrypt [simp]: 
   3.259 -  shows "right (Decrypt K X) = right X"
   3.260 -  by (lifting freeright.simps(4))
   3.261 -
   3.262 -subsection{*Injectivity Properties of Some Constructors*}
   3.263 -
   3.264 -lemma NONCE_imp_eq: 
   3.265 -  shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
   3.266 -  by (drule msgrel_imp_eq_freenonces, simp)
   3.267 -
   3.268 -text{*Can also be proved using the function @{term nonces}*}
   3.269 -lemma Nonce_Nonce_eq [iff]: 
   3.270 -  shows "(Nonce m = Nonce n) = (m = n)"
   3.271 -proof
   3.272 -  assume "Nonce m = Nonce n"
   3.273 -  then show "m = n" by (lifting NONCE_imp_eq)
   3.274 -next
   3.275 -  assume "m = n" 
   3.276 -  then show "Nonce m = Nonce n" by simp
   3.277 -qed
   3.278 -
   3.279 -lemma MPAIR_imp_eqv_left: 
   3.280 -  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
   3.281 -  by (drule msgrel_imp_eqv_freeleft) (simp)
   3.282 -
   3.283 -lemma MPair_imp_eq_left: 
   3.284 -  assumes eq: "MPair X Y = MPair X' Y'" 
   3.285 -  shows "X = X'"
   3.286 -  using eq by (lifting MPAIR_imp_eqv_left)
   3.287 -
   3.288 -lemma MPAIR_imp_eqv_right: 
   3.289 -  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
   3.290 -  by (drule msgrel_imp_eqv_freeright) (simp)
   3.291 -
   3.292 -lemma MPair_imp_eq_right: 
   3.293 -  shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
   3.294 -  by (lifting  MPAIR_imp_eqv_right)
   3.295 -
   3.296 -theorem MPair_MPair_eq [iff]: 
   3.297 -  shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" 
   3.298 -  by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
   3.299 -
   3.300 -lemma NONCE_neqv_MPAIR: 
   3.301 -  shows "\<not>(NONCE m \<sim> MPAIR X Y)"
   3.302 -  by (auto dest: msgrel_imp_eq_freediscrim)
   3.303 -
   3.304 -theorem Nonce_neq_MPair [iff]: 
   3.305 -  shows "Nonce N \<noteq> MPair X Y"
   3.306 -  by (lifting NONCE_neqv_MPAIR)
   3.307 -
   3.308 -text{*Example suggested by a referee*}
   3.309 -
   3.310 -lemma CRYPT_NONCE_neq_NONCE:
   3.311 -  shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
   3.312 -  by (auto dest: msgrel_imp_eq_freediscrim)
   3.313 -
   3.314 -theorem Crypt_Nonce_neq_Nonce: 
   3.315 -  shows "Crypt K (Nonce M) \<noteq> Nonce N"
   3.316 -  by (lifting CRYPT_NONCE_neq_NONCE)
   3.317 -
   3.318 -text{*...and many similar results*}
   3.319 -lemma CRYPT2_NONCE_neq_NONCE: 
   3.320 -  shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
   3.321 -  by (auto dest: msgrel_imp_eq_freediscrim)  
   3.322 -
   3.323 -theorem Crypt2_Nonce_neq_Nonce: 
   3.324 -  shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
   3.325 -  by (lifting CRYPT2_NONCE_neq_NONCE) 
   3.326 -
   3.327 -theorem Crypt_Crypt_eq [iff]: 
   3.328 -  shows "(Crypt K X = Crypt K X') = (X=X')" 
   3.329 -proof
   3.330 -  assume "Crypt K X = Crypt K X'"
   3.331 -  hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
   3.332 -  thus "X = X'" by simp
   3.333 -next
   3.334 -  assume "X = X'"
   3.335 -  thus "Crypt K X = Crypt K X'" by simp
   3.336 -qed
   3.337 -
   3.338 -theorem Decrypt_Decrypt_eq [iff]: 
   3.339 -  shows "(Decrypt K X = Decrypt K X') = (X=X')" 
   3.340 -proof
   3.341 -  assume "Decrypt K X = Decrypt K X'"
   3.342 -  hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
   3.343 -  thus "X = X'" by simp
   3.344 -next
   3.345 -  assume "X = X'"
   3.346 -  thus "Decrypt K X = Decrypt K X'" by simp
   3.347 -qed
   3.348 -
   3.349 -lemma msg_induct_aux:
   3.350 -  shows "\<lbrakk>\<And>N. P (Nonce N);
   3.351 -          \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
   3.352 -          \<And>K X. P X \<Longrightarrow> P (Crypt K X);
   3.353 -          \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
   3.354 -  by (lifting freemsg.induct)
   3.355 -
   3.356 -lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
   3.357 -  assumes N: "\<And>N. P (Nonce N)"
   3.358 -      and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
   3.359 -      and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
   3.360 -      and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
   3.361 -  shows "P msg"
   3.362 -  using N M C D by (rule msg_induct_aux)
   3.363 -
   3.364 -subsection{*The Abstract Discriminator*}
   3.365 -
   3.366 -text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
   3.367 -need this function in order to prove discrimination theorems.*}
   3.368 -
   3.369 -quotient_definition
   3.370 -  "discrim:: msg \<Rightarrow> int"
   3.371 -is
   3.372 -  "freediscrim"
   3.373 -
   3.374 -text{*Now prove the four equations for @{term discrim}*}
   3.375 -
   3.376 -lemma [quot_respect]:
   3.377 -  shows "(op \<sim> ===> op =) freediscrim freediscrim"
   3.378 -  by (auto simp add: msgrel_imp_eq_freediscrim)
   3.379 -
   3.380 -lemma discrim_Nonce [simp]: 
   3.381 -  shows "discrim (Nonce N) = 0"
   3.382 -  by (lifting freediscrim.simps(1))
   3.383 -
   3.384 -lemma discrim_MPair [simp]: 
   3.385 -  shows "discrim (MPair X Y) = 1"
   3.386 -  by (lifting freediscrim.simps(2))
   3.387 -
   3.388 -lemma discrim_Crypt [simp]: 
   3.389 -  shows "discrim (Crypt K X) = discrim X + 2"
   3.390 -  by (lifting freediscrim.simps(3))
   3.391 -
   3.392 -lemma discrim_Decrypt [simp]: 
   3.393 -  shows "discrim (Decrypt K X) = discrim X - 2"
   3.394 -  by (lifting freediscrim.simps(4))
   3.395 -
   3.396 -end
   3.397 -
     4.1 --- a/src/HOL/Quotient_Examples/LarryInt.thy	Wed Apr 28 17:42:37 2010 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,395 +0,0 @@
     4.4 -
     4.5 -header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
     4.6 -
     4.7 -theory LarryInt
     4.8 -imports Main Quotient_Product
     4.9 -begin
    4.10 -
    4.11 -fun
    4.12 -  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" 
    4.13 -where
    4.14 -  "intrel (x, y) (u, v) = (x + v = u + y)"
    4.15 -
    4.16 -quotient_type int = "nat \<times> nat" / intrel
    4.17 -  by (auto simp add: equivp_def expand_fun_eq)
    4.18 -
    4.19 -instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
    4.20 -begin
    4.21 -
    4.22 -quotient_definition
    4.23 -  Zero_int_def: "0::int" is "(0::nat, 0::nat)"
    4.24 -
    4.25 -quotient_definition
    4.26 -  One_int_def: "1::int" is "(1::nat, 0::nat)"
    4.27 -
    4.28 -definition
    4.29 -  "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
    4.30 -
    4.31 -quotient_definition
    4.32 -  "(op +) :: int \<Rightarrow> int \<Rightarrow> int" 
    4.33 -is
    4.34 -  "add_raw"
    4.35 -
    4.36 -definition
    4.37 -  "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
    4.38 -
    4.39 -quotient_definition
    4.40 -  "uminus :: int \<Rightarrow> int" 
    4.41 -is
    4.42 -  "uminus_raw"
    4.43 -
    4.44 -fun
    4.45 -  mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
    4.46 -where
    4.47 -  "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
    4.48 -
    4.49 -quotient_definition
    4.50 -  "(op *) :: int \<Rightarrow> int \<Rightarrow> int" 
    4.51 -is
    4.52 -  "mult_raw"
    4.53 -
    4.54 -definition
    4.55 -  "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
    4.56 -
    4.57 -quotient_definition 
    4.58 -  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" 
    4.59 -is
    4.60 -  "le_raw"
    4.61 -
    4.62 -definition
    4.63 -  less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
    4.64 -
    4.65 -definition
    4.66 -  diff_int_def:  "z - (w::int) \<equiv> z + (-w)"
    4.67 -
    4.68 -instance ..
    4.69 -
    4.70 -end
    4.71 -
    4.72 -subsection{*Construction of the Integers*}
    4.73 -
    4.74 -lemma zminus_zminus_raw:
    4.75 -  "uminus_raw (uminus_raw z) = z"
    4.76 -  by (cases z) (simp add: uminus_raw_def)
    4.77 -
    4.78 -lemma [quot_respect]:
    4.79 -  shows "(intrel ===> intrel) uminus_raw uminus_raw"
    4.80 -  by (simp add: uminus_raw_def)
    4.81 -  
    4.82 -lemma zminus_zminus:
    4.83 -  fixes z::"int"
    4.84 -  shows "- (- z) = z"
    4.85 -  by(lifting zminus_zminus_raw)
    4.86 -
    4.87 -lemma zminus_0_raw:
    4.88 -  shows "uminus_raw (0, 0) = (0, 0::nat)"
    4.89 -  by (simp add: uminus_raw_def)
    4.90 -
    4.91 -lemma zminus_0: 
    4.92 -  shows "- 0 = (0::int)"
    4.93 -  by (lifting zminus_0_raw)
    4.94 -
    4.95 -subsection{*Integer Addition*}
    4.96 -
    4.97 -lemma zminus_zadd_distrib_raw:
    4.98 -  shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"
    4.99 -by (cases z, cases w)
   4.100 -   (auto simp add: add_raw_def uminus_raw_def)
   4.101 -
   4.102 -lemma [quot_respect]:
   4.103 -  shows "(intrel ===> intrel ===> intrel) add_raw add_raw"
   4.104 -by (simp add: add_raw_def)
   4.105 -
   4.106 -lemma zminus_zadd_distrib: 
   4.107 -  fixes z w::"int"
   4.108 -  shows "- (z + w) = (- z) + (- w)"
   4.109 -  by(lifting zminus_zadd_distrib_raw)
   4.110 -
   4.111 -lemma zadd_commute_raw:
   4.112 -  shows "add_raw z w = add_raw w z"
   4.113 -by (cases z, cases w)
   4.114 -   (simp add: add_raw_def)
   4.115 -
   4.116 -lemma zadd_commute:
   4.117 -  fixes z w::"int"
   4.118 -  shows "(z::int) + w = w + z"
   4.119 -  by (lifting zadd_commute_raw)
   4.120 -
   4.121 -lemma zadd_assoc_raw:
   4.122 -  shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
   4.123 -  by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
   4.124 -
   4.125 -lemma zadd_assoc: 
   4.126 -  fixes z1 z2 z3::"int"
   4.127 -  shows "(z1 + z2) + z3 = z1 + (z2 + z3)"
   4.128 -  by (lifting zadd_assoc_raw)
   4.129 -
   4.130 -lemma zadd_0_raw:
   4.131 -  shows "add_raw (0, 0) z = z"
   4.132 -  by (simp add: add_raw_def)
   4.133 -
   4.134 -
   4.135 -text {*also for the instance declaration int :: plus_ac0*}
   4.136 -lemma zadd_0: 
   4.137 -  fixes z::"int"
   4.138 -  shows "0 + z = z"
   4.139 -  by (lifting zadd_0_raw)
   4.140 -
   4.141 -lemma zadd_zminus_inverse_raw:
   4.142 -  shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
   4.143 -  by (cases z) (simp add: add_raw_def uminus_raw_def)
   4.144 -
   4.145 -lemma zadd_zminus_inverse2: 
   4.146 -  fixes z::"int"
   4.147 -  shows "(- z) + z = 0"
   4.148 -  by (lifting zadd_zminus_inverse_raw)
   4.149 -
   4.150 -subsection{*Integer Multiplication*}
   4.151 -
   4.152 -lemma zmult_zminus_raw:
   4.153 -  shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
   4.154 -apply(cases z, cases w)
   4.155 -apply(simp add: uminus_raw_def)
   4.156 -done
   4.157 -
   4.158 -lemma mult_raw_fst:
   4.159 -  assumes a: "intrel x z"
   4.160 -  shows "intrel (mult_raw x y) (mult_raw z y)"
   4.161 -using a
   4.162 -apply(cases x, cases y, cases z)
   4.163 -apply(auto simp add: mult_raw.simps intrel.simps)
   4.164 -apply(rename_tac u v w x y z)
   4.165 -apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
   4.166 -apply(simp add: mult_ac)
   4.167 -apply(simp add: add_mult_distrib [symmetric])
   4.168 -done
   4.169 -
   4.170 -lemma mult_raw_snd:
   4.171 -  assumes a: "intrel x z"
   4.172 -  shows "intrel (mult_raw y x) (mult_raw y z)"
   4.173 -using a
   4.174 -apply(cases x, cases y, cases z)
   4.175 -apply(auto simp add: mult_raw.simps intrel.simps)
   4.176 -apply(rename_tac u v w x y z)
   4.177 -apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
   4.178 -apply(simp add: mult_ac)
   4.179 -apply(simp add: add_mult_distrib [symmetric])
   4.180 -done
   4.181 -
   4.182 -lemma [quot_respect]:
   4.183 -  shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
   4.184 -apply(simp only: fun_rel_def)
   4.185 -apply(rule allI | rule impI)+
   4.186 -apply(rule equivp_transp[OF int_equivp])
   4.187 -apply(rule mult_raw_fst)
   4.188 -apply(assumption)
   4.189 -apply(rule mult_raw_snd)
   4.190 -apply(assumption)
   4.191 -done
   4.192 -
   4.193 -lemma zmult_zminus: 
   4.194 -  fixes z w::"int"
   4.195 -  shows "(- z) * w = - (z * w)"
   4.196 -  by (lifting zmult_zminus_raw)
   4.197 -
   4.198 -lemma zmult_commute_raw: 
   4.199 -  shows "mult_raw z w = mult_raw w z"
   4.200 -apply(cases z, cases w)
   4.201 -apply(simp add: add_ac mult_ac)
   4.202 -done
   4.203 -
   4.204 -lemma zmult_commute: 
   4.205 -  fixes z w::"int"
   4.206 -  shows "z * w = w * z"
   4.207 -  by (lifting zmult_commute_raw)
   4.208 -
   4.209 -lemma zmult_assoc_raw:
   4.210 -  shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
   4.211 -apply(cases z1, cases z2, cases z3)
   4.212 -apply(simp add: add_mult_distrib2 mult_ac)
   4.213 -done
   4.214 -
   4.215 -lemma zmult_assoc: 
   4.216 -  fixes z1 z2 z3::"int"
   4.217 -  shows "(z1 * z2) * z3 = z1 * (z2 * z3)"
   4.218 -  by (lifting zmult_assoc_raw)
   4.219 -
   4.220 -lemma zadd_mult_distrib_raw:
   4.221 -  shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
   4.222 -apply(cases z1, cases z2, cases w)
   4.223 -apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
   4.224 -done
   4.225 -
   4.226 -lemma zadd_zmult_distrib: 
   4.227 -  fixes z1 z2 w::"int"
   4.228 -  shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"
   4.229 -  by(lifting zadd_mult_distrib_raw)
   4.230 -
   4.231 -lemma zadd_zmult_distrib2: 
   4.232 -  fixes w z1 z2::"int"
   4.233 -  shows "w * (z1 + z2) = (w * z1) + (w * z2)"
   4.234 -  by (simp add: zmult_commute [of w] zadd_zmult_distrib)
   4.235 -
   4.236 -lemma zdiff_zmult_distrib: 
   4.237 -  fixes w z1 z2::"int"
   4.238 -  shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"
   4.239 -  by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
   4.240 -
   4.241 -lemma zdiff_zmult_distrib2: 
   4.242 -  fixes w z1 z2::"int"
   4.243 -  shows "w * (z1 - z2) = (w * z1) - (w * z2)"
   4.244 -  by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
   4.245 -
   4.246 -lemmas int_distrib =
   4.247 -  zadd_zmult_distrib zadd_zmult_distrib2
   4.248 -  zdiff_zmult_distrib zdiff_zmult_distrib2
   4.249 -
   4.250 -lemma zmult_1_raw:
   4.251 -  shows "mult_raw (1, 0) z = z"
   4.252 -  by (cases z) (auto)
   4.253 -
   4.254 -lemma zmult_1:
   4.255 -  fixes z::"int"
   4.256 -  shows "1 * z = z"
   4.257 -  by (lifting zmult_1_raw)
   4.258 -
   4.259 -lemma zmult_1_right: 
   4.260 -  fixes z::"int"
   4.261 -  shows "z * 1 = z"
   4.262 -  by (rule trans [OF zmult_commute zmult_1])
   4.263 -
   4.264 -lemma zero_not_one:
   4.265 -  shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
   4.266 -  by auto
   4.267 -
   4.268 -text{*The Integers Form A Ring*}
   4.269 -instance int :: comm_ring_1
   4.270 -proof
   4.271 -  fix i j k :: int
   4.272 -  show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
   4.273 -  show "i + j = j + i" by (simp add: zadd_commute)
   4.274 -  show "0 + i = i" by (rule zadd_0)
   4.275 -  show "- i + i = 0" by (rule zadd_zminus_inverse2)
   4.276 -  show "i - j = i + (-j)" by (simp add: diff_int_def)
   4.277 -  show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
   4.278 -  show "i * j = j * i" by (rule zmult_commute)
   4.279 -  show "1 * i = i" by (rule zmult_1) 
   4.280 -  show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
   4.281 -  show "0 \<noteq> (1::int)" by (lifting zero_not_one)
   4.282 -qed
   4.283 -
   4.284 -
   4.285 -subsection{*The @{text "\<le>"} Ordering*}
   4.286 -
   4.287 -lemma zle_refl_raw:
   4.288 -  shows "le_raw w w"
   4.289 -  by (cases w) (simp add: le_raw_def)
   4.290 -
   4.291 -lemma [quot_respect]:
   4.292 -  shows "(intrel ===> intrel ===> op =) le_raw le_raw"
   4.293 -  by (auto) (simp_all add: le_raw_def)
   4.294 -
   4.295 -lemma zle_refl: 
   4.296 -  fixes w::"int"
   4.297 -  shows "w \<le> w"
   4.298 -  by (lifting zle_refl_raw)
   4.299 -
   4.300 -
   4.301 -lemma zle_trans_raw:
   4.302 -  shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
   4.303 -apply(cases i, cases j, cases k)
   4.304 -apply(auto simp add: le_raw_def)
   4.305 -done
   4.306 -
   4.307 -lemma zle_trans: 
   4.308 -  fixes i j k::"int"
   4.309 -  shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
   4.310 -  by (lifting zle_trans_raw)
   4.311 -
   4.312 -lemma zle_anti_sym_raw:
   4.313 -  shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
   4.314 -apply(cases z, cases w)
   4.315 -apply(auto iff: le_raw_def)
   4.316 -done
   4.317 -
   4.318 -lemma zle_anti_sym: 
   4.319 -  fixes z w::"int"
   4.320 -  shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"
   4.321 -  by (lifting zle_anti_sym_raw)
   4.322 -
   4.323 -
   4.324 -(* Axiom 'order_less_le' of class 'order': *)
   4.325 -lemma zless_le: 
   4.326 -  fixes w z::"int"
   4.327 -  shows "(w < z) = (w \<le> z & w \<noteq> z)"
   4.328 -  by (simp add: less_int_def)
   4.329 -
   4.330 -instance int :: order
   4.331 -apply (default)
   4.332 -apply(auto simp add: zless_le zle_anti_sym)[1]
   4.333 -apply(rule zle_refl)
   4.334 -apply(erule zle_trans, assumption)
   4.335 -apply(erule zle_anti_sym, assumption)
   4.336 -done
   4.337 -
   4.338 -(* Axiom 'linorder_linear' of class 'linorder': *)
   4.339 -
   4.340 -lemma zle_linear_raw:
   4.341 -  shows "le_raw z w \<or> le_raw w z"
   4.342 -apply(cases w, cases z)
   4.343 -apply(auto iff: le_raw_def)
   4.344 -done
   4.345 -
   4.346 -lemma zle_linear: 
   4.347 -  fixes z w::"int"
   4.348 -  shows "z \<le> w \<or> w \<le> z"
   4.349 -  by (lifting zle_linear_raw)
   4.350 -
   4.351 -instance int :: linorder
   4.352 -apply(default)
   4.353 -apply(rule zle_linear)
   4.354 -done
   4.355 -
   4.356 -lemma zadd_left_mono_raw:
   4.357 -  shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
   4.358 -apply(cases k)
   4.359 -apply(auto simp add: add_raw_def le_raw_def)
   4.360 -done
   4.361 -
   4.362 -lemma zadd_left_mono: 
   4.363 -  fixes i j::"int"
   4.364 -  shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"
   4.365 -  by (lifting zadd_left_mono_raw)
   4.366 -
   4.367 -
   4.368 -subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
   4.369 -
   4.370 -definition
   4.371 -  "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
   4.372 -
   4.373 -quotient_definition
   4.374 -  "nat2::int \<Rightarrow> nat"
   4.375 -is
   4.376 -  "nat_raw"
   4.377 -
   4.378 -abbreviation
   4.379 -  "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"
   4.380 -
   4.381 -lemma nat_le_eq_zle_raw:
   4.382 -  shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
   4.383 -  apply (cases w)
   4.384 -  apply (cases z)
   4.385 -  apply (simp add: nat_raw_def le_raw_def)
   4.386 -  by auto
   4.387 -
   4.388 -lemma [quot_respect]:
   4.389 -  shows "(intrel ===> op =) nat_raw nat_raw"
   4.390 -  by (auto iff: nat_raw_def)
   4.391 -
   4.392 -lemma nat_le_eq_zle: 
   4.393 -  fixes w z::"int"
   4.394 -  shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
   4.395 -  unfolding less_int_def
   4.396 -  by (lifting nat_le_eq_zle_raw)
   4.397 -
   4.398 -end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Thu Apr 29 09:06:35 2010 +0200
     5.3 @@ -0,0 +1,380 @@
     5.4 +(*  Title:      HOL/Quotient_Examples/Quotient_Int.thy
     5.5 +    Author:     Cezary Kaliszyk
     5.6 +    Author:     Christian Urban
     5.7 +
     5.8 +Integers based on Quotients, based on an older version by Larry Paulson.
     5.9 +*)
    5.10 +theory Quotient_Int
    5.11 +imports Quotient_Product Nat
    5.12 +begin
    5.13 +
    5.14 +fun
    5.15 +  intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
    5.16 +where
    5.17 +  "intrel (x, y) (u, v) = (x + v = u + y)"
    5.18 +
    5.19 +quotient_type int = "nat \<times> nat" / intrel
    5.20 +  by (auto simp add: equivp_def expand_fun_eq)
    5.21 +
    5.22 +instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
    5.23 +begin
    5.24 +
    5.25 +quotient_definition
    5.26 +  "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
    5.27 +
    5.28 +quotient_definition
    5.29 +  "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
    5.30 +
    5.31 +fun
    5.32 +  plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
    5.33 +where
    5.34 +  "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
    5.35 +
    5.36 +quotient_definition
    5.37 +  "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
    5.38 +
    5.39 +fun
    5.40 +  uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
    5.41 +where
    5.42 +  "uminus_int_raw (x, y) = (y, x)"
    5.43 +
    5.44 +quotient_definition
    5.45 +  "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
    5.46 +
    5.47 +definition
    5.48 +  minus_int_def [code del]:  "z - w = z + (-w\<Colon>int)"
    5.49 +
    5.50 +fun
    5.51 +  times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
    5.52 +where
    5.53 +  "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
    5.54 +
    5.55 +quotient_definition
    5.56 +  "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
    5.57 +
    5.58 +fun
    5.59 +  le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
    5.60 +where
    5.61 +  "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
    5.62 +
    5.63 +quotient_definition
    5.64 +  le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
    5.65 +
    5.66 +definition
    5.67 +  less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
    5.68 +
    5.69 +definition
    5.70 +  zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
    5.71 +
    5.72 +definition
    5.73 +  zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
    5.74 +
    5.75 +instance ..
    5.76 +
    5.77 +end
    5.78 +
    5.79 +lemma [quot_respect]:
    5.80 +  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
    5.81 +  and   "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
    5.82 +  and   "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
    5.83 +  by auto
    5.84 +
    5.85 +lemma times_int_raw_fst:
    5.86 +  assumes a: "x \<approx> z"
    5.87 +  shows "times_int_raw x y \<approx> times_int_raw z y"
    5.88 +  using a
    5.89 +  apply(cases x, cases y, cases z)
    5.90 +  apply(auto simp add: times_int_raw.simps intrel.simps)
    5.91 +  apply(rename_tac u v w x y z)
    5.92 +  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
    5.93 +  apply(simp add: mult_ac)
    5.94 +  apply(simp add: add_mult_distrib [symmetric])
    5.95 +  done
    5.96 +
    5.97 +lemma times_int_raw_snd:
    5.98 +  assumes a: "x \<approx> z"
    5.99 +  shows "times_int_raw y x \<approx> times_int_raw y z"
   5.100 +  using a
   5.101 +  apply(cases x, cases y, cases z)
   5.102 +  apply(auto simp add: times_int_raw.simps intrel.simps)
   5.103 +  apply(rename_tac u v w x y z)
   5.104 +  apply(subgoal_tac "u*w + z*w = y*w + v*w  &  u*x + z*x = y*x + v*x")
   5.105 +  apply(simp add: mult_ac)
   5.106 +  apply(simp add: add_mult_distrib [symmetric])
   5.107 +  done
   5.108 +
   5.109 +lemma [quot_respect]:
   5.110 +  shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
   5.111 +  apply(simp only: fun_rel_def)
   5.112 +  apply(rule allI | rule impI)+
   5.113 +  apply(rule equivp_transp[OF int_equivp])
   5.114 +  apply(rule times_int_raw_fst)
   5.115 +  apply(assumption)
   5.116 +  apply(rule times_int_raw_snd)
   5.117 +  apply(assumption)
   5.118 +  done
   5.119 +
   5.120 +lemma plus_assoc_raw:
   5.121 +  shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)"
   5.122 +  by (cases i, cases j, cases k) (simp)
   5.123 +
   5.124 +lemma plus_sym_raw:
   5.125 +  shows "plus_int_raw i j \<approx> plus_int_raw j i"
   5.126 +  by (cases i, cases j) (simp)
   5.127 +
   5.128 +lemma plus_zero_raw:
   5.129 +  shows "plus_int_raw (0, 0) i \<approx> i"
   5.130 +  by (cases i) (simp)
   5.131 +
   5.132 +lemma plus_minus_zero_raw:
   5.133 +  shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
   5.134 +  by (cases i) (simp)
   5.135 +
   5.136 +lemma times_assoc_raw:
   5.137 +  shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)"
   5.138 +  by (cases i, cases j, cases k)
   5.139 +     (simp add: algebra_simps)
   5.140 +
   5.141 +lemma times_sym_raw:
   5.142 +  shows "times_int_raw i j \<approx> times_int_raw j i"
   5.143 +  by (cases i, cases j) (simp add: algebra_simps)
   5.144 +
   5.145 +lemma times_one_raw:
   5.146 +  shows "times_int_raw  (1, 0) i \<approx> i"
   5.147 +  by (cases i) (simp)
   5.148 +
   5.149 +lemma times_plus_comm_raw:
   5.150 +  shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)"
   5.151 +by (cases i, cases j, cases k)
   5.152 +   (simp add: algebra_simps)
   5.153 +
   5.154 +lemma one_zero_distinct:
   5.155 +  shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
   5.156 +  by simp
   5.157 +
   5.158 +text{* The integers form a @{text comm_ring_1}*}
   5.159 +
   5.160 +instance int :: comm_ring_1
   5.161 +proof
   5.162 +  fix i j k :: int
   5.163 +  show "(i + j) + k = i + (j + k)"
   5.164 +    by (lifting plus_assoc_raw)
   5.165 +  show "i + j = j + i"
   5.166 +    by (lifting plus_sym_raw)
   5.167 +  show "0 + i = (i::int)"
   5.168 +    by (lifting plus_zero_raw)
   5.169 +  show "- i + i = 0"
   5.170 +    by (lifting plus_minus_zero_raw)
   5.171 +  show "i - j = i + - j"
   5.172 +    by (simp add: minus_int_def)
   5.173 +  show "(i * j) * k = i * (j * k)"
   5.174 +    by (lifting times_assoc_raw)
   5.175 +  show "i * j = j * i"
   5.176 +    by (lifting times_sym_raw)
   5.177 +  show "1 * i = i"
   5.178 +    by (lifting times_one_raw)
   5.179 +  show "(i + j) * k = i * k + j * k"
   5.180 +    by (lifting times_plus_comm_raw)
   5.181 +  show "0 \<noteq> (1::int)"
   5.182 +    by (lifting one_zero_distinct)
   5.183 +qed
   5.184 +
   5.185 +lemma plus_int_raw_rsp_aux:
   5.186 +  assumes a: "a \<approx> b" "c \<approx> d"
   5.187 +  shows "plus_int_raw a c \<approx> plus_int_raw b d"
   5.188 +  using a
   5.189 +  by (cases a, cases b, cases c, cases d)
   5.190 +     (simp)
   5.191 +
   5.192 +lemma add_abs_int:
   5.193 +  "(abs_int (x,y)) + (abs_int (u,v)) =
   5.194 +   (abs_int (x + u, y + v))"
   5.195 +  apply(simp add: plus_int_def id_simps)
   5.196 +  apply(fold plus_int_raw.simps)
   5.197 +  apply(rule Quotient_rel_abs[OF Quotient_int])
   5.198 +  apply(rule plus_int_raw_rsp_aux)
   5.199 +  apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
   5.200 +  done
   5.201 +
   5.202 +definition int_of_nat_raw:
   5.203 +  "int_of_nat_raw m = (m :: nat, 0 :: nat)"
   5.204 +
   5.205 +quotient_definition
   5.206 +  "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
   5.207 +
   5.208 +lemma[quot_respect]:
   5.209 +  shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
   5.210 +  by (simp add: equivp_reflp[OF int_equivp])
   5.211 +
   5.212 +lemma int_of_nat:
   5.213 +  shows "of_nat m = int_of_nat m"
   5.214 +  by (induct m)
   5.215 +     (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
   5.216 +
   5.217 +lemma le_antisym_raw:
   5.218 +  shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j"
   5.219 +  by (cases i, cases j) (simp)
   5.220 +
   5.221 +lemma le_refl_raw:
   5.222 +  shows "le_int_raw i i"
   5.223 +  by (cases i) (simp)
   5.224 +
   5.225 +lemma le_trans_raw:
   5.226 +  shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
   5.227 +  by (cases i, cases j, cases k) (simp)
   5.228 +
   5.229 +lemma le_cases_raw:
   5.230 +  shows "le_int_raw i j \<or> le_int_raw j i"
   5.231 +  by (cases i, cases j)
   5.232 +     (simp add: linorder_linear)
   5.233 +
   5.234 +instance int :: linorder
   5.235 +proof
   5.236 +  fix i j k :: int
   5.237 +  show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
   5.238 +    by (lifting le_antisym_raw)
   5.239 +  show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
   5.240 +    by (auto simp add: less_int_def dest: antisym)
   5.241 +  show "i \<le> i"
   5.242 +    by (lifting le_refl_raw)
   5.243 +  show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
   5.244 +    by (lifting le_trans_raw)
   5.245 +  show "i \<le> j \<or> j \<le> i"
   5.246 +    by (lifting le_cases_raw)
   5.247 +qed
   5.248 +
   5.249 +instantiation int :: distrib_lattice
   5.250 +begin
   5.251 +
   5.252 +definition
   5.253 +  "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
   5.254 +
   5.255 +definition
   5.256 +  "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
   5.257 +
   5.258 +instance
   5.259 +  by default
   5.260 +     (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
   5.261 +
   5.262 +end
   5.263 +
   5.264 +lemma le_plus_int_raw:
   5.265 +  shows "le_int_raw i j \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)"
   5.266 +  by (cases i, cases j, cases k) (simp)
   5.267 +
   5.268 +instance int :: ordered_cancel_ab_semigroup_add
   5.269 +proof
   5.270 +  fix i j k :: int
   5.271 +  show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
   5.272 +    by (lifting le_plus_int_raw)
   5.273 +qed
   5.274 +
   5.275 +abbreviation
   5.276 +  "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)"
   5.277 +
   5.278 +lemma zmult_zless_mono2_lemma:
   5.279 +  fixes i j::int
   5.280 +  and   k::nat
   5.281 +  shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
   5.282 +  apply(induct "k")
   5.283 +  apply(simp)
   5.284 +  apply(case_tac "k = 0")
   5.285 +  apply(simp_all add: left_distrib add_strict_mono)
   5.286 +  done
   5.287 +
   5.288 +lemma zero_le_imp_eq_int_raw:
   5.289 +  fixes k::"(nat \<times> nat)"
   5.290 +  shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
   5.291 +  apply(cases k)
   5.292 +  apply(simp add:int_of_nat_raw)
   5.293 +  apply(auto)
   5.294 +  apply(rule_tac i="b" and j="a" in less_Suc_induct)
   5.295 +  apply(auto)
   5.296 +  done
   5.297 +
   5.298 +lemma zero_le_imp_eq_int:
   5.299 +  fixes k::int
   5.300 +  shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
   5.301 +  unfolding less_int_def int_of_nat
   5.302 +  by (lifting zero_le_imp_eq_int_raw)
   5.303 +
   5.304 +lemma zmult_zless_mono2:
   5.305 +  fixes i j k::int
   5.306 +  assumes a: "i < j" "0 < k"
   5.307 +  shows "k * i < k * j"
   5.308 +  using a
   5.309 +  by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
   5.310 +
   5.311 +text{*The integers form an ordered integral domain*}
   5.312 +
   5.313 +instance int :: linordered_idom
   5.314 +proof
   5.315 +  fix i j k :: int
   5.316 +  show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
   5.317 +    by (rule zmult_zless_mono2)
   5.318 +  show "\<bar>i\<bar> = (if i < 0 then -i else i)"
   5.319 +    by (simp only: zabs_def)
   5.320 +  show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
   5.321 +    by (simp only: zsgn_def)
   5.322 +qed
   5.323 +
   5.324 +lemmas int_distrib =
   5.325 +  left_distrib [of "z1::int" "z2" "w", standard]
   5.326 +  right_distrib [of "w::int" "z1" "z2", standard]
   5.327 +  left_diff_distrib [of "z1::int" "z2" "w", standard]
   5.328 +  right_diff_distrib [of "w::int" "z1" "z2", standard]
   5.329 +  minus_add_distrib[of "z1::int" "z2", standard]
   5.330 +
   5.331 +lemma int_induct_raw:
   5.332 +  assumes a: "P (0::nat, 0)"
   5.333 +  and     b: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (1, 0))"
   5.334 +  and     c: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (uminus_int_raw (1, 0)))"
   5.335 +  shows      "P x"
   5.336 +proof (cases x, clarify)
   5.337 +  fix a b
   5.338 +  show "P (a, b)"
   5.339 +  proof (induct a arbitrary: b rule: Nat.induct)
   5.340 +    case zero
   5.341 +    show "P (0, b)" using assms by (induct b) auto
   5.342 +  next
   5.343 +    case (Suc n)
   5.344 +    then show ?case using assms by auto
   5.345 +  qed
   5.346 +qed
   5.347 +
   5.348 +lemma int_induct:
   5.349 +  fixes x :: int
   5.350 +  assumes a: "P 0"
   5.351 +  and     b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
   5.352 +  and     c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
   5.353 +  shows      "P x"
   5.354 +  using a b c unfolding minus_int_def
   5.355 +  by (lifting int_induct_raw)
   5.356 +
   5.357 +text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
   5.358 +
   5.359 +definition
   5.360 +  "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
   5.361 +
   5.362 +quotient_definition
   5.363 +  "int_to_nat::int \<Rightarrow> nat"
   5.364 +is
   5.365 +  "int_to_nat_raw"
   5.366 +
   5.367 +lemma [quot_respect]:
   5.368 +  shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
   5.369 +  by (auto iff: int_to_nat_raw_def)
   5.370 +
   5.371 +lemma nat_le_eq_zle_raw:
   5.372 +  assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z"
   5.373 +  shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)"
   5.374 +  using a
   5.375 +  by (cases w, cases z) (auto simp add: int_to_nat_raw_def)
   5.376 +
   5.377 +lemma nat_le_eq_zle:
   5.378 +  fixes w z::"int"
   5.379 +  shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
   5.380 +  unfolding less_int_def
   5.381 +  by (lifting nat_le_eq_zle_raw)
   5.382 +
   5.383 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Thu Apr 29 09:06:35 2010 +0200
     6.3 @@ -0,0 +1,399 @@
     6.4 +(*  Title:      HOL/Quotient_Examples/Quotient_Message.thy
     6.5 +    Author:     Christian Urban
     6.6 +
     6.7 +Message datatype, based on an older version by Larry Paulson.
     6.8 +*)
     6.9 +theory Quotient_Message
    6.10 +imports Main Quotient_Syntax
    6.11 +begin
    6.12 +
    6.13 +subsection{*Defining the Free Algebra*}
    6.14 +
    6.15 +datatype
    6.16 +  freemsg = NONCE  nat
    6.17 +        | MPAIR  freemsg freemsg
    6.18 +        | CRYPT  nat freemsg
    6.19 +        | DECRYPT  nat freemsg
    6.20 +
    6.21 +inductive
    6.22 +  msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
    6.23 +where
    6.24 +  CD:    "CRYPT K (DECRYPT K X) \<sim> X"
    6.25 +| DC:    "DECRYPT K (CRYPT K X) \<sim> X"
    6.26 +| NONCE: "NONCE N \<sim> NONCE N"
    6.27 +| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
    6.28 +| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
    6.29 +| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
    6.30 +| SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
    6.31 +| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
    6.32 +
    6.33 +lemmas msgrel.intros[intro]
    6.34 +
    6.35 +text{*Proving that it is an equivalence relation*}
    6.36 +
    6.37 +lemma msgrel_refl: "X \<sim> X"
    6.38 +by (induct X, (blast intro: msgrel.intros)+)
    6.39 +
    6.40 +theorem equiv_msgrel: "equivp msgrel"
    6.41 +proof (rule equivpI)
    6.42 +  show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
    6.43 +  show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
    6.44 +  show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
    6.45 +qed
    6.46 +
    6.47 +subsection{*Some Functions on the Free Algebra*}
    6.48 +
    6.49 +subsubsection{*The Set of Nonces*}
    6.50 +
    6.51 +fun
    6.52 +  freenonces :: "freemsg \<Rightarrow> nat set"
    6.53 +where
    6.54 +  "freenonces (NONCE N) = {N}"
    6.55 +| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
    6.56 +| "freenonces (CRYPT K X) = freenonces X"
    6.57 +| "freenonces (DECRYPT K X) = freenonces X"
    6.58 +
    6.59 +theorem msgrel_imp_eq_freenonces:
    6.60 +  assumes a: "U \<sim> V"
    6.61 +  shows "freenonces U = freenonces V"
    6.62 +  using a by (induct) (auto)
    6.63 +
    6.64 +subsubsection{*The Left Projection*}
    6.65 +
    6.66 +text{*A function to return the left part of the top pair in a message.  It will
    6.67 +be lifted to the initial algrebra, to serve as an example of that process.*}
    6.68 +fun
    6.69 +  freeleft :: "freemsg \<Rightarrow> freemsg"
    6.70 +where
    6.71 +  "freeleft (NONCE N) = NONCE N"
    6.72 +| "freeleft (MPAIR X Y) = X"
    6.73 +| "freeleft (CRYPT K X) = freeleft X"
    6.74 +| "freeleft (DECRYPT K X) = freeleft X"
    6.75 +
    6.76 +text{*This theorem lets us prove that the left function respects the
    6.77 +equivalence relation.  It also helps us prove that MPair
    6.78 +  (the abstract constructor) is injective*}
    6.79 +lemma msgrel_imp_eqv_freeleft_aux:
    6.80 +  shows "freeleft U \<sim> freeleft U"
    6.81 +  by (induct rule: freeleft.induct) (auto)
    6.82 +
    6.83 +theorem msgrel_imp_eqv_freeleft:
    6.84 +  assumes a: "U \<sim> V"
    6.85 +  shows "freeleft U \<sim> freeleft V"
    6.86 +  using a
    6.87 +  by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
    6.88 +
    6.89 +subsubsection{*The Right Projection*}
    6.90 +
    6.91 +text{*A function to return the right part of the top pair in a message.*}
    6.92 +fun
    6.93 +  freeright :: "freemsg \<Rightarrow> freemsg"
    6.94 +where
    6.95 +  "freeright (NONCE N) = NONCE N"
    6.96 +| "freeright (MPAIR X Y) = Y"
    6.97 +| "freeright (CRYPT K X) = freeright X"
    6.98 +| "freeright (DECRYPT K X) = freeright X"
    6.99 +
   6.100 +text{*This theorem lets us prove that the right function respects the
   6.101 +equivalence relation.  It also helps us prove that MPair
   6.102 +  (the abstract constructor) is injective*}
   6.103 +lemma msgrel_imp_eqv_freeright_aux:
   6.104 +  shows "freeright U \<sim> freeright U"
   6.105 +  by (induct rule: freeright.induct) (auto)
   6.106 +
   6.107 +theorem msgrel_imp_eqv_freeright:
   6.108 +  assumes a: "U \<sim> V"
   6.109 +  shows "freeright U \<sim> freeright V"
   6.110 +  using a
   6.111 +  by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
   6.112 +
   6.113 +subsubsection{*The Discriminator for Constructors*}
   6.114 +
   6.115 +text{*A function to distinguish nonces, mpairs and encryptions*}
   6.116 +fun
   6.117 +  freediscrim :: "freemsg \<Rightarrow> int"
   6.118 +where
   6.119 +   "freediscrim (NONCE N) = 0"
   6.120 + | "freediscrim (MPAIR X Y) = 1"
   6.121 + | "freediscrim (CRYPT K X) = freediscrim X + 2"
   6.122 + | "freediscrim (DECRYPT K X) = freediscrim X - 2"
   6.123 +
   6.124 +text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
   6.125 +theorem msgrel_imp_eq_freediscrim:
   6.126 +  assumes a: "U \<sim> V"
   6.127 +  shows "freediscrim U = freediscrim V"
   6.128 +  using a by (induct) (auto)
   6.129 +
   6.130 +subsection{*The Initial Algebra: A Quotiented Message Type*}
   6.131 +
   6.132 +quotient_type msg = freemsg / msgrel
   6.133 +  by (rule equiv_msgrel)
   6.134 +
   6.135 +text{*The abstract message constructors*}
   6.136 +
   6.137 +quotient_definition
   6.138 +  "Nonce :: nat \<Rightarrow> msg"
   6.139 +is
   6.140 +  "NONCE"
   6.141 +
   6.142 +quotient_definition
   6.143 +  "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
   6.144 +is
   6.145 +  "MPAIR"
   6.146 +
   6.147 +quotient_definition
   6.148 +  "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
   6.149 +is
   6.150 +  "CRYPT"
   6.151 +
   6.152 +quotient_definition
   6.153 +  "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
   6.154 +is
   6.155 +  "DECRYPT"
   6.156 +
   6.157 +lemma [quot_respect]:
   6.158 +  shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
   6.159 +by (auto intro: CRYPT)
   6.160 +
   6.161 +lemma [quot_respect]:
   6.162 +  shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
   6.163 +by (auto intro: DECRYPT)
   6.164 +
   6.165 +text{*Establishing these two equations is the point of the whole exercise*}
   6.166 +theorem CD_eq [simp]:
   6.167 +  shows "Crypt K (Decrypt K X) = X"
   6.168 +  by (lifting CD)
   6.169 +
   6.170 +theorem DC_eq [simp]:
   6.171 +  shows "Decrypt K (Crypt K X) = X"
   6.172 +  by (lifting DC)
   6.173 +
   6.174 +subsection{*The Abstract Function to Return the Set of Nonces*}
   6.175 +
   6.176 +quotient_definition
   6.177 +   "nonces:: msg \<Rightarrow> nat set"
   6.178 +is
   6.179 +  "freenonces"
   6.180 +
   6.181 +text{*Now prove the four equations for @{term nonces}*}
   6.182 +
   6.183 +lemma [quot_respect]:
   6.184 +  shows "(op \<sim> ===> op =) freenonces freenonces"
   6.185 +  by (simp add: msgrel_imp_eq_freenonces)
   6.186 +
   6.187 +lemma [quot_respect]:
   6.188 +  shows "(op = ===> op \<sim>) NONCE NONCE"
   6.189 +  by (simp add: NONCE)
   6.190 +
   6.191 +lemma nonces_Nonce [simp]:
   6.192 +  shows "nonces (Nonce N) = {N}"
   6.193 +  by (lifting freenonces.simps(1))
   6.194 +
   6.195 +lemma [quot_respect]:
   6.196 +  shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
   6.197 +  by (simp add: MPAIR)
   6.198 +
   6.199 +lemma nonces_MPair [simp]:
   6.200 +  shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
   6.201 +  by (lifting freenonces.simps(2))
   6.202 +
   6.203 +lemma nonces_Crypt [simp]:
   6.204 +  shows "nonces (Crypt K X) = nonces X"
   6.205 +  by (lifting freenonces.simps(3))
   6.206 +
   6.207 +lemma nonces_Decrypt [simp]:
   6.208 +  shows "nonces (Decrypt K X) = nonces X"
   6.209 +  by (lifting freenonces.simps(4))
   6.210 +
   6.211 +subsection{*The Abstract Function to Return the Left Part*}
   6.212 +
   6.213 +quotient_definition
   6.214 +  "left:: msg \<Rightarrow> msg"
   6.215 +is
   6.216 +  "freeleft"
   6.217 +
   6.218 +lemma [quot_respect]:
   6.219 +  shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
   6.220 +  by (simp add: msgrel_imp_eqv_freeleft)
   6.221 +
   6.222 +lemma left_Nonce [simp]:
   6.223 +  shows "left (Nonce N) = Nonce N"
   6.224 +  by (lifting freeleft.simps(1))
   6.225 +
   6.226 +lemma left_MPair [simp]:
   6.227 +  shows "left (MPair X Y) = X"
   6.228 +  by (lifting freeleft.simps(2))
   6.229 +
   6.230 +lemma left_Crypt [simp]:
   6.231 +  shows "left (Crypt K X) = left X"
   6.232 +  by (lifting freeleft.simps(3))
   6.233 +
   6.234 +lemma left_Decrypt [simp]:
   6.235 +  shows "left (Decrypt K X) = left X"
   6.236 +  by (lifting freeleft.simps(4))
   6.237 +
   6.238 +subsection{*The Abstract Function to Return the Right Part*}
   6.239 +
   6.240 +quotient_definition
   6.241 +  "right:: msg \<Rightarrow> msg"
   6.242 +is
   6.243 +  "freeright"
   6.244 +
   6.245 +text{*Now prove the four equations for @{term right}*}
   6.246 +
   6.247 +lemma [quot_respect]:
   6.248 +  shows "(op \<sim> ===> op \<sim>) freeright freeright"
   6.249 +  by (simp add: msgrel_imp_eqv_freeright)
   6.250 +
   6.251 +lemma right_Nonce [simp]:
   6.252 +  shows "right (Nonce N) = Nonce N"
   6.253 +  by (lifting freeright.simps(1))
   6.254 +
   6.255 +lemma right_MPair [simp]:
   6.256 +  shows "right (MPair X Y) = Y"
   6.257 +  by (lifting freeright.simps(2))
   6.258 +
   6.259 +lemma right_Crypt [simp]:
   6.260 +  shows "right (Crypt K X) = right X"
   6.261 +  by (lifting freeright.simps(3))
   6.262 +
   6.263 +lemma right_Decrypt [simp]:
   6.264 +  shows "right (Decrypt K X) = right X"
   6.265 +  by (lifting freeright.simps(4))
   6.266 +
   6.267 +subsection{*Injectivity Properties of Some Constructors*}
   6.268 +
   6.269 +lemma NONCE_imp_eq:
   6.270 +  shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
   6.271 +  by (drule msgrel_imp_eq_freenonces, simp)
   6.272 +
   6.273 +text{*Can also be proved using the function @{term nonces}*}
   6.274 +lemma Nonce_Nonce_eq [iff]:
   6.275 +  shows "(Nonce m = Nonce n) = (m = n)"
   6.276 +proof
   6.277 +  assume "Nonce m = Nonce n"
   6.278 +  then show "m = n" by (lifting NONCE_imp_eq)
   6.279 +next
   6.280 +  assume "m = n"
   6.281 +  then show "Nonce m = Nonce n" by simp
   6.282 +qed
   6.283 +
   6.284 +lemma MPAIR_imp_eqv_left:
   6.285 +  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
   6.286 +  by (drule msgrel_imp_eqv_freeleft) (simp)
   6.287 +
   6.288 +lemma MPair_imp_eq_left:
   6.289 +  assumes eq: "MPair X Y = MPair X' Y'"
   6.290 +  shows "X = X'"
   6.291 +  using eq by (lifting MPAIR_imp_eqv_left)
   6.292 +
   6.293 +lemma MPAIR_imp_eqv_right:
   6.294 +  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
   6.295 +  by (drule msgrel_imp_eqv_freeright) (simp)
   6.296 +
   6.297 +lemma MPair_imp_eq_right:
   6.298 +  shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
   6.299 +  by (lifting  MPAIR_imp_eqv_right)
   6.300 +
   6.301 +theorem MPair_MPair_eq [iff]:
   6.302 +  shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
   6.303 +  by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
   6.304 +
   6.305 +lemma NONCE_neqv_MPAIR:
   6.306 +  shows "\<not>(NONCE m \<sim> MPAIR X Y)"
   6.307 +  by (auto dest: msgrel_imp_eq_freediscrim)
   6.308 +
   6.309 +theorem Nonce_neq_MPair [iff]:
   6.310 +  shows "Nonce N \<noteq> MPair X Y"
   6.311 +  by (lifting NONCE_neqv_MPAIR)
   6.312 +
   6.313 +text{*Example suggested by a referee*}
   6.314 +
   6.315 +lemma CRYPT_NONCE_neq_NONCE:
   6.316 +  shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
   6.317 +  by (auto dest: msgrel_imp_eq_freediscrim)
   6.318 +
   6.319 +theorem Crypt_Nonce_neq_Nonce:
   6.320 +  shows "Crypt K (Nonce M) \<noteq> Nonce N"
   6.321 +  by (lifting CRYPT_NONCE_neq_NONCE)
   6.322 +
   6.323 +text{*...and many similar results*}
   6.324 +lemma CRYPT2_NONCE_neq_NONCE:
   6.325 +  shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
   6.326 +  by (auto dest: msgrel_imp_eq_freediscrim)
   6.327 +
   6.328 +theorem Crypt2_Nonce_neq_Nonce:
   6.329 +  shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
   6.330 +  by (lifting CRYPT2_NONCE_neq_NONCE)
   6.331 +
   6.332 +theorem Crypt_Crypt_eq [iff]:
   6.333 +  shows "(Crypt K X = Crypt K X') = (X=X')"
   6.334 +proof
   6.335 +  assume "Crypt K X = Crypt K X'"
   6.336 +  hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
   6.337 +  thus "X = X'" by simp
   6.338 +next
   6.339 +  assume "X = X'"
   6.340 +  thus "Crypt K X = Crypt K X'" by simp
   6.341 +qed
   6.342 +
   6.343 +theorem Decrypt_Decrypt_eq [iff]:
   6.344 +  shows "(Decrypt K X = Decrypt K X') = (X=X')"
   6.345 +proof
   6.346 +  assume "Decrypt K X = Decrypt K X'"
   6.347 +  hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
   6.348 +  thus "X = X'" by simp
   6.349 +next
   6.350 +  assume "X = X'"
   6.351 +  thus "Decrypt K X = Decrypt K X'" by simp
   6.352 +qed
   6.353 +
   6.354 +lemma msg_induct_aux:
   6.355 +  shows "\<lbrakk>\<And>N. P (Nonce N);
   6.356 +          \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
   6.357 +          \<And>K X. P X \<Longrightarrow> P (Crypt K X);
   6.358 +          \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
   6.359 +  by (lifting freemsg.induct)
   6.360 +
   6.361 +lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
   6.362 +  assumes N: "\<And>N. P (Nonce N)"
   6.363 +      and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
   6.364 +      and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
   6.365 +      and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
   6.366 +  shows "P msg"
   6.367 +  using N M C D by (rule msg_induct_aux)
   6.368 +
   6.369 +subsection{*The Abstract Discriminator*}
   6.370 +
   6.371 +text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
   6.372 +need this function in order to prove discrimination theorems.*}
   6.373 +
   6.374 +quotient_definition
   6.375 +  "discrim:: msg \<Rightarrow> int"
   6.376 +is
   6.377 +  "freediscrim"
   6.378 +
   6.379 +text{*Now prove the four equations for @{term discrim}*}
   6.380 +
   6.381 +lemma [quot_respect]:
   6.382 +  shows "(op \<sim> ===> op =) freediscrim freediscrim"
   6.383 +  by (auto simp add: msgrel_imp_eq_freediscrim)
   6.384 +
   6.385 +lemma discrim_Nonce [simp]:
   6.386 +  shows "discrim (Nonce N) = 0"
   6.387 +  by (lifting freediscrim.simps(1))
   6.388 +
   6.389 +lemma discrim_MPair [simp]:
   6.390 +  shows "discrim (MPair X Y) = 1"
   6.391 +  by (lifting freediscrim.simps(2))
   6.392 +
   6.393 +lemma discrim_Crypt [simp]:
   6.394 +  shows "discrim (Crypt K X) = discrim X + 2"
   6.395 +  by (lifting freediscrim.simps(3))
   6.396 +
   6.397 +lemma discrim_Decrypt [simp]:
   6.398 +  shows "discrim (Decrypt K X) = discrim X - 2"
   6.399 +  by (lifting freediscrim.simps(4))
   6.400 +
   6.401 +end
   6.402 +
     7.1 --- a/src/HOL/Quotient_Examples/ROOT.ML	Wed Apr 28 17:42:37 2010 +0200
     7.2 +++ b/src/HOL/Quotient_Examples/ROOT.ML	Thu Apr 29 09:06:35 2010 +0200
     7.3 @@ -4,5 +4,5 @@
     7.4  Testing the quotient package.
     7.5  *)
     7.6  
     7.7 -use_thys ["FSet", "LarryInt", "LarryDatatype"];
     7.8 +use_thys ["FSet", "Quotient_Int", "Quotient_Message"];
     7.9