Quelle  Rotation.thy

(*  Author:     Tobias Nipkow
*)

section ‹More Rotation›

theory Rotation
imports ListAux PlaneGraphIso
begin

definition rotate_to :: "'a list ==> 'a ==> 'a list" where
"rotate_to vs v ≡ v # snd (splitAt v vs) @ fst (splitAt v vs)"

definition rotate_min :: "nat list ==> nat list" where
"rotate_min vs ≡ rotate_to vs (min_list vs)"


lemma cong_rotate_to:
 "x ∈ set xs ==> xs ≅ rotate_to xs x"
proof -
  assume x: "x ∈ set xs"
  hence ls1: "xs = fst (splitAt x xs) @ x # snd (splitAt x xs)" by (auto dest: splitAt_ram)
  define i where "i = length(fst(splitAt x xs))"
  hence "i < length((fst(splitAt x xs)) @ [x] @ snd(splitAt x xs))" by auto
  with ls1 have i_len: "i < length xs" by auto
  hence ls2: "xs = take i xs @ xs!i # drop (Suc i) xs" by (auto intro: id_take_nth_drop)
  from i_len have "length (take i xs) = i" by auto
  with i_def have len_eq: "length(take i xs) = length(fst(splitAt x xs))" by auto
  moreover
  from ls1 ls2 have eq: "take i xs @ xs!i # drop (Suc i) xs = fst(splitAt x xs) @ x # snd(splitAt x xs)" by simp
  ultimately have
    v_simp: "x = xs!i" and
    take_i: "fst(splitAt x xs) = take i xs" and
    drop_i': "snd(splitAt x xs) = drop (Suc i) xs" by auto
  from i_len have ls3: "xs = take i xs @ drop i xs" by auto
  with take_i have eq: "xs = fst(splitAt x xs) @ drop i xs" by auto
  with ls1 have "fst(splitAt x xs) @ drop i xs = fst(splitAt x xs) @ x # snd(splitAt x xs)" by auto
  then have drop_i: "drop i xs = x # snd(splitAt x xs)" by auto
  have "rotate i xs = drop (i mod length xs) xs @ take (i mod length xs) xs" by (rule rotate_drop_take)
  with i_len have "rotate i xs = drop i xs @ take i xs" by auto
  with take_i drop_i have "rotate i xs = (x # snd(splitAt x xs)) @ fst(splitAt x xs)" by auto
  thus ?thesis apply (auto simp: congs_def rotate_to_def) apply (rule exI) apply (rule sym) .
qed

lemma face_cong_if_norm_eq:
 "[ rotate_min xs = rotate_min ys; xs ≠ []; ys ≠ [] ] ==> xs ≅ ys"
apply(simp add:rotate_min_def)
apply(subgoal_tac "xs ≅ rotate_to xs (Min (set xs))")
 apply(subgoal_tac "ys ≅ rotate_to ys (Min (set ys))")
  apply(simp) apply(blast intro:congs_sym congs_trans)
 apply(simp add: cong_rotate_to)
apply(drule sym)
apply(simp add: cong_rotate_to)
done

lemma norm_eq_if_face_cong:
  "[ xs ≅ ys; distinct xs; xs ≠ [] ] ==> rotate_min xs = rotate_min ys"
by(auto simp:congs_def rotate_min_def rotate_to_def
  splitAt_rotate_pair_conv insert_absorb)

lemma norm_eq_iff_face_cong:
 "[ distinct xs; xs ≠ []; ys ≠ [] ] ==>
  (rotate_min xs = rotate_min ys) = (xs ≅ ys)"
by(blast intro: face_cong_if_norm_eq norm_eq_if_face_cong)

lemma inj_on_rotate_min_iff:
assumes "∀vs ∈ A. distinct vs"  "[] ∉ A"
shows "inj_on rotate_min A = inj_on (λvs. {vs}//{≅}) A"
proof -
  { fix xs ys assume xs: "xs ∈ A" and ys : "ys ∈ A"
    hence "xs ≠ [] ∧ ys ≠ []" using assms(2) by blast
    hence "(rotate_min xs = rotate_min ys) = (xs ≅ ys)"
      using xs assms(1)
      by(simp add: singleton_list_cong_eq_iff norm_eq_iff_face_cong)
  } thus ?thesis by(simp add:inj_on_def)
qed


end