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) (* by(induction l) simp_all *)

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) (* uuuh *)
	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