Checked style.
This commit is contained in:
parent
e0dac8a3ab
commit
61cdc4efcf
19
NAT/NAT.thy
19
NAT/NAT.thy
|
@ -38,7 +38,7 @@
|
|||
subsection{* Network Address Translation *}
|
||||
theory
|
||||
NAT
|
||||
imports
|
||||
imports
|
||||
"../PacketFilter/PacketFilter"
|
||||
begin
|
||||
|
||||
|
@ -91,7 +91,6 @@ definition srcPat2pool_IntProtocol ::
|
|||
"srcPat2pool_IntProtocol srcs transl =
|
||||
{x. (fst (src x)) \<in> srcs} \<triangleleft> (A\<^sub>f (srcPat2poolPort_Protocol_t transl))"
|
||||
|
||||
|
||||
text{*
|
||||
The following lemmas are used for achieving a normalized output format of packages after
|
||||
applying NAT. This is used, e.g., by our firewall execution tool.
|
||||
|
@ -103,7 +102,7 @@ lemma datasimp: "{(i, (s1, s2, s3), aba).
|
|||
= {(i, (s1, s2, s3), aba).
|
||||
i = i1 \<and> s1 = i101 \<and> s3 = iudp \<and> (\<lambda> ((a,aa,b),ba). a = i110 \<and> aa = X606X3 \<and>
|
||||
b = X607X4 \<and> ba = data) aba}"
|
||||
by auto
|
||||
by auto
|
||||
|
||||
lemma datasimp2: "{(i, (s1, s2, s3), aba).
|
||||
\<forall>a aa b ba. aba = ((a, aa, b), ba) \<longrightarrow> i = i1 \<and> s1 = i132 \<and> s3 = iudp \<and>
|
||||
|
@ -111,7 +110,7 @@ lemma datasimp2: "{(i, (s1, s2, s3), aba).
|
|||
= {(i, (s1, s2, s3), aba).
|
||||
i = i1 \<and> s1 = i132 \<and> s3 = iudp \<and> s2 = i1 \<and> (\<lambda> ((a,aa,b),ba). a = i110 \<and>
|
||||
aa = i4 \<and> b = iudp \<and> ba = data) aba}"
|
||||
by auto
|
||||
by auto
|
||||
|
||||
lemma datasimp3: "{(i, (s1, s2, s3), aba).
|
||||
\<forall> a aa b ba. aba = ((a, aa, b), ba) \<longrightarrow> i = i1 \<and> i115 < s1 \<and> s1 < i124 \<and>
|
||||
|
@ -119,7 +118,7 @@ lemma datasimp3: "{(i, (s1, s2, s3), aba).
|
|||
= {(i, (s1, s2, s3), aba).
|
||||
i = i1 \<and> i115 < s1 \<and> s1 < i124 \<and> s3 = iudp \<and> s2 = ii1 \<and>
|
||||
(\<lambda> ((a,aa,b),ba). a = i110 & aa = i3 & b = itcp & ba = data) aba}"
|
||||
by auto
|
||||
by auto
|
||||
|
||||
lemma datasimp4: "{(i, (s1, s2, s3), aba).
|
||||
\<forall>a aa b ba. aba = ((a, aa, b), ba) \<longrightarrow> i = i1 \<and> s1 = i132 \<and> s3 = iudp \<and>
|
||||
|
@ -127,7 +126,7 @@ lemma datasimp4: "{(i, (s1, s2, s3), aba).
|
|||
= {(i, (s1, s2, s3), aba).
|
||||
i = i1 \<and> s1 = i132 \<and> s3 = iudp \<and> s2 = ii1 \<and>
|
||||
(\<lambda> ((a,aa,b),ba). a = i110 \<and> aa = i7 \<and> b = itcp \<and> ba = data) aba}"
|
||||
by auto
|
||||
by auto
|
||||
|
||||
lemma datasimp5: " {(i, (s1, s2, s3), aba).
|
||||
i = i1 \<and> s1 = i101 \<and> s3 = iudp \<and> (\<lambda> ((a,aa,b),ba). a = i110 \<and> aa = X606X3 \<and>
|
||||
|
@ -135,7 +134,7 @@ lemma datasimp5: " {(i, (s1, s2, s3), aba).
|
|||
= {(i, (s1, s2, s3), (a,aa,b),ba).
|
||||
i = i1 \<and> s1 = i101 \<and> s3 = iudp \<and> a = i110 \<and> aa = X606X3 \<and>
|
||||
b = X607X4 \<and> ba = data}"
|
||||
by auto
|
||||
by auto
|
||||
|
||||
lemma datasimp6: "{(i, (s1, s2, s3), aba).
|
||||
i = i1 \<and> s1 = i132 \<and> s3 = iudp \<and> s2 = i1 \<and>
|
||||
|
@ -143,7 +142,7 @@ lemma datasimp6: "{(i, (s1, s2, s3), aba).
|
|||
= {(i, (s1, s2, s3), (a,aa,b),ba).
|
||||
i = i1 \<and> s1 = i132 \<and> s3 = iudp \<and> s2 = i1 \<and> a = i110 \<and>
|
||||
aa = i4 \<and> b = iudp \<and> ba = data}"
|
||||
by auto
|
||||
by auto
|
||||
|
||||
lemma datasimp7: "{(i, (s1, s2, s3), aba).
|
||||
i = i1 \<and> i115 < s1 \<and> s1 < i124 \<and> s3 = iudp \<and> s2 = ii1 \<and>
|
||||
|
@ -151,13 +150,13 @@ lemma datasimp7: "{(i, (s1, s2, s3), aba).
|
|||
= {(i, (s1, s2, s3), (a,aa,b),ba).
|
||||
i = i1 \<and> i115 < s1 \<and> s1 < i124 \<and> s3 = iudp \<and> s2 = ii1
|
||||
\<and> a = i110 \<and> aa = i3 \<and> b = itcp \<and> ba = data}"
|
||||
by auto
|
||||
by auto
|
||||
|
||||
lemma datasimp8: "{(i, (s1, s2, s3), aba). i = i1 \<and> s1 = i132 \<and> s3 = iudp \<and> s2 = ii1 \<and>
|
||||
(\<lambda> ((a,aa,b),ba). a = i110 \<and> aa = i7 \<and> b = itcp \<and> ba = data) aba}
|
||||
= {(i, (s1, s2, s3), (a,aa,b),ba). i = i1 \<and> s1 = i132 \<and> s3 = iudp
|
||||
\<and> s2 = ii1 \<and> a = i110 \<and> aa = i7 \<and> b = itcp \<and> ba = data}"
|
||||
by auto
|
||||
by auto
|
||||
|
||||
lemmas datasimps = datasimp datasimp2 datasimp3 datasimp4
|
||||
datasimp5 datasimp6 datasimp7 datasimp8
|
||||
|
|
Loading…
Reference in New Issue