Cookies disclaimer

I agree Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

Homework 6_1

This is the task corresponding to homework 6_1.


Download Files

Definitions File

theory Defs
  imports "HOL-IMP.Types"

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"


Template File

theory Submission
  imports Defs

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"

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

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

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

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>

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>"

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


Check File

theory Check
  imports Submission

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)


Terms and Conditions