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"
```