# Theory IP_Partition_Preliminaries

(*  Title:      IP_Partition_Preliminaries
Authors:    Cornelius Diekmann, Max Haslbeck
*)
(*SetPartitioning.thy
Original Author: Max Haslbeck, 2015*)
section‹Partition a Set by a Specific Constraint›
theory IP_Partition_Preliminaries
imports Main
begin

text‹Will be used for the IP address space partition of a firewall.
However, this file is completely generic in terms of sets, it only imports Main.

It will be used in @{file ‹../Service_Matrix.thy›}.
Core idea: This file partitions @{typ "'a set set"} by some magic condition.
Later, we will show that this magic condition implies that all IPs that have been grouped
by the magic condition show the same behaviour for a simple firewall.›

(* disjoint, ipPartition definitions *)

definition disjoint :: "'a set set ⇒ bool" where
"disjoint ts ≡ ∀A ∈ ts. ∀B ∈ ts. A ≠ B ⟶ A ∩ B = {}"

text_raw‹We will call two partitioned sets \emph{complete} iff @{term "⋃ ss = ⋃ ts"}.›

text‹The condition we use to partition a set. If this holds and
@{term A} is the set of IP addresses in each rule in a firewall,
then @{term B} is a partition of @{term "⋃ A"} where each member has the same behavior
w.r.t the firewall ruleset.›
text‹@{term A} is the carrier set and @{term B}* should be a partition of @{term "⋃ A"}
which fulfills the following condition:›
definition ipPartition :: "'a set set ⇒ 'a set set ⇒ bool" where
"ipPartition A B ≡ ∀a ∈ A. ∀b ∈ B. a ∩ b = {} ∨ b ⊆ a"

definition disjoint_list :: "'a set list ⇒ bool" where
"disjoint_list ls ≡ distinct ls ∧ disjoint (set ls)"

context begin
(*internal*)
private fun disjoint_list_rec :: "'a set list ⇒ bool" where
"disjoint_list_rec [] = True" |
"disjoint_list_rec (x#xs) = (x ∩ ⋃(set xs) = {} ∧ disjoint_list_rec xs)"

private lemma disjoint_equi: "disjoint_list_rec ts ⟹ disjoint (set ts)"
apply(induction ts)
by fast

private lemma disjoint_list_disjoint_list_rec: "disjoint_list ts ⟹ disjoint_list_rec ts"
apply(induction ts)
by fast

private definition addSubsetSet :: "'a set ⇒ 'a set set ⇒ 'a set set" where
"addSubsetSet s ts = insert (s - ⋃ts) (((∩) s)  ts) ∪ ((λx. x - s)  ts)"

private fun partitioning :: "'a set list ⇒ 'a set set ⇒ 'a set set" where
"partitioning [] ts = ts" |
"partitioning (s#ss) ts = partitioning ss (addSubsetSet s ts)"

text‹simple examples›
lemma "partitioning [{1::nat,2},{3,4},{5,6,7},{6},{10}] {} = {{10}, {6}, {5, 7}, {}, {3, 4}, {1, 2}}" by eval
lemma "⋃ {{1::nat,2},{3,4},{5,6,7},{6},{10}} = ⋃ (partitioning [{1,2},{3,4},{5,6,7},{6},{10}] {})" by eval
lemma "disjoint (partitioning [{1::nat,2},{3,4},{5,6,7},{6},{10}] {})" by eval
lemma "ipPartition {{1::nat,2},{3,4},{5,6,7},{6},{10}} (partitioning [{1::nat,2},{3,4},{5,6,7},{6},{10}] {})" by eval

lemma "ipPartition A {}" by(simp add: ipPartition_def)

lemma ipPartitionUnion: "ipPartition As Cs ∧ ipPartition Bs Cs ⟷ ipPartition (As ∪ Bs) Cs"
unfolding ipPartition_def by fast

apply(safe)
apply blast
apply blast+
done

private lemma ipPartitioningAddSubset1: "disjoint ts ⟹ ipPartition (insert a ts) (addSubsetSet a ts)"
apply(safe)
apply blast
apply blast+
done

"s - ⋃ts ∈ addSubsetSet s ts"
"t ∈ ts ⟹ s ∩ t ∈ addSubsetSet s ts"
"t ∈ ts ⟹ t - s ∈ addSubsetSet s ts"

assumes "A ∈ addSubsetSet s ts"
obtains "A = s - ⋃ts" | T where "T ∈ ts" "A = s ∩ T" | T where "T ∈ ts" "A = T - s"
using assms unfolding addSubsetSet_def by blast

proof -
{
fix A a b assume "A ∈ addSubsetSet a (addSubsetSet b As)"
proof(goal_cases)
case 1
assume "A = a - ⋃(addSubsetSet b As)"
hence "A = (a - ⋃As) - b" by (auto simp add: Union_addSubsetSet)
thus ?thesis by (auto intro: addSubsetSetI)
next
case (2 T)
have "A = b ∩ (a - ⋃As) ∨ (∃S∈As. A = b ∩ (a ∩ S)) ∨ (∃S∈As. A = (a ∩ S) - b)"
by (rule addSubsetSetE[OF 2(1)]) (auto simp: 2(2))
thus ?thesis by (blast intro: addSubsetSetI)
next
case (3 T)
have "A = b - ⋃(addSubsetSet a As) ∨ (∃S∈As. A = b ∩ (S - a)) ∨ (∃S∈As. A = (S - a) - b)"
thus ?thesis by (blast intro: addSubsetSetI)
qed
}
thus ?thesis by blast
qed

by blast

private lemma disjointPartitioning_helper :"disjoint As ⟹ disjoint (partitioning ss As)"
proof(induction ss arbitrary: As)
case Nil thus ?case by(simp)
next
case (Cons s ss)
from Cons.IH d have "disjoint (partitioning ss (addSubsetSet s As))" .
thus ?case by simp
qed

private lemma disjointPartitioning: "disjoint (partitioning ss {})"
proof -
have "disjoint {}" by(simp add: disjoint_def)
from this disjointPartitioning_helper show ?thesis by fast
qed

private lemma coversallPartitioning:"⋃ (set ts) = ⋃ (partitioning ts {})"
proof -
have "⋃ (set ts ∪ As) = ⋃ (partitioning ts As)" for As
apply(induction ts arbitrary: As)
apply(simp_all)
thus ?thesis by (metis sup_bot.right_neutral)
qed

private lemma "⋃ As = ⋃ Bs ⟹ ipPartition As Bs ⟹ ipPartition As (addSubsetSet a Bs)"

private lemma ipPartitionSingleSet: "ipPartition {t} (addSubsetSet t Bs)
⟹ ipPartition {t} (partitioning ts (addSubsetSet t Bs))"
apply(induction ts arbitrary: Bs t)
apply(simp_all)

private lemma ipPartitioning_helper: "disjoint As ⟹ ipPartition (set ts) (partitioning ts As)"
proof(induction ts arbitrary: As)
case Nil thus ?case by(simp add: ipPartition_def)
next
case (Cons t ts)
from Cons.prems ipPartioningAddSubset0 have d: "ipPartition As (addSubsetSet t As)" by blast
have e: "ipPartition (set ts) (partitioning ts (addSubsetSet t As))" by blast
have "ipPartition {t} (addSubsetSet t As)" by blast
from this Cons.prems ipPartitionSingleSet
have f: "ipPartition {t} (partitioning ts (addSubsetSet t As))" by fast
have "set (t#ts) = insert t (set ts)" by auto
from ipPartitionUnion have "⋀ As Bs Cs. ipPartition As Cs ⟹ ipPartition Bs Cs ⟹ ipPartition (As ∪ Bs) Cs" by fast
with this e f
have "ipPartition (set (t # ts)) (partitioning ts (addSubsetSet t As))" by fastforce
thus ?case by simp
qed

private lemma ipPartitioning: "ipPartition (set ts) (partitioning ts {})"
proof -
have "disjoint {}" by(simp add: disjoint_def)
from this ipPartitioning_helper show ?thesis by fast
qed

(* OPTIMIZATION PROOFS *)

private lemma inter_dif_help_lemma: "A ∩ B = {}  ⟹ B - S = B - (S - A)"
by blast

private lemma disjoint_list_lem: "disjoint_list ls ⟹ ∀s ∈ set(ls). ∀t ∈ set(ls). s ≠ t ⟶ s ∩ t = {}"
proof(induction ls)

private lemma disjoint_list_empty: "disjoint_list []"

private lemma disjoint_sublist: "disjoint_list (t#ts) ⟹ disjoint_list ts"
proof(induction ts arbitrary: t)

private fun intersection_list :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"intersection_list _ [] = []" |
"intersection_list s (t#ts) = (s ∩ t)#(intersection_list s ts)"

private fun intersection_list_opt :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"intersection_list_opt _ [] = []" |
"intersection_list_opt s (t#ts) = (s ∩ t)#(intersection_list_opt (s - t) ts)"

private lemma disjoint_subset: "disjoint A ⟹ a ∈ A ⟹ b ⊆ a ⟹ disjoint ((A - {a}) ∪ {b})"
by blast

private lemma disjoint_intersection: "disjoint A ⟹ a ∈ A ⟹ disjoint ({a ∩ b} ∪ (A - {a}))"
by(blast)

private lemma intList_equi: "disjoint_list_rec ts ⟹ intersection_list s ts = intersection_list_opt s ts"
proof(induction ts)
case Nil thus ?case by simp
next
case (Cons t ts)
from Cons.prems have "intersection_list_opt s ts = intersection_list_opt (s - t) ts"
proof(induction ts arbitrary: s t)
case Nil thus ?case by simp
next
case Cons
have "∀t ∈ set ts. u ∩ t = {} ⟹ intersection_list_opt s ts = intersection_list_opt (s - u) ts"
for u
apply(induction ts arbitrary: s u)
apply(simp_all)
by (metis Diff_Int_distrib2 Diff_empty Diff_eq Un_Diff_Int sup_bot.right_neutral)
with Cons show ?case
apply(simp)
by (metis Diff_Int_distrib2 Diff_empty Un_empty inf_sup_distrib1)
qed
with Cons show ?case by simp
qed

private fun difference_list :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"difference_list _ [] = []" |
"difference_list s (t#ts) = (t - s)#(difference_list s ts)"

private fun difference_list_opt :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"difference_list_opt _ [] = []" |
"difference_list_opt s (t#ts) = (t - s)#(difference_list_opt (s - t) ts)"

private lemma difList_equi: "disjoint_list_rec ts ⟹ difference_list s ts = difference_list_opt s ts"
proof(induction ts arbitrary: s)
case Nil thus ?case by simp
next
case (Cons t ts)
have difference_list_opt_lem0: "∀t ∈ set(ts). u ∩ t = {} ⟹
difference_list_opt s ts = difference_list_opt (s - u) ts"
for u proof(induction ts arbitrary: s u)
case Cons thus ?case
by (metis Diff_Int_distrib2 Diff_eq Un_Diff_Int sup_bot.right_neutral)
qed(simp)
have "disjoint_list_rec (t # ts) ⟹ difference_list_opt s ts = difference_list_opt (s - t) ts"
proof(induction ts arbitrary: s t)
case Cons thus ?case
by (metis Un_empty inf_sup_distrib1 inter_dif_help_lemma)
qed(simp)
with Cons show ?case by simp
qed

private fun partList0 :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"partList0 s [] = []" |
"partList0 s (t#ts) = (s ∩ t)#((t - s)#(partList0 s ts))"

private lemma partList0_set_equi: "set(partList0 s ts) = (((∩) s)  (set ts)) ∪ ((λx. x - s)  (set ts))"
by(induction ts arbitrary: s) auto

private lemma partList_sub_equi0: "set(partList0 s ts) =
set(difference_list s ts) ∪ set(intersection_list s ts)"
by(induction ts arbitrary: s) simp+

private fun partList1 :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"partList1 s [] = []" |
"partList1 s (t#ts) = (s ∩ t)#((t - s)#(partList1 (s - t) ts))"

private lemma partList_sub_equi: "set(partList1 s ts) =
set(difference_list_opt s ts) ∪ set(intersection_list_opt s ts)"
by(induction ts arbitrary: s) (simp_all)

private lemma partList0_partList1_equi: "disjoint_list_rec ts ⟹ set (partList0 s ts) = set (partList1 s ts)"
by (simp add: partList_sub_equi partList_sub_equi0 intList_equi difList_equi)

private fun partList2 :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"partList2 s [] = []" |
"partList2 s (t#ts) = (if s ∩ t = {} then  (t#(partList2 (s - t) ts))
else (s ∩ t)#((t - s)#(partList2 (s - t) ts)))"

private lemma partList2_empty: "partList2 {} ts = ts"
by(induction ts) (simp_all)

private lemma partList1_partList2_equi: "set(partList1 s ts) - {{}} = set(partList2 s ts) - {{}}"
by(induction ts arbitrary: s) (auto)

private fun partList3 :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"partList3 s [] = []" |
"partList3 s (t#ts) = (if s = {} then (t#ts) else
(if s ∩ t = {} then (t#(partList3 (s - t) ts))
else
(if t - s = {} then (t#(partList3 (s - t) ts))
else (t ∩ s)#((t - s)#(partList3 (s - t) ts)))))"

private lemma partList2_partList3_equi: "set(partList2 s ts) - {{}} = set(partList3 s ts) - {{}}"
apply(induction ts arbitrary: s)
apply(simp; fail)
by blast

fun partList4 :: "'a set ⇒ 'a set list ⇒ 'a set list" where
"partList4 s [] = []" |
"partList4 s (t#ts) = (if s = {} then (t#ts) else
(if s ∩ t = {} then (t#(partList4 s ts))
else
(if t - s = {} then (t#(partList4 (s - t) ts))
else (t ∩ s)#((t - s)#(partList4 (s - t) ts)))))"

private lemma partList4: "partList4 s ts = partList3 s ts"
apply(induction ts arbitrary: s)
apply(simp; fail)
done

private lemma partList0_addSubsetSet_equi: "s ⊆ ⋃(set ts) ⟹
addSubsetSet s (set ts) - {{}} = set(partList0 s ts) - {{}}"

private fun partitioning_nontail :: "'a set list ⇒ 'a set set ⇒ 'a set set" where
"partitioning_nontail [] ts = ts" |
"partitioning_nontail (s#ss) ts = addSubsetSet s (partitioning_nontail ss ts)"

private lemma partitioningCom: "addSubsetSet a (partitioning ss ts) = partitioning ss (addSubsetSet a ts)"
apply(induction ss arbitrary: a ts)
apply(simp; fail)
done

private lemma partitioning_nottail_equi: "partitioning_nontail ss ts = partitioning ss ts"
apply(induction ss arbitrary: ts)
apply(simp; fail)
done

fun partitioning1 :: "'a set list ⇒ 'a set list ⇒ 'a set list" where
"partitioning1 [] ts = ts" |
"partitioning1 (s#ss) ts = partList4 s (partitioning1 ss ts)"

lemma partList4_empty: "{} ∉ set ts ⟹ {} ∉ set (partList4 s ts)"
apply(induction ts arbitrary: s)
apply(simp; fail)
by auto

lemma partitioning1_empty0: "{} ∉ set ts ⟹ {} ∉ set (partitioning1 ss ts)"
apply(induction ss arbitrary: ts)
apply(simp; fail)
done

lemma partitioning1_empty1: "{} ∉ set ts ⟹
set(partitioning1 ss ts) - {{}} = set(partitioning1 ss ts)"

lemma partList4_subset: "a ⊆ ⋃(set ts) ⟹ a ⊆ ⋃(set (partList4 b ts))"
apply(induction ts arbitrary: a b)
apply(simp; fail)
apply(simp)
by fast

private lemma "a ≠ {} ⟹ disjoint_list_rec (a # ts) ⟷ disjoint_list_rec ts ∧ a ∩ ⋃ (set ts) = {}" by auto

lemma partList4_complete0: "s ⊆ ⋃(set ts) ⟹ ⋃(set (partList4 s ts)) = ⋃(set ts)"
unfolding partList4
proof(induction ts arbitrary: s)
case Nil thus ?case by(simp)
next
case Cons thus ?case by (simp add: Diff_subset_conv Un_Diff_Int inf_sup_aci(7) sup.commute)
qed

private lemma partList4_disjoint: "s ⊆ ⋃(set ts) ⟹ disjoint_list_rec ts ⟹
disjoint_list_rec (partList4 s ts)"
apply(induction ts arbitrary: s)
apply(simp; fail)
apply(rule conjI)
apply (metis Diff_subset_conv Int_absorb1 Int_lower2 Un_absorb1 partList4_complete0)
apply(safe)
using partList4_complete0 apply (metis Diff_subset_conv Diff_triv IntI UnionI)
apply (metis Diff_subset_conv Diff_triv)
using partList4_complete0 by (metis Diff_subset_conv IntI UnionI)+

lemma union_set_partList4: "⋃(set (partList4 s ts)) = ⋃(set ts)"
by (induction ts arbitrary: s, auto)

private lemma partList4_distinct_hlp: assumes "a ≠ {}" "a ∉ set ts" "disjoint (insert a (set ts))"
shows "a ∉ set (partList4 s ts)"
proof -
from assms have "¬ a ⊆ ⋃(set ts)" unfolding disjoint_def by fastforce
hence "¬ a ⊆ ⋃(set (partList4 s ts))" using union_set_partList4 by metis
thus ?thesis by blast
qed

private lemma partList4_distinct: "{} ∉ set ts ⟹ disjoint_list ts ⟹ distinct (partList4 s ts)"
proof(induction ts arbitrary: s)
case Nil thus ?case by simp
next
case(Cons t ts)
have x1: "⋀x xa xb xc.
t ∉ set ts ⟹
disjoint (insert t (set ts)) ⟹
xa ∈ t ⟹
xb ∈ s ⟹
xb ∈ t ⟹
xb ∉ {} ⟹
xc ∈ s ⟹
xc ∉ {} ⟹
t ∩ s ∈ set (partList4 (s - t) ts) ⟹
¬ t ∩ s ⊆ ⋃(set (partList4 (s - t) ts))"
by(simp add: union_set_partList4 disjoint_def, force) (*1s*)
have x2: "⋀x xa xb xc.
t ∉ set ts ⟹
disjoint (insert t (set ts)) ⟹
x ∈ t ⟹
xa ∈ t ⟹
xa ∉ s ⟹
xb ∈ s ⟹
xc ∈ s ⟹
¬ t - s ⊆ ⋃(set (partList4 (s - t) ts))"
by(simp add: union_set_partList4 disjoint_def, force) (*1s*)
from Cons have IH: "distinct (partList4 s ts)" for s
using disjoint_sublist list.set_intros(2) by auto
from Cons.prems(1,2) IH show ?case
unfolding disjoint_list_def
apply(simp)
apply(safe)
apply(metis partList4_distinct_hlp)
apply(metis partList4_distinct_hlp)
apply(metis partList4_distinct_hlp)
apply blast
using x1 apply blast
using x2 by blast
qed

lemma partList4_disjoint_list: assumes "s ⊆ ⋃(set ts)" "disjoint_list ts" "{} ∉ set ts"
shows "disjoint_list (partList4 s ts)"
unfolding disjoint_list_def
proof
from assms(2,3) show "distinct (partList4 s ts)"
using partList4_distinct disjoint_list_def by auto
show "disjoint (set (partList4 s ts))"
proof -
have disjoint_list_disjoint_list_rec: "disjoint_list ts ⟹ disjoint_list_rec ts"
proof(induction ts)
case Cons thus ?case by(auto simp add: disjoint_list_def disjoint_def)
qed(simp)
with partList4_disjoint disjoint_equi assms(1,2) show ?thesis by blast
qed
qed

lemma partitioning1_subset: "a ⊆ ⋃ (set ts) ⟹ a ⊆ ⋃ (set (partitioning1 ss ts))"
apply(induction ss arbitrary: ts a)
apply(simp)
done

lemma partitioning1_disjoint_list: "{} ∉ (set ts) ⟹ ⋃ (set ss) ⊆ ⋃ (set ts) ⟹
disjoint_list ts ⟹ disjoint_list (partitioning1 ss ts)"
proof(induction ss)
case Nil thus ?case by simp
next
case(Cons t ts) thus ?case
apply(clarsimp)
apply(rule partList4_disjoint_list)
using partitioning1_subset apply(metis)
apply(blast)
using partitioning1_empty0 apply(metis)
done
qed

private lemma partitioning1_disjoint: "⋃ (set ss) ⊆ ⋃ (set ts) ⟹
disjoint_list_rec ts ⟹ disjoint_list_rec (partitioning1 ss ts)"
proof(induction ss arbitrary: ts)

private lemma partitioning_equi: "{} ∉ set ts ⟹ disjoint_list_rec ts ⟹ ⋃ (set ss) ⊆ ⋃ (set ts) ⟹
set(partitioning1 ss ts) = partitioning_nontail ss (set ts) - {{}}"
proof(induction ss)
case Nil thus ?case by simp
next
case (Cons s ss)
for s and ts::"'a set set"
have r: "disjoint_list_rec ts ⟹ s ⊆ ⋃(set ts) ⟹
addSubsetSet s (set ts) - {{}} = set (partList4 s ts) - {{}}"
for ts::"'a set list"
unfolding partList4
partList2_partList3_equi)
have 1: "disjoint_list_rec (partitioning1 ss ts)"
using partitioning1_disjoint Cons.prems by auto
from Cons.prems have 2: "s ⊆ ⋃(set (partitioning1 ss ts))"
by (meson Sup_upper dual_order.trans list.set_intros(1) partitioning1_subset)
from Cons have IH: "set (partitioning1 ss ts) = partitioning_nontail ss (set ts) - {{}}" by auto
qed

lemma ipPartitioning_helper_opt: "{} ∉ set ts ⟹ disjoint_list ts ⟹ ⋃ (set ss) ⊆ ⋃ (set ts)
⟹ ipPartition (set ss) (set (partitioning1 ss ts))"
apply(drule disjoint_list_disjoint_list_rec)
by (meson Diff_subset disjoint_equi ipPartition_def ipPartitioning_helper subsetCE)

lemma complete_helper: "{} ∉ set ts ⟹ ⋃ (set ss) ⊆ ⋃ (set ts)⟹
⋃ (set ts) = ⋃ (set (partitioning1 ss ts))"
apply(induction ss arbitrary: ts)
apply(simp_all)
by (metis partList4_complete0)

lemma "partitioning1  [{1::nat},{2},{}] [{1},{},{2},{3}] = [{1}, {}, {2}, {3}]" by eval

lemma partitioning_foldr: "partitioning X B = foldr addSubsetSet X B"
apply(induction X)
apply(simp; fail)
apply(simp)
by (metis partitioningCom)

lemma "ipPartition (set X) (foldr addSubsetSet X {})"
apply(subst partitioning_foldr[symmetric])
using ipPartitioning by auto

lemma "⋃ (set X) = ⋃ (foldr addSubsetSet X {})"
apply(subst partitioning_foldr[symmetric])

lemma "partitioning1 X B = foldr partList4 X B"
by(induction X)(simp_all)

lemma "ipPartition (set X) (set (partitioning1 X [UNIV]))"
apply(rule ipPartitioning_helper_opt)