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