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.

## Resources

### 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```

Terms and Conditions