Theory Alternative_Semantics

theory Alternative_Semantics
imports Semantics
begin
  
context begin
  
(* the first thing (I think) we have to do is alter the Seq rule / merge it with NoMatch.
 Its properties make it hard to work with… *)
private inductive iptables_bigstep_ns :: "'a ruleset ⇒ ('a, 'p) matcher ⇒ 'p ⇒ 'a rule list ⇒ state ⇒ state ⇒ bool"
  ("_,_,_⊢ ⟨_, _⟩ ⇒⇩s _"  [60,60,60,20,98,98] 89)
  for Γ and γ and p where
skip:    "Γ,γ,p⊢ ⟨[], t⟩ ⇒⇩s t" |
accept:  "matches γ m p ⟹ Γ,γ,p⊢ ⟨Rule m Accept # rs, Undecided⟩ ⇒⇩s Decision FinalAllow" |
drop:    "matches γ m p ⟹ Γ,γ,p⊢ ⟨Rule m Drop # rs, Undecided⟩ ⇒⇩s Decision FinalDeny" |
reject:  "matches γ m p ⟹  Γ,γ,p⊢ ⟨Rule m Reject # rs, Undecided⟩ ⇒⇩s Decision FinalDeny" |
log:     "matches γ m p ⟹ Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩s t ⟹ Γ,γ,p⊢ ⟨Rule m Log # rs, Undecided⟩ ⇒⇩s t" |
empty:   "matches γ m p ⟹ Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩s t ⟹ Γ,γ,p⊢ ⟨Rule m Empty # rs, Undecided⟩ ⇒⇩s t" |
nms:     "¬ matches γ m p ⟹ Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩s t ⟹ Γ,γ,p⊢ ⟨Rule m a # rs, Undecided⟩ ⇒⇩s t" |
(*decision: "Γ,γ,p⊢ ⟨rs, Decision X⟩ ⇒⇩s Decision X" |*)
call_return:  "⟦ matches γ m p; Γ chain = Some (rs⇩1 @ Rule m' Return # rs⇩2);
                 matches γ m' p; Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒⇩s Undecided; Γ,γ,p⊢ ⟨rrs, Undecided⟩ ⇒⇩s t ⟧ ⟹
               Γ,γ,p⊢ ⟨Rule m (Call chain) # rrs, Undecided⟩ ⇒⇩s t" |
call_result:  "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩s Decision X ⟧ ⟹
               Γ,γ,p⊢ ⟨Rule m (Call chain) # rrs, Undecided⟩ ⇒⇩s Decision X" |
call_no_result:  "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩s Undecided;
                    Γ,γ,p⊢ ⟨rrs, Undecided⟩ ⇒⇩s t ⟧ ⟹
               Γ,γ,p⊢ ⟨Rule m (Call chain) # rrs, Undecided⟩ ⇒⇩s t"

private lemma a: "Γ,γ,p⊢ ⟨rs, s⟩ ⇒⇩s t ⟹ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
  apply(induction rule: iptables_bigstep_ns.induct; (simp add: iptables_bigstep.intros;fail)?)
  apply (meson iptables_bigstep.decision iptables_bigstep.accept seq_cons)
  apply (meson iptables_bigstep.decision iptables_bigstep.drop seq_cons)
  apply (meson iptables_bigstep.decision iptables_bigstep.reject seq_cons)
  apply (meson iptables_bigstep.log seq_cons)
  apply (meson iptables_bigstep.empty seq_cons)
  apply (meson nomatch seq_cons)
  subgoal using iptables_bigstep.call_return seq_cons by fastforce
  apply (meson iptables_bigstep.decision iptables_bigstep.call_result seq_cons)
  apply (meson iptables_bigstep.call_result seq'_cons)
  done

private lemma empty_rs_stateD: assumes "Γ,γ,p⊢ ⟨[], s⟩ ⇒⇩s t" shows "t = s"
  using assms by(cases rule: iptables_bigstep_ns.cases)
private lemma decided: "⟦Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒⇩s Decision X⟧ ⟹ Γ,γ,p⊢ ⟨rs⇩1@rs⇩2, Undecided⟩ ⇒⇩s Decision X"
proof(induction rs⇩1)
  case Nil
  then show ?case by (fast dest: empty_rs_stateD)
next
  case (Cons a rs⇩1)
  from Cons.prems show ?case 
    by(cases rule: iptables_bigstep_ns.cases; simp add: Cons.IH iptables_bigstep_ns.intros)
qed
  
private lemma decided_determ: "⟦Γ,γ,p⊢ ⟨rs⇩1, s⟩ ⇒⇩s t; s = Decision X⟧ ⟹ t = Decision X"
  by(induction rule: iptables_bigstep_ns.induct; (simp add: iptables_bigstep_ns.intros;fail)?)

private lemma seq_ns:
  "⟦Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒⇩s t; Γ,γ,p⊢ ⟨rs⇩2, t⟩ ⇒⇩s t'⟧ ⟹ Γ,γ,p⊢ ⟨rs⇩1@rs⇩2, Undecided⟩ ⇒⇩s t'"
proof (cases t, goal_cases)
  case 1
  from 1(1,2) show ?case unfolding 1 proof(induction rs⇩1)
    case (Cons a rs⇩3)
    then show ?case
      apply -
      apply(rule iptables_bigstep_ns.cases[OF Cons.prems(1)]; simp add: iptables_bigstep_ns.intros)
    done
  qed simp
next
  case (2 X)
  hence "t' = Decision X" by (simp add: decided_determ)
  from 2(1) show ?case by (simp add: "2"(3) ‹t' = Decision X› decided)
qed
      
private lemma b: "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t ⟹ s = Undecided ⟹ Γ,γ,p⊢ ⟨rs, s⟩ ⇒⇩s t"
  apply(induction rule: iptables_bigstep.induct; (simp add: iptables_bigstep_ns.intros;fail)?)
   apply (metis decided decision seq_ns seq_progress skipD state.exhaust)
  apply(metis call_no_result iptables_bigstep_ns.call_result iptables_bigstep_ns.skip state.exhaust)
  done
    
private inductive iptables_bigstep_nz :: "'a ruleset ⇒ ('a, 'p) matcher ⇒ 'p ⇒ 'a rule list ⇒ state ⇒ bool"
  ("_,_,_⊢ _ ⇒⇩z _"  [60,60,60,20,98] 89)
  for Γ and γ and p where
skip:    "Γ,γ,p ⊢ []  ⇒⇩z Undecided" |
accept:  "matches γ m p ⟹ Γ,γ,p⊢ Rule m Accept # rs ⇒⇩z Decision FinalAllow" |
drop:    "matches γ m p ⟹ Γ,γ,p⊢ Rule m Drop # rs ⇒⇩z Decision FinalDeny" |
reject:  "matches γ m p ⟹  Γ,γ,p⊢ Rule m Reject # rs ⇒⇩z Decision FinalDeny" |
log:     "matches γ m p ⟹ Γ,γ,p⊢ rs ⇒⇩z t ⟹ Γ,γ,p⊢ Rule m Log # rs ⇒⇩z t" |
empty:   "matches γ m p ⟹ Γ,γ,p⊢ rs ⇒⇩z t ⟹ Γ,γ,p⊢ Rule m Empty # rs ⇒⇩z t" |
nms:     "¬ matches γ m p ⟹ Γ,γ,p⊢ rs ⇒⇩z t ⟹ Γ,γ,p⊢ Rule m a # rs ⇒⇩z t" |
call_return:  "⟦ matches γ m p; Γ chain = Some (rs⇩1 @ Rule m' Return # rs⇩2);
                 matches γ m' p; Γ,γ,p⊢ rs⇩1 ⇒⇩z Undecided; Γ,γ,p⊢ rrs ⇒⇩z t ⟧ ⟹
               Γ,γ,p⊢ Rule m (Call chain) # rrs ⇒⇩z t" |
call_result:  "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢ rs ⇒⇩z Decision X ⟧ ⟹
               Γ,γ,p⊢ Rule m (Call chain) # rrs ⇒⇩z Decision X" |
call_no_result:  "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢ rs ⇒⇩z Undecided;
                    Γ,γ,p⊢ rrs ⇒⇩z t ⟧ ⟹
               Γ,γ,p⊢ Rule m (Call chain) # rrs ⇒⇩z t"

private lemma c: "Γ,γ,p⊢ rs ⇒⇩z t ⟹ Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒⇩s t"
  by(induction rule: iptables_bigstep_nz.induct; simp add: iptables_bigstep_ns.intros)
    
private lemma d: "Γ,γ,p⊢ ⟨rs, s⟩ ⇒⇩s t ⟹ s = Undecided ⟹ Γ,γ,p⊢ rs ⇒⇩z t"
  by(induction rule: iptables_bigstep_ns.induct; simp add: iptables_bigstep_nz.intros)
    
inductive iptables_bigstep_r :: "'a ruleset ⇒ ('a, 'p) matcher ⇒ 'p ⇒ 'a rule list ⇒ state ⇒ bool"
  ("_,_,_⊢ _ ⇒⇩r _"  [60,60,60,20,98] 89)
  for Γ and γ and p where
skip:    "Γ,γ,p ⊢ []  ⇒⇩r Undecided" |
accept:  "matches γ m p ⟹ Γ,γ,p⊢ Rule m Accept # rs ⇒⇩r Decision FinalAllow" |
drop:    "matches γ m p ⟹ Γ,γ,p⊢ Rule m Drop # rs ⇒⇩r Decision FinalDeny" |
reject:  "matches γ m p ⟹  Γ,γ,p⊢ Rule m Reject # rs ⇒⇩r Decision FinalDeny" |
return:  "matches γ m p ⟹  Γ,γ,p⊢ Rule m Return # rs ⇒⇩r Undecided" |
log:     "Γ,γ,p⊢ rs ⇒⇩r t ⟹ Γ,γ,p⊢ Rule m Log # rs ⇒⇩r t" |
empty:   "Γ,γ,p⊢ rs ⇒⇩r t ⟹ Γ,γ,p⊢ Rule m Empty # rs ⇒⇩r t" |
nms:     "¬ matches γ m p ⟹ Γ,γ,p⊢ rs ⇒⇩r t ⟹ Γ,γ,p⊢ Rule m a # rs ⇒⇩r t" |
call_result:  "⟦ matches γ m p; Γ chain = Some rs; Γ,γ,p⊢ rs ⇒⇩r Decision X ⟧ ⟹
               Γ,γ,p⊢ Rule m (Call chain) # rrs ⇒⇩r Decision X" |
call_no_result:  "⟦ Γ chain = Some rs; Γ,γ,p⊢ rs ⇒⇩r Undecided;
                    Γ,γ,p⊢ rrs ⇒⇩r t ⟧ ⟹
               Γ,γ,p⊢ Rule m (Call chain) # rrs ⇒⇩r t"

private lemma returning:  "⟦Γ,γ,p⊢ rs⇩1 ⇒⇩r Undecided; matches γ m' p⟧
    ⟹ Γ,γ,p⊢ rs⇩1 @ Rule m' Return # rs⇩2 ⇒⇩r Undecided"
proof(induction rs⇩1)
  case Nil
  then show ?case by (simp add: return)
next
  case (Cons a rs⇩3)
  then show ?case by - (rule iptables_bigstep_r.cases[OF Cons.prems(1)]; simp add: iptables_bigstep_r.intros)
qed
 
private lemma e: "Γ,γ,p⊢ rs ⇒⇩z t ⟹ s = Undecided ⟹ Γ,γ,p⊢ rs ⇒⇩r t"
  by(induction rule: iptables_bigstep_nz.induct; simp add: iptables_bigstep_r.intros returning)
    

definition "no_call_to c rs ≡ (∀r ∈ set rs. case get_action r of Call c' ⇒ c ≠ c' | _ ⇒ True)"
definition "all_chains p Γ rs ≡ (p rs ∧ (∀l rs. Γ l = Some rs ⟶ p rs))"
private lemma all_chains_no_call_upd: "all_chains (no_call_to c) Γ rs ⟹ (Γ(c ↦ x)),γ,p⊢ rs ⇒⇩z t ⟷ Γ,γ,p⊢ rs ⇒⇩z t"
proof (rule iffI, goal_cases)
  case 1
  from 1(2,1) show ?case 
    by(induction rule: iptables_bigstep_nz.induct; 
      (simp add: iptables_bigstep_nz.intros no_call_to_def all_chains_def split: if_splits;fail)?)
next
  case 2
  from 2(2,1) show ?case 
    by(induction rule: iptables_bigstep_nz.induct; 
      (simp add: iptables_bigstep_nz.intros no_call_to_def all_chains_def split:  action.splits;fail)?)
qed

lemma updated_call: "Γ(c ↦ rs),γ,p⊢ rs ⇒⇩z t ⟹ matches γ m p ⟹ Γ(c ↦ rs),γ,p⊢ [Rule m (Call c)] ⇒⇩z t"
  by(cases t; simp add: iptables_bigstep_nz.call_no_result iptables_bigstep_nz.call_result iptables_bigstep_nz.skip)
    
private lemma shows
      log_nz:     "Γ,γ,p⊢ rs ⇒⇩z t ⟹ Γ,γ,p⊢ Rule m Log # rs ⇒⇩z t"
and empty_nz:   "Γ,γ,p⊢ rs ⇒⇩z t ⟹ Γ,γ,p⊢ Rule m Empty # rs ⇒⇩z t"
  by (meson iptables_bigstep_nz.log iptables_bigstep_nz.empty iptables_bigstep_nz.nms)+
    
private lemma nz_empty_rs_stateD: assumes "Γ,γ,p⊢ [] ⇒⇩z t" shows "t = Undecided"
  using assms by(cases rule: iptables_bigstep_nz.cases)
    
private lemma upd_callD: "Γ(c ↦ rs),γ,p⊢ [Rule m (Call c)] ⇒⇩z t ⟹ matches γ m p 
  ⟹ (Γ(c ↦ rs),γ,p⊢ rs ⇒⇩z t ∨ (∃rs⇩1 rs⇩2 m'. rs = rs⇩1 @ Rule m' Return # rs⇩2 ∧ matches γ m' p ∧ Γ(c ↦ rs),γ,p⊢ rs⇩1 ⇒⇩z Undecided ∧ t = Undecided))"
  by(subst (asm) iptables_bigstep_nz.simps) (auto dest!: nz_empty_rs_stateD)
    
private lemma partial_fun_upd: "(f(x ↦ y)) x = Some y" by(fact fun_upd_same)
 
lemma f: "Γ,γ,p⊢ rs ⇒⇩r t ⟹ matches γ m p ⟹ all_chains (no_call_to c) Γ rs ⟹ 
  (Γ(c ↦ rs)),γ,p⊢ [Rule m (Call c)] ⇒⇩z t"
proof(induction rule: iptables_bigstep_r.induct; (simp add: iptables_bigstep_nz.intros;fail)?)
  case (return m rs)
  then show ?case by (metis append_Nil fun_upd_same iptables_bigstep_nz.call_return iptables_bigstep_nz.skip)
next
  case (log rs t mx)
  have ac: "all_chains (no_call_to c) Γ rs"
    using log(4) by(simp add: all_chains_def no_call_to_def)
  have *: "Γ(c ↦ Rule mx Log # rs⇩1 @ Rule m' Return # rs⇩2),γ,p⊢ [Rule m (Call c)] ⇒⇩z Undecided"
    if "rs = rs⇩1 @ Rule m' Return # rs⇩2" "matches γ m' p" 
       "Γ(c ↦ rs⇩1 @ Rule m' Return # rs⇩2),γ,p⊢ rs⇩1 ⇒⇩z Undecided"
    for rs⇩1 rs⇩2 m'
  proof -
    have ac2: "all_chains (no_call_to c) Γ rs⇩1" using log(4) that
      by(simp add: all_chains_def no_call_to_def)
    hence "Γ(c ↦ Rule mx Log # rs⇩1 @ Rule m' Return # rs⇩2),γ,p⊢ rs⇩1 ⇒⇩z Undecided"
      using that(3) unfolding that by(simp add: all_chains_no_call_upd)
        hence "Γ(c ↦ Rule mx Log # rs⇩1 @ Rule m' Return # rs⇩2),γ,p⊢ Rule mx Log # rs⇩1 ⇒⇩z Undecided"
      by (simp add: log_nz)
    thus ?thesis using that(1,2)
      by(elim iptables_bigstep_nz.call_return[where rs⇩2=rs⇩2, OF ‹matches γ m p›, rotated]; simp add: iptables_bigstep_nz.skip)
  qed
  from log(2)[OF log(3) ac] show ?case
    apply -
    apply(drule upd_callD[OF _ ‹matches γ m p›])
    apply(erule disjE)
    subgoal
      apply(rule updated_call[OF _ ‹matches γ m p›])
      apply(rule log_nz)
      apply(simp add: ac all_chains_no_call_upd)
      done
    using * by blast
next
  case (empty rs t mx) text‹analogous› (*<*)
  have ac: "all_chains (no_call_to c) Γ rs"
    using empty(4) by(simp add: all_chains_def no_call_to_def)
  have *: "Γ(c ↦ Rule mx Empty # rs⇩1 @ Rule m' Return # rs⇩2),γ,p⊢ [Rule m (Call c)] ⇒⇩z Undecided"
    if "rs = rs⇩1 @ Rule m' Return # rs⇩2" "matches γ m' p" 
       "Γ(c ↦ rs⇩1 @ Rule m' Return # rs⇩2),γ,p⊢ rs⇩1 ⇒⇩z Undecided"
    for rs⇩1 rs⇩2 m'
  proof -
    have ac2: "all_chains (no_call_to c) Γ rs⇩1" using empty(4) that
      by(simp add: all_chains_def no_call_to_def)
    hence "Γ(c ↦ Rule mx Empty # rs⇩1 @ Rule m' Return # rs⇩2),γ,p⊢ rs⇩1 ⇒⇩z Undecided"
      using that(3) unfolding that by(simp add: all_chains_no_call_upd)
        hence "Γ(c ↦ Rule mx Empty # rs⇩1 @ Rule m' Return # rs⇩2),γ,p⊢ Rule mx Empty # rs⇩1 ⇒⇩z Undecided"
      by (simp add: empty_nz)
    thus ?thesis using that(1,2)
      by(elim iptables_bigstep_nz.call_return[where rs⇩2=rs⇩2, OF ‹matches γ m p›, rotated]; simp add: iptables_bigstep_nz.skip)
  qed
  from empty(2)[OF empty(3) ac] show ?case
    apply -
    apply(drule upd_callD[OF _ ‹matches γ m p›])
    apply(erule disjE)
    subgoal
      apply(rule updated_call[OF _ ‹matches γ m p›])
      apply(rule empty_nz)
      apply(simp add: ac all_chains_no_call_upd)
      done
    using * by blast
    (*>*)
next
  case (nms m' rs t a)
  have ac: "all_chains (no_call_to c) Γ rs" using nms(5) by(simp add: all_chains_def no_call_to_def)
  from nms.IH[OF nms(4) ac] show ?case
    apply -
    apply(drule upd_callD[OF _ ‹matches γ m p›])
    apply(erule disjE)
    subgoal
      apply(rule updated_call[OF _ ‹matches γ m p›])
      apply(rule iptables_bigstep_nz.nms[OF ‹¬ matches γ m' p›])
      apply(simp add: ac all_chains_no_call_upd)
      done
    apply safe
    subgoal for rs⇩1 rs⇩2 r
      apply(subgoal_tac "all_chains (no_call_to c) Γ rs⇩1") (* Ich kann auch anders. *)
       apply(subst (asm) all_chains_no_call_upd, assumption)
       apply(subst (asm) all_chains_no_call_upd[symmetric], assumption)
       apply(drule iptables_bigstep_nz.nms[where a=a, OF ‹¬ matches γ m' p›])
       apply(erule (1) iptables_bigstep_nz.call_return[where rs⇩2=rs⇩2, OF ‹matches γ m p›, rotated])
        apply(insert ac; simp add: all_chains_def no_call_to_def iptables_bigstep_nz.skip)+
      done
    done
next
  case (call_result m' c' rs X rrs)
  have acrs: "all_chains (no_call_to c) Γ rs" using call_result(2,6) by(simp add: all_chains_def no_call_to_def)
  have cc: "c ≠ c'" (* okay, this one is a bit nifty… *) using call_result(6) by(simp add: all_chains_def no_call_to_def)
  have "Γ(c ↦ rs),γ,p⊢ [Rule m (Call c)] ⇒⇩z Decision X" using call_result.IH call_result.prems(1) acrs by blast
  then show ?case
    apply -
    apply(drule upd_callD[OF _ ‹matches γ m p›])
    apply(erule disjE)
    subgoal
      apply(rule updated_call[OF _ ‹matches γ m p›])
      apply(rule iptables_bigstep_nz.call_result[where rs=rs, OF ‹matches γ m' p› ])
      apply(simp add: cc[symmetric] call_result(2);fail)
      apply(simp add: acrs all_chains_no_call_upd;fail)
      done
    apply safe (* oh. Didn't expect that. :) *)
  done
next
  case (call_no_result c' rs rrs t m')
  have acrs: "all_chains (no_call_to c) Γ rs" using call_no_result(1,7) by(simp add: all_chains_def no_call_to_def)
  have acrrs: "all_chains (no_call_to c) Γ rrs" using call_no_result(7) by(simp add: all_chains_def no_call_to_def)
  have acrs1: "all_chains (no_call_to c) Γ rs⇩1" if "rs = rs⇩1 @ rs⇩2" for rs⇩1 rs⇩2
    using acrs that by(simp add: all_chains_def no_call_to_def)
  have acrrs1: "all_chains (no_call_to c) Γ rs⇩1" if "rrs = rs⇩1 @ rs⇩2" for rs⇩1 rs⇩2
    using acrrs that by(simp add: all_chains_def no_call_to_def)
  have cc: "c ≠ c'" (* okay, this one is a bit nifty… *) using call_no_result(7) by(simp add: all_chains_def no_call_to_def)
  have *: "Γ(c ↦ rs),γ,p⊢ [Rule m (Call c)] ⇒⇩z Undecided" using call_no_result.IH call_no_result.prems(1) acrs by blast
  have **: "Γ(c ↦ rrs),γ,p⊢ [Rule m (Call c)] ⇒⇩z t" by (simp add: acrrs call_no_result.IH(2) call_no_result.prems(1))
  show ?case proof(cases ‹matches γ m' p›)
    case True
    from call_no_result(5)[OF ‹matches γ m p› acrrs] * show ?thesis
      apply -
      apply(drule upd_callD[OF _ ‹matches γ m p›])+
      apply(elim disjE) (* 4 sg *)
      apply safe
      subgoal
        apply(rule updated_call[OF _ ‹matches γ m p›])
        apply(rule iptables_bigstep_nz.call_no_result[where rs=rs, OF ‹matches γ m' p› ])
        apply(simp add: cc[symmetric] call_no_result(1);fail)
         apply(simp add: acrs all_chains_no_call_upd;fail)
        apply(simp add: acrrs all_chains_no_call_upd)
        done
      subgoal for rs⇩1 rs⇩2 r
        apply(rule updated_call[OF _ ‹matches γ m p›])
        apply(rule call_return[OF ‹matches γ m' p›])
           apply(simp add: cc[symmetric] call_no_result(1);fail)
          apply(simp;fail)
         apply(simp add: acrs1 all_chains_no_call_upd;fail)
        apply(simp add: acrrs all_chains_no_call_upd)
        done
      subgoal for rs⇩1 rs⇩2 r
        apply(rule call_return[where rs⇩1="Rule m' (Call c') # rs⇩1", OF ‹matches γ m p›])
           apply(simp;fail)
          apply(simp;fail)
        apply(rule iptables_bigstep_nz.call_no_result[OF ‹matches γ m' p›])
           apply(simp add: cc[symmetric] call_no_result(1);fail)
          apply (meson acrs all_chains_no_call_upd)
         apply(subst all_chains_no_call_upd; simp add: acrrs1 all_chains_no_call_upd; fail)
        apply (simp add: iptables_bigstep_nz.skip;fail)
        done
      subgoal for rrs⇩1 rs⇩1 rrs⇩2 rs⇩2 rr r
         apply(rule call_return[where rs⇩1="Rule m' (Call c') # rrs⇩1", OF ‹matches γ m p›])
           apply(simp;fail)
          apply(simp;fail)
         apply(rule call_return[OF ‹matches γ m' p›])
            apply(simp add: cc[symmetric] call_no_result(1);fail)
           apply blast
          apply (meson acrs1 all_chains_no_call_upd)
         apply(subst all_chains_no_call_upd; simp add: acrrs1 all_chains_no_call_upd; fail)
        apply (simp add: iptables_bigstep_nz.skip;fail)
        done
      done
  next
    case False
    from iptables_bigstep_nz.nms[OF False] ** show ?thesis 
      apply -
      apply(drule upd_callD[OF _ ‹matches γ m p›])+
      apply(elim disjE)
      subgoal
        apply(rule updated_call[OF _ ‹matches γ m p›])
        apply(rule iptables_bigstep_nz.nms[OF False])
        apply(simp add: acrrs all_chains_no_call_upd)
        done
      apply safe
      subgoal for rs⇩1 rs⇩2 r
        apply(rule call_return[where rs⇩1="Rule m' (Call c') # rs⇩1", OF ‹matches γ m p›])
           apply(simp;fail)
          apply(simp;fail)
         apply(rule iptables_bigstep_nz.nms[OF False])
         apply(subst all_chains_no_call_upd; simp add: acrrs1 all_chains_no_call_upd; fail)
        apply(simp add: iptables_bigstep_nz.skip;fail)
        done
      done
  qed
qed
  
lemma r_skip_inv: "Γ,γ,p⊢ [] ⇒⇩r t ⟹ t = Undecided"
  by(subst (asm) iptables_bigstep_r.simps) auto
  
(* why did I do all this? essentially, because I thought this should be derivable: *)
lemma r_call_eq: "Γ c = Some rs ⟹ matches γ m p ⟹ Γ,γ,p⊢ [Rule m (Call c)] ⇒⇩r t ⟷ Γ,γ,p⊢ rs ⇒⇩r t"
(* and yes, there is a more general form of this lemma, but… meh. *)
  apply(rule iffI)
  subgoal
    apply(subst (asm) iptables_bigstep_r.simps)
    apply(auto dest: r_skip_inv)
  done
  subgoal
    apply(cases t)
     apply(erule iptables_bigstep_r.call_no_result)
      apply(simp;fail)
     apply(simp add: iptables_bigstep_r.skip;fail)
      apply(simp)
    apply(erule (2) iptables_bigstep_r.call_result)
  done
  by -

(* we can make the same formulation for the original semantics if we tread a bit more carefully *)
lemma call_eq: "Γ c = Some rs ⟹ matches γ m p ⟹ ∀r ∈ set rs. get_action r ≠ Return  ⟹ Γ,γ,p⊢ ⟨[Rule m (Call c)],s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs,s⟩ ⇒ t"
  apply(rule iffI)
  subgoal
    apply(subst (asm) iptables_bigstep.simps)
    apply (auto)
     apply (simp add: decision)
    apply(erule rules_singleton_rev_E; simp; metis callD in_set_conv_decomp rule.sel(2) skipD)
  done
  by (metis decision iptables_bigstep.call_result iptables_bigstep_deterministic state.exhaust)
  
theorem r_eq_orig: "⟦all_chains (no_call_to c) Γ rs; Γ c = Some rs⟧ ⟹
   Γ,γ,p⊢ rs ⇒⇩r t ⟷ Γ,γ,p⊢ ⟨[Rule MatchAny (Call c)], Undecided⟩ ⇒ t"
  apply(rule iffI)
  subgoal
    apply(drule f[where m=MatchAny, THEN c, THEN a])
      apply(simp;fail)
     apply(simp;fail)
    apply (metis fun_upd_triv)
    done  
  subgoal
    apply(subst r_call_eq[where m=MatchAny, symmetric])
      apply(simp;fail)
     apply(simp;fail)
    apply(erule b[THEN d, THEN e, OF _ refl refl refl])
    done
  done
    
lemma r_no_call: "Γ,γ,p⊢ Rule MatchAny (Call c)#rs ⇒⇩r t ⟹ Γ c = None ⟹ False"
  by(subst (asm) iptables_bigstep_r.simps) simp
    
lemma no_call: "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t ⟹ rs = [Rule MatchAny (Call c)] ⟹ s = Undecided ⟹ Γ c = None ⟹ False"
  by (meson b d e r_no_call)
  (*by(induction rule: iptables_bigstep.induct; clarsimp) (metis list_app_singletonE skipD)*)

private corollary r_eq_orig': assumes "∀rs ∈ ran Γ. no_call_to c rs"
  shows "Γ,γ,p⊢ [Rule MatchAny (Call c)] ⇒⇩r t ⟷ Γ,γ,p⊢ ⟨[Rule MatchAny (Call c)], Undecided⟩ ⇒ t"
(* if you really like symmetry *)
proof -
  show ?thesis proof (cases "Γ c")
    fix rs
    assume "Γ c = Some rs"
    moreover hence "all_chains (no_call_to c) Γ rs" using assms by (simp add: all_chains_def ranI)
    ultimately show ?thesis by(simp add: r_call_eq r_eq_orig)
  next
    assume "Γ c = None" thus ?thesis using r_no_call no_call by metis
  qed
qed
  
(* btw, we can still formulate a seq rules, but we have to tread a bit more carefully *)
lemma r_tail: assumes "Γ,γ,p⊢ rs1 ⇒⇩r Decision X" shows "Γ,γ,p⊢ rs1 @ rs2 ⇒⇩r Decision X"
proof -
  have "Γ,γ,p⊢ rs1 ⇒⇩r t ⟹ t = Decision X ⟹ Γ,γ,p⊢ rs1 @ rs2 ⇒⇩r Decision X" for t
    by(induction rule: iptables_bigstep_r.induct; simp add: iptables_bigstep_r.intros)
  thus ?thesis using assms by blast
qed
lemma r_seq: "Γ,γ,p⊢ rs1 ⇒⇩r Undecided ⟹ ∀r ∈ set rs1. ¬(get_action r = Return ∧ matches γ (get_match r) p)
   ⟹ Γ,γ,p⊢ rs2 ⇒⇩r t ⟹ Γ,γ,p⊢ rs1 @ rs2 ⇒⇩r t"
proof(induction rs1)
  case Nil
  then show ?case by simp
next
  case (Cons r rs1)
  have p2: "∀r∈set rs1. ¬ (get_action r = Return ∧ matches γ (get_match r) p)" 
           "¬(get_action r = Return ∧ matches γ (get_match r) p)"
    by (simp_all add: Cons.prems(2))
  from Cons.prems(1) p2(2) Cons.IH[OF _ p2(1) Cons.prems(3)] show ?case 
    by(cases rule: iptables_bigstep_r.cases; simp add: iptables_bigstep_r.intros)
qed

lemma r_appendD: "Γ,γ,p⊢ rs1 @ rs2 ⇒⇩r t ⟹ ∃s. Γ,γ,p⊢ rs1 ⇒⇩r s"
  proof(induction rs1)
    case (Cons r rs1)
    from Cons.prems Cons.IH show ?case by(cases rule: iptables_bigstep_r.cases) (auto intro: iptables_bigstep_r.intros)
  qed (meson iptables_bigstep_r.skip)

corollary iptables_bigstep_r_eq: assumes "∀rs ∈ ran Γ. no_call_to c rs" "A = Accept ∨ A = Drop"
  shows "Γ,γ,p⊢ [Rule MatchAny (Call c), Rule MatchAny A] ⇒⇩r t ⟷ Γ,γ,p⊢ ⟨[Rule MatchAny (Call c), Rule MatchAny A], Undecided⟩ ⇒ t"
(* if you really like the way we do our analyses *)
proof -
  show ?thesis proof (cases "Γ c")
    fix rs
    assume "Γ c = Some rs"
    moreover hence "all_chains (no_call_to c) Γ rs" using assms by (simp add: all_chains_def ranI)
    show ?thesis
      (* if this proof breaks, don't fix it. say 'meh' and re-prove this as a corollary of r_eq_orig''' with a stronger assumption *)
      apply(rule iffI[rotated])
       apply(erule seqE_cons)
       apply(subst (asm) r_eq_orig'[symmetric])
        apply (simp add: assms(1);fail)
       apply (meson assms(1) b d e r_eq_orig' seq'_cons) (* holy shi… *)
      apply(frule r_appendD[of _ _ _ "[Rule MatchAny (Call c)]" "[Rule MatchAny A]", simplified])
      apply(subst (asm) r_eq_orig')
        apply (simp add: assms(1);fail)
        apply(clarsimp)
      apply(subst (asm) r_eq_orig'[symmetric])
       apply (simp add: assms(1);fail)
      apply(subst (asm)(2) iptables_bigstep_r.simps)
      apply(subst (asm)(1) iptables_bigstep_r.simps)
      apply auto
         apply (metis append_Cons append_Nil assms(1) decision matches.simps(4) r_call_eq r_eq_orig' seq)
        apply (metis ‹all_chains (no_call_to c) Γ rs› calculation iptables_bigstep_deterministic option.inject r_eq_orig state.distinct(1))
      subgoal using ‹all_chains (no_call_to c) Γ rs› calculation iptables_bigstep_deterministic r_eq_orig by fastforce
      apply(subst (asm) r_eq_orig[rotated])
        apply(assumption)
      subgoal using ‹all_chains (no_call_to c) Γ rs› calculation by simp
      apply(erule seq'_cons)
      apply(subst (asm)(1) iptables_bigstep_r.simps)  
      apply(insert assms(2); auto simp add: iptables_bigstep.intros)
      done        
  next
    assume "Γ c = None" thus ?thesis using r_no_call no_call by (metis seqE_cons)
  qed
qed

(* now, you don't like that no_call_to assumption? this one's for you: *)
lemma ex_no_call: "finite S ⟹ ∃c. ∀(rs :: 'a rule list) ∈ S. no_call_to c rs"
(* If you want, you can put in ‹ran Γ› for S. *)
proof -
  assume fS: ‹finite S›
  define called_c where "called_c rs = {c. ∃m. Rule m (Call c) ∈ set rs}" for rs :: "'a rule list"
  define called_c' where "called_c' rs = set [c. r ← rs, c ← (case get_action r of Call c ⇒ [c] | _ ⇒ [])]"
    for rs :: "'a rule list"
  have cc: "called_c' rs = called_c rs" for rs
    unfolding called_c'_def called_c_def
    by(induction rs; simp add: Un_def) (auto; metis rule.collapse)      
  have f: "finite (called_c rs)" for rs unfolding cc[symmetric] called_c'_def by blast
  have ncc: "no_call_to c rs ⟷ c ∉ called_c rs" for c rs 
    by(induction rs; auto simp add: no_call_to_def called_c_def split: action.splits) (metis rule.collapse)
  have isu: "infinite (UNIV :: string set)" by (simp add: infinite_UNIV_listI)
  have ff: "finite (⋃rs ∈ S. called_c rs)" using f fS by simp
  then obtain c where ne: "c ∉ (⋃rs ∈ S. called_c rs)"
    by (blast dest: ex_new_if_finite[OF isu])
  thus ?thesis by(intro exI[where x=c]) (simp add: ncc)
  (* stupid way of proving something, once again… *)
qed

private lemma ex_no_call': "finite (dom Γ) ⟹ ∃c. Γ c = None ∧ (∀(rs :: 'a rule list) ∈ (ran Γ). no_call_to c rs)"
(* I want a corollary, and I need something a tad stronger… *)
proof -
  have *: "finite S ⟹ (dom M) = S ⟹ ∃m. M = map_of m" for M S
  proof(induction arbitrary: M rule: finite.induct)
    case emptyI
    then show ?case by(intro exI[where x=Nil]) simp
  next
    case (insertI A a)
    show ?case proof(cases "a ∈ A") (* stupid induction rule *)
      case True
      then show ?thesis using insertI by (simp add: insert_absorb)
    next
      case False
      hence "dom (M(a := None)) = A" using insertI.prems by simp
      from insertI.IH[OF this] obtain m where "M(a := None) = map_of m" ..
      then show ?thesis 
        by(intro exI[where x="(a, the (M a)) # m"]) (simp; metis domIff fun_upd_apply insertCI insertI.prems option.collapse)
    qed
  qed (* hm, thought that would give me what I want… *)
  have ran_alt: "ran f = (the o f) ` dom f" for f by(auto simp add: ran_def dom_def image_def)
  assume fD: ‹finite (dom Γ)›
  hence fS: ‹finite (ran Γ)› by(simp add: ran_alt)
  define called_c where "called_c rs = {c. ∃m. Rule m (Call c) ∈ set rs}" for rs :: "'a rule list"
  define called_c' where "called_c' rs = set [c. r ← rs, c ← (case get_action r of Call c ⇒ [c] | _ ⇒ [])]"
    for rs :: "'a rule list"
  have cc: "called_c' rs = called_c rs" for rs
    unfolding called_c'_def called_c_def
    by(induction rs; simp add: Un_def) (auto; metis rule.collapse)      
  have f: "finite (called_c rs)" for rs unfolding cc[symmetric] called_c'_def by blast
  have ncc: "no_call_to c rs ⟷ c ∉ called_c rs" for c rs 
    by(induction rs; auto simp add: no_call_to_def called_c_def split: action.splits) (metis rule.collapse) 
  have isu: "infinite (UNIV :: string set)" by (simp add: infinite_UNIV_listI)
  have ff: "finite (⋃rs ∈ ran Γ. called_c rs)" using f fS by simp
  hence fff: "finite (dom Γ ∪ (⋃rs ∈ ran Γ. called_c rs))" using fD by simp
  then obtain c where ne: "c ∉ (dom Γ ∪ (⋃rs ∈ ran Γ. called_c rs))" thm ex_new_if_finite
    by (metis UNIV_I isu set_eqI)
  thus ?thesis by(fastforce simp add: ncc)
qed
  
lemma all_chains_no_call_upd_r: "all_chains (no_call_to c) Γ rs ⟹ (Γ(c ↦ x)),γ,p⊢ rs ⇒⇩r t ⟷ Γ,γ,p⊢ rs ⇒⇩r t"
proof (rule iffI, goal_cases)
  case 1
  from 1(2,1) show ?case 
    by(induction rule: iptables_bigstep_r.induct; 
      (simp add: iptables_bigstep_r.intros no_call_to_def all_chains_def split: if_splits;fail)?)
next
  case 2
  from 2(2,1) show ?case 
    by(induction rule: iptables_bigstep_r.induct; 
      (simp add: iptables_bigstep_r.intros no_call_to_def all_chains_def split:  action.splits;fail)?)
qed

(* in a sense, this is code duplication with Ruleset_Update, but it's different enough that I can't use it. *)
lemma all_chains_no_call_upd_orig: "all_chains (no_call_to c) Γ rs ⟹ (Γ(c ↦ x)),γ,p⊢ ⟨rs,s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs,s⟩ ⇒ t"
proof (rule iffI, goal_cases)
  case 1
  from 1(2,1) show ?case 
    by(induction rs s t rule: iptables_bigstep.induct; 
      (simp add: iptables_bigstep.intros no_call_to_def all_chains_def split: if_splits;fail)?)
next
  case 2
  from 2(2,1) show ?case 
    by(induction rule: iptables_bigstep.induct; 
      (simp add: iptables_bigstep.intros no_call_to_def all_chains_def split:  action.splits;fail)?)
qed
  
  
corollary r_eq_orig''': assumes "finite (ran Γ)" and "∀r ∈ set rs. get_action r ≠ Return"
  shows "Γ,γ,p⊢ rs ⇒⇩r t ⟷ Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ t"
proof -
  from assms have "finite ({rs} ∪ (ran Γ))" by simp
  from ex_no_call[OF this] obtain c where c: "(∀rs∈ran Γ. no_call_to c rs)" "no_call_to c rs" by blast
  hence acnc: "all_chains (no_call_to c) Γ rs" unfolding all_chains_def by (simp add: ranI)
  have ranaway: "∀rs∈ran (Γ(c ↦ rs)). no_call_to c rs"
  proof -
    { (* hammer *)
      fix rsa :: "'a rule list"
      assume a1: "rsa ∈ ran (Γ(c ↦ rs))"
      have "⋀R. rs ∈ R ∪ Collect (no_call_to c)"
        using c(2) by force
      then have "rsa ∈ ran (Γ(c := None)) ∪ Collect (no_call_to c)"
        using a1 by (metis (no_types) Un_iff Un_insert_left fun_upd_same fun_upd_upd insert_absorb ran_map_upd)
      then have "no_call_to c rsa"
        by (metis (no_types) Un_iff c(1) mem_Collect_eq ranI ran_restrictD restrict_complement_singleton_eq)
    }
    thus ?thesis by simp
  qed
  have "Γ(c ↦ rs),γ,p⊢ rs ⇒⇩r t ⟷ Γ(c ↦ rs),γ,p⊢ ⟨rs, Undecided⟩ ⇒ t"
    apply(subst r_call_eq[where c=c and m=MatchAny,symmetric])
      apply(simp;fail)
     apply(simp;fail)
    apply(subst call_eq[where c=c and m=MatchAny,symmetric])
      apply(simp;fail)
      apply(simp;fail)
     apply(simp add: assms;fail)
    apply(rule r_eq_orig')
    apply(fact ranaway)
    done
  thus ?thesis 
    apply -
    apply(subst (asm) all_chains_no_call_upd_r[where x=rs, OF acnc])
    apply(subst (asm) all_chains_no_call_upd_orig[where x=rs, OF acnc])
    .
qed

end

end