Theory OpenFlow_Helpers
section‹Misc›
theory OpenFlow_Helpers
imports Main
begin
lemma hrule: "(S = UNIV) = (∀x. x ∈ S)"
by blast
subsection‹Single valuedness on lists›
lemma foldr_True_set: "foldr (λx. (∧) (f x)) l True = (∀x ∈ set l. f x)"
by (induction l) simp_all
fun single_valued_code where
"single_valued_code [] = True" |
"single_valued_code (e#es) = (foldr (λx. (∧) (fst x ≠ fst e ∨ snd x = snd e)) es True ∧ single_valued_code es)"
lemma single_valued_code_lam[code_unfold]:
"single_valued (set r) = single_valued_code r"
proof(induction r)
case Nil show ?case by simp
next
case (Cons e es)
show ?case
proof (rule iffI, goal_cases fwd bwd)
case bwd
have "single_valued (set es)" using Cons.IH conjunct2[OF bwd[unfolded single_valued_code.simps]] ..
moreover
have "∀x∈set es. fst x ≠ fst e ∨ snd x = snd e"
using conjunct1[OF bwd[unfolded single_valued_code.simps(2)], unfolded foldr_True_set] .
ultimately
show ?case unfolding single_valued_def by auto
next
case fwd
have "single_valued (set es)" using fwd unfolding single_valued_def by simp
with Cons.IH[symmetric] have "single_valued_code es" ..
moreover
have "∀x∈set es. fst x ≠ fst e ∨ snd x = snd e" using fwd unfolding single_valued_def by clarsimp
from conjI[OF this calculation, unfolded foldr_True_set[symmetric]]
show ?case unfolding single_valued_code.simps .
qed
qed
lemma set_Cons: "e ∈ set (a # as) ⟷ (e = a ∨ e ∈ set as)" by simp
subsection‹List fun›
lemma sorted_const: "sorted (map (λy. x) k)"
by(induction k) simp_all
lemma list_all_map: "list_all f (map g l) = list_all (f ∘ g) l"
unfolding comp_def by (simp add: list_all_length)
lemma distinct_2lcomprI: "distinct as ⟹ distinct bs ⟹
(⋀a b e i. f a b = f e i ⟹ a = e ∧ b = i) ⟹
distinct [f a b. a ← as, b ← bs]"
apply(induction as)
apply(simp;fail)
apply(clarsimp simp only: distinct.simps simp_thms list.map concat.simps map_append distinct_append)
apply(rule)
subgoal
apply(clarify;fail | subst distinct_map, rule)+
by (rule inj_onI) simp
subgoal by fastforce
done
lemma distinct_3lcomprI: "distinct as ⟹ distinct bs ⟹ distinct cs ⟹
(⋀a b c e i g. f a b c = f e i g ⟹ a = e ∧ b = i ∧ c = g) ⟹
distinct [f a b c. a ← as, b ← bs, c ← cs]"
apply(induction as)
apply(simp;fail)
apply(clarsimp simp only: distinct.simps simp_thms list.map concat.simps map_append distinct_append)
apply(rule)
apply(rule distinct_2lcomprI; simp_all; fail)
apply fastforce
done
lemma distinct_fst: "distinct (map fst a) ⟹ distinct a" by (metis distinct_zipI1 zip_map_fst_snd)
lemma distinct_snd: "distinct (map snd a) ⟹ distinct a" by (metis distinct_zipI2 zip_map_fst_snd)
lemma inter_empty_fst2: "(λ(p, m, a). (p, m)) ` S ∩ (λ(p, m, a). (p, m)) ` T = {} ⟹ S ∩ T = {}" by blast
subsection‹Cardinality and Existence of Distinct Members›
lemma card1_eI: "1 ≤ card S ⟹ ∃y S'. S = {y} ∪ S' ∧ y ∉ S'"
by (metis One_nat_def card.infinite card_le_Suc_iff insert_is_Un leD zero_less_Suc)
lemma card2_eI: "2 ≤ card S ⟹ ∃x y. x ≠ y ∧ x ∈ S ∧ y ∈ S"
proof goal_cases
case (1)
then have "1 ≤ card S" by simp
note card1_eI[OF this]
then obtain x S' where xs: "S = {x} ∪ S' ∧ x ∉ S'" by presburger
then have "1 ≤ card S'"
by (metis 1 Suc_1 card.infinite card_insert_if finite_Un insert_is_Un le0 not_less_eq_eq)
then obtain y where "y ∈ S'" by fastforce
then show ?case using xs by force
qed
lemma card3_eI: "3 ≤ card S ⟹ ∃x y z. x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ x ∈ S ∧ y ∈ S"
proof goal_cases
case 1
then have "2 ≤ card S" by simp
note card2_eI[OF this]
then obtain x y S' where xs: "S = {x,y} ∪ S' ∧ x ∉ S' ∧ y ∉ S' ∧ x ≠ y"
by (metis Set.set_insert Un_insert_left insert_eq_iff insert_is_Un)
then have "1 ≤ card S'"
using 1 by (metis One_nat_def Suc_leI Un_insert_left card_gt_0_iff insert_absorb numeral_3_eq_3 singleton_insert_inj_eq card.infinite card_insert_if finite_Un insert_is_Un le0 not_less_eq_eq)
then obtain z where "z ∈ S'" by fastforce
then show ?case using xs by force
qed
lemma card1_eE: "finite S ⟹ ∃y. y ∈ S ⟹ 1 ≤ card S" using card_0_eq by fastforce
lemma card2_eE: "finite S ⟹ ∃x y. x ≠ y ∧ x ∈ S ∧ y ∈ S ⟹ 2 ≤ card S"
using card1_eE card_Suc_eq card_insert_if by fastforce
lemma card3_eE: "finite S ⟹ ∃x y z. x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ x ∈ S ∧ y ∈ S ⟹ 3 ≤ card S"
using card2_eE card_Suc_eq card_insert_if oops
lemma f_Img_ex_set: "{f x|x. P x} = f ` {x. P x}" by auto
lemma set_maps: "set (List.maps f a) = (⋃a∈set a. set (f a))"
unfolding List.maps_def set_concat set_map UN_simps(10) ..
end