Homework 6_1

Definitions File

theory Defs
  imports "HOL-IMP.Types"
begin

no_notation btyping (infix "\<turnstile>" 50)
no_notation ctyping (infix "\<turnstile>" 50)

type_synonym ptyenv = "vname \<Rightarrow> ty option"

definition is_inst :: "tyenv \<Rightarrow> ptyenv \<Rightarrow> bool"
  where "is_inst \<Gamma> p\<Gamma> \<equiv> \<forall>x T. p\<Gamma> x = Some T \<longrightarrow> \<Gamma> x = T"

definition combines_to :: "ptyenv \<Rightarrow> ptyenv \<Rightarrow> ptyenv \<Rightarrow> bool" where
  "combines_to p\<Gamma>1 p\<Gamma>2 p\<Gamma> \<equiv> p\<Gamma> = p\<Gamma>1++p\<Gamma>2 \<and>
    (\<forall>x T1 T2. p\<Gamma>1 x = Some T1 \<and> p\<Gamma>2 x = Some T2 \<longrightarrow> T1 = T2)"

definition "test_c \<equiv>
  ''x'' ::= Ic 0;;
  (IF Less (V ''x'') (Ic 2) THEN SKIP ELSE ''y'' ::= Rc 1.0);;
  ''y'' ::= Plus (V ''y'') (Rc 3.1)"


consts check_aexp :: "ptyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"

consts check_bexp :: "ptyenv \<Rightarrow> bexp \<Rightarrow> bool"

consts infer_com :: "ptyenv \<Rightarrow> com \<Rightarrow> ptyenv \<Rightarrow> bool"


end

Template File

theory Submission
  imports Defs
begin

type_synonym ptyenv = "vname \<Rightarrow> ty option"

inductive check_aexp :: "ptyenv \<Rightarrow> aexp \<Rightarrow> ty \<Rightarrow> bool"


inductive check_bexp :: "ptyenv \<Rightarrow> bexp \<Rightarrow> bool"


lemma atyping_if_check_aexp:
    assumes "check_aexp p\<Gamma> a T"
      and "is_inst \<Gamma> p\<Gamma>"
  shows "atyping \<Gamma> a T"
  sorry

lemma check_aexp_if_atyping:
    assumes "atyping \<Gamma> a T"
  shows "check_aexp (\<lambda>x. Some (\<Gamma> x)) a T"
  sorry

lemma btyping_if_check_bexp:
    assumes "check_bexp p\<Gamma> b"
      and "is_inst \<Gamma> p\<Gamma>"
  shows "btyping \<Gamma> b"
  sorry

lemma check_bexp_if_btyping:
    assumes "btyping \<Gamma> b"
  shows "check_bexp (\<lambda>x. Some (\<Gamma> x)) b"
  sorry

inductive infer_com :: "ptyenv \<Rightarrow> com \<Rightarrow> ptyenv \<Rightarrow> bool"


lemma type_test_c:
  "\<exists>p\<Gamma>. infer_com (\<lambda>_. None) test_c p\<Gamma> \<and> ctyping (\<lambda>x. case (p\<Gamma> x) of Some T \<Rightarrow> T | _ \<Rightarrow> Ity) test_c"
txt \<open>As sketched below, a safe way to prove such a lemma is to apply the introduction rules
  manually. Of course, you may also try to automate this proof.
  Note that you may have to adjust the applied introduction rules for your solution.\<close>
  unfolding test_c_def
  apply (rule exI)
  apply (rule conjI)
  apply (rule infer_com.intros)
  apply (rule infer_com.intros)
  apply (rule infer_com.intros)
  apply (rule check_aexp.intros)
  apply (rule refl)
  txt \<open>and so on ...\<close>
sorry

lemma is_inst_if_is_inst_if_infer:
    assumes "infer_com p\<Gamma> c p\<Gamma>'"
      and "is_inst \<Gamma> p\<Gamma>'"
  shows "is_inst \<Gamma> p\<Gamma>"
  sorry

lemma ctyping_if_infer_com:
    assumes "infer_com p\<Gamma> c p\<Gamma>'"
      and "is_inst \<Gamma> p\<Gamma>'"
  shows "ctyping \<Gamma> c"
  sorry

end

Check File

theory Check
  imports Submission
begin

lemma atyping_if_check_aexp: "(check_aexp p\<Gamma> a T) \<Longrightarrow> (is_inst \<Gamma> p\<Gamma>) \<Longrightarrow> atyping \<Gamma> a T"
  by (rule Submission.atyping_if_check_aexp)

lemma check_aexp_if_atyping: "(atyping \<Gamma> a T) \<Longrightarrow> check_aexp (\<lambda>x. Some (\<Gamma> x)) a T"
  by (rule Submission.check_aexp_if_atyping)

lemma btyping_if_check_bexp: "(check_bexp p\<Gamma> b) \<Longrightarrow> (is_inst \<Gamma> p\<Gamma>) \<Longrightarrow> btyping \<Gamma> b"
  by (rule Submission.btyping_if_check_bexp)

lemma check_bexp_if_btyping: "(btyping \<Gamma> b) \<Longrightarrow> check_bexp (\<lambda>x. Some (\<Gamma> x)) b"
  by (rule Submission.check_bexp_if_btyping)

lemma type_test_c: "\<exists>p\<Gamma>. infer_com (\<lambda>_. None) test_c p\<Gamma> \<and> ctyping (\<lambda>x. case (p\<Gamma> x) of Some T \<Rightarrow> T | _ \<Rightarrow> Ity) test_c"
  by (rule Submission.type_test_c)

lemma is_inst_if_is_inst_if_infer: "(infer_com p\<Gamma> c p\<Gamma>') \<Longrightarrow> (is_inst \<Gamma> p\<Gamma>') \<Longrightarrow> is_inst \<Gamma> p\<Gamma>"
  by (rule Submission.is_inst_if_is_inst_if_infer)

lemma ctyping_if_infer_com: "(infer_com p\<Gamma> c p\<Gamma>') \<Longrightarrow> (is_inst \<Gamma> p\<Gamma>') \<Longrightarrow> ctyping \<Gamma> c"
  by (rule Submission.ctyping_if_infer_com)

end