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