diff -r 6f6ee78c7357 -r ba7e81531c6d Quot/Examples/LarryDatatype.thy
--- a/Quot/Examples/LarryDatatype.thy	Fri Jan 01 11:30:00 2010 +0100
+++ b/Quot/Examples/LarryDatatype.thy	Fri Jan 01 23:59:32 2010 +0100
@@ -51,7 +51,7 @@
 theorem msgrel_imp_eq_freenonces: 
   assumes a: "U \<sim> V"
   shows "freenonces U = freenonces V"
-using a by (induct) (auto) 
+  using a by (induct) (auto) 
 
 subsubsection{*The Left Projection*}
 
@@ -70,13 +70,13 @@
   (the abstract constructor) is injective*}
 lemma msgrel_imp_eqv_freeleft_aux:
   shows "freeleft U \<sim> freeleft U"
-by (induct rule: freeleft.induct) (auto)
+  by (induct rule: freeleft.induct) (auto)
 
 theorem msgrel_imp_eqv_freeleft:
   assumes a: "U \<sim> V" 
   shows "freeleft U \<sim> freeleft V"
-using a
-by (induct)(auto intro: msgrel_imp_eqv_freeleft_aux)
+  using a
+  by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
 
 subsubsection{*The Right Projection*}
 
@@ -94,13 +94,13 @@
   (the abstract constructor) is injective*}
 lemma msgrel_imp_eqv_freeright_aux:
   shows "freeright U \<sim> freeright U"
-by (induct rule: freeright.induct) (auto)
+  by (induct rule: freeright.induct) (auto)
 
 theorem msgrel_imp_eqv_freeright:
   assumes a: "U \<sim> V" 
   shows "freeright U \<sim> freeright V"
-using a
-by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
+  using a
+  by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
 
 subsubsection{*The Discriminator for Constructors*}
 
@@ -117,7 +117,7 @@
 theorem msgrel_imp_eq_freediscrim:
   assumes a: "U \<sim> V"
   shows "freediscrim U = freediscrim V"
-using a by (induct, auto)
+  using a by (induct) (auto)
 
 subsection{*The Initial Algebra: A Quotiented Message Type*}
 
@@ -155,11 +155,13 @@
 by (auto intro: DECRYPT)
 
 text{*Establishing these two equations is the point of the whole exercise*}
-theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
-by (lifting CD)
+theorem CD_eq [simp]: 
+  shows "Crypt K (Decrypt K X) = X"
+  by (lifting CD)
 
-theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
-by (lifting DC)
+theorem DC_eq [simp]: 
+  shows "Decrypt K (Crypt K X) = X"
+  by (lifting DC)
 
 subsection{*The Abstract Function to Return the Set of Nonces*}
 
@@ -172,30 +174,31 @@
 
 lemma [quot_respect]:
   shows "(op \<sim> ===> op =) freenonces freenonces"
-by (simp add: msgrel_imp_eq_freenonces)
+  by (simp add: msgrel_imp_eq_freenonces)
 
 lemma [quot_respect]:
   shows "(op = ===> op \<sim>) NONCE NONCE"
-by (simp add: NONCE)
+  by (simp add: NONCE)
 
 lemma nonces_Nonce [simp]: 
   shows "nonces (Nonce N) = {N}"
-by (lifting freenonces.simps(1))
+  by (lifting freenonces.simps(1))
  
 lemma [quot_respect]:
   shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
-by (simp add: MPAIR)
+  by (simp add: MPAIR)
 
 lemma nonces_MPair [simp]: 
   shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
-by (lifting freenonces.simps(2))
+  by (lifting freenonces.simps(2))
 
 lemma nonces_Crypt [simp]: 
   shows "nonces (Crypt K X) = nonces X"
-by (lifting freenonces.simps(3))
+  by (lifting freenonces.simps(3))
 
-lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
-by (lifting freenonces.simps(4))
+lemma nonces_Decrypt [simp]: 
+  shows "nonces (Decrypt K X) = nonces X"
+  by (lifting freenonces.simps(4))
 
 subsection{*The Abstract Function to Return the Left Part*}
 
@@ -206,23 +209,23 @@
 
 lemma [quot_respect]:
   shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
-by (simp add: msgrel_imp_eqv_freeleft)
+  by (simp add: msgrel_imp_eqv_freeleft)
 
 lemma left_Nonce [simp]: 
   shows "left (Nonce N) = Nonce N"
-by (lifting freeleft.simps(1))
+  by (lifting freeleft.simps(1))
 
 lemma left_MPair [simp]: 
   shows "left (MPair X Y) = X"
-by (lifting freeleft.simps(2))
+  by (lifting freeleft.simps(2))
 
 lemma left_Crypt [simp]: 
   shows "left (Crypt K X) = left X"
-by (lifting freeleft.simps(3))
+  by (lifting freeleft.simps(3))
 
 lemma left_Decrypt [simp]: 
   shows "left (Decrypt K X) = left X"
-by (lifting freeleft.simps(4))
+  by (lifting freeleft.simps(4))
 
 subsection{*The Abstract Function to Return the Right Part*}
 
@@ -235,29 +238,29 @@
 
 lemma [quot_respect]:
   shows "(op \<sim> ===> op \<sim>) freeright freeright"
-by (simp add: msgrel_imp_eqv_freeright)
+  by (simp add: msgrel_imp_eqv_freeright)
 
 lemma right_Nonce [simp]: 
   shows "right (Nonce N) = Nonce N"
-by (lifting freeright.simps(1))
+  by (lifting freeright.simps(1))
 
 lemma right_MPair [simp]: 
   shows "right (MPair X Y) = Y"
-by (lifting freeright.simps(2))
+  by (lifting freeright.simps(2))
 
 lemma right_Crypt [simp]: 
   shows "right (Crypt K X) = right X"
-by (lifting freeright.simps(3))
+  by (lifting freeright.simps(3))
 
 lemma right_Decrypt [simp]: 
   shows "right (Decrypt K X) = right X"
-by (lifting freeright.simps(4))
+  by (lifting freeright.simps(4))
 
 subsection{*Injectivity Properties of Some Constructors*}
 
 lemma NONCE_imp_eq: 
   shows "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
-by (drule msgrel_imp_eq_freenonces, simp)
+  by (drule msgrel_imp_eq_freenonces, simp)
 
 text{*Can also be proved using the function @{term nonces}*}
 lemma Nonce_Nonce_eq [iff]: 
@@ -272,51 +275,51 @@
 
 lemma MPAIR_imp_eqv_left: 
   shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
-by (drule msgrel_imp_eqv_freeleft) (simp)
+  by (drule msgrel_imp_eqv_freeleft) (simp)
 
 lemma MPair_imp_eq_left: 
   assumes eq: "MPair X Y = MPair X' Y'" 
   shows "X = X'"
-using eq by (lifting MPAIR_imp_eqv_left)
+  using eq by (lifting MPAIR_imp_eqv_left)
 
 lemma MPAIR_imp_eqv_right: 
   shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
-by (drule msgrel_imp_eqv_freeright) (simp)
+  by (drule msgrel_imp_eqv_freeright) (simp)
 
 lemma MPair_imp_eq_right: 
   shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
-by (lifting  MPAIR_imp_eqv_right)
+  by (lifting  MPAIR_imp_eqv_right)
 
 theorem MPair_MPair_eq [iff]: 
   shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" 
-by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
+  by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
 
 lemma NONCE_neqv_MPAIR: 
   shows "\<not>(NONCE m \<sim> MPAIR X Y)"
-by (auto dest: msgrel_imp_eq_freediscrim)
+  by (auto dest: msgrel_imp_eq_freediscrim)
 
 theorem Nonce_neq_MPair [iff]: 
   shows "Nonce N \<noteq> MPair X Y"
-by (lifting NONCE_neqv_MPAIR)
+  by (lifting NONCE_neqv_MPAIR)
 
 text{*Example suggested by a referee*}
 
 lemma CRYPT_NONCE_neq_NONCE:
   shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
-by (auto dest: msgrel_imp_eq_freediscrim)
+  by (auto dest: msgrel_imp_eq_freediscrim)
 
 theorem Crypt_Nonce_neq_Nonce: 
   shows "Crypt K (Nonce M) \<noteq> Nonce N"
-by (lifting CRYPT_NONCE_neq_NONCE)
+  by (lifting CRYPT_NONCE_neq_NONCE)
 
 text{*...and many similar results*}
 lemma CRYPT2_NONCE_neq_NONCE: 
   shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
-by (auto dest: msgrel_imp_eq_freediscrim)  
+  by (auto dest: msgrel_imp_eq_freediscrim)  
 
 theorem Crypt2_Nonce_neq_Nonce: 
   shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
-by (lifting CRYPT2_NONCE_neq_NONCE) 
+  by (lifting CRYPT2_NONCE_neq_NONCE) 
 
 theorem Crypt_Crypt_eq [iff]: 
   shows "(Crypt K X = Crypt K X') = (X=X')" 
@@ -345,7 +348,7 @@
           \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
           \<And>K X. P X \<Longrightarrow> P (Crypt K X);
           \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
-by (lifting freemsg.induct)
+  by (lifting freemsg.induct)
 
 lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
   assumes N: "\<And>N. P (Nonce N)"
@@ -353,7 +356,7 @@
       and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
       and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
   shows "P msg"
-using N M C D by (rule msg_induct_aux)
+  using N M C D by (rule msg_induct_aux)
 
 subsection{*The Abstract Discriminator*}
 
@@ -369,23 +372,23 @@
 
 lemma [quot_respect]:
   shows "(op \<sim> ===> op =) freediscrim freediscrim"
-by (auto simp add: msgrel_imp_eq_freediscrim)
+  by (auto simp add: msgrel_imp_eq_freediscrim)
 
 lemma discrim_Nonce [simp]: 
   shows "discrim (Nonce N) = 0"
-by (lifting freediscrim.simps(1))
+  by (lifting freediscrim.simps(1))
 
 lemma discrim_MPair [simp]: 
   shows "discrim (MPair X Y) = 1"
-by (lifting freediscrim.simps(2))
+  by (lifting freediscrim.simps(2))
 
 lemma discrim_Crypt [simp]: 
   shows "discrim (Crypt K X) = discrim X + 2"
-by (lifting freediscrim.simps(3))
+  by (lifting freediscrim.simps(3))
 
 lemma discrim_Decrypt [simp]: 
   shows "discrim (Decrypt K X) = discrim X - 2"
-by (lifting freediscrim.simps(4))
+  by (lifting freediscrim.simps(4))
 
 end