Download HOL-TestGen: User Guide

apply
apply
apply
apply
apply
apply
apply
done
(simp add: PLemmas subnetsOfAdr_def)
(simp add: PLemmas subnetsOfAdr_def)
(rule impI)+
simp
(case_tac "p ∈ dom (C (Combinators2))")
simp_all
(auto simp: PLemmas subnetsOfAdr_def)
lemma disjSD_no_p_in_both[rule_format]:
"[[disjSD_2 x y; ¬ member DenyAll x; ¬ member DenyAll y;
p ∈ dom (C x); p ∈ dom (C y)]] =⇒ False"
apply (rule_tac A = "sdnets x" and B = "sdnets y" and D = "src p"
and F = "dest p" in tndFalse)
by (auto simp: dest_in_sdnets src_in_sdnets sdnets_in_subnets disjSD_2_def)
lemma list2policy_eq: "zs 6= [] =⇒
C (list2policy (x ⊕ y # z)) p = C (x ⊕ list2policy (y # z)) p"
apply (metis C.simps(4) CConcStartaux C_eq_None C_eq_RS3 C_eq_if_mr_eq C_eq_rd
Cdom2 ConcAssoc domIff in_set_conv_decomp l2p_aux2 list.simps(1)
list2policy.simps(2) list2policyconc map_add_None mem_def mrMTNone
mrconcNone mreq_end3 mreq_endNone nlpaux not_Cons_self
remdups.simps(2) removeShadowRules3.simps(2) self_append_conv2)
done
lemma sepnMT[rule_format]: "p 6= [] −→ (separate p) 6= []"
apply (rule separate.induct) back back back
by simp_all
lemma sepDA[rule_format]: "DenyAll ∈
/ set p −→ DenyAll ∈
/ set (separate p)"
apply (rule separate.induct) back
apply simp_all
done
lemma dom_sep[rule_format]: "x ∈ dom (C (list2policy p)) −→
x ∈ dom (C (list2policy(separate p)))"
apply (rule separate.induct) back
apply simp_all
apply (rule conjI)
apply (rule impI)+
apply simp
apply (thin_tac "False =⇒ ?S")
apply (drule mp)
apply (case_tac "x ∈ dom (C (DenyAllFromTo v va))")
apply (metis CConcStartA domIff eq_Nil_appendI in_set_conv_decomp l2p_aux2
list2policyconc mem_def not_Cons_self notindom)
apply (subgoal_tac "x ∈ dom (C (list2policy (y #z)))")
apply (metis CConcStartA Cdom2 InDomConc domIff l2p_aux2 list2policyconc nlpaux)
apply (subgoal_tac "x ∈ dom (C (list2policy ((DenyAllFromTo v va)#y#z)))")
apply (simp add: dom_def C.simps)
apply simp
apply simp
apply (rule impI)+
apply simp
apply (thin_tac "False =⇒ ?S")
apply (case_tac "x ∈ dom (C (DenyAllFromTo v va))")
154