Theory HelloWorld_Proof

theory HelloWorld_Proof
  imports HelloWorld
begin

section‹Correctness›


subsection‹Modeling Input and Output›

text‹
  With the appropriate assumptions about \<^const>‹println› and \<^const>‹getLine›,
  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 \<^const>‹println› appends to the end of ▩‹STDOUT› and \<^const>‹getLine› 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 \<^const>‹println› does not change anything and \<^const>‹getLine› 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 \<^const>‹main›:
    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