src/HOL/Quotient_Examples/Quotient_Message.thy
changeset 47304 a0d97d919f01
parent 47092 fa3538d6004b
child 58305 57752a91eec4
     1.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Mon Apr 02 18:12:53 2012 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Mon Apr 02 21:26:07 2012 +0100
     1.3 @@ -307,20 +307,15 @@
     1.4    thus "Decrypt K X = Decrypt K X'" by simp
     1.5  qed
     1.6  
     1.7 -lemma msg_induct_aux:
     1.8 -  shows "\<lbrakk>\<And>N. P (Nonce N);
     1.9 -          \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
    1.10 -          \<And>K X. P X \<Longrightarrow> P (Crypt K X);
    1.11 -          \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
    1.12 -  by (lifting freemsg.induct)
    1.13 -
    1.14  lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
    1.15    assumes N: "\<And>N. P (Nonce N)"
    1.16        and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
    1.17        and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
    1.18        and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
    1.19    shows "P msg"
    1.20 -  using N M C D by (rule msg_induct_aux)
    1.21 +  using N M C D 
    1.22 +  by (descending) (auto intro: freemsg.induct)
    1.23 +
    1.24  
    1.25  subsection{*The Abstract Discriminator*}
    1.26