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 rs1, Undecided α t; γ,p rs2, t α t'  γ,p rs1@rs2, 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 rs1 rs2 t t'. rs = rs1 @ rs2  γ,p rs1,Undecided α t  P rs1 Undecided t  γ,p rs2,t α t'  P rs2 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 = rs1 @ rs2" "γ,p rs1,s α t" "γ,p rs2,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 = rs1@rs2"
  obtains t' where "γ,p rs1,s α t'" "γ,p rs2,t' α t"
  using assms
  proof (induction rs s t arbitrary: rs1 rs2 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 = rs1 @ rs2" 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) rs1, Undecided α t"
          by simp
        from Seq longer obtain t2
          where t2a: "γ,p drop (length rsa) rs1,t α t2"
            and rs2_t2: "γ,p rs2,t2 α t'"
          by blast
        with t1 rs2_t2 have "γ,p take (length rsa) rs1 @ drop (length rsa) rs1,Undecided α t2"
          by (blast intro: approximating_bigstep.seq)
        with Seq rs2_t2 show ?thesis
          by simp
      next
        case shorter
        with rs have rsa': "rsa = rs1 @ take (length rsa - length rs1) rs2"
          by (metis append_eq_conv_conj length_drop)
        from shorter rs have rsb': "rsb = drop (length rsa - length rs1) rs2"
          by (metis append_eq_conv_conj length_drop)
        from Seq rsa' obtain t1
          where t1a: "γ,p rs1,Undecided α t1"
            and t1b: "γ,p take (length rsa - length rs1) rs2,t1 α t"
          by blast
        from rsb' Seq.hyps have t2: "γ,p drop (length rsa - length rs1) rs2,t α t'"
          by blast
        with seq' t1b have "γ,p rs2,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 rs1 
      approximating_bigstep_fun γ p (rs1 @ rs2) s = approximating_bigstep_fun γ p rs2 (approximating_bigstep_fun γ p rs1 s)"
   proof(induction γ p rs1 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 = (rset 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 = (rset 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 (rs1 @ rs2)  good_ruleset rs1  good_ruleset rs2"
    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 rs1, s α t   
    approximating_bigstep_fun γ p (rs1 @ rs2) s = approximating_bigstep_fun γ p rs2 t"
  proof(induction rs1 s t arbitrary: rs2 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 rs1 rs2 t t')
apply(drule_tac rs1="rm_LogEmpty rs1" and rs2="rm_LogEmpty rs2" 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