# Theory Optimizing

```theory Optimizing
imports Semantics_Ternary
begin

section‹Optimizing›

text‹Note: there is no executable code for rmshadow at the moment›

text‹Assumes: @{term "simple_ruleset"}›
fun rmshadow :: "('a, 'p) match_tac ⇒ 'a rule list ⇒ 'p set ⇒ 'a rule list" where
"rmshadow _ [] _ = []" |
"rmshadow γ ((Rule m a)#rs) P = (if (∀p∈P. ¬ matches γ m a p)
then
else
(Rule m a) # (rmshadow γ rs {p ∈ P. ¬ matches γ m a p}))"
(*needs a ruleset without log and empty*)

subsubsection‹Soundness›
"simple_ruleset rs ⟹ p ∈ P ⟹ approximating_bigstep_fun γ p (rmshadow γ rs P) = approximating_bigstep_fun γ p rs"
proof(induction rs arbitrary: P)
case Nil thus ?case by simp
next
case (Cons r rs)
let ?fw="approximating_bigstep_fun γ" ― ‹firewall semantics›
let ?match="matches γ (get_match r) (get_action r)"
let ?set="{p ∈ P. ¬ ?match p}"
from Cons.IH Cons.prems have IH: "?fw p (?rm rs P) = ?fw p rs" by (simp add: simple_ruleset_def)
from Cons.IH[of "?set"] Cons.prems have IH': "p ∈ ?set ⟹ ?fw p (?rm rs ?set) = ?fw p rs" by (simp add: simple_ruleset_def)
from Cons show ?case
proof(cases "∀p∈P. ¬ ?match p") ― ‹the if-condition of rmshadow›
case True
from True have 1: "?rm (r#rs) P = ?rm rs P"
apply(cases r)
apply(rename_tac m a)
apply(clarify)
apply(simp)
done
from True Cons.prems have "?fw p (r # rs) = ?fw p rs"
apply(cases r)
apply(rename_tac m a)
apply(clarify)
apply(rule just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided)
apply(simp)
done
from this IH have "?fw p (?rm rs P) = ?fw p (r#rs) " by simp
thus "?fw p (?rm (r#rs) P) = ?fw p (r#rs) " using 1 by simp
next
case False ― ‹else›
have "?fw p (r # (?rm rs ?set)) = ?fw p (r # rs)"
proof(cases "p ∈ ?set")
case True
from True IH' show "?fw p (r # (?rm rs ?set)) = ?fw p (r#rs)"
apply(cases r)
apply(rename_tac m a)
apply(clarify)
apply(rule just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided)
apply(simp)
done
next
case False
from False Cons.prems have "?match p" by simp
from Cons.prems have "get_action r = Accept ∨ get_action r = Drop" by(simp add: simple_ruleset_def)
from this ‹?match p›show "?fw p (r # (?rm rs ?set)) = ?fw p (r#rs)"
apply(cases r)
apply(rename_tac m a)
apply(clarify)
apply(rename_tac s)
apply(rule just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided)
apply(simp split:action.split)
apply fast
done
qed
from False this show ?thesis
apply(cases r)
apply(rename_tac m a)
apply(clarify)
apply(rule just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided)
apply(simp)
done
qed
qed

subsection‹Removing rules which cannot apply›

fun rmMatchFalse :: "'a rule list ⇒ 'a rule list" where
"rmMatchFalse [] = []" |
"rmMatchFalse ((Rule (MatchNot MatchAny) _)#rs) = rmMatchFalse rs" |
"rmMatchFalse (r#rs) = r # rmMatchFalse rs"

lemma rmMatchFalse_correct: "approximating_bigstep_fun γ p (rmMatchFalse rs) s = approximating_bigstep_fun γ p rs s"
proof-
{ fix m::"'a match_expr" and a and rs
assume assm: "m ≠ MatchNot MatchAny"
have "rmMatchFalse (Rule m a # rs) = Rule m a # (rmMatchFalse rs)" (is ?hlp)
proof(cases m)
case (MatchNot mexpr) with assm show ?hlp by(cases mexpr) simp_all
qed(simp_all)
} note rmMatchFalse_helper=this
show ?thesis
proof(induction γ p rs s rule: approximating_bigstep_fun_induct)
case Empty thus ?case by(simp)
next
case Decision thus ?case by(metis Decision_approximating_bigstep_fun)
next
case (Nomatch γ p m a) thus ?case
by(cases "m = MatchNot MatchAny") (simp_all add: rmMatchFalse_helper)
next
case (Match γ p m a rs)
from Match(1) have "m ≠ MatchNot MatchAny" using bunch_of_lemmata_about_matches(3) by fast
with Match rmMatchFalse_helper show ?case by(simp split:action.split)
qed
qed

text‹We can stop after a default rule (a rule which matches anything) is observed.›
fun cut_off_after_match_any :: "'a rule list ⇒ 'a rule list" where
"cut_off_after_match_any [] = []" |
"cut_off_after_match_any (Rule m a # rs) =
(if m = MatchAny ∧ (a = Accept ∨ a = Drop ∨ a = Reject)
then [Rule m a] else Rule m a # cut_off_after_match_any rs)"

lemma cut_off_after_match_any:
"approximating_bigstep_fun γ p (cut_off_after_match_any rs) s = approximating_bigstep_fun γ p rs s"
apply(rule just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided)
apply(induction γ p rs s rule: approximating_bigstep_fun.induct)
apply(simp; fail)
apply(simp; fail)