IsaMakefile
authorpaulson
Wed Apr 07 14:25:48 2004 +0200 (2004-04-07)
changeset 14527bc9e5587d05a
parent 14526 51dc6c7b1fd7
child 14528 1457584110ac
IsaMakefile
src/HOL/Induct/Com.thy
src/HOL/Induct/QuoDataType.thy
src/HOL/Induct/ROOT.ML
     1.1 --- a/src/HOL/Induct/Com.thy	Tue Apr 06 16:19:45 2004 +0200
     1.2 +++ b/src/HOL/Induct/Com.thy	Wed Apr 07 14:25:48 2004 +0200
     1.3 @@ -6,6 +6,8 @@
     1.4  Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     1.5  *)
     1.6  
     1.7 +header{*Mutual Induction via Iteratived Inductive Definitions*}
     1.8 +
     1.9  theory Com = Main:
    1.10  
    1.11  typedecl loc
    1.12 @@ -27,6 +29,9 @@
    1.13        | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
    1.14        | While exp com          ("WHILE _ DO _"  60)
    1.15  
    1.16 +
    1.17 +subsection {* Commands *}
    1.18 +
    1.19  text{* Execution of commands *}
    1.20  consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
    1.21         "@exec"  :: "((exp*state) * (nat*state)) set => 
    1.22 @@ -97,7 +102,7 @@
    1.23  done
    1.24  
    1.25  
    1.26 -section {* Expressions *}
    1.27 +subsection {* Expressions *}
    1.28  
    1.29  text{* Evaluation of arithmetic expressions *}
    1.30  consts  eval    :: "((exp*state) * (nat*state)) set"
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Induct/QuoDataType.thy	Wed Apr 07 14:25:48 2004 +0200
     2.3 @@ -0,0 +1,375 @@
     2.4 +(*  Title:      HOL/Induct/QuoDataType
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   2004  University of Cambridge
     2.8 +
     2.9 +*)
    2.10 +
    2.11 +header{*Defining an Initial Algebra by Quotienting a Free Algebra*}
    2.12 +
    2.13 +theory QuoDataType = Main:
    2.14 +
    2.15 +subsection{*Defining the Free Algebra*}
    2.16 +
    2.17 +text{*Messages with encryption and decryption as free constructors.*}
    2.18 +datatype
    2.19 +     freemsg = NONCE  nat
    2.20 +	     | MPAIR  freemsg freemsg
    2.21 +	     | CRYPT  nat freemsg  
    2.22 +	     | DECRYPT  nat freemsg
    2.23 +
    2.24 +text{*The equivalence relation, which makes encryption and decryption inverses
    2.25 +provided the keys are the same.*}
    2.26 +consts  msgrel :: "(freemsg * freemsg) set"
    2.27 +
    2.28 +syntax
    2.29 +  "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "~~" 50)
    2.30 +syntax (xsymbols)
    2.31 +  "_msgrel" :: "[freemsg, freemsg] => bool"  (infixl "\<sim>" 50)
    2.32 +translations
    2.33 +  "X \<sim> Y" == "(X,Y) \<in> msgrel"
    2.34 +
    2.35 +text{*The first two rules are the desired equations. The next four rules
    2.36 +make the equations applicable to subterms. The last two rules are symmetry
    2.37 +and transitivity.*}
    2.38 +inductive "msgrel"
    2.39 +  intros 
    2.40 +    CD:    "CRYPT K (DECRYPT K X) \<sim> X"
    2.41 +    DC:    "DECRYPT K (CRYPT K X) \<sim> X"
    2.42 +    NONCE: "NONCE N \<sim> NONCE N"
    2.43 +    MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
    2.44 +    CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
    2.45 +    DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
    2.46 +    SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
    2.47 +    TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
    2.48 +
    2.49 +
    2.50 +text{*Proving that it is an equivalence relation*}
    2.51 +
    2.52 +lemma msgrel_refl: "X \<sim> X"
    2.53 +by (induct X, (blast intro: msgrel.intros)+)
    2.54 +
    2.55 +theorem equiv_msgrel: "equiv UNIV msgrel"
    2.56 +proof (simp add: equiv_def, intro conjI)
    2.57 +  show "reflexive msgrel" by (simp add: refl_def msgrel_refl)
    2.58 +  show "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM)
    2.59 +  show "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS)
    2.60 +qed
    2.61 +
    2.62 +
    2.63 +subsection{*Some Functions on the Free Algebra*}
    2.64 +
    2.65 +subsubsection{*The Set of Nonces*}
    2.66 +
    2.67 +text{*A function to return the set of nonces present in a message.  It will
    2.68 +be lifted to the initial algrebra, to serve as an example of that process.*}
    2.69 +consts
    2.70 +  freenonces :: "freemsg \<Rightarrow> nat set"
    2.71 +
    2.72 +primrec
    2.73 +   "freenonces (NONCE N) = {N}"
    2.74 +   "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
    2.75 +   "freenonces (CRYPT K X) = freenonces X"
    2.76 +   "freenonces (DECRYPT K X) = freenonces X"
    2.77 +
    2.78 +text{*This theorem lets us prove that the nonces function respects the
    2.79 +equivalence relation.  It also helps us prove that Nonce
    2.80 +  (the abstract constructor) is injective*}
    2.81 +theorem msgrel_imp_eq_freenonces: "U \<sim> V \<Longrightarrow> freenonces U = freenonces V"
    2.82 +by (erule msgrel.induct, auto) 
    2.83 +
    2.84 +
    2.85 +subsubsection{*The Left Projection*}
    2.86 +
    2.87 +text{*A function to return the left part of the top pair in a message.  It will
    2.88 +be lifted to the initial algrebra, to serve as an example of that process.*}
    2.89 +consts free_left :: "freemsg \<Rightarrow> freemsg"
    2.90 +primrec
    2.91 +   "free_left (NONCE N) = NONCE N"
    2.92 +   "free_left (MPAIR X Y) = X"
    2.93 +   "free_left (CRYPT K X) = free_left X"
    2.94 +   "free_left (DECRYPT K X) = free_left X"
    2.95 +
    2.96 +text{*This theorem lets us prove that the left function respects the
    2.97 +equivalence relation.  It also helps us prove that MPair
    2.98 +  (the abstract constructor) is injective*}
    2.99 +theorem msgrel_imp_eqv_free_left:
   2.100 +     "U \<sim> V \<Longrightarrow> free_left U \<sim> free_left V"
   2.101 +by (erule msgrel.induct, auto intro: msgrel.intros)
   2.102 +
   2.103 +
   2.104 +subsubsection{*The Right Projection*}
   2.105 +
   2.106 +text{*A function to return the right part of the top pair in a message.*}
   2.107 +consts free_right :: "freemsg \<Rightarrow> freemsg"
   2.108 +primrec
   2.109 +   "free_right (NONCE N) = NONCE N"
   2.110 +   "free_right (MPAIR X Y) = Y"
   2.111 +   "free_right (CRYPT K X) = free_right X"
   2.112 +   "free_right (DECRYPT K X) = free_right X"
   2.113 +
   2.114 +text{*This theorem lets us prove that the right function respects the
   2.115 +equivalence relation.  It also helps us prove that MPair
   2.116 +  (the abstract constructor) is injective*}
   2.117 +theorem msgrel_imp_eqv_free_right:
   2.118 +     "U \<sim> V \<Longrightarrow> free_right U \<sim> free_right V"
   2.119 +by (erule msgrel.induct, auto intro: msgrel.intros)
   2.120 +
   2.121 +
   2.122 +subsubsection{*The Discriminator for Nonces*}
   2.123 +
   2.124 +text{*A function to identify nonces*}
   2.125 +consts isNONCE :: "freemsg \<Rightarrow> bool"
   2.126 +primrec
   2.127 +   "isNONCE (NONCE N) = True"
   2.128 +   "isNONCE (MPAIR X Y) = False"
   2.129 +   "isNONCE (CRYPT K X) = isNONCE X"
   2.130 +   "isNONCE (DECRYPT K X) = isNONCE X"
   2.131 +
   2.132 +text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
   2.133 +theorem msgrel_imp_eq_isNONCE:
   2.134 +     "U \<sim> V \<Longrightarrow> isNONCE U = isNONCE V"
   2.135 +by (erule msgrel.induct, auto)
   2.136 +
   2.137 +
   2.138 +subsection{*The Initial Algebra: A Quotiented Message Type*}
   2.139 +
   2.140 +typedef (Msg)  msg = "UNIV//msgrel"
   2.141 +    by (auto simp add: quotient_def)
   2.142 +
   2.143 +
   2.144 +text{*The abstract message constructors*}
   2.145 +constdefs
   2.146 +  Nonce :: "nat \<Rightarrow> msg"
   2.147 +  "Nonce N == Abs_Msg(msgrel``{NONCE N})"
   2.148 +
   2.149 +  MPair :: "[msg,msg] \<Rightarrow> msg"
   2.150 +   "MPair X Y ==
   2.151 +       Abs_Msg (\<Union>U \<in> Rep_Msg(X). \<Union>V \<in> Rep_Msg(Y). msgrel``{MPAIR U V})"
   2.152 +
   2.153 +  Crypt :: "[nat,msg] \<Rightarrow> msg"
   2.154 +   "Crypt K X ==
   2.155 +       Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{CRYPT K U})"
   2.156 +
   2.157 +  Decrypt :: "[nat,msg] \<Rightarrow> msg"
   2.158 +   "Decrypt K X ==
   2.159 +       Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{DECRYPT K U})"
   2.160 +
   2.161 +
   2.162 +text{*Reduces equality of equivalence classes to the @{term msgrel} relation:
   2.163 +  @{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)"} *}
   2.164 +lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I]
   2.165 +
   2.166 +declare equiv_msgrel_iff [simp]
   2.167 +
   2.168 +
   2.169 +text{*All equivalence classes belong to set of representatives*}
   2.170 +lemma msgrel_in_integ [simp]: "msgrel``{U} \<in> Msg"
   2.171 +by (auto simp add: Msg_def quotient_def intro: msgrel_refl)
   2.172 +
   2.173 +lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg"
   2.174 +apply (rule inj_on_inverseI)
   2.175 +apply (erule Abs_Msg_inverse)
   2.176 +done
   2.177 +
   2.178 +text{*Reduces equality on abstractions to equality on representatives*}
   2.179 +declare inj_on_Abs_Msg [THEN inj_on_iff, simp]
   2.180 +
   2.181 +declare Abs_Msg_inverse [simp]
   2.182 +
   2.183 +
   2.184 +subsubsection{*Characteristic Equations for the Abstract Constructors*}
   2.185 +
   2.186 +lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) = 
   2.187 +              Abs_Msg (msgrel``{MPAIR U V})"
   2.188 +proof -
   2.189 +  have "congruent2 msgrel (\<lambda>U V. msgrel `` {MPAIR U V})"
   2.190 +    by (simp add: congruent2_def msgrel.MPAIR)
   2.191 +  thus ?thesis
   2.192 +    by (simp add: MPair_def UN_equiv_class2 [OF equiv_msgrel])
   2.193 +qed
   2.194 +
   2.195 +lemma Crypt: "Crypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{CRYPT K U})"
   2.196 +proof -
   2.197 +  have "congruent msgrel (\<lambda>U. msgrel `` {CRYPT K U})"
   2.198 +    by (simp add: congruent_def msgrel.CRYPT)
   2.199 +  thus ?thesis
   2.200 +    by (simp add: Crypt_def UN_equiv_class [OF equiv_msgrel])
   2.201 +qed
   2.202 +
   2.203 +lemma Decrypt:
   2.204 +     "Decrypt K (Abs_Msg(msgrel``{U})) = Abs_Msg (msgrel``{DECRYPT K U})"
   2.205 +proof -
   2.206 +  have "congruent msgrel (\<lambda>U. msgrel `` {DECRYPT K U})"
   2.207 +    by (simp add: congruent_def msgrel.DECRYPT)
   2.208 +  thus ?thesis
   2.209 +    by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
   2.210 +qed
   2.211 +
   2.212 +text{*Case analysis on the representation of a msg as an equivalence class.*}
   2.213 +lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]:
   2.214 +     "(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P"
   2.215 +apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE])
   2.216 +apply (drule arg_cong [where f=Abs_Msg])
   2.217 +apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl)
   2.218 +done
   2.219 +
   2.220 +text{*Establishing these two equations is the point of the whole exercise*}
   2.221 +theorem CD_eq: "Crypt K (Decrypt K X) = X"
   2.222 +by (cases X, simp add: Crypt Decrypt CD)
   2.223 +
   2.224 +theorem DC_eq: "Decrypt K (Crypt K X) = X"
   2.225 +by (cases X, simp add: Crypt Decrypt DC)
   2.226 +
   2.227 +
   2.228 +subsection{*The Abstract Function to Return the Set of Nonces*}
   2.229 +
   2.230 +constdefs
   2.231 +  nonces :: "msg \<Rightarrow> nat set"
   2.232 +   "nonces X == \<Union>U \<in> Rep_Msg(X). freenonces U"
   2.233 +
   2.234 +lemma nonces_congruent: "congruent msgrel (\<lambda>x. freenonces x)"
   2.235 +by (simp add: congruent_def msgrel_imp_eq_freenonces) 
   2.236 +
   2.237 +
   2.238 +text{*Now prove the four equations for @{term nonces}*}
   2.239 +
   2.240 +lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}"
   2.241 +by (simp add: nonces_def Nonce_def 
   2.242 +              UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
   2.243 + 
   2.244 +lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X \<union> nonces Y"
   2.245 +apply (cases X, cases Y) 
   2.246 +apply (simp add: nonces_def MPair 
   2.247 +                 UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
   2.248 +done
   2.249 +
   2.250 +lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X"
   2.251 +apply (cases X) 
   2.252 +apply (simp add: nonces_def Crypt
   2.253 +                 UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
   2.254 +done
   2.255 +
   2.256 +lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
   2.257 +apply (cases X) 
   2.258 +apply (simp add: nonces_def Decrypt
   2.259 +                 UN_equiv_class [OF equiv_msgrel nonces_congruent]) 
   2.260 +done
   2.261 +
   2.262 +
   2.263 +subsection{*The Abstract Function to Return the Left Part*}
   2.264 +
   2.265 +constdefs
   2.266 +  left :: "msg \<Rightarrow> msg"
   2.267 +   "left X == Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{free_left U})"
   2.268 +
   2.269 +lemma left_congruent: "congruent msgrel (\<lambda>U. msgrel `` {free_left U})"
   2.270 +by (simp add: congruent_def msgrel_imp_eqv_free_left) 
   2.271 +
   2.272 +text{*Now prove the four equations for @{term left}*}
   2.273 +
   2.274 +lemma left_Nonce [simp]: "left (Nonce N) = Nonce N"
   2.275 +by (simp add: left_def Nonce_def 
   2.276 +              UN_equiv_class [OF equiv_msgrel left_congruent]) 
   2.277 +
   2.278 +lemma left_MPair [simp]: "left (MPair X Y) = X"
   2.279 +apply (cases X, cases Y) 
   2.280 +apply (simp add: left_def MPair 
   2.281 +                 UN_equiv_class [OF equiv_msgrel left_congruent]) 
   2.282 +done
   2.283 +
   2.284 +lemma left_Crypt [simp]: "left (Crypt K X) = left X"
   2.285 +apply (cases X) 
   2.286 +apply (simp add: left_def Crypt
   2.287 +                 UN_equiv_class [OF equiv_msgrel left_congruent]) 
   2.288 +done
   2.289 +
   2.290 +lemma left_Decrypt [simp]: "left (Decrypt K X) = left X"
   2.291 +apply (cases X) 
   2.292 +apply (simp add: left_def Decrypt
   2.293 +                 UN_equiv_class [OF equiv_msgrel left_congruent]) 
   2.294 +done
   2.295 +
   2.296 +
   2.297 +subsection{*The Abstract Function to Return the Right Part*}
   2.298 +
   2.299 +constdefs
   2.300 +  right :: "msg \<Rightarrow> msg"
   2.301 +   "right X == Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{free_right U})"
   2.302 +
   2.303 +lemma right_congruent: "congruent msgrel (\<lambda>U. msgrel `` {free_right U})"
   2.304 +by (simp add: congruent_def msgrel_imp_eqv_free_right) 
   2.305 +
   2.306 +text{*Now prove the four equations for @{term right}*}
   2.307 +
   2.308 +lemma right_Nonce [simp]: "right (Nonce N) = Nonce N"
   2.309 +by (simp add: right_def Nonce_def 
   2.310 +              UN_equiv_class [OF equiv_msgrel right_congruent]) 
   2.311 +
   2.312 +lemma right_MPair [simp]: "right (MPair X Y) = Y"
   2.313 +apply (cases X, cases Y) 
   2.314 +apply (simp add: right_def MPair 
   2.315 +                 UN_equiv_class [OF equiv_msgrel right_congruent]) 
   2.316 +done
   2.317 +
   2.318 +lemma right_Crypt [simp]: "right (Crypt K X) = right X"
   2.319 +apply (cases X) 
   2.320 +apply (simp add: right_def Crypt
   2.321 +                 UN_equiv_class [OF equiv_msgrel right_congruent]) 
   2.322 +done
   2.323 +
   2.324 +lemma right_Decrypt [simp]: "right (Decrypt K X) = right X"
   2.325 +apply (cases X) 
   2.326 +apply (simp add: right_def Decrypt
   2.327 +                 UN_equiv_class [OF equiv_msgrel right_congruent]) 
   2.328 +done
   2.329 +
   2.330 +
   2.331 +subsection{*Injectivity Properties of Some Constructors*}
   2.332 +
   2.333 +lemma NONCE_imp_eq: "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
   2.334 +by (drule msgrel_imp_eq_freenonces, simp)
   2.335 +
   2.336 +text{*Can also be proved using the function @{term nonces}*}
   2.337 +lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)"
   2.338 +by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)
   2.339 +
   2.340 +lemma MPAIR_imp_eqv_left: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
   2.341 +apply (drule msgrel_imp_eqv_free_left)
   2.342 +apply (simp add: ); 
   2.343 +done
   2.344 +
   2.345 +lemma MPair_imp_eq_left: 
   2.346 +  assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'"
   2.347 +proof -
   2.348 +  from eq
   2.349 +  have "left (MPair X Y) = left (MPair X' Y')" by simp
   2.350 +  thus ?thesis by simp
   2.351 +qed
   2.352 +
   2.353 +lemma MPAIR_imp_eqv_right: "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
   2.354 +apply (drule msgrel_imp_eqv_free_right)
   2.355 +apply (simp add: ); 
   2.356 +done
   2.357 +
   2.358 +lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'" 
   2.359 +apply (cases X, cases X', cases Y, cases Y') 
   2.360 +apply (simp add: MPair)
   2.361 +apply (erule MPAIR_imp_eqv_right)  
   2.362 +done
   2.363 +
   2.364 +theorem MPair_MPair_eq [iff]: "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" 
   2.365 +apply (blast dest: MPair_imp_eq_left MPair_imp_eq_right) 
   2.366 +done
   2.367 +
   2.368 +lemma NONCE_neqv_MPAIR: "NONCE m \<sim> MPAIR X Y \<Longrightarrow> False"
   2.369 +by (drule msgrel_imp_eq_isNONCE, simp)
   2.370 +
   2.371 +theorem Nonce_neq_MPair [iff]: "Nonce N \<noteq> MPair X Y"
   2.372 +apply (cases X, cases Y) 
   2.373 +apply (simp add: Nonce_def MPair) 
   2.374 +apply (blast dest: NONCE_neqv_MPAIR) 
   2.375 +done
   2.376 +
   2.377 +end
   2.378 +
     3.1 --- a/src/HOL/Induct/ROOT.ML	Tue Apr 06 16:19:45 2004 +0200
     3.2 +++ b/src/HOL/Induct/ROOT.ML	Wed Apr 07 14:25:48 2004 +0200
     3.3 @@ -1,5 +1,6 @@
     3.4  
     3.5  time_use_thy "Mutil";
     3.6 +time_use_thy "QuoDataType";
     3.7  time_use_thy "Term";
     3.8  time_use_thy "ABexp";
     3.9  time_use_thy "Tree";