
diff -r 29ee987174c0 -r 7add2d5322a7 src/HOL/Induct/QuoDataType.thy
--- a/src/HOL/Induct/QuoDataType.thy	Tue Mar 15 14:15:11 2022 +0100
+++ b/src/HOL/Induct/QuoDataType.thy	Wed Mar 16 16:14:22 2022 +0000
@@ -5,6 +5,11 @@
 
 section\<open>Defining an Initial Algebra by Quotienting a Free Algebra\<close>
 
+text \<open>For Lawrence Paulson's paper ``Defining functions on equivalence classes''
+\emph{ACM Transactions on Computational Logic} \textbf{7}:40 (2006), 658--675,
+illustrating bare-bones quotient constructions. Any comparison using lifting and transfer
+should be done in a separate theory.\<close>
+
 theory QuoDataType imports Main begin
 
 subsection\<open>Defining the Free Algebra\<close>
@@ -163,9 +168,7 @@
 by (auto simp add: Msg_def quotient_def intro: msgrel_refl)
 
 lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"
-apply (rule inj_on_inverseI)
-apply (erule Abs_Msg_inverse)
-done
+  by (meson Abs_Msg_inject inj_onI)
 
 text\<open>Reduces equality on abstractions to equality on representatives\<close>
 declare inj_on_Abs_Msg [THEN inj_on_eq_iff, simp]
@@ -203,11 +206,8 @@
 
 text\<open>Case analysis on the representation of a msg as an equivalence class.\<close>
 lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]:
-     "(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P"
-apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE])
-apply (drule arg_cong [where f=Abs_Msg])
-apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl)
-done
+     "(\<And>U. z = Abs_Msg (msgrel `` {U}) \<Longrightarrow> P) \<Longrightarrow> P"
+  by (metis Abs_Msg_cases Msg_def quotientE)
 
 text\<open>Establishing these two equations is the point of the whole exercise\<close>
 theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
@@ -234,32 +234,40 @@
               UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
  
 lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X \<union> nonces Y"
-apply (cases X, cases Y) 
-apply (simp add: nonces_def MPair 
-                 UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
-done
+proof -
+  have "\<And>U V. \<lbrakk>X = Abs_Msg (msgrel `` {U}); Y = Abs_Msg (msgrel `` {V})\<rbrakk>
+             \<Longrightarrow> nonces (MPair X Y) = nonces X \<union> nonces Y"
+    by (simp add: nonces_def MPair 
+        UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
+  then show ?thesis
+    by (meson eq_Abs_Msg)
+qed
 
 lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X"
-apply (cases X) 
-apply (simp add: nonces_def Crypt
-                 UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
-done
+proof -
+  have "\<And>U. X = Abs_Msg (msgrel `` {U}) \<Longrightarrow> nonces (Crypt K X) = nonces X"
+    by (simp add: nonces_def Crypt UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
+  then show ?thesis
+    by (meson eq_Abs_Msg)
+qed
 
 lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
-apply (cases X) 
-apply (simp add: nonces_def Decrypt
-                 UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
-done
+proof -
+  have "\<And>U. X = Abs_Msg (msgrel `` {U}) \<Longrightarrow> nonces (Decrypt K X) = nonces X"
+    by (simp add: nonces_def Decrypt UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
+  then show ?thesis
+    by (meson eq_Abs_Msg)
+qed
 
 
 subsection\<open>The Abstract Function to Return the Left Part\<close>
 
 definition
-  left :: "msg \<Rightarrow> msg" where
-   "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
+  left :: "msg \<Rightarrow> msg" 
+    where "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
 
 lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
-by (auto simp add: congruent_def msgrel_imp_eqv_freeleft) 
+  by (auto simp add: congruent_def msgrel_imp_eqv_freeleft) 
 
 text\<open>Now prove the four equations for \<^term>\<open>left\<close>\<close>
 
@@ -268,69 +276,51 @@
               UN_equiv_class [OF equiv_msgrel left_congruent]) 
 
 lemma left_MPair [simp]: "left (MPair X Y) = X"
-apply (cases X, cases Y) 
-apply (simp add: left_def MPair 
-                 UN_equiv_class [OF equiv_msgrel left_congruent]) 
-done
+  by (cases X, cases Y) (simp add: left_def MPair UN_equiv_class [OF equiv_msgrel left_congruent]) 
 
 lemma left_Crypt [simp]: "left (Crypt K X) = left X"
-apply (cases X) 
-apply (simp add: left_def Crypt
-                 UN_equiv_class [OF equiv_msgrel left_congruent]) 
-done
+  by (cases X) (simp add: left_def Crypt UN_equiv_class [OF equiv_msgrel left_congruent]) 
 
 lemma left_Decrypt [simp]: "left (Decrypt K X) = left X"
-apply (cases X) 
-apply (simp add: left_def Decrypt
-                 UN_equiv_class [OF equiv_msgrel left_congruent]) 
-done
+  by (metis CD_eq left_Crypt)
 
 
 subsection\<open>The Abstract Function to Return the Right Part\<close>
 
 definition
-  right :: "msg \<Rightarrow> msg" where
-   "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
+  right :: "msg \<Rightarrow> msg" 
+    where "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
 
 lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
-by (auto simp add: congruent_def msgrel_imp_eqv_freeright) 
+  by (auto simp add: congruent_def msgrel_imp_eqv_freeright) 
 
 text\<open>Now prove the four equations for \<^term>\<open>right\<close>\<close>
 
 lemma right_Nonce [simp]: "right (Nonce N) = Nonce N"
-by (simp add: right_def Nonce_def 
-              UN_equiv_class [OF equiv_msgrel right_congruent]) 
+  by (simp add: right_def Nonce_def 
+      UN_equiv_class [OF equiv_msgrel right_congruent]) 
 
 lemma right_MPair [simp]: "right (MPair X Y) = Y"
-apply (cases X, cases Y) 
-apply (simp add: right_def MPair 
-                 UN_equiv_class [OF equiv_msgrel right_congruent]) 
-done
+  by (cases X, cases Y) (simp add: right_def MPair UN_equiv_class [OF equiv_msgrel right_congruent]) 
 
 lemma right_Crypt [simp]: "right (Crypt K X) = right X"
-apply (cases X) 
-apply (simp add: right_def Crypt
-                 UN_equiv_class [OF equiv_msgrel right_congruent]) 
-done
+  by (cases X) (simp add: right_def Crypt UN_equiv_class [OF equiv_msgrel right_congruent]) 
 
 lemma right_Decrypt [simp]: "right (Decrypt K X) = right X"
-apply (cases X) 
-apply (simp add: right_def Decrypt
-                 UN_equiv_class [OF equiv_msgrel right_congruent]) 
-done
+  by (metis CD_eq right_Crypt)
 
 
 subsection\<open>Injectivity Properties of Some Constructors\<close>
 
 lemma NONCE_imp_eq: "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
-by (drule msgrel_imp_eq_freenonces, simp)
+  by (drule msgrel_imp_eq_freenonces, simp)
 
 text\<open>Can also be proved using the function \<^term>\<open>nonces\<close>\<close>
 lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)"
-by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)
+  by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)
 
 lemma MPAIR_imp_eqv_left: "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'"
@@ -341,33 +331,27 @@
 qed
 
 lemma MPAIR_imp_eqv_right: "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: "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'" 
-apply (cases X, cases X', cases Y, cases Y') 
-apply (simp add: MPair)
-apply (erule MPAIR_imp_eqv_right)  
-done
+lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
+  by (metis right_MPair) 
 
 theorem MPair_MPair_eq [iff]: "(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: "NONCE m \<sim> MPAIR X Y \<Longrightarrow> False"
-by (drule msgrel_imp_eq_freediscrim, simp)
+  by (drule msgrel_imp_eq_freediscrim, simp)
 
 theorem Nonce_neq_MPair [iff]: "Nonce N \<noteq> MPair X Y"
-apply (cases X, cases Y) 
-apply (simp add: Nonce_def MPair) 
-apply (blast dest: NONCE_neqv_MPAIR) 
-done
+  by (cases X, cases Y) (use MPair NONCE_neqv_MPAIR Nonce_def in fastforce)
 
 text\<open>Example suggested by a referee\<close>
 theorem Crypt_Nonce_neq_Nonce: "Crypt K (Nonce M) \<noteq> Nonce N" 
-by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)  
+  by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)  
 
 text\<open>...and many similar results\<close>
 theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N" 
-by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)  
+  by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)  
 
 theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')" 
 proof
@@ -428,32 +412,27 @@
    "discrim X = the_elem (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
 
 lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
-by (auto simp add: congruent_def msgrel_imp_eq_freediscrim) 
+  by (auto simp add: congruent_def msgrel_imp_eq_freediscrim) 
 
 text\<open>Now prove the four equations for \<^term>\<open>discrim\<close>\<close>
 
 lemma discrim_Nonce [simp]: "discrim (Nonce N) = 0"
-by (simp add: discrim_def Nonce_def 
-              UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
+  by (simp add: discrim_def Nonce_def 
+      UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
 
 lemma discrim_MPair [simp]: "discrim (MPair X Y) = 1"
-apply (cases X, cases Y) 
-apply (simp add: discrim_def MPair 
-                 UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
-done
+proof -
+  have "\<And>U V. discrim (MPair (Abs_Msg (msgrel `` {U})) (Abs_Msg (msgrel `` {V}))) = 1"
+    by (simp add: discrim_def MPair  UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
+  then show ?thesis
+    by (metis eq_Abs_Msg)
+qed
 
 lemma discrim_Crypt [simp]: "discrim (Crypt K X) = discrim X + 2"
-apply (cases X) 
-apply (simp add: discrim_def Crypt
-                 UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
-done
+  by (cases X) (use Crypt UN_equiv_class discrim_congruent discrim_def equiv_msgrel in fastforce)
 
 lemma discrim_Decrypt [simp]: "discrim (Decrypt K X) = discrim X - 2"
-apply (cases X) 
-apply (simp add: discrim_def Decrypt
-                 UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
-done
-
+  by (cases X) (use Decrypt UN_equiv_class discrim_congruent discrim_def equiv_msgrel in fastforce)
 
 end
 




