# Theory QuoDataType

Up to index of Isabelle/HOL/Induct

theory QuoDataType
imports Main
begin

    (*  Title:      HOL/Induct/QuoDataType
        ID:         $Id: QuoDataType.thy,v 1.9 2005/06/17 14:13:07 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   2004  University of Cambridge

    *)

    header{*Defining an Initial Algebra by Quotienting a Free Algebra*}

    theory QuoDataType imports Main begin

    subsection{*Defining the Free Algebra*}

    text{*Messages with encryption and decryption as free constructors.*}
    datatype
         freemsg = NONCE  nat
                 | MPAIR  freemsg freemsg
                 | CRYPT  nat freemsg
                 | DECRYPT  nat freemsg

    text{*The equivalence relation, which makes encryption and decryption inverses
    provided the keys are the same.*}
    consts  msgrel :: "(freemsg * freemsg) set"

    syntax
      "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "~~" 50)
    syntax (xsymbols)
      "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "∼" 50)
    syntax (HTML output)
      "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "∼" 50)
    translations
      "X ∼ Y" == "(X,Y) ∈ msgrel"

    text{*The first two rules are the desired equations. The next four rules
    make the equations applicable to subterms. The last two rules are symmetry
    and transitivity.*}
    inductive "msgrel"
      intros
        CD:    "CRYPT K (DECRYPT K X) ∼ X"
        DC:    "DECRYPT K (CRYPT K X) ∼ X"
        NONCE: "NONCE N ∼ NONCE N"
        MPAIR: "[|X ∼ X'; Y ∼ Y'|] ==> MPAIR X Y ∼ MPAIR X' Y'"
        CRYPT: "X ∼ X' ==> CRYPT K X ∼ CRYPT K X'"
        DECRYPT: "X ∼ X' ==> DECRYPT K X ∼ DECRYPT K X'"
        SYM:   "X ∼ Y ==> Y ∼ X"
        TRANS: "[|X ∼ Y; Y ∼ Z|] ==> X ∼ Z"

    text{*Proving that it is an equivalence relation*}

    lemma msgrel_refl: "X ∼ X"
    by (induct X, (blast intro: msgrel.intros)+)

    theorem equiv_msgrel: "equiv UNIV msgrel"
    proof (simp add: equiv_def, intro conjI)
      show "reflexive msgrel" by (simp add: refl_def msgrel_refl)
      show "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
      show "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
    qed

    subsection{*Some Functions on the Free Algebra*}

    subsubsection{*The Set of Nonces*}

    text{*A function to return the set of nonces present in a message.  It will
    be lifted to the initial algrebra, to serve as an example of that process.*}
    consts
      freenonces :: "freemsg => nat set"

    primrec
       "freenonces (NONCE N) = {N}"
       "freenonces (MPAIR X Y) = freenonces X ∪ freenonces Y"
       "freenonces (CRYPT K X) = freenonces X"
       "freenonces (DECRYPT K X) = freenonces X"

    text{*This theorem lets us prove that the nonces function respects the
    equivalence relation.  It also helps us prove that Nonce
      (the abstract constructor) is injective*}
    theorem msgrel_imp_eq_freenonces: "U ∼ V ==> freenonces U = freenonces V"
    by (erule msgrel.induct, auto)

    subsubsection{*The Left Projection*}

    text{*A function to return the left part of the top pair in a message.  It will
    be lifted to the initial algrebra, to serve as an example of that process.*}
    consts freeleft :: "freemsg => freemsg"
    primrec
       "freeleft (NONCE N) = NONCE N"
       "freeleft (MPAIR X Y) = X"
       "freeleft (CRYPT K X) = freeleft X"
       "freeleft (DECRYPT K X) = freeleft X"

    text{*This theorem lets us prove that the left function respects the
    equivalence relation.  It also helps us prove that MPair
      (the abstract constructor) is injective*}
    theorem msgrel_imp_eqv_freeleft:
         "U ∼ V ==> freeleft U ∼ freeleft V"
    by (erule msgrel.induct, auto intro: msgrel.intros)

    subsubsection{*The Right Projection*}

    text{*A function to return the right part of the top pair in a message.*}
    consts freeright :: "freemsg => freemsg"
    primrec
       "freeright (NONCE N) = NONCE N"
       "freeright (MPAIR X Y) = Y"
       "freeright (CRYPT K X) = freeright X"
       "freeright (DECRYPT K X) = freeright X"

    text{*This theorem lets us prove that the right function respects the
    equivalence relation.  It also helps us prove that MPair
      (the abstract constructor) is injective*}
    theorem msgrel_imp_eqv_freeright:
         "U ∼ V ==> freeright U ∼ freeright V"
    by (erule msgrel.induct, auto intro: msgrel.intros)

    subsubsection{*The Discriminator for Constructors*}

    text{*A function to distinguish nonces, mpairs and encryptions*}
    consts freediscrim :: "freemsg => int"
    primrec
       "freediscrim (NONCE N) = 0"
       "freediscrim (MPAIR X Y) = 1"
       "freediscrim (CRYPT K X) = freediscrim X + 2"
       "freediscrim (DECRYPT K X) = freediscrim X - 2"

    text{*This theorem helps us prove @{term "Nonce N ≠ MPair X Y"}*}
    theorem msgrel_imp_eq_freediscrim:
         "U ∼ V ==> freediscrim U = freediscrim V"
    by (erule msgrel.induct, auto)

    subsection{*The Initial Algebra: A Quotiented Message Type*}

    typedef (Msg)  msg = "UNIV//msgrel"
        by (auto simp add: quotient_def)

    text{*The abstract message constructors*}
    constdefs
      Nonce :: "nat => msg"
      "Nonce N == Abs_Msg(msgrel``{NONCE N})"

      MPair :: "[msg,msg] => msg"
       "MPair X Y ==
           Abs_Msg (\<Union>U ∈ Rep_Msg X. \<Union>V ∈ Rep_Msg Y. msgrel``{MPAIR U V})"

      Crypt :: "[nat,msg] => msg"
       "Crypt K X ==
           Abs_Msg (\<Union>U ∈ Rep_Msg X. msgrel``{CRYPT K U})"

      Decrypt :: "[nat,msg] => msg"
       "Decrypt K X ==
           Abs_Msg (\<Union>U ∈ Rep_Msg X. msgrel``{DECRYPT K U})"

    text{*Reduces equality of equivalence classes to the @{term msgrel} relation:
      @{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) ∈ msgrel)"} *}
    lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I]

    declare equiv_msgrel_iff [simp]

    text{*All equivalence classes belong to set of representatives*}
    lemma [simp]: "msgrel``{U} ∈ Msg"
    by (auto simp add: Msg_def quotient_def intro: msgrel_refl)

    lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"
    apply (rule inj_on_inverseI)
    apply (erule Abs_Msg_inverse)
    done

    text{*Reduces equality on abstractions to equality on representatives*}
    declare inj_on_Abs_Msg [THEN inj_on_iff, simp]

    declare Abs_Msg_inverse [simp]

    subsubsection{*Characteristic Equations for the Abstract Constructors*}

    lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) =
                  Abs_Msg (msgrel``{MPAIR U V})"
    proof -
      have "(λU V. msgrel `` {MPAIR U V}) respects2 msgrel"
        by (simp add: congruent2_def msgrel.MPAIR)
      thus ?thesis
        by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel equiv_msgrel])
    qed

    lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
    proof -
      have "(λU. msgrel `` {CRYPT K U}) respects msgrel"
        by (simp add: congruent_def msgrel.CRYPT)
      thus ?thesis
        by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
    qed

    lemma Decrypt:
         "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
    proof -
      have "(λU. msgrel `` {DECRYPT K U}) respects msgrel"
        by (simp add: congruent_def msgrel.DECRYPT)
      thus ?thesis
        by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
    qed

    text{*Case analysis on the representation of a msg as an equivalence class.*}
    lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]:
         "(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P"
    apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE])
    apply (drule arg_cong [where f=Abs_Msg])
    apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl)
    done

    text{*Establishing these two equations is the point of the whole exercise*}
    theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
    by (cases X, simp add: Crypt Decrypt CD)

    theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
    by (cases X, simp add: Crypt Decrypt DC)

    subsection{*The Abstract Function to Return the Set of Nonces*}

    constdefs
      nonces :: "msg => nat set"
       "nonces X == \<Union>U ∈ Rep_Msg X. freenonces U"

    lemma nonces_congruent: "freenonces respects msgrel"
    by (simp add: congruent_def msgrel_imp_eq_freenonces)

    text{*Now prove the four equations for @{term nonces}*}

    lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}"
    by (simp add: nonces_def Nonce_def
                  UN_equiv_class [OF equiv_msgrel nonces_congruent])

    lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X ∪ nonces Y"
    apply (cases X, cases Y)
    apply (simp add: nonces_def MPair
                     UN_equiv_class [OF equiv_msgrel nonces_congruent])
    done

    lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X"
    apply (cases X)
    apply (simp add: nonces_def Crypt
                     UN_equiv_class [OF equiv_msgrel nonces_congruent])
    done

    lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
    apply (cases X)
    apply (simp add: nonces_def Decrypt
                     UN_equiv_class [OF equiv_msgrel nonces_congruent])
    done

    subsection{*The Abstract Function to Return the Left Part*}

    constdefs
      left :: "msg => msg"
       "left X == Abs_Msg (\<Union>U ∈ Rep_Msg X. msgrel``{freeleft U})"

    lemma left_congruent: "(λU. msgrel `` {freeleft U}) respects msgrel"
    by (simp add: congruent_def msgrel_imp_eqv_freeleft)

    text{*Now prove the four equations for @{term left}*}

    lemma left_Nonce [simp]: "left (Nonce N) = Nonce N"
    by (simp add: left_def Nonce_def
                  UN_equiv_class [OF equiv_msgrel left_congruent])

    lemma left_MPair [simp]: "left (MPair X Y) = X"
    apply (cases X, cases Y)
    apply (simp add: left_def MPair
                     UN_equiv_class [OF equiv_msgrel left_congruent])
    done

    lemma left_Crypt [simp]: "left (Crypt K X) = left X"
    apply (cases X)
    apply (simp add: left_def Crypt
                     UN_equiv_class [OF equiv_msgrel left_congruent])
    done

    lemma left_Decrypt [simp]: "left (Decrypt K X) = left X"
    apply (cases X)
    apply (simp add: left_def Decrypt
                     UN_equiv_class [OF equiv_msgrel left_congruent])
    done

    subsection{*The Abstract Function to Return the Right Part*}

    constdefs
      right :: "msg => msg"
       "right X == Abs_Msg (\<Union>U ∈ Rep_Msg X. msgrel``{freeright U})"

    lemma right_congruent: "(λU. msgrel `` {freeright U}) respects msgrel"
    by (simp add: congruent_def msgrel_imp_eqv_freeright)

    text{*Now prove the four equations for @{term right}*}

    lemma right_Nonce [simp]: "right (Nonce N) = Nonce N"
    by (simp add: right_def Nonce_def
                  UN_equiv_class [OF equiv_msgrel right_congruent])

    lemma right_MPair [simp]: "right (MPair X Y) = Y"
    apply (cases X, cases Y)
    apply (simp add: right_def MPair
                     UN_equiv_class [OF equiv_msgrel right_congruent])
    done

    lemma right_Crypt [simp]: "right (Crypt K X) = right X"
    apply (cases X)
    apply (simp add: right_def Crypt
                     UN_equiv_class [OF equiv_msgrel right_congruent])
    done

    lemma right_Decrypt [simp]: "right (Decrypt K X) = right X"
    apply (cases X)
    apply (simp add: right_def Decrypt
                     UN_equiv_class [OF equiv_msgrel right_congruent])
    done

    subsection{*Injectivity Properties of Some Constructors*}

    lemma NONCE_imp_eq: "NONCE m ∼ NONCE n ==> m = n"
    by (drule msgrel_imp_eq_freenonces, simp)

    text{*Can also be proved using the function @{term nonces}*}
    lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)"
    by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)

    lemma MPAIR_imp_eqv_left: "MPAIR X Y ∼ MPAIR X' Y' ==> X ∼ X'"
    by (drule msgrel_imp_eqv_freeleft, simp)

    lemma MPair_imp_eq_left:
      assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'"
    proof -
      from eq
      have "left (MPair X Y) = left (MPair X' Y')" by simp
      thus ?thesis by simp
    qed

    lemma MPAIR_imp_eqv_right: "MPAIR X Y ∼ MPAIR X' Y' ==> Y ∼ Y'"
    by (drule msgrel_imp_eqv_freeright, simp)

    lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' ==> Y = Y'"
    apply (cases X, cases X', cases Y, cases Y')
    apply (simp add: MPair)
    apply (erule MPAIR_imp_eqv_right)
    done

    theorem MPair_MPair_eq [iff]: "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')"
    by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)

    lemma NONCE_neqv_MPAIR: "NONCE m ∼ MPAIR X Y ==> False"
    by (drule msgrel_imp_eq_freediscrim, simp)

    theorem Nonce_neq_MPair [iff]: "Nonce N ≠ MPair X Y"
    apply (cases X, cases Y)
    apply (simp add: Nonce_def MPair)
    apply (blast dest: NONCE_neqv_MPAIR)
    done

    text{*Example suggested by a referee*}
    theorem Crypt_Nonce_neq_Nonce: "Crypt K (Nonce M) ≠ Nonce N"
    by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)

    text{*...and many similar results*}
    theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) ≠ Nonce N"
    by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)

    theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')"
    proof
      assume "Crypt K X = Crypt K X'"
      hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
      thus "X = X'" by simp
    next
      assume "X = X'"
      thus "Crypt K X = Crypt K X'" by simp
    qed

    theorem Decrypt_Decrypt_eq [iff]: "(Decrypt K X = Decrypt K X') = (X=X')"
    proof
      assume "Decrypt K X = Decrypt K X'"
      hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
      thus "X = X'" by simp
    next
      assume "X = X'"
      thus "Decrypt K X = Decrypt K X'" by simp
    qed

    lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
      assumes N: "!!N. P (Nonce N)"
          and M: "!!X Y. [|P X; P Y|] ==> P (MPair X Y)"
          and C: "!!K X. P X ==> P (Crypt K X)"
          and D: "!!K X. P X ==> P (Decrypt K X)"
      shows "P msg"
    proof (cases msg, erule ssubst)
      fix U::freemsg
      show "P (Abs_Msg (msgrel `` {U}))"
      proof (induct U)
        case (NONCE N)
        with N show ?case by (simp add: Nonce_def)
      next
        case (MPAIR X Y)
        with M [of "Abs_Msg (msgrel `` {X})" "Abs_Msg (msgrel `` {Y})"]
        show ?case by (simp add: MPair)
      next
        case (CRYPT K X)
        with C [of "Abs_Msg (msgrel `` {X})"]
        show ?case by (simp add: Crypt)
      next
        case (DECRYPT K X)
        with D [of "Abs_Msg (msgrel `` {X})"]
        show ?case by (simp add: Decrypt)
      qed
    qed

    subsection{*The Abstract Discriminator*}

    text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
    need this function in order to prove discrimination theorems.*}

    constdefs
      discrim :: "msg => int"
       "discrim X == contents (\<Union>U ∈ Rep_Msg X. {freediscrim U})"

    lemma discrim_congruent: "(λU. {freediscrim U}) respects msgrel"
    by (simp add: congruent_def msgrel_imp_eq_freediscrim)

    text{*Now prove the four equations for @{term discrim}*}

    lemma discrim_Nonce [simp]: "discrim (Nonce N) = 0"
    by (simp add: discrim_def Nonce_def
                  UN_equiv_class [OF equiv_msgrel discrim_congruent])

    lemma discrim_MPair [simp]: "discrim (MPair X Y) = 1"
    apply (cases X, cases Y)
    apply (simp add: discrim_def MPair
                     UN_equiv_class [OF equiv_msgrel discrim_congruent])
    done

    lemma discrim_Crypt [simp]: "discrim (Crypt K X) = discrim X + 2"
    apply (cases X)
    apply (simp add: discrim_def Crypt
                     UN_equiv_class [OF equiv_msgrel discrim_congruent])
    done

    lemma discrim_Decrypt [simp]: "discrim (Decrypt K X) = discrim X - 2"
    apply (cases X)
    apply (simp add: discrim_def Decrypt
                     UN_equiv_class [OF equiv_msgrel discrim_congruent])
    done

    end

### Defining the Free Algebra

lemma msgrel_refl:

      X ∼ X

theorem equiv_msgrel:

      equiv UNIV msgrel

### Some Functions on the Free Algebra

#### The Set of Nonces

theorem msgrel_imp_eq_freenonces:

      U ∼ V ==> freenonces U = freenonces V

#### The Left Projection

theorem msgrel_imp_eqv_freeleft:

      U ∼ V ==> freeleft U ∼ freeleft V

#### The Right Projection

theorem msgrel_imp_eqv_freeright:

      U ∼ V ==> freeright U ∼ freeright V

#### The Discriminator for Constructors

theorem msgrel_imp_eq_freediscrim:

      U ∼ V ==> freediscrim U = freediscrim V

### The Initial Algebra: A Quotiented Message Type

lemmas equiv_msgrel_iff:

      (msgrel `` {x} = msgrel `` {y}) = (x ∼ y)

lemmas equiv_msgrel_iff:

      (msgrel `` {x} = msgrel `` {y}) = (x ∼ y)

lemma

      msgrel `` {U} ∈ Msg

lemma inj_on_Abs_Msg:

      inj_on Abs_Msg Msg

#### Characteristic Equations for the Abstract Constructors

lemma MPair:

      MPair (Abs_Msg (msgrel `` {U})) (Abs_Msg (msgrel `` {V})) =
      Abs_Msg (msgrel `` {MPAIR U V})

lemma Crypt:

      Crypt K (Abs_Msg (msgrel `` {U})) = Abs_Msg (msgrel `` {CRYPT K U})

lemma Decrypt:

      Decrypt K (Abs_Msg (msgrel `` {U})) = Abs_Msg (msgrel `` {DECRYPT K U})

lemma eq_Abs_Msg:

      (!!U. z = Abs_Msg (msgrel `` {U}) ==> P) ==> P

theorem CD_eq:

      Crypt K (Decrypt K X) = X

theorem DC_eq:

      Decrypt K (Crypt K X) = X

### The Abstract Function to Return the Set of Nonces

lemma nonces_congruent:

      freenonces respects msgrel

lemma nonces_Nonce:

      nonces (Nonce N) = {N}

lemma nonces_MPair:

      nonces (MPair X Y) = nonces X ∪ nonces Y

lemma nonces_Crypt:

      nonces (Crypt K X) = nonces X

lemma nonces_Decrypt:

      nonces (Decrypt K X) = nonces X

### The Abstract Function to Return the Left Part

lemma left_congruent:

      (%U. msgrel `` {freeleft U}) respects msgrel

lemma left_Nonce:

      left (Nonce N) = Nonce N

lemma left_MPair:

      left (MPair X Y) = X

lemma left_Crypt:

      left (Crypt K X) = left X

lemma left_Decrypt:

      left (Decrypt K X) = left X

### The Abstract Function to Return the Right Part

lemma right_congruent:

      (%U. msgrel `` {freeright U}) respects msgrel

lemma right_Nonce:

      right (Nonce N) = Nonce N

lemma right_MPair:

      right (MPair X Y) = Y

lemma right_Crypt:

      right (Crypt K X) = right X

lemma right_Decrypt:

      right (Decrypt K X) = right X

### Injectivity Properties of Some Constructors

lemma NONCE_imp_eq:

      NONCE m ∼ NONCE n ==> m = n

lemma Nonce_Nonce_eq:

      (Nonce m = Nonce n) = (m = n)

lemma MPAIR_imp_eqv_left:

      MPAIR X Y ∼ MPAIR X' Y' ==> X ∼ X'

lemma MPair_imp_eq_left:

      MPair X Y = MPair X' Y' ==> X = X'

lemma MPAIR_imp_eqv_right:

      MPAIR X Y ∼ MPAIR X' Y' ==> Y ∼ Y'

lemma MPair_imp_eq_right:

      MPair X Y = MPair X' Y' ==> Y = Y'

theorem MPair_MPair_eq:

      (MPair X Y = MPair X' Y') = (X = X' ∧ Y = Y')

lemma NONCE_neqv_MPAIR:

      NONCE m ∼ MPAIR X Y ==> False

theorem Nonce_neq_MPair:

      Nonce N ≠ MPair X Y

theorem Crypt_Nonce_neq_Nonce:

      Crypt K (Nonce M) ≠ Nonce N

theorem Crypt2_Nonce_neq_Nonce:

      Crypt K (Crypt K' (Nonce M)) ≠ Nonce N

theorem Crypt_Crypt_eq:

      (Crypt K X = Crypt K X') = (X = X')

theorem Decrypt_Decrypt_eq:

      (Decrypt K X = Decrypt K X') = (X = X')

lemma msg_induct:

      [| !!N. P (Nonce N); !!X Y. [| P X; P Y |] ==> P (MPair X Y);
         !!K X. P X ==> P (Crypt K X); !!K X. P X ==> P (Decrypt K X) |]
      ==> P msg

### The Abstract Discriminator

lemma discrim_congruent:

      (%U. {freediscrim U}) respects msgrel

lemma discrim_Nonce:

      discrim (Nonce N) = 0

lemma discrim_MPair:

      discrim (MPair X Y) = 1

lemma discrim_Crypt:

      discrim (Crypt K X) = discrim X + 2

lemma discrim_Decrypt:

      discrim (Decrypt K X) = discrim X - 2