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 "xset 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 "xset 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) = (aset a. set (f a))" 
unfolding List.maps_def set_concat set_map UN_simps(10) ..


end