# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260466121 -3600
# Node ID 1f4dfcd9351b2e74af316c7273c5e4aa4ca81472
# Parent  91b079db738019fdd586a466e8f6d2e1f9b9b918# Parent  ed44eaaea63e19233af3ec9e813fcb621c36855d
merged

diff -r ed44eaaea63e -r 1f4dfcd9351b FIXME-TODO
--- a/FIXME-TODO	Thu Dec 10 14:35:06 2009 +0100
+++ b/FIXME-TODO	Thu Dec 10 18:28:41 2009 +0100
@@ -1,8 +1,10 @@
 Higher Priority
 ===============
 
-- redoing Int.thy (problem at the moment with overloaded
-  definitions....Florian)
+- handling constant definitions is ugly at the moment
+
+- if the constant definition gives the wrong definition
+  term, one gets a cryptic message about get_fun
 
 - have FSet.thy to have a simple infrastructure for 
   finite sets (syntax should be \<lbrace> \<rbrace>,
@@ -16,8 +18,6 @@
   And for examples where it is useful to lift types
   over a relation being only a partial equivalence
 
-
-
 - Handle theorems that include Ball/Bex
 
 - Test theorems with abstractions
diff -r ed44eaaea63e -r 1f4dfcd9351b Quot/Examples/Larry.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/Examples/Larry.thy	Thu Dec 10 18:28:41 2009 +0100
@@ -0,0 +1,387 @@
+theory Larry
+imports Main "../QuotMain"
+begin
+
+subsection{*Defining the Free Algebra*}
+
+datatype
+  freemsg = NONCE  nat
+        | MPAIR  freemsg freemsg
+        | CRYPT  nat freemsg  
+        | DECRYPT  nat freemsg
+
+inductive 
+  msgrel::"freemsg \<Rightarrow> freemsg \<Rightarrow> bool" (infixl "\<sim>" 50)
+where 
+  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: "equivp msgrel"
+proof (rule equivpI)
+  show "reflp msgrel" by (simp add: reflp_def msgrel_refl)
+  show "symp msgrel" by (simp add: symp_def, blast intro: msgrel.SYM)
+  show "transp msgrel" by (simp add: transp_def, blast intro: msgrel.TRANS)
+qed
+
+subsection{*Some Functions on the Free Algebra*}
+
+subsubsection{*The Set of Nonces*}
+
+primrec
+  freenonces :: "freemsg \<Rightarrow> nat set"
+where
+  "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"
+
+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.*}
+fun
+  freeleft :: "freemsg \<Rightarrow> freemsg"
+where
+  "freeleft (NONCE N) = NONCE N"
+| "freeleft (MPAIR X Y) = X"
+| "freeleft (CRYPT K X) = freeleft X"
+| "freeleft (DECRYPT K X) = freeleft 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*}
+lemma msgrel_imp_eqv_freeleft_aux:
+  shows "freeleft U \<sim> freeleft U"
+apply(induct rule: freeleft.induct)
+apply(auto intro: msgrel.intros)
+done
+
+theorem msgrel_imp_eqv_freeleft:
+  "U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V"
+apply(erule msgrel.induct)
+apply(auto intro: msgrel.intros msgrel_imp_eqv_freeleft_aux)
+done
+
+subsubsection{*The Right Projection*}
+
+text{*A function to return the right part of the top pair in a message.*}
+fun
+  freeright :: "freemsg \<Rightarrow> freemsg"
+where
+  "freeright (NONCE N) = NONCE N"
+| "freeright (MPAIR X Y) = Y"
+| "freeright (CRYPT K X) = freeright X"
+| "freeright (DECRYPT K X) = freeright 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*}
+lemma msgrel_imp_eqv_freeright_aux:
+  shows "freeright U \<sim> freeright U"
+apply(induct rule: freeright.induct)
+apply(auto intro: msgrel.intros)
+done
+
+theorem msgrel_imp_eqv_freeright:
+     "U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V"
+by (erule msgrel.induct, auto intro: msgrel.intros msgrel_imp_eqv_freeright_aux)
+
+subsubsection{*The Discriminator for Constructors*}
+
+text{*A function to distinguish nonces, mpairs and encryptions*}
+fun 
+  freediscrim :: "freemsg \<Rightarrow> int"
+where
+   "freediscrim (NONCE N) = 0"
+ | "freediscrim (MPAIR X Y) = 1"
+ | "freediscrim (CRYPT K X) = freediscrim X + 2"
+ | "freediscrim (DECRYPT K X) = freediscrim X - 2"
+
+text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
+theorem msgrel_imp_eq_freediscrim:
+     "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
+by (erule msgrel.induct, auto)
+
+
+subsection{*The Initial Algebra: A Quotiented Message Type*}
+
+quotient  msg = freemsg / msgrel
+  by (rule equiv_msgrel)
+
+text{*The abstract message constructors*}
+
+quotient_def
+  Nonce::"Nonce :: nat \<Rightarrow> msg"
+where
+  "NONCE"
+
+quotient_def
+  MPair::"MPair :: msg \<Rightarrow> msg \<Rightarrow> msg"
+where
+  "MPAIR"
+
+quotient_def
+  Crypt::"Crypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+where
+  "CRYPT"
+
+quotient_def
+  Decrypt::"Decrypt :: nat \<Rightarrow> msg \<Rightarrow> msg"
+where
+  "DECRYPT"
+
+lemma [quot_respect]:
+  shows "(op = ===> op \<sim> ===> op \<sim>) CRYPT CRYPT"
+by (auto intro: CRYPT)
+
+lemma [quot_respect]:
+  shows "(op = ===> op \<sim> ===> op \<sim>) DECRYPT DECRYPT"
+by (auto intro: DECRYPT)
+
+text{*Establishing these two equations is the point of the whole exercise*}
+theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
+by (lifting CD)
+
+theorem DC_eq [simp]: "Decrypt K (Crypt K X) = X"
+by (lifting DC)
+
+subsection{*The Abstract Function to Return the Set of Nonces*}
+
+quotient_def
+  nonces :: "nounces:: msg \<Rightarrow> nat set"
+where
+  "freenonces"
+
+text{*Now prove the four equations for @{term nonces}*}
+
+lemma [quot_respect]:
+  shows "(op \<sim> ===> op =) freenonces freenonces"
+by (simp add: msgrel_imp_eq_freenonces)
+
+lemma [quot_respect]:
+  shows "(op = ===> op \<sim>) NONCE NONCE"
+by (simp add: NONCE)
+
+lemma nonces_Nonce [simp]: 
+  shows "nonces (Nonce N) = {N}"
+by (lifting freenonces.simps(1))
+ 
+lemma [quot_respect]:
+  shows " (op \<sim> ===> op \<sim> ===> op \<sim>) MPAIR MPAIR"
+by (simp add: MPAIR)
+
+lemma nonces_MPair [simp]: 
+  shows "nonces (MPair X Y) = nonces X \<union> nonces Y"
+by (lifting freenonces.simps(2))
+
+lemma nonces_Crypt [simp]: 
+  shows "nonces (Crypt K X) = nonces X"
+by (lifting freenonces.simps(3))
+
+lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X"
+by (lifting freenonces.simps(4))
+
+subsection{*The Abstract Function to Return the Left Part*}
+
+quotient_def
+  left :: "left:: msg \<Rightarrow> msg"
+where
+  "freeleft"
+
+lemma [quot_respect]:
+  shows "(op \<sim> ===> op \<sim>) freeleft freeleft"
+by (simp add: msgrel_imp_eqv_freeleft)
+
+lemma left_Nonce [simp]: 
+  shows "left (Nonce N) = Nonce N"
+by (lifting freeleft.simps(1))
+
+lemma left_MPair [simp]: 
+  shows "left (MPair X Y) = X"
+by (lifting freeleft.simps(2))
+
+lemma left_Crypt [simp]: 
+  shows "left (Crypt K X) = left X"
+by (lifting freeleft.simps(3))
+
+lemma left_Decrypt [simp]: 
+  shows "left (Decrypt K X) = left X"
+by (lifting freeleft.simps(4))
+
+subsection{*The Abstract Function to Return the Right Part*}
+
+quotient_def
+  right :: "right:: msg \<Rightarrow> msg"
+where
+  "freeright"
+
+text{*Now prove the four equations for @{term right}*}
+
+lemma [quot_respect]:
+  shows "(op \<sim> ===> op \<sim>) freeright freeright"
+by (simp add: msgrel_imp_eqv_freeright)
+
+lemma right_Nonce [simp]: 
+  shows "right (Nonce N) = Nonce N"
+by (lifting freeright.simps(1))
+
+lemma right_MPair [simp]: 
+  shows "right (MPair X Y) = Y"
+by (lifting freeright.simps(2))
+
+lemma right_Crypt [simp]: 
+  shows "right (Crypt K X) = right X"
+by (lifting freeright.simps(3))
+
+lemma right_Decrypt [simp]: 
+  shows "right (Decrypt K X) = right X"
+by (lifting freeright.simps(4))
+
+subsection{*Injectivity Properties of Some Constructors*}
+
+lemma NONCE_imp_eq: 
+  shows "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]: 
+  shows "(Nonce m = Nonce n) = (m = n)"
+apply(rule iffI)
+apply(lifting NONCE_imp_eq)
+apply(simp)
+done
+
+lemma MPAIR_imp_eqv_left: 
+  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> X \<sim> X'"
+by (drule msgrel_imp_eqv_freeleft, simp)
+
+lemma MPair_imp_eq_left: 
+  assumes eq: "MPair X Y = MPair X' Y'" 
+  shows "X = X'"
+using eq by (lifting MPAIR_imp_eqv_left)
+
+lemma MPAIR_imp_eqv_right: 
+  shows "MPAIR X Y \<sim> MPAIR X' Y' \<Longrightarrow> Y \<sim> Y'"
+by (drule msgrel_imp_eqv_freeright, simp)
+
+lemma MPair_imp_eq_right: 
+  shows "MPair X Y = MPair X' Y' \<Longrightarrow> Y = Y'"
+by (lifting  MPAIR_imp_eqv_right)
+
+theorem MPair_MPair_eq [iff]: 
+  shows "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" 
+by (blast dest: MPair_imp_eq_left MPair_imp_eq_right)
+
+lemma NONCE_neqv_MPAIR: 
+  shows "\<not>(NONCE m \<sim> MPAIR X Y)"
+by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Nonce_neq_MPair [iff]: 
+  shows "Nonce N \<noteq> MPair X Y"
+by (lifting NONCE_neqv_MPAIR)
+
+text{*Example suggested by a referee*}
+
+lemma CRYPT_NONCE_neq_NONCE:
+  shows "\<not>(CRYPT K (NONCE M) \<sim> NONCE N)"
+by (auto dest: msgrel_imp_eq_freediscrim)
+
+theorem Crypt_Nonce_neq_Nonce: 
+  shows "Crypt K (Nonce M) \<noteq> Nonce N"
+by (lifting CRYPT_NONCE_neq_NONCE)
+
+text{*...and many similar results*}
+lemma CRYPT2_NONCE_neq_NONCE: 
+  shows "\<not>(CRYPT K (CRYPT K' (NONCE M)) \<sim> NONCE N)"
+by (auto dest: msgrel_imp_eq_freediscrim)  
+
+theorem Crypt2_Nonce_neq_Nonce: 
+  shows "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
+by (lifting CRYPT2_NONCE_neq_NONCE) 
+
+theorem Crypt_Crypt_eq [iff]: 
+  shows "(Crypt K X = Crypt K X') = (X=X')" 
+proof
+  assume "Crypt K X = Crypt K X'"
+  hence "Decrypt K (Crypt K X) = Decrypt K (Crypt K X')" by simp
+  thus "X = X'" by simp
+next
+  assume "X = X'"
+  thus "Crypt K X = Crypt K X'" by simp
+qed
+
+theorem Decrypt_Decrypt_eq [iff]: 
+  shows "(Decrypt K X = Decrypt K X') = (X=X')" 
+proof
+  assume "Decrypt K X = Decrypt K X'"
+  hence "Crypt K (Decrypt K X) = Crypt K (Decrypt K X')" by simp
+  thus "X = X'" by simp
+next
+  assume "X = X'"
+  thus "Decrypt K X = Decrypt K X'" by simp
+qed
+
+lemma msg_induct_aux:
+  shows "\<lbrakk>\<And>N. P (Nonce N);
+          \<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y);
+          \<And>K X. P X \<Longrightarrow> P (Crypt K X);
+          \<And>K X. P X \<Longrightarrow> P (Decrypt K X)\<rbrakk> \<Longrightarrow> P msg"
+by (lifting freemsg.induct)
+
+lemma msg_induct [case_names Nonce MPair Crypt Decrypt, cases type: msg]:
+  assumes N: "\<And>N. P (Nonce N)"
+      and M: "\<And>X Y. \<lbrakk>P X; P Y\<rbrakk> \<Longrightarrow> P (MPair X Y)"
+      and C: "\<And>K X. P X \<Longrightarrow> P (Crypt K X)"
+      and D: "\<And>K X. P X \<Longrightarrow> P (Decrypt K X)"
+  shows "P msg"
+using N M C D by (blast intro:  msg_induct_aux)
+
+subsection{*The Abstract Discriminator*}
+
+text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
+need this function in order to prove discrimination theorems.*}
+
+quotient_def
+  discrim :: "discrim:: msg \<Rightarrow> int"
+where
+  "freediscrim"
+
+text{*Now prove the four equations for @{term discrim}*}
+
+lemma [quot_respect]:
+  shows "(op \<sim> ===> op =) freediscrim freediscrim"
+by (auto simp add: msgrel_imp_eq_freediscrim)
+
+lemma discrim_Nonce [simp]: 
+  shows "discrim (Nonce N) = 0"
+by (lifting freediscrim.simps(1))
+
+lemma discrim_MPair [simp]: 
+  shows "discrim (MPair X Y) = 1"
+by (lifting freediscrim.simps(2))
+
+lemma discrim_Crypt [simp]: 
+  shows "discrim (Crypt K X) = discrim X + 2"
+by (lifting freediscrim.simps(3))
+
+lemma discrim_Decrypt [simp]: 
+  shows "discrim (Decrypt K X) = discrim X - 2"
+by (lifting freediscrim.simps(4))
+
+end
+
diff -r ed44eaaea63e -r 1f4dfcd9351b Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Dec 10 14:35:06 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 18:28:41 2009 +0100
@@ -91,6 +91,8 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 
+ML {* print_mapsinfo @{context} *}
+
 declare [[map "fun" = (fun_map, fun_rel)]]
 
 lemmas [quot_thm] = fun_quotient 
@@ -996,18 +998,18 @@
   end)  
 *}
 
-section {* General Shape of the Lifting Procedure *}
+section {* The General Shape of the Lifting Procedure *}
 
-(* - A is the original raw theorem                  *)
-(* - B is the regularized theorem                   *)
-(* - C is the rep/abs injected version of B         *) 
-(* - D is the lifted theorem                        *)
-(*                                                  *)
-(* - b is the regularization step                   *)
-(* - c is the rep/abs injection step                *)
-(* - d is the cleaning part                         *)
-(*                                                  *)
-(* the QUOT_TRUE premise records the lifted theorem *)
+(* - A is the original raw theorem                       *)
+(* - B is the regularized theorem                        *)
+(* - C is the rep/abs injected version of B              *) 
+(* - D is the lifted theorem                             *)
+(*                                                       *)
+(* - b is the regularization step                        *)
+(* - c is the rep/abs injection step                     *)
+(* - d is the cleaning part                              *)
+(*                                                       *)
+(* the QUOT_TRUE premise in c records the lifted theorem *)
 
 lemma lifting_procedure:
   assumes a: "A"
diff -r ed44eaaea63e -r 1f4dfcd9351b Quot/QuotProd.thy
--- a/Quot/QuotProd.thy	Thu Dec 10 14:35:06 2009 +0100
+++ b/Quot/QuotProd.thy	Thu Dec 10 18:28:41 2009 +0100
@@ -26,7 +26,8 @@
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "Quotient (prod_rel R1 R2) (prod_fun Abs1 Abs2) (prod_fun Rep1 Rep2)"
 unfolding Quotient_def
-apply (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q1] Quotient_rel_rep[OF q2])
+using q1 q2
+apply (simp add: Quotient_abs_rep Quotient_abs_rep Quotient_rel_rep Quotient_rel_rep)
 using Quotient_rel[OF q1] Quotient_rel[OF q2] by blast
 
 lemma pair_rsp:
@@ -41,8 +42,6 @@
   shows "(prod_fun Abs1 Abs2) (Rep1 l, Rep2 r) \<equiv> (l, r)"
   by (simp add: Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
-term Pair
-
 lemma pair_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
diff -r ed44eaaea63e -r 1f4dfcd9351b Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Thu Dec 10 14:35:06 2009 +0100
+++ b/Quot/QuotScript.thy	Thu Dec 10 18:28:41 2009 +0100
@@ -31,6 +31,11 @@
   shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"
 by (metis equivp_reflp_symp_transp transp_def)
 
+lemma equivpI:
+  assumes "reflp R" "symp R" "transp R"
+  shows "equivp R"
+using assms by (simp add: equivp_reflp_symp_transp)
+
 definition
   "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
 
diff -r ed44eaaea63e -r 1f4dfcd9351b Quot/ROOT.ML
--- a/Quot/ROOT.ML	Thu Dec 10 14:35:06 2009 +0100
+++ b/Quot/ROOT.ML	Thu Dec 10 18:28:41 2009 +0100
@@ -7,4 +7,5 @@
     "Examples/IntEx",
     "Examples/IntEx2",
     "Examples/LFex",
-    "Examples/LamEx"];
+    "Examples/LamEx",
+    "Examples/Larry"];
diff -r ed44eaaea63e -r 1f4dfcd9351b Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Thu Dec 10 14:35:06 2009 +0100
+++ b/Quot/quotient_info.ML	Thu Dec 10 18:28:41 2009 +0100
@@ -6,14 +6,15 @@
   val maps_lookup: theory -> string -> maps_info option
   val maps_update_thy: string -> maps_info -> theory -> theory    
   val maps_update: string -> maps_info -> Proof.context -> Proof.context     
+  val print_mapsinfo: Proof.context -> unit
 
   type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}
-  val print_quotinfo: Proof.context -> unit
   val quotdata_lookup_thy: theory -> string -> quotient_info option
   val quotdata_lookup: Proof.context -> string -> quotient_info option
   val quotdata_update_thy: string -> (typ * typ * term * thm) -> theory -> theory
   val quotdata_update: string -> (typ * typ * term * thm) -> Proof.context -> Proof.context
   val quotdata_dest: theory -> quotient_info list
+  val print_quotinfo: Proof.context -> unit
 
   type qconsts_info = {qconst: term, rconst: term, def: thm}
   val qconsts_transfer: morphism -> qconsts_info -> qconsts_info
@@ -81,6 +82,25 @@
          (Attrib.setup @{binding "map"} (maps_attr_parser >> maps_attribute) 
            "declaration of map information"))
 
+fun print_mapsinfo ctxt =
+let
+  fun prt_map (ty_name, {mapfun, relfun}) = 
+      Pretty.block (Library.separate (Pretty.brk 2)
+          [Pretty.str "type:", 
+           Pretty.str ty_name,
+           Pretty.str "map fun:", 
+           Pretty.str mapfun,
+           Pretty.str "relation map:", 
+           Pretty.str relfun])
+in
+  MapsData.get (ProofContext.theory_of ctxt)
+  |> Symtab.dest
+  |> map (prt_map)
+  |> Pretty.big_list "maps:" 
+  |> Pretty.writeln
+end
+
+
 
 (* info about quotient types *)
 type quotient_info = {qtyp: typ, rtyp: typ, rel: term, equiv_thm: thm}