# HG changeset patch # User paulson # Date 1081340748 -7200 # Node ID bc9e5587d05a53a57368a7be97569c43b89f45f5 # Parent 51dc6c7b1fd763b422f51ccdc3827d0e1ee74f39 IsaMakefile diff -r 51dc6c7b1fd7 -r bc9e5587d05a src/HOL/Induct/Com.thy --- a/src/HOL/Induct/Com.thy Tue Apr 06 16:19:45 2004 +0200 +++ b/src/HOL/Induct/Com.thy Wed Apr 07 14:25:48 2004 +0200 @@ -6,6 +6,8 @@ Example of Mutual Induction via Iteratived Inductive Definitions: Commands *) +header{*Mutual Induction via Iteratived Inductive Definitions*} + theory Com = Main: typedecl loc @@ -27,6 +29,9 @@ | Cond exp com com ("IF _ THEN _ ELSE _" 60) | While exp com ("WHILE _ DO _" 60) + +subsection {* Commands *} + text{* Execution of commands *} consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set" "@exec" :: "((exp*state) * (nat*state)) set => @@ -97,7 +102,7 @@ done -section {* Expressions *} +subsection {* Expressions *} text{* Evaluation of arithmetic expressions *} consts eval :: "((exp*state) * (nat*state)) set" diff -r 51dc6c7b1fd7 -r bc9e5587d05a src/HOL/Induct/QuoDataType.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Induct/QuoDataType.thy Wed Apr 07 14:25:48 2004 +0200 @@ -0,0 +1,375 @@ +(* Title: HOL/Induct/QuoDataType + ID: $Id$ + 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 = Main: + +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) +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 free_left :: "freemsg \ freemsg" +primrec + "free_left (NONCE N) = NONCE N" + "free_left (MPAIR X Y) = X" + "free_left (CRYPT K X) = free_left X" + "free_left (DECRYPT K X) = free_left 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_free_left: + "U \ V \ free_left U \ free_left 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 free_right :: "freemsg \ freemsg" +primrec + "free_right (NONCE N) = NONCE N" + "free_right (MPAIR X Y) = Y" + "free_right (CRYPT K X) = free_right X" + "free_right (DECRYPT K X) = free_right 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_free_right: + "U \ V \ free_right U \ free_right V" +by (erule msgrel.induct, auto intro: msgrel.intros) + + +subsubsection{*The Discriminator for Nonces*} + +text{*A function to identify nonces*} +consts isNONCE :: "freemsg \ bool" +primrec + "isNONCE (NONCE N) = True" + "isNONCE (MPAIR X Y) = False" + "isNONCE (CRYPT K X) = isNONCE X" + "isNONCE (DECRYPT K X) = isNONCE X" + +text{*This theorem helps us prove @{term "Nonce N \ MPair X Y"}*} +theorem msgrel_imp_eq_isNONCE: + "U \ V \ isNONCE U = isNONCE 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 (\U \ Rep_Msg(X). \V \ Rep_Msg(Y). msgrel``{MPAIR U V})" + + Crypt :: "[nat,msg] \ msg" + "Crypt K X == + Abs_Msg (\U \ Rep_Msg(X). msgrel``{CRYPT K U})" + + Decrypt :: "[nat,msg] \ msg" + "Decrypt K X == + Abs_Msg (\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 msgrel_in_integ [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 "congruent2 msgrel (\U V. msgrel `` {MPAIR U V})" + by (simp add: congruent2_def msgrel.MPAIR) + thus ?thesis + by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel]) +qed + +lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})" +proof - + have "congruent msgrel (\U. msgrel `` {CRYPT K U})" + 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 "congruent msgrel (\U. msgrel `` {DECRYPT K U})" + 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: "Crypt K (Decrypt K X) = X" +by (cases X, simp add: Crypt Decrypt CD) + +theorem DC_eq: "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 == \U \ Rep_Msg(X). freenonces U" + +lemma nonces_congruent: "congruent msgrel (\x. freenonces x)" +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 (\U \ Rep_Msg(X). msgrel``{free_left U})" + +lemma left_congruent: "congruent msgrel (\U. msgrel `` {free_left U})" +by (simp add: congruent_def msgrel_imp_eqv_free_left) + +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 (\U \ Rep_Msg(X). msgrel``{free_right U})" + +lemma right_congruent: "congruent msgrel (\U. msgrel `` {free_right U})" +by (simp add: congruent_def msgrel_imp_eqv_free_right) + +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'" +apply (drule msgrel_imp_eqv_free_left) +apply (simp add: ); +done + +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'" +apply (drule msgrel_imp_eqv_free_right) +apply (simp add: ); +done + +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')" +apply (blast dest: MPair_imp_eq_left MPair_imp_eq_right) +done + +lemma NONCE_neqv_MPAIR: "NONCE m \ MPAIR X Y \ False" +by (drule msgrel_imp_eq_isNONCE, 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 + +end + diff -r 51dc6c7b1fd7 -r bc9e5587d05a src/HOL/Induct/ROOT.ML --- a/src/HOL/Induct/ROOT.ML Tue Apr 06 16:19:45 2004 +0200 +++ b/src/HOL/Induct/ROOT.ML Wed Apr 07 14:25:48 2004 +0200 @@ -1,5 +1,6 @@ time_use_thy "Mutil"; +time_use_thy "QuoDataType"; time_use_thy "Term"; time_use_thy "ABexp"; time_use_thy "Tree";