# Theory Rotation

Up to index of Isabelle/HOL/Tame

theory Rotation
imports ListAux PlaneGraphIso
begin

```(*  ID:         \$Id: Rotation.thy,v 1.1 2006/01/04 13:44:05 nipkow Exp \$
Author:     Tobias Nipkow
*)

theory Rotation
imports ListAux PlaneGraphIso
begin

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

rotate_min :: "nat list => nat list"
"rotate_min vs ≡ rotate_to vs (minList 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)
def 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 arith
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(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(drule sym)
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 prems(2) by blast
hence "(rotate_min xs = rotate_min ys) = (xs ≅ ys)"
using xs prems(1)
qed

end
```

lemma cong_rotate_to:

`  x ∈ set xs ==> xs ≅ rotate_to xs x`

lemma face_cong_if_norm_eq:

`  [| rotate_min xs = rotate_min ys; xs ≠ []; ys ≠ [] |] ==> xs ≅ ys`

lemma norm_eq_if_face_cong:

`  [| xs ≅ ys; distinct xs; xs ≠ [] |] ==> rotate_min xs = rotate_min ys`

lemma norm_eq_iff_face_cong:

```  [| distinct xs; xs ≠ []; ys ≠ [] |]
==> (rotate_min xs = rotate_min ys) = xs ≅ ys```

lemma inj_on_rotate_min_iff:

```  [| ∀vs∈A. distinct vs; [] ∉ A |]
==> inj_on rotate_min A = inj_on (λvs. {vs} // {≅}) A```