Theory Definedness

section ‹Definedness›

theory Definedness
  imports
    Data_List
begin

text ‹
  This is an attempt for a setup for better handling bottom, by a better
  simp setup, and less breaking the abstractions.
›

definition defined :: "'a :: pcpo ⇒ bool" where
  "defined x = (x ≠ ⊥)"

lemma defined_bottom [simp]: "¬ defined ⊥"
  by (simp add: defined_def)

lemma defined_seq [simp]: "defined x ⟹ seq⋅x⋅y = y"
  by (simp add: defined_def)

consts val :: "'a::type ⇒ 'b::type" (‹⟦_⟧›)

text ‹val for booleans›

definition val_Bool :: "tr ⇒ bool" where
  "val_Bool i = (THE j. i = Def j)"

adhoc_overloading
  val val_Bool

lemma defined_Bool_simps [simp]:
  "defined (Def i)"
  "defined TT"
  "defined FF"
  by (simp_all add: defined_def)

lemma val_Bool_simp1 [simp]:
  "⟦Def i⟧ = i"
  by (simp_all add: val_Bool_def TT_def FF_def)

lemma val_Bool_simp2 [simp]:
  "⟦TT⟧ = True"
  "⟦FF⟧ = False"
  by (simp_all add: TT_def FF_def)

lemma IF_simps [simp]:
  "defined b ⟹ ⟦ b ⟧ ⟹ (If b then x else y) = x"
  "defined b ⟹ ⟦ b ⟧ = False ⟹ (If b then x else y) = y"
  by (cases b, simp_all)+

lemma defined_neg [simp]: "defined (neg⋅b) ⟷ defined b"
  by (cases b, auto)

lemma val_Bool_neg [simp]: "defined b ⟹ ⟦ neg ⋅ b ⟧ = (¬ ⟦ b ⟧)"
  by (cases b, auto)

text ‹val for integers›

definition val_Integer :: "Integer ⇒ int" where
  "val_Integer i = (THE j. i = MkI⋅j)"

adhoc_overloading
  val val_Integer

lemma defined_Integer_simps [simp]:
  "defined (MkI⋅i)"
  "defined (0::Integer)"
  "defined (1::Integer)"
  by (simp_all add: defined_def)

lemma defined_numeral [simp]: "defined (numeral x :: Integer)"
  by (simp add: defined_def)

lemma val_Integer_simps [simp]:
  "⟦MkI⋅i⟧ = i"
  "⟦0⟧ = 0"
  "⟦1⟧ = 1"
  by (simp_all add: val_Integer_def)

lemma val_Integer_numeral [simp]: "⟦ numeral x :: Integer ⟧ = numeral x"
  by (simp_all add: val_Integer_def)


lemma val_Integer_to_MkI:
  "defined i ⟹ i = (MkI ⋅ ⟦ i ⟧)"
  apply (cases i)
   apply (auto simp add: val_Integer_def defined_def)
  done

lemma defined_Integer_minus [simp]: "defined i ⟹ defined j ⟹ defined (i - (j::Integer))"
  apply (cases i, auto)
  apply (cases j, auto)
  done

lemma val_Integer_minus [simp]: "defined i ⟹ defined j ⟹ ⟦ i - j ⟧ = ⟦ i ⟧ - ⟦ j ⟧"
  apply (cases i, auto)
  apply (cases j, auto)
  done

lemma defined_Integer_plus [simp]: "defined i ⟹ defined j ⟹ defined (i + (j::Integer))"
  apply (cases i, auto)
  apply (cases j, auto)
  done

lemma val_Integer_plus [simp]: "defined i ⟹ defined j ⟹ ⟦ i + j ⟧ = ⟦ i ⟧ + ⟦ j ⟧"
  apply (cases i, auto)
  apply (cases j, auto)
  done

lemma defined_Integer_eq [simp]: "defined (eq⋅a⋅b) ⟷ defined a ∧ defined (b::Integer)"
  apply (cases a, simp)
  apply (cases b, simp)
  apply simp
  done

lemma val_Integer_eq [simp]: "defined a ⟹ defined b ⟹ ⟦ eq⋅a⋅b ⟧ = (⟦ a ⟧ = (⟦ b ⟧ :: int))"
  apply (cases a, simp)
  apply (cases b, simp)
  apply simp
  done


text ‹Full induction for non-negative integers›

lemma nonneg_full_Int_induct [consumes 1, case_names neg Suc]:
  assumes defined: "defined i"
  assumes neg: "⋀ i. defined i ⟹ ⟦i⟧ < 0 ⟹ P i"
  assumes step: "⋀ i. defined i ⟹ 0 ≤ ⟦i⟧ ⟹ (⋀ j. defined j ⟹ ⟦ j ⟧ < ⟦ i ⟧ ⟹ P j) ⟹ P i"
  shows "P (i::Integer)"
proof (cases i)
  case bottom
  then have False using defined by simp
  then show ?thesis ..
next
  case (MkI integer)
  show ?thesis
  proof (cases integer)
    case neg
    then show ?thesis using assms(2) MkI by simp
  next
    case (nonneg nat)
    have "P (MkI⋅(int nat))"
    proof(induction nat rule:full_nat_induct)
      case (1 nat)
      have "defined (MkI⋅(int nat))" by simp
      moreover
      have "0 ≤ ⟦ MkI⋅(int nat) ⟧"  by simp
      moreover
      have "P j" if "defined j" and le: "⟦ j ⟧ < ⟦ MkI⋅(int nat) ⟧" for j::Integer
      proof(cases j)
        case bottom with ‹defined j› show ?thesis by simp
      next
        case (MkI integer)
        show ?thesis
        proof(cases integer)
          case (neg nat)
          have "⟦j⟧ < 0" using neg MkI by simp
          with ‹defined j›
          show ?thesis by (rule assms(2))
        next
          case (nonneg m)
          have "Suc m ≤ nat" using le nonneg MkI by simp
          then have "P (MkI⋅(int m))" by (metis "1.IH")
          then show ?thesis using nonneg MkI by simp
        qed
      qed
      ultimately
      show ?case
        by (rule step)
    qed
    then show ?thesis using nonneg MkI by simp
  qed
qed

text ‹Some list lemmas re-done with the new setup.›

lemma nth_tail: (* TODO: move *)
  "defined n ⟹ ⟦ n ⟧ ≥ 0  ⟹ tail⋅xs !! n = xs !! (1 + n)"
  apply (cases xs, simp_all)
  apply (cases n, simp)
  apply (simp add: one_Integer_def zero_Integer_def)
  done

lemma nth_zipWith: (* TODO: move *)
  assumes f1 [simp]: "⋀y. f⋅⊥⋅y = ⊥"
  assumes f2 [simp]: "⋀x. f⋅x⋅⊥ = ⊥"
  shows "zipWith⋅f⋅xs⋅ys !! n = f⋅(xs !! n)⋅(ys !! n)"
proof (induct xs arbitrary: ys n)
  case (Cons x xs ys n) then show ?case
    by (cases ys, simp_all split:nth_Cons_split)
qed simp_all


lemma nth_neg [simp]: "defined n ⟹ ⟦ n ⟧ < 0 ⟹ nth⋅xs⋅n = ⊥"
proof (induction xs arbitrary: n)
  have [simp]: "eq⋅n⋅0 = TT ⟷ (n::Integer) = 0" for n
    by (cases n, auto simp add: zero_Integer_def)
  case (Cons a xs n)
  have "eq⋅n⋅0 = FF"
    using Cons.prems
    by (cases "eq⋅n⋅0") auto
  then show ?case
    using Cons.prems
    by (auto intro: Cons.IH)
qed simp_all

lemma nth_Cons_simp [simp]:
  "defined n ⟹ ⟦ n ⟧ = 0 ⟹ nth⋅(x : xs)⋅n = x"
  "defined n ⟹ ⟦ n ⟧ > 0 ⟹ nth⋅(x : xs)⋅n = nth⋅xs⋅(n - 1)"
proof -
  assume "defined n" and "⟦ n ⟧ = 0"
  then have "n = 0"  by (cases n) auto
  then show "nth⋅(x : xs)⋅n = x" by simp
next
  assume "defined n" and "⟦ n ⟧ > 0"
  then have "eq⋅n⋅0 = FF" by (cases "eq⋅n⋅0") auto
  then show "nth⋅(x : xs)⋅n = nth⋅xs⋅(n - 1)" by simp
qed

end