src/HOL/Quotient_Examples/Quotient_Message.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47304 a0d97d919f01
child 58305 57752a91eec4
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
     1
(*  Title:      HOL/Quotient_Examples/Quotient_Message.thy
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
     2
    Author:     Christian Urban
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
     3
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
     4
Message datatype, based on an older version by Larry Paulson.
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
     5
*)
41467
8fc17c5e11c0 tuned headers;
wenzelm
parents: 40823
diff changeset
     6
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
     7
theory Quotient_Message
45535
fbad87611fae tuned header
bulwahn
parents: 41467
diff changeset
     8
imports Main "~~/src/HOL/Library/Quotient_Syntax"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     9
begin
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    10
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    11
subsection{*Defining the Free Algebra*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    12
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    13
datatype
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
  freemsg = NONCE  nat
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
        | MPAIR  freemsg freemsg
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
    16
        | CRYPT  nat freemsg
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    17
        | DECRYPT  nat freemsg
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
    19
inductive
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
  msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
    21
where
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    22
  CD:    "CRYPT K (DECRYPT K X) \<sim> X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    23
| DC:    "DECRYPT K (CRYPT K X) \<sim> X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
| NONCE: "NONCE N \<sim> NONCE N"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    25
| MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
| CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    27
| DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    28
| SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    29
| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    30
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
lemmas msgrel.intros[intro]
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    32
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
text{*Proving that it is an equivalence relation*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    34
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    35
lemma msgrel_refl: "X \<sim> X"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
    36
by (induct X) (auto intro: msgrel.intros)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
theorem equiv_msgrel: "equivp msgrel"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    39
proof (rule equivpI)
40823
37b25a87d7ef adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
haftmann
parents: 40468
diff changeset
    40
  show "reflp msgrel" by (rule reflpI) (simp add: msgrel_refl)
37b25a87d7ef adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
haftmann
parents: 40468
diff changeset
    41
  show "symp msgrel" by (rule sympI) (blast intro: msgrel.SYM)
37b25a87d7ef adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
haftmann
parents: 40468
diff changeset
    42
  show "transp msgrel" by (rule transpI) (blast intro: msgrel.TRANS)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
qed
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    44
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    45
subsection{*Some Functions on the Free Algebra*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    46
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    47
subsubsection{*The Set of Nonces*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    48
40823
37b25a87d7ef adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
haftmann
parents: 40468
diff changeset
    49
primrec
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    50
  freenonces :: "freemsg \<Rightarrow> nat set"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    51
where
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    52
  "freenonces (NONCE N) = {N}"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    53
| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    54
| "freenonces (CRYPT K X) = freenonces X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    55
| "freenonces (DECRYPT K X) = freenonces X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    56
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
    57
theorem msgrel_imp_eq_freenonces:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    58
  assumes a: "U \<sim> V"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    59
  shows "freenonces U = freenonces V"
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
    60
  using a by (induct) (auto)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    61
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    62
subsubsection{*The Left Projection*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    63
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    64
text{*A function to return the left part of the top pair in a message.  It will
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    65
be lifted to the initial algrebra, to serve as an example of that process.*}
40823
37b25a87d7ef adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
haftmann
parents: 40468
diff changeset
    66
primrec
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    67
  freeleft :: "freemsg \<Rightarrow> freemsg"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    68
where
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    69
  "freeleft (NONCE N) = NONCE N"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    70
| "freeleft (MPAIR X Y) = X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
| "freeleft (CRYPT K X) = freeleft X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
| "freeleft (DECRYPT K X) = freeleft X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    73
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    74
text{*This theorem lets us prove that the left function respects the
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    75
equivalence relation.  It also helps us prove that MPair
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    76
  (the abstract constructor) is injective*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    77
lemma msgrel_imp_eqv_freeleft_aux:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    78
  shows "freeleft U \<sim> freeleft U"
40823
37b25a87d7ef adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
haftmann
parents: 40468
diff changeset
    79
  by (fact msgrel_refl)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    80
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    81
theorem msgrel_imp_eqv_freeleft:
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
    82
  assumes a: "U \<sim> V"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    83
  shows "freeleft U \<sim> freeleft V"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    84
  using a
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    85
  by (induct) (auto intro: msgrel_imp_eqv_freeleft_aux)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    86
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    87
subsubsection{*The Right Projection*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    88
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    89
text{*A function to return the right part of the top pair in a message.*}
40823
37b25a87d7ef adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
haftmann
parents: 40468
diff changeset
    90
primrec
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    91
  freeright :: "freemsg \<Rightarrow> freemsg"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    92
where
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    93
  "freeright (NONCE N) = NONCE N"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    94
| "freeright (MPAIR X Y) = Y"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    95
| "freeright (CRYPT K X) = freeright X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    96
| "freeright (DECRYPT K X) = freeright X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    97
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    98
text{*This theorem lets us prove that the right function respects the
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    99
equivalence relation.  It also helps us prove that MPair
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   100
  (the abstract constructor) is injective*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   101
lemma msgrel_imp_eqv_freeright_aux:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   102
  shows "freeright U \<sim> freeright U"
40823
37b25a87d7ef adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
haftmann
parents: 40468
diff changeset
   103
  by (fact msgrel_refl)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   104
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   105
theorem msgrel_imp_eqv_freeright:
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   106
  assumes a: "U \<sim> V"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   107
  shows "freeright U \<sim> freeright V"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   108
  using a
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   109
  by (induct) (auto intro: msgrel_imp_eqv_freeright_aux)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   110
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   111
subsubsection{*The Discriminator for Constructors*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   112
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   113
text{*A function to distinguish nonces, mpairs and encryptions*}
40823
37b25a87d7ef adaptions to changes in Equiv_Relation.thy; prefer primrec if possible
haftmann
parents: 40468
diff changeset
   114
primrec
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   115
  freediscrim :: "freemsg \<Rightarrow> int"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   116
where
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   117
   "freediscrim (NONCE N) = 0"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   118
 | "freediscrim (MPAIR X Y) = 1"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   119
 | "freediscrim (CRYPT K X) = freediscrim X + 2"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   120
 | "freediscrim (DECRYPT K X) = freediscrim X - 2"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   121
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   122
text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   123
theorem msgrel_imp_eq_freediscrim:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   124
  assumes a: "U \<sim> V"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   125
  shows "freediscrim U = freediscrim V"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   126
  using a by (induct) (auto)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   127
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   128
subsection{*The Initial Algebra: A Quotiented Message Type*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   129
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   130
quotient_type msg = freemsg / msgrel
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   131
  by (rule equiv_msgrel)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   132
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   133
text{*The abstract message constructors*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   134
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   135
quotient_definition
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   136
  "Nonce :: nat \<Rightarrow> msg"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   137
is
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   138
  "NONCE"
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45535
diff changeset
   139
done
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   140
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   141
quotient_definition
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   142
  "MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   143
is
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   144
  "MPAIR"
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45535
diff changeset
   145
by (rule MPAIR)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   146
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   147
quotient_definition
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   148
  "Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   149
is
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   150
  "CRYPT"
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45535
diff changeset
   151
by (rule CRYPT)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   152
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   153
quotient_definition
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   154
  "Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   155
is
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   156
  "DECRYPT"
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45535
diff changeset
   157
by (rule DECRYPT)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   158
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   159
text{*Establishing these two equations is the point of the whole exercise*}
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   160
theorem CD_eq [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   161
  shows "Crypt K (Decrypt K X) = X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   162
  by (lifting CD)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   163
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   164
theorem DC_eq [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   165
  shows "Decrypt K (Crypt K X) = X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   166
  by (lifting DC)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   167
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   168
subsection{*The Abstract Function to Return the Set of Nonces*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   169
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   170
quotient_definition
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   171
   "nonces:: msg \<Rightarrow> nat set"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   172
is
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   173
  "freenonces"
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45535
diff changeset
   174
by (rule msgrel_imp_eq_freenonces)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   175
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   176
text{*Now prove the four equations for @{term nonces}*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   177
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   178
lemma nonces_Nonce [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   179
  shows "nonces (Nonce N) = {N}"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   180
  by (lifting freenonces.simps(1))
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   181
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   182
lemma nonces_MPair [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   183
  shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   184
  by (lifting freenonces.simps(2))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   185
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   186
lemma nonces_Crypt [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   187
  shows "nonces (Crypt K X) = nonces X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   188
  by (lifting freenonces.simps(3))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   189
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   190
lemma nonces_Decrypt [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   191
  shows "nonces (Decrypt K X) = nonces X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   192
  by (lifting freenonces.simps(4))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   193
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   194
subsection{*The Abstract Function to Return the Left Part*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   195
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   196
quotient_definition
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   197
  "left:: msg \<Rightarrow> msg"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   198
is
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   199
  "freeleft"
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45535
diff changeset
   200
by (rule msgrel_imp_eqv_freeleft)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   201
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   202
lemma left_Nonce [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   203
  shows "left (Nonce N) = Nonce N"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   204
  by (lifting freeleft.simps(1))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   205
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   206
lemma left_MPair [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   207
  shows "left (MPair X Y) = X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   208
  by (lifting freeleft.simps(2))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   209
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   210
lemma left_Crypt [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   211
  shows "left (Crypt K X) = left X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   212
  by (lifting freeleft.simps(3))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   213
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   214
lemma left_Decrypt [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   215
  shows "left (Decrypt K X) = left X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   216
  by (lifting freeleft.simps(4))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   217
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   218
subsection{*The Abstract Function to Return the Right Part*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   219
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   220
quotient_definition
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   221
  "right:: msg \<Rightarrow> msg"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   222
is
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   223
  "freeright"
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45535
diff changeset
   224
by (rule msgrel_imp_eqv_freeright)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   225
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   226
text{*Now prove the four equations for @{term right}*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   227
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   228
lemma right_Nonce [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   229
  shows "right (Nonce N) = Nonce N"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   230
  by (lifting freeright.simps(1))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   231
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   232
lemma right_MPair [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   233
  shows "right (MPair X Y) = Y"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   234
  by (lifting freeright.simps(2))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   235
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   236
lemma right_Crypt [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   237
  shows "right (Crypt K X) = right X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   238
  by (lifting freeright.simps(3))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   239
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   240
lemma right_Decrypt [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   241
  shows "right (Decrypt K X) = right X"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   242
  by (lifting freeright.simps(4))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   243
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   244
subsection{*Injectivity Properties of Some Constructors*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   245
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   246
text{*Can also be proved using the function @{term nonces}*}
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   247
lemma Nonce_Nonce_eq [iff]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   248
  shows "(Nonce m = Nonce n) = (m = n)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   249
proof
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   250
  assume "Nonce m = Nonce n"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   251
  then show "m = n" 
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   252
    by (descending) (drule msgrel_imp_eq_freenonces, simp)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   253
next
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   254
  assume "m = n"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   255
  then show "Nonce m = Nonce n" by simp
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   256
qed
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   257
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   258
lemma MPair_imp_eq_left:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   259
  assumes eq: "MPair X Y = MPair X' Y'"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   260
  shows "X = X'"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   261
  using eq 
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   262
  by (descending) (drule msgrel_imp_eqv_freeleft, simp)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   263
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   264
lemma MPair_imp_eq_right:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   265
  shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   266
  by (descending) (drule msgrel_imp_eqv_freeright, simp)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   267
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   268
theorem MPair_MPair_eq [iff]:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   269
  shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   270
  by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   271
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   272
theorem Nonce_neq_MPair [iff]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   273
  shows "Nonce N \<noteq> MPair X Y"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   274
  by (descending) (auto dest: msgrel_imp_eq_freediscrim)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   275
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   276
text{*Example suggested by a referee*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   277
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   278
theorem Crypt_Nonce_neq_Nonce:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   279
  shows "Crypt K (Nonce M) \<noteq> Nonce N"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   280
  by (descending) (auto dest: msgrel_imp_eq_freediscrim) 
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   281
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   282
text{*...and many similar results*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   283
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   284
theorem Crypt2_Nonce_neq_Nonce:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   285
  shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
37594
32ad67684ee7 cosmetics: avoided statement of raw theorems, used the method descending instead
Christian Urban <urbanc@in.tum.de>
parents: 36524
diff changeset
   286
  by (descending) (auto dest: msgrel_imp_eq_freediscrim)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   287
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   288
theorem Crypt_Crypt_eq [iff]:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   289
  shows "(Crypt K X = Crypt K X') = (X=X')"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   290
proof
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   291
  assume "Crypt K X = Crypt K X'"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   292
  hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   293
  thus "X = X'" by simp
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   294
next
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   295
  assume "X = X'"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   296
  thus "Crypt K X = Crypt K X'" by simp
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   297
qed
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   298
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   299
theorem Decrypt_Decrypt_eq [iff]:
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   300
  shows "(Decrypt K X = Decrypt K X') = (X=X')"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   301
proof
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   302
  assume "Decrypt K X = Decrypt K X'"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   303
  hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   304
  thus "X = X'" by simp
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   305
next
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   306
  assume "X = X'"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   307
  thus "Decrypt K X = Decrypt K X'" by simp
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   308
qed
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   309
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   310
lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   311
  assumes N: "\<And>N. P (Nonce N)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   312
      and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   313
      and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   314
      and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   315
  shows "P msg"
47304
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   316
  using N M C D 
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   317
  by (descending) (auto intro: freemsg.induct)
a0d97d919f01 tuned proofs
Christian Urban <urbanc@in.tum.de>
parents: 47092
diff changeset
   318
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   319
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   320
subsection{*The Abstract Discriminator*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   321
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   322
text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   323
need this function in order to prove discrimination theorems.*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   324
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   325
quotient_definition
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   326
  "discrim:: msg \<Rightarrow> int"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   327
is
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   328
  "freediscrim"
47092
fa3538d6004b fix Quotient_Examples
kuncar
parents: 45535
diff changeset
   329
by (rule msgrel_imp_eq_freediscrim)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   330
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   331
text{*Now prove the four equations for @{term discrim}*}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   332
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   333
lemma discrim_Nonce [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   334
  shows "discrim (Nonce N) = 0"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   335
  by (lifting freediscrim.simps(1))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   336
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   337
lemma discrim_MPair [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   338
  shows "discrim (MPair X Y) = 1"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   339
  by (lifting freediscrim.simps(2))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   340
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   341
lemma discrim_Crypt [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   342
  shows "discrim (Crypt K X) = discrim X + 2"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   343
  by (lifting freediscrim.simps(3))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   344
36524
3909002beca5 Tuning the quotient examples
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35222
diff changeset
   345
lemma discrim_Decrypt [simp]:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   346
  shows "discrim (Decrypt K X) = discrim X - 2"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   347
  by (lifting freediscrim.simps(4))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   348
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   349
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   350