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 13

This is the task corresponding to homework 13.

## Resources

### Definitions File

```theory Defs
imports Main
begin

(* auxiliary lemmas *)
lemma mono_Sup:
fixes F :: "('a::complete_lattice \<Rightarrow> 'a) set"
assumes "\<And> f. f \<in> F \<Longrightarrow> mono f"
shows "mono (Sup F)"
using assms unfolding mono_def Sup_fun_def by (auto simp add: SUP_subset_mono)

lemma lfp_pres_mono:
fixes F :: "('a::complete_lattice \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
assumes "mono F" "\<And>f. mono f \<Longrightarrow> mono (F f)"
shows "mono (lfp F)"
by (simp add: mono_Sup assms lfp_ordinal_induct)

(* definitions *)
definition "mono2 f \<equiv> \<forall> x1 x2 y1 y2. x1 \<le> y1 \<and> x2 \<le> y2 \<longrightarrow> f x1 x2 \<le> f y1 y2"

type_synonym vname = string
datatype aexp = V vname | N int | Plus aexp aexp

datatype bexp = Bc bool | Less aexp aexp

datatype
com = SKIP
| Assign vname aexp       ("_ ::= _" [1000, 61] 61)
| Seq    com  com         ("_;/ _"  [60, 61] 60)
| If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
| While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)

type_synonym 'val state = "vname \<Rightarrow> 'val"

datatype bval = Nothing | Tr | Fl | Any

fun BBc where "BBc True = Tr" | "BBc False = Fl"

consts less_eq_bval :: "bval \<Rightarrow> bval \<Rightarrow> bool"

consts less_bval :: "bval \<Rightarrow> bval \<Rightarrow> bool"

consts aval :: "aexp \<Rightarrow> 'val state \<Rightarrow> 'val"

consts bval :: "bexp \<Rightarrow> 'val state \<Rightarrow> bval"

consts \<gamma>_st :: "'aval state \<Rightarrow> 'cval state"

consts \<alpha>_st :: "'cval state \<Rightarrow> 'aval state"

end```

### Template File

```theory Submission
imports Defs
begin

type_synonym 'val state = "vname \<Rightarrow> 'val"

instantiation bval :: order
begin
definition less_eq_bval :: "bval \<Rightarrow> bval \<Rightarrow> bool" where
"less_eq_bval _ = undefined"

definition less_bval :: "bval \<Rightarrow> bval \<Rightarrow> bool"  where
"less_bval _ = undefined"

instance sorry
end

lemma not_less_eq_bval[simp]:
"a \<le> Nothing \<longleftrightarrow> a = Nothing" "\<not> Any \<le> Fl" "\<not> Tr \<le> Fl" "\<not> Any \<le> Tr" "\<not> Fl \<le> Tr"
sorry

locale SEM =
fixes NN :: "int \<Rightarrow> 'val::complete_lattice"
and PPlus :: "'val \<Rightarrow> 'val \<Rightarrow> 'val"
and LLess :: "'val \<Rightarrow> 'val \<Rightarrow> bval"
assumes mono2_PPlus: "mono2 PPlus"
and mono2_LLess: "mono2 LLess"
begin

fun aval :: "aexp \<Rightarrow> 'val state \<Rightarrow> 'val"  where
"aval _ = undefined"

fun bval :: "bexp \<Rightarrow> 'val state \<Rightarrow> bval"  where
"bval _ = undefined"

definition wcomb :: "('val state \<Rightarrow> bval) \<Rightarrow> ('val state \<Rightarrow> 'val state) \<Rightarrow> ('val state \<Rightarrow> 'val state)
\<Rightarrow> ('val state \<Rightarrow> 'val state)" where
"wcomb b c w s \<equiv> case b s of
Nothing \<Rightarrow> bot
| Fl \<Rightarrow> s
| Tr \<Rightarrow> w (c s)
| Any \<Rightarrow> sup (w (c s)) s"

fun sem :: "com \<Rightarrow> 'val state \<Rightarrow> 'val state" where
"sem SKIP s = s"
| "sem (x ::= a) s = s(x := aval a s)"
| "sem (c1 ; c2) s = sem c2 (sem c1 s)"
| "sem (IF b THEN c1 ELSE c2) s = (case bval b s of
Nothing \<Rightarrow> bot
| Tr \<Rightarrow> sem c1 s
| Fl \<Rightarrow> sem c2 s
| Any \<Rightarrow> sup (sem c1 s) (sem c2 s))"
| "sem (WHILE b DO c) s = lfp (wcomb (bval b) (sem c)) s"

lemma pres_mono_wcomb:
assumes b: "mono b"
and c: "mono c"
and w: "mono w"
shows "mono (wcomb b c w)"
sorry

lemma mono_wcomb: assumes c: "mono c"  shows "mono (wcomb b c)"
sorry

lemma mono_sem: "mono (sem c)"
sorry

end

locale AI = C : SEM C_NN C_PPlus C_LLess + A : SEM A_NN A_PPlus A_LLess

for C_NN :: "int \<Rightarrow> 'cval::complete_lattice"
and C_PPlus :: "'cval \<Rightarrow> 'cval \<Rightarrow> 'cval"
and C_LLess :: "'cval \<Rightarrow> 'cval \<Rightarrow> bval"

and A_NN :: "int \<Rightarrow> 'aval::complete_lattice"
and A_PPlus :: "'aval \<Rightarrow> 'aval \<Rightarrow> 'aval"
and A_LLess :: "'aval \<Rightarrow> 'aval \<Rightarrow> bval"
+
fixes \<gamma> :: "'aval \<Rightarrow> 'cval"
and \<alpha> :: "'cval \<Rightarrow> 'aval"

assumes \<alpha>_\<gamma>: "cv \<le> \<gamma> (\<alpha> cv)"
and mono_\<gamma>: "mono \<gamma>"
and NN_\<gamma>[simp]: "C_NN i \<le> \<gamma> (A_NN i)"
and PPlus_\<gamma>[simp]: "C_PPlus (\<gamma> av1) (\<gamma> av2) \<le> \<gamma> (A_PPlus av1 av2)"
and LLess_\<gamma>[simp]: "C_LLess (\<gamma> av1) (\<gamma> av2) \<le> A_LLess av1 av2"
begin

abbreviation "C_aval \<equiv> C.aval"  abbreviation "C_bval \<equiv> C.bval"
abbreviation "C_wcomb \<equiv> C.wcomb"  abbreviation "C_sem \<equiv> C.sem"
abbreviation "A_aval \<equiv> A.aval"  abbreviation "A_bval \<equiv> A.bval"
abbreviation "A_wcomb \<equiv> A.wcomb"  abbreviation "A_sem \<equiv> A.sem"

definition \<gamma>_st :: "'aval state \<Rightarrow> 'cval state"
where "\<gamma>_st s x \<equiv> \<gamma> (s x)"

lemma wcomb_\<gamma>:
assumes mw: "mono w"
and w: "w o \<gamma>_st \<le> \<gamma>_st o w'" and c: "c o \<gamma>_st \<le> \<gamma>_st o c'" and b: "b o \<gamma>_st \<le> b'"
shows "(C_wcomb b c w) o \<gamma>_st \<le> \<gamma>_st o (A_wcomb b' c' w')"
proof (subst le_fun_def, standard)
have 0: "\<And>s. w (c (\<gamma>_st s)) \<le> \<gamma>_st (w' (c' s))"
using mw w c order_trans unfolding mono_def comp_def le_fun_def by blast
fix s show " (C_wcomb b c w \<circ> \<gamma>_st) s \<le> (\<gamma>_st \<circ> A_wcomb b' c' w') s"
proof (cases "b' s")
case Nothing
hence "b (\<gamma>_st s) = Nothing"
using b unfolding comp_def le_fun_def
by (cases "b (\<gamma>_st s)") (metis bval.simps not_less_eq_bval)+
thus ?thesis using Nothing unfolding C.wcomb_def A.wcomb_def by auto
next
case Tr
hence "b (\<gamma>_st s) = Nothing \<or> b (\<gamma>_st s) = Tr"
using b unfolding comp_def le_fun_def
by (cases "b (\<gamma>_st s)") (metis not_less_eq_bval)+
thus ?thesis using Tr 0 unfolding C.wcomb_def A.wcomb_def by auto
next
case Fl
hence "b (\<gamma>_st s) = Nothing \<or> b (\<gamma>_st s) = Fl"
using b unfolding comp_def le_fun_def
by (cases "b (\<gamma>_st s)") (metis not_less_eq_bval)+
thus ?thesis using Fl 0 unfolding C.wcomb_def A.wcomb_def by auto
next
case Any
thus ?thesis
unfolding C.wcomb_def A.wcomb_def
by (auto split: bval.splits)
(smt 0 \<gamma>_st_def le_fun_def le_sup_iff mono_\<gamma> mono_sup order_trans sup_fun_def)+
qed
qed

lemma lfp_wcomb_\<gamma>:
assumes c: "mono c"
and b: "mono b"
and c': "mono c'"
and b': "mono b'"
and cc': "c o \<gamma>_st \<le> \<gamma>_st o c'"
and bb': "b o \<gamma>_st \<le> b'"
shows "lfp (C_wcomb b c) (\<gamma>_st s) \<le> \<gamma>_st (lfp (A_wcomb b' c') s)"
proof -
let ?F = "C_wcomb b c"
let ?F' = "A_wcomb b' c'"
have F: "mono ?F" and F': "mono ?F'"
using C.mono_wcomb[OF c] A.mono_wcomb[OF c'] by auto
have "mono (lfp ?F) \<and> lfp ?F \<circ> \<gamma>_st \<le> \<gamma>_st \<circ> lfp ?F'"
proof (induction rule: lfp_ordinal_induct[OF F])
case 1 then show ?case
using wcomb_\<gamma>[OF _ _ cc' bb', of _"lfp ?F'"] C.pres_mono_wcomb[OF b c]
unfolding lfp_unfold[symmetric, OF F'] by blast
next
case (2 A)
then have "mono (Sup A)"
using mono_Sup by fast
moreover have "Sup A \<circ> \<gamma>_st \<le> \<gamma>_st \<circ> lfp ?F'"
unfolding comp_def using 2 by (auto simp: le_fun_def intro: SUP_least)
ultimately show ?case by blast
qed
thus ?thesis by (simp add: le_fun_def)
qed

lemma soundness: "C_sem c (\<gamma>_st s) \<le> \<gamma>_st (A_sem c s)"
sorry

definition \<alpha>_st :: "'cval state \<Rightarrow> 'aval state" where
"\<alpha>_st _ = undefined"

lemma soundness_\<alpha>: "C_sem c s \<le> \<gamma>_st (A_sem c (\<alpha>_st s))"
sorry

end

end```

### Check File

```theory Check
imports Submission
begin

lemma not_less_eq_bval: "a \<le> Nothing \<longleftrightarrow> a = Nothing"
by (rule Submission.not_less_eq_bval)

context SEM begin
lemma pres_mono_wcomb: "(mono b) \<Longrightarrow> (mono c) \<Longrightarrow> (mono w) \<Longrightarrow> mono (wcomb b c w)"
by (rule pres_mono_wcomb)

lemma mono_wcomb: "(mono c) \<Longrightarrow> mono (wcomb b c)"
by (rule mono_wcomb)

lemma mono_sem: "mono (sem c)"
by (rule mono_sem)

end

context AI begin
lemma lfp_wcomb_\<gamma>: "(mono c) \<Longrightarrow> (mono b) \<Longrightarrow> (mono c') \<Longrightarrow> (mono b') \<Longrightarrow> (c o \<gamma>_st \<le> \<gamma>_st o c') \<Longrightarrow> (b o \<gamma>_st \<le> b') \<Longrightarrow> lfp (C_wcomb b c) (\<gamma>_st s) \<le> \<gamma>_st (lfp (A_wcomb b' c') s)"
by (rule lfp_wcomb_\<gamma>)

lemma soundness: "C_sem c (\<gamma>_st s) \<le> \<gamma>_st (A_sem c s)"
by (rule soundness)

lemma soundness_\<alpha>: "C_sem c s \<le> \<gamma>_st (A_sem c (\<alpha>_st s))"
by (rule soundness_\<alpha>)
end

end```

Terms and Conditions