Theory Semantics_Goto

theory Semantics_Goto
imports Main Firewall_Common "Common/List_Misc" "HOL-Library.LaTeXsugar"
begin

section‹Big Step Semantics with Goto›
text‹
  We extend the iptables semantics to support the goto action.
  A goto directly continues processing at the start of the called chain.
  It does not change the call stack.
  In contrast to calls, goto does not return.
  Consequently, everything behind a matching goto cannot be reached.
›
text‹
  This theory is structured as follows.
  Fist, the goto semantics are introduced.
  Then, we show that those semantics are deterministic.
  Finally, we present two methods to remove gotos.
   The first unfolds goto.
   The second replaces gotos with calls.
  Finally, since the goto rules makes all proofs quite ugly, we never mention the goto semantics again.
  As we have shown, we can get rid of the gotos easily, thus, we stick to the nicer iptables semantics without goto.
›

context
begin
  
  subsection‹Semantics›
    private type_synonym 'a ruleset = "string  'a rule list"
    
    private type_synonym ('a, 'p) matcher = "'a  'p  bool"
    
    qualified fun matches :: "('a, 'p) matcher  'a match_expr  'p  bool" where
      "matches γ (MatchAnd e1 e2) p  matches γ e1 p  matches γ e2 p" |
      "matches γ (MatchNot me) p  ¬ matches γ me p" |
      "matches γ (Match e) p  γ e p" |
      "matches _ MatchAny _  True"
    
    
    (*
    main:
      call foo
      deny-all
    foo:
      goto bar
    bar:
      [nothing]
    
    The call returns, even if a goto is executed in the called chains. The deny-all will be executed!
    
    Chain OUTPUT (policy ACCEPT 98 packets, 34936 bytes)
     pkts bytes target     prot opt in     out     source               destination         
        1    84            all  --  *      *       0.0.0.0/0            127.42.0.1          
        1    84 foo        all  --  *      *       0.0.0.0/0            127.42.0.1          
        1    84            all  --  *      *       0.0.0.0/0            127.42.0.1          
    
    Chain bar (1 references)
     pkts bytes target     prot opt in     out     source               destination         
    
    Chain foo (1 references)
     pkts bytes target     prot opt in     out     source               destination         
        1    84 bar        all  --  *      *       0.0.0.0/0            0.0.0.0/0           [goto] 
    
    *)
    qualified fun no_matching_Goto :: "('a, 'p) matcher  'p  'a rule list  bool" where
      "no_matching_Goto _ _ []  True" |
      "no_matching_Goto γ p ((Rule m (Goto _))#rs)  ¬ matches γ m p  no_matching_Goto γ p rs" |
      "no_matching_Goto γ p (_#rs)  no_matching_Goto γ p rs"
    
    inductive iptables_goto_bigstep :: "'a ruleset  ('a, 'p) matcher  'p  'a rule list  state  state  bool"
      ("_,_,_g _, _  _"  [60,60,60,20,98,98] 89)
      for Γ and γ and p where
    skip:    "Γ,γ,pg [], t  t" |
    accept:  "matches γ m p  Γ,γ,pg [Rule m Accept], Undecided  Decision FinalAllow" |
    drop:    "matches γ m p  Γ,γ,pg [Rule m Drop], Undecided  Decision FinalDeny" |
    reject:  "matches γ m p   Γ,γ,pg [Rule m Reject], Undecided  Decision FinalDeny" |
    log:     "matches γ m p  Γ,γ,pg [Rule m Log], Undecided  Undecided" |
    empty:   "matches γ m p  Γ,γ,pg [Rule m Empty], Undecided  Undecided" |
    nomatch: "¬ matches γ m p  Γ,γ,pg [Rule m a], Undecided  Undecided" |
    decision: "Γ,γ,pg rs, Decision X  Decision X" |
    seq:      "Γ,γ,pg rs1, Undecided  t; Γ,γ,pg rs2, t  t'; no_matching_Goto γ p rs1  Γ,γ,pg rs1@rs2, Undecided  t'" |
    call_return:  " matches γ m p; Γ chain = Some (rs1@[Rule m' Return]@rs2);
                     matches γ m' p; Γ,γ,pg rs1, Undecided  Undecided;
                     no_matching_Goto γ p rs1 
                     ― ‹we do not support a goto in the first part if you want to return›
                     ― ‹probably unhandled case:›
                     ― ‹‹main:›
                     ― ‹‹  call foo›
                     ― ‹‹foo:›
                     ― ‹‹  goto bar›
                     ― ‹‹bar:›
                     ― ‹  Return //returns to ‹call foo›
                     ― ‹But this would be a really awkward ruleset!›
                   Γ,γ,pg [Rule m (Call chain)], Undecided  Undecided" |
    call_result:  " matches γ m p; Γ chain = Some rs; Γ,γ,pg rs, Undecided  t  
                   Γ,γ,pg [Rule m (Call chain)], Undecided  t" | ― ‹goto handling here seems okay›
    goto_decision:  " matches γ m p; Γ chain = Some rs; Γ,γ,pg rs, Undecided  Decision X  
                   Γ,γ,pg (Rule m (Goto chain))#rest, Undecided  Decision X" |
    goto_no_decision:  " matches γ m p; Γ chain = Some rs; Γ,γ,pg rs, Undecided  Undecided  
                   Γ,γ,pg (Rule m (Goto chain))#rest, Undecided  Undecided"
    
    text‹
    The semantic rules again in pretty format:
    \begin{center}
    @{thm[mode=Axiom] skip [no_vars]}\\[1ex]
    @{thm[mode=Rule] accept [no_vars]}\\[1ex]
    @{thm[mode=Rule] drop [no_vars]}\\[1ex]
    @{thm[mode=Rule] reject [no_vars]}\\[1ex]
    @{thm[mode=Rule] log [no_vars]}\\[1ex]
    @{thm[mode=Rule] empty [no_vars]}\\[1ex]
    @{thm[mode=Rule] nomatch [no_vars]}\\[1ex]
    @{thm[mode=Rule] decision [no_vars]}\\[1ex]
    @{thm[mode=Rule] seq [no_vars]} \\[1ex]
    @{thm[mode=Rule] call_return [no_vars]}\\[1ex] 
    @{thm[mode=Rule] call_result [no_vars]}\\[1ex] 
    @{thm[mode=Rule] goto_decision [no_vars]}\\[1ex] 
    @{thm[mode=Rule] goto_no_decision [no_vars]}
    \end{center}
›
    
    private lemma deny:
      "matches γ m p  a = Drop  a = Reject  iptables_goto_bigstep Γ γ p [Rule m a] Undecided (Decision FinalDeny)"
    by (auto intro: drop reject)
    
    
    private lemma iptables_goto_bigstep_induct
      [case_names
        Skip Allow Deny Log Nomatch Decision Seq Call_return Call_result Goto_Decision Goto_no_Decision,
       induct pred: iptables_goto_bigstep]:
    " Γ,γ,pg rs,s  t;
       t. P [] t t;
       m a. matches γ m p  a = Accept  P [Rule m a] Undecided (Decision FinalAllow);
       m a. matches γ m p  a = Drop  a = Reject  P [Rule m a] Undecided (Decision FinalDeny);
       m a. matches γ m p  a = Log  a = Empty  P [Rule m a] Undecided Undecided;
       m a. ¬ matches γ m p  P [Rule m a] Undecided Undecided;
       rs X. P rs (Decision X) (Decision X);
       rs rs1 rs2 t t'. rs = rs1 @ rs2  Γ,γ,pg rs1,Undecided  t  P rs1 Undecided t  
                          Γ,γ,pg rs2,t  t'  P rs2 t t'  no_matching_Goto γ p rs1  
                          P rs Undecided t';
       m a chain rs1 m' rs2. matches γ m p  a = Call chain 
                              Γ chain = Some (rs1 @ [Rule m' Return] @ rs2) 
                              matches γ m' p  Γ,γ,pg rs1,Undecided  Undecided 
                              no_matching_Goto γ p rs1   P rs1 Undecided Undecided 
                              P [Rule m a] Undecided Undecided;
       m a chain rs t. matches γ m p  a = Call chain  Γ chain = Some rs 
                         Γ,γ,pg rs,Undecided  t  P rs Undecided t  P [Rule m a] Undecided t;
       m a chain rs rest X. matches γ m p  a = Goto chain  Γ chain = Some rs 
                              Γ,γ,pg rs,Undecided  (Decision X)  P rs Undecided (Decision X) 
                              P (Rule m a#rest) Undecided (Decision X);
       m a chain rs rest. matches γ m p  a = Goto chain  Γ chain = Some rs 
                           Γ,γ,pg rs,Undecided  Undecided  P rs Undecided Undecided 
                           P (Rule m a#rest) Undecided Undecided 
     P rs s t"
    by (induction rule: iptables_goto_bigstep.induct) auto


  
  subsubsection‹Forward reasoning›
  
    private lemma decisionD: "Γ,γ,pg r, s  t  s = Decision X  t = Decision X"
      by (induction rule: iptables_goto_bigstep_induct) auto
    
    private lemma iptables_goto_bigstep_to_undecided: "Γ,γ,pg rs, s  Undecided  s = Undecided"
      by (metis decisionD state.exhaust)
    
    private lemma iptables_goto_bigstep_to_decision: "Γ,γ,pg rs, Decision Y  Decision X  Y = X"
      by (metis decisionD state.inject)
    
    
    private lemma skipD: "Γ,γ,pg r, s  t  r = []  s = t"
      by (induction rule: iptables_goto_bigstep.induct) auto
    
    
    private lemma gotoD: "Γ,γ,pg r, s  t  r = [Rule m (Goto chain)]  s = Undecided  matches γ m p 
                     rs. Γ chain = Some rs  Γ,γ,pg rs,s  t"
      by (induction rule: iptables_goto_bigstep.induct) (auto dest: skipD elim: list_app_singletonE)
    
    private lemma not_no_matching_Goto_singleton_cases: "¬ no_matching_Goto γ p [Rule m a]  ( chain. a = (Goto chain))  matches γ m p"
      by(case_tac a) (simp_all)
    
    private lemma no_matching_Goto_Cons: "no_matching_Goto γ p [r]  no_matching_Goto γ p rs  no_matching_Goto γ p (r#rs)"
      by(cases r)(rename_tac m a, case_tac a, simp_all)
    
    private lemma no_matching_Goto_head: "no_matching_Goto γ p (r#rs)  no_matching_Goto γ p [r]"
      by(cases r)(rename_tac m a, case_tac a, simp_all)
    private lemma no_matching_Goto_tail: "no_matching_Goto γ p (r#rs)  no_matching_Goto γ p rs"
      by(cases r)(rename_tac m a, case_tac a, simp_all)
    
    private lemma not_no_matching_Goto_cases:
      assumes "¬ no_matching_Goto γ p rs" "rs  []"
      shows "rs1 m chain rs2. rs = rs1@(Rule m (Goto chain))#rs2  no_matching_Goto γ p rs1  matches γ m p"
        using assms
        proof(induction rs)
        case Nil thus ?case by simp
        next
        case (Cons r rs)
          note Cons_outer=this
          from Cons have "¬ no_matching_Goto γ p (r # rs)" by simp
          show ?case
          proof(cases rs)
          case Nil
            obtain m a where "r = Rule m a" by (cases r) simp
            with ¬ no_matching_Goto γ p (r # rs) Nil not_no_matching_Goto_singleton_cases have "( chain. a = (Goto chain))  matches γ m p" by metis
            from this obtain chain where "a = (Goto chain)" and "matches γ m p" by blast
            have "r # rs = [] @ Rule m (Goto chain) # []" "no_matching_Goto γ p []" "matches γ m p"
              by (simp_all add: a = Goto chain r = Rule m a Nil matches γ m p)
            thus ?thesis by blast
          next
          case(Cons r' rs')
            with Cons_outer have "r # rs =  r # r' # rs'" by simp
            show ?thesis
            proof(cases"no_matching_Goto γ p [r]")
            case True 
              with ¬ no_matching_Goto γ p (r # rs) have "¬ no_matching_Goto γ p rs" by (meson no_matching_Goto_Cons)
              have "rs  []" using Cons by simp
              from Cons_outer(1)[OF ¬ no_matching_Goto γ p rs rs  []]
                obtain rs1 m chain rs2 where "rs = rs1 @ Rule m (Goto chain) # rs2" "no_matching_Goto γ p rs1" "matches γ m p" by blast
              with r # rs =  r # r' # rs' no_matching_Goto γ p [r] no_matching_Goto_Cons
                  have "r # rs = r # rs1 @ Rule m (Goto chain) # rs2  no_matching_Goto γ p (r#rs1)  matches γ m p" by fast
              thus ?thesis
                apply(rule_tac x="r#rs1" in exI)
                by auto
            next
            case False
              obtain m a where "r = Rule m a" by (cases r) simp
              with False not_no_matching_Goto_singleton_cases have "( chain. a = (Goto chain))  matches γ m p" by metis
              from this obtain chain where "a = (Goto chain)" and "matches γ m p" by blast
              have "r # rs = [] @ Rule m (Goto chain) # rs" "no_matching_Goto γ p []" "matches γ m p"
                by (simp_all add: a = Goto chain r = Rule m a matches γ m p)
              thus ?thesis by blast
            qed
          qed
        qed
    
    private lemma seq_cons_Goto_Undecided: 
      assumes "Γ,γ,pg [Rule m (Goto chain)], Undecided  Undecided"
      and "¬ matches γ m p  Γ,γ,pg rs, Undecided  Undecided"
      shows "Γ,γ,pg Rule m (Goto chain) # rs, Undecided  Undecided"
      proof(cases "matches γ m p")
        case True
          from True assms have "rs. Γ chain = Some rs  Γ,γ,pg rs, Undecided  Undecided" by(auto dest: gotoD)
          with True show ?thesis using goto_no_decision by fast
      next
        case False
        with assms have " Γ,γ,pg [Rule m (Goto chain)] @ rs, Undecided  Undecided" by(auto dest: seq)
        with False show ?thesis by simp
      qed

    private lemma seq_cons_Goto_t: 
      "Γ,γ,pg [Rule m (Goto chain)], Undecided  t  matches γ m p  Γ,γ,pg Rule m (Goto chain) # rs, Undecided  t"
       apply(frule gotoD)
          apply(simp_all)
       apply(clarify)
       apply(cases t)
        apply(auto intro: iptables_goto_bigstep.intros)
    done
    
    
    private lemma no_matching_Goto_append: "no_matching_Goto γ p (rs1@rs2)  no_matching_Goto γ p rs1   no_matching_Goto γ p rs2"
      by(induction γ p rs1 rule: no_matching_Goto.induct) (simp_all)
    
    private lemma no_matching_Goto_append1: "no_matching_Goto γ p (rs1@rs2)  no_matching_Goto γ p rs1"
      using no_matching_Goto_append by fast
    private lemma no_matching_Goto_append2: "no_matching_Goto γ p (rs1@rs2)  no_matching_Goto γ p rs2"
      using no_matching_Goto_append by fast
    
    private lemma seq_cons:
      assumes "Γ,γ,pg [r],Undecided  t" and "Γ,γ,pg rs,t  t'" and "no_matching_Goto γ p [r]"
      shows "Γ,γ,pg r#rs, Undecided  t'"
      proof -
        from assms have "Γ,γ,pg [r] @ rs, Undecided  t'" by (rule seq)
        thus ?thesis by simp
      qed
    
    context
      notes skipD[dest] list_app_singletonE[elim]
    begin
      lemma acceptD: "Γ,γ,pg r, s  t  r = [Rule m Accept]  matches γ m p  s = Undecided  t = Decision FinalAllow"
      by (induction rule: iptables_goto_bigstep.induct) auto
      
      lemma dropD: "Γ,γ,pg r, s  t  r = [Rule m Drop]  matches γ m p  s = Undecided  t = Decision FinalDeny"
      by (induction rule: iptables_goto_bigstep.induct) auto
      
      lemma rejectD: "Γ,γ,pg r, s  t  r = [Rule m Reject]  matches γ m p  s = Undecided  t = Decision FinalDeny"
      by (induction rule: iptables_goto_bigstep.induct) auto
      
      lemma logD: "Γ,γ,pg r, s  t  r = [Rule m Log]  matches γ m p  s = Undecided  t = Undecided"
      by (induction rule: iptables_goto_bigstep.induct) auto
      
      lemma emptyD: "Γ,γ,pg r, s  t  r = [Rule m Empty]  matches γ m p  s = Undecided  t = Undecided"
      by (induction rule: iptables_goto_bigstep.induct) auto
      
      lemma nomatchD: "Γ,γ,pg r, s  t  r = [Rule m a]  s = Undecided  ¬ matches γ m p  t = Undecided"
      by (induction rule: iptables_goto_bigstep.induct) auto
      
      lemma callD:
        assumes "Γ,γ,pg r, s  t" "r = [Rule m (Call chain)]" "s = Undecided" "matches γ m p" "Γ chain = Some rs"
        obtains "Γ,γ,pg rs,s  t"
              | rs1 rs2 m' where "rs = rs1 @ Rule m' Return # rs2" "matches γ m' p" "Γ,γ,pg rs1,s  Undecided" "no_matching_Goto γ p rs1" "t = Undecided"
        using assms
        proof (induction r s t arbitrary: rs rule: iptables_goto_bigstep.induct)
          case (seq rs1)
          thus ?case by (cases rs1) auto
        qed auto
    end
    
    private lemmas iptables_goto_bigstepD = skipD acceptD dropD rejectD logD emptyD nomatchD decisionD callD gotoD
    
    private lemma seq':
      assumes "rs = rs1 @ rs2" "Γ,γ,pg rs1,s  t" "Γ,γ,pg rs2,t  t'" and "no_matching_Goto γ p rs1"
      shows "Γ,γ,pg rs,s  t'"
      using assms by (cases s) (auto intro: seq decision dest: decisionD)
    
    
    private lemma seq'_cons: "Γ,γ,pg [r],s  t  Γ,γ,pg rs,t  t'  no_matching_Goto γ p [r]  Γ,γ,pg r#rs, s  t'"
      by (metis decision decisionD state.exhaust seq_cons)
    
    
    private lemma no_matching_Goto_take: "no_matching_Goto γ p rs  no_matching_Goto γ p  (take n rs)"
      apply(induction n arbitrary: rs)
       apply(simp_all)
      apply(rename_tac r rs)
      apply(case_tac rs)
       apply(simp_all)
      apply(rename_tac r' rs')
      apply(case_tac r')
      apply(simp)
      apply(rename_tac m a)
      by(case_tac a) (simp_all)
    
    private lemma seq_split:
      assumes "Γ,γ,pg rs, s  t" "rs = rs1@rs2"
      obtains (no_matching_Goto) t' where "Γ,γ,pg rs1,s  t'" "Γ,γ,pg rs2,t'  t" "no_matching_Goto γ p rs1"
            | (matching_Goto) "Γ,γ,pg rs1,s  t" "¬ no_matching_Goto γ p rs1"
    proof -
      have "(t'. Γ,γ,pg rs1,s  t'  Γ,γ,pg rs2,t'  t  no_matching_Goto γ p rs1)  (Γ,γ,pg rs1,s  t  ¬ no_matching_Goto γ p rs1)"
      using assms
      proof (induction rs s t arbitrary: rs1 rs2 rule: iptables_goto_bigstep_induct)
        case Skip thus ?case by (auto intro: iptables_goto_bigstep.intros simp add: accept)
      next
        case Allow thus ?case by (cases rs1) (auto intro: iptables_goto_bigstep.intros simp add: accept)
      next
        case Deny thus ?case by (cases rs1) (auto intro: iptables_goto_bigstep.intros simp add: deny)
      next
        case Log thus ?case by (cases rs1) (auto intro: iptables_goto_bigstep.intros simp add: log empty)
      next
        case Nomatch thus ?case by (cases rs1)
          (auto intro: iptables_goto_bigstep.intros simp add: not_no_matching_Goto_singleton_cases, meson nomatch not_no_matching_Goto_singleton_cases skip)
      next
        case Decision thus ?case by (auto intro: iptables_goto_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: "Γ,γ,pg take (length rsa) rs1, Undecided  t"
              by simp
            from Seq.IH(2)[OF longer(2)] have IH:
              "(t'a. Γ,γ,pg drop (length rsa) rs1, t  t'a  Γ,γ,pg rs2, t'a  t'  no_matching_Goto γ p (drop (length rsa) rs1)) 
               Γ,γ,pg drop (length rsa) rs1, t  t'  ¬ no_matching_Goto γ p (drop (length rsa) rs1)" (is "?IH_no_Goto  ?IH_Goto") by simp
            thus ?thesis
              proof(rule disjE)
                assume IH: ?IH_no_Goto
                from IH obtain t2
                  where t2a: "Γ,γ,pg drop (length rsa) rs1,t  t2"
                    and rs_part2: "Γ,γ,pg rs2,t2  t'"
                    and "no_matching_Goto γ p (drop (length rsa) rs1)"
                  by blast
                with t1 rs_part2 have rs_part1: "Γ,γ,pg take (length rsa) rs1 @ drop (length rsa) rs1, Undecided  t2"
                  using Seq.hyps(4) longer(1) seq by fastforce
                have "no_matching_Goto γ p (take (length rsa) rs1 @ drop (length rsa) rs1)"
                  using Seq.hyps(4) no_matching_Goto γ p (drop (length rsa) rs1) longer(1)
                        no_matching_Goto_append by fastforce 
                with Seq rs_part1 rs_part2 show ?thesis by auto
              next
                assume ?IH_Goto
                thus ?thesis by (metis Seq.hyps(2) Seq.hyps(4) append_take_drop_id longer(1) no_matching_Goto_append2 seq')
              qed
          next
            case shorter
            from shorter 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.hyps(4) rsa' no_matching_Goto_append2 have
                no_matching_Goto_rs2: "no_matching_Goto γ p (take (length rsa - length rs1) rs2)" by metis
    
            from rsb' Seq.hyps have t2: "Γ,γ,pg drop (length rsa - length rs1) rs2,t  t'"
              by blast
    
            from Seq.IH(1)[OF rsa'] have IH:
              "(t'. Γ,γ,pg rs1, Undecided  t'  Γ,γ,pg take (length rsa - length rs1) rs2, t'  t  no_matching_Goto γ p rs1) 
                Γ,γ,pg rs1, Undecided  t  ¬ no_matching_Goto γ p rs1" (is "?IH_no_Goto  ?IH_Goto") by simp
    
            thus ?thesis
              proof(rule disjE)
                assume IH: ?IH_no_Goto
                from IH obtain t1
                  where t1a: "Γ,γ,pg rs1,Undecided  t1"
                    and t1b: "Γ,γ,pg take (length rsa - length rs1) rs2,t1  t"
                    and "no_matching_Goto γ p rs1"
                  by blast
        
                  from no_matching_Goto_rs2 t2 seq' t1b have rs2: "Γ,γ,pg rs2,t1  t'"
                    by  fastforce
                  from t1a rs2 no_matching_Goto γ p rs1 show ?thesis by fast
              next
                assume ?IH_Goto
                thus ?thesis by (metis Seq.hyps(4) no_matching_Goto_append1 rsa') 
              qed
          qed
      next
        case Call_return
        hence "Γ,γ,pg rs1, Undecided  Undecided" "Γ,γ,pg rs2, Undecided  Undecided"
          by (case_tac [!] rs1) (auto intro: iptables_goto_bigstep.skip iptables_goto_bigstep.call_return)
        thus ?case by fast
      next
        case (Call_result _ _ _ _ t)
        show ?case
          proof (cases rs1)
            case Nil
            with Call_result have "Γ,γ,pg rs1, Undecided  Undecided" "Γ,γ,pg rs2, Undecided  t"
              by (auto intro: iptables_goto_bigstep.intros)
            thus ?thesis using local.Nil by auto 
          next
            case Cons
            with Call_result have "Γ,γ,pg rs1, Undecided  t" "Γ,γ,pg rs2, t  t"
              by (auto intro: iptables_goto_bigstep.intros)
            thus ?thesis by fast
          qed
      next
        case (Goto_Decision m a chain rs rest X)
        thus ?case
          proof (cases rs1)
            case Nil
            with Goto_Decision have "Γ,γ,pg rs1, Undecided  Undecided" "Γ,γ,pg rs2, Undecided  Decision X"
              by (auto intro: iptables_goto_bigstep.intros)
            thus ?thesis using local.Nil by auto
          next
            case Cons
            with Goto_Decision have "Γ,γ,pg rs1, Undecided  Decision X" "Γ,γ,pg rs2, Decision X  Decision X"
              by (auto intro: iptables_goto_bigstep.intros) 
            thus ?thesis by fast
          qed
      next
        case (Goto_no_Decision m a chain rs rest rs1)
        from Goto_no_Decision have rs1rs2: "Rule m (Goto chain) # rest = rs1 @ rs2" by simp
        from goto_no_decision[OF Goto_no_Decision(1)]  Goto_no_Decision(3)  Goto_no_Decision(4)
          have x: "rest. Γ,γ,pg Rule m (Goto chain) # rest, Undecided  Undecided" by simp
        show ?case
          proof (cases rs1)
            case Nil
            with Goto_no_Decision have "Γ,γ,pg rs1, Undecided  Undecided" "Γ,γ,pg rs2, Undecided  Undecided"
              by (auto intro: iptables_goto_bigstep.intros)
            thus ?thesis by fast
          next
            case (Cons rs1a rs1s)
            with rs1rs2 have "rs1 = Rule m (Goto chain) # (take (length rs1s) rest)" by simp
            from Cons rs1rs2 have"rs2 = drop (length rs1s) rest" by simp
            
            from Cons Goto_no_Decision have 1: "Γ,γ,pg rs1, Undecided  Undecided"
              using x by auto[1]
            have 2: "¬ no_matching_Goto γ p rs1"
              by (simp add: Goto_no_Decision.hyps(1) rs1 = Rule m (Goto chain) # take (length rs1s) rest) 
            from 1 2 show ?thesis by fast
          qed
      qed
    thus ?thesis using matching_Goto no_matching_Goto by blast 
    qed
    
    private lemma seqE:
      assumes "Γ,γ,pg rs1@rs2, s  t"
      obtains (no_matching_Goto) ti where "Γ,γ,pg rs1,s  ti" "Γ,γ,pg rs2,ti  t" "no_matching_Goto γ p rs1"
            | (matching_Goto) "Γ,γ,pg rs1,s  t" "¬ no_matching_Goto γ p rs1"
      using assms by (force elim: seq_split)
    
    private lemma seqE_cons:
      assumes "Γ,γ,pg r#rs, s  t"
      obtains (no_matching_Goto) ti where "Γ,γ,pg [r],s  ti" "Γ,γ,pg rs,ti  t" "no_matching_Goto γ p [r]"
            | (matching_Goto) "Γ,γ,pg [r],s  t" "¬ no_matching_Goto γ p [r]"
      using assms by (metis append_Cons append_Nil seqE)
    
    private lemma seqE_cons_Undecided:
      assumes "Γ,γ,pg r#rs, Undecided  t"
      obtains (no_matching_Goto) ti where "Γ,γ,pg [r],Undecided  ti" and "Γ,γ,pg rs,ti  t" and "no_matching_Goto γ p [r]"
            | (matching_Goto) m chain rs' where "r = Rule m (Goto chain)" and "Γ,γ,pg [Rule m (Goto chain)],Undecided  t" and "matches γ m p" "Γ chain = Some rs'"
      using assms
      proof(cases rule: seqE_cons)
      case no_matching_Goto thus ?thesis using local.that by simp
      next
      case matching_Goto
        from this(2) not_no_matching_Goto_singleton_cases[of γ p "(get_match r)" "(get_action r)", simplified] have
          "((chain. (get_action r) = Goto chain)  matches γ (get_match r) p)" by simp
        from this obtain chain m where r: "r = Rule m (Goto chain)" "matches γ m p" by(cases r) auto
        from matching_Goto r have "Γ,γ,pg [Rule m (Goto chain)],Undecided  t" by simp
        from gotoD[OF matching_Goto(1)] r matches γ m p obtain rs' where "Γ chain = Some rs'" by blast
      from local.that 
      show ?thesis using Γ chain = Some rs' Γ,γ,pg [Rule m (Goto chain)], Undecided  t r(1) r(2) by blast
    qed
    
    private lemma nomatch':
      assumes "r. r  set rs  ¬ matches γ (get_match r) p"
      shows "Γ,γ,pg rs, s  s"
      proof(cases s)
        case Undecided
        have "rset rs. ¬ matches γ (get_match r) p  Γ,γ,pg rs, Undecided  Undecided"
          proof(induction rs)
            case Nil
            thus ?case by (fast intro: skip)
          next
            case (Cons r rs)
            hence "Γ,γ,pg [r], Undecided  Undecided"
              by (cases r) (auto intro: nomatch)
            with Cons show ?case
              by (metis list.set_intros(1) list.set_intros(2) not_no_matching_Goto_singleton_cases rule.collapse seq'_cons)
          qed
        with assms Undecided show ?thesis by simp
      qed (blast intro: decision)
    
    private lemma no_free_return: assumes "Γ,γ,pg [Rule m Return], Undecided  t" and "matches γ m p" shows "False"
      proof -
      { fix a s
        have no_free_return_hlp: "Γ,γ,pg a,s  t  matches γ m p   s = Undecided  a = [Rule m Return]  False"
        proof (induction rule: iptables_goto_bigstep.induct)
          case (seq rs1)
          thus ?case
            by (cases rs1) (auto dest: skipD)
        qed simp_all
      } with assms show ?thesis by blast
      qed
  
  subsection‹Determinism›
    private lemma iptables_goto_bigstep_Undecided_Undecided_deterministic: 
      "Γ,γ,pg rs, Undecided  Undecided  Γ,γ,pg rs, Undecided  t  t = Undecided"
    proof(induction rs Undecided Undecided arbitrary: t rule: iptables_goto_bigstep_induct)
      case Skip thus ?case by(fastforce  dest: skipD logD emptyD nomatchD decisionD)
      next
      case Log thus ?case by(fastforce  dest: skipD logD emptyD nomatchD decisionD)
      next
      case Nomatch thus ?case by(fastforce  dest: skipD logD emptyD nomatchD decisionD)
      next
      case Seq thus ?case by (metis iptables_goto_bigstep_to_undecided seqE)
      next
      case (Call_return m a chain rs1 m' rs2) 
        from Call_return have " Γ,γ,pg [Rule m (Call chain)], Undecided  Undecided"
          apply(frule_tac rs1=rs1 and m'=m' and chain=chain in call_return)
              by(simp_all)
        with Call_return show ?case
          apply simp
          apply (metis callD no_free_return seqE seqE_cons)
          done
      next
      case Call_result thus ?case by (meson callD)
      next
      case Goto_no_Decision thus ?case by (metis gotoD no_matching_Goto.simps(2) option.sel seqE_cons)
    qed
    
    private lemma iptables_goto_bigstep_Undecided_deterministic:
      "Γ,γ,pg rs, Undecided  t  Γ,γ,pg rs, Undecided  t'   t' = t"
    proof(induction rs Undecided t arbitrary: t' rule: iptables_goto_bigstep_induct)
      case Skip thus ?case by(fastforce  dest: skipD logD emptyD nomatchD decisionD)
      next
      case Allow thus ?case by (auto dest: iptables_goto_bigstepD)
      next
      case Deny thus ?case by (auto dest: iptables_goto_bigstepD)
      next
      case Log thus ?case by (auto dest: iptables_goto_bigstepD)
      next
      case Nomatch thus ?case by (auto dest: iptables_goto_bigstepD)
      next
      case Seq thus ?case by (metis decisionD seqE state.exhaust)
      next
      case Call_return thus ?case by (meson call_return iptables_goto_bigstep_Undecided_Undecided_deterministic)
      next
      case Call_result thus ?case by (metis callD call_result iptables_goto_bigstep_Undecided_Undecided_deterministic)
      next
      case Goto_Decision thus ?case by (metis gotoD no_matching_Goto.simps(2) option.sel seqE_cons)
      next
      case Goto_no_Decision thus ?case by (meson goto_no_decision iptables_goto_bigstep_Undecided_Undecided_deterministic)
    qed
    
    qualified theorem iptables_goto_bigstep_deterministic: assumes "Γ,γ,pg rs, s  t" and "Γ,γ,pg rs, s  t'" shows "t = t'"
    using assms
      apply(cases s)
       apply(simp add: iptables_goto_bigstep_Undecided_deterministic)
      by(auto dest: decisionD)
  
  subsection‹Matching›
    
    private lemma matches_rule_and_simp_help:
      assumes "matches γ m p"
      shows "Γ,γ,pg [Rule (MatchAnd m m') a'], s  t  Γ,γ,pg [Rule m' a'], s  t" (is "?l ?r")
      proof
        assume ?l thus ?r
          by (induction "[Rule (MatchAnd m m') a']" s t rule: iptables_goto_bigstep_induct)
             (auto intro: iptables_goto_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
      next
        assume ?r thus ?l
          by (induction "[Rule m' a']" s t rule: iptables_goto_bigstep_induct)
             (auto intro: iptables_goto_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
      qed
    
    private lemma matches_MatchNot_simp: 
      assumes "matches γ m p"
      shows "Γ,γ,pg [Rule (MatchNot m) a], Undecided  t  Γ,γ,pg [], Undecided  t" (is "?l  ?r")
      proof
        assume ?l thus ?r
          by (induction "[Rule (MatchNot m) a]" "Undecided" t rule: iptables_goto_bigstep_induct)
             (auto intro: iptables_goto_bigstep.intros simp: assms Cons_eq_append_conv dest: skipD)
      next
        assume ?r
        hence "t = Undecided"
          by (metis skipD)
        with assms show ?l
          by (fastforce intro: nomatch)
      qed
    
    private lemma matches_MatchNotAnd_simp:
      assumes "matches γ m p"
      shows "Γ,γ,pg [Rule (MatchAnd (MatchNot m) m') a], Undecided  t  Γ,γ,pg [], Undecided  t" (is "?l  ?r")
      proof
        assume ?l thus ?r
          by (induction "[Rule (MatchAnd (MatchNot m) m') a]" "Undecided" t rule: iptables_goto_bigstep_induct)
             (auto intro: iptables_goto_bigstep.intros simp add: assms Cons_eq_append_conv dest: skipD)
      next
        assume ?r
        hence "t = Undecided"
          by (metis skipD)
        with assms show ?l
          by (fastforce intro: nomatch)
      qed
      
    private lemma matches_rule_and_simp:
      assumes "matches γ m p"
      shows "Γ,γ,pg [Rule (MatchAnd m m') a'], s  t  Γ,γ,pg [Rule m' a'], s  t"
      proof (cases s)
        case Undecided
        with assms show ?thesis
          by (simp add: matches_rule_and_simp_help)
      next
        case Decision
        thus ?thesis by (metis decision decisionD)
      qed
    
    
    
    qualified definition add_match :: "'a match_expr  'a rule list  'a rule list" where
      "add_match m rs = map (λr. case r of Rule m' a'  Rule (MatchAnd m m') a') rs"
    
    private lemma add_match_split: "add_match m (rs1@rs2) = add_match m rs1 @ add_match m rs2"
      unfolding add_match_def
      by (fact map_append)
    
    private lemma add_match_split_fst: "add_match m (Rule m' a' # rs) = Rule (MatchAnd m m') a' # add_match m rs"
      unfolding add_match_def
      by simp
    
    private lemma matches_add_match_no_matching_Goto_simp: "matches γ m p  no_matching_Goto γ p (add_match m rs)  no_matching_Goto γ p rs"
      apply(induction rs)
       apply(simp_all)
      apply(rename_tac r rs)
      apply(case_tac r)
      apply(simp add: add_match_split_fst no_matching_Goto_tail)
      apply(drule no_matching_Goto_head)
      apply(rename_tac m' a')
      apply(case_tac a')
              apply simp_all
      done
    
    
    private lemma matches_add_match_no_matching_Goto_simp2: "matches γ m p   no_matching_Goto γ p rs  no_matching_Goto γ p (add_match m rs)"
      apply(induction rs)
       apply(simp add: add_match_def)
      apply(rename_tac r rs)
      apply(case_tac r)
      apply(simp add: add_match_split_fst no_matching_Goto_tail)
      apply(rename_tac m' a')
      apply(case_tac a')
              apply simp_all
      done
    
    private lemma matches_add_match_MatchNot_no_matching_Goto_simp: "¬ matches γ m p  no_matching_Goto γ p (add_match m rs)"
      apply(induction rs)
       apply(simp add: add_match_def)
      apply(rename_tac r rs)
      apply(case_tac r)
      apply(simp add: add_match_split_fst no_matching_Goto_tail)
      apply(rename_tac m' a')
      apply(case_tac a')
              apply simp_all
      done
    
    
    private lemma not_matches_add_match_simp:
      assumes "¬ matches γ m p"
      shows "Γ,γ,pg add_match m rs, Undecided  t  Γ,γ,pg [], Undecided  t"
      proof(induction rs)
      case Nil thus ?case unfolding add_match_def by simp
      next
      case (Cons r rs)
        obtain m' a where r: "r = Rule m' a" by(cases r, simp)
        let ?lhs="Γ,γ,pg Rule (MatchAnd m m') a # add_match m rs, Undecided  t"
        let ?rhs="Γ,γ,pg [], Undecided  t"
        { assume ?lhs
          from ?lhs Cons have ?rhs
           proof(cases  Γ γ p "Rule (MatchAnd m m') a" "add_match m rs"  t rule: seqE_cons_Undecided)
           case (no_matching_Goto ti)
             hence "ti = Undecided"  by (simp add: assms nomatchD)
             with no_matching_Goto Cons show ?thesis by simp
           next
           case (matching_Goto) with Cons assms show ?thesis by force
         qed
        } note 1=this
        { assume ?rhs
          hence "t = Undecided" using skipD by metis
          with Cons.IH ?rhs have ?lhs 
           by (meson assms matches.simps(1) nomatch not_no_matching_Goto_singleton_cases seq_cons)  
        } with 1 show ?case by(auto simp add: r add_match_split_fst)
      qed
    
    private lemma matches_add_match_MatchNot_simp:
      assumes m: "matches γ m p"
      shows "Γ,γ,pg add_match (MatchNot m) rs, s  t  Γ,γ,pg [], s  t" (is "?l s  ?r s")
      proof (cases s)
        case Undecided
        have "?l Undecided  ?r Undecided"
          proof
            assume "?l Undecided" with m show "?r Undecided"
              proof (induction rs)
                case Nil
                thus ?case
                  unfolding add_match_def by simp
              next
                case (Cons r rs)
                thus ?case
                  by (cases r) (metis matches_MatchNotAnd_simp skipD seqE_cons add_match_split_fst)
              qed
          next
            assume "?r Undecided" with m show "?l Undecided"
              proof (induction rs)
                case Nil
                thus ?case
                  unfolding add_match_def by simp
              next
                case (Cons r rs)
                hence "t = Undecided" using skipD by metis
                with Cons show ?case
                  apply (cases r)
                  apply(simp add: add_match_split_fst)
                  by (metis matches.simps(1) matches.simps(2) matches_MatchNotAnd_simp not_no_matching_Goto_singleton_cases seq_cons)
              qed
          qed
        with Undecided show ?thesis by fast
      next
        case (Decision d)
        thus ?thesis
          by(metis decision decisionD)
      qed
    
    
    private lemma just_show_all_bigstep_semantics_equalities_with_start_Undecided: 
          "Γ,γ,pg rs1, Undecided  t  Γ,γ,pg rs2, Undecided  t  
           Γ,γ,pg rs1, s  t  Γ,γ,pg rs2, s  t"
      apply(cases s)
       apply(simp)
      apply(simp)
      using decision decisionD by fastforce
      
    private lemma matches_add_match_simp_helper:
      assumes m: "matches γ m p"
      shows "Γ,γ,pg add_match m rs, Undecided  t  Γ,γ,pg rs, Undecided  t" (is "?l  ?r")
      proof
        assume ?l with m show ?r
          proof (induction rs)
            case Nil
            thus ?case
              unfolding add_match_def by simp
          next
            case (Cons r rs)
             obtain m' a where r: "r = Rule m' a" by(cases r, simp)
             from Cons have " Γ,γ,pg Rule (MatchAnd m m') a # add_match m rs, Undecided  t"
               by(simp add: r add_match_split_fst)
             from this Cons have "Γ,γ,pg Rule m' a # rs, Undecided  t"
             proof(cases rule: seqE_cons_Undecided)
               case (no_matching_Goto ti)
                from no_matching_Goto(3) Cons.prems(1) not_no_matching_Goto_singleton_cases
                  have "no_matching_Goto γ p [Rule m' a]" by (metis matches.simps(1))
                with no_matching_Goto Cons show ?thesis
                 apply(simp add: matches_rule_and_simp)
                 apply(cases ti)
                  apply (simp add: seq'_cons)
                 by (metis decision decisionD seq'_cons)
               next
               case (matching_Goto) with Cons show ?thesis
                apply(clarify)
                apply(simp add: matches_rule_and_simp_help)
                by (simp add: seq_cons_Goto_t)
             qed
             thus ?case by(simp add: r)
          qed
      next
        assume ?r with m show ?l
          proof (induction rs)
            case Nil
            thus ?case
              unfolding add_match_def by simp
          next
            case (Cons r rs)
             obtain m' a where r: "r = Rule m' a" by(cases r, simp)
             from Cons have "Γ,γ,pg Rule m' a # rs, Undecided  t" by(simp add: r)
             from this have "Γ,γ,pg Rule (MatchAnd m m') a # add_match m rs, Undecided  t"
                proof(cases Γ γ p "Rule m' a" rs t rule: seqE_cons_Undecided)
                case (no_matching_Goto ti)
                  from no_matching_Goto Cons.prems matches_rule_and_simp[symmetric] have
                    "Γ,γ,pg [Rule (MatchAnd m m') a], Undecided  ti" by fast
                  with Cons.prems Cons.IH no_matching_Goto show ?thesis
                   apply(cases ti)
                    apply (metis matches.simps(1) not_no_matching_Goto_singleton_cases seq_cons)
                   apply (metis decision decisionD matches.simps(1) not_no_matching_Goto_singleton_cases seq_cons)
                   done
                next
                case (matching_Goto) with Cons show ?thesis
                  by (simp add: matches_rule_and_simp_help seq_cons_Goto_t)
             qed
             thus ?case by(simp add: r add_match_split_fst)
          qed
      qed
    
    
    private lemma matches_add_match_simp:
      "matches γ m p  Γ,γ,pg add_match m rs, s  t  Γ,γ,pg rs, s  t"
      apply(rule just_show_all_bigstep_semantics_equalities_with_start_Undecided)
      by(simp add: matches_add_match_simp_helper)
    
    private lemma not_matches_add_matchNot_simp:
      "¬ matches γ m p  Γ,γ,pg add_match (MatchNot m) rs, s  t  Γ,γ,pg rs, s  t"
      by (simp add: matches_add_match_simp)
    
  subsection‹Goto Unfolding›
    private lemma unfold_Goto_Undecided:
        assumes chain_defined: "Γ chain = Some rs" and no_matching_Goto_rs: "no_matching_Goto γ p rs"
        shows "Γ,γ,pg (Rule m (Goto chain))#rest, Undecided  t  Γ,γ,pg add_match m rs @ add_match (MatchNot m) rest, Undecided  t"
              (is "?l  ?r")
    proof
      assume ?l
      thus ?r
        proof(cases rule: seqE_cons_Undecided)
        case (no_matching_Goto ti)
          from no_matching_Goto have "¬ matches γ m p" by simp
          with no_matching_Goto have ti: "ti = Undecided" using nomatchD by metis
          from ¬ matches γ m p have "Γ,γ,pg add_match m rs, Undecided  Undecided"
            using not_matches_add_match_simp skip by fast
          from ¬ matches γ m p matches_add_match_MatchNot_no_matching_Goto_simp have "no_matching_Goto γ p (add_match m rs)" by force
          from no_matching_Goto ti have "Γ,γ,pg rest, Undecided  t" by simp
          with not_matches_add_matchNot_simp[OF ¬ matches γ m p] have "Γ,γ,pg add_match (MatchNot m) rest, Undecided  t" by simp
          show ?thesis
            by (meson Γ,γ,pg add_match (MatchNot m) rest, Undecided  t Γ,γ,pg add_match m rs, Undecided  Undecided no_matching_Goto γ p (add_match m rs) seq)
        next
        case (matching_Goto m chain rs')
          from matching_Goto gotoD assms have "Γ,γ,pg rs, Undecided  t" by fastforce
          hence 1: "Γ,γ,pg add_match m rs, Undecided  t" by (simp add: matches_add_match_simp matching_Goto(3))
          have 2: "Γ,γ,pg add_match (MatchNot m) rest, t  t" by (simp add: matches_add_match_MatchNot_simp matching_Goto(3) skip)
          from no_matching_Goto_rs matches_add_match_no_matching_Goto_simp2 matching_Goto have 3: "no_matching_Goto γ p (add_match m rs)" by fast
          from 1 2 3 show ?thesis using matching_Goto(1) seq by fastforce
        qed
    next
      assume ?r
      thus ?l
        proof(cases "matches γ m p")
        case True
          have "Γ,γ,pg rs, Undecided  t"
            by (metis True Γ,γ,pg add_match m rs @ add_match (MatchNot m) rest, Undecided  t
                matches_add_match_MatchNot_simp matches_add_match_simp_helper self_append_conv seq' seqE)
          show ?l
          apply(cases t)
           using goto_no_decision[OF True] chain_defined apply (metis Γ,γ,pg rs, Undecided  t)
          using goto_decision[OF True, of Γ chain rs _ rest] chain_defined apply (metis Γ,γ,pg rs, Undecided  t)
          done
        next
        case False
          with ?r have "Γ,γ,pg add_match (MatchNot m) rest, Undecided  t"
            by (metis matches_add_match_MatchNot_no_matching_Goto_simp not_matches_add_match_simp seqE skipD)
          with False have "Γ,γ,pg rest, Undecided  t" by (meson not_matches_add_matchNot_simp) 
          show ?l by (meson False Γ,γ,pg rest, Undecided  t nomatch not_no_matching_Goto_singleton_cases seq_cons)
        qed
    qed
    
    
    (*
    This theorem allows us to unfold the deepest goto in a ruleset.
    This can be iterated to get to the higher-level gotos.
    *)
    qualified theorem unfold_Goto:
        assumes chain_defined: "Γ chain = Some rs" and no_matching_Goto_rs: "no_matching_Goto γ p rs"
        shows "Γ,γ,pg (Rule m (Goto chain))#rest, s  t  Γ,γ,pg add_match m rs @ add_match (MatchNot m) rest, s  t"
      apply(rule just_show_all_bigstep_semantics_equalities_with_start_Undecided)
      using assms unfold_Goto_Undecided by fast
    
    
    
    text‹A chain that will definitely come to a direct decision›
    qualified fun terminal_chain :: "'a rule list  bool" where
      "terminal_chain [] = False" |
      "terminal_chain [Rule MatchAny Accept] = True" |
      "terminal_chain [Rule MatchAny Drop] = True" |
      "terminal_chain [Rule MatchAny Reject] = True" |
      "terminal_chain ((Rule _ (Goto _))#rs) = False" |
      "terminal_chain ((Rule _ (Call _))#rs) = False" |
      "terminal_chain ((Rule _ Return)#rs) = False" |
      "terminal_chain ((Rule _ Unknown)#rs) = False" |
      "terminal_chain (_#rs) = terminal_chain rs"
    
    private lemma terminal_chain_no_matching_Goto: "terminal_chain rs  no_matching_Goto γ p rs"
       by(induction rs rule: terminal_chain.induct)  simp_all
    
    text‹A terminal chain means (if the semantics are actually defined) that the chain will
         ultimately yield a final filtering decision, for all packets.›
    qualified lemma "terminal_chain rs  Γ,γ,pg rs, Undecided  t  X. t = Decision X"
            apply(induction rs)
             apply(simp)
            apply(rename_tac r rs)
            apply(case_tac r)
            apply(rename_tac m a)
            apply(simp)
            apply(frule_tac γ=γ and p=p in terminal_chain_no_matching_Goto)
            apply(case_tac a)
                    apply(simp_all)
                apply(erule seqE_cons, simp_all,
                       metis iptables_goto_bigstepD matches.elims terminal_chain.simps terminal_chain.simps terminal_chain.simps)+
            done
    
    private lemma replace_Goto_with_Call_in_terminal_chain_Undecided:
        assumes chain_defined: "Γ chain = Some rs" and terminal_chain: "terminal_chain rs"
        shows "Γ,γ,pg [Rule m (Goto chain)], Undecided  t  Γ,γ,pg [Rule m (Call chain)], Undecided  t"
              (is "?l  ?r")
      proof
        assume ?l
        thus ?r
          proof(cases rule: seqE_cons_Undecided)
          case (no_matching_Goto ti)
            from no_matching_Goto have "¬ matches γ m p" by simp
            with nomatch have 1: "Γ,γ,pg [Rule m (Goto chain)], Undecided  Undecided" by fast
            from ¬ matches γ m p nomatch have 2: "Γ,γ,pg [Rule m (Call chain)], Undecided  Undecided" by fast
            from 1 2 show ?thesis
              using ?l iptables_goto_bigstep_Undecided_Undecided_deterministic by fastforce 
          next
          case (matching_Goto m chain rs')
            from matching_Goto gotoD assms have "Γ,γ,pg rs, Undecided  t" by fastforce
            from call_result[OF matches γ m p chain_defined Γ,γ,pg rs, Undecided  t] show ?thesis
              by (metis matching_Goto(1) rule.sel(1))
          qed
      next
        assume ?r
        thus ?l
          proof(cases "matches γ m p")
          case True
            {fix rs1::"'a rule list" and  m' and rs2
              have "terminal_chain (rs1 @ Rule m' Return # rs2)  False"
              apply(induction rs1)
               apply(simp_all)
              apply(rename_tac r' rs')
              apply(case_tac r')
              apply(rename_tac m a)
              apply(simp_all)
              apply(case_tac a)
                      apply(simp_all)
                apply (metis append_is_Nil_conv hd_Cons_tl terminal_chain.simps)+
              done
            } note no_return=this
            have "Γ,γ,pg rs, Undecided  t"
              apply(rule callD[OF ?r _ _ True chain_defined])
                 apply(simp_all)
              using no_return terminal_chain by blast
            show ?l
              apply(cases t)
               using goto_no_decision[OF True] chain_defined apply (metis Γ,γ,pg rs, Undecided  t)
              using goto_decision[OF True, of Γ chain rs _ "[]"] chain_defined apply (metis Γ,γ,pg rs, Undecided  t)
              done
          next
          case False
            show ?l using False Γ,γ,pg [Rule m (Call chain)], Undecided  t nomatch nomatchD by fastforce 
          qed
      qed
    
  
  qualified theorem replace_Goto_with_Call_in_terminal_chain:
        assumes chain_defined: "Γ chain = Some rs" and terminal_chain: "terminal_chain rs"
        shows "Γ,γ,pg [Rule m (Goto chain)], s  t  Γ,γ,pg [Rule m (Call chain)], s  t"
      apply(rule just_show_all_bigstep_semantics_equalities_with_start_Undecided)
      using assms replace_Goto_with_Call_in_terminal_chain_Undecided by fast
  

  qualified fun rewrite_Goto_chain_safe :: "(string  'a rule list)  'a rule list  ('a rule list) option" where
    "rewrite_Goto_chain_safe _ [] = Some []" |
    "rewrite_Goto_chain_safe Γ ((Rule m (Goto chain))#rs) =
      (case (Γ chain) of None      None
                      |  Some rs'  (if
                                         ¬ terminal_chain rs'
                                      then
                                         None
                                      else
                                         map_option (λrs. Rule m (Call chain) # rs) (rewrite_Goto_chain_safe Γ rs)
                                     )
      )" |
    "rewrite_Goto_chain_safe Γ (r#rs) = map_option (λrs. r # rs) (rewrite_Goto_chain_safe Γ rs)"

  private fun rewrite_Goto_safe_internal
    :: "(string × 'a rule list) list  (string × 'a rule list) list  (string × 'a rule list) list option" where
    "rewrite_Goto_safe_internal _ [] = Some []" |
    "rewrite_Goto_safe_internal Γ ((chain_name, rs)#cs) = 
                (case rewrite_Goto_chain_safe (map_of Γ) rs of
                         None  None
                       | Some rs'  map_option (λrst. (chain_name, rs')#rst) (rewrite_Goto_safe_internal Γ cs)
                )"

  qualified fun rewrite_Goto_safe :: "(string × 'a rule list) list  (string × 'a rule list) list option" where
    "rewrite_Goto_safe cs = rewrite_Goto_safe_internal cs cs"


  (*use rewrite_Goto_chain_safe whenever possible!*)
  qualified definition rewrite_Goto :: "(string × 'a rule list) list  (string × 'a rule list) list" where
    "rewrite_Goto cs = the (rewrite_Goto_safe cs)"


  private lemma step_IH_cong: "(s. Γ,γ,pg rs1, s  t = Γ,γ,pg rs2, s  t) 
         Γ,γ,pg r#rs1, s  t = Γ,γ,pg r#rs2, s  t"
  apply(rule iffI)
   apply(erule seqE_cons)
    apply(rule seq'_cons)
      apply simp_all
   apply(drule not_no_matching_Goto_cases)
    apply(simp; fail)
   apply(elim exE conjE, rename_tac rs1a m chain rs2a)
   apply(subgoal_tac "r = Rule m (Goto chain)")
    prefer 2
    subgoal by (simp add: Cons_eq_append_conv)
   apply(thin_tac "[r] = _ @ Rule m (Goto chain) # _")
   apply simp
   apply (metis decision decisionD seq_cons_Goto_t state.exhaust)
  apply(erule seqE_cons)
   apply(rule seq'_cons)
     apply simp_all
  apply(drule not_no_matching_Goto_cases)
   apply(simp; fail)
  apply(elim exE conjE, rename_tac rs1a m chain rs2a)
  apply(subgoal_tac "r = Rule m (Goto chain)")
   prefer 2
   subgoal by (simp add: Cons_eq_append_conv)
  apply(thin_tac "[r] = _ @ Rule m (Goto chain) # _")
  apply simp
  apply (metis decision decisionD seq_cons_Goto_t state.exhaust)
  done

  private lemma terminal_chain_decision: 
    "terminal_chain rs  Γ,γ,pg rs, Undecided  t  X. t = Decision X"
    apply(induction rs arbitrary: t rule: terminal_chain.induct)
                                         apply simp_all
                                    apply(auto dest: iptables_goto_bigstepD)[3]
                                 apply(erule seqE_cons, simp_all, blast dest: iptables_goto_bigstepD)+ (*6s*)
    done
    

  private lemma terminal_chain_Goto_decision: "Γ chain = Some rs  terminal_chain rs  matches γ m p 
       Γ,γ,pg [Rule m (Goto chain)], s  t  X. t = Decision X"
    apply(cases s)
     apply(drule gotoD, simp_all)
     apply(elim exE conjE, simp_all)
     using terminal_chain_decision apply fast
    by (meson decisionD)
    

  qualified theorem rewrite_Goto_chain_safe:
    "rewrite_Goto_chain_safe Γ rs = Some rs'  Γ,γ,pg rs', s  t  Γ,γ,pg rs, s  t"
  proof(induction Γ rs arbitrary: rs' s rule: rewrite_Goto_chain_safe.induct)
  case 1 thus ?case by (simp split: option.split_asm if_split_asm)
  next
  case (2 Γ m chain rs) 
    from 2(2) obtain z x2 where "Γ chain = Some x2" and "terminal_chain x2"
            and "rs' = Rule m (Call chain) # z"
            and "Some z = rewrite_Goto_chain_safe Γ rs"
    by(auto split: option.split_asm if_split_asm)
    from 2(1) Γ chain = Some x2 terminal_chain x2 Some z = rewrite_Goto_chain_safe Γ rs 
      have IH: "Γ,γ,pg z, s  t = Γ,γ,pg rs, s  t" for s by simp

    have "Γ,γ,pg Rule m (Call chain) # z, Undecided  t  Γ,γ,pg Rule m (Goto chain) # rs, Undecided  t"
          (is "?lhs  ?rhs")
    proof(intro iffI)
      assume ?lhs
      with IH obtain ti where ti1: "Γ,γ,pg [Rule m (Call chain)], Undecided  ti" and ti2: "Γ,γ,pg rs, ti  t"
        by(auto elim: seqE_cons)
      show ?rhs
      proof(cases "matches γ m p")
      case False
        from replace_Goto_with_Call_in_terminal_chain Γ chain = Some x2 terminal_chain x2 
        have " Γ,γ,pg [Rule m (Call chain)], Undecided  ti  Γ,γ,pg [Rule m (Goto chain)], Undecided  ti"
          by fast
        with False ti1 ti2 show ?thesis by(rule_tac t=ti in seq'_cons) simp+
      next
      case True
        from ti1 Γ chain = Some x2 terminal_chain x2
        have g: "Γ,γ,pg [Rule m (Goto chain)], Undecided  ti"
          by(subst(asm) replace_Goto_with_Call_in_terminal_chain[symmetric]) simp+
        with True Γ chain = Some x2 terminal_chain x2 obtain X where X: "ti = Decision X"
          by(blast dest: terminal_chain_Goto_decision)
        with this ti2 have "t = Decision X"
          by(simp add: decisionD)
        with g X True ti2 Γ chain = Some x2 terminal_chain x2 show ?thesis
          apply(simp)
          apply(rule seq_cons_Goto_t, simp_all)
          done
      qed
    next
      assume ?rhs
      with IH Γ chain = Some x2 terminal_chain x2 Some z = rewrite_Goto_chain_safe Γ rs show ?lhs
        apply -
        apply(erule seqE_cons)
         subgoal for ti
         apply simp_all
         apply(rule_tac t=ti in seq'_cons)
           apply simp_all
         using replace_Goto_with_Call_in_terminal_chain by fast
        apply simp
        apply(frule(3) terminal_chain_Goto_decision)
        apply(subst(asm) replace_Goto_with_Call_in_terminal_chain, simp_all)
        apply(rule seq'_cons, simp_all)
        apply(elim exE)
        by (simp add: decision)
    qed
    with rs' = Rule m (Call chain) # z show ?case
      apply -
      apply(rule just_show_all_bigstep_semantics_equalities_with_start_Undecided)
      by simp

  qed(auto cong: step_IH_cong)
  


  text‹Example: The semantics are actually defined (for this example).›
  lemma defines "γ  (λ_ _. True)" and "m  MatchAny"
  shows "[''FORWARD''  [Rule m Log, Rule m (Call ''foo''), Rule m Drop],
          ''foo''  [Rule m Log, Rule m (Goto ''bar''), Rule m Reject],
          ''bar''  [Rule m (Goto ''baz''), Rule m Reject],
          ''baz''  [(Rule m Accept)]],
      γ,pg[Rule MatchAny (Call ''FORWARD'')], Undecided  (Decision FinalAllow)"
  apply(subgoal_tac "matches γ m p")
   prefer 2
   apply(simp add: γ_def m_def; fail)
  apply(rule call_result)
    apply(auto)
  apply(rule_tac t=Undecided in seq_cons)
    apply(auto intro: log)
  apply(rule_tac t="Decision FinalAllow" in seq_cons)
    apply(auto intro: decision)
  apply(rule call_result)
     apply(simp)+
  apply(rule_tac t=Undecided in seq_cons)
    apply(auto intro: log)
  apply(rule goto_decision)
    apply(simp)+
  apply(rule goto_decision)
    apply(simp)+
  apply(auto intro: accept)
  done


end


end