[STATEMENT]
lemma approximating_bigstep_undecided_to_undecided_in_doubt_deny_approx: "matcher_agree_on_exact_matches \<gamma> \<beta> \<Longrightarrow>
       good_ruleset rs \<Longrightarrow>
       (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided \<or>  \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(rotate_tac 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(induction rs Undecided Undecided rule: approximating_bigstep_induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset []\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p; a = Log \<or> a = Empty; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>m a. \<lbrakk>\<not> Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 4. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset []\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p; a = Log \<or> a = Empty; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>m a. \<lbrakk>\<not> Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 4. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply (metis iptables_bigstep.skip)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p; a = Log \<or> a = Empty; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a. \<lbrakk>\<not> Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply (metis iptables_bigstep.empty iptables_bigstep.log iptables_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>\<not> Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp split: ternaryvalue.split_asm add: matches_case_ternaryvalue_tuple)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryFalse\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply (metis in_doubt_allow_allows_Accept iptables_bigstep.nomatch matches_casesE ternaryvalue.distinct(1) ternaryvalue.distinct(5))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(case_tac a)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p; a = action.Accept\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p; a = action.Drop\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p; a = Log\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 4. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p; a = Reject\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 5. \<And>m a x5. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p; a = Call x5\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 6. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 7. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 8. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 9. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> in_doubt_deny a p; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 10. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m action.Accept]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; a = action.Accept\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m action.Accept], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m action.Accept], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Log]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Log\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Log], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Log], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>m a x5. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call x5)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Call x5\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 4. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Return]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 5. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 6. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 7. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 8. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply (metis iptables_bigstep.accept iptables_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Log]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Log\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Log], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Log], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a x5. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call x5)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Call x5\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Return]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 4. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 5. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 6. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 7. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply (metis iptables_bigstep.log iptables_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>m a x5. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Call x5)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Call x5\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Call x5)], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Return]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 4. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 5. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 6. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp add: good_ruleset_alt)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Return]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Return\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Return], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 4. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 5. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp add: good_ruleset_alt)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>m a x7. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m (Goto x7)]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Goto x7\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m (Goto x7)], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 4. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp add: good_ruleset_alt)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Empty]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Empty], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply (metis iptables_bigstep.empty iptables_bigstep.nomatch)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m Unknown]; ternary_ternary_eval (map_match_tac \<beta> p m) = TernaryUnknown; \<not> undefined; a = Unknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m Unknown], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp add: good_ruleset_alt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp add: good_ruleset_append,clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; \<not> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Undecided
[PROOF STEP]
by (metis approximating_bigstep_to_undecided iptables_bigstep.decision iptables_bigstep.seq)


[STATEMENT]
lemma FinalAllow_approximating_in_doubt_deny: "matcher_agree_on_exact_matches \<gamma> \<beta> \<Longrightarrow>
   good_ruleset rs \<Longrightarrow>
   (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(rotate_tac 2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(induction rs Undecided "Decision FinalAllow" rule: approximating_bigstep_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, in_doubt_deny) m a p; a = action.Accept; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m a]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<lbrakk>t = Undecided; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, in_doubt_deny) m action.Accept p; a = action.Accept; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset [Rule m action.Accept]\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m action.Accept], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Decision FinalAllow; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply (metis action.distinct(1) action.distinct(5) iptables_bigstep.accept not_exact_match_in_doubt_deny_approx_match)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>t = Decision FinalAllow; good_ruleset rs\<^sub>1\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<lbrakk>t = Undecided; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset (rs\<^sub>1 @ rs\<^sub>2)\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp add: good_ruleset_append, clarify)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalAllow \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(case_tac t)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalAllow \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalAllow \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalAllow \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(drule(2) approximating_bigstep_undecided_to_undecided_in_doubt_deny_approx[where \<Gamma>=\<Gamma>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided \<or> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalAllow \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply(erule disjE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalAllow \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply (metis iptables_bigstep.seq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>rs\<^sub>1 rs\<^sub>2 t. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Undecided; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 2. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalAllow \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
apply (metis iptables_bigstep.decision iptables_bigstep.seq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rs rs\<^sub>1 rs\<^sub>2 t x2. \<lbrakk>(\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; t = Decision FinalAllow \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow; t = Undecided \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow; matcher_agree_on_exact_matches \<gamma> \<beta>; good_ruleset rs\<^sub>1; good_ruleset rs\<^sub>2; t = Decision x2\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1 @ rs\<^sub>2, Undecided\<rangle> \<Rightarrow> Decision FinalAllow
[PROOF STEP]
by (metis Decision_approximating_bigstep_fun approximating_semantics_imp_fun iptables_bigstep.decision iptables_bigstep.seq)


[STATEMENT]
theorem FinalAllowClosure:
  assumes "matcher_agree_on_exact_matches \<gamma> \<beta>" and "good_ruleset rs"
  shows "{p. (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow} \<subseteq> {p. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow}"
  and   "{p. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow} \<subseteq> {p. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. _Collect p ((\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow) \<subseteq> _Collect p (\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow) &&& _Collect p (\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow) \<subseteq> _Collect p ((\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow)
[PROOF STEP]
apply (metis FinalAllows_subseteq_in_doubt_deny assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. _Collect p (\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalAllow) \<subseteq> _Collect p ((\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow)
[PROOF STEP]
by (metis FinalAllows_subseteq_in_doubt_allow assms)


[STATEMENT]
theorem FinalDenyClosure:
  assumes "matcher_agree_on_exact_matches \<gamma> \<beta>" and "good_ruleset rs"
  shows "{p. (\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny} \<subseteq> {p. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny}"
  and   "{p. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny} \<subseteq> {p. (\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. _Collect p ((\<beta>, in_doubt_allow),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny) \<subseteq> _Collect p (\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny) &&& _Collect p (\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny) \<subseteq> _Collect p ((\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny)
[PROOF STEP]
apply (metis FinalDenys_subseteq_in_doubt_allow assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. _Collect p (\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> Decision FinalDeny) \<subseteq> _Collect p ((\<beta>, in_doubt_deny),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny)
[PROOF STEP]
by (metis FinalDeny_approximating_in_doubt_deny assms mem_Collect_eq subsetI)


[STATEMENT]
lemma LukassLemma: assumes agree: "matcher_agree_on_exact_matches \<gamma> \<beta>"
        and noUnknown: "(\<forall> r \<in> set rs. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown)"
        and good: "good_ruleset rs"
      shows "(\<beta>,\<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t \<longleftrightarrow>  \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
fix t \<comment> \<open>if we show it for arbitrary @{term t}, we can reuse this fact for the other direction.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
assume a: "(\<beta>,\<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t"
[PROOF STATE]
proof (state)
this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
from a good agree noUnknown
[PROOF STATE]
proof (chain)
picking this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t
good_ruleset rs
matcher_agree_on_exact_matches \<gamma> \<beta>
\<forall>r\<in>set rs. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown
[PROOF STEP]
have "\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
using this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t
good_ruleset rs
matcher_agree_on_exact_matches \<gamma> \<beta>
\<forall>r\<in>set rs. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown

goal (1 subgoal):
 1. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
proof(induction rs s t rule: approximating_bigstep_induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>t. \<lbrakk>good_ruleset []; matcher_agree_on_exact_matches \<gamma> \<beta>; \<forall>r\<in>set []. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[], t\<rangle> \<Rightarrow> t
 2. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, \<alpha>) m a p; a = action.Accept; good_ruleset [Rule m a]; matcher_agree_on_exact_matches \<gamma> \<beta>; \<forall>r\<in>set [Rule m a]. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, \<alpha>) m a p; a = action.Drop \<or> a = Reject; good_ruleset [Rule m a]; matcher_agree_on_exact_matches \<gamma> \<beta>; \<forall>r\<in>set [Rule m a]. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>, \<alpha>) m a p; a = Log \<or> a = Empty; good_ruleset [Rule m a]; matcher_agree_on_exact_matches \<gamma> \<beta>; \<forall>r\<in>set [Rule m a]. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided
 5. \<And>m a. \<lbrakk>\<not> Matching_Ternary.matches (\<beta>, \<alpha>) m a p; good_ruleset [Rule m a]; matcher_agree_on_exact_matches \<gamma> \<beta>; \<forall>r\<in>set [Rule m a]. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided
 6. \<And>rs X. \<lbrakk>good_ruleset rs; matcher_agree_on_exact_matches \<gamma> \<beta>; \<forall>r\<in>set rs. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Decision X\<rangle> \<Rightarrow> Decision X
 7. \<And>rs rs\<^sub>1 rs\<^sub>2 t t'. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>, \<alpha>),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<lbrakk>good_ruleset rs\<^sub>1; matcher_agree_on_exact_matches \<gamma> \<beta>; \<forall>r\<in>set rs\<^sub>1. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; (\<beta>, \<alpha>),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> t'; \<lbrakk>good_ruleset rs\<^sub>2; matcher_agree_on_exact_matches \<gamma> \<beta>; \<forall>r\<in>set rs\<^sub>2. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> t'; good_ruleset rs; matcher_agree_on_exact_matches \<gamma> \<beta>; \<forall>r\<in>set rs. ternary_ternary_eval (map_match_tac \<beta> p (get_match r)) \<noteq> TernaryUnknown\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> t'
[PROOF STEP]
qed(auto intro: approximating_bigstep.intros iptables_bigstep.intros dest: iptables_bigstepD dest: matches_comply_exact simp: good_ruleset_append)
[PROOF STATE]
proof (state)
this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?ta2 \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> ?ta2

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
note 1=this
[PROOF STATE]
proof (state)
this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?ta2 \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> ?ta2

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?ta2 \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> ?ta2

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
assume a: "\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (state)
this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
obtain x where "approximating_bigstep_fun (\<beta>,\<alpha>) p rs s = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. approximating_bigstep_fun (\<beta>, \<alpha>) p rs s = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
approximating_bigstep_fun (\<beta>, \<alpha>) p rs s = x

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
with approximating_fun_imp_semantics[OF good_imp_wf_ruleset[OF good]]
[PROOF STATE]
proof (chain)
picking this:
approximating_bigstep_fun ?\<gamma> ?p rs ?s = ?t \<Longrightarrow> ?\<gamma>,?p\<turnstile> \<langle>rs, ?s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?t
approximating_bigstep_fun (\<beta>, \<alpha>) p rs s = x
[PROOF STEP]
have x: "(\<beta>,\<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> x"
[PROOF STATE]
proof (prove)
using this:
approximating_bigstep_fun ?\<gamma> ?p rs ?s = ?t \<Longrightarrow> ?\<gamma>,?p\<turnstile> \<langle>rs, ?s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?t
approximating_bigstep_fun (\<beta>, \<alpha>) p rs s = x

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> x
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> x

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?ta2 \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> ?ta2
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> x
[PROOF STEP]
have "\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> x"
[PROOF STATE]
proof (prove)
using this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?ta2 \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> ?ta2
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> x

goal (1 subgoal):
 1. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> x

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
with a iptables_bigstep_deterministic
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
\<lbrakk>?\<Gamma>,?\<gamma>,?p\<turnstile> \<langle>?rs, ?s\<rangle> \<Rightarrow> ?t; ?\<Gamma>,?\<gamma>,?p\<turnstile> \<langle>?rs, ?s\<rangle> \<Rightarrow> ?t'\<rbrakk> \<Longrightarrow> ?t = ?t'
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> x
[PROOF STEP]
have "x = t"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
\<lbrakk>?\<Gamma>,?\<gamma>,?p\<turnstile> \<langle>?rs, ?s\<rangle> \<Rightarrow> ?t; ?\<Gamma>,?\<gamma>,?p\<turnstile> \<langle>?rs, ?s\<rangle> \<Rightarrow> ?t'\<rbrakk> \<Longrightarrow> ?t = ?t'
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> x

goal (1 subgoal):
 1. x = t
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
x = t

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
hence "(\<beta>,\<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t"
[PROOF STATE]
proof (prove)
using this:
x = t

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
x = t
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> x

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t \<Longrightarrow> (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
note 2=this
[PROOF STATE]
proof (state)
this:
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t \<Longrightarrow> (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?ta2 \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> ?ta2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t \<Longrightarrow> (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> ?ta2 \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> ?ta2
\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t \<Longrightarrow> (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t

goal (1 subgoal):
 1. (\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<beta>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem \<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c_approximating_bigstep_iff_iptables_bigstep:
  assumes "\<forall>r \<in> set rs. \<forall>c. get_action r \<noteq> Call c"
  shows "((\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>),\<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t \<longleftrightarrow>  \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t = \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
[PROOF STEP]
apply(rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t
 2. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t
[PROOF STEP]
apply(induction rs s t rule: approximating_bigstep_induct)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>t. \<Gamma>,\<gamma>,p\<turnstile> \<langle>[], t\<rangle> \<Rightarrow> t
 2. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>) m a p; a = action.Accept\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalAllow
 3. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>) m a p; a = action.Drop \<or> a = Reject\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Decision FinalDeny
 4. \<And>m a. \<lbrakk>Matching_Ternary.matches (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>) m a p; a = Log \<or> a = Empty\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided
 5. \<And>m a. \<not> Matching_Ternary.matches (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>) m a p \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow> Undecided
 6. \<And>rs X. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Decision X\<rangle> \<Rightarrow> Decision X
 7. \<And>rs rs\<^sub>1 rs\<^sub>2 t t'. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> t'; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> t'
 8. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t
[PROOF STEP]
apply(auto intro: iptables_bigstep.intros simp: \<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c_matching)[7]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t
[PROOF STEP]
apply(insert assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow> t; \<forall>r\<in>set rs. \<forall>c. get_action r \<noteq> Call c\<rbrakk> \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs, s\<rangle> \<Rightarrow>\<^sub>\<alpha> t
[PROOF STEP]
apply(induction rs s t rule: iptables_bigstep_induct)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>t. \<forall>r\<in>set []. \<forall>c. get_action r \<noteq> Call c \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>[], t\<rangle> \<Rightarrow>\<^sub>\<alpha> t
 2. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = action.Accept; \<forall>r\<in>set [Rule m a]. \<forall>c. get_action r \<noteq> Call c\<rbrakk> \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalAllow
 3. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = action.Drop \<or> a = Reject; \<forall>r\<in>set [Rule m a]. \<forall>c. get_action r \<noteq> Call c\<rbrakk> \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision FinalDeny
 4. \<And>m a. \<lbrakk>Semantics.matches \<gamma> m p; a = Log \<or> a = Empty; \<forall>r\<in>set [Rule m a]. \<forall>c. get_action r \<noteq> Call c\<rbrakk> \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided
 5. \<And>m a. \<lbrakk>\<not> Semantics.matches \<gamma> m p; \<forall>r\<in>set [Rule m a]. \<forall>c. get_action r \<noteq> Call c\<rbrakk> \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided
 6. \<And>rs X. \<forall>r\<in>set rs. \<forall>c. get_action r \<noteq> Call c \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs, Decision X\<rangle> \<Rightarrow>\<^sub>\<alpha> Decision X
 7. \<And>rs rs\<^sub>1 rs\<^sub>2 t t'. \<lbrakk>rs = rs\<^sub>1 @ rs\<^sub>2; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> t; \<forall>r\<in>set rs\<^sub>1. \<forall>c. get_action r \<noteq> Call c \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow> t'; \<forall>r\<in>set rs\<^sub>2. \<forall>c. get_action r \<noteq> Call c \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs\<^sub>2, t\<rangle> \<Rightarrow>\<^sub>\<alpha> t'; \<forall>r\<in>set rs. \<forall>c. get_action r \<noteq> Call c\<rbrakk> \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t'
 8. \<And>m a chain rs\<^sub>1 m' rs\<^sub>2. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some (rs\<^sub>1 @ [Rule m' Return] @ rs\<^sub>2); Semantics.matches \<gamma> m' p; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow> Undecided; \<forall>r\<in>set rs\<^sub>1. \<forall>c. get_action r \<noteq> Call c \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs\<^sub>1, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided; \<forall>r\<in>set [Rule m a]. \<forall>c. get_action r \<noteq> Call c\<rbrakk> \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> Undecided
 9. \<And>m a chain rs t. \<lbrakk>Semantics.matches \<gamma> m p; a = Call chain; \<Gamma> chain = Some rs; \<Gamma>,\<gamma>,p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow> t; \<forall>r\<in>set rs. \<forall>c. get_action r \<noteq> Call c \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>rs, Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t; \<forall>r\<in>set [Rule m a]. \<forall>c. get_action r \<noteq> Call c\<rbrakk> \<Longrightarrow> (\<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c \<gamma>, \<alpha>),p\<turnstile> \<langle>[Rule m a], Undecided\<rangle> \<Rightarrow>\<^sub>\<alpha> t
[PROOF STEP]
apply(auto intro: approximating_bigstep.intros simp: \<beta>\<^sub>m\<^sub>a\<^sub>g\<^sub>i\<^sub>c_matching)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Semantics_optimize_primitive_univ_common_matcher:
  assumes "matcher_agree_on_exact_matches \<gamma> common_matcher"
    shows "Semantics.matches \<gamma> (optimize_primitive_univ m) p = Semantics.matches \<gamma> m p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Semantics.matches \<gamma> (optimize_primitive_univ m) p = Semantics.matches \<gamma> m p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Semantics.matches \<gamma> (optimize_primitive_univ m) p = Semantics.matches \<gamma> m p
[PROOF STEP]
have "65535 = (- 1::16 word)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 65535 = - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
65535 = - 1

goal (1 subgoal):
 1. Semantics.matches \<gamma> (optimize_primitive_univ m) p = Semantics.matches \<gamma> m p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
65535 = - 1
[PROOF STEP]
have port_range: "\<And>s e port. s = 0 \<and> e = 0xFFFF \<longrightarrow> (port::16 word) \<le> 0xFFFF"
[PROOF STATE]
proof (prove)
using this:
65535 = - 1

goal (1 subgoal):
 1. \<And>s e port. s = (0::'c) \<and> e = (65535::'d) \<longrightarrow> port \<le> 65535
[PROOF STEP]
by (simp only:) simp
[PROOF STATE]
proof (state)
this:
?s = (0::?'c1) \<and> ?e = (65535::?'d1) \<longrightarrow> ?port \<le> 65535

goal (1 subgoal):
 1. Semantics.matches \<gamma> (optimize_primitive_univ m) p = Semantics.matches \<gamma> m p
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
matcher_agree_on_exact_matches \<gamma> common_matcher
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
matcher_agree_on_exact_matches \<gamma> common_matcher

goal (1 subgoal):
 1. Semantics.matches \<gamma> (optimize_primitive_univ m) p = Semantics.matches \<gamma> m p
[PROOF STEP]
apply(induction m rule: optimize_primitive_univ.induct)
[PROOF STATE]
proof (prove)
goal (21 subgoals):
 1. \<And>uu_. matcher_agree_on_exact_matches \<gamma> common_matcher \<Longrightarrow> Semantics.matches \<gamma> (optimize_primitive_univ (Match (Src (IpAddrNetmask uu_ 0)))) p = Semantics.matches \<gamma> (Match (Src (IpAddrNetmask uu_ 0))) p
 2. \<And>uv_. matcher_agree_on_exact_matches \<gamma> common_matcher \<Longrightarrow> Semantics.matches \<gamma> (optimize_primitive_univ (Match (Dst (IpAddrNetmask uv_ 0)))) p = Semantics.matches \<gamma> (Match (Dst (IpAddrNetmask uv_ 0))) p
 3. \<And>iface. matcher_agree_on_exact_matches \<gamma> common_matcher \<Longrightarrow> Semantics.matches \<gamma> (optimize_primitive_univ (Match (IIface iface))) p = Semantics.matches \<gamma> (Match (IIface iface)) p
 4. \<And>iface. matcher_agree_on_exact_matches \<gamma> common_matcher \<Longrightarrow> Semantics.matches \<gamma> (optimize_primitive_univ (Match (OIface iface))) p = Semantics.matches \<gamma> (Match (OIface iface)) p
 5. matcher_agree_on_exact_matches \<gamma> common_matcher \<Longrightarrow> Semantics.matches \<gamma> (optimize_primitive_univ (Match (Prot ProtoAny))) p = Semantics.matches \<gamma> (Match (Prot ProtoAny)) p
 6. \<And>m c. matcher_agree_on_exact_matches \<gamma> common_matcher \<Longrightarrow> Semantics.matches \<gamma> (optimize_primitive_univ (Match (L4_Flags (TCP_Flags m c)))) p = Semantics.matches \<gamma> (Match (L4_Flags (TCP_Flags m c))) p
 7. \<And>ctstate. matcher_agree_on_exact_matches \<gamma> common_matcher \<Longrightarrow> Semantics.matches \<gamma> (optimize_primitive_univ (Match (CT_State ctstate))) p = Semantics.matches \<gamma> (Match (CT_State ctstate)) p
 8. \<And>va. matcher_agree_on_exact_matches \<gamma> common_matcher \<Longrightarrow> Semantics.matches \<gamma> (optimize_primitive_univ (Match (Src (IpAddr va)))) p = Semantics.matches \<gamma> (Match (Src (IpAddr va))) p
 9. \<And>va vc. matcher_agree_on_exact_matches \<gamma> common_matcher \<Longrightarrow> Semantics.matches \<gamma> (optimize_primitive_univ (Match (Src (IpAddrNetmask va (Suc vc))))) p = Semantics.matches \<gamma> (Match (Src (IpAddrNetmask va (Suc vc)))) p
 10. \<And>va vb. matcher_agree_on_exact_matches \<gamma> common_matcher \<Longrightarrow> Semantics.matches \<gamma> (optimize_primitive_univ (Match (Src (IpAddrRange va vb)))) p = Semantics.matches \<gamma> (Match (Src (IpAddrRange va vb))) p
A total of 21 subgoals...
[PROOF STEP]
apply(auto elim!: matcher_agree_on_exact_matches_gammaE
             simp add: port_range match_ifaceAny ipset_from_cidr_0 ctstate_is_UNIV)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Semantics.matches \<gamma> (optimize_primitive_univ m) p = Semantics.matches \<gamma> m p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inc_above_dec_above: "x < b \<or> b + i \<le> x \<Longrightarrow> inc_above b i (dec_above b i x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < b \<or> b + i \<le> x \<Longrightarrow> inc_above b i (dec_above b i x) = x
[PROOF STEP]
by (auto simp: inc_above_def dec_above_def)


[STATEMENT]
lemma dec_above_inc_above: "dec_above b i (inc_above b i x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dec_above b i (inc_above b i x) = x
[PROOF STEP]
by (auto simp: inc_above_def dec_above_def)


[STATEMENT]
lemma inc_above_dec_above_iff: "inc_above b i (dec_above b i x) = x \<longleftrightarrow> x < b \<or> b + i \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inc_above b i (dec_above b i x) = x) = (x < b \<or> b + i \<le> x)
[PROOF STEP]
by (auto simp: inc_above_def dec_above_def)


[STATEMENT]
lemma inj_on_dec_above: "inj_on (dec_above b i) {x. x < b \<or> b + i \<le> x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (dec_above b i) {x. x < b \<or> b + i \<le> x}
[PROOF STEP]
by (rule inj_on_inverseI[where g = "inc_above b i"]) (auto simp: inc_above_dec_above)


[STATEMENT]
lemma finite_inc_above_ne: "finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (inc_above b i x) \<noteq> c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (inc_above b i x) \<noteq> c}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (inc_above b i x) \<noteq> c}
[PROOF STEP]
fix b and f::"nat\<Rightarrow>'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (inc_above b i x) \<noteq> c}
[PROOF STEP]
assume f: "finite {x. f x \<noteq> c}"
[PROOF STATE]
proof (state)
this:
finite {x. f x \<noteq> c}

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (inc_above b i x) \<noteq> c}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {x. f x \<noteq> c}

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (inc_above b i x) \<noteq> c}
[PROOF STEP]
have "finite {x. f (x + i) \<noteq> c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. f (x + i) \<noteq> c}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite {x. f (x + i) \<noteq> c}
[PROOF STEP]
have "{x. f (x + i) \<noteq> c} = (+) i -` {x. f x \<noteq> c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. f (x + i) \<noteq> c} = (+) i -` {x. f x \<noteq> c}
[PROOF STEP]
by (auto simp: ac_simps)
[PROOF STATE]
proof (state)
this:
{x. f (x + i) \<noteq> c} = (+) i -` {x. f x \<noteq> c}

goal (1 subgoal):
 1. finite {x. f (x + i) \<noteq> c}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{x. f (x + i) \<noteq> c} = (+) i -` {x. f x \<noteq> c}

goal (1 subgoal):
 1. finite {x. f (x + i) \<noteq> c}
[PROOF STEP]
have "finite \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ((+) i -` {x. f x \<noteq> c})
[PROOF STEP]
by (rule finite_vimageI) (use f in auto)
[PROOF STATE]
proof (state)
this:
finite ((+) i -` {x. f x \<noteq> c})

goal (1 subgoal):
 1. finite {x. f (x + i) \<noteq> c}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
finite {x. f (x + i) \<noteq> c}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {x. f (x + i) \<noteq> c}

goal (1 subgoal):
 1. finite {x. f (x + i) \<noteq> c}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite {x. f (x + i) \<noteq> c}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {x. f (x + i) \<noteq> c}

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (inc_above b i x) \<noteq> c}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {x. f x \<noteq> c}
finite {x. f (x + i) \<noteq> c}
[PROOF STEP]
have "finite ({x. f x \<noteq> c} \<union> {x. f (x + i) \<noteq> c})"
[PROOF STATE]
proof (prove)
using this:
finite {x. f x \<noteq> c}
finite {x. f (x + i) \<noteq> c}

goal (1 subgoal):
 1. finite ({x. f x \<noteq> c} \<union> {x. f (x + i) \<noteq> c})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ({x. f x \<noteq> c} \<union> {x. f (x + i) \<noteq> c})

goal (1 subgoal):
 1. finite {x. f x \<noteq> c} \<Longrightarrow> finite {x. f (inc_above b i x) \<noteq> c}
[PROOF STEP]
from _ this
[PROOF STATE]
proof (chain)
picking this:
PROP ?psi \<Longrightarrow> PROP ?psi
finite ({x. f x \<noteq> c} \<union> {x. f (x + i) \<noteq> c})
[PROOF STEP]
show "finite {x. f (inc_above b i x) \<noteq> c}"
[PROOF STATE]
proof (prove)
using this:
PROP ?psi \<Longrightarrow> PROP ?psi
finite ({x. f x \<noteq> c} \<union> {x. f (x + i) \<noteq> c})

goal (1 subgoal):
 1. finite {x. f (inc_above b i x) \<noteq> c}
[PROOF STEP]
by (rule finite_subset) (auto simp: inc_above_def)
[PROOF STATE]
proof (state)
this:
finite {x. f (inc_above b i x) \<noteq> c}

goal:
No subgoals!
[PROOF STEP]
qed