Theory Transformation02
subsection ‹Transforamtion Example 2›
theory
Transformation02
imports
"../../UPF-Firewall"
begin
definition
FWLink :: "adr⇩i⇩p net" where
"FWLink = {{(a,b). a = 1}}"
definition
any :: "adr⇩i⇩p net" where
"any = {{(a,b). a > 5}}"
definition
i4_32:: "adr⇩i⇩p net" where
"i4_32 = {{(a,b). a = 2 }}"
definition
i10_32:: "adr⇩i⇩p net" where
"i10_32 = {{(a,b). a = 3 }}"
definition
eth_intern:: "adr⇩i⇩p net" where
"eth_intern = {{(a,b). a = 4 }}"
definition
eth_private:: "adr⇩i⇩p net" where
"eth_private = {{(a,b). a = 5 }}"
definition
D1a :: "(adr⇩i⇩p net, port) Combinators" where
"D1a = AllowPortFromTo eth_intern any 1 ⊕
AllowPortFromTo eth_intern any 2"
definition
D1b :: "(adr⇩i⇩p net, port) Combinators" where
"D1b = AllowPortFromTo eth_private any 1 ⊕
AllowPortFromTo eth_private any 2"
definition
D2a :: "(adr⇩i⇩p net, port) Combinators" where
"D2a = AllowPortFromTo any i4_32 21"
definition
D2b :: "(adr⇩i⇩p net, port) Combinators" where
"D2b = AllowPortFromTo any i10_32 21 ⊕
AllowPortFromTo any i10_32 43"
definition
Policy :: "(adr⇩i⇩p net, port) Combinators" where
"Policy = DenyAll ⊕ D2b ⊕ D2a ⊕ D1b ⊕ D1a"
lemmas PolicyLemmas = Policy_def D1a_def D1b_def D2a_def D2b_def
lemmas PolicyL = Policy_def
FWLink_def
any_def
i10_32_def
i4_32_def
eth_intern_def
eth_private_def
D1a_def D1b_def D2a_def D2b_def
consts fixID :: id
consts fixContent :: DummyContent
definition "fixElements p = (id p = fixID ∧ content p = fixContent)"
lemmas fixDefs = fixElements_def NetworkCore.id_def NetworkCore.content_def
lemma sets_distinct1: "(n::int) ≠ m ⟹ {(a,b). a = n} ≠ {(a,b). a = m}"
by auto
lemma sets_distinct2: "(m::int) ≠ n ⟹ {(a,b). a = n} ≠ {(a,b). a = m}"
by auto
lemma sets_distinct3: "{((a::int),(b::int)). a = n} ≠ {(a,b). a > n}"
by auto
lemma sets_distinct4: "{((a::int),(b::int)). a > n} ≠ {(a,b). a = n}"
by auto
lemma aux: "⟦a ∈ c; a ∉ d; c = d⟧ ⟹ False"
by auto
lemma sets_distinct5: "(s::int) < g ⟹ {(a::int, b::int). a = s} ≠ {(a::int, b::int). g < a}"
apply (auto simp: sets_distinct3)
apply (subgoal_tac "(s,4) ∈ {(a::int,b::int). a = (s)}")
apply (subgoal_tac "(s,4) ∉ {(a::int,b::int). g < a}")
apply (erule aux)
apply assumption+
apply simp
by blast
lemma sets_distinct6: "(s::int) < g ⟹ {(a::int, b::int). g < a} ≠ {(a::int, b::int). a = s}"
apply (rule not_sym)
apply (rule sets_distinct5)
by simp
lemma distinctNets: "FWLink ≠ any ∧ FWLink ≠ i4_32 ∧ FWLink ≠ i10_32 ∧
FWLink ≠ eth_intern ∧ FWLink ≠ eth_private ∧ any ≠ FWLink ∧ any ≠
i4_32 ∧ any ≠ i10_32 ∧ any ≠ eth_intern ∧ any ≠ eth_private ∧ i4_32 ≠
FWLink ∧ i4_32 ≠ any ∧ i4_32 ≠ i10_32 ∧ i4_32 ≠ eth_intern ∧ i4_32 ≠
eth_private ∧ i10_32 ≠ FWLink ∧ i10_32 ≠ any ∧ i10_32 ≠ i4_32 ∧ i10_32
≠ eth_intern ∧ i10_32 ≠ eth_private ∧ eth_intern ≠ FWLink ∧ eth_intern
≠ any ∧ eth_intern ≠ i4_32 ∧ eth_intern ≠ i10_32 ∧ eth_intern ≠
eth_private ∧ eth_private ≠ FWLink ∧ eth_private ≠ any ∧ eth_private ≠
i4_32 ∧ eth_private ≠ i10_32 ∧ eth_private ≠ eth_intern "
by (simp add: PolicyL sets_distinct1 sets_distinct2 sets_distinct3
sets_distinct4 sets_distinct5 sets_distinct6)
lemma aux5: "⟦x ≠ a; y≠b; (x ≠ y ∧ x ≠ b) ∨ (a ≠ b ∧ a ≠ y)⟧ ⟹ {x,a} ≠ {y,b}"
by auto
lemma aux2: "{a,b} = {b,a}"
by auto
lemma ANDex: "allNetsDistinct (policy2list Policy)"
apply (simp add: PolicyLemmas allNetsDistinct_def distinctNets)
apply (simp add: PolicyL)
by (auto simp: PLemmas PolicyL netsDistinct_def sets_distinct5 sets_distinct6 sets_distinct1
sets_distinct2)
fun (sequential) numberOfRules where
"numberOfRules (a⊕b) = numberOfRules a + numberOfRules b"
|"numberOfRules a = (1::int)"
fun numberOfRulesList where
"numberOfRulesList (x#xs) = ((numberOfRules x)#(numberOfRulesList xs)) "
|"numberOfRulesList [] = []"
lemma all_in_list: "all_in_list (policy2list Policy) (Nets_List Policy)"
apply (simp add: PolicyLemmas)
apply (unfold Nets_List_def)
apply (unfold bothNets_def)
apply (insert distinctNets)
by simp
lemmas normalizeUnfold = normalize_def PolicyL Nets_List_def bothNets_def aux aux2 bothNets_def sets_distinct1 sets_distinct2 sets_distinct3 sets_distinct4 sets_distinct5 sets_distinct6 aux5 aux2
end