# Theory Semantics_Ternary

```theory Semantics_Ternary
imports Matching_Ternary "../Common/List_Misc"
begin

section‹Embedded Ternary-Matching Big Step Semantics›

subsection‹Ternary Semantics (Big Step)›

inductive approximating_bigstep :: "('a, 'p) match_tac ⇒ 'p ⇒ 'a rule list ⇒ state ⇒ state ⇒ bool"
("_,_⊢ ⟨_, _⟩ ⇒⇩α _"  [60,60,20,98,98] 89)
for γ and p where
skip:  "γ,p⊢ ⟨[], t⟩ ⇒⇩α t" |
accept:  "⟦matches γ m Accept p⟧ ⟹ γ,p⊢ ⟨[Rule m Accept], Undecided⟩ ⇒⇩α Decision FinalAllow" |
drop:  "⟦matches γ m Drop p⟧ ⟹ γ,p⊢ ⟨[Rule m Drop], Undecided⟩ ⇒⇩α Decision FinalDeny" |
reject:  "⟦matches γ m Reject p⟧ ⟹  γ,p⊢ ⟨[Rule m Reject], Undecided⟩ ⇒⇩α Decision FinalDeny" |
log:   "⟦matches γ m Log p⟧ ⟹ γ,p⊢ ⟨[Rule m Log], Undecided⟩ ⇒⇩α Undecided" |
empty:   "⟦matches γ m Empty p⟧ ⟹ γ,p⊢ ⟨[Rule m Empty], Undecided⟩ ⇒⇩α Undecided" |
nomatch:  "⟦¬ matches γ m a p⟧ ⟹ γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒⇩α Undecided" |
decision:  "γ,p⊢ ⟨rs, Decision X⟩ ⇒⇩α Decision X" |
seq:  "⟦γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒⇩α t; γ,p⊢ ⟨rs⇩2, t⟩ ⇒⇩α t'⟧ ⟹ γ,p⊢ ⟨rs⇩1@rs⇩2, Undecided⟩ ⇒⇩α t'"

thm approximating_bigstep.induct[of γ p rs s t P]
(*tuned induction rule*)
lemma approximating_bigstep_induct[case_names Skip Allow Deny Log Nomatch Decision Seq, induct pred: approximating_bigstep] : "γ,p⊢ ⟨rs,s⟩ ⇒⇩α t ⟹
(⋀t. P [] t t) ⟹
(⋀m a. matches γ m a p ⟹ a = Accept ⟹ P [Rule m a] Undecided (Decision FinalAllow)) ⟹
(⋀m a. matches γ m a p ⟹ a = Drop ∨ a = Reject ⟹ P [Rule m a] Undecided (Decision FinalDeny)) ⟹
(⋀m a. matches γ m a p ⟹ a = Log ∨ a = Empty ⟹ P [Rule m a] Undecided Undecided) ⟹
(⋀m a. ¬ matches γ m a p ⟹ P [Rule m a] Undecided Undecided) ⟹
(⋀rs X. P rs (Decision X) (Decision X)) ⟹
(⋀rs rs⇩1 rs⇩2 t t'. rs = rs⇩1 @ rs⇩2 ⟹ γ,p⊢ ⟨rs⇩1,Undecided⟩ ⇒⇩α t ⟹ P rs⇩1 Undecided t ⟹ γ,p⊢ ⟨rs⇩2,t⟩ ⇒⇩α t' ⟹ P rs⇩2 t t' ⟹ P rs Undecided t')
⟹ P rs s t"
by (induction rule: approximating_bigstep.induct) (simp_all)

lemma skipD: "γ,p⊢ ⟨[], s⟩ ⇒⇩α t ⟹ s = t"
by (induction "[]::'a rule list" s t rule: approximating_bigstep_induct) (simp_all)

lemma decisionD: "γ,p⊢ ⟨rs, Decision X⟩ ⇒⇩α t ⟹ t = Decision X"
by (induction rs "Decision X" t rule: approximating_bigstep_induct) (simp_all)

lemma acceptD: "γ,p⊢ ⟨[Rule m Accept], Undecided⟩ ⇒⇩α t ⟹ matches γ m Accept p ⟹ t = Decision FinalAllow"
proof (induction "[Rule m Accept]" Undecided t rule: approximating_bigstep_induct)
case Seq thus ?case by (metis list_app_singletonE skipD)
qed(simp_all)

lemma dropD: "γ,p⊢ ⟨[Rule m Drop], Undecided⟩ ⇒⇩α t ⟹ matches γ m Drop p ⟹ t = Decision FinalDeny"
apply (induction "[Rule m Drop]" Undecided t rule: approximating_bigstep_induct)
by(auto dest: skipD elim!: rules_singleton_rev_E)

lemma rejectD: "γ,p⊢ ⟨[Rule m Reject], Undecided⟩ ⇒⇩α t ⟹ matches γ m Reject p ⟹ t = Decision FinalDeny"
apply (induction "[Rule m Reject]" Undecided t rule: approximating_bigstep_induct)
by(auto dest: skipD elim!: rules_singleton_rev_E)

lemma logD: "γ,p⊢ ⟨[Rule m Log], Undecided⟩ ⇒⇩α t ⟹ t = Undecided"
apply (induction "[Rule m Log]" Undecided t rule: approximating_bigstep_induct)
by(auto dest: skipD elim!: rules_singleton_rev_E)

lemma emptyD: "γ,p⊢ ⟨[Rule m Empty], Undecided⟩ ⇒⇩α t ⟹ t = Undecided"
apply (induction "[Rule m Empty]" Undecided t rule: approximating_bigstep_induct)
by(auto dest: skipD elim!: rules_singleton_rev_E)

lemma nomatchD: "γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒⇩α t ⟹ ¬ matches γ m a p ⟹ t = Undecided"
apply (induction "[Rule m a]" Undecided t rule: approximating_bigstep_induct)
by(auto dest: skipD elim!: rules_singleton_rev_E)

lemmas approximating_bigstepD = skipD acceptD dropD rejectD logD emptyD nomatchD decisionD

lemma approximating_bigstep_to_undecided: "γ,p⊢ ⟨rs, s⟩ ⇒⇩α Undecided ⟹ s = Undecided"
by (metis decisionD state.exhaust)

lemma approximating_bigstep_to_decision1: "γ,p⊢ ⟨rs, Decision Y⟩ ⇒⇩α Decision X ⟹ Y = X"
by (metis decisionD state.inject)

lemma nomatch_fst: "¬ matches γ m a p ⟹  γ,p⊢ ⟨rs, s⟩ ⇒⇩α t ⟹ γ,p⊢ ⟨Rule m a # rs, s⟩ ⇒⇩α t"
apply(cases s)
apply(clarify)
apply(drule nomatch)
apply(drule(1) seq)
apply (simp; fail)
apply(clarify)
apply(drule decisionD)
apply(clarify)
done

lemma seq':
assumes "rs = rs⇩1 @ rs⇩2" "γ,p⊢ ⟨rs⇩1,s⟩ ⇒⇩α t" "γ,p⊢ ⟨rs⇩2,t⟩ ⇒⇩α t'"
shows "γ,p⊢ ⟨rs,s⟩ ⇒⇩α t'"
using assms by (cases s) (auto intro: seq decision dest: decisionD)

lemma seq_split:
assumes "γ,p⊢ ⟨rs, s⟩ ⇒⇩α t" "rs = rs⇩1@rs⇩2"
obtains t' where "γ,p⊢ ⟨rs⇩1,s⟩ ⇒⇩α t'" "γ,p⊢ ⟨rs⇩2,t'⟩ ⇒⇩α t"
using assms
proof (induction rs s t arbitrary: rs⇩1 rs⇩2 thesis rule: approximating_bigstep_induct)
case Allow thus ?case by (auto dest: skipD elim!: rules_singleton_rev_E intro: approximating_bigstep.intros)
next
case Deny thus ?case by (auto dest: skipD elim!: rules_singleton_rev_E intro: approximating_bigstep.intros)
next
case Log thus ?case by (auto dest: skipD elim!: rules_singleton_rev_E intro: approximating_bigstep.intros)
next
case Nomatch thus ?case by (auto dest: skipD elim!: rules_singleton_rev_E intro: approximating_bigstep.intros)
next
case (Seq rs rsa rsb t t')
hence rs: "rsa @ rsb = rs⇩1 @ rs⇩2" by simp
note List.append_eq_append_conv_if[simp]
from rs show ?case
proof (cases rule: list_app_eq_cases)
case longer
with Seq have t1: "γ,p⊢ ⟨take (length rsa) rs⇩1, Undecided⟩ ⇒⇩α t"
by simp
from Seq longer obtain t2
where t2a: "γ,p⊢ ⟨drop (length rsa) rs⇩1,t⟩ ⇒⇩α t2"
and rs2_t2: "γ,p⊢ ⟨rs⇩2,t2⟩ ⇒⇩α t'"
by blast
with t1 rs2_t2 have "γ,p⊢ ⟨take (length rsa) rs⇩1 @ drop (length rsa) rs⇩1,Undecided⟩ ⇒⇩α t2"
by (blast intro: approximating_bigstep.seq)
with Seq rs2_t2 show ?thesis
by simp
next
case shorter
with rs have rsa': "rsa = rs⇩1 @ take (length rsa - length rs⇩1) rs⇩2"
by (metis append_eq_conv_conj length_drop)
from shorter rs have rsb': "rsb = drop (length rsa - length rs⇩1) rs⇩2"
by (metis append_eq_conv_conj length_drop)
from Seq rsa' obtain t1
where t1a: "γ,p⊢ ⟨rs⇩1,Undecided⟩ ⇒⇩α t1"
and t1b: "γ,p⊢ ⟨take (length rsa - length rs⇩1) rs⇩2,t1⟩ ⇒⇩α t"
by blast
from rsb' Seq.hyps have t2: "γ,p⊢ ⟨drop (length rsa - length rs⇩1) rs⇩2,t⟩ ⇒⇩α t'"
by blast
with seq' t1b have "γ,p⊢ ⟨rs⇩2,t1⟩ ⇒⇩α t'" by (metis append_take_drop_id)
with Seq t1a show ?thesis
by fast
qed
qed (auto intro: approximating_bigstep.intros)

lemma seqE_fst:
assumes "γ,p⊢ ⟨r#rs, s⟩ ⇒⇩α t"
obtains t' where "γ,p⊢ ⟨[r],s⟩ ⇒⇩α t'" "γ,p⊢ ⟨rs,t'⟩ ⇒⇩α t"
using assms seq_split by (metis append_Cons append_Nil)

lemma seq_fst: assumes "γ,p⊢ ⟨[r], s⟩ ⇒⇩α t" and "γ,p⊢ ⟨rs, t⟩ ⇒⇩α t'" shows "γ,p⊢ ⟨r # rs, s⟩ ⇒⇩α t'"
proof(cases s)
case Undecided with assms seq show "γ,p⊢ ⟨r # rs, s⟩ ⇒⇩α t'" by fastforce
next
case Decision with assms show "γ,p⊢ ⟨r # rs, s⟩ ⇒⇩α t'"
by(auto simp: decision dest!: decisionD)
qed

subsection‹wf ruleset›
text‹
A @{typ "'a rule list"} here is well-formed (for a packet) if
▪ either the rules do not match
▪ or the action is not @{const Call}, not @{const Return}, not @{const Unknown}
›
definition wf_ruleset :: "('a, 'p) match_tac ⇒ 'p ⇒ 'a rule list ⇒ bool" where
"wf_ruleset γ p rs ≡ ∀r ∈ set rs.
(¬ matches γ (get_match r) (get_action r) p) ∨
(¬(∃chain. get_action r = Call chain) ∧ get_action r ≠ Return ∧ ¬(∃chain. get_action r = Goto chain) ∧ get_action r ≠ Unknown)"

lemma wf_ruleset_append: "wf_ruleset γ p (rs1@rs2) ⟷ wf_ruleset γ p rs1 ∧ wf_ruleset γ p rs2"
by(auto simp add: wf_ruleset_def)
lemma wf_rulesetD: assumes "wf_ruleset γ p (r # rs)" shows "wf_ruleset γ p [r]" and "wf_ruleset γ p rs"
using assms by(auto simp add: wf_ruleset_def)
lemma wf_ruleset_fst: "wf_ruleset γ p (Rule m a # rs) ⟷ wf_ruleset γ p [Rule m a] ∧ wf_ruleset γ p rs"
by(auto simp add: wf_ruleset_def)
lemma wf_ruleset_stripfst: "wf_ruleset γ p (r # rs) ⟹ wf_ruleset γ p (rs)"
lemma wf_ruleset_rest: "wf_ruleset γ p (Rule m a # rs) ⟹ wf_ruleset γ p [Rule m a]"

subsection‹Ternary Semantics (Function)›

fun approximating_bigstep_fun :: "('a, 'p) match_tac ⇒ 'p ⇒ 'a rule list ⇒ state ⇒ state" where
"approximating_bigstep_fun γ p [] s = s" |
"approximating_bigstep_fun γ p rs (Decision X) = (Decision X)" |
"approximating_bigstep_fun γ p ((Rule m a)#rs) Undecided = (if
¬ matches γ m a p
then
approximating_bigstep_fun γ p rs Undecided
else
case a of Accept ⇒ Decision FinalAllow
| Drop ⇒ Decision FinalDeny
| Reject ⇒ Decision FinalDeny
| Log ⇒ approximating_bigstep_fun γ p rs Undecided
| Empty ⇒ approximating_bigstep_fun γ p rs Undecided
― ‹unhandled cases›
)"

(*tuned induction rule*)
lemma approximating_bigstep_fun_induct[case_names Empty Decision Nomatch Match] : "
(⋀γ p s. P γ p [] s) ⟹
(⋀γ p r rs X. P γ p (r # rs) (Decision X)) ⟹
(⋀γ p m a rs.
¬ matches γ m a p ⟹ P γ p rs Undecided ⟹ P γ p (Rule m a # rs) Undecided) ⟹
(⋀γ p m a rs.
matches γ m a p ⟹ (a = Log ⟹ P γ p rs Undecided) ⟹ (a = Empty ⟹ P γ p rs Undecided) ⟹ P γ p (Rule m a # rs) Undecided) ⟹
P γ p rs s"
apply (rule approximating_bigstep_fun.induct[of P γ p rs s])
apply (simp_all)
by metis

lemma Decision_approximating_bigstep_fun: "approximating_bigstep_fun γ p rs (Decision X) = Decision X"
by(induction rs) (simp_all)

lemma approximating_bigstep_fun_induct_wf[case_names Empty Decision Nomatch MatchAccept MatchDrop MatchReject MatchLog MatchEmpty, consumes 1]:
"wf_ruleset γ p rs ⟹
(⋀γ p s. P γ p [] s) ⟹
(⋀γ p r rs X. P γ p (r # rs) (Decision X)) ⟹
(⋀γ p m a rs.
¬ matches γ m a p ⟹ P γ p rs Undecided ⟹ P γ p (Rule m a # rs) Undecided) ⟹
(⋀γ p m a rs.
matches γ m a p ⟹ a = Accept  ⟹ P γ p (Rule m a # rs) Undecided) ⟹
(⋀γ p m a rs.
matches γ m a p ⟹ a = Drop ⟹ P γ p (Rule m a # rs) Undecided) ⟹
(⋀γ p m a rs.
matches γ m a p ⟹ a = Reject ⟹ P γ p (Rule m a # rs) Undecided) ⟹
(⋀γ p m a rs.
matches γ m a p ⟹ a = Log ⟹ P γ p rs Undecided  ⟹ P γ p (Rule m a # rs) Undecided) ⟹
(⋀γ p m a rs.
matches γ m a p ⟹ a = Empty ⟹ P γ p rs Undecided ⟹ P γ p (Rule m a # rs) Undecided) ⟹
P γ p rs s"
proof(induction γ p rs s rule: approximating_bigstep_fun_induct)
case Empty thus ?case by blast
next
case Decision thus ?case by blast
next
case Nomatch thus ?case by(simp add: wf_ruleset_def)
next
case (Match γ p m a) thus ?case
apply -
apply(frule wf_rulesetD(1), drule wf_rulesetD(2))
apply(simp)
apply(cases a)
apply(simp_all)
apply(auto simp add: wf_ruleset_def)
done
qed

lemma just_show_all_approximating_bigstep_fun_equalities_with_start_Undecided[case_names Undecided]:
assumes "s = Undecided ⟹ approximating_bigstep_fun γ p rs1 s = approximating_bigstep_fun γ p rs2 s"
shows "approximating_bigstep_fun γ p rs1 s = approximating_bigstep_fun γ p rs2 s"
proof(cases s)
case Undecided thus ?thesis using assms by simp
next
case Decision thus ?thesis by (simp add: Decision_approximating_bigstep_fun)
qed

subsubsection‹Append, Prepend, Postpend, Composition›
lemma approximating_bigstep_fun_seq_wf: "⟦ wf_ruleset γ p rs⇩1⟧ ⟹
approximating_bigstep_fun γ p (rs⇩1 @ rs⇩2) s = approximating_bigstep_fun γ p rs⇩2 (approximating_bigstep_fun γ p rs⇩1 s)"
proof(induction γ p rs⇩1 s rule: approximating_bigstep_fun_induct)
qed(simp_all add: wf_ruleset_def Decision_approximating_bigstep_fun split: action.split)

text‹The state transitions from @{const Undecided} to @{const Undecided} if all intermediate states are @{const Undecided}›
lemma approximating_bigstep_fun_seq_Undecided_wf: "⟦ wf_ruleset γ p (rs1@rs2)⟧ ⟹
approximating_bigstep_fun γ p (rs1@rs2) Undecided = Undecided ⟷
approximating_bigstep_fun γ p rs1 Undecided = Undecided ∧ approximating_bigstep_fun γ p rs2 Undecided = Undecided"
proof(induction γ p rs1 Undecided rule: approximating_bigstep_fun_induct)
qed(simp_all add: wf_ruleset_def split: action.split)

lemma approximating_bigstep_fun_seq_Undecided_t_wf: "⟦ wf_ruleset γ p (rs1@rs2)⟧ ⟹
approximating_bigstep_fun γ p (rs1@rs2) Undecided = t ⟷
approximating_bigstep_fun γ p rs1 Undecided = Undecided ∧ approximating_bigstep_fun γ p rs2 Undecided = t ∨
approximating_bigstep_fun γ p rs1 Undecided = t ∧ t ≠ Undecided"
proof(induction γ p rs1 Undecided rule: approximating_bigstep_fun_induct)
case Empty thus ?case by(cases t) simp_all
next
case Nomatch thus ?case by(simp add: wf_ruleset_def)
next
case Match thus ?case by(auto simp add: wf_ruleset_def split: action.split)
qed

lemma approximating_bigstep_fun_wf_postpend: "wf_ruleset γ p rsA ⟹ wf_ruleset γ p rsB ⟹
approximating_bigstep_fun γ p rsA s = approximating_bigstep_fun γ p rsB s ⟹
approximating_bigstep_fun γ p (rsA@rsC) s = approximating_bigstep_fun γ p (rsB@rsC) s"
apply(induction γ p rsA s rule: approximating_bigstep_fun_induct_wf)
apply (metis Decision_approximating_bigstep_fun)+
done

lemma approximating_bigstep_fun_singleton_prepend:
assumes "approximating_bigstep_fun γ p rsB s = approximating_bigstep_fun γ p rsC s"
shows "approximating_bigstep_fun γ p (r#rsB) s = approximating_bigstep_fun γ p (r#rsC) s"
proof(cases s)
case Decision thus ?thesis by(simp add: Decision_approximating_bigstep_fun)
next
case Undecided
with assms show ?thesis by(cases r)(simp split: action.split)
qed

subsection‹Equality with @{term "γ,p⊢ ⟨rs, s⟩ ⇒⇩α t"} semantics›
lemma approximating_bigstep_wf: "γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩α Undecided ⟹ wf_ruleset γ p rs"
unfolding wf_ruleset_def
proof(induction rs Undecided Undecided rule: approximating_bigstep_induct)
case Skip thus ?case by simp
next
case Log thus ?case by auto
next
case Nomatch thus ?case by simp
next
case (Seq rs rs1 rs2 t)
from Seq approximating_bigstep_to_undecided have "t = Undecided" by fast
from this Seq show ?case by auto
qed

text‹only valid actions appear in this ruleset›
definition good_ruleset :: "'a rule list ⇒ bool" where
"good_ruleset rs ≡ ∀r ∈ set rs. (¬(∃chain. get_action r = Call chain) ∧ get_action r ≠ Return ∧ ¬(∃chain. get_action r = Goto chain) ∧ get_action r ≠ Unknown)"

lemma[code_unfold]: "good_ruleset rs = (∀r∈set rs. (case get_action r of Call chain ⇒ False | Return ⇒ False | Goto chain ⇒ False | Unknown ⇒ False | _ ⇒ True))"
unfolding good_ruleset_def
apply(rule Set.ball_cong)
apply(simp_all)
apply(rename_tac r)
by(case_tac "get_action r")(simp_all)

lemma good_ruleset_alt: "good_ruleset rs = (∀r∈set rs. get_action r = Accept ∨ get_action r = Drop ∨
get_action r = Reject ∨ get_action r = Log  ∨ get_action r = Empty)"
unfolding good_ruleset_def
apply(rule Set.ball_cong)
apply(simp_all)
apply(rename_tac r)
by(case_tac "get_action r")(simp_all)

lemma good_ruleset_append: "good_ruleset (rs⇩1 @ rs⇩2) ⟷ good_ruleset rs⇩1 ∧ good_ruleset rs⇩2"
by(simp add: good_ruleset_alt, blast)

lemma good_ruleset_fst: "good_ruleset (r#rs) ⟹ good_ruleset [r]"
lemma good_ruleset_tail: "good_ruleset (r#rs) ⟹ good_ruleset rs"

text‹
@{term good_ruleset} is stricter than @{term wf_ruleset}. It can be easily checked with running code!
›
lemma good_imp_wf_ruleset: "good_ruleset rs ⟹ wf_ruleset γ p rs" by (metis good_ruleset_def wf_ruleset_def)

lemma simple_imp_good_ruleset: "simple_ruleset rs ⟹ good_ruleset rs"
by(simp add: simple_ruleset_def good_ruleset_def, fastforce)

lemma approximating_bigstep_fun_seq_semantics: "⟦ γ,p⊢ ⟨rs⇩1, s⟩ ⇒⇩α t ⟧ ⟹
approximating_bigstep_fun γ p (rs⇩1 @ rs⇩2) s = approximating_bigstep_fun γ p rs⇩2 t"
proof(induction rs⇩1 s t arbitrary: rs⇩2 rule: approximating_bigstep.induct)

lemma approximating_semantics_imp_fun: "γ,p⊢ ⟨rs, s⟩ ⇒⇩α t ⟹ approximating_bigstep_fun γ p rs s = t"
proof(induction rs s t rule: approximating_bigstep_induct)
qed(auto simp add: approximating_bigstep_fun_seq_semantics Decision_approximating_bigstep_fun)

lemma approximating_fun_imp_semantics: assumes "wf_ruleset γ p rs"
shows "approximating_bigstep_fun γ p rs s = t ⟹ γ,p⊢ ⟨rs, s⟩ ⇒⇩α t"
using assms proof(induction γ p rs s rule: approximating_bigstep_fun_induct_wf)
case (Empty γ p s)
thus "γ,p⊢ ⟨[], s⟩ ⇒⇩α t"  using skip by(simp)
next
case (Decision γ p r rs X)
hence "t = Decision X" by simp
thus "γ,p⊢ ⟨r # rs, Decision X⟩ ⇒⇩α t" using decision by fast
next
case (Nomatch γ p m a rs)
thus "γ,p⊢ ⟨Rule m a # rs, Undecided⟩ ⇒⇩α t"
apply(rule_tac t=Undecided in seq_fst)
done
next
case (MatchAccept γ p m a rs)
hence "t = Decision FinalAllow" by simp
thus ?case by (metis MatchAccept.hyps accept decision seq_fst)
next
case (MatchDrop γ p m a rs)
hence "t = Decision FinalDeny" by simp
thus ?case by (metis MatchDrop.hyps drop decision seq_fst)
next
case (MatchReject γ p m a rs)
hence "t = Decision FinalDeny" by simp
thus ?case by (metis MatchReject.hyps reject decision seq_fst)
next
case (MatchLog γ p m a rs)
thus ?case
apply(simp)
apply(rule_tac t=Undecided in seq_fst)
done
next
case (MatchEmpty γ p m a rs)
thus ?case
apply(simp)
apply(rule_tac t=Undecided in seq_fst)
done
qed

text‹Henceforth, we will use the @{term approximating_bigstep_fun} semantics, because they are easier.
We show that they are equal.
›
theorem approximating_semantics_iff_fun: "wf_ruleset γ p rs ⟹
γ,p⊢ ⟨rs, s⟩ ⇒⇩α t ⟷ approximating_bigstep_fun γ p rs s = t"
by (metis approximating_fun_imp_semantics approximating_semantics_imp_fun)

corollary approximating_semantics_iff_fun_good_ruleset: "good_ruleset rs ⟹
γ,p⊢ ⟨rs, s⟩ ⇒⇩α t ⟷ approximating_bigstep_fun γ p rs s = t"
by (metis approximating_semantics_iff_fun good_imp_wf_ruleset)

lemma approximating_bigstep_deterministic: "⟦ γ,p⊢ ⟨rs, s⟩ ⇒⇩α t; γ,p⊢ ⟨rs, s⟩ ⇒⇩α t' ⟧ ⟹ t = t'"
proof(induction arbitrary: t' rule: approximating_bigstep_induct)
case Seq thus ?case
by (metis (opaque_lifting, mono_tags) append_Nil2 approximating_bigstep_fun.simps(1) approximating_bigstep_fun_seq_semantics)
qed(auto dest: approximating_bigstepD)

lemma rm_LogEmpty_fun_semantics:
"approximating_bigstep_fun γ p (rm_LogEmpty rs) s = approximating_bigstep_fun γ p rs s"
proof(induction γ p rs s rule: approximating_bigstep_fun_induct)
case Empty thus ?case by(simp)
next
case Decision thus ?case by(simp add: Decision_approximating_bigstep_fun)
next
case (Nomatch γ p m a rs) thus ?case by(cases a,simp_all)
next
case (Match γ p m a rs) thus ?case by(cases a,simp_all)
qed

(*we probably don't need the following*)
lemma "γ,p⊢ ⟨rm_LogEmpty rs, s⟩ ⇒⇩α t ⟷ γ,p⊢ ⟨rs, s⟩ ⇒⇩α t"
apply(rule iffI)
apply(induction rs arbitrary: s t)
apply(simp_all)
apply(rename_tac r rs s t)
apply(case_tac r)
apply(simp)
apply(rename_tac m a)
apply(case_tac a)
apply(simp_all)
apply(auto intro: approximating_bigstep.intros )
apply(erule seqE_fst, simp add: seq_fst)
apply(erule seqE_fst, simp add: seq_fst)
apply (metis decision log nomatch_fst seq_fst state.exhaust)
apply(erule seqE_fst, simp add: seq_fst)
apply(erule seqE_fst, simp add: seq_fst)
apply(erule seqE_fst, simp add: seq_fst)
apply(erule seqE_fst, simp add: seq_fst)
apply (metis decision empty nomatch_fst seq_fst state.exhaust)
apply(erule seqE_fst, simp add: seq_fst)
apply(induction rs s t rule: approximating_bigstep_induct)
apply(auto intro: approximating_bigstep.intros)
apply(rename_tac m a)
apply(case_tac a)
apply(auto intro: approximating_bigstep.intros)
apply(rename_tac rs⇩1 rs⇩2 t t')
apply(drule_tac rs⇩1="rm_LogEmpty rs⇩1" and rs⇩2="rm_LogEmpty rs⇩2" in seq)
apply(simp_all)
using rm_LogEmpty_seq apply metis
done

lemma rm_LogEmpty_simple_but_Reject:
"good_ruleset rs ⟹ ∀r ∈ set (rm_LogEmpty rs). get_action r = Accept ∨ get_action r = Reject ∨ get_action r = Drop"
proof(induction rs)
case Nil thus ?case by(simp add: good_ruleset_def)
next
case (Cons r rs) thus ?case
apply(clarify)
apply(cases r, rename_tac m a, simp)
by(case_tac a) (auto simp add: good_ruleset_def)
qed

lemma rw_Reject_fun_semantics:
"wf_unknown_match_tac α ⟹
(approximating_bigstep_fun (β, α) p (rw_Reject rs) s = approximating_bigstep_fun (β, α) p rs s)"
proof(induction rs)
case Nil thus ?case by simp
next
case (Cons r rs)
thus ?case
apply(case_tac r, rename_tac m a, simp)
apply(case_tac a)
apply(case_tac [!] s)
apply(auto dest: wf_unknown_match_tacD_False1 wf_unknown_match_tacD_False2)
done
qed

lemma rmLogEmpty_rwReject_good_to_simple: "good_ruleset rs ⟹ simple_ruleset (rw_Reject (rm_LogEmpty rs))"
apply(drule rm_LogEmpty_simple_but_Reject)
apply(induction rs)
apply(simp_all)
apply(rename_tac r rs)
apply(case_tac r)
apply(rename_tac m a)
apply(case_tac a)
apply(simp_all)
done

subsection‹Matching›
lemma optimize_matches_option_generic:
assumes "∀ r ∈ set rs. P (get_match r) (get_action r)"
and "(⋀m m' a. P m a ⟹ f m = Some m' ⟹ matches γ m' a p = matches γ m a p)"
and "(⋀m a. P m a ⟹ f m = None ⟹ ¬ matches γ m a p)"
shows "approximating_bigstep_fun γ p (optimize_matches_option f rs) s = approximating_bigstep_fun γ p rs s"
using assms proof(induction γ p rs s rule: approximating_bigstep_fun_induct)
case Decision thus ?case by (simp add: Decision_approximating_bigstep_fun)
next
case (Nomatch γ p m a rs) thus ?case
apply(simp)
apply(cases "f m")
apply(simp; fail)
apply(simp del: approximating_bigstep_fun.simps)
apply(rename_tac m')
apply(subgoal_tac "¬ matches γ m' a p")
apply(simp; fail)
using assms by blast
next
case (Match γ p m a rs) thus ?case
apply(cases "f m")
apply(simp; fail)
apply(simp del: approximating_bigstep_fun.simps)
apply(rename_tac m')
apply(subgoal_tac "matches γ m' a p")
apply(simp split: action.split; fail)
using assms by blast
qed(simp)

lemma optimize_matches_generic: "∀ r ∈ set rs. P (get_match r) (get_action r) ⟹
(⋀m a. P m a ⟹ matches γ (f m) a p = matches γ m a p) ⟹
approximating_bigstep_fun γ p (optimize_matches f rs) s = approximating_bigstep_fun γ p rs s"
unfolding optimize_matches_def
apply(rule optimize_matches_option_generic)
apply(simp; fail)
apply(simp split: if_split_asm)
apply blast
apply(simp split: if_split_asm)
using matcheq_matchNone_not_matches by fast

lemma optimize_matches_matches_fst: "matches γ (f m) a p ⟹ optimize_matches f (Rule m a # rs) = (Rule (f m) a)# optimize_matches f rs"
by (meson matcheq_matchNone_not_matches)

lemma optimize_matches: "∀m a. matches γ (f m) a p = matches γ m a p ⟹ approximating_bigstep_fun γ p (optimize_matches f rs) s = approximating_bigstep_fun γ p rs s"
using optimize_matches_generic[where P="λ_ _. True"] by metis

lemma optimize_matches_opt_MatchAny_match_expr: "approximating_bigstep_fun γ p (optimize_matches opt_MatchAny_match_expr rs) s = approximating_bigstep_fun γ p rs s"
using optimize_matches opt_MatchAny_match_expr_correct by metis

lemma optimize_matches_a: "∀a m. matches γ m a = matches γ (f a m) a ⟹ approximating_bigstep_fun γ p (optimize_matches_a f rs) s = approximating_bigstep_fun γ p rs s"
proof(induction γ p rs s rule: approximating_bigstep_fun_induct)
case (Match γ p m a rs) thus ?case by(case_tac a)(simp_all add: optimize_matches_a_def)

lemma optimize_matches_a_simplers:
assumes "simple_ruleset rs" and "∀a m. a = Accept ∨ a = Drop ⟶ matches γ (f a m) a = matches γ m a"
shows "approximating_bigstep_fun γ p (optimize_matches_a f rs) s = approximating_bigstep_fun γ p rs s"
proof -
from assms(1) have "wf_ruleset γ p rs" by(simp add: simple_imp_good_ruleset good_imp_wf_ruleset)
from ‹wf_ruleset γ p rs› assms show "approximating_bigstep_fun γ p (optimize_matches_a f rs) s = approximating_bigstep_fun γ p rs s"
proof(induction γ p rs s rule: approximating_bigstep_fun_induct_wf)
case Nomatch thus ?case
apply(simp add: optimize_matches_a_def simple_ruleset_def)
apply(safe)
apply(simp_all)
done
next
case MatchReject thus ?case by(simp add: optimize_matches_a_def simple_ruleset_def)
qed(simp_all add: optimize_matches_a_def simple_ruleset_tail)
qed

lemma not_matches_removeAll: "¬ matches γ m a p ⟹
approximating_bigstep_fun γ p (removeAll (Rule m a) rs) Undecided = approximating_bigstep_fun γ p rs Undecided"
apply(induction γ p rs Undecided rule: approximating_bigstep_fun.induct)
apply(simp)
apply(simp split: action.split)
apply blast
done

end
```