src/HOL/Quotient_Examples/Quotient_Message.thy
changeset 40823 37b25a87d7ef
parent 40468 d4aac200199e
child 41467 8fc17c5e11c0
     1.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 30 17:19:11 2010 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Tue Nov 30 17:19:11 2010 +0100
     1.3 @@ -36,16 +36,16 @@
     1.4  
     1.5  theorem equiv_msgrel: "equivp msgrel"
     1.6  proof (rule equivpI)
     1.7 -  show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
     1.8 -  show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
     1.9 -  show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
    1.10 +  show "reflp msgrel" by (rule reflpI) (simp add: msgrel_refl)
    1.11 +  show "symp msgrel" by (rule sympI) (blast intro: msgrel.SYM)
    1.12 +  show "transp msgrel" by (rule transpI) (blast intro: msgrel.TRANS)
    1.13  qed
    1.14  
    1.15  subsection{*Some Functions on the Free Algebra*}
    1.16  
    1.17  subsubsection{*The Set of Nonces*}
    1.18  
    1.19 -fun
    1.20 +primrec
    1.21    freenonces :: "freemsg \<Rightarrow> nat set"
    1.22  where
    1.23    "freenonces (NONCE N) = {N}"
    1.24 @@ -62,7 +62,7 @@
    1.25  
    1.26  text{*A function to return the left part of the top pair in a message.  It will
    1.27  be lifted to the initial algrebra, to serve as an example of that process.*}
    1.28 -fun
    1.29 +primrec
    1.30    freeleft :: "freemsg \<Rightarrow> freemsg"
    1.31  where
    1.32    "freeleft (NONCE N) = NONCE N"
    1.33 @@ -75,7 +75,7 @@
    1.34    (the abstract constructor) is injective*}
    1.35  lemma msgrel_imp_eqv_freeleft_aux:
    1.36    shows "freeleft U \<sim> freeleft U"
    1.37 -  by (induct rule: freeleft.induct) (auto)
    1.38 +  by (fact msgrel_refl)
    1.39  
    1.40  theorem msgrel_imp_eqv_freeleft:
    1.41    assumes a: "U \<sim> V"
    1.42 @@ -86,7 +86,7 @@
    1.43  subsubsection{*The Right Projection*}
    1.44  
    1.45  text{*A function to return the right part of the top pair in a message.*}
    1.46 -fun
    1.47 +primrec
    1.48    freeright :: "freemsg \<Rightarrow> freemsg"
    1.49  where
    1.50    "freeright (NONCE N) = NONCE N"
    1.51 @@ -99,7 +99,7 @@
    1.52    (the abstract constructor) is injective*}
    1.53  lemma msgrel_imp_eqv_freeright_aux:
    1.54    shows "freeright U \<sim> freeright U"
    1.55 -  by (induct rule: freeright.induct) (auto)
    1.56 +  by (fact msgrel_refl)
    1.57  
    1.58  theorem msgrel_imp_eqv_freeright:
    1.59    assumes a: "U \<sim> V"
    1.60 @@ -110,7 +110,7 @@
    1.61  subsubsection{*The Discriminator for Constructors*}
    1.62  
    1.63  text{*A function to distinguish nonces, mpairs and encryptions*}
    1.64 -fun
    1.65 +primrec
    1.66    freediscrim :: "freemsg \<Rightarrow> int"
    1.67  where
    1.68     "freediscrim (NONCE N) = 0"