--- a/src/HOL/IsaMakefile Wed Apr 28 17:42:37 2010 +0200
+++ b/src/HOL/IsaMakefile Thu Apr 29 09:06:35 2010 +0200
@@ -1295,8 +1295,8 @@
HOL-Quotient_Examples: HOL $(LOG)/HOL-Quotient_Examples.gz
$(LOG)/HOL-Quotient_Examples.gz: $(OUT)/HOL \
- Quotient_Examples/FSet.thy \
- Quotient_Examples/LarryInt.thy Quotient_Examples/LarryDatatype.thy
+ Quotient_Examples/FSet.thy Quotient_Examples/Quotient_Int.thy \
+ Quotient_Examples/Quotient_Message.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Quotient_Examples
--- a/src/HOL/Quotient_Examples/FSet.thy Wed Apr 28 17:42:37 2010 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy Thu Apr 29 09:06:35 2010 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/Quotient_Examples/Quotient.thy
+(* Title: HOL/Quotient_Examples/FSet.thy
Author: Cezary Kaliszyk, TU Munich
Author: Christian Urban, TU Munich
--- a/src/HOL/Quotient_Examples/LarryDatatype.thy Wed Apr 28 17:42:37 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,394 +0,0 @@
-theory LarryDatatype
-imports Main Quotient_Syntax
-begin
-
-subsection{*Defining the Free Algebra*}
-
-datatype
- freemsg = NONCE nat
- | MPAIR freemsg freemsg
- | CRYPT nat freemsg
- | DECRYPT nat freemsg
-
-inductive
- msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
-where
- CD: "CRYPT K (DECRYPT K X) \<sim> X"
-| DC: "DECRYPT K (CRYPT K X) \<sim> X"
-| NONCE: "NONCE N \<sim> NONCE N"
-| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
-| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
-| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
-| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
-| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
-
-lemmas msgrel.intros[intro]
-
-text{*Proving that it is an equivalence relation*}
-
-lemma msgrel_refl: "X \<sim> X"
-by (induct X, (blast intro: msgrel.intros)+)
-
-theorem equiv_msgrel: "equivp msgrel"
-proof (rule equivpI)
- show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
- show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
- show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
-qed
-
-subsection{*Some Functions on the Free Algebra*}
-
-subsubsection{*The Set of Nonces*}
-
-fun
- freenonces :: "freemsg \<Rightarrow> nat set"
-where
- "freenonces (NONCE N) = {N}"
-| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
-| "freenonces (CRYPT K X) = freenonces X"
-| "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.*}
-fun
- freeleft :: "freemsg \<Rightarrow> freemsg"
-where
- "freeleft (NONCE N) = NONCE N"
-| "freeleft (MPAIR X Y) = X"
-| "freeleft (CRYPT K X) = freeleft X"
-| "freeleft (DECRYPT K X) = freeleft X"
-
-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)
-
-subsubsection{*The Right Projection*}
-
-text{*A function to return the right part of the top pair in a message.*}
-fun
- freeright :: "freemsg \<Rightarrow> freemsg"
-where
- "freeright (NONCE N) = NONCE N"
-| "freeright (MPAIR X Y) = Y"
-| "freeright (CRYPT K X) = freeright X"
-| "freeright (DECRYPT K X) = freeright X"
-
-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
- freediscrim :: "freemsg \<Rightarrow> int"
-where
- "freediscrim (NONCE N) = 0"
- | "freediscrim (MPAIR X Y) = 1"
- | "freediscrim (CRYPT K X) = freediscrim X + 2"
- | "freediscrim (DECRYPT K X) = freediscrim X - 2"
-
-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)
-
-subsection{*The Initial Algebra: A Quotiented Message Type*}
-
-quotient_type msg = freemsg / msgrel
- by (rule equiv_msgrel)
-
-text{*The abstract message constructors*}
-
-quotient_definition
- "Nonce :: nat \<Rightarrow> msg"
-is
- "NONCE"
-
-quotient_definition
- "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
-is
- "MPAIR"
-
-quotient_definition
- "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-is
- "CRYPT"
-
-quotient_definition
- "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
-is
- "DECRYPT"
-
-lemma [quot_respect]:
- shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
-by (auto intro: CRYPT)
-
-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]:
- shows "Crypt K (Decrypt K X) = X"
- by (lifting CD)
-
-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"
-is
- "freenonces"
-
-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]:
- 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"
-is
- "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"
-is
- "freeright"
-
-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
- assume "Nonce m = Nonce n"
- then show "m = n" by (lifting NONCE_imp_eq)
-next
- assume "m = n"
- 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'"
- hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
- thus "X = X'" by simp
-next
- assume "X = X'"
- thus "Crypt K X = Crypt K X'" by simp
-qed
-
-theorem Decrypt_Decrypt_eq [iff]:
- shows "(Decrypt K X = Decrypt K X') = (X=X')"
-proof
- assume "Decrypt K X = Decrypt K X'"
- hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
- thus "X = X'" by simp
-next
- assume "X = X'"
- thus "Decrypt K X = Decrypt K X'" by simp
-qed
-
-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.*}
-
-quotient_definition
- "discrim:: msg \<Rightarrow> int"
-is
- "freediscrim"
-
-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
-
--- a/src/HOL/Quotient_Examples/LarryInt.thy Wed Apr 28 17:42:37 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,395 +0,0 @@
-
-header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
-
-theory LarryInt
-imports Main Quotient_Product
-begin
-
-fun
- intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
-where
- "intrel (x, y) (u, v) = (x + v = u + y)"
-
-quotient_type int = "nat \<times> nat" / intrel
- by (auto simp add: equivp_def expand_fun_eq)
-
-instantiation int :: "{zero, one, plus, uminus, minus, times, ord}"
-begin
-
-quotient_definition
- Zero_int_def: "0::int" is "(0::nat, 0::nat)"
-
-quotient_definition
- One_int_def: "1::int" is "(1::nat, 0::nat)"
-
-definition
- "add_raw \<equiv> \<lambda>(x, y) (u, v). (x + (u::nat), y + (v::nat))"
-
-quotient_definition
- "(op +) :: int \<Rightarrow> int \<Rightarrow> int"
-is
- "add_raw"
-
-definition
- "uminus_raw \<equiv> \<lambda>(x::nat, y::nat). (y, x)"
-
-quotient_definition
- "uminus :: int \<Rightarrow> int"
-is
- "uminus_raw"
-
-fun
- mult_raw::"nat \<times> nat \<Rightarrow> nat \<times> nat \<Rightarrow> nat \<times> nat"
-where
- "mult_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
-
-quotient_definition
- "(op *) :: int \<Rightarrow> int \<Rightarrow> int"
-is
- "mult_raw"
-
-definition
- "le_raw \<equiv> \<lambda>(x, y) (u, v). (x+v \<le> u+(y::nat))"
-
-quotient_definition
- le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool"
-is
- "le_raw"
-
-definition
- less_int_def: "z < (w::int) \<equiv> (z \<le> w & z \<noteq> w)"
-
-definition
- diff_int_def: "z - (w::int) \<equiv> z + (-w)"
-
-instance ..
-
-end
-
-subsection{*Construction of the Integers*}
-
-lemma zminus_zminus_raw:
- "uminus_raw (uminus_raw z) = z"
- by (cases z) (simp add: uminus_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel) uminus_raw uminus_raw"
- by (simp add: uminus_raw_def)
-
-lemma zminus_zminus:
- fixes z::"int"
- shows "- (- z) = z"
- by(lifting zminus_zminus_raw)
-
-lemma zminus_0_raw:
- shows "uminus_raw (0, 0) = (0, 0::nat)"
- by (simp add: uminus_raw_def)
-
-lemma zminus_0:
- shows "- 0 = (0::int)"
- by (lifting zminus_0_raw)
-
-subsection{*Integer Addition*}
-
-lemma zminus_zadd_distrib_raw:
- shows "uminus_raw (add_raw z w) = add_raw (uminus_raw z) (uminus_raw w)"
-by (cases z, cases w)
- (auto simp add: add_raw_def uminus_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> intrel) add_raw add_raw"
-by (simp add: add_raw_def)
-
-lemma zminus_zadd_distrib:
- fixes z w::"int"
- shows "- (z + w) = (- z) + (- w)"
- by(lifting zminus_zadd_distrib_raw)
-
-lemma zadd_commute_raw:
- shows "add_raw z w = add_raw w z"
-by (cases z, cases w)
- (simp add: add_raw_def)
-
-lemma zadd_commute:
- fixes z w::"int"
- shows "(z::int) + w = w + z"
- by (lifting zadd_commute_raw)
-
-lemma zadd_assoc_raw:
- shows "add_raw (add_raw z1 z2) z3 = add_raw z1 (add_raw z2 z3)"
- by (cases z1, cases z2, cases z3) (simp add: add_raw_def)
-
-lemma zadd_assoc:
- fixes z1 z2 z3::"int"
- shows "(z1 + z2) + z3 = z1 + (z2 + z3)"
- by (lifting zadd_assoc_raw)
-
-lemma zadd_0_raw:
- shows "add_raw (0, 0) z = z"
- by (simp add: add_raw_def)
-
-
-text {*also for the instance declaration int :: plus_ac0*}
-lemma zadd_0:
- fixes z::"int"
- shows "0 + z = z"
- by (lifting zadd_0_raw)
-
-lemma zadd_zminus_inverse_raw:
- shows "intrel (add_raw (uminus_raw z) z) (0, 0)"
- by (cases z) (simp add: add_raw_def uminus_raw_def)
-
-lemma zadd_zminus_inverse2:
- fixes z::"int"
- shows "(- z) + z = 0"
- by (lifting zadd_zminus_inverse_raw)
-
-subsection{*Integer Multiplication*}
-
-lemma zmult_zminus_raw:
- shows "mult_raw (uminus_raw z) w = uminus_raw (mult_raw z w)"
-apply(cases z, cases w)
-apply(simp add: uminus_raw_def)
-done
-
-lemma mult_raw_fst:
- assumes a: "intrel x z"
- shows "intrel (mult_raw x y) (mult_raw z y)"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma mult_raw_snd:
- assumes a: "intrel x z"
- shows "intrel (mult_raw y x) (mult_raw y z)"
-using a
-apply(cases x, cases y, cases z)
-apply(auto simp add: mult_raw.simps intrel.simps)
-apply(rename_tac u v w x y z)
-apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
-apply(simp add: mult_ac)
-apply(simp add: add_mult_distrib [symmetric])
-done
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> intrel) mult_raw mult_raw"
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule equivp_transp[OF int_equivp])
-apply(rule mult_raw_fst)
-apply(assumption)
-apply(rule mult_raw_snd)
-apply(assumption)
-done
-
-lemma zmult_zminus:
- fixes z w::"int"
- shows "(- z) * w = - (z * w)"
- by (lifting zmult_zminus_raw)
-
-lemma zmult_commute_raw:
- shows "mult_raw z w = mult_raw w z"
-apply(cases z, cases w)
-apply(simp add: add_ac mult_ac)
-done
-
-lemma zmult_commute:
- fixes z w::"int"
- shows "z * w = w * z"
- by (lifting zmult_commute_raw)
-
-lemma zmult_assoc_raw:
- shows "mult_raw (mult_raw z1 z2) z3 = mult_raw z1 (mult_raw z2 z3)"
-apply(cases z1, cases z2, cases z3)
-apply(simp add: add_mult_distrib2 mult_ac)
-done
-
-lemma zmult_assoc:
- fixes z1 z2 z3::"int"
- shows "(z1 * z2) * z3 = z1 * (z2 * z3)"
- by (lifting zmult_assoc_raw)
-
-lemma zadd_mult_distrib_raw:
- shows "mult_raw (add_raw z1 z2) w = add_raw (mult_raw z1 w) (mult_raw z2 w)"
-apply(cases z1, cases z2, cases w)
-apply(simp add: add_mult_distrib2 mult_ac add_raw_def)
-done
-
-lemma zadd_zmult_distrib:
- fixes z1 z2 w::"int"
- shows "(z1 + z2) * w = (z1 * w) + (z2 * w)"
- by(lifting zadd_mult_distrib_raw)
-
-lemma zadd_zmult_distrib2:
- fixes w z1 z2::"int"
- shows "w * (z1 + z2) = (w * z1) + (w * z2)"
- by (simp add: zmult_commute [of w] zadd_zmult_distrib)
-
-lemma zdiff_zmult_distrib:
- fixes w z1 z2::"int"
- shows "(z1 - z2) * w = (z1 * w) - (z2 * w)"
- by (simp add: diff_int_def zadd_zmult_distrib zmult_zminus)
-
-lemma zdiff_zmult_distrib2:
- fixes w z1 z2::"int"
- shows "w * (z1 - z2) = (w * z1) - (w * z2)"
- by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
-
-lemmas int_distrib =
- zadd_zmult_distrib zadd_zmult_distrib2
- zdiff_zmult_distrib zdiff_zmult_distrib2
-
-lemma zmult_1_raw:
- shows "mult_raw (1, 0) z = z"
- by (cases z) (auto)
-
-lemma zmult_1:
- fixes z::"int"
- shows "1 * z = z"
- by (lifting zmult_1_raw)
-
-lemma zmult_1_right:
- fixes z::"int"
- shows "z * 1 = z"
- by (rule trans [OF zmult_commute zmult_1])
-
-lemma zero_not_one:
- shows "\<not>(intrel (0, 0) (1::nat, 0::nat))"
- by auto
-
-text{*The Integers Form A Ring*}
-instance int :: comm_ring_1
-proof
- fix i j k :: int
- show "(i + j) + k = i + (j + k)" by (simp add: zadd_assoc)
- show "i + j = j + i" by (simp add: zadd_commute)
- show "0 + i = i" by (rule zadd_0)
- show "- i + i = 0" by (rule zadd_zminus_inverse2)
- show "i - j = i + (-j)" by (simp add: diff_int_def)
- show "(i * j) * k = i * (j * k)" by (rule zmult_assoc)
- show "i * j = j * i" by (rule zmult_commute)
- show "1 * i = i" by (rule zmult_1)
- show "(i + j) * k = i * k + j * k" by (simp add: int_distrib)
- show "0 \<noteq> (1::int)" by (lifting zero_not_one)
-qed
-
-
-subsection{*The @{text "\<le>"} Ordering*}
-
-lemma zle_refl_raw:
- shows "le_raw w w"
- by (cases w) (simp add: le_raw_def)
-
-lemma [quot_respect]:
- shows "(intrel ===> intrel ===> op =) le_raw le_raw"
- by (auto) (simp_all add: le_raw_def)
-
-lemma zle_refl:
- fixes w::"int"
- shows "w \<le> w"
- by (lifting zle_refl_raw)
-
-
-lemma zle_trans_raw:
- shows "\<lbrakk>le_raw i j; le_raw j k\<rbrakk> \<Longrightarrow> le_raw i k"
-apply(cases i, cases j, cases k)
-apply(auto simp add: le_raw_def)
-done
-
-lemma zle_trans:
- fixes i j k::"int"
- shows "\<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> i \<le> k"
- by (lifting zle_trans_raw)
-
-lemma zle_anti_sym_raw:
- shows "\<lbrakk>le_raw z w; le_raw w z\<rbrakk> \<Longrightarrow> intrel z w"
-apply(cases z, cases w)
-apply(auto iff: le_raw_def)
-done
-
-lemma zle_anti_sym:
- fixes z w::"int"
- shows "\<lbrakk>z \<le> w; w \<le> z\<rbrakk> \<Longrightarrow> z = w"
- by (lifting zle_anti_sym_raw)
-
-
-(* Axiom 'order_less_le' of class 'order': *)
-lemma zless_le:
- fixes w z::"int"
- shows "(w < z) = (w \<le> z & w \<noteq> z)"
- by (simp add: less_int_def)
-
-instance int :: order
-apply (default)
-apply(auto simp add: zless_le zle_anti_sym)[1]
-apply(rule zle_refl)
-apply(erule zle_trans, assumption)
-apply(erule zle_anti_sym, assumption)
-done
-
-(* Axiom 'linorder_linear' of class 'linorder': *)
-
-lemma zle_linear_raw:
- shows "le_raw z w \<or> le_raw w z"
-apply(cases w, cases z)
-apply(auto iff: le_raw_def)
-done
-
-lemma zle_linear:
- fixes z w::"int"
- shows "z \<le> w \<or> w \<le> z"
- by (lifting zle_linear_raw)
-
-instance int :: linorder
-apply(default)
-apply(rule zle_linear)
-done
-
-lemma zadd_left_mono_raw:
- shows "le_raw i j \<Longrightarrow> le_raw (add_raw k i) (add_raw k j)"
-apply(cases k)
-apply(auto simp add: add_raw_def le_raw_def)
-done
-
-lemma zadd_left_mono:
- fixes i j::"int"
- shows "i \<le> j \<Longrightarrow> k + i \<le> k + j"
- by (lifting zadd_left_mono_raw)
-
-
-subsection{*Magnitide of an Integer, as a Natural Number: @{term nat}*}
-
-definition
- "nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
-
-quotient_definition
- "nat2::int \<Rightarrow> nat"
-is
- "nat_raw"
-
-abbreviation
- "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"
-
-lemma nat_le_eq_zle_raw:
- shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
- apply (cases w)
- apply (cases z)
- apply (simp add: nat_raw_def le_raw_def)
- by auto
-
-lemma [quot_respect]:
- shows "(intrel ===> op =) nat_raw nat_raw"
- by (auto iff: nat_raw_def)
-
-lemma nat_le_eq_zle:
- fixes w z::"int"
- shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (nat2 w \<le> nat2 z) = (w\<le>z)"
- unfolding less_int_def
- by (lifting nat_le_eq_zle_raw)
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Thu Apr 29 09:06:35 2010 +0200
@@ -0,0 +1,380 @@
+(* Title: HOL/Quotient_Examples/Quotient_Int.thy
+ Author: Cezary Kaliszyk
+ Author: Christian Urban
+
+Integers based on Quotients, based on an older version by Larry Paulson.
+*)
+theory Quotient_Int
+imports Quotient_Product Nat
+begin
+
+fun
+ intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
+where
+ "intrel (x, y) (u, v) = (x + v = u + y)"
+
+quotient_type int = "nat \<times> nat" / intrel
+ by (auto simp add: equivp_def expand_fun_eq)
+
+instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}"
+begin
+
+quotient_definition
+ "0 \<Colon> int" is "(0\<Colon>nat, 0\<Colon>nat)"
+
+quotient_definition
+ "1 \<Colon> int" is "(1\<Colon>nat, 0\<Colon>nat)"
+
+fun
+ plus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "plus_int_raw (x, y) (u, v) = (x + u, y + v)"
+
+quotient_definition
+ "(op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int)" is "plus_int_raw"
+
+fun
+ uminus_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "uminus_int_raw (x, y) = (y, x)"
+
+quotient_definition
+ "(uminus \<Colon> (int \<Rightarrow> int))" is "uminus_int_raw"
+
+definition
+ minus_int_def [code del]: "z - w = z + (-w\<Colon>int)"
+
+fun
+ times_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
+where
+ "times_int_raw (x, y) (u, v) = (x*u + y*v, x*v + y*u)"
+
+quotient_definition
+ "(op *) :: (int \<Rightarrow> int \<Rightarrow> int)" is "times_int_raw"
+
+fun
+ le_int_raw :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
+where
+ "le_int_raw (x, y) (u, v) = (x+v \<le> u+y)"
+
+quotient_definition
+ le_int_def: "(op \<le>) :: int \<Rightarrow> int \<Rightarrow> bool" is "le_int_raw"
+
+definition
+ less_int_def [code del]: "(z\<Colon>int) < w = (z \<le> w \<and> z \<noteq> w)"
+
+definition
+ zabs_def: "\<bar>i\<Colon>int\<bar> = (if i < 0 then - i else i)"
+
+definition
+ zsgn_def: "sgn (i\<Colon>int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"
+
+instance ..
+
+end
+
+lemma [quot_respect]:
+ shows "(op \<approx> ===> op \<approx> ===> op \<approx>) plus_int_raw plus_int_raw"
+ and "(op \<approx> ===> op \<approx>) uminus_int_raw uminus_int_raw"
+ and "(op \<approx> ===> op \<approx> ===> op =) le_int_raw le_int_raw"
+ by auto
+
+lemma times_int_raw_fst:
+ assumes a: "x \<approx> z"
+ shows "times_int_raw x y \<approx> times_int_raw z y"
+ using a
+ apply(cases x, cases y, cases z)
+ apply(auto simp add: times_int_raw.simps intrel.simps)
+ apply(rename_tac u v w x y z)
+ apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
+ apply(simp add: mult_ac)
+ apply(simp add: add_mult_distrib [symmetric])
+ done
+
+lemma times_int_raw_snd:
+ assumes a: "x \<approx> z"
+ shows "times_int_raw y x \<approx> times_int_raw y z"
+ using a
+ apply(cases x, cases y, cases z)
+ apply(auto simp add: times_int_raw.simps intrel.simps)
+ apply(rename_tac u v w x y z)
+ apply(subgoal_tac "u*w + z*w = y*w + v*w & u*x + z*x = y*x + v*x")
+ apply(simp add: mult_ac)
+ apply(simp add: add_mult_distrib [symmetric])
+ done
+
+lemma [quot_respect]:
+ shows "(op \<approx> ===> op \<approx> ===> op \<approx>) times_int_raw times_int_raw"
+ apply(simp only: fun_rel_def)
+ apply(rule allI | rule impI)+
+ apply(rule equivp_transp[OF int_equivp])
+ apply(rule times_int_raw_fst)
+ apply(assumption)
+ apply(rule times_int_raw_snd)
+ apply(assumption)
+ done
+
+lemma plus_assoc_raw:
+ shows "plus_int_raw (plus_int_raw i j) k \<approx> plus_int_raw i (plus_int_raw j k)"
+ by (cases i, cases j, cases k) (simp)
+
+lemma plus_sym_raw:
+ shows "plus_int_raw i j \<approx> plus_int_raw j i"
+ by (cases i, cases j) (simp)
+
+lemma plus_zero_raw:
+ shows "plus_int_raw (0, 0) i \<approx> i"
+ by (cases i) (simp)
+
+lemma plus_minus_zero_raw:
+ shows "plus_int_raw (uminus_int_raw i) i \<approx> (0, 0)"
+ by (cases i) (simp)
+
+lemma times_assoc_raw:
+ shows "times_int_raw (times_int_raw i j) k \<approx> times_int_raw i (times_int_raw j k)"
+ by (cases i, cases j, cases k)
+ (simp add: algebra_simps)
+
+lemma times_sym_raw:
+ shows "times_int_raw i j \<approx> times_int_raw j i"
+ by (cases i, cases j) (simp add: algebra_simps)
+
+lemma times_one_raw:
+ shows "times_int_raw (1, 0) i \<approx> i"
+ by (cases i) (simp)
+
+lemma times_plus_comm_raw:
+ shows "times_int_raw (plus_int_raw i j) k \<approx> plus_int_raw (times_int_raw i k) (times_int_raw j k)"
+by (cases i, cases j, cases k)
+ (simp add: algebra_simps)
+
+lemma one_zero_distinct:
+ shows "\<not> (0, 0) \<approx> ((1::nat), (0::nat))"
+ by simp
+
+text{* The integers form a @{text comm_ring_1}*}
+
+instance int :: comm_ring_1
+proof
+ fix i j k :: int
+ show "(i + j) + k = i + (j + k)"
+ by (lifting plus_assoc_raw)
+ show "i + j = j + i"
+ by (lifting plus_sym_raw)
+ show "0 + i = (i::int)"
+ by (lifting plus_zero_raw)
+ show "- i + i = 0"
+ by (lifting plus_minus_zero_raw)
+ show "i - j = i + - j"
+ by (simp add: minus_int_def)
+ show "(i * j) * k = i * (j * k)"
+ by (lifting times_assoc_raw)
+ show "i * j = j * i"
+ by (lifting times_sym_raw)
+ show "1 * i = i"
+ by (lifting times_one_raw)
+ show "(i + j) * k = i * k + j * k"
+ by (lifting times_plus_comm_raw)
+ show "0 \<noteq> (1::int)"
+ by (lifting one_zero_distinct)
+qed
+
+lemma plus_int_raw_rsp_aux:
+ assumes a: "a \<approx> b" "c \<approx> d"
+ shows "plus_int_raw a c \<approx> plus_int_raw b d"
+ using a
+ by (cases a, cases b, cases c, cases d)
+ (simp)
+
+lemma add_abs_int:
+ "(abs_int (x,y)) + (abs_int (u,v)) =
+ (abs_int (x + u, y + v))"
+ apply(simp add: plus_int_def id_simps)
+ apply(fold plus_int_raw.simps)
+ apply(rule Quotient_rel_abs[OF Quotient_int])
+ apply(rule plus_int_raw_rsp_aux)
+ apply(simp_all add: rep_abs_rsp_left[OF Quotient_int])
+ done
+
+definition int_of_nat_raw:
+ "int_of_nat_raw m = (m :: nat, 0 :: nat)"
+
+quotient_definition
+ "int_of_nat :: nat \<Rightarrow> int" is "int_of_nat_raw"
+
+lemma[quot_respect]:
+ shows "(op = ===> op \<approx>) int_of_nat_raw int_of_nat_raw"
+ by (simp add: equivp_reflp[OF int_equivp])
+
+lemma int_of_nat:
+ shows "of_nat m = int_of_nat m"
+ by (induct m)
+ (simp_all add: zero_int_def one_int_def int_of_nat_def int_of_nat_raw add_abs_int)
+
+lemma le_antisym_raw:
+ shows "le_int_raw i j \<Longrightarrow> le_int_raw j i \<Longrightarrow> i \<approx> j"
+ by (cases i, cases j) (simp)
+
+lemma le_refl_raw:
+ shows "le_int_raw i i"
+ by (cases i) (simp)
+
+lemma le_trans_raw:
+ shows "le_int_raw i j \<Longrightarrow> le_int_raw j k \<Longrightarrow> le_int_raw i k"
+ by (cases i, cases j, cases k) (simp)
+
+lemma le_cases_raw:
+ shows "le_int_raw i j \<or> le_int_raw j i"
+ by (cases i, cases j)
+ (simp add: linorder_linear)
+
+instance int :: linorder
+proof
+ fix i j k :: int
+ show antisym: "i \<le> j \<Longrightarrow> j \<le> i \<Longrightarrow> i = j"
+ by (lifting le_antisym_raw)
+ show "(i < j) = (i \<le> j \<and> \<not> j \<le> i)"
+ by (auto simp add: less_int_def dest: antisym)
+ show "i \<le> i"
+ by (lifting le_refl_raw)
+ show "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> i \<le> k"
+ by (lifting le_trans_raw)
+ show "i \<le> j \<or> j \<le> i"
+ by (lifting le_cases_raw)
+qed
+
+instantiation int :: distrib_lattice
+begin
+
+definition
+ "(inf \<Colon> int \<Rightarrow> int \<Rightarrow> int) = min"
+
+definition
+ "(sup \<Colon> int \<Rightarrow> int \<Rightarrow> int) = max"
+
+instance
+ by default
+ (auto simp add: inf_int_def sup_int_def min_max.sup_inf_distrib1)
+
+end
+
+lemma le_plus_int_raw:
+ shows "le_int_raw i j \<Longrightarrow> le_int_raw (plus_int_raw k i) (plus_int_raw k j)"
+ by (cases i, cases j, cases k) (simp)
+
+instance int :: ordered_cancel_ab_semigroup_add
+proof
+ fix i j k :: int
+ show "i \<le> j \<Longrightarrow> k + i \<le> k + j"
+ by (lifting le_plus_int_raw)
+qed
+
+abbreviation
+ "less_int_raw i j \<equiv> le_int_raw i j \<and> \<not>(i \<approx> j)"
+
+lemma zmult_zless_mono2_lemma:
+ fixes i j::int
+ and k::nat
+ shows "i < j \<Longrightarrow> 0 < k \<Longrightarrow> of_nat k * i < of_nat k * j"
+ apply(induct "k")
+ apply(simp)
+ apply(case_tac "k = 0")
+ apply(simp_all add: left_distrib add_strict_mono)
+ done
+
+lemma zero_le_imp_eq_int_raw:
+ fixes k::"(nat \<times> nat)"
+ shows "less_int_raw (0, 0) k \<Longrightarrow> (\<exists>n > 0. k \<approx> int_of_nat_raw n)"
+ apply(cases k)
+ apply(simp add:int_of_nat_raw)
+ apply(auto)
+ apply(rule_tac i="b" and j="a" in less_Suc_induct)
+ apply(auto)
+ done
+
+lemma zero_le_imp_eq_int:
+ fixes k::int
+ shows "0 < k \<Longrightarrow> \<exists>n > 0. k = of_nat n"
+ unfolding less_int_def int_of_nat
+ by (lifting zero_le_imp_eq_int_raw)
+
+lemma zmult_zless_mono2:
+ fixes i j k::int
+ assumes a: "i < j" "0 < k"
+ shows "k * i < k * j"
+ using a
+ by (drule_tac zero_le_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)
+
+text{*The integers form an ordered integral domain*}
+
+instance int :: linordered_idom
+proof
+ fix i j k :: int
+ show "i < j \<Longrightarrow> 0 < k \<Longrightarrow> k * i < k * j"
+ by (rule zmult_zless_mono2)
+ show "\<bar>i\<bar> = (if i < 0 then -i else i)"
+ by (simp only: zabs_def)
+ show "sgn (i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+ by (simp only: zsgn_def)
+qed
+
+lemmas int_distrib =
+ left_distrib [of "z1::int" "z2" "w", standard]
+ right_distrib [of "w::int" "z1" "z2", standard]
+ left_diff_distrib [of "z1::int" "z2" "w", standard]
+ right_diff_distrib [of "w::int" "z1" "z2", standard]
+ minus_add_distrib[of "z1::int" "z2", standard]
+
+lemma int_induct_raw:
+ assumes a: "P (0::nat, 0)"
+ and b: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (1, 0))"
+ and c: "\<And>i. P i \<Longrightarrow> P (plus_int_raw i (uminus_int_raw (1, 0)))"
+ shows "P x"
+proof (cases x, clarify)
+ fix a b
+ show "P (a, b)"
+ proof (induct a arbitrary: b rule: Nat.induct)
+ case zero
+ show "P (0, b)" using assms by (induct b) auto
+ next
+ case (Suc n)
+ then show ?case using assms by auto
+ qed
+qed
+
+lemma int_induct:
+ fixes x :: int
+ assumes a: "P 0"
+ and b: "\<And>i. P i \<Longrightarrow> P (i + 1)"
+ and c: "\<And>i. P i \<Longrightarrow> P (i - 1)"
+ shows "P x"
+ using a b c unfolding minus_int_def
+ by (lifting int_induct_raw)
+
+text {* Magnitide of an Integer, as a Natural Number: @{term nat} *}
+
+definition
+ "int_to_nat_raw \<equiv> \<lambda>(x, y).x - (y::nat)"
+
+quotient_definition
+ "int_to_nat::int \<Rightarrow> nat"
+is
+ "int_to_nat_raw"
+
+lemma [quot_respect]:
+ shows "(intrel ===> op =) int_to_nat_raw int_to_nat_raw"
+ by (auto iff: int_to_nat_raw_def)
+
+lemma nat_le_eq_zle_raw:
+ assumes a: "less_int_raw (0, 0) w \<or> le_int_raw (0, 0) z"
+ shows "(int_to_nat_raw w \<le> int_to_nat_raw z) = (le_int_raw w z)"
+ using a
+ by (cases w, cases z) (auto simp add: int_to_nat_raw_def)
+
+lemma nat_le_eq_zle:
+ fixes w z::"int"
+ shows "0 < w \<or> 0 \<le> z \<Longrightarrow> (int_to_nat w \<le> int_to_nat z) = (w \<le> z)"
+ unfolding less_int_def
+ by (lifting nat_le_eq_zle_raw)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Apr 29 09:06:35 2010 +0200
@@ -0,0 +1,399 @@
+(* Title: HOL/Quotient_Examples/Quotient_Message.thy
+ Author: Christian Urban
+
+Message datatype, based on an older version by Larry Paulson.
+*)
+theory Quotient_Message
+imports Main Quotient_Syntax
+begin
+
+subsection{*Defining the Free Algebra*}
+
+datatype
+ freemsg = NONCE nat
+ | MPAIR freemsg freemsg
+ | CRYPT nat freemsg
+ | DECRYPT nat freemsg
+
+inductive
+ msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
+where
+ CD: "CRYPT K (DECRYPT K X) \<sim> X"
+| DC: "DECRYPT K (CRYPT K X) \<sim> X"
+| NONCE: "NONCE N \<sim> NONCE N"
+| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
+| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
+| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
+| SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
+| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
+
+lemmas msgrel.intros[intro]
+
+text{*Proving that it is an equivalence relation*}
+
+lemma msgrel_refl: "X \<sim> X"
+by (induct X, (blast intro: msgrel.intros)+)
+
+theorem equiv_msgrel: "equivp msgrel"
+proof (rule equivpI)
+ show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
+ show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
+ show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
+qed
+
+subsection{*Some Functions on the Free Algebra*}
+
+subsubsection{*The Set of Nonces*}
+
+fun
+ freenonces :: "freemsg \<Rightarrow> nat set"
+where
+ "freenonces (NONCE N) = {N}"
+| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
+| "freenonces (CRYPT K X) = freenonces X"
+| "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.*}
+fun
+ freeleft :: "freemsg \<Rightarrow> freemsg"
+where
+ "freeleft (NONCE N) = NONCE N"
+| "freeleft (MPAIR X Y) = X"
+| "freeleft (CRYPT K X) = freeleft X"
+| "freeleft (DECRYPT K X) = freeleft X"
+
+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)
+
+subsubsection{*The Right Projection*}
+
+text{*A function to return the right part of the top pair in a message.*}
+fun
+ freeright :: "freemsg \<Rightarrow> freemsg"
+where
+ "freeright (NONCE N) = NONCE N"
+| "freeright (MPAIR X Y) = Y"
+| "freeright (CRYPT K X) = freeright X"
+| "freeright (DECRYPT K X) = freeright X"
+
+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
+ freediscrim :: "freemsg \<Rightarrow> int"
+where
+ "freediscrim (NONCE N) = 0"
+ | "freediscrim (MPAIR X Y) = 1"
+ | "freediscrim (CRYPT K X) = freediscrim X + 2"
+ | "freediscrim (DECRYPT K X) = freediscrim X - 2"
+
+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)
+
+subsection{*The Initial Algebra: A Quotiented Message Type*}
+
+quotient_type msg = freemsg / msgrel
+ by (rule equiv_msgrel)
+
+text{*The abstract message constructors*}
+
+quotient_definition
+ "Nonce :: nat \<Rightarrow> msg"
+is
+ "NONCE"
+
+quotient_definition
+ "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "MPAIR"
+
+quotient_definition
+ "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "CRYPT"
+
+quotient_definition
+ "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+is
+ "DECRYPT"
+
+lemma [quot_respect]:
+ shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
+by (auto intro: CRYPT)
+
+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]:
+ shows "Crypt K (Decrypt K X) = X"
+ by (lifting CD)
+
+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"
+is
+ "freenonces"
+
+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]:
+ 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"
+is
+ "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"
+is
+ "freeright"
+
+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
+ assume "Nonce m = Nonce n"
+ then show "m = n" by (lifting NONCE_imp_eq)
+next
+ assume "m = n"
+ 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'"
+ hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
+ thus "X = X'" by simp
+next
+ assume "X = X'"
+ thus "Crypt K X = Crypt K X'" by simp
+qed
+
+theorem Decrypt_Decrypt_eq [iff]:
+ shows "(Decrypt K X = Decrypt K X') = (X=X')"
+proof
+ assume "Decrypt K X = Decrypt K X'"
+ hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
+ thus "X = X'" by simp
+next
+ assume "X = X'"
+ thus "Decrypt K X = Decrypt K X'" by simp
+qed
+
+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.*}
+
+quotient_definition
+ "discrim:: msg \<Rightarrow> int"
+is
+ "freediscrim"
+
+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
+
--- a/src/HOL/Quotient_Examples/ROOT.ML Wed Apr 28 17:42:37 2010 +0200
+++ b/src/HOL/Quotient_Examples/ROOT.ML Thu Apr 29 09:06:35 2010 +0200
@@ -4,5 +4,5 @@
Testing the quotient package.
*)
-use_thys ["FSet", "LarryInt", "LarryDatatype"];
+use_thys ["FSet", "Quotient_Int", "Quotient_Message"];