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))