Theory Higher_Order_Terms.Name

chapter ‹Names as a unique datatype›

theory Name
imports Main
begin

text ‹
  I would like to model names as @{typ string}s. Unfortunately, there is no default order on lists,
  as there could be multiple reasonable implementations: e.g.\ lexicographic and point-wise.
  For both choices, users can import the corresponding instantiation.

  In Isabelle, only at most one implementation of a given type class for a given type may be present
  in the same theory. Consequently, I avoided importing a list ordering from the library, because it
  may cause conflicts with users who use another ordering. The general approach for these situations
  is to introduce a type copy.

  The full flexibility of strings (i.e.\ string manipulations) is only required where fresh names
  are being produced. Otherwise, only a linear order on terms is needed. Conveniently, Sternagel and
  Thiemann \<^cite>‹sternagel2015deriving› provide tooling to automatically generate such a
  lexicographic order.
›

datatype name = Name (as_string: string)

― ‹Mostly copied from ‹List_Lexorder››

instantiation name :: ord
begin

definition less_name where
"xs < ys ⟷ (as_string xs, as_string ys) ∈ lexord {(u, v). (of_char u :: nat) < of_char v}"

definition less_eq_name where
"(xs :: name) ≤ ys ⟷ xs < ys ∨ xs = ys"

instance ..

end

instance name :: order
proof
  fix xs :: "name"
  show "xs ≤ xs" by (simp add: less_eq_name_def)
next
  fix xs ys zs :: "name"
  assume "xs ≤ ys" and "ys ≤ zs"
  then show "xs ≤ zs"
    apply (auto simp add: less_eq_name_def less_name_def)
    apply (rule lexord_trans)
    apply (auto intro: transI)
    done
next
  fix xs ys :: "name"
  assume "xs ≤ ys" and "ys ≤ xs"
  then show "xs = ys"
    apply (auto simp add: less_eq_name_def less_name_def)
    apply (rule lexord_irreflexive [THEN notE])
    defer
    apply (rule lexord_trans)
    apply (auto intro: transI)
    done
next
  fix xs ys :: "name"
  show "xs < ys ⟷ xs ≤ ys ∧ ¬ ys ≤ xs"
    apply (auto simp add: less_name_def less_eq_name_def)
    defer
    apply (rule lexord_irreflexive [THEN notE])
    apply auto
    apply (rule lexord_irreflexive [THEN notE])
    defer
    apply (rule lexord_trans)
    apply (auto intro: transI)
    done
qed

instance name :: linorder
proof
  fix xs ys :: "name"
  have "(as_string xs, as_string ys) ∈ lexord {(u, v). (of_char u::nat) < of_char v} ∨ xs = ys ∨ (as_string ys, as_string xs) ∈ lexord {(u, v). (of_char u::nat) < of_char v}"
    by (metis (no_types, lifting) case_prodI lexord_linear linorder_neqE_nat mem_Collect_eq name.expand of_char_eq_iff)
  then show "xs ≤ ys ∨ ys ≤ xs"
    by (auto simp add: less_eq_name_def less_name_def)
qed

lemma less_name_code [code]:
  "Name xs < Name [] ⟷ False"
  "Name [] < Name (x # xs) ⟷ True"
  "Name (x # xs) < Name (y # ys) ⟷ (of_char x::nat) < of_char y ∨ x = y ∧ Name xs < Name ys"
  by (simp_all add: less_name_def)

lemma le_name_code [code]:
  "Name (x # xs) ≤ Name [] ⟷ False"
  "Name [] ≤ Name (x # xs) ⟷ True"
  "Name (x # xs) ≤ Name (y # ys) ⟷ (of_char x::nat) < of_char y ∨ x = y ∧ Name xs ≤ Name ys"
  by (auto simp add: less_eq_name_def less_name_def)

context begin

qualified definition append :: "name ⇒ name ⇒ name" where
"append v1 v2 = Name (as_string v1 @ as_string v2)"

lemma name_append_less:
  assumes "xs ≠ Name []"
  shows "append ys xs > ys"
proof -
  have "Name (ys @ xs) > Name ys" if "xs ≠ []" for xs ys
    using that
    proof (induction ys)
      case Nil
      thus ?case
        unfolding less_name_def
        by (cases xs) auto
    next
      case (Cons y ys)
      thus ?case
        unfolding less_name_def
        by auto
    qed
  with assms show ?thesis
    unfolding append_def
    by (cases xs, cases ys) auto
qed

end

end