Theory Psi

subsection ‹Definition of \texorpdfstring{$\Psi$}{Psi}\label{sec:psi}›

theory Psi
  imports SortKeys "HOL-Eisbach.Eisbach"
begin

fun extended_size :: "('ℐ sort_key) extended ⇒ nat"
  where
    "extended_size ⟦x⟧ = size x" |
    "extended_size _ = 0"

lemma extended_simps [simp]:
  "(⊢ < x) = (x ≠ ⊢)"
  "(⟦x'⟧ < ⟦y'⟧) = (x' < y')"
  "⟦x'⟧ < ⊣"
  "¬(⟦x'⟧ < ⊢)"
  "¬(⊣ < x)"
  "⊢ ≤ x"
  "(⟦x'⟧ ≤ ⟦y'⟧) = ((x' :: 'ℐ :: linorder) ≤ y')"
  "x ≤ ⊣"
  "¬(⟦x'⟧ ≤ ⊢)"
  "(⊣ ≤ x) = (x = ⊣)"
  by (case_tac [!] x, simp_all add:less_extended_def less_eq_extended_def le_less)

fun int_size where "int_size (l,u) = max (extended_size l) (extended_size u)"

lemma position_cases:
  assumes "⋀ y z. x = ⟦NonFinal (y,Left) z⟧ ⟹ p"
  assumes "⋀ y z. x = ⟦NonFinal (y,Right) z⟧ ⟹ p"
  assumes "⋀ y. x = ⟦Final y⟧ ⟹ p"
  assumes "x = ⊢ ⟹ p"
  assumes "x = ⊣ ⟹ p"
  shows "p"
  by (metis assms embed_dir.cases extended_size.cases sort_key_embedding.cases)

fun derive_pos ::
  "('ℐ :: linorder) × sort_dir ⇒ 'ℐ sort_key extended ⇒ 'ℐ sort_key extended"
  where
    "derive_pos h ⟦NonFinal x y⟧ = 
      (if h < x then ⊣ else (if x < h then ⊢ else ⟦y⟧))" |
    "derive_pos h ⟦Final x⟧ = 
      (if fst h < x ∨ fst h = x ∧ snd h = Left then ⊣ else ⊢)" |
    "derive_pos _ ⊢ = ⊢" |
    "derive_pos _ ⊣ = ⊣"

lemma derive_pos_mono: "x ≤ y ⟹ derive_pos h x ≤ derive_pos h y"
  apply (cases h, cases "snd h")
  apply (rule_tac [!] position_cases [where x=x])
  apply (rule_tac [!] position_cases [where x=y])
  by (simp_all, auto)

fun γ :: "('ℐ :: linorder) position ⇒ sort_dir ⇒ 'ℐ × sort_dir"
  where
    "γ ⟦NonFinal x y⟧ _ = x" |
    "γ ⟦Final x⟧ d = (x,d)" |
    "γ ⊢ _ = undefined" |
    "γ ⊣ _ = undefined"

fun derive_left  where
  "derive_left (l, u) = (derive_pos (γ l Right) l, derive_pos (γ l Right) u)"

fun derive_right where
  "derive_right (l, u) = (derive_pos (γ u Left) l, derive_pos (γ u Left) u)"

fun is_interval where "is_interval (l,u) = (l < u)"

fun elem where "elem x (l,u) = (l < x ∧ x < u)"

fun subset where "subset (l,u) (l',u') = (l' ≤ l ∧ u ≤ u')"

method interval_split for x :: "('ℐ :: linorder) position × 'ℐ position" = 
  (case_tac [!] x, 
   rule_tac [!] position_cases [where x="fst x"], 
   rule_tac [!] position_cases [where x="snd x"])

lemma derive_size:
  "⟦Final i⟧ ≤ fst x ∧ is_interval x ⟹ int_size (derive_left x) < int_size x" 
  "snd x ≤ ⟦Final i⟧ ∧ is_interval x ⟹ int_size (derive_right x) < int_size x"
  by (interval_split x, simp_all add:less_SucI)

lemma derive_interval:
  "⟦Final i⟧ ≤ fst x ⟹ is_interval x ⟹ is_interval (derive_left x)"
  "snd x ≤ ⟦Final i⟧ ⟹ is_interval x ⟹ is_interval (derive_right x)"
  by (interval_split x, simp_all, auto)

function Ψ :: "('ℐ :: linorder) position × 'ℐ position ⇒ 'ℐ ⇒ 'ℐ sort_key"
  where
    "Ψ (l,u) i = Final i"
      if "l < ⟦Final i⟧ ∧ ⟦Final i⟧ < u" |
    "Ψ (l,u) i = NonFinal (γ l Right) (Ψ (derive_left (l,u)) i)" 
      if "⟦Final i⟧ ≤ l ∧ l < u" |
    "Ψ (l,u) i = NonFinal (γ u Left) (Ψ (derive_right (l,u)) i)" 
      if "u ≤ ⟦Final i⟧ ∧ l < u" |
    "Ψ (l,u) i = undefined" if "u ≤ l"
  by (metis leI old.prod.exhaust, auto)

termination
  apply (relation "measure (λ(p,i). int_size p)", simp)
  using derive_size by fastforce+

proposition psi_elem: "is_interval x ⟹ elem ⟦Ψ x i⟧ x"
proof (induct "int_size x" arbitrary:x rule: nat_less_induct)
  case 1
  consider (a) "⟦Final i⟧ ≤ fst x" | (b) "elem ⟦Final i⟧ x" | (c) "snd x ≤ ⟦Final i⟧"
    using not_le by (metis elem.simps prod.collapse)
  then show ?case
  proof (cases)
    case a
    hence "elem  ⟦Ψ (derive_left x) i⟧ (derive_left x)"
      by (metis 1 derive_size(1) derive_interval(1))
    then show ?thesis using a "1"(2)
      by (interval_split x, simp_all del:Ψ.simps, auto)
  next
    case b
    then show ?thesis by (cases x, simp)
  next
    case c 
    hence "elem  ⟦Ψ (derive_right x) i⟧ (derive_right x)"
      by (metis 1 derive_size(2) derive_interval(2))
    then show ?thesis using c "1"(2)
      by (interval_split x, simp_all del:Ψ.simps, auto)
  qed
qed

proposition psi_mono:
  assumes "i1 < i2"
  shows "is_interval x ⟹ Ψ x i1 < Ψ x i2"
proof (induct "int_size x" arbitrary:x rule: nat_less_induct)
  case 1
  have a:"⟦Final i1⟧ < ⟦Final i2⟧"
    using assms by auto
  then consider 
    (a) "⟦Final i1⟧ ≤ fst x ∧ ⟦Final i2⟧ ≤ fst x" | 
    (b) "⟦Final i1⟧ ≤ fst x ∧ elem ⟦Final i2⟧ x" | 
    (c) "⟦Final i1⟧ ≤ fst x ∧ snd x ≤ ⟦Final i2⟧" |
    (d) "elem ⟦Final i1⟧ x  ∧ elem ⟦Final i2⟧ x" |
    (e) "elem ⟦Final i1⟧ x ∧ snd x ≤ ⟦Final i2⟧" |
    (f) "snd x ≤ ⟦Final i2⟧ ∧ snd x ≤ ⟦Final i1⟧" 
    using assms "1"(2) apply (cases x) 
    by (metis (mono_tags, opaque_lifting) dual_order.strict_trans elem.simps
        fst_conv leI snd_conv)
  then show ?case
  proof (cases)
    case a
    hence "Ψ (derive_left x) i1  < Ψ (derive_left x) i2"
      by (metis 1 derive_size(1) derive_interval(1))
    thus ?thesis using a "1"(2) by (cases x, simp)
  next
    case b
    thus ?thesis using "1"(2) apply (cases x, simp) 
      by (rule_tac [!] position_cases [where x="fst x"], simp_all)
  next
    case c
    show ?thesis
    proof (cases "γ (fst x) Right = γ (snd x) Left")
      case True 
      have e:"is_interval (derive_left x)" using c "1"(2) derive_interval(1) by blast
      have f:"derive_left x = derive_right x" using True by (cases x, simp)
      have h:"Ψ (derive_left x) i1 < Ψ (derive_right x) i2"
        apply (cases x, simp only: f) 
        by (metis "1.hyps" "1.prems" c derive_size(2) e f)
      show ?thesis using c "1"(2) h True by (cases x, simp)
    next
      case False
      hence "γ (fst x) Right < γ (snd x) Left" using "1"(2) c
      by (interval_split x, simp_all, auto)
      then show ?thesis using c "1"(2) by (cases x, simp)
    qed
  next
    case d
    thus ?thesis using "1"(2) a by (cases x, simp)
  next
    case e
    thus ?thesis using "1"(2) apply (cases x, simp) 
      by (rule_tac [!] position_cases [where x="snd x"], simp_all del:Ψ.simps)
  next
    case f
    hence b:"Ψ (derive_right x) i1  < Ψ (derive_right x) i2" 
      by (metis 1 derive_size(2) derive_interval(2))
    thus ?thesis using f "1"(2) by (cases x, simp)
  qed
qed

proposition psi_narrow:
  "elem ⟦Ψ x' i⟧ x ⟹ subset x x' ⟹ Ψ x' i = Ψ x i" 
proof (induct "int_size x'" arbitrary: x x' rule: nat_less_induct)
  case 1
  have a: "is_interval x" using "1"(2)
    by (metis dual_order.strict_trans elem.elims(2) is_interval.simps)
  have d: "is_interval x'" using a "1"(3) apply (cases x', cases x, simp) by auto
  consider
    (before) "⟦Final i⟧ ≤ fst x'" |
    (between) "elem ⟦Final i⟧ x'" | 
    (after) "snd x' ≤ ⟦Final i⟧" using 1 apply simp
    by (metis elem.simps leI prod.collapse)
  then show ?case
  proof (cases)
    case before
    have b: "⟦Final i⟧ ≤ fst x" using before 1 apply (cases x)
      by (metis dual_order.trans fst_conv subset.elims(2))
    obtain z where z_def: "Ψ x' i = NonFinal (γ (fst x') Right) z" 
      using before d apply (cases x') by simp
    have c:"γ (fst x') Right = γ (fst x) Right"
      using "1"(3) z_def "1"(2) apply (cases x, cases x', simp)
      apply (rule_tac [!] position_cases [where x="fst x"])
      apply (rule_tac [!] position_cases [where x="fst x'"])
      using before by (simp_all del:Ψ.simps, auto)
    have c1:"subset (derive_left x) (derive_left x')"
      using c "1"(3) by (cases x, cases x', simp add:derive_pos_mono)
    have g:"z = Ψ (derive_left x') i" using z_def before d by (cases x', simp)
    have "elem ⟦NonFinal (γ (fst x) Right) z⟧ x" 
      using "1"(2) z_def by (simp add: c)
    hence "elem ⟦z⟧ (derive_left x)" using before b
      by (interval_split x, simp_all del:Ψ.simps, auto)
    hence "Ψ (derive_left x') i = Ψ (derive_left x) i"
      using "1"(1) before d c1 apply (simp only:g)
      by (metis (no_types) derive_size(1))
    thus ?thesis using before b a d c by (cases x, cases x', simp)
  next
    case between
    thus ?thesis using 1 by (cases x, cases x', auto) 
  next
    case after
    have b: "snd x ≤ ⟦Final i⟧" using after 1 apply (cases x) 
      by (metis (mono_tags, opaque_lifting) dual_order.trans prod.exhaust_sel
          subset.simps)
    obtain z where z_def:"Ψ x' i = NonFinal (γ (snd x') Left) z" 
      using after d by (cases x', simp)
    have c:"γ (snd x') Left = γ (snd x) Left"
      using "1"(3) z_def "1"(2) apply (simp, cases x, cases x')
      apply (rule_tac [!] position_cases [where x="snd x"])
      apply (rule_tac [!] position_cases [where x="snd x'"]) using after
      by (simp_all del:Ψ.simps, auto)
    have c1:"subset (derive_right x) (derive_right x')"
      using c "1"(3) by (cases x, cases x', simp add:derive_pos_mono)
    have g:"z = Ψ (derive_right x') i" using z_def after d by (cases x', simp)
    have "elem ⟦NonFinal (γ (snd x) Left) z⟧ x" 
      using "1"(2) z_def by (simp add: c)
    hence "elem ⟦z⟧ (derive_right x)" using after b
      by (interval_split x, simp_all del:Ψ.simps, auto)
    hence "Ψ (derive_right x') i = Ψ (derive_right x) i"
      using "1"(1) after d c1 apply (simp only:g)   
      by (metis (no_types) derive_size(2))
    thus ?thesis using after b a d c by (cases x, cases x', simp)
  qed
qed

definition preserve_order :: "'a :: linorder ⇒ 'a ⇒ 'b :: linorder ⇒ 'b ⇒ bool"
  where "preserve_order x y u v ≡ (x < y ⟶ u < v) ∧ (x > y ⟶ u > v)"

proposition psi_preserve_order:
  fixes l l' u u' i i'
  assumes "elem ⟦Ψ (l, u) i⟧ (l',u')"
  assumes "elem ⟦Ψ (l', u') i'⟧ (l, u)"
  shows "preserve_order i i' ⟦Ψ (l,u) i⟧ ⟦Ψ (l', u') i'⟧"
proof -
  have "l < u" using assms(2) by auto
  hence a:"elem ⟦Ψ (l, u) i⟧ (max l l', min u u')"
    using assms(1) psi_elem by fastforce
  hence b:"Ψ (l,u) i = Ψ (max l l', min u u') i"
    by (simp add: psi_narrow)
  have "l' < u'" using assms(1) by auto
  hence "elem ⟦Ψ (l',u') i'⟧ (max l l', min u u')"
    using assms(2) psi_elem by fastforce
  hence c:"Ψ (l',u') i' = Ψ (max l l', min u u') i'"
    by (simp add: psi_narrow)
  hence "max l l' < min u u'" using a min_def by auto
  then show ?thesis apply (simp only: preserve_order_def b c)
    using psi_mono extended_simps(2) is_interval.simps by blast
qed

end