src/HOL/Induct/QuoDataType.thy
author wenzelm
Sat, 17 Oct 2009 14:43:18 +0200
changeset 32960 69916a850301
parent 30198 922f944f03b2
child 39246 9e58f0499f57
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Induct/QuoDataType
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
     3
    Copyright   2004  University of Cambridge
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
     4
*)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
     5
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
     6
header{*Defining an Initial Algebra by Quotienting a Free Algebra*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
     7
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15172
diff changeset
     8
theory QuoDataType imports Main begin
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
     9
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    10
subsection{*Defining the Free Algebra*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    11
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    12
text{*Messages with encryption and decryption as free constructors.*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    13
datatype
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    14
     freemsg = NONCE  nat
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30198
diff changeset
    15
             | MPAIR  freemsg freemsg
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30198
diff changeset
    16
             | CRYPT  nat freemsg  
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30198
diff changeset
    17
             | DECRYPT  nat freemsg
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    18
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    19
text{*The equivalence relation, which makes encryption and decryption inverses
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    20
provided the keys are the same.
19736
wenzelm
parents: 18460
diff changeset
    21
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    22
The first two rules are the desired equations. The next four rules
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    23
make the equations applicable to subterms. The last two rules are symmetry
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    24
and transitivity.*}
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    25
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    26
inductive_set
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    27
  msgrel :: "(freemsg * freemsg) set"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    28
  and msg_rel :: "[freemsg, freemsg] => bool"  (infixl "\<sim>" 50)
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    29
  where
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    30
    "X \<sim> Y == (X,Y) \<in> msgrel"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    31
  | CD:    "CRYPT K (DECRYPT K X) \<sim> X"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    32
  | DC:    "DECRYPT K (CRYPT K X) \<sim> X"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    33
  | NONCE: "NONCE N \<sim> NONCE N"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    34
  | MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    35
  | CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    36
  | DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    37
  | SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 21404
diff changeset
    38
  | TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    39
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    40
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    41
text{*Proving that it is an equivalence relation*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    42
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    43
lemma msgrel_refl: "X \<sim> X"
18460
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
    44
  by (induct X) (blast intro: msgrel.intros)+
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    45
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    46
theorem equiv_msgrel: "equiv UNIV msgrel"
18460
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
    47
proof -
30198
922f944f03b2 name changes
nipkow
parents: 23746
diff changeset
    48
  have "refl msgrel" by (simp add: refl_on_def msgrel_refl)
18460
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
    49
  moreover have "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
    50
  moreover have "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
    51
  ultimately show ?thesis by (simp add: equiv_def)
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    52
qed
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    53
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    54
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    55
subsection{*Some Functions on the Free Algebra*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    56
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    57
subsubsection{*The Set of Nonces*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    58
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    59
text{*A function to return the set of nonces present in a message.  It will
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    60
be lifted to the initial algrebra, to serve as an example of that process.*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    61
consts
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    62
  freenonces :: "freemsg \<Rightarrow> nat set"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    63
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    64
primrec
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    65
   "freenonces (NONCE N) = {N}"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    66
   "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    67
   "freenonces (CRYPT K X) = freenonces X"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    68
   "freenonces (DECRYPT K X) = freenonces X"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    69
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    70
text{*This theorem lets us prove that the nonces function respects the
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    71
equivalence relation.  It also helps us prove that Nonce
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    72
  (the abstract constructor) is injective*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    73
theorem msgrel_imp_eq_freenonces: "U \<sim> V \<Longrightarrow> freenonces U = freenonces V"
18460
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
    74
  by (induct set: msgrel) auto
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    75
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    76
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    77
subsubsection{*The Left Projection*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    78
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    79
text{*A function to return the left part of the top pair in a message.  It will
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    80
be lifted to the initial algrebra, to serve as an example of that process.*}
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
    81
consts freeleft :: "freemsg \<Rightarrow> freemsg"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    82
primrec
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
    83
   "freeleft (NONCE N) = NONCE N"
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
    84
   "freeleft (MPAIR X Y) = X"
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
    85
   "freeleft (CRYPT K X) = freeleft X"
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
    86
   "freeleft (DECRYPT K X) = freeleft X"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    87
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    88
text{*This theorem lets us prove that the left function respects the
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    89
equivalence relation.  It also helps us prove that MPair
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    90
  (the abstract constructor) is injective*}
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
    91
theorem msgrel_imp_eqv_freeleft:
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
    92
     "U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V"
18460
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
    93
  by (induct set: msgrel) (auto intro: msgrel.intros)
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    94
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    95
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    96
subsubsection{*The Right Projection*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    97
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
    98
text{*A function to return the right part of the top pair in a message.*}
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
    99
consts freeright :: "freemsg \<Rightarrow> freemsg"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   100
primrec
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   101
   "freeright (NONCE N) = NONCE N"
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   102
   "freeright (MPAIR X Y) = Y"
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   103
   "freeright (CRYPT K X) = freeright X"
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   104
   "freeright (DECRYPT K X) = freeright X"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   105
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   106
text{*This theorem lets us prove that the right function respects the
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   107
equivalence relation.  It also helps us prove that MPair
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   108
  (the abstract constructor) is injective*}
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   109
theorem msgrel_imp_eqv_freeright:
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   110
     "U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V"
18460
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   111
  by (induct set: msgrel) (auto intro: msgrel.intros)
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   112
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   113
15152
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   114
subsubsection{*The Discriminator for Constructors*}
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   115
15152
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   116
text{*A function to distinguish nonces, mpairs and encryptions*}
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   117
consts freediscrim :: "freemsg \<Rightarrow> int"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   118
primrec
15152
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   119
   "freediscrim (NONCE N) = 0"
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   120
   "freediscrim (MPAIR X Y) = 1"
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   121
   "freediscrim (CRYPT K X) = freediscrim X + 2"
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   122
   "freediscrim (DECRYPT K X) = freediscrim X - 2"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   123
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   124
text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
15152
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   125
theorem msgrel_imp_eq_freediscrim:
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   126
     "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
18460
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   127
  by (induct set: msgrel) auto
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   128
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   129
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   130
subsection{*The Initial Algebra: A Quotiented Message Type*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   131
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   132
typedef (Msg)  msg = "UNIV//msgrel"
18460
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   133
  by (auto simp add: quotient_def)
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   134
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   135
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   136
text{*The abstract message constructors*}
19736
wenzelm
parents: 18460
diff changeset
   137
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   138
  Nonce :: "nat \<Rightarrow> msg" where
19736
wenzelm
parents: 18460
diff changeset
   139
  "Nonce N = Abs_Msg(msgrel``{NONCE N})"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   140
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   141
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   142
  MPair :: "[msg,msg] \<Rightarrow> msg" where
19736
wenzelm
parents: 18460
diff changeset
   143
   "MPair X Y =
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14658
diff changeset
   144
       Abs_Msg (\<Union>U \<in> Rep_Msg X. \<Union>V \<in> Rep_Msg Y. msgrel``{MPAIR U V})"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   145
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   146
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   147
  Crypt :: "[nat,msg] \<Rightarrow> msg" where
19736
wenzelm
parents: 18460
diff changeset
   148
   "Crypt K X =
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14658
diff changeset
   149
       Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{CRYPT K U})"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   150
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   151
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   152
  Decrypt :: "[nat,msg] \<Rightarrow> msg" where
19736
wenzelm
parents: 18460
diff changeset
   153
   "Decrypt K X =
15120
f0359f75682e undid UN/INT syntax
nipkow
parents: 14658
diff changeset
   154
       Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   155
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   156
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   157
text{*Reduces equality of equivalence classes to the @{term msgrel} relation:
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   158
  @{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)"} *}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   159
lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I]
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   160
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   161
declare equiv_msgrel_iff [simp]
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   162
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   163
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   164
text{*All equivalence classes belong to set of representatives*}
15169
2b5da07a0b89 new "respects" syntax for quotienting
paulson
parents: 15152
diff changeset
   165
lemma [simp]: "msgrel``{U} \<in> Msg"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   166
by (auto simp add: Msg_def quotient_def intro: msgrel_refl)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   167
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   168
lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   169
apply (rule inj_on_inverseI)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   170
apply (erule Abs_Msg_inverse)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   171
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   172
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   173
text{*Reduces equality on abstractions to equality on representatives*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   174
declare inj_on_Abs_Msg [THEN inj_on_iff, simp]
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   175
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   176
declare Abs_Msg_inverse [simp]
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   177
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   178
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   179
subsubsection{*Characteristic Equations for the Abstract Constructors*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   180
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   181
lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) = 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   182
              Abs_Msg (msgrel``{MPAIR U V})"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   183
proof -
15169
2b5da07a0b89 new "respects" syntax for quotienting
paulson
parents: 15152
diff changeset
   184
  have "(\<lambda>U V. msgrel `` {MPAIR U V}) respects2 msgrel"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   185
    by (simp add: congruent2_def msgrel.MPAIR)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   186
  thus ?thesis
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   187
    by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   188
qed
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   189
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   190
lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   191
proof -
15169
2b5da07a0b89 new "respects" syntax for quotienting
paulson
parents: 15152
diff changeset
   192
  have "(\<lambda>U. msgrel `` {CRYPT K U}) respects msgrel"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   193
    by (simp add: congruent_def msgrel.CRYPT)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   194
  thus ?thesis
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   195
    by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   196
qed
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   197
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   198
lemma Decrypt:
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   199
     "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   200
proof -
15169
2b5da07a0b89 new "respects" syntax for quotienting
paulson
parents: 15152
diff changeset
   201
  have "(\<lambda>U. msgrel `` {DECRYPT K U}) respects msgrel"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   202
    by (simp add: congruent_def msgrel.DECRYPT)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   203
  thus ?thesis
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   204
    by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   205
qed
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   206
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   207
text{*Case analysis on the representation of a msg as an equivalence class.*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   208
lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]:
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   209
     "(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   210
apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE])
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   211
apply (drule arg_cong [where f=Abs_Msg])
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   212
apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   213
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   214
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   215
text{*Establishing these two equations is the point of the whole exercise*}
14533
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   216
theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   217
by (cases X, simp add: Crypt Decrypt CD)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   218
14533
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   219
theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   220
by (cases X, simp add: Crypt Decrypt DC)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   221
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   222
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   223
subsection{*The Abstract Function to Return the Set of Nonces*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   224
19736
wenzelm
parents: 18460
diff changeset
   225
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   226
  nonces :: "msg \<Rightarrow> nat set" where
19736
wenzelm
parents: 18460
diff changeset
   227
   "nonces X = (\<Union>U \<in> Rep_Msg X. freenonces U)"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   228
15169
2b5da07a0b89 new "respects" syntax for quotienting
paulson
parents: 15152
diff changeset
   229
lemma nonces_congruent: "freenonces respects msgrel"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   230
by (simp add: congruent_def msgrel_imp_eq_freenonces) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   231
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   232
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   233
text{*Now prove the four equations for @{term nonces}*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   234
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   235
lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   236
by (simp add: nonces_def Nonce_def 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   237
              UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   238
 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   239
lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X \<union> nonces Y"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   240
apply (cases X, cases Y) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   241
apply (simp add: nonces_def MPair 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   242
                 UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   243
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   244
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   245
lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   246
apply (cases X) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   247
apply (simp add: nonces_def Crypt
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   248
                 UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   249
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   250
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   251
lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   252
apply (cases X) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   253
apply (simp add: nonces_def Decrypt
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   254
                 UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   255
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   256
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   257
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   258
subsection{*The Abstract Function to Return the Left Part*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   259
19736
wenzelm
parents: 18460
diff changeset
   260
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   261
  left :: "msg \<Rightarrow> msg" where
19736
wenzelm
parents: 18460
diff changeset
   262
   "left X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeleft U})"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   263
15169
2b5da07a0b89 new "respects" syntax for quotienting
paulson
parents: 15152
diff changeset
   264
lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   265
by (simp add: congruent_def msgrel_imp_eqv_freeleft) 
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   266
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   267
text{*Now prove the four equations for @{term left}*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   268
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   269
lemma left_Nonce [simp]: "left (Nonce N) = Nonce N"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   270
by (simp add: left_def Nonce_def 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   271
              UN_equiv_class [OF equiv_msgrel left_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   272
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   273
lemma left_MPair [simp]: "left (MPair X Y) = X"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   274
apply (cases X, cases Y) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   275
apply (simp add: left_def MPair 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   276
                 UN_equiv_class [OF equiv_msgrel left_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   277
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   278
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   279
lemma left_Crypt [simp]: "left (Crypt K X) = left X"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   280
apply (cases X) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   281
apply (simp add: left_def Crypt
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   282
                 UN_equiv_class [OF equiv_msgrel left_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   283
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   284
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   285
lemma left_Decrypt [simp]: "left (Decrypt K X) = left X"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   286
apply (cases X) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   287
apply (simp add: left_def Decrypt
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   288
                 UN_equiv_class [OF equiv_msgrel left_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   289
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   290
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   291
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   292
subsection{*The Abstract Function to Return the Right Part*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   293
19736
wenzelm
parents: 18460
diff changeset
   294
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   295
  right :: "msg \<Rightarrow> msg" where
19736
wenzelm
parents: 18460
diff changeset
   296
   "right X = Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{freeright U})"
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   297
15169
2b5da07a0b89 new "respects" syntax for quotienting
paulson
parents: 15152
diff changeset
   298
lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   299
by (simp add: congruent_def msgrel_imp_eqv_freeright) 
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   300
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   301
text{*Now prove the four equations for @{term right}*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   302
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   303
lemma right_Nonce [simp]: "right (Nonce N) = Nonce N"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   304
by (simp add: right_def Nonce_def 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   305
              UN_equiv_class [OF equiv_msgrel right_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   306
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   307
lemma right_MPair [simp]: "right (MPair X Y) = Y"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   308
apply (cases X, cases Y) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   309
apply (simp add: right_def MPair 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   310
                 UN_equiv_class [OF equiv_msgrel right_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   311
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   312
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   313
lemma right_Crypt [simp]: "right (Crypt K X) = right X"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   314
apply (cases X) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   315
apply (simp add: right_def Crypt
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   316
                 UN_equiv_class [OF equiv_msgrel right_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   317
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   318
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   319
lemma right_Decrypt [simp]: "right (Decrypt K X) = right X"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   320
apply (cases X) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   321
apply (simp add: right_def Decrypt
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   322
                 UN_equiv_class [OF equiv_msgrel right_congruent]) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   323
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   324
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   325
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   326
subsection{*Injectivity Properties of Some Constructors*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   327
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   328
lemma NONCE_imp_eq: "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   329
by (drule msgrel_imp_eq_freenonces, simp)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   330
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   331
text{*Can also be proved using the function @{term nonces}*}
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   332
lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   333
by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   334
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   335
lemma MPAIR_imp_eqv_left: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   336
by (drule msgrel_imp_eqv_freeleft, simp)
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   337
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   338
lemma MPair_imp_eq_left: 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   339
  assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   340
proof -
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   341
  from eq
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   342
  have "left (MPair X Y) = left (MPair X' Y')" by simp
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   343
  thus ?thesis by simp
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   344
qed
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   345
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   346
lemma MPAIR_imp_eqv_right: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
14658
b1293d0f8d5f congruent2 now allows different equiv relations
paulson
parents: 14565
diff changeset
   347
by (drule msgrel_imp_eqv_freeright, simp)
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   348
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   349
lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'" 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   350
apply (cases X, cases X', cases Y, cases Y') 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   351
apply (simp add: MPair)
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   352
apply (erule MPAIR_imp_eqv_right)  
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   353
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   354
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   355
theorem MPair_MPair_eq [iff]: "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" 
14533
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   356
by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   357
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   358
lemma NONCE_neqv_MPAIR: "NONCE m \<sim> MPAIR X Y \<Longrightarrow> False"
15152
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   359
by (drule msgrel_imp_eq_freediscrim, simp)
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   360
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   361
theorem Nonce_neq_MPair [iff]: "Nonce N \<noteq> MPair X Y"
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   362
apply (cases X, cases Y) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   363
apply (simp add: Nonce_def MPair) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   364
apply (blast dest: NONCE_neqv_MPAIR) 
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   365
done
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   366
15152
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   367
text{*Example suggested by a referee*}
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   368
theorem Crypt_Nonce_neq_Nonce: "Crypt K (Nonce M) \<noteq> Nonce N" 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   369
by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)  
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   370
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   371
text{*...and many similar results*}
15172
73069e033a0b new example of a quotiented nested data type
paulson
parents: 15169
diff changeset
   372
theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N" 
15152
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   373
by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)  
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   374
14533
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   375
theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')" 
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   376
proof
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   377
  assume "Crypt K X = Crypt K X'"
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   378
  hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   379
  thus "X = X'" by simp
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   380
next
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   381
  assume "X = X'"
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   382
  thus "Crypt K X = Crypt K X'" by simp
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   383
qed
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   384
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   385
theorem Decrypt_Decrypt_eq [iff]: "(Decrypt K X = Decrypt K X') = (X=X')" 
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   386
proof
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   387
  assume "Decrypt K X = Decrypt K X'"
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   388
  hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   389
  thus "X = X'" by simp
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   390
next
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   391
  assume "X = X'"
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   392
  thus "Decrypt K X = Decrypt K X'" by simp
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   393
qed
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   394
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   395
lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   396
  assumes N: "\<And>N. P (Nonce N)"
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   397
      and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   398
      and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   399
      and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   400
  shows "P msg"
18460
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   401
proof (cases msg)
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   402
  case (Abs_Msg U)
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   403
  have "P (Abs_Msg (msgrel `` {U}))"
14533
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   404
  proof (induct U)
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   405
    case (NONCE N) 
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   406
    with N show ?case by (simp add: Nonce_def) 
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   407
  next
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   408
    case (MPAIR X Y)
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   409
    with M [of "Abs_Msg (msgrel `` {X})" "Abs_Msg (msgrel `` {Y})"]
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   410
    show ?case by (simp add: MPair) 
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   411
  next
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   412
    case (CRYPT K X)
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   413
    with C [of "Abs_Msg (msgrel `` {X})"]
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   414
    show ?case by (simp add: Crypt) 
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   415
  next
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   416
    case (DECRYPT K X)
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   417
    with D [of "Abs_Msg (msgrel `` {X})"]
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   418
    show ?case by (simp add: Decrypt)
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   419
  qed
18460
9a1458cb2956 tuned induct proofs;
wenzelm
parents: 16417
diff changeset
   420
  with Abs_Msg show ?thesis by (simp only:)
14533
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   421
qed
32806c0afebf freeness theorems and induction rule
paulson
parents: 14527
diff changeset
   422
15152
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   423
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   424
subsection{*The Abstract Discriminator*}
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   425
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   426
text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   427
need this function in order to prove discrimination theorems.*}
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   428
19736
wenzelm
parents: 18460
diff changeset
   429
definition
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 21210
diff changeset
   430
  discrim :: "msg \<Rightarrow> int" where
19736
wenzelm
parents: 18460
diff changeset
   431
   "discrim X = contents (\<Union>U \<in> Rep_Msg X. {freediscrim U})"
15152
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   432
15169
2b5da07a0b89 new "respects" syntax for quotienting
paulson
parents: 15152
diff changeset
   433
lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
15152
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   434
by (simp add: congruent_def msgrel_imp_eq_freediscrim) 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   435
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   436
text{*Now prove the four equations for @{term discrim}*}
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   437
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   438
lemma discrim_Nonce [simp]: "discrim (Nonce N) = 0"
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   439
by (simp add: discrim_def Nonce_def 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   440
              UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   441
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   442
lemma discrim_MPair [simp]: "discrim (MPair X Y) = 1"
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   443
apply (cases X, cases Y) 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   444
apply (simp add: discrim_def MPair 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   445
                 UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   446
done
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   447
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   448
lemma discrim_Crypt [simp]: "discrim (Crypt K X) = discrim X + 2"
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   449
apply (cases X) 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   450
apply (simp add: discrim_def Crypt
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   451
                 UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   452
done
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   453
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   454
lemma discrim_Decrypt [simp]: "discrim (Decrypt K X) = discrim X - 2"
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   455
apply (cases X) 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   456
apply (simp add: discrim_def Decrypt
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   457
                 UN_equiv_class [OF equiv_msgrel discrim_congruent]) 
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   458
done
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   459
5c4d3f10ac5a new examples
paulson
parents: 15120
diff changeset
   460
14527
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   461
end
bc9e5587d05a IsaMakefile
paulson
parents:
diff changeset
   462