Homework 7

Definitions File

theory Defs
  imports "HOL-IMP.Big_Step"
begin

declare [[names_short]]
declare [[syntax_ambiguity_warning=false]]


consts invar :: "vname \<Rightarrow> com \<Rightarrow> bool"

consts incr :: "vname \<Rightarrow> com \<Rightarrow> bool"

consts terminates :: "com \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

fun invar :: "vname \<Rightarrow> com \<Rightarrow> bool"  where
  "invar _ = undefined"

fun incr :: "vname \<Rightarrow> com \<Rightarrow> bool"  where
  "incr _ = undefined"

value "incr ''x'' (''x'' ::= Plus (V ''x'') (N 0);; ''x'' ::= Plus (V ''x'') (N 2)) = True"
value "incr ''y'' (
        WHILE Less (V ''y'') (N 2)
        DO 
          ''y'' ::= Plus (V ''y'') (N 1);;
          ''x''::=Plus (V ''x'') (N (-1))
       ) = False"

lemma incr_less: "(c,s) \<Rightarrow> t \<Longrightarrow> incr x c \<Longrightarrow> s x < t x"
  sorry

fun terminates :: "com \<Rightarrow> bool"  where
  "terminates _ = undefined"

lemma term_w:
  assumes step: "\<And>s. \<exists>t. (c,s) \<Rightarrow> t"
      and incr: "incr x c"
  shows "\<exists>t. (WHILE Less (V x) (N k) DO c, s) \<Rightarrow> t"
  sorry

theorem term_big_step: "terminates c \<Longrightarrow> \<exists>t. (c,s) \<Rightarrow> t"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma incr_less: "(c,s) \<Rightarrow> t \<Longrightarrow> incr x c \<Longrightarrow> s x < t x"
  by (rule Submission.incr_less)

lemma term_w: "(\<And>s. \<exists>t. (c,s) \<Rightarrow> t) \<Longrightarrow> (incr x c) \<Longrightarrow> \<exists>t. (WHILE Less (V x) (N k) DO c, s) \<Rightarrow> t"
  by (rule Submission.term_w)

theorem term_big_step: "terminates c \<Longrightarrow> \<exists>t. (c,s) \<Rightarrow> t"
  by (rule Submission.term_big_step)

end