Download HOL-TestGen: User Guide

apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
apply
done
(rule impI)+
(rule conjI)
(rule impI)
(rotate_tac -1, drule sym)
simp
(rule impI)
(subgoal_tac "smaller (AllowPortFromTo a b w) (DenyAllFromTo u v) l")
(subgoal_tac "¬ smaller (DenyAllFromTo u v) (AllowPortFromTo a b w) l")
(simp split: if_splits)
(rule_tac y = aa and z = list in notSmallerTrans)
(simp_all del: smaller.simps)
(rule smalleraux3a)
(simp_all del: smaller.simps)
(case_tac aa, simp_all del: smaller.simps)
(case_tac aa, simp_all del: smaller.simps)
(rule_tac y = aa in order_trans)
(simp_all del: smaller.simps)
(subgoal_tac "in_list (DenyAllFromTo u v) l")
simp
(rule_tac p = list in in_set_in_list)
simp
simp
(rule_tac p = list in sorted_is_smaller)
(simp_all del: smaller.simps)
(subgoal_tac "in_list (DenyAllFromTo u v) l")
simp
(rule_tac p = list in in_set_in_list)
simp
simp
(erule singleCombinatorsConc)
lemma NCSaux4[rule_format]:
"noDenyAll p −→ {a, b} ∈ set l −→ all_in_list p l −→ singleCombinators p −→
sorted (AllowPortFromTo a b c # p) l −→ {a, b} 6= firstList p −→
AllowPortFromTo u v w ∈ set p −→ {a, b} 6= {u, v}"
apply (case_tac p)
apply simp_all
apply (rule impI)+
apply (rule conjI)
apply (rule impI)
apply (rotate_tac -1, drule sym)
apply simp
apply (rule impI)
apply (subgoal_tac "smaller (AllowPortFromTo a b c) (AllowPortFromTo u v w) l")
apply (subgoal_tac "¬ smaller (AllowPortFromTo u v w) (AllowPortFromTo a b c) l")
apply (simp split: if_splits)
apply (rule_tac y = aa and z = list in notSmallerTrans)
apply (simp_all del: smaller.simps)
apply (rule smalleraux3a)
apply (simp_all del: smaller.simps)
apply (case_tac aa, simp_all del: smaller.simps)
apply (case_tac aa, simp_all del: smaller.simps)
apply (case_tac aa, simp_all del: smaller.simps)
apply (rule_tac y = aa in order_trans)
181