Theory Value

theory "Value"
  imports HOLCF
begin

subsubsection ‹The semantic domain for values and environments›

domain Value = Fn (lazy "Value → Value") | B (lazy "bool discr")

fixrec Fn_project :: "Value → Value → Value"
 where "Fn_project⋅(Fn⋅f) = f"

abbreviation Fn_project_abbr (infix "↓Fn" 55)
  where "f ↓Fn v ≡ Fn_project⋅f⋅v"

lemma [simp]:
  "⊥ ↓Fn x = ⊥"
  "(B⋅b) ↓Fn x = ⊥"
  by (fixrec_simp)+

fixrec B_project :: "Value → Value → Value → Value" where
  "B_project⋅(B⋅db)⋅v⇩1⋅v⇩2 = (if undiscr db then v⇩1 else v⇩2)"

lemma [simp]:
  "B_project⋅(B⋅(Discr b))⋅v⇩1⋅v⇩2 = (if b then v⇩1 else v⇩2)"
  "B_project⋅⊥⋅v⇩1⋅v⇩2 = ⊥"
  "B_project⋅(Fn⋅f)⋅v⇩1⋅v⇩2 = ⊥"
by fixrec_simp+

text ‹
A chain in the domain @{typ Value} is either always bottom, or eventually @{term "Fn"} of another
chain
›

lemma Value_chainE[consumes 1, case_names bot B Fn]:
  assumes "chain Y"
  obtains "Y = (λ _ . ⊥)" |
          n b where "Y = (λ m. (if m < n then ⊥ else B⋅b))" |
          n Y' where "Y = (λ m. (if m < n then ⊥ else Fn⋅(Y' (m-n))))" "chain Y'"
proof(cases "Y = (λ _ . ⊥)")
  case True
  thus ?thesis by (rule that(1))
next
  case False
  hence "∃ i. Y i ≠ ⊥" by auto
  hence "∃ n. Y n ≠ ⊥ ∧ (∀m. Y m ≠ ⊥ ⟶ m ≥ n)"
    by (rule exE)(rule ex_has_least_nat)
  then obtain n where "Y n ≠ ⊥" and "∀m. m < n ⟶ Y m = ⊥" by fastforce
  hence "(∃ f. Y n = Fn⋅f) ∨ (∃ b. Y n = B⋅b)" by (metis Value.exhaust)
  thus ?thesis
  proof
    assume "(∃ f. Y n = Fn⋅f)"
    then obtain f where "Y n = Fn ⋅ f" by blast
    {
      fix i
      from ‹chain Y› have "Y n ⊑ Y (i+n)" by (metis chain_mono le_add2)
      with ‹Y n = _›
      have "∃ g. (Y (i+n) = Fn ⋅ g)"
        by (metis Value.dist_les(1) Value.exhaust below_bottom_iff)
    }
    then obtain Y' where Y': "⋀ i. Y (i + n) = Fn ⋅ (Y' i)" by metis

    have "Y = (λm. if m < n then ⊥ else Fn⋅(Y' (m - n)))"
        using ‹∀m. _› Y' by (metis add_diff_inverse add.commute)
    moreover
    have"chain Y'" using ‹chain Y›
      by (auto intro!:chainI elim: chainE  simp add: Value.inverts[symmetric] Y'[symmetric] simp del: Value.inverts)
    ultimately
    show ?thesis by (rule that(3))
  next
    assume "(∃ b. Y n = B⋅b)"
    then obtain b where "Y n = B⋅b" by blast
    {
      fix i
      from ‹chain Y› have "Y n ⊑ Y (i+n)" by (metis chain_mono le_add2)
      with ‹Y n = _›
      have "Y (i+n) = B⋅b"
        by (metis Value.dist_les(2) Value.exhaust Value.inverts(2) below_bottom_iff discrete_cpo)
    }
    hence  Y': "⋀ i. Y (i + n) = B⋅b" by metis

    have "Y = (λm. if m < n then ⊥ else B⋅b)"
        using ‹∀m. _› Y' by (metis add_diff_inverse add.commute)
    thus ?thesis by (rule that(2))
  qed
qed


end