Theory Ruleset_Update

theory Ruleset_Update
imports Matching
begin

lemma free_return_not_match: "Γ,γ,p⊢ ⟨[Rule m Return], Undecided⟩ ⇒ t ⟹ ¬ matches γ m p"
  using no_free_return by fast


subsection‹Background Ruleset Updating›
lemma update_Gamma_nomatch: 
  assumes "¬ matches γ m p"
  shows "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨rs', s⟩ ⇒ t ⟷ Γ(chain ↦ rs),γ,p⊢ ⟨rs', s⟩ ⇒ t" (is "?l ⟷ ?r")
  proof
    assume ?l thus ?r
      proof (induction rs' s t rule: iptables_bigstep_induct)
        case (Call_return m a chain' rs⇩1 m' rs⇩2)
        thus ?case
          proof (cases "chain' = chain")
            case True
            with Call_return show ?thesis
              apply simp
              apply(cases "rs⇩1")
              using assms apply fastforce
              apply(rule_tac rs⇩1="list" and m'="m'" and rs⇩2="rs⇩2" in call_return)
                 apply(simp)
                apply(simp)
               apply(simp)
              apply(simp)
              apply(erule seqE_cons[where Γ="(λa. if a = chain then Some rs else Γ a)"])
              apply(frule iptables_bigstep_to_undecided[where Γ="(λa. if a = chain then Some rs else Γ a)"])
              apply(simp)
              done
          qed (auto intro: call_return)
      next
        case (Call_result m' a' chain' rs' t')
        have "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m' (Call chain')], Undecided⟩ ⇒ t'"
          proof (cases "chain' = chain")
            case True
            with Call_result have "Rule m a # rs = rs'" "(Γ(chain ↦ rs)) chain' = Some rs"
              by simp+
            with assms Call_result show ?thesis
              by (metis call_result nomatchD seqE_cons)
          next
            case False
            with Call_result show ?thesis
              by (metis call_result fun_upd_apply)
          qed
        with Call_result show ?case
          by fast
      qed (auto intro: iptables_bigstep.intros)
  next
    assume ?r thus ?l
      proof (induction rs' s t rule: iptables_bigstep_induct)
        case (Call_return m' a' chain' rs⇩1)
        thus ?case
          proof (cases "chain' = chain")
            case True
            with Call_return show ?thesis
              using assms
              by (auto intro: seq_cons nomatch intro!: call_return[where rs⇩1 = "Rule m a # rs⇩1"])
          qed (auto intro: call_return)
      next
        case (Call_result m' a' chain' rs')
        thus ?case
          proof (cases "chain' = chain")
            case True
            with Call_result show ?thesis
              using assms by (auto intro: seq_cons nomatch intro!: call_result)
          qed (auto intro: call_result)
      qed (auto intro: iptables_bigstep.intros)
  qed

lemma update_Gamma_log_empty:
  assumes "a = Log ∨ a = Empty"
  shows "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨rs', s⟩ ⇒ t ⟷
         Γ(chain ↦ rs),γ,p⊢ ⟨rs', s⟩ ⇒ t" (is "?l ⟷ ?r")
  proof
    assume ?l thus ?r
      proof (induction rs' s t rule: iptables_bigstep_induct)
        case (Call_return m' a' chain' rs⇩1 m'' rs⇩2)
        (*it seems that Isabelle has problems to apply @{thm fun_upd_apply} at the semantics if it appears in the goal without @{text λ}*)
        note [simp] = fun_upd_apply[abs_def]

        from Call_return have "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m' (Call chain')], Undecided⟩ ⇒ Undecided" (is ?Call_return_case)
          proof(cases "chain' = chain")
          case True with Call_return show ?Call_return_case
            ― ‹@{term rs⇩1} cannot be empty›
            proof(cases "rs⇩1")
            case Nil with Call_return(3) ‹chain' = chain› assms have "False" by simp
              thus ?Call_return_case by simp
            next
            case (Cons r⇩1 rs⇩1s)
            from Cons Call_return have "Γ(chain ↦ rs),γ,p⊢ ⟨r⇩1 # rs⇩1s, Undecided⟩ ⇒ Undecided" by blast
            with seqE_cons[where Γ="Γ(chain ↦ rs)"] obtain ti where 
              "Γ(chain ↦ rs),γ,p⊢ ⟨[r⇩1], Undecided⟩ ⇒ ti" and "Γ(chain ↦ rs),γ,p⊢ ⟨rs⇩1s, ti⟩ ⇒ Undecided" by metis
            with iptables_bigstep_to_undecided[where Γ="Γ(chain ↦ rs)"] have "Γ(chain ↦ rs),γ,p⊢ ⟨rs⇩1s, Undecided⟩ ⇒ Undecided" by fast
            with Cons Call_return ‹chain' = chain› show ?Call_return_case
               apply(rule_tac rs⇩1="rs⇩1s" and m'="m''" and rs⇩2="rs⇩2" in call_return)
                  apply(simp_all)
               done
             qed
          next
          case False with Call_return show ?Call_return_case
           by (auto intro: call_return)
          qed
        thus ?case using Call_return by blast
      next
        case (Call_result m' a' chain' rs' t')
        thus ?case
          proof (cases "chain' = chain")
            case True
            with Call_result have "rs' = [] @ [Rule m a] @ rs"
              by simp
            with Call_result assms have "Γ(chain ↦ rs),γ,p⊢ ⟨[] @ rs, Undecided⟩ ⇒ t'"
              using log_remove empty_empty by fast
            hence "Γ(chain ↦ rs),γ,p⊢ ⟨rs, Undecided⟩ ⇒ t'"
              by simp
            with Call_result True show ?thesis
              by (metis call_result fun_upd_same)
          qed (fastforce intro: call_result)
      qed (auto intro: iptables_bigstep.intros)
  next
    have cases_a: "⋀P. (a = Log ⟹ P a) ⟹ (a = Empty ⟹ P a) ⟹ P a" using assms by blast
    assume ?r thus ?l
      proof (induction rs' s t rule: iptables_bigstep_induct)
        case (Call_return m' a' chain' rs⇩1 m'' rs⇩2)
        from Call_return have xx: "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨Rule m a # rs⇩1, Undecided⟩ ⇒ Undecided"
          apply -
          apply(rule cases_a)
          apply (auto intro: nomatch seq_cons intro!: log empty simp del: fun_upd_apply)
          done
        with Call_return show ?case
          proof(cases "chain' = chain")
            case False
            with Call_return have x: "(Γ(chain ↦ Rule m a # rs)) chain' = Some (rs⇩1 @ Rule m'' Return # rs⇩2)"
              by(simp)
            with Call_return have "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨[Rule m' (Call chain')], Undecided⟩ ⇒ Undecided"
             apply -
             apply(rule call_return[where rs⇩1="rs⇩1" and m'="m''" and rs⇩2="rs⇩2"])
                apply(simp_all add: x xx del: fun_upd_apply)
             done
             thus "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨[Rule m' a'], Undecided⟩ ⇒ Undecided" using Call_return by simp
            next
            case True
            with Call_return have x: "(Γ(chain ↦ Rule m a # rs)) chain' = Some (Rule m a # rs⇩1 @ Rule m'' Return # rs⇩2)"
              by(simp)
            with Call_return have "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨[Rule m' (Call chain')], Undecided⟩ ⇒ Undecided"
             apply -
             apply(rule call_return[where rs⇩1="Rule m a#rs⇩1" and m'="m''" and rs⇩2="rs⇩2"])
                apply(simp_all add: x xx del: fun_upd_apply)
             done
             thus "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨[Rule m' a'], Undecided⟩ ⇒ Undecided" using Call_return by simp
          qed
      next
        case (Call_result ma a chaina rs t)
        thus ?case
          apply (cases "chaina = chain")
           apply(rule cases_a)
            apply (auto intro: nomatch seq_cons intro!: log empty call_result)[2]
          by (auto intro!: call_result)[1]
      qed (auto intro: iptables_bigstep.intros)
  qed

lemma map_update_chain_if: "(λb. if b = chain then Some rs else Γ b) = Γ(chain ↦ rs)"
  by auto

lemma no_recursive_calls_helper:
  assumes "Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t"
  and     "matches γ m p"
  and     "Γ chain = Some [Rule m (Call chain)]"
  shows   False
  using assms
  proof (induction "[Rule m (Call chain)]" Undecided t rule: iptables_bigstep_induct)
    case Seq
    thus ?case
      by (metis Cons_eq_append_conv append_is_Nil_conv skipD)
  next
    case (Call_return chain' rs⇩1 m' rs⇩2)
    hence "rs⇩1 @ Rule m' Return # rs⇩2 = [Rule m (Call chain')]"
      by simp
    thus ?case
      by (cases "rs⇩1") auto
  next
    case Call_result
    thus ?case
      by simp
  qed (auto intro: iptables_bigstep.intros)

lemma no_recursive_calls:
  "Γ(chain ↦ [Rule m (Call chain)]),γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ t ⟹ matches γ m p ⟹ False"
  by (fastforce intro: no_recursive_calls_helper)

lemma no_recursive_calls2:
  assumes "Γ(chain ↦ (Rule m (Call chain)) # rs''),γ,p⊢ ⟨(Rule m (Call chain)) # rs', Undecided⟩ ⇒ Undecided"
  and     "matches γ m p"
  shows   False
  using assms
  proof (induction "(Rule m (Call chain)) # rs'" Undecided Undecided arbitrary: rs' rule: iptables_bigstep_induct)
    case (Seq rs⇩1 rs⇩2 t)
    thus ?case
      by (cases rs⇩1) (auto elim: seqE_cons simp add: iptables_bigstep_to_undecided)
  qed (auto intro: iptables_bigstep.intros simp: Cons_eq_append_conv)


lemma update_Gamma_nochange1: 
  assumes "Γ(chain ↦ rs),γ,p⊢ ⟨[Rule m a], Undecided⟩ ⇒ Undecided"
  and     "Γ(chain ↦ Rule m a # rs),γ,p⊢ ⟨rs', s⟩ ⇒ t"
  shows   "Γ(chain ↦ rs),γ,p⊢ ⟨rs', s⟩ ⇒ t"
  using assms(2) proof (induction rs' s t rule: iptables_bigstep_induct)
    case (Call_return m a chaina rs⇩1 m' rs⇩2)
    thus ?case
      proof (cases "chaina = chain")
        case True
        with Call_return show ?thesis
          apply simp
          apply(cases "rs⇩1")
          apply(simp)
          using assms apply (metis no_free_return) (*gives False*)
          apply(rule_tac rs⇩1="list" and m'="m'" and rs⇩2="rs⇩2" in call_return)
          apply(simp)
          apply(simp)
          apply(simp)
          apply(simp)
          apply(erule seqE_cons[where Γ="(λa. if a = chain then Some rs else Γ a)"])
          apply(frule iptables_bigstep_to_undecided[where Γ="(λa. if a = chain then Some rs else Γ a)"])
          apply(simp)
          done
      qed (auto intro: call_return)
  next
    case (Call_result m a chaina rsa t)
    thus ?case
      proof (cases "chaina = chain")
        case True
        with Call_result show ?thesis
          apply(simp)
          apply(cases "rsa")
           apply(simp)
           apply(rule_tac rs=rs in call_result)
            apply(simp_all)
          apply(erule_tac seqE_cons[where Γ="(λb. if b = chain then Some rs else Γ b)"])
          apply(case_tac t)
           apply(simp)
           apply(frule iptables_bigstep_to_undecided[where Γ="(λb. if b = chain then Some rs else Γ b)"])
           apply(simp)
          apply(simp)
          apply(subgoal_tac "ti = Undecided")
           apply(simp)
          using assms(1)[simplified map_update_chain_if[symmetric]] iptables_bigstep_deterministic apply fast
          done
      qed (fastforce intro: call_result)
  qed (auto intro: iptables_bigstep.intros)

lemma update_gamme_remove_Undecidedpart:
  assumes "Γ(chain ↦ rs'),γ,p⊢ ⟨rs', Undecided⟩ ⇒ Undecided"
  and     "Γ(chain ↦ rs1@rs'),γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
  shows   "Γ(chain ↦rs'),γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
  using assms(2) proof (induction rs Undecided Undecided rule: iptables_bigstep_induct)
    case Seq
    thus ?case
      by (auto simp: iptables_bigstep_to_undecided intro: seq)
  next
    case (Call_return m a chaina rs⇩1 m' rs⇩2)
    thus ?case
      apply(cases "chaina = chain")
       apply(simp)
       apply(cases "length rs1 ≤ length rs⇩1")
        apply(simp add: List.append_eq_append_conv_if)
        apply(rule_tac rs⇩1="drop (length rs1) rs⇩1" and m'=m' and rs⇩2=rs⇩2 in call_return)
          apply(simp_all)[3]
        apply(subgoal_tac "rs⇩1 = (take (length rs1) rs⇩1) @ drop (length rs1) rs⇩1")
         prefer 2 apply (metis append_take_drop_id)
        apply(clarify)
        apply(subgoal_tac "Γ(chain ↦ drop (length rs1) rs⇩1 @ Rule m' Return # rs⇩2),γ,p⊢ 
            ⟨(take (length rs1) rs⇩1) @ drop (length rs1) rs⇩1, Undecided⟩ ⇒ Undecided")
         prefer 2 apply(auto)[1]
        apply(erule_tac rs⇩1="take (length rs1) rs⇩1" and rs⇩2="drop (length rs1) rs⇩1" in seqE)
        apply(simp)
        apply(frule_tac rs="drop (length rs1) rs⇩1" in iptables_bigstep_to_undecided)
        apply(simp; fail) (*oh wow*)
       using assms apply (auto intro: call_result call_return)
      done
  next
    case (Call_result _ _ chain' rsa)
    thus ?case
      apply(cases "chain' = chain")
       apply(simp)
       apply(rule call_result)
         apply(simp_all)[2]
       apply (metis iptables_bigstep_to_undecided seqE)
      apply (auto intro: call_result)
      done
  qed (auto intro: iptables_bigstep.intros)

lemma update_Gamma_nocall:
  assumes "¬ (∃chain. a = Call chain)"
  shows "Γ,γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t ⟷ Γ',γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t"
  proof -
    {
      fix Γ Γ'
      have "Γ,γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t ⟹ Γ',γ,p⊢ ⟨[Rule m a], s⟩ ⇒ t"
        proof (induction "[Rule m a]" s t rule: iptables_bigstep_induct)
          case Seq
          thus ?case by (metis (lifting, no_types) list_app_singletonE[where x = "Rule m a"] skipD)
        next
          case Call_return thus ?case using assms by metis
        next
          case Call_result thus ?case using assms by metis
        qed (auto intro: iptables_bigstep.intros)
    }
    thus ?thesis
      by blast
  qed

lemma update_Gamma_call:
  assumes "Γ chain = Some rs" and "Γ' chain = Some rs'"
  assumes "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided" and "Γ',γ,p⊢ ⟨rs', Undecided⟩ ⇒ Undecided"
  shows "Γ,γ,p⊢ ⟨[Rule m (Call chain)], s⟩ ⇒ t ⟷ Γ',γ,p⊢ ⟨[Rule m (Call chain)], s⟩ ⇒ t"
  proof -
    {
      fix Γ Γ' rs rs'
      assume assms:
        "Γ chain = Some rs" "Γ' chain = Some rs'"
        "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided" "Γ',γ,p⊢ ⟨rs', Undecided⟩ ⇒ Undecided"
      have "Γ,γ,p⊢ ⟨[Rule m (Call chain)], s⟩ ⇒ t ⟹ Γ',γ,p⊢ ⟨[Rule m (Call chain)], s⟩ ⇒ t"
        proof (induction "[Rule m (Call chain)]" s t rule: iptables_bigstep_induct)
          case Seq
          thus ?case by (metis (lifting, no_types) list_app_singletonE[where x = "Rule m (Call chain)"] skipD)
        next
          case Call_result
          thus ?case
            using assms by (metis call_result iptables_bigstep_deterministic)
        qed (auto intro: iptables_bigstep.intros assms)
    }
    note * = this
    show ?thesis
      using *[OF assms(1-4)] *[OF assms(2,1,4,3)] by blast
  qed

lemma update_Gamma_remove_call_undecided:
  assumes "Γ(chain ↦ Rule m (Call foo) # rs'),γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
  and     "matches γ m p"
  shows "Γ(chain ↦ rs'),γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
  using assms
  proof (induction rs Undecided Undecided arbitrary: rule: iptables_bigstep_induct)
    case Seq
    thus ?case
      by (force simp: iptables_bigstep_to_undecided intro: seq')
  next
    case (Call_return m a chaina rs⇩1 m' rs⇩2)
    thus ?case
      apply(cases "chaina = chain")
      apply(cases "rs⇩1")
      apply(force intro: call_return)
      apply(simp)
      apply(erule_tac Γ="Γ(chain ↦ list @ Rule m' Return # rs⇩2)" in seqE_cons)
      apply(frule_tac Γ="Γ(chain ↦ list @ Rule m' Return # rs⇩2)" in iptables_bigstep_to_undecided)
      apply(auto intro: call_return)
      done
  next
    case (Call_result m a chaina rsa)
    thus ?case
      apply(cases "chaina = chain")
      apply(simp)
      apply (metis call_result fun_upd_same iptables_bigstep_to_undecided seqE_cons)
      apply (auto intro: call_result)
      done
  qed (auto intro: iptables_bigstep.intros)

lemma all_return_subchain:
  assumes a1: "Γ chain = Some rs"
  and     a2: "matches γ m p"
  and     a3: "∀r∈set rs. get_action r = Return"
  shows "Γ,γ,p⊢ ⟨[Rule m (Call chain)], Undecided⟩ ⇒ Undecided"
  proof (cases "∃r ∈ set rs. matches γ (get_match r) p")
    case True
    hence "(∃rs1 r rs2. rs = rs1 @ r # rs2 ∧ matches γ (get_match r) p ∧ (∀r'∈set rs1. ¬ matches γ (get_match r') p))"
      by (subst split_list_first_prop_iff[symmetric])
    then obtain rs1 r rs2
      where *: "rs = rs1 @ r # rs2" "matches γ (get_match r) p" "∀r'∈set rs1. ¬ matches γ (get_match r') p"
      by auto

    with a3 obtain m' where "r = Rule m' Return"
      by (cases r) simp
    with * assms show ?thesis
      by (fastforce intro: call_return nomatch')
  next
    case False
    hence "Γ,γ,p⊢ ⟨rs, Undecided⟩ ⇒ Undecided"
      by (blast intro: nomatch')
    with a1 a2 show ?thesis
      by (metis call_result)
qed


lemma get_action_case_simp: "get_action (case r of Rule m' x ⇒ Rule (MatchAnd m m') x) = get_action r"
by (metis rule.case_eq_if rule.sel(2))


lemma updategamma_insert_new: "Γ,γ,p⊢ ⟨rs, s⟩ ⇒ t ⟹ chain ∉ dom Γ ⟹ Γ(chain ↦ rs'),γ,p⊢ ⟨rs, s⟩ ⇒ t"
proof(induction rule: iptables_bigstep_induct)
case (Call_result m a chain' rs t)
  thus ?case by (metis call_result domI fun_upd_def)
next
case Call_return
  thus ?case by (metis call_return domI fun_upd_def)
qed(auto intro: iptables_bigstep.intros)




end