Theory HelloWorld_Proof

theory HelloWorld_Proof
  imports HelloWorld
begin

section‹Correctness›


subsection‹Modeling Input and Output›

text‹
  With the appropriate assumptions about constprintln and constgetLine,
  we can even prove something.
  We summarize our model about input and output in the assumptions of a locale.
›
locale io_stdio =
  ― ‹We model ‹STDIN› and ‹STDOUT› as part of the typ🌐.
     Note that we know nothing about typ🌐,
     we just model that we can find ‹STDIN› and ‹STDOUT› somewhere in there.›
  fixes stdout_of::"🌐  string list"
  and stdin_of::"🌐  string list"

  ― ‹Assumptions about ‹STDIN›:
      Calling constprintln appends to the end of ‹STDOUT› and constgetLine does not change
      anything.›
assumes stdout_of_println[simp]:
    "stdout_of (exec (println str) world) = stdout_of world@[String.explode str]"
  and stdout_of_getLine[simp]:
    "stdout_of (exec getLine world) = stdout_of world"

  ― ‹Assumptions about ‹STDIN›:
      Calling constprintln does not change anything and constgetLine removes the first element
      from the ‹STDIN› stream.›
  and stdin_of_println[simp]:
    "stdin_of (exec (println str) world) = stdin_of world"
  and stdin_of_getLine:
    "stdin_of world = inp#stdin 
     stdin_of (exec getLine world) = stdin  eval getLine world = String.implode inp"
begin
end


subsection‹Correctness of Hello World›

text‹Correctness of constmain:
    If ‹STDOUT› is initially empty and only term''corny'' will be typed into ‹STDIN›,
    then the program will output: term[''Hello World! What is your name?'', ''Hello, corny!''].
  ›
theorem (in io_stdio)
  assumes stdout: "stdout_of world = []"
       and stdin: "stdin_of world = [''corny'']"
     shows "stdout_of (exec main world) =
              [''Hello World! What is your name?'',
               ''Hello, corny!'']"
proof -
  let ?world1="exec (println (STR ''Hello World! What is your name?'')) world"
  have stdout_world2:
    "literal.explode STR ''Hello World! What is your name?'' =
     ''Hello World! What is your name?''"
    by code_simp
  from stdin_of_getLine[where stdin="[]", OF stdin] have stdin_world2:
    "eval getLine ?world1 = String.implode ''corny''"
    by (simp add: stdin_of_getLine stdin)
  show ?thesis
    unfolding main_def
    apply(simp add: exec_bind)
    apply(simp add: stdout)
    apply(simp add: stdout_world2 stdin_world2)
    apply(simp add: plus_literal.rep_eq)
    apply code_simp
    done
qed

end