# HG changeset patch
# User huffman
# Date 1268264313 28800
# Node ID 29cb504abbb540e824ebcd8f8a4a1b11e93eb1bc
# Parent  fb7a386a15cb3d63c0a7c343ec6955e82bf004aa
convert SET_Protocol to use Nat_Bijection library

diff -r fb7a386a15cb -r 29cb504abbb5 src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Wed Mar 10 15:33:13 2010 -0800
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Wed Mar 10 15:38:33 2010 -0800
@@ -7,7 +7,7 @@
 header{*The Message Theory, Modified for SET*}
 
 theory Message_SET
-imports Main Nat_Int_Bij
+imports Main Nat_Bijection
 begin
 
 subsection{*General Lemmas*}
@@ -81,17 +81,16 @@
 
 
 definition nat_of_agent :: "agent => nat" where
-   "nat_of_agent == agent_case (curry nat2_to_nat 0)
-                               (curry nat2_to_nat 1)
-                               (curry nat2_to_nat 2)
-                               (curry nat2_to_nat 3)
-                               (nat2_to_nat (4,0))"
+   "nat_of_agent == agent_case (curry prod_encode 0)
+                               (curry prod_encode 1)
+                               (curry prod_encode 2)
+                               (curry prod_encode 3)
+                               (prod_encode (4,0))"
     --{*maps each agent to a unique natural number, for specifications*}
 
 text{*The function is indeed injective*}
 lemma inj_nat_of_agent: "inj nat_of_agent"
-by (simp add: nat_of_agent_def inj_on_def curry_def
-              nat2_to_nat_inj [THEN inj_eq]  split: agent.split) 
+by (simp add: nat_of_agent_def inj_on_def curry_def prod_encode_eq split: agent.split) 
 
 
 constdefs
diff -r fb7a386a15cb -r 29cb504abbb5 src/HOL/SET_Protocol/Purchase.thy
--- a/src/HOL/SET_Protocol/Purchase.thy	Wed Mar 10 15:33:13 2010 -0800
+++ b/src/HOL/SET_Protocol/Purchase.thy	Wed Mar 10 15:38:33 2010 -0800
@@ -280,9 +280,9 @@
   inj_PANSecret:   "inj PANSecret"
   CardSecret_neq_PANSecret: "CardSecret k \<noteq> PANSecret k'"
     --{*No CardSecret equals any PANSecret*}
-  apply (rule_tac x="curry nat2_to_nat 0" in exI)
-  apply (rule_tac x="curry nat2_to_nat 1" in exI)
-  apply (simp add: nat2_to_nat_inj [THEN inj_eq] inj_on_def)
+  apply (rule_tac x="curry prod_encode 0" in exI)
+  apply (rule_tac x="curry prod_encode 1" in exI)
+  apply (simp add: prod_encode_eq inj_on_def)
   done
 
 declare Says_imp_knows_Spy [THEN parts.Inj, dest]