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