Theory LocalLexingLemmas

theory LocalLexingLemmas
imports LocalLexing Limit
begin

context LocalLexing begin

lemma[simp]: "setmonotone (Append Z k)" by (auto simp add: Append_def setmonotone_def)

lemma subset_𝒫Suc: "𝒫 k u ⊆ 𝒫 k (Suc u)"
  by (simp add: subset_setmonotone[OF setmonotone_limit])

lemma subset_fSuc_strict:
  assumes f: "⋀ u. f u ⊆ f (Suc u)"
  shows "u < v ⟹ f u ⊆ f v"
proof (induct v)
  show "u < 0 ⟹ f u ⊆ f 0"
    by auto
next
  fix v
  assume a:"(u < v ⟹ f u ⊆ f v)"
  assume b:"u < Suc v"
  from b have c: "f u ⊆ f v"
    apply (case_tac "u < v")
    apply (simp add: a)
    apply (case_tac "u = v")
    apply simp
    by auto
  show "f u ⊆ f (Suc v)"
    apply (rule subset_trans[OF c])
    by (rule f)
qed

lemma subset_fSuc:
  assumes f: "⋀ u. f u ⊆ f (Suc u)"
  shows "u ≤ v ⟹ f u ⊆ f v"
  apply (case_tac "u < v")
  apply (rule subset_fSuc_strict[where f=f, OF f])
  by auto

lemma subset_𝒫k: "u ≤ v ⟹ 𝒫 k u ⊆ 𝒫 k v"
  by (rule subset_fSuc, rule subset_𝒫Suc) 
  
lemma subset_𝒫𝒬k: "𝒫 k u ⊆ 𝒬 k" by (auto simp add: natUnion_def)

lemma subset_𝒬𝒫Suc: "𝒬 k ⊆ 𝒫 (Suc k) u" 
proof -
  have a: "𝒬 k ⊆ 𝒫 (Suc k) 0" by simp
  show ?thesis 
    apply (case_tac "u = 0")
    apply (simp add: a)
    apply (rule subset_trans[OF a subset_𝒫k])
    by auto
qed

lemma subset_𝒬Suc: "𝒬 k ⊆ 𝒬 (Suc k)"
  by (rule subset_trans[OF subset_𝒬𝒫Suc subset_𝒫𝒬k])

lemma subset_𝒬: "i ≤ j ⟹ 𝒬 i ⊆ 𝒬 j"
  by (rule subset_fSuc[where u=i and v=j and f = 𝒬, OF subset_𝒬Suc])

lemma empty_𝒳[simp]: "k > length Doc ⟹ 𝒳 k = {}"
  apply (simp add: 𝒳_def)
  apply (insert Lex_is_lexer)
  by (simp add: is_lexer_def)

lemma Sel_empty[simp]: "Sel {} {} = {}"
  apply (insert Sel_is_selector)
  by (auto simp add: is_selector_def)

lemma empty_𝒵[simp]: "k > length Doc ⟹ 𝒵 k u = {}"
  apply (induct u)
  by (simp_all add: 𝒴_def 𝒲_def)

lemma[simp]: "Append {} k = id" by (auto simp add: Append_def)

lemma[simp]: "k > length Doc ⟹ 𝒫 k v = 𝒫 k 0"
  by (induct v, simp_all add: 𝒴_def 𝒲_def)

lemma 𝒬SucEq: "k ≥ length Doc ⟹ 𝒬 (Suc k) = 𝒬 k"
  by (simp add: natUnion_def) 

lemma 𝒬_converges:
  assumes k: "k ≥ length Doc"
  shows "𝒬 k = 𝔓"
proof -
  { 
    fix n
    have "𝒬 (length Doc + n) = 𝔓"
    proof (induct n)
      show "𝒬 (length Doc + 0) = 𝔓" by (simp add: 𝔓_def)
    next
      fix n
      assume hyp: "𝒬 (length Doc + n) = 𝔓"
      have "𝒬 (Suc (length Doc + n)) = 𝔓"
        by (rule trans[OF 𝒬SucEq hyp], auto)
      then show "𝒬 (length Doc + Suc n) = 𝔓"
        by auto
    qed
  }
  note helper = this
  from k have "∃ n. k = length Doc + n" by presburger
  then obtain "n" where n: "k = length Doc + n" by blast
  then show ?thesis
    apply (simp only: n)
    by (rule helper)
qed

lemma 𝔓_covers_𝒬: "𝒬 k ⊆ 𝔓"
proof (case_tac "k ≥ length Doc")
  assume "k ≥ length Doc"
  then have 𝒬: "𝒬 k = 𝔓" by (rule 𝒬_converges)
  then show "𝒬 k ⊆ 𝔓" by (simp only: 𝒬)
next
  assume "¬ length Doc ≤ k"
  then have "k < length Doc" by auto
  then show ?thesis
    apply (simp only: 𝔓_def)
    apply (rule subset_𝒬)
    by auto
qed

lemma Sel_upper_bound: "A ⊆ B ⟹ Sel A B ⊆ B"
  by (metis Sel_is_selector is_selector_def)

lemma Sel_lower_bound: "A ⊆ B ⟹ A ⊆ Sel A B"
  by (metis Sel_is_selector is_selector_def)  

lemma 𝔓_covers_𝒫: "𝒫 k u ⊆ 𝔓"
  by (rule subset_trans[OF subset_𝒫𝒬k 𝔓_covers_𝒬])

lemma 𝒲_montone: "P ⊆ Q ⟹ 𝒲 P k ⊆ 𝒲 Q k"
  by (auto simp add: 𝒲_def)

lemma Sel_precondition: 
  "𝒵 k u ⊆ 𝒲 (𝒫 k u) k"
proof (induct u)
  case 0 thus ?case by simp
next
  case (Suc u)
  have 1: "𝒴 (𝒵 k u) (𝒫 k u) k ⊆ 𝒲 (𝒫 k u) k"
    apply (simp add: 𝒴_def)
    apply (rule_tac Sel_upper_bound)
    using Suc by simp
  have 2: "𝒲 (𝒫 k u) k ⊆ 𝒲 (𝒫 k (Suc u)) k"
    by (metis 𝒲_montone subset_𝒫Suc)    
  show ?case
    apply (rule_tac subset_trans[where B="𝒲 (𝒫 k u) k"])
    apply (simp add: 1)
    apply (simp only: 2)
    done
qed    

lemma 𝒲_bounded_by_𝒳: "𝒲 P k ⊆ 𝒳 k"
  by (metis (no_types, lifting) 𝒲_def mem_Collect_eq subsetI)

lemma 𝒵_subset_𝒳: "𝒵 k n ⊆ 𝒳 k"
  by (metis Sel_precondition 𝒲_bounded_by_𝒳 rev_subsetD subsetI)

lemma 𝒵_subset_Suc: "𝒵 k n ⊆ 𝒵 k (Suc n)"
apply (induct n)
apply simp
by (metis Sel_lower_bound Sel_precondition 𝒴_def 𝒵.simps(2))

lemma 𝒴_upper_bound: "𝒴 (𝒵 k u) (𝒫 k u) k ⊆ 𝒲  (𝒫 k u) k"
  apply (simp add: 𝒴_def)
  by (metis Sel_precondition Sel_upper_bound)

lemma 𝔓_induct[consumes 1, case_names Base Induct]:
  assumes p: "p ∈ 𝔓"
  assumes base: "P []"
  assumes induct: "⋀ p k u. (⋀ q. q ∈ 𝒫 k u ⟹ P q) ⟹ p ∈ 𝒫 k (Suc u) ⟹ P p"
  shows "P p"
proof -
  {
    fix p :: "tokens"
    fix k :: nat
    fix u :: nat
    have "p ∈ 𝒫 k u ⟹ P p"
    proof (induct k arbitrary: p u)
      case 0
        have "p ∈ 𝒫 0 u ⟹ P p"
        proof (induct u arbitrary: p)
          case 0 thus ?case using base by simp
        next
          case (Suc u) show ?case
            apply (rule induct[OF _ Suc(2)])
            apply (rule Suc(1))
            by simp
        qed
        with 0 show ?case by simp
    next
      case (Suc k)
        have "p ∈ 𝒫 (Suc k) u ⟹ P p"
        proof (induct u arbitrary: p)
          case 0 thus ?case
            apply simp
            apply (induct rule: natUnion_decompose) 
            using Suc by simp
        next
          case (Suc u) show ?case
            apply (rule induct[OF _ Suc(2)])
            apply (rule Suc(1))
            by simp
        qed
        with Suc show ?case by simp
    qed 
  }
  note all = this
  from p show ?thesis
    apply (simp add: 𝔓_def)
    apply (induct rule: natUnion_decompose)
    using all by simp
qed 
    
lemma Append_mono: "U ⊆ V ⟹ P ⊆ Q ⟹ Append U k P ⊆ Append V k Q"
  by (auto simp add: Append_def)

lemma pointwise_Append: "pointwise (Append T k)"
by (auto simp add: pointwise_def Append_def)

lemma regular_Append: "regular (Append T k)"
proof -
  have "pointwise (Append T k)" using pointwise_Append by blast
  then have "pointbased (Append T k)" using pointwise_implies_pointbased by blast
  then have "continuous (Append T k)" using pointbased_implies_continuous by blast 
  moreover have "setmonotone (Append T k)" by (simp add: setmonotone_def Append_def)
  ultimately show ?thesis using regular_def by blast
qed

end

end