Theory Refine_String

theory Refine_String
imports
  Autoref_Misc
begin

subsection ‹Setup for characters›
context includes autoref_syntax begin
lemma [autoref_itype]: "Char b0 b1 b2 b3 b4 b5 b6 b7 ::⇩i I"
  and [autoref_op_pat_def]: "Char b0 b1 b2 b3 b4 b5 b6 b7 ≡ OP (Char b0 b1 b2 b3 b4 b5 b6 b7) :::⇩i I"
  and [autoref_rules]: "(Char b0 b1 b2 b3 b4 b5 b6 b7, OP (Char b0 b1 b2 b3 b4 b5 b6 b7) ::: Id) ∈ Id"
  by simp_all
end

subsection ‹setup for strings›

consts i_string :: interface
consts i_char :: interface

abbreviation "char_rel ≡ Id::(char×_) set"
definition "string_rel ≡ ⟨char_rel⟩list_rel::(string×_) set"
lemmas [autoref_rel_intf] = REL_INTFI[of string_rel i_string]
lemmas [autoref_rel_intf] = REL_INTFI[of char_rel i_char]

definition op_str_Nil::"string" where [simp]: "op_str_Nil = Nil"
definition op_str_Cons::"char ⇒ string ⇒ string" where [simp]: "op_str_Cons = Cons"
definition op_str_append::"string ⇒ string ⇒ string" where [simp]: "op_str_append = (@)"

context includes autoref_syntax begin
lemma
  shows [autoref_itype]:
    "op_str_Nil ::⇩i i_string"
    "op_str_Cons ::⇩i i_char →⇩i i_string →⇩i i_string"
    "op_str_append ::⇩i i_string →⇩i i_string →⇩i i_string"
  and [autoref_rules]:
    "(Nil, op_str_Nil::string) ∈ string_rel"
    "(Cons, op_str_Cons) ∈ char_rel → string_rel → string_rel"
    "((@), op_str_append) ∈ string_rel → string_rel → string_rel"
  and [autoref_op_pat_def]:
    "Nil ≡ op_str_Nil"
    "Cons ≡ op_str_Cons"
    "(@) ≡ op_str_append"
  by (simp_all add: string_rel_def)
end

subsection ‹Setup for literals›
context includes autoref_syntax begin
lemma [autoref_itype]: "String.empty_literal ::⇩i I"
  and [autoref_op_pat_def]: "String.empty_literal ≡ OP String.empty_literal :::⇩i I"
  and [autoref_rules]: "(String.empty_literal, OP String.empty_literal ::: Id) ∈ Id"
  by simp_all

lemma [autoref_itype]: "String.Literal b0 b1 b2 b3 b4 b5 b6 s ::⇩i I"
  and [autoref_op_pat_def]: "String.Literal b0 b1 b2 b3 b4 b5 b6 s ≡
    OP (String.Literal b0 b1 b2 b3 b4 b5 b6 s) :::⇩i I"
  and [autoref_rules]: "(String.Literal b0 b1 b2 b3 b4 b5 b6 s,
    OP (String.Literal b0 b1 b2 b3 b4 b5 b6 s) ::: Id) ∈ Id"
  by simp_all

definition [simp]: "ST (x::char list) = x"
lemma [autoref_op_pat_def]: "ST xs ≡ OP (ST xs)" by simp
lemma [autoref_rules]: "(x, ST x) ∈ string_rel"
  by (auto simp: string_rel_def)

end

text ‹A little check›

schematic_goal "(?c::?'c, RETURN (STR '''', STR ''Hello''))∈?R"
  by autoref

end