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 13

This is the task corresponding to homework 13.

Resources

Download Files

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