Reformatting.
This commit is contained in:
parent
1ab1f96579
commit
ef12bd7397
|
|
@ -36,8 +36,10 @@
|
|||
*****************************************************************************)
|
||||
|
||||
subsection {* Elementary Firewall Policy Transformation Rules *}
|
||||
theory ElementaryRules
|
||||
imports FWNormalisationCore
|
||||
theory
|
||||
ElementaryRules
|
||||
imports
|
||||
FWNormalisationCore
|
||||
begin
|
||||
|
||||
|
||||
|
|
@ -48,29 +50,29 @@ text{*
|
|||
|
||||
lemma elem1:
|
||||
"C (AllowPortFromTo x y p \<oplus> DenyAllFromTo x y) = C (DenyAllFromTo x y)"
|
||||
by (rule ext, auto simp: PLemmas)
|
||||
by (rule ext, auto simp: PLemmas)
|
||||
|
||||
|
||||
lemma elem2:
|
||||
"C ((a \<oplus> b) \<oplus> c) = C (a \<oplus> (b \<oplus> c))"
|
||||
by (simp add: C.simps)
|
||||
by (simp add: C.simps)
|
||||
|
||||
lemma elem3:
|
||||
"C (AllowPortFromTo x y a \<oplus> AllowPortFromTo x y b) =
|
||||
C (AllowPortFromTo x y b \<oplus> AllowPortFromTo x y a)"
|
||||
by (rule ext, auto simp: PLemmas)
|
||||
by (rule ext, auto simp: PLemmas)
|
||||
|
||||
lemma elem4:
|
||||
"C (a \<oplus> DenyAll) = C DenyAll"
|
||||
by (rule ext, auto simp: PLemmas)
|
||||
by (rule ext, auto simp: PLemmas)
|
||||
|
||||
lemma elem5:
|
||||
"C (DenyAllFromTo x y \<oplus> DenyAllFromTo u v) = C (DenyAllFromTo u v \<oplus> DenyAllFromTo x y)"
|
||||
by (rule ext, auto simp: PLemmas)
|
||||
by (rule ext, auto simp: PLemmas)
|
||||
|
||||
|
||||
lemma elem6:
|
||||
"dom (C a) \<inter> dom (C b) = {} \<Longrightarrow> C (a \<oplus> b) = C (b \<oplus> a)"
|
||||
by (rule ext, metis C.simps(4) map_add_comm)
|
||||
by (rule ext, metis C.simps(4) map_add_comm)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -35,8 +35,11 @@
|
|||
*****************************************************************************)
|
||||
|
||||
chapter {* Firewall Policy Normalisation *}
|
||||
theory FWNormalisation
|
||||
imports NormalisationIPPProofs
|
||||
theory
|
||||
FWNormalisation
|
||||
imports
|
||||
NormalisationIPPProofs
|
||||
ElementaryRules
|
||||
begin
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -85,21 +85,23 @@ text{* We define a very simple policy language: *}
|
|||
|
||||
datatype ('\<alpha>,'\<beta>) Combinators =
|
||||
DenyAll
|
||||
| DenyAllFromTo '\<alpha> '\<alpha>
|
||||
| AllowPortFromTo '\<alpha> '\<alpha> '\<beta>
|
||||
| Conc "(('\<alpha>,'\<beta>) Combinators)" "(('\<alpha>,'\<beta>) Combinators)" (infixr "\<oplus>" 80)
|
||||
| DenyAllFromTo '\<alpha> '\<alpha>
|
||||
| AllowPortFromTo '\<alpha> '\<alpha> '\<beta>
|
||||
| Conc "(('\<alpha>,'\<beta>) Combinators)" "(('\<alpha>,'\<beta>) Combinators)" (infixr "\<oplus>" 80)
|
||||
|
||||
text{*
|
||||
And define the semantic interpretation of it. For technical reasons, we fix here the type to
|
||||
policies over IntegerPort addresses. However, we could easily provide definitions for other
|
||||
address types as well, using a generic consts for the type definition and a primitive recursive
|
||||
definition for each desired address model. *}
|
||||
address types as well, using a generic constants for the type definition and a primitive
|
||||
recursive definition for each desired address model.
|
||||
*}
|
||||
|
||||
subsubsection{* Auxiliary definitions and functions. *}
|
||||
text{*
|
||||
This subsubsection defines several functions which are useful later for the combinators, invariants,
|
||||
This section defines several functions which are useful later for the combinators, invariants,
|
||||
and proofs.
|
||||
*}
|
||||
|
||||
fun srcNet where
|
||||
"srcNet (DenyAllFromTo x y) = x"
|
||||
|"srcNet (AllowPortFromTo x y p) = x"
|
||||
|
|
@ -275,8 +277,8 @@ fun NetsCollected2 where
|
|||
subsubsection{* Transformations *}
|
||||
|
||||
text {*
|
||||
The following two functions transform a policy into a list of single rules and vice-versa - by
|
||||
staying on the combinator level.
|
||||
The following two functions transform a policy into a list of single rules and vice-versa (by
|
||||
staying on the combinator level).
|
||||
*}
|
||||
|
||||
fun policy2list::"('\<alpha>, '\<beta>) Combinators \<Rightarrow>
|
||||
|
|
@ -309,7 +311,9 @@ definition removeShadowRules1_alternative where
|
|||
"removeShadowRules1_alternative p =
|
||||
rev (removeShadowRules1_alternative_rev (rev p))"
|
||||
|
||||
text{* Remove all the rules which allow a port, but are shadowed by a deny between these subnets *}
|
||||
text{*
|
||||
Remove all the rules which allow a port, but are shadowed by a deny between these subnets.
|
||||
*}
|
||||
|
||||
fun removeShadowRules2:: "(('\<alpha>, '\<beta>) Combinators) list \<Rightarrow>
|
||||
(('\<alpha>, '\<beta>) Combinators) list"
|
||||
|
|
@ -321,8 +325,10 @@ where
|
|||
| "removeShadowRules2 (x#y) = x#(removeShadowRules2 y)"
|
||||
| "removeShadowRules2 [] = []"
|
||||
|
||||
text{* Sorting a pocliy. We first need to define an ordering on
|
||||
rules. This ordering depends on the $Nets\_List$ of a policy. *}
|
||||
text{*
|
||||
Sorting a policies: We first need to define an ordering on rules. This ordering depends
|
||||
on the $Nets\_List$ of a policy.
|
||||
*}
|
||||
|
||||
fun smaller :: "('\<alpha>, '\<beta>) Combinators \<Rightarrow>
|
||||
('\<alpha>, '\<beta>) Combinators \<Rightarrow>
|
||||
|
|
@ -346,15 +352,10 @@ fun qsort where
|
|||
lemma qsort_permutes:
|
||||
"set (qsort xs l) = set xs"
|
||||
apply (induct xs l rule: qsort.induct)
|
||||
apply (simp_all)
|
||||
apply auto
|
||||
done
|
||||
by (auto)
|
||||
|
||||
lemma set_qsort [simp]: "set (qsort xs l) = set xs"
|
||||
apply (induct xs l rule: qsort.induct)
|
||||
apply (simp_all)
|
||||
apply auto
|
||||
done
|
||||
by (simp add: qsort_permutes)
|
||||
|
||||
fun insort where
|
||||
"insort a [] l = [a]"
|
||||
|
|
@ -364,12 +365,10 @@ fun sort where
|
|||
"sort [] l = []"
|
||||
| "sort (x#xs) l = insort x (sort xs l) l"
|
||||
|
||||
|
||||
|
||||
fun sorted where
|
||||
"sorted [] l \<longleftrightarrow> True" |
|
||||
"sorted [x] l \<longleftrightarrow> True" |
|
||||
"sorted (x#y#zs) l \<longleftrightarrow> smaller x y l \<and> sorted (y#zs) l"
|
||||
"sorted [] l = True"
|
||||
| "sorted [x] l = True"
|
||||
| "sorted (x#y#zs) l = (smaller x y l \<and> sorted (y#zs) l)"
|
||||
|
||||
fun separate where
|
||||
"separate (DenyAll#x) = DenyAll#(separate x)"
|
||||
|
|
@ -379,7 +378,8 @@ fun separate where
|
|||
|"separate x = x"
|
||||
|
||||
text {*
|
||||
Insert the DenyAllFromTo rules, such that traffic between two networks can be tested individually
|
||||
Insert the DenyAllFromTo rules, such that traffic between two networks can be tested
|
||||
individually.
|
||||
*}
|
||||
|
||||
fun insertDenies where
|
||||
|
|
@ -389,11 +389,11 @@ fun insertDenies where
|
|||
(insertDenies xs))"
|
||||
| "insertDenies [] = []"
|
||||
|
||||
text{* Remove duplicate rules. This is especially necessary as
|
||||
insertDenies might have inserted duplicate rules.
|
||||
|
||||
The second function is supposed to work on a list of policies. Only
|
||||
rules which are duplicated within the same policy are removed. *}
|
||||
text{*
|
||||
Remove duplicate rules. This is especially necessary as insertDenies might have inserted
|
||||
duplicate rules. The second function is supposed to work on a list of policies. Only
|
||||
rules which are duplicated within the same policy are removed.
|
||||
*}
|
||||
|
||||
|
||||
fun removeDuplicates where
|
||||
|
|
@ -412,10 +412,8 @@ fun insertDeny where
|
|||
|
||||
|
||||
definition "sort' p l = sort l p"
|
||||
|
||||
definition "qsort' p l = qsort l p"
|
||||
|
||||
|
||||
declare dom_eq_empty_conv [simp del]
|
||||
|
||||
fun list2policyR::"(('\<alpha>, '\<beta>) Combinators) list \<Rightarrow>
|
||||
|
|
@ -425,7 +423,9 @@ fun list2policyR::"(('\<alpha>, '\<beta>) Combinators) list \<Rightarrow>
|
|||
|"list2policyR [] = undefined "
|
||||
|
||||
|
||||
text{* We provide the definitions for two address representations. *}
|
||||
text{*
|
||||
We provide the definitions for two address representations.
|
||||
*}
|
||||
|
||||
|
||||
subsubsection{* IntPort *}
|
||||
|
|
@ -437,9 +437,6 @@ where
|
|||
|"C (AllowPortFromTo x y p) = allow_from_to_port p x y"
|
||||
|"C (x \<oplus> y) = C x ++ C y"
|
||||
|
||||
|
||||
|
||||
|
||||
fun CRotate :: "(adr\<^sub>i\<^sub>p net, port) Combinators \<Rightarrow> (adr\<^sub>i\<^sub>p,DummyContent) packet \<mapsto> unit"
|
||||
where
|
||||
" CRotate DenyAll = C DenyAll"
|
||||
|
|
@ -447,24 +444,20 @@ where
|
|||
|"CRotate (AllowPortFromTo x y p) = C (AllowPortFromTo x y p)"
|
||||
|"CRotate (x \<oplus> y) = ((CRotate y) ++ ((CRotate x)))"
|
||||
|
||||
|
||||
fun rotatePolicy where
|
||||
"rotatePolicy DenyAll = DenyAll"
|
||||
| "rotatePolicy (DenyAllFromTo a b) = DenyAllFromTo a b"
|
||||
| "rotatePolicy (AllowPortFromTo a b p) = AllowPortFromTo a b p"
|
||||
| "rotatePolicy (a\<oplus>b) = (rotatePolicy b) \<oplus> (rotatePolicy a)"
|
||||
|
||||
|
||||
lemma check: "rev (policy2list (rotatePolicy p)) = policy2list p"
|
||||
apply (induct p)
|
||||
apply simp
|
||||
apply simp_all
|
||||
done
|
||||
|
||||
apply (induct p)
|
||||
by (simp_all)
|
||||
|
||||
|
||||
text{*
|
||||
All rules appearing at the left of a DenyAllFromTo, have disjunct domains from it (except DenyAll)
|
||||
All rules appearing at the left of a DenyAllFromTo, have disjunct domains from it
|
||||
(except DenyAll).
|
||||
*}
|
||||
fun (sequential) wellformed_policy2 where
|
||||
"wellformed_policy2 [] = True"
|
||||
|
|
@ -472,8 +465,10 @@ fun (sequential) wellformed_policy2 where
|
|||
| "wellformed_policy2 (x#xs) = ((\<forall> c a b. c = DenyAllFromTo a b \<and> c \<in> set xs \<longrightarrow>
|
||||
Map.dom (C x) \<inter> Map.dom (C c) = {}) \<and> wellformed_policy2 xs)"
|
||||
|
||||
text{* An allow rule is disjunct with all rules appearing at the right of it. This invariant is not
|
||||
necessary as it is a consequence from others, but facilitates some proofs. *}
|
||||
text{*
|
||||
An allow rule is disjunct with all rules appearing at the right of it. This invariant is not
|
||||
necessary as it is a consequence from others, but facilitates some proofs.
|
||||
*}
|
||||
|
||||
fun (sequential) wellformed_policy3::"((adr\<^sub>i\<^sub>p net,port) Combinators) list \<Rightarrow> bool" where
|
||||
"wellformed_policy3 [] = True"
|
||||
|
|
@ -494,7 +489,6 @@ definition
|
|||
(rm_MT_rules C) o insertDeny o removeShadowRules1 o
|
||||
policy2list) p"
|
||||
|
||||
|
||||
definition normalize ::
|
||||
"(adr\<^sub>i\<^sub>p net, port) Combinators \<Rightarrow>
|
||||
(adr\<^sub>i\<^sub>p net, port) Combinators list"
|
||||
|
|
@ -508,9 +502,6 @@ definition
|
|||
(sort (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny
|
||||
(removeShadowRules1 (policy2list p)))))) ((l)))))"
|
||||
|
||||
|
||||
|
||||
|
||||
definition normalizeQ ::
|
||||
"(adr\<^sub>i\<^sub>p net, port) Combinators \<Rightarrow>
|
||||
(adr\<^sub>i\<^sub>p net, port) Combinators list"
|
||||
|
|
@ -524,11 +515,11 @@ definition
|
|||
(qsort (removeShadowRules2 (remdups ((rm_MT_rules C) (insertDeny
|
||||
(removeShadowRules1 (policy2list p)))))) ((l)))))"
|
||||
|
||||
text{* Of course, normalize is equal to normalize', the latter looks nicer though. *}
|
||||
text{*
|
||||
Of course, normalize is equal to normalize', the latter looks nicer though.
|
||||
*}
|
||||
lemma "normalize = normalize'"
|
||||
by (rule ext, simp add: normalize_def normalize'_def sort'_def)
|
||||
|
||||
|
||||
by (rule ext, simp add: normalize_def normalize'_def sort'_def)
|
||||
|
||||
declare C.simps [simp del]
|
||||
|
||||
|
|
@ -552,19 +543,20 @@ where
|
|||
|"Dp (AllowPortFromTo x y p) = Cp (AllowPortFromTo x y p)"
|
||||
|"Dp (x \<oplus> y) = Cp (y \<oplus> x)"
|
||||
|
||||
|
||||
|
||||
|
||||
text{* All rules appearing at the left of a DenyAllFromTo, have disjunct domains from it
|
||||
(except DenyAll) *}
|
||||
text{*
|
||||
All rules appearing at the left of a DenyAllFromTo, have disjunct domains from it
|
||||
(except DenyAll).
|
||||
*}
|
||||
fun (sequential) wellformed_policy2Pr where
|
||||
"wellformed_policy2Pr [] = True"
|
||||
| "wellformed_policy2Pr (DenyAll#xs) = wellformed_policy2Pr xs"
|
||||
| "wellformed_policy2Pr (x#xs) = ((\<forall> c a b. c = DenyAllFromTo a b \<and> c \<in> set xs \<longrightarrow>
|
||||
Map.dom (Cp x) \<inter> Map.dom (Cp c) = {}) \<and> wellformed_policy2Pr xs)"
|
||||
|
||||
text{* An allow rule is disjunct with all rules appearing at the right of it. This invariant is not
|
||||
necessary as it is a consequence from others, but facilitates some proofs. *}
|
||||
text{*
|
||||
An allow rule is disjunct with all rules appearing at the right of it. This invariant is not
|
||||
necessary as it is a consequence from others, but facilitates some proofs.
|
||||
*}
|
||||
|
||||
fun (sequential) wellformed_policy3Pr::"((adr\<^sub>i\<^sub>p\<^sub>p net, protocol \<times> port) Combinators) list \<Rightarrow> bool" where
|
||||
"wellformed_policy3Pr [] = True"
|
||||
|
|
@ -572,9 +564,6 @@ fun (sequential) wellformed_policy3Pr::"((adr\<^sub>i\<^sub>p\<^sub>p net, proto
|
|||
dom (Cp r) \<inter> dom (Cp (AllowPortFromTo a b p)) = {}) \<and> wellformed_policy3Pr xs)"
|
||||
| "wellformed_policy3Pr (x#xs) = wellformed_policy3Pr xs"
|
||||
|
||||
|
||||
|
||||
|
||||
definition
|
||||
normalizePr' :: "(adr\<^sub>i\<^sub>p\<^sub>p net, protocol \<times> port) Combinators
|
||||
\<Rightarrow> (adr\<^sub>i\<^sub>p\<^sub>p net, protocol \<times> port) Combinators list" where
|
||||
|
|
@ -583,7 +572,6 @@ definition
|
|||
(rm_MT_rules Cp) o insertDeny o removeShadowRules1 o
|
||||
policy2list) p"
|
||||
|
||||
|
||||
definition normalizePr ::
|
||||
"(adr\<^sub>i\<^sub>p\<^sub>p net, protocol \<times> port) Combinators
|
||||
\<Rightarrow> (adr\<^sub>i\<^sub>p\<^sub>p net, protocol \<times> port) Combinators list" where
|
||||
|
|
@ -605,7 +593,6 @@ definition
|
|||
(rm_MT_rules Cp) o insertDeny o removeShadowRules1 o
|
||||
policy2list) p"
|
||||
|
||||
|
||||
definition normalizePrQ ::
|
||||
"(adr\<^sub>i\<^sub>p\<^sub>p net, protocol \<times> port) Combinators
|
||||
\<Rightarrow> (adr\<^sub>i\<^sub>p\<^sub>p net, protocol \<times> port) Combinators list" where
|
||||
|
|
@ -618,37 +605,33 @@ definition
|
|||
(qsort (removeShadowRules2 (remdups ((rm_MT_rules Cp) (insertDeny
|
||||
(removeShadowRules1 (policy2list p)))))) ((l)))))"
|
||||
|
||||
|
||||
text{* Of course, normalize is equal to normalize', the latter looks nicer though. *}
|
||||
text{*
|
||||
Of course, normalize is equal to normalize', the latter looks nicer though.
|
||||
*}
|
||||
lemma "normalizePr = normalizePr'"
|
||||
by (rule ext, simp add: normalizePr_def normalizePr'_def sort'_def)
|
||||
by (rule ext, simp add: normalizePr_def normalizePr'_def sort'_def)
|
||||
|
||||
|
||||
text{* The following definition helps in creating the test specification for the individual parts
|
||||
of a normalized policy. *}
|
||||
text{*
|
||||
The following definition helps in creating the test specification for the individual parts
|
||||
of a normalized policy.
|
||||
*}
|
||||
definition makeFUTPr where
|
||||
"makeFUTPr FUT p x n =
|
||||
(packet_Nets x (fst (normBothNets (bothNets p)!n))
|
||||
(snd(normBothNets (bothNets p)!n)) \<longrightarrow>
|
||||
FUT x = Cp ((normalizePr p)!Suc n) x)"
|
||||
|
||||
|
||||
declare Cp.simps [simp del]
|
||||
|
||||
|
||||
lemmas PLemmas = C.simps Cp.simps dom_def PolicyCombinators.PolicyCombinators
|
||||
PortCombinators.PortCombinatorsCore aux
|
||||
ProtocolPortCombinators.ProtocolCombinatorsCore src_def dest_def in_subnet_def
|
||||
adr\<^sub>i\<^sub>p\<^sub>pLemmas adr\<^sub>i\<^sub>p\<^sub>pLemmas
|
||||
|
||||
|
||||
lemma aux: "\<lbrakk>x \<noteq> a; y\<noteq>b; (x \<noteq> y \<and> x \<noteq> b) \<or> (a \<noteq> b \<and> a \<noteq> y)\<rbrakk> \<Longrightarrow> {x,a} \<noteq> {y,b}"
|
||||
by (auto)
|
||||
|
||||
|
||||
|
||||
lemma aux2: "{a,b} = {b,a}"
|
||||
by auto
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -36,31 +36,28 @@
|
|||
*****************************************************************************)
|
||||
|
||||
subsection{* Normalisation Proofs (Generic) *}
|
||||
theory NormalisationGenericProofs
|
||||
theory
|
||||
NormalisationGenericProofs
|
||||
imports
|
||||
FWNormalisationCore
|
||||
begin
|
||||
|
||||
text {* This theory contains the generic proofs of the normalisation
|
||||
procedure, i.e. those which are independent from the concrete
|
||||
semantical interpretation function. *}
|
||||
|
||||
text {*
|
||||
This theory contains the generic proofs of the normalisation procedure, i.e. those which
|
||||
are independent from the concrete semantical interpretation function.
|
||||
*}
|
||||
|
||||
lemma domNMT: "dom X \<noteq> {} \<Longrightarrow> X \<noteq> \<emptyset>"
|
||||
apply auto
|
||||
done
|
||||
by auto
|
||||
|
||||
lemma denyNMT: "deny_all \<noteq> \<emptyset>"
|
||||
apply (rule domNMT)
|
||||
apply (simp add: deny_all_def dom_def)
|
||||
done
|
||||
by (simp add: deny_all_def dom_def)
|
||||
|
||||
|
||||
lemma wellformed_policy1_charn[rule_format] : "wellformed_policy1 p \<longrightarrow>
|
||||
DenyAll \<in> set p \<longrightarrow> (\<exists> p'. p = DenyAll # p' \<and> DenyAll \<notin> set p')"
|
||||
lemma wellformed_policy1_charn[rule_format]:
|
||||
"wellformed_policy1 p \<longrightarrow> DenyAll \<in> set p \<longrightarrow> (\<exists> p'. p = DenyAll # p' \<and> DenyAll \<notin> set p')"
|
||||
by(induct p,simp_all)
|
||||
|
||||
|
||||
lemma singleCombinatorsConc: "singleCombinators (x#xs) \<Longrightarrow> singleCombinators xs"
|
||||
by (case_tac x,simp_all)
|
||||
|
||||
|
|
@ -69,7 +66,6 @@ lemma aux0_0: "singleCombinators x \<Longrightarrow> \<not> (\<exists> a b. (a\<
|
|||
apply (rule allI)+
|
||||
by (case_tac a,simp_all)
|
||||
|
||||
|
||||
lemma aux0_4: "(a \<in> set x \<or> a \<in> set y) = (a \<in> set (x@y))"
|
||||
by auto
|
||||
|
||||
|
|
@ -77,27 +73,22 @@ lemma aux0_1: "\<lbrakk>singleCombinators xs; singleCombinators [x]\<rbrakk> \<L
|
|||
singleCombinators (x#xs)"
|
||||
by (case_tac x,simp_all)
|
||||
|
||||
|
||||
lemma aux0_6: "\<lbrakk>singleCombinators xs; \<not> (\<exists> a b. x = a \<oplus> b)\<rbrakk> \<Longrightarrow>
|
||||
singleCombinators(x#xs)"
|
||||
apply (rule aux0_1,simp_all)
|
||||
apply (case_tac x,simp_all)
|
||||
apply auto
|
||||
done
|
||||
by auto
|
||||
|
||||
lemma aux0_5: " \<not> (\<exists> a b. (a\<oplus>b) \<in> set x) \<Longrightarrow> singleCombinators x"
|
||||
apply (induct x)
|
||||
apply simp_all
|
||||
by (metis aux0_6)
|
||||
|
||||
|
||||
|
||||
lemma ANDConc[rule_format]: "allNetsDistinct (a#p) \<longrightarrow> allNetsDistinct (p)"
|
||||
apply (simp add: allNetsDistinct_def)
|
||||
apply (case_tac "a")
|
||||
by simp_all
|
||||
|
||||
|
||||
lemma aux6: "twoNetsDistinct a1 a2 a b \<Longrightarrow>
|
||||
dom (deny_all_from_to a1 a2) \<inter> dom (deny_all_from_to a b) = {}"
|
||||
by (auto simp: twoNetsDistinct_def netsDistinct_def src_def dest_def
|
||||
|
|
@ -106,7 +97,6 @@ lemma aux6: "twoNetsDistinct a1 a2 a b \<Longrightarrow>
|
|||
lemma aux5[rule_format]: "(DenyAllFromTo a b) \<in> set p \<longrightarrow> a \<in> set (net_list p)"
|
||||
by (rule net_list_aux.induct,simp_all)
|
||||
|
||||
|
||||
lemma aux5a[rule_format]: "(DenyAllFromTo b a) \<in> set p \<longrightarrow> a \<in> set (net_list p)"
|
||||
by (rule net_list_aux.induct,simp_all)
|
||||
|
||||
|
|
@ -121,25 +111,22 @@ lemma aux5d[rule_format]:
|
|||
lemma aux10[rule_format]: "a \<in> set (net_list p) \<longrightarrow> a \<in> set (net_list_aux p)"
|
||||
by simp
|
||||
|
||||
|
||||
lemma srcInNetListaux[simp]: "\<lbrakk>x \<in> set p; singleCombinators[x]; x \<noteq> DenyAll\<rbrakk> \<Longrightarrow>
|
||||
srcNet x \<in> set (net_list_aux p)"
|
||||
lemma srcInNetListaux[simp]:
|
||||
"\<lbrakk>x \<in> set p; singleCombinators[x]; x \<noteq> DenyAll\<rbrakk> \<Longrightarrow> srcNet x \<in> set (net_list_aux p)"
|
||||
apply (induct p)
|
||||
apply simp_all
|
||||
apply (case_tac "x = a", simp_all)
|
||||
apply (case_tac a, simp_all)+
|
||||
done
|
||||
|
||||
|
||||
lemma destInNetListaux[simp]: "\<lbrakk>x \<in> set p; singleCombinators[x]; x \<noteq> DenyAll\<rbrakk> \<Longrightarrow>
|
||||
destNet x \<in> set (net_list_aux p)"
|
||||
lemma destInNetListaux[simp]:
|
||||
"\<lbrakk>x \<in> set p; singleCombinators[x]; x \<noteq> DenyAll\<rbrakk> \<Longrightarrow> destNet x \<in> set (net_list_aux p)"
|
||||
apply (induct p)
|
||||
apply simp_all
|
||||
apply (case_tac "x = a", simp_all)
|
||||
apply (case_tac a, simp_all)+
|
||||
done
|
||||
|
||||
|
||||
lemma tND1: "\<lbrakk>allNetsDistinct p; x \<in> set p; y \<in> set p; a = srcNet x;
|
||||
b = destNet x; c = srcNet y; d = destNet y; a \<noteq> c;
|
||||
singleCombinators[x]; x \<noteq> DenyAll; singleCombinators[y];
|
||||
|
|
@ -189,8 +176,6 @@ lemma aux[rule_format]: "a \<in> set (removeShadowRules2 p) \<longrightarrow> a
|
|||
lemma aux12: "\<lbrakk>a \<in> x; b \<notin> x\<rbrakk> \<Longrightarrow> a \<noteq> b"
|
||||
by auto
|
||||
|
||||
|
||||
|
||||
lemma ND0aux1[rule_format]: "DenyAllFromTo x y \<in> set b \<Longrightarrow>
|
||||
x \<in> set (net_list_aux b)"
|
||||
by (metis aux5 net_list.simps set_remdups)
|
||||
|
|
@ -233,8 +218,7 @@ lemma aNDSubset: "\<lbrakk>singleCombinators a;set a \<subseteq> set b; allNetsD
|
|||
apply (rule allI)+
|
||||
apply (rule impI)+
|
||||
apply (drule_tac x = "aa" in spec, drule_tac x = "ba" in spec)
|
||||
apply (metis subsetD aNDSubsetaux)
|
||||
done
|
||||
using aNDSubsetaux by blast
|
||||
|
||||
lemma aNDSetsEq: "\<lbrakk>singleCombinators a; singleCombinators b; set a = set b;
|
||||
allNetsDistinct b\<rbrakk> \<Longrightarrow> allNetsDistinct a"
|
||||
|
|
@ -242,21 +226,15 @@ lemma aNDSetsEq: "\<lbrakk>singleCombinators a; singleCombinators b; set a = set
|
|||
apply (rule allI)+
|
||||
apply (rule impI)+
|
||||
apply (drule_tac x = "aa" in spec, drule_tac x = "ba" in spec)
|
||||
apply (metis aNDSetsEqaux )
|
||||
done
|
||||
using aNDSetsEqaux by auto
|
||||
|
||||
lemma SCConca: "\<lbrakk>singleCombinators p; singleCombinators [a]\<rbrakk> \<Longrightarrow>
|
||||
singleCombinators (a#p)"
|
||||
by (case_tac "a",simp_all)
|
||||
by(metis aux0_1)
|
||||
|
||||
lemma aux3[simp]: "\<lbrakk>singleCombinators p; singleCombinators [a];
|
||||
allNetsDistinct (a#p)\<rbrakk> \<Longrightarrow> allNetsDistinct (a#a#p)"
|
||||
apply (insert aNDSubset[of "(a#a#p)" "(a#p)"])
|
||||
by (simp add: SCConca)
|
||||
|
||||
|
||||
|
||||
|
||||
by (metis aNDSetsEq aux0_1 insert_absorb2 list.set(2))
|
||||
|
||||
lemma wp1_aux1a[rule_format]: "xs \<noteq> [] \<longrightarrow> wellformed_policy1_strong (xs @ [x]) \<longrightarrow>
|
||||
wellformed_policy1_strong xs"
|
||||
|
|
@ -307,10 +285,9 @@ lemma waux3[rule_format]: "\<lbrakk>x \<noteq> a; x \<notin> set p\<rbrakk> \<L
|
|||
by (metis aux79)
|
||||
|
||||
lemma wellformed1_sorted_aux[rule_format]: "wellformed_policy1 (x#p) \<Longrightarrow>
|
||||
wellformed_policy1 (insort x p l)"
|
||||
apply (case_tac x,simp_all)
|
||||
by (rule waux2,rule waux3, simp_all)+
|
||||
|
||||
wellformed_policy1 (insort x p l)" try
|
||||
by (metis NormalisationGenericProofs.set_insort list.set(2) saux waux2 wellformed_eq
|
||||
wellformed_policy1_strong.simps(2))
|
||||
|
||||
lemma wellformed1_sorted_auxQ[rule_format]: "wellformed_policy1 (p) \<Longrightarrow>
|
||||
wellformed_policy1 (qsort p l)"
|
||||
|
|
@ -323,9 +300,6 @@ next
|
|||
by (metis Combinators.simps append_Cons append_Nil qsort.simps(2) set_ConsD set_qsort waux2)+
|
||||
qed
|
||||
|
||||
|
||||
|
||||
|
||||
lemma SR1Subset: "set (removeShadowRules1 p) \<subseteq> set p"
|
||||
apply (induct_tac p, simp_all)
|
||||
apply (case_tac a, simp_all)
|
||||
|
|
@ -363,7 +337,6 @@ lemma denyAllDom[simp]: "x \<in> dom (deny_all)"
|
|||
lemma lCdom2: "(list2FWpolicy (a @ (b @ c))) = (list2FWpolicy ((a@b)@c))"
|
||||
by auto
|
||||
|
||||
|
||||
lemma SCConcEnd: "singleCombinators (xs @ [xa]) \<Longrightarrow> singleCombinators xs"
|
||||
by (induct "xs", simp_all, case_tac a, simp_all)
|
||||
|
||||
|
|
@ -371,7 +344,6 @@ lemma list2FWpolicyconc[rule_format]: "a \<noteq> [] \<longrightarrow>
|
|||
(list2FWpolicy (xa # a)) = (xa) \<oplus> (list2FWpolicy a)"
|
||||
by (induct a,simp_all)
|
||||
|
||||
|
||||
lemma wp1n_tl [rule_format]: "wellformed_policy1_strong p \<longrightarrow>
|
||||
p = (DenyAll#(tl p))"
|
||||
by (induct p, simp_all)
|
||||
|
|
@ -424,7 +396,6 @@ lemma domInterMT[rule_format]: "\<lbrakk>dom a \<inter> dom b = {}; x \<in> dom
|
|||
lemma domComm: "dom a \<inter> dom b = dom b \<inter> dom a"
|
||||
by auto
|
||||
|
||||
|
||||
lemma r_not_DA_in_tl[rule_format]:
|
||||
"wellformed_policy1_strong p \<longrightarrow> a \<in> set p\<longrightarrow> a \<noteq> DenyAll \<longrightarrow> a \<in> set (tl p)"
|
||||
by (induct p,simp_all)
|
||||
|
|
@ -442,8 +413,6 @@ lemma l2p_aux[rule_format]: "list \<noteq> [] \<longrightarrow>
|
|||
lemma l2p_aux2[rule_format]: "list = [] \<Longrightarrow> list2FWpolicy (a # list) = a"
|
||||
by simp
|
||||
|
||||
|
||||
|
||||
lemma aux7aa:
|
||||
assumes 1 : "AllowPortFromTo a b poo \<in> set p"
|
||||
and 2 : "allNetsDistinct ((AllowPortFromTo c d po) # p)"
|
||||
|
|
@ -459,10 +428,9 @@ next
|
|||
list.set_intros(2) twoNetsDistinct_def)
|
||||
qed
|
||||
|
||||
|
||||
lemma ANDConcEnd: "\<lbrakk> allNetsDistinct (xs @ [xa]); singleCombinators xs\<rbrakk> \<Longrightarrow>
|
||||
allNetsDistinct xs"
|
||||
by (rule aNDSubset) auto
|
||||
by (rule aNDSubset, auto)
|
||||
|
||||
lemma WP1ConcEnd[rule_format]:
|
||||
"wellformed_policy1 (xs@[xa]) \<longrightarrow> wellformed_policy1 xs"
|
||||
|
|
@ -505,21 +473,15 @@ next
|
|||
qed
|
||||
qed
|
||||
|
||||
|
||||
|
||||
|
||||
lemma SC1[simp]: "singleCombinators p \<Longrightarrow>singleCombinators (removeShadowRules1 p)"
|
||||
by (erule SCSubset) (rule SR1Subset)
|
||||
|
||||
lemma SC2[simp]: "singleCombinators p \<Longrightarrow>singleCombinators (removeShadowRules2 p)"
|
||||
by (erule SCSubset) (rule RS2Set)
|
||||
|
||||
|
||||
lemma SC3[simp]: "singleCombinators p \<Longrightarrow> singleCombinators (sort p l)"
|
||||
by (erule SCSubset) simp
|
||||
|
||||
|
||||
|
||||
lemma SC3Q[simp]: "singleCombinators p \<Longrightarrow> singleCombinators (qsort p l)"
|
||||
by (erule SCSubset) simp
|
||||
|
||||
|
|
@ -549,8 +511,6 @@ lemma aND_sortQ[simp]: "\<lbrakk>singleCombinators p; allNetsDistinct p\<rbrakk>
|
|||
apply (rule aNDSubset)
|
||||
by (erule SC3Q, simp_all)
|
||||
|
||||
|
||||
|
||||
lemma inRS2[rule_format,simp]: "x \<notin> set p \<longrightarrow> x \<notin> set (removeShadowRules2 p)"
|
||||
apply (insert RS2Set [of p])
|
||||
by blast
|
||||
|
|
@ -715,8 +675,6 @@ lemma sorted_ConsA:"\<lbrakk>all_in_list (x#xs) l; singleCombinators (x#xs)\<rbr
|
|||
lemma is_in_insort: "y \<in> set xs \<Longrightarrow> y \<in> set (insort x xs l)"
|
||||
by (simp add: NormalisationGenericProofs.set_insort)
|
||||
|
||||
|
||||
|
||||
lemma sorted_insorta[rule_format]:
|
||||
assumes 1 : "sorted (insort x xs l) l"
|
||||
and 2 : "all_in_list (x#xs) l"
|
||||
|
|
@ -732,7 +690,7 @@ next
|
|||
then show ?case
|
||||
apply simp
|
||||
apply (auto intro: is_in_insort sorted_ConsA set_insort singleCombinators_insort
|
||||
singleCombinatorsConc sortedConcEnd all_in_list_insort)
|
||||
singleCombinatorsConc sortedConcEnd all_in_list_insort) [1]
|
||||
apply(cases "smaller x a l", simp_all)
|
||||
by (metis NormalisationGenericProofs.set_insort NormalisationGenericProofs.sorted_Cons
|
||||
all_in_list.simps(2) all_in_list_insort aux0_1 insert_iff singleCombinatorsConc
|
||||
|
|
@ -750,11 +708,11 @@ next
|
|||
have * : "sorted (a # xs) l \<Longrightarrow> all_in_list (x # a # xs) l \<Longrightarrow>
|
||||
distinct (x # a # xs) \<Longrightarrow> singleCombinators [x] \<Longrightarrow>
|
||||
singleCombinators (a # xs) \<Longrightarrow> sorted (insort x xs l) l"
|
||||
apply(insert Cons.hyps)apply simp_all
|
||||
apply (metis sorted_Cons all_in_list.simps(2) singleCombinatorsConc)
|
||||
apply(insert Cons.hyps, simp_all)
|
||||
apply(metis sorted_Cons all_in_list.simps(2) singleCombinatorsConc)
|
||||
done
|
||||
show ?case
|
||||
apply(insert Cons.hyps)
|
||||
apply (insert Cons.hyps)
|
||||
apply (rule impI)+
|
||||
apply (insert *, auto intro!: sorted_Consb)
|
||||
proof (rule_tac b = "x#xs" in all_in_listSubset)
|
||||
|
|
@ -789,7 +747,6 @@ next
|
|||
qed
|
||||
qed
|
||||
|
||||
|
||||
lemma sorted_insort:
|
||||
"\<lbrakk>all_in_list (x#xs) l; distinct(x#xs); singleCombinators [x];
|
||||
singleCombinators xs\<rbrakk> \<Longrightarrow>
|
||||
|
|
@ -806,52 +763,42 @@ lemma distinct_sort[simp]: "distinct (sort xs l) = distinct xs"
|
|||
lemma sort_is_sorted[rule_format]:
|
||||
"all_in_list p l \<longrightarrow> distinct p \<longrightarrow> singleCombinators p \<longrightarrow> sorted (sort p l) l"
|
||||
apply (induct p)
|
||||
apply (auto intro: SC3 all_in_listSubset singleCombinatorsConc sorted_insort)
|
||||
apply (subst sorted_insort)
|
||||
apply (auto intro: singleCombinatorsConc all_in_listSubset SC3)
|
||||
apply (erule all_in_listSubset)
|
||||
by (auto intro: SC3 singleCombinatorsConc sorted_insort)
|
||||
|
||||
|
||||
|
||||
apply simp
|
||||
by (metis (no_types, lifting) NormalisationGenericProofs.distinct_sort
|
||||
NormalisationGenericProofs.set_sort SC3 all_in_list.simps(2) all_in_listSubset
|
||||
distinct.simps(2) set_subset_Cons singleCombinatorsConc singleCombinatorsStart
|
||||
sort.simps(2) sorted_insortb)
|
||||
|
||||
lemma smaller_sym[rule_format]: "all_in_list [a] l \<longrightarrow> smaller a a l"
|
||||
by (case_tac a,simp_all)
|
||||
|
||||
|
||||
lemma SC_sublist[rule_format]:
|
||||
"singleCombinators xs \<Longrightarrow> singleCombinators (qsort [y\<leftarrow>xs. P y] l)"
|
||||
by (auto intro: SCSubset)
|
||||
|
||||
|
||||
lemma all_in_list_sublist[rule_format]:
|
||||
"singleCombinators xs \<longrightarrow> all_in_list xs l \<longrightarrow> all_in_list (qsort [y\<leftarrow>xs. P y] l) l"
|
||||
by (auto intro: all_in_listSubset SC_sublist)
|
||||
|
||||
|
||||
lemma SC_sublist2[rule_format]:
|
||||
"singleCombinators xs \<longrightarrow> singleCombinators ([y\<leftarrow>xs. P y])"
|
||||
by (auto intro: SCSubset)
|
||||
|
||||
|
||||
lemma all_in_list_sublist2[rule_format]:
|
||||
"singleCombinators xs \<longrightarrow> all_in_list xs l \<longrightarrow> all_in_list ( [y\<leftarrow>xs. P y]) l"
|
||||
by (auto intro: all_in_listSubset SC_sublist2)
|
||||
|
||||
|
||||
lemma all_in_listAppend[rule_format]:
|
||||
"all_in_list (xs) l \<longrightarrow> all_in_list (ys) l \<longrightarrow> all_in_list (xs @ ys) l"
|
||||
by (induct xs) simp_all
|
||||
|
||||
|
||||
|
||||
lemma distinct_sortQ[rule_format]:
|
||||
"singleCombinators xs \<longrightarrow> all_in_list xs l \<longrightarrow> distinct xs \<longrightarrow> distinct (qsort xs l)"
|
||||
apply (induct xs l rule: qsort.induct)
|
||||
apply simp
|
||||
apply (auto simp: SC_sublist2 singleCombinatorsConc all_in_list_sublist2)
|
||||
done
|
||||
|
||||
|
||||
lemma singleCombinatorsAppend[rule_format]:
|
||||
"singleCombinators (xs) \<longrightarrow> singleCombinators (ys) \<longrightarrow> singleCombinators (xs @ ys)"
|
||||
apply (induct xs, auto)
|
||||
|
|
@ -889,9 +836,6 @@ lemma sorted_append[rule_format]:
|
|||
apply (rule sorted_append2,simp_all)
|
||||
done
|
||||
|
||||
|
||||
|
||||
|
||||
lemma sort_is_sortedQ[rule_format]:
|
||||
"all_in_list p l \<longrightarrow> singleCombinators p \<longrightarrow> sorted (qsort p l) l"
|
||||
proof (induct p l rule: qsort.induct) print_cases
|
||||
|
|
@ -941,7 +885,7 @@ next
|
|||
FWNormalisationCore.sorted (x # qsort [y\<leftarrow>xs . smaller x y l] l) l \<and>
|
||||
(\<forall>x'\<in>set (qsort [y\<leftarrow>xs . \<not> smaller x y l] l).
|
||||
\<forall>y\<in>set (x # qsort [y\<leftarrow>xs . smaller x y l] l). smaller x' y l)"
|
||||
apply auto
|
||||
apply(auto)[1]
|
||||
apply (metis (mono_tags, lifting) SC_sublist all_in_list.simps(2)
|
||||
all_in_list_sublist aux0_1 mem_Collect_eq set_filter set_qsort
|
||||
singleCombinatorsConc singleCombinatorsStart sorted_Consb)
|
||||
|
|
@ -974,7 +918,6 @@ lemma RS1n_nMT[rule_format,simp]: "p \<noteq> []\<longrightarrow> removeShadowRu
|
|||
lemma RS1N_DA[simp]: "removeShadowRules1_alternative (a@[DenyAll]) = [DenyAll]"
|
||||
by (simp add: removeShadowRules1_alternative_def)
|
||||
|
||||
|
||||
lemma WP1n_DA_notinSet[rule_format]: "wellformed_policy1_strong p \<longrightarrow>
|
||||
DenyAll \<notin> set (tl p)"
|
||||
by (induct p) (simp_all)
|
||||
|
|
@ -991,11 +934,9 @@ lemma AND_tl[rule_format]: "allNetsDistinct ( p) \<longrightarrow> allNetsDistin
|
|||
apply (induct p, simp_all)
|
||||
by (auto intro: ANDConc)
|
||||
|
||||
|
||||
lemma distinct_tl[rule_format]: "distinct p \<longrightarrow> distinct (tl p)"
|
||||
by (induct p, simp_all)
|
||||
|
||||
|
||||
lemma SC_tl[rule_format]: "singleCombinators ( p) \<longrightarrow> singleCombinators (tl p)"
|
||||
by (induct p, simp_all) (auto intro: singleCombinatorsConc)
|
||||
|
||||
|
|
@ -1006,7 +947,6 @@ lemma wp1_tl[rule_format]:
|
|||
"p \<noteq> [] \<and> wellformed_policy1 p \<longrightarrow> wellformed_policy1 (tl p)"
|
||||
by (induct p) (auto intro: waux2)
|
||||
|
||||
|
||||
lemma wp1_eq[rule_format]:
|
||||
"wellformed_policy1_strong p \<Longrightarrow> wellformed_policy1 p"
|
||||
apply (case_tac "DenyAll \<in> set p")
|
||||
|
|
@ -1014,13 +954,10 @@ lemma wp1_eq[rule_format]:
|
|||
apply (auto elim: waux2)
|
||||
done
|
||||
|
||||
|
||||
lemma wellformed1_alternative_sorted:
|
||||
"wellformed_policy1_strong p \<Longrightarrow> wellformed_policy1_strong (sort p l)"
|
||||
by (case_tac "p", simp_all)
|
||||
|
||||
|
||||
|
||||
lemma wp1n_RS2[rule_format]:
|
||||
"wellformed_policy1_strong p \<longrightarrow> wellformed_policy1_strong (removeShadowRules2 p)"
|
||||
by (induct p, simp_all)
|
||||
|
|
@ -1031,7 +968,6 @@ lemma RS2_NMT[rule_format]: "p \<noteq> [] \<longrightarrow> removeShadowRules2
|
|||
apply (case_tac "a", simp_all)+
|
||||
done
|
||||
|
||||
|
||||
lemma wp1_alternative_not_mt[simp]: "wellformed_policy1_strong p \<Longrightarrow> p \<noteq> []"
|
||||
by auto
|
||||
|
||||
|
|
@ -1039,8 +975,6 @@ lemma AIL1[rule_format,simp]: "all_in_list p l \<longrightarrow>
|
|||
all_in_list (removeShadowRules1 p) l"
|
||||
by (induct_tac p, simp_all)
|
||||
|
||||
|
||||
|
||||
lemma wp1ID: "wellformed_policy1_strong (insertDeny (removeShadowRules1 p))"
|
||||
by (induct p, simp_all, case_tac a, simp_all)
|
||||
|
||||
|
|
@ -1050,7 +984,6 @@ lemma dRD[simp]: "distinct (remdups p)"
|
|||
lemma AILrd[rule_format,simp]: "all_in_list p l \<longrightarrow> all_in_list (remdups p) l"
|
||||
by (induct p, simp_all)
|
||||
|
||||
|
||||
lemma AILiD[rule_format,simp]: "all_in_list p l \<longrightarrow> all_in_list (insertDeny p) l"
|
||||
apply (induct p, simp_all)
|
||||
apply (rule impI, simp)
|
||||
|
|
@ -1069,7 +1002,6 @@ lemma SCRiD[rule_format,simp]: "singleCombinators p \<longrightarrow>
|
|||
apply (case_tac "a", simp_all)
|
||||
done
|
||||
|
||||
|
||||
lemma WP1rd[rule_format,simp]:
|
||||
"wellformed_policy1_strong p \<longrightarrow> wellformed_policy1_strong (remdups p)"
|
||||
by (induct p, simp_all)
|
||||
|
|
@ -1089,7 +1021,6 @@ lemma ANDiD[rule_format,simp]:
|
|||
apply (case_tac "a",simp_all add: allNetsDistinct_def)
|
||||
done
|
||||
|
||||
|
||||
lemma mr_iD[rule_format]:
|
||||
"wellformed_policy1_strong p \<longrightarrow> matching_rule x p = matching_rule x (insertDeny p)"
|
||||
by (induct p, simp_all)
|
||||
|
|
@ -1098,7 +1029,6 @@ lemma WP1iD[rule_format,simp]: "wellformed_policy1_strong p \<longrightarrow>
|
|||
wellformed_policy1_strong (insertDeny p)"
|
||||
by (induct p, simp_all)
|
||||
|
||||
|
||||
lemma DAiniD: "DenyAll \<in> set (insertDeny p)"
|
||||
by (induct p, simp_all, case_tac a, simp_all)
|
||||
|
||||
|
|
@ -1109,7 +1039,6 @@ lemma AIL2[rule_format,simp]:
|
|||
"all_in_list p l \<longrightarrow> all_in_list (removeShadowRules2 p) l"
|
||||
by (induct_tac p, simp_all, case_tac a, simp_all)
|
||||
|
||||
|
||||
lemma SCConc: "singleCombinators x \<Longrightarrow> singleCombinators y \<Longrightarrow> singleCombinators (x@y)"
|
||||
apply (rule aux0_5)
|
||||
apply (metis aux0_0 aux0_4)
|
||||
|
|
@ -1118,7 +1047,6 @@ lemma SCConc: "singleCombinators x \<Longrightarrow> singleCombinators y \<Long
|
|||
lemma SCp2l: "singleCombinators (policy2list p)"
|
||||
by (induct_tac p) (auto intro: SCConc)
|
||||
|
||||
|
||||
lemma subnetAux: "Dd \<inter> A \<noteq> {} \<Longrightarrow> A \<subseteq> B \<Longrightarrow> Dd \<inter> B \<noteq> {}"
|
||||
by auto
|
||||
|
||||
|
|
@ -1126,8 +1054,7 @@ lemma soadisj: "x \<in> subnetsOfAdr a \<Longrightarrow> y \<in> subnetsOfAdr a
|
|||
by(simp add: subnetsOfAdr_def netsDistinct_def,auto)
|
||||
|
||||
lemma not_member: "\<not> member a (x\<oplus>y) \<Longrightarrow> \<not> member a x"
|
||||
apply auto
|
||||
done
|
||||
by auto
|
||||
|
||||
lemma soadisj2: "(\<forall> a x y. x \<in> subnetsOfAdr a \<and> y \<in> subnetsOfAdr a \<longrightarrow> \<not> netsDistinct x y)"
|
||||
by (simp add: subnetsOfAdr_def netsDistinct_def, auto)
|
||||
|
|
@ -1139,14 +1066,12 @@ lemma ndFalse1:
|
|||
apply (auto simp: soadisj)
|
||||
using soadisj2 by blast
|
||||
|
||||
|
||||
lemma ndFalse2: "(\<forall>a b c d. (a,b)\<in>A \<and> (c,d)\<in>B \<longrightarrow> netsDistinct b d) \<Longrightarrow>
|
||||
\<exists>(a, b)\<in>A. b \<in> subnetsOfAdr D \<Longrightarrow>
|
||||
\<exists>(a, b)\<in>B. b \<in> subnetsOfAdr D \<Longrightarrow> False"
|
||||
apply (auto simp: soadisj)
|
||||
using soadisj2 by blast
|
||||
|
||||
|
||||
lemma tndFalse: "(\<forall>a b c d. (a,b)\<in>A \<and> (c,d)\<in>B \<longrightarrow> twoNetsDistinct a b c d) \<Longrightarrow>
|
||||
\<exists>(a, b)\<in>A. a \<in> subnetsOfAdr (D::('a::adr)) \<and> b \<in> subnetsOfAdr (F::'a) \<Longrightarrow>
|
||||
\<exists>(a, b)\<in>B. a \<in> subnetsOfAdr D\<and> b\<in> subnetsOfAdr F
|
||||
|
|
@ -1162,7 +1087,6 @@ lemma sepnMT[rule_format]: "p \<noteq> [] \<longrightarrow> (separate p) \<noteq
|
|||
lemma sepDA[rule_format]: "DenyAll \<notin> set p \<longrightarrow> DenyAll \<notin> set (separate p)"
|
||||
by (induct p rule: separate.induct) simp_all
|
||||
|
||||
|
||||
lemma setnMT: "set a = set b \<Longrightarrow> a \<noteq> [] \<Longrightarrow> b \<noteq> []"
|
||||
by auto
|
||||
|
||||
|
|
@ -1185,7 +1109,6 @@ lemma OTNoTN[rule_format]: " OnlyTwoNets p \<longrightarrow> x \<noteq> DenyAll
|
|||
lemma first_isIn[rule_format]: "\<not> member DenyAll x \<longrightarrow> (first_srcNet x,first_destNet x) \<in> sdnets x"
|
||||
by (induct x,case_tac x, simp_all)
|
||||
|
||||
|
||||
lemma sdnets2:
|
||||
"\<exists>a b. sdnets x = {(a, b), (b, a)} \<Longrightarrow> \<not> member DenyAll x \<Longrightarrow>
|
||||
sdnets x = {(first_srcNet x, first_destNet x), (first_destNet x, first_srcNet x)}"
|
||||
|
|
@ -1193,7 +1116,6 @@ proof -
|
|||
have * : "\<exists>a b. sdnets x = {(a, b), (b, a)} \<Longrightarrow> \<not> member DenyAll x
|
||||
\<Longrightarrow> (first_srcNet x, first_destNet x) \<in> sdnets x"
|
||||
by (erule first_isIn)
|
||||
|
||||
show "\<exists>a b. sdnets x = {(a, b), (b, a)} \<Longrightarrow> \<not> member DenyAll x \<Longrightarrow>
|
||||
sdnets x = {(first_srcNet x, first_destNet x), (first_destNet x, first_srcNet x)}"
|
||||
using * by auto
|
||||
|
|
@ -1207,7 +1129,6 @@ lemma alternativelistconc2[rule_format]:
|
|||
"a \<in> set (net_list_aux [x]) \<longrightarrow> a \<in> set (net_list_aux [y,x])"
|
||||
by (induct y, simp_all)
|
||||
|
||||
|
||||
lemma noDA[rule_format]:
|
||||
"noDenyAll xs \<longrightarrow> s \<in> set xs \<longrightarrow> \<not> member DenyAll s"
|
||||
by (induct xs, simp_all)
|
||||
|
|
@ -1240,7 +1161,6 @@ lemma disjComm: "disjSD_2 a b \<Longrightarrow> disjSD_2 b a"
|
|||
using tNDComm apply blast
|
||||
by (meson tNDComm twoNetsDistinct_def)
|
||||
|
||||
|
||||
lemma disjSD2aux:
|
||||
"disjSD_2 a b \<Longrightarrow> \<not> member DenyAll a \<Longrightarrow> \<not> member DenyAll b \<Longrightarrow>
|
||||
disjSD_2 (DenyAllFromTo (first_srcNet a) (first_destNet a) \<oplus>
|
||||
|
|
@ -1250,11 +1170,9 @@ lemma disjSD2aux:
|
|||
apply (simp add: disjSD_2_def)
|
||||
using first_isIn by blast
|
||||
|
||||
|
||||
lemma noDA1eq[rule_format]: "noDenyAll p \<longrightarrow> noDenyAll1 p"
|
||||
by (induct p, simp,rename_tac a p, case_tac a, simp_all)
|
||||
|
||||
|
||||
lemma noDA1C[rule_format]: "noDenyAll1 (a#p) \<longrightarrow> noDenyAll1 p"
|
||||
by (case_tac a, simp_all,rule impI, rule noDA1eq, simp)+
|
||||
|
||||
|
|
@ -1267,11 +1185,9 @@ lemma disjSD_2IDa:
|
|||
disjSD_2 (DenyAllFromTo a b \<oplus> DenyAllFromTo b a \<oplus> x) y"
|
||||
by(simp add:disjSD2aux)
|
||||
|
||||
|
||||
lemma noDAID[rule_format]: "noDenyAll p \<longrightarrow> noDenyAll (insertDenies p)"
|
||||
by (induct p, simp_all,case_tac a, simp_all)
|
||||
|
||||
|
||||
lemma isInIDo[rule_format]:
|
||||
"noDenyAll p \<longrightarrow> s \<in> set (insertDenies p) \<longrightarrow>
|
||||
(\<exists>! a. s = (DenyAllFromTo (first_srcNet a) (first_destNet a)) \<oplus>
|
||||
|
|
@ -1286,7 +1202,6 @@ lemma id_aux1[rule_format]: "DenyAllFromTo (first_srcNet s) (first_destNet s) \<
|
|||
\<longrightarrow> s \<in> set p"
|
||||
by (induct p, simp_all, rename_tac a p, case_tac a, simp_all)
|
||||
|
||||
|
||||
lemma id_aux2:
|
||||
"noDenyAll p \<Longrightarrow>
|
||||
\<forall>s. s \<in> set p \<longrightarrow> disjSD_2 a s \<Longrightarrow>
|
||||
|
|
@ -1297,8 +1212,6 @@ lemma id_aux2:
|
|||
DenyAllFromTo (first_destNet s) (first_srcNet s) \<oplus> s)"
|
||||
by (metis disjComm disjSD2aux isInIDo noDA)
|
||||
|
||||
|
||||
|
||||
lemma id_aux4[rule_format]:
|
||||
"noDenyAll p \<Longrightarrow> \<forall>s. s \<in> set p \<longrightarrow> disjSD_2 a s \<Longrightarrow>
|
||||
s \<in> set (insertDenies p) \<Longrightarrow> \<not> member DenyAll a \<Longrightarrow>
|
||||
|
|
@ -1310,10 +1223,6 @@ lemma id_aux4[rule_format]:
|
|||
apply (drule_tac Q = "disjSD_2 a s" in exE, simp_all, rule id_aux2, simp_all)
|
||||
using isInIDo by blast
|
||||
|
||||
|
||||
(* XXX *)
|
||||
|
||||
|
||||
lemma sepNetsID[rule_format]:
|
||||
"noDenyAll1 p \<longrightarrow> separated p \<longrightarrow> separated (insertDenies p)"
|
||||
apply (induct p, simp)
|
||||
|
|
@ -1328,7 +1237,6 @@ lemma sepNetsID[rule_format]:
|
|||
lemma aNDDA[rule_format]: "allNetsDistinct p \<longrightarrow> allNetsDistinct(DenyAll#p)"
|
||||
by (case_tac p,auto simp: allNetsDistinct_def)
|
||||
|
||||
|
||||
lemma OTNConc[rule_format]: "OnlyTwoNets (y # z) \<longrightarrow> OnlyTwoNets z"
|
||||
by (case_tac y, simp_all)
|
||||
|
||||
|
|
@ -1353,7 +1261,6 @@ lemma setPair4: "{a,b} = {c,d} \<Longrightarrow> a \<noteq> c \<Longrightarrow>
|
|||
lemma otnaux1: " {x, y, x, y} = {x,y}"
|
||||
by auto
|
||||
|
||||
|
||||
lemma OTNIDaux4: "{x,y,x} = {y,x}"
|
||||
by auto
|
||||
|
||||
|
|
@ -1383,8 +1290,7 @@ lemma otnaux: "
|
|||
apply simp
|
||||
apply (subgoal_tac "first_destNet x = first_srcNet y")
|
||||
apply simp
|
||||
apply (rule_tac x ="first_srcNet y" in exI,
|
||||
rule_tac x = "first_destNet y" in exI,simp)
|
||||
apply (rule_tac x ="first_srcNet y" in exI, rule_tac x = "first_destNet y" in exI,simp)
|
||||
apply (rule setPair1)
|
||||
apply simp
|
||||
apply (rule setPair4)
|
||||
|
|
@ -1405,8 +1311,7 @@ lemma otnaux: "
|
|||
apply simp
|
||||
apply (subgoal_tac "first_destNet x = first_srcNet y")
|
||||
apply simp
|
||||
apply (rule_tac x ="first_srcNet y" in exI,
|
||||
rule_tac x = "first_destNet y" in exI)
|
||||
apply (rule_tac x ="first_srcNet y" in exI, rule_tac x = "first_destNet y" in exI)
|
||||
apply (metis OTNIDaux4 insert_commute )
|
||||
apply (rule setPair1)
|
||||
apply simp
|
||||
|
|
@ -1426,8 +1331,7 @@ lemma otnaux: "
|
|||
apply simp_all
|
||||
apply (subgoal_tac "first_destNet x = first_destNet y")
|
||||
apply simp
|
||||
apply (rule_tac x ="first_srcNet y" in exI,
|
||||
rule_tac x = "first_destNet y" in exI)
|
||||
apply (rule_tac x ="first_srcNet y" in exI, rule_tac x = "first_destNet y" in exI)
|
||||
apply (metis OTNIDaux4 insert_commute )
|
||||
apply (rule setPair)
|
||||
apply simp
|
||||
|
|
@ -1453,8 +1357,7 @@ lemma otnaux: "
|
|||
apply simp_all
|
||||
apply (subgoal_tac "first_destNet x = first_destNet y")
|
||||
apply simp
|
||||
apply (rule_tac x ="first_srcNet y" in exI,
|
||||
rule_tac x = "first_destNet y" in exI)
|
||||
apply (rule_tac x ="first_srcNet y" in exI, rule_tac x = "first_destNet y" in exI)
|
||||
apply (rule otnaux1)
|
||||
apply (rule setPair)
|
||||
apply simp
|
||||
|
|
@ -1462,8 +1365,7 @@ lemma otnaux: "
|
|||
apply simp
|
||||
apply (subgoal_tac "first_destNet x = first_srcNet y")
|
||||
apply simp
|
||||
apply (rule_tac x ="first_srcNet y" in exI,
|
||||
rule_tac x = "first_destNet y" in exI)
|
||||
apply (rule_tac x ="first_srcNet y" in exI, rule_tac x = "first_destNet y" in exI)
|
||||
apply (metis OTNIDaux4 insert_commute)
|
||||
apply (rule setPair1)
|
||||
apply simp
|
||||
|
|
@ -1503,8 +1405,7 @@ lemma nda[rule_format]:
|
|||
done
|
||||
|
||||
lemma nDAcharn[rule_format]: "noDenyAll p = (\<forall> r \<in> set p. \<not> member DenyAll r)"
|
||||
by (induct p) simp_all
|
||||
|
||||
by (induct p, simp_all)
|
||||
|
||||
lemma nDAeqSet: "set p = set s \<Longrightarrow> noDenyAll p = noDenyAll s"
|
||||
by (simp add: nDAcharn)
|
||||
|
|
@ -1520,40 +1421,32 @@ lemma nDASC[rule_format]:
|
|||
apply (induct p, simp_all)
|
||||
using nDASCaux nDAcharn nda singleCombinatorsConc by blast
|
||||
|
||||
|
||||
lemma noDAAll[rule_format]: "noDenyAll p = (\<not> memberP DenyAll p)"
|
||||
by (induct p) simp_all
|
||||
|
||||
|
||||
lemma memberPsep[symmetric]: "memberP x p = memberP x (separate p)"
|
||||
by (induct p rule: separate.induct) simp_all
|
||||
|
||||
|
||||
lemma noDAsep[rule_format]: "noDenyAll p \<Longrightarrow> noDenyAll (separate p)"
|
||||
by (simp add:noDAAll,subst memberPsep, simp)
|
||||
|
||||
|
||||
lemma noDA1sep[rule_format]: "noDenyAll1 p \<longrightarrow> noDenyAll1 (separate p)"
|
||||
by (induct p rule:separate.induct, simp_all add: noDAsep)
|
||||
|
||||
|
||||
lemma isInAlternativeLista:
|
||||
"(aa \<in> set (net_list_aux [a]))\<Longrightarrow> aa \<in> set (net_list_aux (a # p))"
|
||||
by (case_tac a,auto)
|
||||
|
||||
|
||||
lemma isInAlternativeListb:
|
||||
"(aa \<in> set (net_list_aux p))\<Longrightarrow> aa \<in> set (net_list_aux (a # p))"
|
||||
by (case_tac a,simp_all)
|
||||
|
||||
|
||||
lemma ANDSepaux: "allNetsDistinct (x # y # z) \<Longrightarrow> allNetsDistinct (x \<oplus> y # z)"
|
||||
apply (simp add: allNetsDistinct_def)
|
||||
apply (intro allI impI, rename_tac a b)
|
||||
apply (drule_tac x = a in spec, drule_tac x = b in spec)
|
||||
by (meson isInAlternativeList)
|
||||
|
||||
|
||||
lemma netlistalternativeSeparateaux:
|
||||
"net_list_aux [y] @ net_list_aux z = net_list_aux (y # z)"
|
||||
by (case_tac y, simp_all)
|
||||
|
|
@ -1561,14 +1454,11 @@ lemma netlistalternativeSeparateaux:
|
|||
lemma netlistalternativeSeparate: "net_list_aux p = net_list_aux (separate p)"
|
||||
by (induct p rule:separate.induct, simp_all) (simp_all add: netlistalternativeSeparateaux)
|
||||
|
||||
|
||||
lemma ANDSepaux2:
|
||||
"allNetsDistinct(x#y#z) \<Longrightarrow> allNetsDistinct(separate(y#z)) \<Longrightarrow> allNetsDistinct(x#separate(y#z))"
|
||||
apply (simp add: allNetsDistinct_def)
|
||||
by (metis isInAlternativeList netlistalternativeSeparate netlistaux)
|
||||
|
||||
|
||||
|
||||
lemma ANDSep[rule_format]: "allNetsDistinct p \<longrightarrow> allNetsDistinct(separate p)"
|
||||
apply (induct p rule: separate.induct, simp_all)
|
||||
apply (metis ANDConc aNDDA)
|
||||
|
|
@ -1595,7 +1485,6 @@ proof -
|
|||
list.simps(15) nDAeqSet noDA1eq)
|
||||
qed
|
||||
|
||||
|
||||
lemma OTNSC[rule_format]: "singleCombinators p \<longrightarrow> OnlyTwoNets p"
|
||||
apply (induct p,simp_all)
|
||||
apply (rename_tac a p)
|
||||
|
|
@ -1616,35 +1505,30 @@ lemma fl3[rule_format]: "NetsCollected p \<longrightarrow> (first_bothNet x \<no
|
|||
(\<forall>a\<in>set p. first_bothNet x \<noteq> first_bothNet a))\<longrightarrow> NetsCollected (x#p)"
|
||||
by (induct p) simp_all
|
||||
|
||||
|
||||
lemma sortedConc[rule_format]: " sorted (a # p) l \<longrightarrow> sorted p l"
|
||||
by (induct p) simp_all
|
||||
|
||||
|
||||
lemma smalleraux2:
|
||||
"{a,b} \<in> set l \<Longrightarrow> {c,d} \<in> set l \<Longrightarrow> {a,b} \<noteq> {c,d} \<Longrightarrow>
|
||||
smaller (DenyAllFromTo a b) (DenyAllFromTo c d) l \<Longrightarrow>
|
||||
\<not> smaller (DenyAllFromTo c d) (DenyAllFromTo a b) l"
|
||||
by (metis bothNet.simps(2) pos_noteq smaller.simps(5))
|
||||
|
||||
|
||||
lemma smalleraux2a:
|
||||
"{a,b} \<in> set l \<Longrightarrow> {c,d} \<in> set l \<Longrightarrow> {a,b} \<noteq> {c,d} \<Longrightarrow>
|
||||
smaller (DenyAllFromTo a b) (AllowPortFromTo c d p) l \<Longrightarrow>
|
||||
\<not> smaller (AllowPortFromTo c d p) (DenyAllFromTo a b) l"
|
||||
by (simp) (metis eq_imp_le pos_noteq)
|
||||
|
||||
|
||||
lemma smalleraux2b:
|
||||
"{a,b} \<in> set l \<Longrightarrow> {c,d} \<in> set l \<Longrightarrow> {a,b} \<noteq> {c,d} \<Longrightarrow> y = DenyAllFromTo a b \<Longrightarrow>
|
||||
smaller (AllowPortFromTo c d p) y l \<Longrightarrow>
|
||||
\<not> smaller y (AllowPortFromTo c d p) l"
|
||||
by (simp) (metis eq_imp_le pos_noteq)
|
||||
|
||||
|
||||
lemma smalleraux2c:
|
||||
"{a,b} \<in> set l\<Longrightarrow>{c,d}\<in>set l\<Longrightarrow>{a,b} \<noteq> {c,d} \<Longrightarrow> y = AllowPortFromTo a b q \<Longrightarrow>
|
||||
smaller (AllowPortFromTo c d p) y l \<Longrightarrow> \<not> smaller y (AllowPortFromTo c d p) l"
|
||||
smaller (AllowPortFromTo c d p) y l \<Longrightarrow> \<not> smaller y (AllowPortFromTo c d p) l"
|
||||
by (simp) (metis pos_noteq)
|
||||
|
||||
lemma smalleraux3:
|
||||
|
|
@ -1684,8 +1568,6 @@ next
|
|||
case (Conc c d) thus ?thesis using assms by simp
|
||||
qed
|
||||
|
||||
thm Combinators.split
|
||||
|
||||
lemma smalleraux3a:
|
||||
"a \<noteq> DenyAll \<Longrightarrow> b \<noteq> DenyAll \<Longrightarrow> in_list b l \<Longrightarrow> in_list a l \<Longrightarrow>
|
||||
bothNet a \<noteq> bothNet b \<Longrightarrow> smaller a b l \<Longrightarrow> singleCombinators [a] \<Longrightarrow>
|
||||
|
|
@ -1696,13 +1578,12 @@ lemma smalleraux3a:
|
|||
done
|
||||
|
||||
lemma posaux[rule_format]: "position a l < position b l \<longrightarrow> a \<noteq> b"
|
||||
by (induct l) simp_all
|
||||
by (induct l, simp_all)
|
||||
|
||||
lemma posaux6[rule_format]:
|
||||
"a \<in> set l \<longrightarrow> b \<in> set l \<longrightarrow> a \<noteq> b \<longrightarrow> position a l \<noteq> position b l"
|
||||
by (induct l) (simp_all add: position_positive)
|
||||
|
||||
|
||||
lemma notSmallerTransaux[rule_format]:
|
||||
"x \<noteq> DenyAll \<Longrightarrow> r \<noteq> DenyAll \<Longrightarrow>
|
||||
singleCombinators [x] \<Longrightarrow> singleCombinators [y] \<Longrightarrow> singleCombinators [r] \<Longrightarrow>
|
||||
|
|
@ -1710,7 +1591,6 @@ lemma notSmallerTransaux[rule_format]:
|
|||
in_list x l \<Longrightarrow> in_list y l \<Longrightarrow> in_list r l \<Longrightarrow> \<not> smaller r x l"
|
||||
by (metis order_trans)
|
||||
|
||||
|
||||
lemma notSmallerTrans[rule_format]:
|
||||
"x \<noteq> DenyAll \<longrightarrow> r \<noteq> DenyAll \<longrightarrow> singleCombinators (x#y#z) \<longrightarrow>
|
||||
\<not> smaller y x l \<longrightarrow> sorted (x#y#z) l \<longrightarrow> r \<in> set z \<longrightarrow>
|
||||
|
|
@ -1800,9 +1680,6 @@ next
|
|||
case (Conc c d) thus ?thesis by simp
|
||||
qed
|
||||
|
||||
|
||||
(* a terrible proof, but I didn't get it better;
|
||||
complex context dependencies into huge case-distinction cascades. bu *)
|
||||
lemma NCSaux2[rule_format]:
|
||||
"noDenyAll p \<longrightarrow> {a, b} \<in> set l \<longrightarrow> all_in_list p l \<longrightarrow>singleCombinators p \<longrightarrow>
|
||||
sorted (DenyAllFromTo a b # p) l \<longrightarrow> {a, b} \<noteq> firstList p \<longrightarrow>
|
||||
|
|
@ -1859,8 +1736,6 @@ next
|
|||
using * by force
|
||||
qed
|
||||
|
||||
|
||||
|
||||
lemma NCSaux3[rule_format]:
|
||||
"noDenyAll p \<longrightarrow> {a, b} \<in> set l \<longrightarrow> all_in_list p l \<longrightarrow>singleCombinators p \<longrightarrow>
|
||||
sorted (AllowPortFromTo a b w # p) l \<longrightarrow> {a, b} \<noteq> firstList p \<longrightarrow>
|
||||
|
|
@ -1891,7 +1766,6 @@ proof -
|
|||
show "{a, b} \<noteq> {u, v}" by (insert * **, simp split: if_splits)
|
||||
qed
|
||||
|
||||
|
||||
lemma NCSaux4[rule_format]:
|
||||
"noDenyAll p \<longrightarrow> {a, b} \<in> set l \<longrightarrow> all_in_list p l \<longrightarrow> singleCombinators p \<longrightarrow>
|
||||
sorted (AllowPortFromTo a b c # p) l \<longrightarrow> {a, b} \<noteq> firstList p \<longrightarrow>
|
||||
|
|
@ -1930,7 +1804,6 @@ proof -
|
|||
show "{a, b} \<noteq> {u, v}" by (insert * **, simp_all split: if_splits)
|
||||
qed
|
||||
|
||||
|
||||
lemma NetsCollectedSorted[rule_format]:
|
||||
"noDenyAll1 p \<longrightarrow> all_in_list p l \<longrightarrow> singleCombinators p \<longrightarrow> sorted p l \<longrightarrow> NetsCollected p"
|
||||
apply (induct p)
|
||||
|
|
@ -1980,37 +1853,28 @@ proof -
|
|||
qed
|
||||
qed
|
||||
|
||||
|
||||
|
||||
lemma NetsCollectedSort: "distinct p \<Longrightarrow>noDenyAll1 p \<Longrightarrow> all_in_list p l \<Longrightarrow>
|
||||
singleCombinators p \<Longrightarrow> NetsCollected (sort p l)"
|
||||
apply (rule_tac l = l in NetsCollectedSorted,rule noDAsort, simp_all)
|
||||
apply (rule_tac b=p in all_in_listSubset)
|
||||
by (auto intro: sort_is_sorted)
|
||||
|
||||
|
||||
|
||||
lemma fBNsep[rule_format]: "(\<forall>a\<in>set z. {b,c} \<noteq> first_bothNet a) \<longrightarrow>
|
||||
(\<forall>a\<in>set (separate z). {b,c} \<noteq> first_bothNet a)"
|
||||
apply (induct z rule: separate.induct, simp)
|
||||
by (rule impI, simp)+
|
||||
|
||||
|
||||
|
||||
lemma fBNsep1[rule_format]: " (\<forall>a\<in>set z. first_bothNet x \<noteq> first_bothNet a) \<longrightarrow>
|
||||
(\<forall>a\<in>set (separate z). first_bothNet x \<noteq> first_bothNet a)"
|
||||
apply (induct z rule: separate.induct, simp)
|
||||
by (rule impI, simp)+
|
||||
|
||||
|
||||
|
||||
lemma NetsCollectedSepauxa:
|
||||
"{b,c}\<noteq>firstList z \<Longrightarrow> noDenyAll1 z \<Longrightarrow> \<forall>a\<in>set z. {b,c}\<noteq>first_bothNet a \<Longrightarrow> NetsCollected z \<Longrightarrow>
|
||||
NetsCollected (separate z) \<Longrightarrow> {b, c} \<noteq> firstList (separate z) \<Longrightarrow> a \<in> set (separate z) \<Longrightarrow>
|
||||
{b, c} \<noteq> first_bothNet a"
|
||||
by (rule fBNsep) simp_all
|
||||
|
||||
|
||||
lemma NetsCollectedSepaux:
|
||||
"first_bothNet (x::('a,'b)Combinators) \<noteq> first_bothNet y \<Longrightarrow> \<not> member DenyAll y \<and> noDenyAll z \<Longrightarrow>
|
||||
(\<forall>a\<in>set z. first_bothNet x \<noteq> first_bothNet a) \<and> NetsCollected (y # z) \<Longrightarrow>
|
||||
|
|
@ -2044,7 +1908,6 @@ next
|
|||
by (metis NetsCollectedSepaux fl3 noDA1eq noDenyAll.simps(1))
|
||||
qed
|
||||
|
||||
|
||||
lemma OTNaux:
|
||||
"onlyTwoNets a \<Longrightarrow> \<not> member DenyAll a \<Longrightarrow> (x,y) \<in> sdnets a \<Longrightarrow>
|
||||
(x = first_srcNet a \<and> y = first_destNet a) \<or> (x = first_destNet a \<and> y = first_srcNet a)"
|
||||
|
|
@ -2078,8 +1941,6 @@ lemma sdnets_noteq:
|
|||
apply (insert first_bothNet_charn [of aa])
|
||||
by(metis OTNaux first_isIn insert_absorb2 insert_commute)
|
||||
|
||||
|
||||
|
||||
lemma fbn_noteq:
|
||||
"onlyTwoNets a \<Longrightarrow> onlyTwoNets aa \<Longrightarrow> first_bothNet a \<noteq> first_bothNet aa \<Longrightarrow>
|
||||
\<not> member DenyAll a \<Longrightarrow> \<not> member DenyAll aa \<Longrightarrow> allNetsDistinct [a, aa] \<Longrightarrow>
|
||||
|
|
@ -2089,7 +1950,6 @@ lemma fbn_noteq:
|
|||
apply (insert sdnets_charn [of aa])
|
||||
by (metis first_bothNet_charn)
|
||||
|
||||
|
||||
lemma NCisSD2aux:
|
||||
assumes 1: "onlyTwoNets a" and 2 : "onlyTwoNets aa" and 3 : "first_bothNet a \<noteq> first_bothNet aa"
|
||||
and 4: "\<not> member DenyAll a" and 5: "\<not> member DenyAll aa" and 6:" allNetsDistinct [a, aa]"
|
||||
|
|
@ -2146,7 +2006,6 @@ proof -
|
|||
apply (metis 4 5 firstInNeta firstInNet alternativelistconc2)
|
||||
apply (metis 3 4 5 first_bothNetsd insert_commute)
|
||||
apply (metis)
|
||||
|
||||
proof -
|
||||
assume 14 : "(ab = first_srcNet a \<and> b = first_destNet a \<or> ab = first_destNet a \<and> b = first_srcNet a) \<and> (c, d) \<in> sdnets aa "
|
||||
and 15 : "sdnets a = {(first_srcNet a, first_destNet a), (first_destNet a, first_srcNet a)} "
|
||||
|
|
@ -2156,7 +2015,6 @@ proof -
|
|||
and 19 : "first_destNet a \<noteq> first_srcNet a"
|
||||
and 20 : "c = first_srcNet aa \<longrightarrow> d \<noteq> first_destNet aa"
|
||||
show " netsDistinct ab c \<or> netsDistinct b d"
|
||||
|
||||
apply (case_tac "(ab = first_srcNet a \<and> b = first_destNet a)",simp_all)
|
||||
apply (case_tac "c = first_srcNet aa", simp_all)
|
||||
apply (metis 2 5 14 20 OTNaux)
|
||||
|
|
@ -2268,14 +2126,11 @@ lemma ANDaux3[rule_format]:
|
|||
"y \<in> set xs \<longrightarrow> a \<in> set (net_list_aux [y]) \<longrightarrow> a \<in> set (net_list_aux xs)"
|
||||
by (induct xs) (simp_all add: isInAlternativeList)
|
||||
|
||||
|
||||
lemma ANDaux2:
|
||||
"allNetsDistinct (x # xs) \<Longrightarrow> y \<in> set xs \<Longrightarrow> allNetsDistinct [x,y]"
|
||||
apply (simp add: allNetsDistinct_def)
|
||||
by (meson ANDaux3 isInAlternativeList netlistaux)
|
||||
|
||||
|
||||
|
||||
lemma NCisSD2[rule_format]:
|
||||
"\<not> member DenyAll a \<Longrightarrow> OnlyTwoNets (a#p) \<Longrightarrow>
|
||||
NetsCollected2 (a # p) \<Longrightarrow> NetsCollected (a#p) \<Longrightarrow>
|
||||
|
|
@ -2343,7 +2198,6 @@ next
|
|||
qed
|
||||
qed
|
||||
|
||||
|
||||
lemma NC2Sep[rule_format]: "noDenyAll1 p \<longrightarrow> NetsCollected2 (separate p)"
|
||||
proof (induct p rule: separate.induct, simp_all, goal_cases)
|
||||
fix x :: "('a, 'b) Combinators list"
|
||||
|
|
@ -2352,15 +2206,15 @@ proof (induct p rule: separate.induct, simp_all, goal_cases)
|
|||
next
|
||||
fix v va fix y::" ('a, 'b) Combinators" fix z
|
||||
case 2 then show ?case
|
||||
by (simp add: firstList.simps(1) fl2 noDA1eq noDenyAll.simps(1))
|
||||
by (simp add: fl2 noDA1eq)
|
||||
next
|
||||
fix v va vb fix y::" ('a, 'b) Combinators" fix z
|
||||
case 3 then show ?case
|
||||
by (simp add: firstList.simps(1) fl2 noDA1eq noDenyAll.simps(1))
|
||||
by (simp add: fl2 noDA1eq)
|
||||
next
|
||||
fix v va fix y::" ('a, 'b) Combinators" fix z
|
||||
case 4 then show ?case
|
||||
by (simp add: firstList.simps(1) fl2 noDA1eq noDenyAll.simps(1))
|
||||
by (simp add: fl2 noDA1eq)
|
||||
qed
|
||||
|
||||
lemma separatedSep[rule_format]:
|
||||
|
|
@ -2372,12 +2226,6 @@ lemma separatedSep[rule_format]:
|
|||
lemma rADnMT[rule_format]: "p \<noteq> [] \<longrightarrow> removeAllDuplicates p \<noteq> []"
|
||||
by (induct p) simp_all
|
||||
|
||||
(* TODO: Prove this lemma:
|
||||
lemma all2: "all_in_list (policy2list p) (Nets_List p)"
|
||||
apply (induct "policy2list p" "Nets_List p" rule: all_in_list.induct)
|
||||
apply simp_all
|
||||
*)
|
||||
|
||||
lemma remDupsNMT[rule_format]: "p \<noteq> [] \<longrightarrow> remdups p \<noteq> []"
|
||||
by (metis remdups_eq_nil_iff)
|
||||
|
||||
|
|
@ -2392,6 +2240,5 @@ lemma sets_distinct5: "(n::int) < m \<Longrightarrow> {(a,b). a = n} \<noteq> {(
|
|||
|
||||
lemma sets_distinct6: "(m::int) < n \<Longrightarrow> {(a,b). a = n} \<noteq> {(a,b). a = m}"
|
||||
by auto
|
||||
|
||||
end
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
File diff suppressed because it is too large
Load Diff
Loading…
Reference in New Issue