theory Position
imports
"HOL-Library.Infinite_Set"
Show.Show_Instances
begin
type_synonym pos = "nat list"
definition less_eq_pos :: "pos ⇒ pos ⇒ bool" (infix "≤⇩p" 50)
where
"p ≤⇩p q ⟷ (∃r. p @ r = q)"
definition less_pos :: "pos ⇒ pos ⇒ bool" (infix "<⇩p" 50)
where
"p <⇩p q ⟷ p ≤⇩p q ∧ p ≠ q"
interpretation order_pos: order less_eq_pos less_pos
by (standard) (auto simp: less_eq_pos_def less_pos_def)
lemma Nil_least [intro!, simp]:
"[] ≤⇩p p"
by (auto simp: less_eq_pos_def)
lemma less_eq_pos_simps [simp]:
"p ≤⇩p p @ q"
"p @ q1 ≤⇩p p @ q2 ⟷ q1 ≤⇩p q2"
"i # q1 ≤⇩p [] ⟷ False"
"i # q1 ≤⇩p j # q2 ⟷ i = j ∧ q1 ≤⇩p q2"
"p @ q ≤⇩p p ⟷ q = []"
"p ≤⇩p [] ⟷ p = []"
by (auto simp: less_eq_pos_def)
lemma less_eq_pos_code [code]:
"([] :: pos) ≤⇩p p = True"
"(i # q1 ≤⇩p []) = False"
"(i # q1 ≤⇩p j # q2) = (i = j ∧ q1 ≤⇩p q2)"
by auto
lemma less_pos_simps[simp]:
"(p <⇩p p @ q) = (q ≠ [])"
"(p @ q1 <⇩p p @ q2) = (q1 <⇩p q2)"
"(p <⇩p []) = False"
"(i # q1 <⇩p j # q2) = (i = j ∧ q1 <⇩p q2)"
"(p @ q <⇩p p) = False"
by (auto simp: less_pos_def)
lemma prefix_smaller [simp]:
assumes "p <⇩p q" shows "size p < size q"
using assms by (auto simp: less_pos_def less_eq_pos_def)
instantiation list :: (type) one
begin
definition one_list_def [simp]: "1 = []"
instance by (intro_classes)
end
instantiation list :: (type) times
begin
definition times_list_def [simp]: "times p q = p @ q"
instance by (intro_classes)
end
instantiation list :: (type) semigroup_mult
begin
instance by (intro_classes) simp
end
instantiation list :: (type) power
begin
instance by (intro_classes)
end
lemma power_append_distr:
"p ^ (m + n) = p ^ m @ p ^ n"
by (induct m) auto
lemma power_pos_Suc: "p ^ Suc n = p ^ n @ p"
proof -
have "p ^ Suc n = p ^ (n + Suc 0)" by simp
also have "... = p ^ n @ p" unfolding power_append_distr by auto
finally show ?thesis .
qed
lemma power_subtract_less_eq:
"p ^ (n - m) ≤⇩p p ^ n"
proof (cases "m ≥ n")
case False
then have "(n - m) + m = n" by auto
then show ?thesis unfolding less_eq_pos_def using power_append_distr by metis
qed simp
lemma power_size: fixes p :: "pos" shows "size (p ^ n) = size p * n"
by (induct n, simp, auto)
fun remove_prefix :: "'a list ⇒ 'a list ⇒ 'a list option"
where
"remove_prefix [] ys = Some ys"
| "remove_prefix (x#xs) (y#ys) = (if x = y then remove_prefix xs ys else None)"
| "remove_prefix xs ys = None"
lemma remove_prefix [simp]:
"remove_prefix (x # xs) ys =
(case ys of
[] ⇒ None
| z # zs ⇒ if x = z then remove_prefix xs zs else None)"
by (cases ys) auto
lemma remove_prefix_Some [simp]:
"remove_prefix xs ys = Some zs ⟷ ys = xs @ zs"
by (induct xs ys rule: remove_prefix.induct) (auto)
lemma remove_prefix_append [simp]:
"remove_prefix xs (xs @ ys) = Some ys"
by simp
lemma less_eq_pos_remove_prefix:
assumes "p ≤⇩p q"
obtains r where "q = p @ r" and "remove_prefix p q = Some r"
using assms by (induct p arbitrary: q) (auto simp: less_eq_pos_def)
lemma suffix_exists:
assumes "p ≤⇩p q"
shows "∃r. p @ r = q ∧ remove_prefix p q = Some r"
using assms by (elim less_eq_pos_remove_prefix) auto
fun remove_suffix :: "'a list ⇒ 'a list ⇒ 'a list option"
where
"remove_suffix p q =
(case remove_prefix (rev p) (rev q) of
None ⇒ None
| Some r ⇒ Some (rev r))"
lemma remove_suffix_Some [simp]:
"remove_suffix xs ys = Some zs ⟷ ys = zs @ xs"
by (auto split: option.splits) (metis rev_append rev_rev_ident)
lemma Nil_power [simp]: "[] ^ n = []" by (induct n) auto
fun parallel_pos :: "pos ⇒ pos ⇒ bool" (infixr "⊥" 64)
where
"[] ⊥ _ ⟷ False"
| "_ ⊥ [] ⟷ False"
| "i # p ⊥ j # q ⟷ i ≠ j ∨ p ⊥ q"
lemma parallel_pos: "p ⊥ q = (¬ p ≤⇩p q ∧ ¬ q ≤⇩p p)"
by (induct p q rule: parallel_pos.induct) auto
lemma parallel_remove_prefix: "p1 ⊥ p2 ⟹
∃ p i j q1 q2. p1 = p @ i # q1 ∧ p2 = p @ j # q2 ∧ i ≠ j"
apply (induct p1 p2 rule: parallel_pos.induct)
apply auto
apply blast
by (metis append_Cons append_Nil)
lemma pos_cases: "p ≤⇩p q ∨ q <⇩p p ∨ p ⊥ q"
by (induct p q rule: parallel_pos.induct)
(auto simp: less_pos_def)
lemma parallel_pos_sym: "p1 ⊥ p2 ⟹ p2 ⊥ p1"
unfolding parallel_pos by auto
lemma less_pos_def': "(p <⇩p q) = (∃ r. q = p @ r ∧ r ≠ [])" (is "?l = ?r")
by (auto simp: less_pos_def less_eq_pos_def)
lemma pos_append_cases:
"p1 @ p2 = q1 @ q2 ⟹
(∃ q3. p1 = q1 @ q3 ∧ q2 = q3 @ p2) ∨
(∃ p3. q1 = p1 @ p3 ∧ p2 = p3 @ q2)"
proof (induct p1 arbitrary: q1)
case Nil
then show ?case by auto
next
case (Cons i p1' q1) note IH = this
show ?case
proof (cases q1)
case Nil
then show ?thesis using IH(2) by auto
next
case (Cons j q1')
with IH(2) have id: "p1' @ p2 = q1' @ q2" and ij: "i = j" by auto
from IH(1)[OF id]
show ?thesis unfolding Cons ij by auto
qed
qed
lemma pos_less_eq_append_not_parallel:
assumes "q ≤⇩p p @ q'"
shows "¬ (q ⊥ p)"
proof-
from assms obtain r where "q @ r = p @ q'" unfolding less_eq_pos_def ..
then have dec:"(∃ q3. q = p @ q3 ∧ q' = q3 @ r) ∨
(∃ p3. p = q @ p3 ∧ r = p3 @ q')" (is "?a ∨ ?b") by (rule pos_append_cases)
then have "p ≤⇩p q ∨ q ≤⇩p p" unfolding less_eq_pos_def by blast
then show ?thesis unfolding parallel_pos by auto
qed
lemma less_pos_power_split: "q <⇩p p ^ m ⟹ ∃ p' k. q = p ^ k @ p' ∧ p' <⇩p p ∧ k < m"
proof (induct m arbitrary: q)
case 0
then show ?case by auto
next
case (Suc n q)
show ?case
proof (cases "q <⇩p p")
case True
show ?thesis
by (rule exI[of _ q], rule exI[of _ 0], insert True, auto)
next
case False
from Suc(2) obtain r where pn: "p @ p^n = q @ r" unfolding less_pos_def' by auto
from pos_append_cases[OF this]
have "∃ r. q = p @ r"
proof
assume "∃ s. p = q @ s ∧ r = s @ p ^ n"
then obtain s where p: "p = q @ s" by auto
with False show ?thesis by auto
qed auto
then obtain r where q: "q = p @ r" by auto
with Suc(2) have "r <⇩p p ^ n" by simp
from Suc(1)[OF this] obtain p' k where r: "r = p ^ k @ p'" "p' <⇩p p" "k < n" by auto
show ?thesis unfolding q
by (rule exI[of _ p'], rule exI[of _ "Suc k"], insert r, auto)
qed
qed
definition shows_pos :: "pos ⇒ shows"
where
"shows_pos p = shows_list_gen shows ''[]'' ''['' '','' '']'' p"
fun proper_prefix_list :: "pos ⇒ pos list"
where
"proper_prefix_list [] = []" |
"proper_prefix_list (i # p) = [] # map (Cons i) (proper_prefix_list p)"
lemma proper_prefix_list [simp]: "set (proper_prefix_list p) = {q. q <⇩p p}"
proof (induction p)
case (Cons i p)
note IH = this
show ?case (is "?l = ?r")
proof (rule set_eqI)
fix q
show "q ∈ ?l = (q ∈ ?r)"
proof (cases q)
case Nil
have less: "[] <⇩p i # p" unfolding less_pos_def by auto
show ?thesis unfolding Nil using less by auto
next
case (Cons j q')
show ?thesis unfolding Cons by (auto simp: IH)
qed
qed
qed simp
definition prefix_list :: "pos ⇒ pos list"
where
"prefix_list p = p # proper_prefix_list p"
lemma prefix_list [simp]: "set (prefix_list p) = { q. q ≤⇩p p}"
by (auto simp: prefix_list_def)
definition bounded_postfixes :: "pos ⇒ pos list ⇒ pos list"
where
"bounded_postfixes p ps = map the [opt←map (remove_prefix p) ps . opt ≠ None]"
lemma bounded_postfixes [simp]:
"set (bounded_postfixes p ps) = { r. p @ r ∈ set ps}" (is "?l = ?r")
by (auto simp: bounded_postfixes_def)
(metis (mono_tags, lifting) image_eqI mem_Collect_eq option.sel remove_prefix_append)
definition left_of_pos :: "pos ⇒ pos ⇒ bool"
where
"left_of_pos p q = (∃r i j. r @ [i] ≤⇩p p ∧ r @ [j] ≤⇩p q ∧ i < j)"
lemma left_of_pos_append:
"left_of_pos p q ⟹ left_of_pos (p @ p') (q @ q')"
apply (auto simp: left_of_pos_def)
using less_eq_pos_simps(1) order_pos.order.trans by blast
lemma append_left_of_pos:
"left_of_pos p q = left_of_pos (p' @ p) (p' @ q)"
proof (rule iffI)
assume "left_of_pos p q"
then show "left_of_pos (p' @ p) (p' @ q)"
unfolding left_of_pos_def by (metis less_eq_pos_simps(2) append_assoc)
next
assume "left_of_pos (p' @ p) (p' @ q)"
then show "left_of_pos p q"
proof (induct p' arbitrary: p q rule:rev_induct)
case (snoc a p')
then have IH:"left_of_pos (p' @ p) (p' @ q) ⟹ left_of_pos p q" and
left:"left_of_pos ((p' @ [a]) @ p) ((p' @ [a]) @ q)" by auto
from left[unfolded left_of_pos_def] have "left_of_pos (p' @ (a # p)) (p' @ (a # q))"
by (metis append_assoc append_Cons append.left_neutral snoc.prems)
with IH have "left_of_pos (a # p) (a # q)" unfolding left_of_pos_def by (metis left_of_pos_def snoc.hyps)
then obtain r i j r' r'' where x:"r @ [i] @ r' = a # p" and y:"(r @ [j]) @ r'' = a # q"
and ij:"i < j" unfolding left_of_pos_def less_eq_pos_def by auto
then have "[] <⇩p r" unfolding less_pos_def'
by (metis append_Nil append_Cons not_less_iff_gr_or_eq list.inject)
with x obtain rr where "r = a # rr" using list.exhaust[of r]
by (metis less_eq_pos_simps(1) less_eq_pos_simps(4) less_pos_simps(1) append.left_neutral)
with x y have "rr @ [i] @ r' = p" and y:"(rr @ [j]) @ r'' = q" by auto
with ij show ?case unfolding left_of_pos_def less_eq_pos_def by auto
qed simp
qed
lemma left_pos_parallel: "left_of_pos p q ⟹ q ⊥ p" unfolding left_of_pos_def
proof -
assume "∃r i j. r @ [i] ≤⇩p p ∧ r @ [j] ≤⇩p q ∧ i < j"
then obtain r i j where rp:"r @ [i] ≤⇩p p" and rq:"r @ [j] ≤⇩p q" and ij:"i < j" by auto
from rp obtain p' where rp:"p = r @ i # p'" unfolding less_eq_pos_def by auto
from rq obtain q' where rq:"q = (r @ (j # q'))" unfolding less_eq_pos_def by auto
from rp rq ij have pq:"¬ p ≤⇩p q" by force
from rp rq ij have "¬ q ≤⇩p p" by force
with pq show ?thesis using parallel_pos by auto
qed
lemma left_of_append_cases:" left_of_pos (p0 @ p1) q ⟹ p0 <⇩p q ∨ left_of_pos p0 q"
proof -
assume "left_of_pos (p0 @ p1) q"
then obtain r i j where rp:"r @ [i] ≤⇩p (p0 @ p1)" and rq:"r @ [j] ≤⇩p q" and ij:"i < j"
unfolding left_of_pos_def by auto
show ?thesis proof(cases "p0 ≤⇩p r")
case True
with rq have "p0 <⇩p q"
by (metis less_eq_pos_simps(1) less_eq_pos_simps(5) less_pos_def list.simps(3) order_pos.order.trans)
then show ?thesis by auto
next
case False
then have aux:"¬ (∃ r'. p0 @ r' = r)" unfolding less_eq_pos_def by auto
from rp have par:"¬ (r @ [i] ⊥ p0)" using pos_less_eq_append_not_parallel by auto
from aux have a:"¬ (p0 ≤⇩p r)" unfolding less_eq_pos_def by auto
from rp have "¬ (p0 ⊥ r)"
using less_eq_pos_simps(1) order_pos.order.trans parallel_pos pos_less_eq_append_not_parallel by blast
with a have "r <⇩p p0" using pos_cases by auto
then obtain oo where p0:"p0 = r @ oo" and "[] <⇩p oo" unfolding less_pos_def less_eq_pos_def by auto
have "¬ (p0 <⇩p r @ [i])" unfolding less_pos_def less_eq_pos_def
by (metis aux butlast_append butlast_snoc self_append_conv)
with par have "r @ [i] ≤⇩p p0" using pos_cases by auto
with ij this[unfolded less_eq_pos_def] have "left_of_pos p0 q" unfolding left_of_pos_def using rq by auto
then show ?thesis by auto
qed
qed
lemma append_left_of_cases:
assumes left: "left_of_pos q (p0 @ p1)"
shows "p0 <⇩p q ∨ left_of_pos q p0"
proof -
from left obtain r i j where rp:"r @ [i] ≤⇩p q" and rq:"r @ [j] ≤⇩p (p0 @ p1)" and ij:"i < j"
unfolding left_of_pos_def by auto
show ?thesis proof(cases "p0 ≤⇩p r")
case True
with rp have "p0 <⇩p q" unfolding less_pos_def
by (meson less_eq_pos_simps(1) less_eq_pos_simps(5) list.simps(3) order_pos.order.trans)
then show ?thesis by auto
next
case False
then have aux:"¬ (∃ r'. p0 @ r' = r)" unfolding less_eq_pos_def by auto
from rp rq have par:"¬ (r @ [j] ⊥ p0)" using pos_less_eq_append_not_parallel by auto
from aux have a:"¬ (p0 ≤⇩p r)" unfolding less_eq_pos_def by auto
from rq have "¬ (p0 ⊥ r)"
using less_eq_pos_simps(1) order_pos.order.trans parallel_pos pos_less_eq_append_not_parallel by blast
with a have "r <⇩p p0" using pos_cases by auto
then obtain oo where p0:"p0 = r @ oo" and "[] <⇩p oo" unfolding less_pos_def less_eq_pos_def by auto
have "¬ (p0 <⇩p r @ [j])" unfolding less_pos_def less_eq_pos_def using p0 a list.exhaust[of p0]
by (metis append_Nil2 aux butlast_append butlast_snoc)
with par have "r @ [j] ≤⇩p p0" using pos_cases by auto
with ij this[unfolded less_eq_pos_def] have "left_of_pos q p0" unfolding left_of_pos_def using rp by auto
then show ?thesis by auto
qed
qed
lemma parallel_imp_right_or_left_of:
assumes par:"p ⊥ q" shows "left_of_pos p q ∨ left_of_pos q p"
proof -
from parallel_remove_prefix[OF par] obtain r i j p' q' where "p = r @ i# p'" and "q = r @ j # q'"
and ij:"i ≠ j" by blast
then have "r @ [i] ≤⇩p p ∧ r @ [j] ≤⇩p q" by simp
then show ?thesis unfolding left_of_pos_def using ij less_linear by blast
qed
lemma left_of_imp_not_right_of:
assumes l:"left_of_pos p q" shows "¬ left_of_pos q p"
proof
assume l':"left_of_pos q p"
from l obtain r i j where "r @ [i] ≤⇩p p" and ij:"i < j" and "r @ [j] ≤⇩p q" unfolding left_of_pos_def by blast
then obtain p0 q0 where p:"p = (r @ [i]) @ p0" and q:"q = (r @ [j]) @ q0" unfolding less_eq_pos_def by auto
from l' obtain r' i' j' where "r' @ [j'] ≤⇩p p" and ij':"i' < j'" and "r' @ [i'] ≤⇩p q" unfolding left_of_pos_def by blast
then obtain p0' q0' where p':"p = (r' @ [j']) @ p0'" and q':"q = (r' @ [i']) @ q0'" unfolding less_eq_pos_def by auto
from p p' have p:"r @ (i # p0) = r' @ (j' # p0')" by auto
from q q' have q:"r @ (j # q0) = r' @ (i' # q0')" by auto
with p ij ij' have ne:"r ≠ r'" using same_append_eq[of r] by (metis less_imp_not_less list.inject)
have nlt:"¬ r <⇩p r'" proof
assume "r <⇩p r'"
then obtain r2 where r1:"r' = r @ r2" and r2:"r2 ≠ []" unfolding less_pos_def less_eq_pos_def by auto
from p have p':"i # p0 = r2 @ j' # p0'" unfolding r1 append_assoc using less_eq_pos_simps(2) by auto
from q have q':"j # q0 = r2 @ i' # q0'" unfolding r1 append_assoc using less_eq_pos_simps(2) by auto
from r2 obtain k rr where r2:"r2 = k# rr" by (cases r2, auto)
from p' q' ij list.inject show False unfolding r2 by simp
qed
have "¬ r' <⇩p r" proof
assume "r' <⇩p r"
then obtain r2 where r1:"r = r' @ r2" and r2:"r2 ≠ []" unfolding less_pos_def less_eq_pos_def by auto
from p have p':"r2 @ i # p0 = j' # p0'" unfolding r1 append_assoc using less_eq_pos_simps(2) by auto
from q have q':"r2 @ j # q0 = i' # q0'" unfolding r1 append_assoc using less_eq_pos_simps(2) by auto
from r2 obtain k rr where r2:"r2 = k# rr" by (cases r2, auto)
from p' q' ij' list.inject show False unfolding r2 by simp
qed
with nlt ne have "r ⊥ r'" by (auto simp: parallel_pos less_pos_def)
with p q show False by (metis less_eq_pos_simps(1) pos_less_eq_append_not_parallel)
qed
primrec is_left_of :: "pos ⇒ pos ⇒ bool"
where
left_Nil: "is_left_of [] q = False"
| left_Cons: "is_left_of (i # p) q =
(case q of
[] ⇒ False
| j # q' ⇒ if i < j then True else if i > j then False else is_left_of p q')"
lemma is_left_of: "is_left_of p q = left_of_pos p q"
proof
assume l:"is_left_of p q"
then show "left_of_pos p q"
proof (induct p arbitrary:q)
case Nil
with left_Nil show ?case by auto
next
case (Cons i p) note IH = this
assume l:"is_left_of (i # p) q"
show ?case
proof (cases q)
case Nil
with l show ?thesis unfolding left_Cons by auto
next
case (Cons j q')
show ?thesis
proof (cases "¬ (i < j)", cases "j < i")
case True
with l Cons show ?thesis unfolding left_Cons by auto
next
assume "¬ j < i" and "¬ i < j"
then have ij:"i = j" by auto
with Cons l have "is_left_of p q'" unfolding left_Cons by auto
with IH have "left_of_pos p q'" by blast
with ij show "left_of_pos (i # p) q" unfolding Cons left_of_pos_def
by (metis append_Cons less_eq_pos_simps(4))
next
assume ij:"¬ ¬ (i < j)"
then have "[] @ [i] ≤⇩p (i # p) ∧ [] @ [j] ≤⇩p (j # q')" unfolding less_eq_pos_def by auto
with Cons ij show ?thesis unfolding left_of_pos_def by blast
qed
qed
qed
next
assume l:"left_of_pos p q"
from this[unfolded left_of_pos_def] obtain r i j where "r @[i] ≤⇩p p" and "r @ [j] ≤⇩p q"
and ij:"i < j" by blast
then obtain p' q' where "p = (r @[i]) @ p'" and "q = (r @[j]) @ q'" unfolding less_eq_pos_def
by auto
then show "is_left_of p q"
proof (induct r arbitrary: p q p' q')
case Nil
assume p:"p = ([] @ [i]) @ p'" and q:"q = ([] @ [j]) @ q'"
with l[unfolded p q append_Nil] show ?case using left_Cons ij by force
next
case (Cons k r') note IH = this
assume p:"p = ((k # r') @ [i]) @ p'" and q:"q = ((k # r') @ [j]) @ q'"
from ij have "left_of_pos ((r' @ [i]) @ p') (( r' @ [j]) @ q')" unfolding left_of_pos_def
by (metis less_eq_pos_def)
with IH have "is_left_of ((r' @ [i]) @ p') (( r' @ [j]) @ q')" by auto
then show "is_left_of p q" unfolding p q using left_Cons by force
qed
qed
abbreviation right_of_pos :: "pos ⇒ pos ⇒ bool"
where
"right_of_pos p q ≡ left_of_pos q p"
lemma remove_prefix_same [simp]:
"remove_prefix p p = Some []"
by (induct p) simp_all
definition "pos_diff p q = the (remove_prefix q p)"
lemma prefix_pos_diff [simp]:
assumes "p ≤⇩p q"
shows "p @ pos_diff q p = q"
using suffix_exists [OF assms] by (auto simp: pos_diff_def)
lemma pos_diff_Nil2 [simp]:
"pos_diff p [] = p"
by (auto simp: pos_diff_def)
lemma inj_nat_to_pos: "inj (rec_nat [] Cons)" (is "inj ?f")
unfolding inj_on_def
proof (intro ballI impI)
fix x y
show "?f x = ?f y ⟹ x = y"
proof (induct x arbitrary: y)
case 0
then show ?case by (cases y, auto)
next
case (Suc x sy)
then obtain y where sy: "sy = Suc y" by (cases sy, auto)
from Suc(2)[unfolded sy] have id: "?f x = ?f y" by auto
from Suc(1)[OF this] sy show ?case by simp
qed
qed
lemma infinite_UNIV_pos[simp]: "infinite (UNIV :: pos set)"
proof
assume "finite (UNIV :: pos set)"
from finite_subset[OF _ this, of "range (rec_nat [] Cons)"]
range_inj_infinite[OF inj_nat_to_pos]
show False by blast
qed
lemma less_pos_right_mono:
"p @ q <⇩p r @ q ⟹ p <⇩p r"
apply (induct q rule: rev_induct)
apply (auto simp: less_pos_def less_eq_pos_def)
by (metis append_is_Nil_conv butlast_append butlast_snoc list.simps(3))
lemma less_pos_left_mono:
"p @ q <⇩p p @ r ⟹ q <⇩p r"
by auto
end