Download HOL-TestGen: User Guide

apply simp_all
apply (case_tac "a = α1")
apply simp_all
apply (rule basic_trans_rules(18))
apply simp
apply (rule posaux3)
apply simp
apply simp
apply simp
apply (rule basic_trans_rules(18))
apply simp
apply (rule posaux3)
apply simp
apply simp
apply simp
apply (rule basic_trans_rules(18))
apply simp
apply (rule posaux3)
apply simp
apply simp
apply simp
apply (rule basic_trans_rules(18))
apply (rule_tac a = "DenyAllFromTo a b" and b = aa in posaux4)
apply simp_all
apply (case_tac aa,simp_all)
apply (case_tac aa, simp_all)
apply (rule posaux3)
apply simp_all
apply (case_tac aa, simp_all)
apply (simp split: if_splits)
apply (rule_tac a = aa and b = "AllowPortFromTo u v w" in posaux4)
apply simp_all
apply (case_tac aa,simp_all)
apply (rule_tac p = list in sorted_is_smaller)
apply simp_all
apply (case_tac aa, simp_all)
apply (case_tac aa, simp_all)
apply (rule_tac a = aa and b = "AllowPortFromTo u v w" in posaux4)
apply simp_all
apply (case_tac aa,simp_all)
apply (subgoal_tac "in_list (AllowPortFromTo u v w) l")
apply simp
apply (rule_tac p = list in in_set_in_list)
apply simp
defer 1
apply simp_all
apply (metis all_in_list.simps(2) sorted_Cons mem_def)
apply (case_tac aa, simp_all)
done
lemma NCSaux3[rule_format]:
"noDenyAll p −→ {a, b} ∈ set l −→ all_in_list p l −→singleCombinators p −→
sorted (AllowPortFromTo a b w # p) l −→ {a, b} 6= firstList p −→
DenyAllFromTo u v ∈ set p −→ {a, b} 6= {u, v}"
apply (case_tac p)
apply simp_all
180