Theory Call_Return_Unfolding

theory Call_Return_Unfolding
imports Matching Ruleset_Update
  "Common/Repeat_Stabilize"
begin


section‹@{term Call} @{term Return} Unfolding›

text‹Remove @{term Return}s›
fun process_ret :: "'a rule list ⇒ 'a rule list" where
  "process_ret [] = []" |
  "process_ret (Rule m Return # rs) = add_match (MatchNot m) (process_ret rs)" |
  "process_ret (r#rs) = r # process_ret rs"


text‹Remove @{term Call}s›
fun process_call :: "'a ruleset ⇒ 'a rule list ⇒ 'a rule list" where
  "process_call Γ [] = []" |
  "process_call Γ (Rule m (Call chain) # rs) = add_match m (process_ret (the (Γ chain))) @ process_call Γ rs" |
  "process_call Γ (r#rs) = r # process_call Γ rs"

lemma process_ret_split_fst_Return:
  "a = Return ⟹ process_ret (Rule m a # rs) = add_match (MatchNot m) (process_ret rs)"
  by auto

lemma process_ret_split_fst_NeqReturn:
  "a ≠ Return ⟹ process_ret((Rule m a) # rs) = (Rule m a) # (process_ret rs)"
  by (cases a) auto

lemma add_match_simp: "add_match m = map (λr. Rule (MatchAnd m (get_match r)) (get_action r))"
by (auto simp: add_match_def cong: map_cong split: rule.split)

definition add_missing_ret_unfoldings :: "'a rule list ⇒ 'a rule list ⇒ 'a rule list" where
  "add_missing_ret_unfoldings rs1 rs2 ≡ 
  foldr (λrf acc. add_match (MatchNot (get_match rf)) ∘ acc) [r←rs1. get_action r = Return] id rs2"


fun MatchAnd_foldr :: "'a match_expr list ⇒ 'a match_expr" where
  "MatchAnd_foldr [] = undefined" | (*error, semantically, MatchAny would match*)
  "MatchAnd_foldr [e] = e" |
  "MatchAnd_foldr (e # es) = MatchAnd e (MatchAnd_foldr es)" 
fun add_match_MatchAnd_foldr :: "'a match_expr list ⇒ ('a rule list ⇒ 'a rule list)" where
  "add_match_MatchAnd_foldr [] = id" |
  "add_match_MatchAnd_foldr es = add_match (MatchAnd_foldr es)"

lemma add_match_add_match_MatchAnd_foldr:
  "Γ,γ,p⊢ ⟨add_match m (add_match_MatchAnd_foldr ms rs2), s⟩ ⇒ t = Γ,γ,p⊢ ⟨add_match (MatchAnd_foldr (m#ms)) rs2, s⟩ ⇒ t"
  proof (induction ms)
    case Nil
    show ?case by (simp add: add_match_def)
  next
    case Cons
    thus ?case by (simp add: iptables_bigstep_add_match_and)
  qed

lemma add_match_MatchAnd_foldr_empty_rs2: "add_match_MatchAnd_foldr ms [] = []"
  by (induction ms) (simp_all add: add_match_def)

lemma add_missing_ret_unfoldings_alt: "Γ,γ,p⊢ ⟨add_missing_ret_unfoldings rs1 rs2, s⟩ ⇒ t ⟷
  Γ,γ,p⊢ ⟨(add_match_MatchAnd_foldr (map (λr. MatchNot (get_match r)) [r←rs1. get_action r = Return])) rs2, s ⟩ ⇒ t"
  proof(induction rs1)
    case Nil
    thus ?case
      unfolding add_missing_ret_unfoldings_def by simp
  next
    case (Cons r rs)
    from Cons obtain m a where "r = Rule m a" by(cases r) (simp)
    with Cons show ?case
      unfolding add_missing_ret_unfoldings_def
      apply(cases "matches γ m p")
       apply (simp_all add: matches_add_match_simp matches_add_match_MatchNot_simp add_match_add_match_MatchAnd_foldr[symmetric])
      done
  qed

lemma add_match_add_missing_ret_unfoldings_rot:
  "Γ,γ,p⊢ ⟨add_match m (add_missing_ret_unfoldings rs1 rs2), s⟩ ⇒ t =  
   Γ,γ,p⊢ ⟨add_missing_ret_unfoldings (Rule (MatchNot m) Return#rs1) rs2, s⟩ ⇒ t"
  by(simp add: add_missing_ret_unfoldings_def iptables_bigstep_add_match_notnot_simp)


subsection‹Completeness›
lemma process_ret_split_obvious: "process_ret (rs⇩1 @ rs⇩2) = 
  (process_ret rs⇩1) @ (add_missing_ret_unfoldings rs⇩1 (process_ret rs⇩2))"
  unfolding add_missing_ret_unfoldings_def
  proof (induction rs⇩1 arbitrary: rs⇩2)
    case (Cons r rs)
    from Cons obtain m a where "r = Rule m a" by (cases r) simp
    with Cons.IH show ?case
      apply(cases a)
             apply(simp_all add: add_match_split)
      done
  qed simp

lemma add_missing_ret_unfoldings_emptyrs2: "add_missing_ret_unfoldings rs1 [] = []"
  unfolding add_missing_ret_unfoldings_def
  by (induction rs1) (simp_all add: add_match_def)

lemma process_call_split: "process_call Γ (rs1 @ rs2) = process_call Γ rs1 @ process_call Γ rs2"
  proof (induction rs1)
    case (Cons r rs1)
    thus ?case
      apply(cases r, rename_tac m a)
      apply(case_tac a)
              apply(simp_all)
      done
  qed simp

lemma process_call_split_fst: "process_call Γ (a # rs) = process_call Γ [a] @ process_call Γ rs"
  by (simp add: process_call_split[symmetric])


lemma iptables_bigstep_process_ret_undecided: "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ t"
proof (induction rs)
  case (Cons r rs)
  show ?case
    proof (cases r)
      case (Rule m' a')
      show "Γ,γ,p⊢ ⟨process_ret (r # rs), Undecided⟩ ⇒ t"
        proof (cases a')
          case Accept
          with Cons Rule show ?thesis
            by simp (metis acceptD decision decisionD nomatchD seqE_cons seq_cons)
        next
          case Drop
          with Cons Rule show ?thesis
            by simp (metis decision decisionD dropD nomatchD seqE_cons seq_cons)
        next
          case Log
          with Cons Rule show ?thesis
            by simp (metis logD nomatchD seqE_cons seq_cons)
        next
          case Reject
          with Cons Rule show ?thesis
            by simp (metis decision decisionD nomatchD rejectD seqE_cons seq_cons)
        next
          case (Call chain)
          from Cons.prems obtain ti where 1:"Γ,γ,p⊢ ⟨[r], Undecided⟩ ⇒ ti" and 2: "Γ,γ,p⊢ ⟨rs, ti⟩ ⇒ t" using seqE_cons by metis
          thus ?thesis
            proof(cases ti)
            case Undecided
              with Cons.IH 2 have IH: "Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ t" by simp
              from Undecided 1 Call Rule have "Γ,γ,p⊢ ⟨[Rule m' (Call chain)], Undecided⟩ ⇒ Undecided" by simp
              with IH  have" Γ,γ,p⊢ ⟨Rule m' (Call chain) # process_ret rs, Undecided⟩ ⇒ t" using seq'_cons by fast
              thus ?thesis using Rule Call by force
            next
            case (Decision X)
              with 1 Rule Call have "Γ,γ,p⊢ ⟨[Rule m' (Call chain)], Undecided⟩ ⇒ Decision X" by simp
              moreover from 2 Decision have "t = Decision X" using decisionD by fast
              moreover from decision have "Γ,γ,p⊢ ⟨process_ret rs, Decision X⟩ ⇒ Decision X" by fast
              ultimately show ?thesis using seq_cons by (metis Call Rule process_ret.simps(7))
            qed
        next
          case Return
          with Cons Rule show ?thesis
            by simp (metis matches.simps(2) matches_add_match_simp no_free_return nomatchD seqE_cons)
        next
          case Empty
          show ?thesis 
            apply (insert Empty Cons Rule)
            apply(erule seqE_cons)
            apply (rename_tac ti)
            apply(case_tac ti)
             apply (simp add: seq_cons)
            apply (metis Rule_DecisionE emptyD state.distinct(1))
            done
        next
          case Unknown
          show ?thesis using Unknown_actions_False
            by (metis Cons.IH Cons.prems Rule Unknown nomatchD process_ret.simps(10) seqE_cons seq_cons)
        next
          case Goto thus ?thesis  using Unknown_actions_False
            by (metis Cons.IH Cons.prems Rule Goto nomatchD process_ret.simps(8) seqE_cons seq_cons) 
        qed
    qed
qed simp


lemma add_match_rot_add_missing_ret_unfoldings:
  "Γ,γ,p⊢ ⟨add_match m (add_missing_ret_unfoldings rs1 rs2), Undecided⟩ ⇒ Undecided =
   Γ,γ,p⊢ ⟨add_missing_ret_unfoldings rs1 (add_match m rs2), Undecided⟩ ⇒ Undecided"
apply(simp add: add_missing_ret_unfoldings_alt add_match_add_missing_ret_unfoldings_rot add_match_add_match_MatchAnd_foldr[symmetric] iptables_bigstep_add_match_notnot_simp)
apply(cases "map (λr. MatchNot (get_match r)) [r←rs1 . (get_action r) = Return]")
 apply(simp_all add: add_match_distrib)
done

text ‹Completeness›
theorem unfolding_complete: "Γ,γ,p⊢ ⟨rs,s⟩ ⇒ t  ⟹  Γ,γ,p⊢ ⟨process_call Γ rs,s⟩ ⇒ t"
  proof (induction rule: iptables_bigstep_induct)
    case (Nomatch m a)
    thus ?case
      by (cases a) (auto intro: iptables_bigstep.intros simp add: not_matches_add_match_simp skip)
  next
    case Seq
    thus ?case
      by(simp add: process_call_split seq')
  next
    case (Call_return m a chain rs⇩1 m' rs⇩2)
    hence "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided"
      by simp
    hence "Γ,γ,p⊢ ⟨process_ret rs⇩1, Undecided⟩ ⇒ Undecided"
      by (rule iptables_bigstep_process_ret_undecided)
    with Call_return have "Γ,γ,p⊢ ⟨process_ret rs⇩1 @ add_missing_ret_unfoldings rs⇩1 (add_match (MatchNot m') (process_ret rs⇩2)), Undecided⟩ ⇒ Undecided"
      by (metis matches_add_match_MatchNot_simp skip add_match_rot_add_missing_ret_unfoldings seq')
    with Call_return show ?case
      by (simp add: matches_add_match_simp process_ret_split_obvious)
  next
    case Call_result
    thus ?case
      by (simp add: matches_add_match_simp iptables_bigstep_process_ret_undecided)
  qed (auto intro: iptables_bigstep.intros)



lemma process_ret_cases:
  "process_ret rs = rs ∨ (∃rs⇩1 rs⇩2 m. rs = rs⇩1@[Rule m Return]@rs⇩2 ∧ (process_ret rs) = rs⇩1@(process_ret ([Rule m Return]@rs⇩2)))"
  proof (induction rs)
    case (Cons r rs)
    thus ?case
      apply(cases r, rename_tac m' a')
      apply(case_tac a')
              apply(simp_all)
              apply(erule disjE,simp,rule disjI2,elim exE,simp add: process_ret_split_obvious,
                metis append_Cons process_ret_split_obvious process_ret.simps(2))+
         apply(rule disjI2)
         apply(rule_tac x="[]" in exI)
         apply(rule_tac x="rs" in exI)
         apply(rule_tac x="m'" in exI)
         apply(simp)
        apply(erule disjE,simp,rule disjI2,elim exE,simp add: process_ret_split_obvious,
           metis append_Cons process_ret_split_obvious process_ret.simps(2))+
      done
  qed simp

lemma process_ret_splitcases:
  obtains (id) "process_ret rs = rs"
        | (split) rs⇩1 rs⇩2 m where "rs = rs⇩1@[Rule m Return]@rs⇩2" and "process_ret rs = rs⇩1@(process_ret ([Rule m Return]@rs⇩2))"
 by (metis process_ret_cases)


lemma iptables_bigstep_process_ret_cases3:
  assumes "Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided"
  obtains (noreturn) "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
        | (return) rs⇩1 rs⇩2 m where "rs = rs⇩1@[Rule m Return]@rs⇩2" "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided" "matches γ m p"
proof -
  have "Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided ⟹ 
    (Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided) ∨
    (∃rs⇩1 rs⇩2 m. rs = rs⇩1@[Rule m Return]@rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)"
  proof (induction rs)
    case Nil thus ?case by simp
    next
    case (Cons r rs)
    from Cons obtain m a where r: "r = Rule m a" by (cases r) simp
    from r Cons show ?case
      proof(cases "a ≠ Return")
        case True
        with r Cons.prems have prems_r: "Γ,γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided " and prems_rs: "Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided"
         apply(simp_all add: process_ret_split_fst_NeqReturn)
         apply(erule seqE_cons, frule iptables_bigstep_to_undecided, simp)+
         done
        from prems_rs Cons.IH have "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided ∨
                      (∃rs⇩1 rs⇩2 m. rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)" by simp
        thus "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ Undecided ∨ (∃rs⇩1 rs⇩2 m. r # rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)"
          proof(elim disjE)
            assume "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
            hence "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ Undecided" using prems_r by (metis r seq'_cons) 
            thus ?thesis by simp
          next
            assume "(∃rs⇩1 rs⇩2 m. rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)"
            from this obtain rs⇩1 rs⇩2 m' where "rs = rs⇩1 @ [Rule m' Return] @ rs⇩2" and "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided" and "matches γ m' p" by blast
            hence "∃rs⇩1 rs⇩2 m. r # rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p"
              apply(rule_tac x="Rule m a # rs⇩1" in exI)
              apply(rule_tac x=rs⇩2 in exI)
              apply(rule_tac x=m' in exI)
              apply(simp add: r)
              using prems_r seq'_cons by fast
            thus ?thesis by simp
          qed
      next
      case False
        hence "a = Return" by simp
        with Cons.prems r have prems: "Γ,γ,p⊢ ⟨add_match (MatchNot m) (process_ret rs), Undecided⟩ ⇒ Undecided" by simp
        show "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ Undecided ∨ (∃rs⇩1 rs⇩2 m. r # rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)"
          proof(cases "matches γ m p")
          case True
            (*the Cons premises are useless in this case*)
            hence "∃rs⇩1 rs⇩2 m. r # rs = rs⇩1 @ Rule m Return # rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p"
               apply(rule_tac x="[]" in exI)
               apply(rule_tac x="rs" in exI)
               apply(rule_tac x="m" in exI)
               apply(simp add: skip r ‹a = Return›)
               done
            thus ?thesis by simp
          next
          case False
            with nomatch seq_cons False r have r_nomatch: "⋀rs. Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided ⟹ Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ Undecided" by fast
            note r_nomatch'=r_nomatch[simplified r ‹a = Return›] ― ‹r unfolded›
            from False not_matches_add_matchNot_simp prems have "Γ,γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided" by fast
            with Cons.IH have IH: "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided ∨ (∃rs⇩1 rs⇩2 m. rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p)" .
            thus ?thesis
              proof(elim disjE)
                assume "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
                hence "Γ,γ,p⊢ ⟨r # rs, Undecided⟩ ⇒ Undecided" using r_nomatch by simp
                thus ?thesis by simp
              next
                assume "∃rs⇩1 rs⇩2 m. rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p"
                from this obtain rs⇩1 rs⇩2 m' where "rs = rs⇩1 @ [Rule m' Return] @ rs⇩2" and "Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided" and "matches γ m' p" by blast
                hence "∃rs⇩1 rs⇩2 m. r # rs = rs⇩1 @ [Rule m Return] @ rs⇩2 ∧ Γ,γ,p⊢ ⟨rs⇩1, Undecided⟩ ⇒ Undecided ∧ matches γ m p" 
                  apply(rule_tac x="Rule m Return # rs⇩1" in exI)
                  apply(rule_tac x="rs⇩2" in exI)
                  apply(rule_tac x="m'" in exI)
                  by(simp add:  ‹a = Return› False r r_nomatch')
                thus ?thesis by simp
              qed
          qed
       qed
  qed
  with assms noreturn return show ?thesis by auto
qed

lemma iptables_bigstep_process_ret_DecisionD: "Γ,γ,p⊢ ⟨process_ret rs, s⟩ ⇒ Decision X ⟹ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ Decision X"
proof (induction rs arbitrary: s)
  case (Cons r rs)
  thus ?case
    apply(cases r, rename_tac m a)
    apply(clarify)

    apply(case_tac "a ≠ Return")
    apply(simp add: process_ret_split_fst_NeqReturn)
    apply(erule seqE_cons)
    apply(simp add: seq'_cons)

    apply(simp) (*case a = AReturn*)

    apply(case_tac "matches γ m p")
    apply(simp add: matches_add_match_MatchNot_simp skip) (*the prems becomes useless in this case*)
    apply (metis decision skipD)

    (*case ¬ matches*)
    apply(simp add: not_matches_add_matchNot_simp) (*get IH*)
    by (metis decision state.exhaust nomatch seq'_cons)
qed simp

subsection‹@{const process_ret} correctness›
lemma process_ret_add_match_dist1: "Γ,γ,p⊢ ⟨process_ret (add_match m rs), s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨add_match m (process_ret rs), s⟩ ⇒ t"
apply(induction rs arbitrary: s t)
 apply(simp add: add_match_def)
apply(rename_tac r rs s t)
apply(case_tac r)
apply(rename_tac m' a')
apply(simp)
apply(case_tac a')
        apply(simp_all add: add_match_split_fst)
        apply(erule seqE_cons)
        using seq' apply(fastforce)
       apply(erule seqE_cons)
       using seq' apply(fastforce)
      apply(erule seqE_cons)
      using seq' apply(fastforce)
     apply(erule seqE_cons)
     using seq' apply(fastforce)
    apply(erule seqE_cons)
    using seq' apply(fastforce)
   defer
   apply(erule seqE_cons)
   using seq' apply(fastforce)
  apply(erule seqE_cons)
  using seq' apply(fastforce)
 apply(case_tac "matches γ (MatchNot (MatchAnd m m')) p")
  apply(simp)
  apply (meson seq'_cons seqE_cons)
 apply (meson seq'_cons seqE_cons)
by (metis decision decisionD matches.simps(1) matches_add_match_MatchNot_simp matches_add_match_simp
  not_matches_add_matchNot_simp not_matches_add_match_simp state.exhaust)

lemma process_ret_add_match_dist2: "Γ,γ,p⊢ ⟨add_match m (process_ret rs), s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨process_ret (add_match m rs), s⟩ ⇒ t"
apply(induction rs arbitrary: s t)
 apply(simp add: add_match_def)
apply(rename_tac r rs s t)
apply(case_tac r)
apply(rename_tac m' a')
apply(simp)
apply(case_tac a')
        apply(simp_all add: add_match_split_fst)
        apply(erule seqE_cons)
        using seq' apply(fastforce)
       apply(erule seqE_cons)
       using seq' apply(fastforce)
      apply(erule seqE_cons)
      using seq' apply(fastforce)
     apply(erule seqE_cons)
     using seq' apply(fastforce)
    apply(erule seqE_cons)
    using seq' apply(fastforce)
   defer
   apply(erule seqE_cons)
   using seq' apply(fastforce)
  apply(erule seqE_cons)
  using seq' apply(fastforce)
 apply(case_tac "matches γ (MatchNot (MatchAnd m m')) p")
  apply(simp)
  apply (meson seq'_cons seqE_cons)
 apply (meson seq'_cons seqE_cons)
by (metis decision decisionD matches.simps(1) matches_add_match_MatchNot_simp matches_add_match_simp
  not_matches_add_matchNot_simp not_matches_add_match_simp state.exhaust)

(*such fuckup*)
lemma process_ret_add_match_dist: "Γ,γ,p⊢ ⟨process_ret (add_match m rs), s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨add_match m (process_ret rs), s⟩ ⇒ t"
by (metis process_ret_add_match_dist1 process_ret_add_match_dist2)


lemma process_ret_Undecided_sound:
  assumes "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (add_match m rs), Undecided⟩ ⇒ Undecided"
  shows "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
  proof (cases "matches γ m p")
    case False
    thus ?thesis
      by (metis nomatch)
  next
    case True
    note matches = this
    show ?thesis
      using assms proof (induction rs)
        case Nil
        from call_result[OF matches, where Γ="Γ(chain ↦ [])"]
        have "(Γ(chain ↦ [])) chain = Some [] ⟹ Γ(chain ↦ []),γ,p⊢ ⟨[], Undecided⟩ ⇒ Undecided ⟹ Γ(chain ↦ []),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
          by simp
        thus ?case
          by (fastforce intro: skip)
      next
        case (Cons r rs)
        obtain m' a' where r: "r = Rule m' a'" by (cases r) blast

        with Cons.prems have prems: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret (add_match m (Rule m' a' # rs)), Undecided⟩ ⇒ Undecided"
          by fast
        hence prems_simplified: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret (Rule m' a' # rs), Undecided⟩ ⇒ Undecided"
          using matches by (metis matches_add_match_simp process_ret_add_match_dist)

        have "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
          proof (cases "a' = Return")
            case True
            note a' = this
            have "Γ(chain ↦ Rule m' Return # rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
              proof (cases "matches γ m' p")
                case True
                with matches show ?thesis
                  by (fastforce intro: call_return skip)
              next
                case False
                note matches' = this
                hence "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (Rule m' a' # rs), Undecided⟩ ⇒ Undecided"
                  by (metis prems_simplified update_Gamma_nomatch)
                with a' have "Γ(chain ↦ rs),γ,p⊢ ⟨add_match (MatchNot m') (process_ret rs), Undecided⟩ ⇒ Undecided"
                  by simp
                with matches matches' have "Γ(chain ↦ rs),γ,p⊢ ⟨add_match m (process_ret rs), Undecided⟩ ⇒ Undecided" 
                  by (simp add: matches_add_match_simp not_matches_add_matchNot_simp)
                with matches' Cons.IH show ?thesis
                  by (fastforce simp: update_Gamma_nomatch process_ret_add_match_dist)
              qed
            with a' show ?thesis
              by simp
          next
            case False
            note a' = this
            with prems_simplified have "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨Rule m' a' # process_ret rs, Undecided⟩ ⇒ Undecided"
              by (simp add: process_ret_split_fst_NeqReturn)
            hence step: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨[Rule m' a'], Undecided⟩ ⇒ Undecided"
            and   IH_pre: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided"
              by (metis seqE_cons iptables_bigstep_to_undecided)+
            
            from step have "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret rs, Undecided⟩ ⇒ Undecided"
              proof (cases rule: Rule_UndecidedE)
                case log thus ?thesis
                  using IH_pre by (metis empty iptables_bigstep.log update_Gamma_nochange1 update_Gamma_nomatch)
              next
                case call thus ?thesis
                  using IH_pre by (metis update_Gamma_remove_call_undecided)
              next
                case nomatch thus ?thesis
                  using IH_pre by (metis update_Gamma_nomatch)
              qed

            hence "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (add_match m rs), Undecided⟩ ⇒ Undecided"
              by (metis matches matches_add_match_simp process_ret_add_match_dist)
            with Cons.IH have IH: "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
              by fast

            from step show ?thesis
              proof (cases rule: Rule_UndecidedE)
                case log thus ?thesis using IH
                   by (simp add: update_Gamma_log_empty)
              next
                case nomatch
                thus ?thesis
                  using IH by (metis update_Gamma_nomatch)
              next
                case (call c)
                let ?Γ' = "Γ(chain ↦ Rule m' a' # rs)"
                from IH_pre show ?thesis
                  proof (cases rule: iptables_bigstep_process_ret_cases3)
                    case noreturn
                    with call have "?Γ',γ,p⊢ ⟨Rule m' (Call c) # rs, Undecided⟩ ⇒ Undecided"
                      by (metis step seq_cons)
                    from call have "?Γ' chain = Some (Rule m' (Call c) # rs)"
                      by simp
                    from matches show ?thesis
                      by (rule call_result) fact+
                  next
                    case (return rs⇩1 rs⇩2 new_m')
                    with call have "?Γ' chain = Some ((Rule m' (Call c) # rs⇩1) @ [Rule new_m' Return] @ rs⇩2)"
                      by simp
                    from call return step have "?Γ',γ,p⊢ ⟨Rule m' (Call c) # rs⇩1, Undecided⟩ ⇒ Undecided"
                      using IH_pre by (auto intro: seq_cons)
                    from matches show ?thesis
                      by (rule call_return) fact+
                  qed
              qed
          qed
        thus ?case
          by (metis r)
      qed
  qed

lemma process_ret_Decision_sound:
  assumes "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (add_match m rs), Undecided⟩ ⇒ Decision X"
  shows "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Decision X"
  proof (cases "matches γ m p")
    case False
    thus ?thesis by (metis assms state.distinct(1) not_matches_add_match_simp process_ret_add_match_dist1 skipD)
  next
    case True
    note matches = this
    show ?thesis
      using assms proof (induction rs)
        case Nil
        hence False by (metis add_match_split append_self_conv state.distinct(1) process_ret.simps(1) skipD)
        thus ?case by simp
      next
        case (Cons r rs)
        obtain m' a' where r: "r = Rule m' a'" by (cases r) blast

        with Cons.prems have prems: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret (add_match m (Rule m' a' # rs)), Undecided⟩ ⇒ Decision X"
          by fast
        hence prems_simplified: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret (Rule m' a' # rs), Undecided⟩ ⇒ Decision X"
          using matches by (metis matches_add_match_simp process_ret_add_match_dist)

        have "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Decision X"
          proof (cases "a' = Return")
            case True
            note a' = this
            have "Γ(chain ↦ Rule m' Return # rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Decision X"
              proof (cases "matches γ m' p")
                case True
                with matches prems_simplified a' show ?thesis
                  by (auto simp: not_matches_add_match_simp dest: skipD)
              next
                case False
                note matches' = this
                with prems_simplified have "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (Rule m' a' # rs), Undecided⟩ ⇒ Decision X"
                  by (metis update_Gamma_nomatch)
                with a' matches matches' have "Γ(chain ↦ rs),γ,p⊢ ⟨add_match m (process_ret rs), Undecided⟩ ⇒ Decision X" 
                  by (simp add: matches_add_match_simp not_matches_add_matchNot_simp)
                with matches matches' Cons.IH show ?thesis
                  by (fastforce simp: update_Gamma_nomatch process_ret_add_match_dist matches_add_match_simp not_matches_add_matchNot_simp)
              qed
            with a' show ?thesis
              by simp
          next
            case False
            with prems_simplified obtain ti
              where step: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨[Rule m' a'], Undecided⟩ ⇒ ti"
                and IH_pre: "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨process_ret rs, ti⟩ ⇒ Decision X"
              by (auto simp: process_ret_split_fst_NeqReturn elim: seqE_cons)

            hence "Γ(chain ↦ Rule m' a' # rs),γ,p⊢ ⟨rs, ti⟩ ⇒ Decision X"
              by (metis iptables_bigstep_process_ret_DecisionD)

            thus ?thesis
              using matches step by (force intro: call_result seq'_cons)
          qed
        thus ?case
          by (metis r)
      qed
  qed

lemma process_ret_result_empty: "[] = process_ret rs ⟹ ∀r ∈ set rs. get_action r = Return"
  proof (induction rs)
    case (Cons r rs)
    thus ?case
      apply(simp)
      apply(case_tac r)
      apply(rename_tac m a)
      apply(case_tac a)
              apply(simp_all add: add_match_def)
      done
  qed simp


lemma process_ret_sound':
  assumes "Γ(chain ↦ rs),γ,p⊢ ⟨process_ret (add_match m rs), Undecided⟩ ⇒ t"
  shows "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t"
using assms by (metis state.exhaust process_ret_Undecided_sound process_ret_Decision_sound)



lemma wf_chain_process_ret: "wf_chain Γ rs ⟹ wf_chain Γ (process_ret rs)"
  apply(induction rs)
  apply(simp add: wf_chain_def add_match_def)
  apply(case_tac a)
  apply(case_tac "x2 ≠ Return")
   apply(simp add: process_ret_split_fst_NeqReturn)
   using wf_chain_append apply (metis Cons_eq_appendI append_Nil)
  apply(simp add: process_ret_split_fst_Return)
  apply(simp add: wf_chain_def add_match_def get_action_case_simp)
  done
lemma wf_chain_add_match: "wf_chain Γ rs ⟹ wf_chain Γ (add_match m rs)"
  by(induction rs) (simp_all add: wf_chain_def add_match_def get_action_case_simp)

subsection‹Soundness›
theorem unfolding_sound: "wf_chain Γ rs ⟹ Γ,γ,p⊢ ⟨process_call Γ rs, s⟩ ⇒ t ⟹ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof (induction rs arbitrary: s t)
  case (Cons r rs)
  thus ?case
    apply -
    apply(subst(asm) process_call_split_fst)
    apply(erule seqE)

    unfolding wf_chain_def
    apply(case_tac r, rename_tac m a)
    apply(case_tac a)
            apply(simp_all add: seq'_cons)

    apply(case_tac s)
     defer
     apply (metis decision decisionD)
    apply(case_tac "matches γ m p")
     defer
     apply(simp add: not_matches_add_match_simp)
     apply(drule skipD, simp)
     apply (metis nomatch seq_cons)
    apply(clarify)
    apply(simp add: matches_add_match_simp)
    apply(rule_tac t=ti in seq_cons)
     apply(simp_all)

    using process_ret_sound'
    by (metis fun_upd_triv matches_add_match_simp process_ret_add_match_dist)
qed simp

corollary unfolding_sound_complete: "wf_chain Γ rs ⟹ Γ,γ,p⊢ ⟨process_call Γ rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
by (metis unfolding_complete unfolding_sound)

corollary unfolding_n_sound_complete: "∀rsg ∈ ran Γ ∪ {rs}. wf_chain Γ rsg ⟹ Γ,γ,p⊢ ⟨((process_call Γ)^^n) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
  proof(induction n arbitrary: rs)
    case 0 thus ?case by simp
  next
    case (Suc n)
      from Suc have "Γ,γ,p⊢ ⟨(process_call Γ ^^ n) rs, s⟩ ⇒ t = Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" by blast
      from Suc.prems have "∀a∈ran Γ ∪ {process_call Γ rs}. wf_chain Γ a"
        proof(induction rs)
          case Nil thus ?case by simp
        next
          case(Cons r rs)
            from Cons.prems have "∀a∈ran Γ. wf_chain Γ a" by blast
            from Cons.prems have "wf_chain Γ [r]"
              apply(simp)
              apply(clarify)
              apply(simp add: wf_chain_def)
              done
            from Cons.prems have "wf_chain Γ rs"
              apply(simp)
              apply(clarify)
              apply(simp add: wf_chain_def)
              done
            from this Cons.prems Cons.IH have "wf_chain Γ (process_call Γ rs)" by blast
            from this ‹wf_chain Γ [r]›have "wf_chain Γ (r # (process_call Γ rs))" by(simp add: wf_chain_def)
            from this Cons.prems have "wf_chain Γ (process_call Γ (r#rs))"
              apply(cases r)
              apply(rename_tac m a, clarify)
              apply(case_tac a)
                      apply(simp_all)
              apply(simp add: wf_chain_append)
              apply(clarify)
              apply(simp add: ‹wf_chain Γ (process_call Γ rs)›)
              apply(rule wf_chain_add_match)
              apply(rule wf_chain_process_ret)
              apply(simp add: wf_chain_def)
              apply(clarify)
              by (metis ranI option.sel)
          from this ‹∀a∈ran Γ. wf_chain Γ a› show ?case by simp
        qed
      from this Suc.IH[of "((process_call Γ) rs)"] have 
        "Γ,γ,p⊢ ⟨(process_call Γ ^^ n) (process_call Γ rs), s⟩ ⇒ t = Γ,γ,p⊢ ⟨process_call Γ rs, s⟩ ⇒ t"
        by simp
    from this show ?case by (simp add: Suc.prems funpow_swap1 unfolding_sound_complete)
  qed


text_raw‹
\begin{verbatim}
loops in the linux kernel:
http://lxr.linux.no/linux+v3.2/net/ipv4/netfilter/ip_tables.c#L464
/* Figures out from what hook each rule can be called: returns 0 if
   there are loops.  Puts hook bitmask in comefrom. */
   static int mark_source_chains(const struct xt_table_info *newinfo,
                   unsigned int valid_hooks, void *entry0)

discussion: http://marc.info/?l=netfilter-devel&m=105190848425334&w=2
\end{verbatim}
›

text‹Example›
lemma "process_call [''X'' ↦ [Rule (Match b) Return, Rule (Match c) Accept]] [Rule (Match a) (Call ''X'')] =
       [Rule (MatchAnd (Match a) (MatchAnd (MatchNot (Match b)) (Match c))) Accept]" by (simp add: add_match_def)




text‹This is how a firewall processes a ruleset. 
       It starts at a certain chain, usually INPUT, FORWARD, or OUTPUT (called @{term chain_name} in the lemma).
       The firewall has a default action of accept or drop.
      We can check @{const sanity_wf_ruleset} and the other assumptions at runtime.
      Consequently, we can apply @{const repeat_stabilize} as often as we want.
›

theorem repeat_stabilize_process_call:
    assumes "sanity_wf_ruleset Γ" and "chain_name ∈ set (map fst Γ)" and "default_action = Accept ∨ default_action = Drop"
    shows "(map_of Γ),γ,p⊢ ⟨repeat_stabilize n (process_call (map_of Γ)) [Rule MatchAny (Call chain_name), Rule MatchAny default_action], s⟩ ⇒ t ⟷
           (map_of Γ),γ,p⊢ ⟨[Rule MatchAny (Call chain_name), Rule MatchAny default_action], s⟩ ⇒ t"
proof -
  have x: "sanity_wf_ruleset Γ ⟹ rs ∈ ran (map_of Γ) ⟹ wf_chain (map_of Γ) rs" for Γ and rs::"'a rule list"
  apply(simp add: sanity_wf_ruleset_def wf_chain_def)
  by fastforce

  from assms(1) have 1: "∀rsg ∈ ran (map_of Γ). wf_chain (map_of Γ) rsg"
    apply(intro ballI)
    apply(drule x, simp)
    apply(simp)
    done
  let ?rs="[Rule MatchAny (Call chain_name), Rule MatchAny default_action]::'a rule list"
  from assms(2,3) have 2: "wf_chain (map_of Γ) ?rs"
    apply(simp add: wf_chain_def domD dom_map_of_conv_image_fst)
    by blast

  have "∀rsg ∈ ran Γ ∪ {rs}. wf_chain Γ rsg ⟹ 
    Γ,γ,p⊢ ⟨repeat_stabilize n (process_call Γ) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t" for Γ rs
  by(simp add: repeat_stabilize_funpow unfolding_n_sound_complete)
  moreover from 1 2 have "∀rsg ∈ ran (map_of Γ) ∪ {?rs}. wf_chain (map_of Γ) rsg" by simp
  ultimately show ?thesis by simp
qed



definition unfold_optimize_ruleset_CHAIN
  :: "('a match_expr ⇒ 'a match_expr) ⇒ string ⇒ action ⇒ 'a ruleset ⇒ 'a rule list option"
where
"unfold_optimize_ruleset_CHAIN optimize chain_name default_action rs = (let rs =
  (repeat_stabilize 1000 (optimize_matches opt_MatchAny_match_expr)
    (optimize_matches optimize
      (rw_Reject (rm_LogEmpty (repeat_stabilize 10000 (process_call rs)
        [Rule MatchAny (Call chain_name), Rule MatchAny default_action]
  )))))
  in if simple_ruleset rs then Some rs else None)"


lemma unfold_optimize_ruleset_CHAIN:
    assumes "sanity_wf_ruleset Γ" and "chain_name ∈ set (map fst Γ)"
    and "default_action = Accept ∨ default_action = Drop"
    and "⋀m. matches γ (optimize m) p = matches γ m p"
    and "unfold_optimize_ruleset_CHAIN optimize chain_name default_action (map_of Γ) = Some rs"
    shows "(map_of Γ),γ,p⊢ ⟨rs, s⟩ ⇒ t ⟷
           (map_of Γ),γ,p⊢ ⟨[Rule MatchAny (Call chain_name), Rule MatchAny default_action], s⟩ ⇒ t"
proof -
  from assms(5) have rs: "rs = repeat_stabilize 1000 (optimize_matches opt_MatchAny_match_expr)
      (optimize_matches optimize
        (rw_Reject
          (rm_LogEmpty
            (repeat_stabilize 10000 (process_call (map_of Γ)) [Rule MatchAny (Call chain_name), Rule MatchAny default_action]))))"
    by(simp add: unfold_optimize_ruleset_CHAIN_def Let_def split: if_split_asm)

  have optimize_matches_generic_funpow_helper: "(⋀m. matches γ (f m) p = matches γ m p) ⟹
        Γ,γ,p⊢ ⟨(optimize_matches f ^^ n) rs, s⟩ ⇒ t ⟷ Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t"
    for Γ f n rs
    proof(induction n arbitrary:)
      case 0 thus ?case by simp
    next
      case (Suc n) thus ?case
       apply(simp)
       apply(subst optimize_matches_generic[where P="λ_. True"])
       by simp_all
    qed

  have "(map_of Γ),γ,p⊢ ⟨rs, s⟩ ⇒ t ⟷ map_of Γ,γ,p⊢ ⟨repeat_stabilize 10000 (process_call (map_of Γ))
    [Rule MatchAny (Call chain_name), Rule MatchAny default_action], s⟩ ⇒ t"
    apply(simp add: rs repeat_stabilize_funpow)
    apply(subst optimize_matches_generic_funpow_helper)
     apply (simp add: opt_MatchAny_match_expr_correct; fail)
    apply(subst optimize_matches_generic[where P="λ_. True"], simp_all add: assms(4))
    apply(simp add: iptables_bigstep_rw_Reject iptables_bigstep_rm_LogEmpty)
    done
  also have "… ⟷ (map_of Γ),γ,p⊢ ⟨[Rule MatchAny (Call chain_name), Rule MatchAny default_action], s⟩ ⇒ t"
    using assms(1,2,3) by(intro repeat_stabilize_process_call[of Γ chain_name default_action γ p 10000 s t]) simp_all
  finally show ?thesis .
qed

end