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.


Download Files

Definitions File

theory Defs
  imports Main

(* 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

  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"


Template File

theory Submission
  imports Defs

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

instantiation bval :: order
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

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"

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"

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

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

lemma mono_sem: "mono (sem c)"


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"

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
    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
    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
    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)+

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
    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
  thus ?thesis by (simp add: le_fun_def)

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

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



Check File

theory Check
  imports Submission

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)


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


Terms and Conditions