src/HOL/Quotient_Examples/Quotient_Message.thy
 changeset 47092 fa3538d6004b parent 45535 fbad87611fae child 47304 a0d97d919f01
```     1.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Mar 23 14:03:58 2012 +0100
1.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Mar 23 14:17:29 2012 +0100
1.3 @@ -136,29 +136,25 @@
1.4    "Nonce :: nat \<Rightarrow> msg"
1.5  is
1.6    "NONCE"
1.7 +done
1.8
1.9  quotient_definition
1.10    "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
1.11  is
1.12    "MPAIR"
1.13 +by (rule MPAIR)
1.14
1.15  quotient_definition
1.16    "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
1.17  is
1.18    "CRYPT"
1.19 +by (rule CRYPT)
1.20
1.21  quotient_definition
1.22    "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
1.23  is
1.24    "DECRYPT"
1.25 -
1.26 -lemma [quot_respect]:
1.27 -  shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
1.28 -by (auto intro: CRYPT)
1.29 -
1.30 -lemma [quot_respect]:
1.31 -  shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
1.32 -by (auto intro: DECRYPT)
1.33 +by (rule DECRYPT)
1.34
1.35  text{*Establishing these two equations is the point of the whole exercise*}
1.36  theorem CD_eq [simp]:
1.37 @@ -175,25 +171,14 @@
1.38     "nonces:: msg \<Rightarrow> nat set"
1.39  is
1.40    "freenonces"
1.41 +by (rule msgrel_imp_eq_freenonces)
1.42
1.43  text{*Now prove the four equations for @{term nonces}*}
1.44
1.45 -lemma [quot_respect]:
1.46 -  shows "(op \<sim> ===> op =) freenonces freenonces"
1.47 -  by (auto simp add: msgrel_imp_eq_freenonces)
1.48 -
1.49 -lemma [quot_respect]:
1.50 -  shows "(op = ===> op \<sim>) NONCE NONCE"
1.51 -  by (auto simp add: NONCE)
1.52 -
1.53  lemma nonces_Nonce [simp]:
1.54    shows "nonces (Nonce N) = {N}"
1.55    by (lifting freenonces.simps(1))
1.56
1.57 -lemma [quot_respect]:
1.58 -  shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
1.59 -  by (auto simp add: MPAIR)
1.60 -
1.61  lemma nonces_MPair [simp]:
1.62    shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
1.63    by (lifting freenonces.simps(2))
1.64 @@ -212,10 +197,7 @@
1.65    "left:: msg \<Rightarrow> msg"
1.66  is
1.67    "freeleft"
1.68 -
1.69 -lemma [quot_respect]:
1.70 -  shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
1.71 -  by (auto simp add: msgrel_imp_eqv_freeleft)
1.72 +by (rule msgrel_imp_eqv_freeleft)
1.73
1.74  lemma left_Nonce [simp]:
1.75    shows "left (Nonce N) = Nonce N"
1.76 @@ -239,13 +221,10 @@
1.77    "right:: msg \<Rightarrow> msg"
1.78  is
1.79    "freeright"
1.80 +by (rule msgrel_imp_eqv_freeright)
1.81
1.82  text{*Now prove the four equations for @{term right}*}
1.83
1.84 -lemma [quot_respect]:
1.85 -  shows "(op \<sim> ===> op \<sim>) freeright freeright"
1.86 -  by (auto simp add: msgrel_imp_eqv_freeright)
1.87 -
1.88  lemma right_Nonce [simp]:
1.89    shows "right (Nonce N) = Nonce N"
1.90    by (lifting freeright.simps(1))
1.91 @@ -352,13 +331,10 @@
1.92    "discrim:: msg \<Rightarrow> int"
1.93  is
1.94    "freediscrim"
1.95 +by (rule msgrel_imp_eq_freediscrim)
1.96
1.97  text{*Now prove the four equations for @{term discrim}*}
1.98
1.99 -lemma [quot_respect]:
1.100 -  shows "(op \<sim> ===> op =) freediscrim freediscrim"
1.101 -  by (auto simp add: msgrel_imp_eq_freediscrim)
1.102 -
1.103  lemma discrim_Nonce [simp]:
1.104    shows "discrim (Nonce N) = 0"
1.105    by (lifting freediscrim.simps(1))
```