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)
 apply(simp add: decision)
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)"
    by(simp add: wf_ruleset_def)
  lemma wf_ruleset_rest: "wf_ruleset γ p (Rule m a # rs) ⟹ wf_ruleset γ p [Rule m a]"
    by(simp add: wf_ruleset_def)

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(simp_all add: approximating_bigstep_fun_seq_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]"
    by(simp add: good_ruleset_def)
  lemma good_ruleset_tail: "good_ruleset (r#rs) ⟹ good_ruleset rs"
    by(simp add: good_ruleset_def)

  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)
  qed(simp_all add: Decision_approximating_bigstep_fun)

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)
         apply(simp add: nomatch)
        apply(simp add: Nomatch.IH)
        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)
         apply(simp add: log)
        apply(simp add: MatchLog.IH)
        done
    next
    case (MatchEmpty γ p m a rs)
      thus ?case
        apply(simp)
        apply(rule_tac t=Undecided in seq_fst)
         apply(simp add: empty)
        apply(simp add: MatchEmpty.IH)
        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(simp add: simple_ruleset_def)
  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"
  apply(simp add: optimize_matches_def)
  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)
  qed(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