theory Position
imports
"HOL-Library.Infinite_Set"
"Show.Show_Instances"
begin
datatype pos = Empty ("ε") | PCons "nat" "pos" (infixr "<#" 70)
primrec append :: "pos ⇒ pos ⇒ pos" (infixr "<#>" 70) where
append_Empty: "ε <#> q = q" |
append_PCons: "(i <# p) <#> q = i <# (p <#> q)"
abbreviation singleton :: "nat ⇒ pos" ("<_>") where "<i> == i<#ε"
abbreviation snoc :: "pos ⇒ nat ⇒ pos" (infixl "#>" 70) where "p#>i == p <#> <i>"
lemma not_PCons_self[simp]: "p ≠ i<#p" by (induct p) auto
lemmas not_PCons_self2[simp] = not_PCons_self[symmetric]
lemma not_snoc_self[simp]: "p ≠ p#>i" by (induct p) auto
lemmas not_snoc_self2[simp] = not_snoc_self[symmetric]
lemma impossible_PCons: "size p ≤ size q ⟹ p = i<#q = False" by (induct p) auto
lemma size_0_conv[iff]: "(0 = size p) = (p = ε)" by (cases p) auto
lemma size_greater_0_conf[iff]: "(0 < size p) = (p ≠ ε)" by (cases p) auto
lemma append_assoc[simp]: fixes p q r :: "pos" shows "(p <#> q) <#> r = p <#> (q <#> r)" by (induct p) auto
lemma append_Empty2[simp]: "p <#> ε = p" by (induct p) auto
lemma size_append[iff]: fixes p :: "pos" shows "size(p <#> q) = size p + size q" by (induct p) auto
interpretation semigroup_append: semigroup_add "op <#> :: pos ⇒ pos ⇒ pos" by unfold_locales simp
interpretation monoid_append: monoid_add "op <#> :: pos ⇒ pos ⇒ pos" "ε" by unfold_locales simp+
lemma append_is_Empty_conv[iff]: "(p <#> q = ε) = (p = ε ∧ q = ε)" by (induct p) auto
lemma Empty_is_append_conv[iff]: "(ε = p <#> q) = (p = ε ∧ q = ε)" by (induct p) auto
lemma append_self_conv[iff]: "(p <#> q = p) = (q = ε)" by (induct p) auto
lemma self_append_conv[iff]: "(p = p <#> q) = (q = ε)" by (induct p) auto
lemma append_eq_append_conv[simp,no_atp]:
fixes p q r s :: "pos"
assumes "size p = size q ∨ size r = size s"
shows "(p <#> r = q <#> s) = (p = q ∧ r = s)"
using assms proof (induct p arbitrary: q)
case Empty thus ?case by (cases q,simp,force)
next
case (PCons i p) thus ?case by (cases q,force,simp)
qed
lemma same_append_eq[iff]: fixes p :: "pos" shows "(p <#> q = p <#> r) = (q = r)" by simp
lemma same_append_eq'[iff]: fixes p :: "pos" shows "(q <#> p = r <#> p) = (q = r)" by simp
primrec rev :: "pos ⇒ pos"
where "rev ε = ε"
| "rev(i<#p) = rev p #> i"
lemma rev_append[simp]: fixes p :: "pos" shows "rev(p <#> q) = rev q <#> rev p" by (induct p) auto
lemma rev_rev_ident[simp]: fixes p :: "pos" shows "rev(rev p) = p" by (induct p) auto
lemma rev_size[simp]: fixes p :: "pos" shows "size(rev p) = size p" by (induct p) auto
lemma rev_inj: assumes "rev xs = rev ys" shows "xs = ys" using arg_cong[OF assms, of rev] by simp
lemma rev_induct[case_names Empty snoc]:
fixes P :: "pos ⇒ bool" assumes A: "P ε" and B: "⋀i q. P q ⟹ P(q#>i)"
shows "P p"
using assms by (simplesubst rev_rev_ident[symmetric],induct rule: pos.induct[where pos = "rev p"]) simp_all
lemma [simp]: "i<#p ≠ ε" by simp
lemma [simp]: "ε ≠ i<#p" by simp
lemma [simp]: "p#>i ≠ ε" by simp
lemma [simp]: "ε ≠ p#>i" by simp
instantiation pos :: order begin
definition less_eq_pos :: "pos ⇒ pos ⇒ bool" where "less_eq_pos p q == (∃r. (p <#> r) = q)"
definition less_pos :: "pos ⇒ pos ⇒ bool" where "less_pos p q == (p ≤ q ∧ p ≠ q)"
instance by (intro_classes, auto simp: less_eq_pos_def less_pos_def)
end
lemma Empty_least [intro!, simp]:
"(ε :: pos) ≤ p"
by (auto simp: less_eq_pos_def)
lemma less_eq_simps[simp]:
"p ≤ p <#> q"
"(p <#> q1 ≤ p <#> q2) = (q1 ≤ q2)"
"(i <# q1 ≤ ε) = False"
"(i <# q1 ≤ j <# q2) = (i = j ∧ q1 ≤ q2)"
"(p <#> q ≤ p) = (q = ε)" unfolding less_eq_pos_def by auto
lemma [code]: "(ε :: pos) ≤ p = True"
"(i <# q1 ≤ ε) = False"
"(i <# q1 ≤ j <# q2) = (i = j ∧ q1 ≤ q2)" by auto
lemma less_simps[simp]:
"(p < p <#> q) = (q ≠ ε)"
"(p <#> q1 < p <#> q2) = (q1 < q2)"
"(p < ε) = False"
"(i <# q1 < j <# q2) = (i = j ∧ q1 < q2)"
"(p <#> q < p) = False" unfolding less_pos_def less_eq_pos_def by auto
lemma prefix_smaller[simp]: fixes p :: "pos" assumes "p < q" shows "size p < size q"
using assms unfolding less_pos_def less_eq_pos_def by auto
lemma size_induct:
fixes p :: "pos"
assumes "⋀p. (∀q. size q < size p ⟶ P q) ⟹ P p" shows "P p"
using assms by (rule measure_induct[of "size"]) iprover
lemma prefix_induct:
fixes p :: "pos"
assumes "⋀p. (∀q<p. P q) ⟹ P p" shows "P p"
using assms by (rule measure_induct[of "size"]) auto
interpretation pos: semigroup_mult "op <#> :: pos ⇒ pos ⇒ pos" by (unfold_locales) simp
interpretation pos: monoid_mult "ε :: pos" "op <#> :: pos ⇒ pos ⇒ pos" by unfold_locales simp_all
instantiation pos :: one begin
definition one_pos_def[simp]: "1 = ε"
instance by (intro_classes)
end
instantiation pos :: times begin
definition times_pos_def[simp]: "times p q = p <#> q"
instance by (intro_classes)
end
instantiation pos :: power begin
instance by (intro_classes)
end
instantiation pos :: semigroup_mult begin
instance proof
fix a b c::pos show "a * b * c = a * (b * c)" by simp
qed
end
lemma power_append_distr: "p^(m+n) = p^(m::nat) <#> 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::pos)^((n::nat) - m) ≤ p^n"
proof(cases "m ≥ n",simp)
case False
hence "(n -m) + m = n" by auto
thus ?thesis unfolding less_eq_pos_def using power_append_distr by metis
qed
lemma power_size: fixes p :: "pos" shows "size (p^n) = size p * n"
by (induct n, simp, auto)
primrec pos_prefix :: "pos ⇒ pos ⇒ pos option"
where pre_Empty: "pos_prefix ε q = Some q"
| pre_PCons: "pos_prefix (i <# p) q =
(case q of ε ⇒ None | j <# q' ⇒ if i=j then pos_prefix p q' else None)"
lemma prefix_sound:
"pos_prefix p q = Some r ⟹ p <#> r = q"
proof (induct p arbitrary: q,simp)
case (PCons i p) note IH = this
thus ?case
proof(cases q,simp)
case (PCons j q')
with IH have pq':"pos_prefix p q' = Some r" using pre_PCons option.distinct(1) by (cases "i = j",simp,force)
have "i = j" using PCons option.distinct(1) pre_PCons IH by (cases "i = j",simp,force)
with pq' IH PCons show "(i <# p) <#> r = q" by auto
qed
qed
lemma prefix_exists:
assumes "p ≤ q"
shows "∃ q'. p <#> q' = q ∧ pos_prefix p q = Some q'"
using assms
proof (induct p arbitrary: q)
case (PCons i p')
from PCons have "∃ q'. q = i <# q'" by (auto simp: less_eq_pos_def)
then obtain q' where q_is: "q = i <# q'" and leq': "p' ≤ q'" using PCons by auto
then have res: "pos_prefix (i <# p') q = pos_prefix p' q'" by (auto simp: pos_prefix_def)
then have "∃ r. p' <#> r = q' ∧ pos_prefix p' q' = Some r" using leq' and PCons by auto
then obtain r where "p' <#> r = q'" and "pos_prefix p' q' = Some r" by auto
then show ?case using q_is and res by auto
qed simp
fun pos_suffix :: "pos ⇒ pos ⇒ pos option"
where "pos_suffix p q = (case pos_prefix (rev p) (rev q) of
None ⇒ None | Some q' ⇒ Some (rev q'))"
lemma suffix_sound: "pos_suffix p q = Some r ⟹ r <#> p = q" (is "?l ⟹ ?r")
proof-
assume ?l
hence "pos_prefix (rev p) (rev q) = Some (rev r)" using option.distinct(1)
by (cases "pos_prefix (rev p) (rev q)",simp,auto)
thus ?thesis using prefix_sound rev_append rev_inj by auto
qed
lemma suffix_complete:
"∃r. r <#> p = q ⟹ ∃r. r <#> p = q ∧ pos_suffix p q = Some r" (is "?ls ⟹ ?rs")
proof-
assume ?ls
hence "rev p ≤ rev q" using rev_append less_eq_pos_def by auto
hence "∃ q'. (rev p) <#> q' = (rev q) ∧ pos_prefix (rev p) (rev q) = Some q'" using prefix_exists by auto
then obtain r where r:"(rev p) <#> r = (rev q)" and "pos_prefix (rev p) (rev q) = Some r" by auto
hence "pos_suffix p q = Some (rev r)" and "rev ((rev r) <#> p) = rev q" using rev_rev_ident rev_append by auto
thus ?rs using rev_inj by auto
qed
text ‹Hide unqualified names of constants that are already used elsewhere.›
hide_const (open) append rev
lemma pos_exhaust_rev[case_names empty snoc]:
assumes "p = ε ⟹ P" and "⋀π i. p = π#>i ⟹ P" shows "P"
using assms by (induct p rule:rev_induct) auto
lemma epsilon_power_epsilon[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 ≤ q ∧ ¬ q ≤ p)"
proof (induct p arbitrary: q)
case Empty
show ?case by simp
next
case (PCons i p q) note IH = this
show ?case
proof (cases q)
case Empty
thus ?thesis by simp
next
case (PCons j q')
show ?thesis
proof (cases "i = j")
case False
thus ?thesis unfolding PCons by simp
next
case True
with IH[of q'] show ?thesis unfolding PCons by auto
qed
qed
qed
lemma parallel_pos_prefix: "p1 ⊥ p2 ⟹
∃ p i j q1 q2. p1 = p <#> i <# q1 ∧ p2 = p <#> j <# q2 ∧ i ≠ j"
proof (induct p1 arbitrary: p2)
case Empty thus ?case by simp
next
case (PCons i p1)
from PCons(2) obtain j p2' where p2: "p2 = j <# p2'" by (cases p2, auto)
with PCons(2) have "i ≠ j ∨ (i = j) ∧ p1 ⊥ p2'" by simp
thus ?case
proof
assume ij: "i ≠ j"
show ?case
proof (intro exI conjI)
show "i <# p1 = ε <#> i <# p1" by simp
next
show "p2 = ε <#> j <# p2'" unfolding p2 by simp
qed (rule ij)
next
assume "i = j ∧ p1 ⊥ p2'" hence
p12: "p1 ⊥ p2'" and ij: "i = j" by auto
from PCons(1)[OF p12] obtain p i' j' q1 q2 where p1: "p1 = p <#> i' <# q1"
and p2': "p2' = p <#> j' <# q2" and ij': "i' ≠ j'" by blast
show ?thesis
proof (intro exI conjI)
show "i <# p1 = (i <# p) <#> i' <# q1" unfolding p1 by simp
next
show "p2 = (i <# p) <#> j' <# q2" unfolding p2 p2' ij by simp
qed (rule ij')
qed
qed
lemma position_cases: "p ≤ q ∨ q < p ∨ p ⊥ q"
proof (cases "p ⊥ q")
case True thus ?thesis by auto
next
case False
from this[unfolded parallel_pos] have "p ≤ q ∨ (¬ p ≤ q ∧ q ≤ p)" by auto
thus ?thesis
proof
assume "p ≤ q" thus ?thesis by auto
next
assume "¬ p ≤ q ∧ q ≤ p"
hence "q < p" by auto
thus ?thesis by auto
qed
qed
lemma parallel_pos_sym: "p1 ⊥ p2 ⟹ p2 ⊥ p1"
unfolding parallel_pos by auto
lemma less_pos_def': "(p < q) = (∃ r. q = p <#> r ∧ r ≠ ε)" (is "?l = ?r")
proof
assume ?r then obtain r where id: "p <#> r = q" "r ≠ ε" by blast
show ?l unfolding less_pos_def less_eq_pos_def
by (rule conjI[OF exI[of _ r]], unfold id[symmetric], insert id(2), auto)
next
assume ?l
then obtain r where id: "p <#> r = q" "p ≠ q" unfolding less_pos_def less_eq_pos_def by blast
show ?r
by (rule exI[of _ r], insert id(2), unfold id[symmetric], auto)
qed
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 Empty
thus ?case by auto
next
case (PCons i p1' q1) note IH = this
show ?case
proof (cases q1)
case Empty
thus ?thesis using IH(2) by auto
next
case (PCons 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 PCons ij by auto
qed
qed
lemma pos_less_eq_append_not_parallel:
assumes "q ≤ p <#> q'"
shows "¬ (q ⊥ p)"
proof-
from assms obtain r where "q <#> r = p <#> q'" unfolding less_eq_pos_def ..
hence dec:"(∃ q3. q = p <#> q3 ∧ q' = q3 <#> r) ∨
(∃ p3. p = q <#> p3 ∧ r = p3 <#> q')" (is "?a ∨ ?b") by (rule pos_append_cases)
hence "p ≤ q ∨ q ≤ p" unfolding less_eq_pos_def by blast
thus ?thesis unfolding parallel_pos by auto
qed
lemma less_pos_power_split: "q < p^m ⟹ ∃ p' k. q = p^k <#> p' ∧ p' < p ∧ k < m"
proof (induct m arbitrary: q)
case 0
thus ?case by auto
next
case (Suc n q)
show ?case
proof (cases "q < 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 ^ n" by simp
from Suc(1)[OF this] obtain p' k where r: "r = p ^ k <#> 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
instantiation pos :: "show"
begin
fun shows_pos :: "pos ⇒ shows"
where
"shows_pos (i <# ε) = shows (Suc i)" |
"shows_pos (i <# ps) = (shows (Suc i) +@+ shows_pos ps)" |
"shows_pos ε = shows_string ''epsilon''"
definition "shows_prec (d::nat) (p::pos) = shows_pos p"
definition "shows_list_pos (ps :: pos list) = showsp_list shows_prec 0 ps"
lemma shows_prec_pos_append [show_law_simps]:
"shows_prec d (p::pos) (r @ s) = shows_prec d p r @ s"
proof (induct p arbitrary: r s)
case (PCons i ps)
then show ?case by (cases ps) (simp_all add: shows_prec_pos_def show_law_simps)
qed (simp add: shows_prec_pos_def show_law_simps)
instance by standard (simp_all add: show_law_simps shows_list_pos_def)
end
fun proper_prefix_list :: "pos ⇒ pos list"
where
"proper_prefix_list ε = []" |
"proper_prefix_list (PCons i p) = ε # map (PCons i) (proper_prefix_list p)"
lemma proper_prefix_list[simp]: "set (proper_prefix_list p) = {q. q < p}"
proof (induction p)
case Empty
show ?case by auto
next
case (PCons 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 Empty
have less: "ε < i <# p" unfolding less_pos_def by auto
show ?thesis unfolding Empty using less by auto
next
case (PCons j q')
show ?thesis unfolding PCons by (auto simp: IH)
qed
qed
qed
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}"
unfolding prefix_list_def by auto
definition bounded_postfixes :: "pos ⇒ pos list ⇒ pos list" where
"bounded_postfixes p ps ≡ map the [opt←map (pos_prefix p) ps . opt ≠ None]"
lemma bounded_postfixes[simp]: "set (bounded_postfixes p ps) = { r. p <#> r ∈ set ps}" (is "?l = ?r")
proof -
note d = bounded_postfixes_def
{
fix r
assume "r ∈ ?l"
from this[unfolded d] obtain q res where q: "q ∈ set ps" and pre: "pos_prefix p q = res" and
res: "res ≠ None" and r: "r = the res" by auto
from res r have res: "res = Some r" by (cases res, auto)
from prefix_sound[OF pre[unfolded res]] q have "r ∈ ?r" by auto
}
moreover
{
fix r
assume "r ∈ ?r"
then obtain q where q: "q ∈ set ps" and p: "p <#> r = q" by auto
hence "p ≤ q" by auto
from prefix_exists[OF this] obtain q' where "p <#> q' = q ∧ pos_prefix p q = Some q'" by auto
with p have "pos_prefix p q = Some r" by auto
with ‹q ∈ set ps› have "r ∈ ?l" unfolding d by force
}
ultimately show ?thesis by blast
qed
definition left_of_pos :: "pos ⇒ pos ⇒ bool"
where "left_of_pos p q == (∃r i j. r #> i ≤ p ∧ r #> j ≤ q ∧ i < j)"
lemma "¬(left_of_pos ε p)" unfolding left_of_pos_def
using Empty_is_append_conv by (metis Empty_least eq_iff pos.distinct(1))
lemma left_of_pos_append: "left_of_pos p q ⟹ left_of_pos (p <#> p') (q <#> q')"
unfolding left_of_pos_def by (metis dual_order.trans less_eq_simps(1))
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"
thus "left_of_pos (p' <#> p) (p' <#> q)" unfolding left_of_pos_def by (metis less_eq_simps(2) semigroup_append.add_assoc)
next
assume "left_of_pos (p' <#> p) (p' <#> q)"
thus "left_of_pos p q"
proof(induct p' arbitrary: p q rule:rev_induct,simp)
case (snoc a p')
hence 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 Position.append_assoc append_PCons monoid_append.add.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
hence "r > ε" unfolding less_pos_def'
by (metis append_Empty append_PCons not_less_iff_gr_or_eq pos.inject)
with x obtain rr where "r = a <# rr" using pos.exhaust[of r]
by (metis less_eq_simps(1) less_eq_simps(4) less_simps(1) monoid_append.add.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
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 ∧ r #> j ≤ q ∧ i < j"
then obtain r i j where rp:"r #> i ≤ p" and rq:"r #> j ≤ 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 ≤ q" by force
from rp rq ij have "¬ q ≤ 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 < q ∨ left_of_pos p0 q"
proof-
assume "left_of_pos (p0 <#> p1) q"
then obtain r i j where rp:"r #> i ≤ (p0 <#> p1)" and rq:"r #> j ≤ q" and ij:"i < j"
unfolding left_of_pos_def by auto
show ?thesis proof(cases "p0 ≤ r")
case True
with rq have "p0 < q" by (metis dual_order.strict_trans1 le_less_trans less_simps(1) not_PCons_self)
thus ?thesis by auto
next
case False
hence 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 ≤ r)" unfolding less_eq_pos_def by auto
from rp have "¬ (p0 ⊥ r)" by (metis less_eq_simps(1) order.trans parallel_pos_sym pos_less_eq_append_not_parallel)
with a have "p0 > r" using position_cases by auto
then obtain oo where p0:"p0 = r <#> oo" and "oo > ε" unfolding less_pos_def less_eq_pos_def by auto
have "¬ (r #> i > p0)" unfolding less_pos_def less_eq_pos_def
by (metis ‹p0 = r <#> oo› a less_eq_simps(1) less_eq_simps(2) less_eq_simps(3) less_eq_simps(4) less_eq_simps(5) pos.exhaust)
with par have "p0 ≥ r #> i" using position_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
thus ?thesis by auto
qed
qed
lemma append_left_of_cases: assumes left:"left_of_pos q (p0 <#> p1)" shows "p0 < q ∨ left_of_pos q p0"
proof-
from left obtain r i j where rp:"r #> i ≤ q" and rq:"r #> j ≤ (p0 <#> p1)" and ij:"i < j"
unfolding left_of_pos_def by auto
show ?thesis proof(cases "p0 ≤ r")
case True
with rp have "p0 < q" unfolding less_pos_def using not_snoc_self2 by (metis eq_iff less_eq_simps(1) order.trans)
thus ?thesis by auto
next
case False
hence 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 ≤ r)" unfolding less_eq_pos_def by auto
from rq have "¬ (p0 ⊥ r)" by (metis less_eq_simps(1) order.trans parallel_pos_sym pos_less_eq_append_not_parallel)
with a have "p0 > r" using position_cases by auto
then obtain oo where p0:"p0 = r <#> oo" and "oo > ε" unfolding less_pos_def less_eq_pos_def by auto
have "¬ (r #> j > p0)" unfolding less_pos_def less_eq_pos_def using p0 a pos.exhaust[of p0]
by (metis less_eq_simps(1) less_eq_simps(2) less_eq_simps(3) less_eq_simps(4) less_eq_simps(5) pos.exhaust)
with par have "p0 ≥ r #> j" using position_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
thus ?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_pos_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
hence "r <#> <i> ≤ p ∧ r <#> <j> ≤ q" by simp
thus ?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" and ij:"i < j" and "r #> j ≤ 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" and ij':"i' < j'" and "r' #> i' ≤ 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 pos.inject)
have nlt:"¬ r < r'" proof
assume "r < 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_simps(2) by auto
from q have q':"j <# q0 = r2 <#> i' <# q0'" unfolding r1 append_assoc using less_eq_simps(2) by auto
from r2 obtain k rr where r2:"r2 = k<# rr" by (cases r2, auto)
from p' q' ij pos.inject show False unfolding r2 by simp
qed
have "¬ r' < r" proof
assume "r' < 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_simps(2) by auto
from q have q':"r2 <#> j <# q0 = i' <# q0'" unfolding r1 append_assoc using less_eq_simps(2) by auto
from r2 obtain k rr where r2:"r2 = k<# rr" by (cases r2, auto)
from p' q' ij' pos.inject show False unfolding r2 by simp
qed
with nlt ne position_cases[of r r', unfolded order_le_less[of r r']] have "r ⊥ r'" by fast
with p q show False by (metis less_eq_simps(1) pos_less_eq_append_not_parallel)
qed
primrec is_left_of :: "pos ⇒ pos ⇒ bool"
where left_Empty: "is_left_of ε q = False"
| left_PCons: "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"
thus "left_of_pos p q"
proof(induct p arbitrary:q)
case Empty
with left_Empty show ?case by auto
next
case (PCons i p) note IH = this
assume l:"is_left_of (i <# p) q"
show ?case proof(cases q)
case Empty
with l show ?thesis unfolding left_PCons by auto
next
case (PCons j q')
show ?thesis proof(cases "¬ (i < j)", cases "j < i")
case True
with l PCons show ?thesis unfolding left_PCons by auto
next
assume "¬ j < i" and "¬ i < j"
hence ij:"i = j" by auto
with PCons l have "is_left_of p q'" unfolding left_PCons by auto
with IH have "left_of_pos p q'" by blast
with ij show "left_of_pos (i <# p) q" unfolding PCons left_of_pos_def
by (metis append_PCons less_eq_simps(4))
next
assume ij:"¬ ¬ (i < j)"
hence "ε #> i ≤ (i <# p) ∧ ε #> j ≤ (j <# q')" unfolding less_eq_pos_def by auto
with PCons 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" and "r #> j ≤ 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
thus "is_left_of p q" proof(induct r arbitrary: p q p' q')
case Empty
assume p:"p = (ε #> i) <#> p'" and q:"q = (ε #> j) <#> q'"
with l[unfolded p q append_Empty] show ?case using left_PCons ij by force
next
case (PCons 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
thus "is_left_of p q" unfolding p q using left_PCons by force
qed
qed
abbreviation right_of_pos :: "pos ⇒ pos ⇒ bool"
where
"right_of_pos p q ≡ left_of_pos q p"
primrec to_list :: "pos ⇒ nat list"
where
"to_list ε = []" |
"to_list (i <# p) = i # (to_list p)"
lemma pos_prefix_same [simp]:
"pos_prefix p p = Some ε"
by (induct p) simp_all
definition "pos_diff p q = the (pos_prefix q p)"
lemma prefix_pos_diff [simp]:
assumes "p ≤ q"
shows "p <#> pos_diff q p = q"
using prefix_exists [OF assms] by (auto simp: pos_diff_def)
lemma pos_diff_Empty2 [simp]:
"pos_diff p ε = p"
by (auto simp: pos_diff_def)
lemma inj_nat_to_pos: "inj (rec_nat ε PCons)" (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
thus ?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 ε PCons)"]
range_inj_infinite[OF inj_nat_to_pos]
show False by blast
qed
end