nominal2: comparison Quot/Examples/LarryDatatype.thy

equal deleted inserted replaced

-:6f6ee78c7357
+:ba7e81531c6d
 | "freenonces (DECRYPT K X) = freenonces X"
 theorem msgrel_imp_eq_freenonces:
 assumes a: "U \<sim> V"
 shows "freenonces U = freenonces V"
 using a by (induct) (auto)
 subsubsection{*The Left Projection*}
 text{*A function to return the left part of the top pair in a message.  It will
 be lifted to the initial algrebra, to serve as an example of that process.*}
 text{*This theorem lets us prove that the left function respects the
 equivalence relation.  It also helps us prove that MPair
 (the abstract constructor) is injective*}
 lemma msgrel_imp_eqv_freeleft_aux:
 shows "freeleft U \<sim> freeleft U"
 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)
+by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
 subsubsection{*The Right Projection*}
 text{*A function to return the right part of the top pair in a message.*}
 fun
 text{*This theorem lets us prove that the right function respects the
 equivalence relation.  It also helps us prove that MPair
 (the abstract constructor) is injective*}
 lemma msgrel_imp_eqv_freeright_aux:
 shows "freeright U \<sim> freeright U"
 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)
 subsubsection{*The Discriminator for Constructors*}
 text{*A function to distinguish nonces, mpairs and encryptions*}
 fun
 text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
 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*}
 quotient_type msg = freemsg / msgrel
 by (rule equiv_msgrel)
 lemma [quot_respect]:
 shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
 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"
+theorem CD_eq [simp]:
-by (lifting CD)
+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*}
 quotient_definition
 "nonces:: msg \<Rightarrow> nat set"
 text{*Now prove the four equations for @{term nonces}*}
 lemma [quot_respect]:
 shows "(op \<sim> ===> op =) freenonces freenonces"
 by (simp add: msgrel_imp_eq_freenonces)
 lemma [quot_respect]:
 shows "(op = ===> op \<sim>) NONCE NONCE"
 by (simp add: NONCE)
 lemma nonces_Nonce [simp]:
 shows "nonces (Nonce N) = {N}"
 by (lifting freenonces.simps(1))
 lemma [quot_respect]:
 shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
 by (simp add: MPAIR)
 lemma nonces_MPair [simp]:
 shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
 by (lifting freenonces.simps(2))
 lemma nonces_Crypt [simp]:
 shows "nonces (Crypt K X) = nonces X"
 by (lifting freenonces.simps(3))
-lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
+lemma nonces_Decrypt [simp]:
-by (lifting freenonces.simps(4))
+shows "nonces (Decrypt K X) = nonces X"
+by (lifting freenonces.simps(4))
 subsection{*The Abstract Function to Return the Left Part*}
 quotient_definition
 "left:: msg \<Rightarrow> msg"
 as
 "freeleft"
 lemma [quot_respect]:
 shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
 by (simp add: msgrel_imp_eqv_freeleft)
 lemma left_Nonce [simp]:
 shows "left (Nonce N) = Nonce N"
 by (lifting freeleft.simps(1))
 lemma left_MPair [simp]:
 shows "left (MPair X Y) = X"
 by (lifting freeleft.simps(2))
 lemma left_Crypt [simp]:
 shows "left (Crypt K X) = left X"
 by (lifting freeleft.simps(3))
 lemma left_Decrypt [simp]:
 shows "left (Decrypt K X) = left X"
 by (lifting freeleft.simps(4))
 subsection{*The Abstract Function to Return the Right Part*}
 quotient_definition
 "right:: msg \<Rightarrow> msg"
 text{*Now prove the four equations for @{term right}*}
 lemma [quot_respect]:
 shows "(op \<sim> ===> op \<sim>) freeright freeright"
 by (simp add: msgrel_imp_eqv_freeright)
 lemma right_Nonce [simp]:
 shows "right (Nonce N) = Nonce N"
 by (lifting freeright.simps(1))
 lemma right_MPair [simp]:
 shows "right (MPair X Y) = Y"
 by (lifting freeright.simps(2))
 lemma right_Crypt [simp]:
 shows "right (Crypt K X) = right X"
 by (lifting freeright.simps(3))
 lemma right_Decrypt [simp]:
 shows "right (Decrypt K X) = right X"
 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)
 text{*Can also be proved using the function @{term nonces}*}
 lemma Nonce_Nonce_eq [iff]:
 shows "(Nonce m = Nonce n) = (m = n)"
 proof
 then show "Nonce m = Nonce n" by simp
 qed
 lemma MPAIR_imp_eqv_left:
 shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
 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)
 lemma MPAIR_imp_eqv_right:
 shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
 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)
 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)
 lemma NONCE_neqv_MPAIR:
 shows "\<not>(NONCE m \<sim> MPAIR X Y)"
 by (auto dest: msgrel_imp_eq_freediscrim)
 theorem Nonce_neq_MPair [iff]:
 shows "Nonce N \<noteq> MPair X Y"
 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)
 theorem Crypt_Nonce_neq_Nonce:
 shows "Crypt K (Nonce M) \<noteq> Nonce N"
 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)
 theorem Crypt2_Nonce_neq_Nonce:
 shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
 by (lifting CRYPT2_NONCE_neq_NONCE)
 theorem Crypt_Crypt_eq [iff]:
 shows "(Crypt K X = Crypt K X') = (X=X')"
 proof
 assume "Crypt K X = Crypt K X'"
 lemma msg_induct_aux:
 shows "\<lbrakk>\<And>N. P (Nonce N);
 \<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)
 lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
 assumes N: "\<And>N. P (Nonce N)"
 and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
 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)
 subsection{*The Abstract Discriminator*}
 text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
 need this function in order to prove discrimination theorems.*}
 text{*Now prove the four equations for @{term discrim}*}
 lemma [quot_respect]:
 shows "(op \<sim> ===> op =) freediscrim freediscrim"
 by (auto simp add: msgrel_imp_eq_freediscrim)
 lemma discrim_Nonce [simp]:
 shows "discrim (Nonce N) = 0"
 by (lifting freediscrim.simps(1))
 lemma discrim_MPair [simp]:
 shows "discrim (MPair X Y) = 1"
 by (lifting freediscrim.simps(2))
 lemma discrim_Crypt [simp]:
 shows "discrim (Crypt K X) = discrim X + 2"
 by (lifting freediscrim.simps(3))
 lemma discrim_Decrypt [simp]:
 shows "discrim (Decrypt K X) = discrim X - 2"
 by (lifting freediscrim.simps(4))
 end

changeset 804	ba7e81531c6d
parent 767	37285ec4387d
child 1128	17ca92ab4660