IsaMakefile

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

--- /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 "\<sim>" 50)
+translations
+  "X \<sim> Y" == "(X,Y) \<in> 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) \<sim> X"
+    DC:    "DECRYPT K (CRYPT K X) \<sim> X"
+    NONCE: "NONCE N \<sim> NONCE N"
+    MPAIR: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> MPAIR X Y \<sim> MPAIR X' Y'"
+    CRYPT: "X \<sim> X' \<Longrightarrow> CRYPT K X \<sim> CRYPT K X'"
+    DECRYPT: "X \<sim> X' \<Longrightarrow> DECRYPT K X \<sim> DECRYPT K X'"
+    SYM:   "X \<sim> Y \<Longrightarrow> Y \<sim> X"
+    TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
+
+
+text{*Proving that it is an equivalence relation*}
+
+lemma msgrel_refl: "X \<sim> 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 \<Rightarrow> nat set"
+
+primrec
+   "freenonces (NONCE N) = {N}"
+   "freenonces (MPAIR X Y) = freenonces X \<union> 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 \<sim> V \<Longrightarrow> 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 \<Rightarrow> 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 \<sim> V \<Longrightarrow> free_left U \<sim> 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 \<Rightarrow> 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 \<sim> V \<Longrightarrow> free_right U \<sim> 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 \<Rightarrow> 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 \<noteq> MPair X Y"}*}
+theorem msgrel_imp_eq_isNONCE:
+     "U \<sim> V \<Longrightarrow> 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 \<Rightarrow> msg"
+  "Nonce N == Abs_Msg(msgrel``{NONCE N})"
+
+  MPair :: "[msg,msg] \<Rightarrow> msg"
+   "MPair X Y ==
+       Abs_Msg (\<Union>U \<in> Rep_Msg(X). \<Union>V \<in> Rep_Msg(Y). msgrel``{MPAIR U V})"
+
+  Crypt :: "[nat,msg] \<Rightarrow> msg"
+   "Crypt K X ==
+       Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{CRYPT K U})"
+
+  Decrypt :: "[nat,msg] \<Rightarrow> msg"
+   "Decrypt K X ==
+       Abs_Msg (\<Union>U \<in> 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) \<in> 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} \<in> 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 (\<lambda>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 (\<lambda>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 (\<lambda>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 \<Rightarrow> nat set"
+   "nonces X == \<Union>U \<in> Rep_Msg(X). freenonces U"
+
+lemma nonces_congruent: "congruent msgrel (\<lambda>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 \<union> 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 \<Rightarrow> msg"
+   "left X == Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{free_left U})"
+
+lemma left_congruent: "congruent msgrel (\<lambda>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 \<Rightarrow> msg"
+   "right X == Abs_Msg (\<Union>U \<in> Rep_Msg(X). msgrel``{free_right U})"
+
+lemma right_congruent: "congruent msgrel (\<lambda>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 \<sim> NONCE n \<Longrightarrow> 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 \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> 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 \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
+apply (drule msgrel_imp_eqv_free_right)
+apply (simp add: ); 
+done
+
+lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \<Longrightarrow> 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 \<sim> MPAIR X Y \<Longrightarrow> False"
+by (drule msgrel_imp_eq_isNONCE, simp)
+
+theorem Nonce_neq_MPair [iff]: "Nonce N \<noteq> MPair X Y"
+apply (cases X, cases Y) 
+apply (simp add: Nonce_def MPair) 
+apply (blast dest: NONCE_neqv_MPAIR) 
+done
+
+end
+

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