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-Library.While_Combinator" "HOL-Library.Extended" "HOL-IMP.Complete_Lattice" begin
datatype 'a word = Word 'a 'a 'a 'a
type_synonym vname = string
type_synonym val = "bool word"
type_synonym state = "vname \<Rightarrow> val"
datatype aexp = N val | V vname | Bit_And aexp aexp | Bit_Or aexp aexp
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
fun bitwise :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a word \<Rightarrow> 'b word \<Rightarrow> 'c word" where
"bitwise f w v = (case (w, v) of (Word a b c d, Word u v w x) \<Rightarrow> Word (f a u) (f b v) (f c w) (f d x))"
fun split :: "('a \<times> 'b) word \<Rightarrow> ('a word \<times> 'b word)" where
"split w = (case w of (Word (a\<^sub>1,a\<^sub>2) (b\<^sub>1,b\<^sub>2) (c\<^sub>1,c\<^sub>2) (d\<^sub>1,d\<^sub>2)) \<Rightarrow> (Word a\<^sub>1 b\<^sub>1 c\<^sub>1 d\<^sub>1, Word a\<^sub>2 b\<^sub>2 c\<^sub>2 d\<^sub>2))"
definition all :: "bool word \<Rightarrow> bool" where
"all w = (w = Word True True True True)"
instantiation word :: (ord) ord
begin
definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
"w \<le> v = all (bitwise (\<le>) w v)"
definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
"less_word w v = (w \<le> v \<and> w \<noteq> v)"
instance by standard
end
instance word :: (order) order
by standard (auto simp: less_eq_word_def less_word_def all_def split: word.splits)
instantiation word :: (inf) inf
begin
definition inf_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" where
"inf_word = bitwise inf"
instance by standard
end
instantiation word :: (sup) sup
begin
definition sup_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" where
"sup_word = bitwise sup"
instance by standard
end
instance word :: (semilattice_inf) semilattice_inf
by standard (auto simp: less_eq_word_def inf_word_def all_def split: word.splits)
instance word :: (semilattice_sup) semilattice_sup
by standard (auto simp: less_eq_word_def sup_word_def all_def split: word.splits)
instantiation word :: (top) top
begin
definition top_word :: "'a word" where
"top_word = Word top top top top"
instance ..
end
instantiation word :: (bot) bot
begin
definition bot_word :: "'a word" where
"bot_word = Word bot bot bot bot"
instance ..
end
instance word :: (order_top) order_top
by standard (auto simp: less_eq_word_def all_def top_word_def split: word.splits)
instance word :: (bounded_lattice) bounded_lattice
by standard (auto simp: less_eq_word_def all_def bot_word_def split: word.splits)
class vars =
fixes vars :: "'a \<Rightarrow> vname set"
definition bit_and ("_ AND _") where
"(w AND v) = bitwise (\<and>) w v"
definition bit_or ("_ OR _") where
"(w OR v) = bitwise (\<or>) w v"
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
"aval (N n) s = n" |
"aval (V x) s = s x" |
"aval (Bit_And a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s AND aval a\<^sub>2 s" |
"aval (Bit_Or a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s OR aval a\<^sub>2 s"
instantiation aexp :: vars
begin
fun vars_aexp :: "aexp \<Rightarrow> vname set" where
"vars (N n) = {}" |
"vars (V x) = {x}" |
"vars (Bit_And a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \<union> vars a\<^sub>2" |
"vars (Bit_Or a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \<union> vars a\<^sub>2"
instance ..
end
definition null_state ("<>") where
"null_state \<equiv> \<lambda>x. 0"
syntax
"_State" :: "updbinds => 'a" ("<_>")
translations
"_State ms" == "_Update <> ms"
"_State (_updbinds b bs)" <= "_Update (_State b) bs"
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
"bval (Bc v) s = v" |
"bval (Not b) s = (\<not> bval b s)" |
"bval (And b\<^sub>1 b\<^sub>2) s = (bval b\<^sub>1 s \<and> bval b\<^sub>2 s)" |
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
instantiation bexp :: vars
begin
fun vars_bexp :: "bexp \<Rightarrow> vname set" where
"vars (Bc v) = {}" |
"vars (Not b) = vars b" |
"vars (And b1 b2) = vars b1 \<union> vars b2" |
"vars (Less a1 a2) = vars a1 \<union> vars a2"
instance ..
end
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)
fun lvars :: "com \<Rightarrow> vname set" where
"lvars SKIP = {}" |
"lvars (x::=e) = {x}" |
"lvars (c1;;c2) = lvars c1 \<union> lvars c2" |
"lvars (IF b THEN c1 ELSE c2) = lvars c1 \<union> lvars c2" |
"lvars (WHILE b DO c) = lvars c"
fun rvars :: "com \<Rightarrow> vname set" where
"rvars SKIP = {}" |
"rvars (x::=e) = vars e" |
"rvars (c1;;c2) = rvars c1 \<union> rvars c2" |
"rvars (IF b THEN c1 ELSE c2) = vars b \<union> rvars c1 \<union> rvars c2" |
"rvars (WHILE b DO c) = vars b \<union> rvars c"
instantiation com :: vars
begin
definition "vars_com c = lvars c \<union> rvars c"
instance ..
end
lemma vars_com_simps[simp]:
"vars SKIP = {}"
"vars (x::=e) = {x} \<union> vars e"
"vars (c1;;c2) = vars c1 \<union> vars c2"
"vars (IF b THEN c1 ELSE c2) = vars b \<union> vars c1 \<union> vars c2"
"vars (WHILE b DO c) = vars b \<union> vars c"
by(auto simp: vars_com_def)
inductive
big_step :: "com \<times> state \<Rightarrow> state \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
where
Skip: "(SKIP,s) \<Rightarrow> s" |
Assign: "(x ::= a,s) \<Rightarrow> s(x := aval a s)" |
Seq: "\<lbrakk> (c\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2; (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk> \<Longrightarrow> (c\<^sub>1;;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3" |
IfTrue: "\<lbrakk> bval b s; (c\<^sub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
IfFalse: "\<lbrakk> \<not>bval b s; (c\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
WhileTrue:
"\<lbrakk> bval b s\<^sub>1; (c,s\<^sub>1) \<Rightarrow> s\<^sub>2; (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3 \<rbrakk>
\<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>3"
lemmas big_step_induct = big_step.induct[split_format(complete)]
code_pred big_step .
datatype 'a acom =
SKIP 'a ("SKIP {_}" 61) |
Assign vname aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
Seq "('a acom)" "('a acom)" ("_;;//_" [60, 61] 60) |
If bexp 'a "('a acom)" 'a "('a acom)" 'a
("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})" [0, 0, 0, 61, 0, 0] 61) |
While 'a bexp 'a "('a acom)" 'a
("({_}//WHILE _//DO ({_}//_)//{_})" [0, 0, 0, 61, 0] 61)
notation com.SKIP ("SKIP")
fun strip :: "'a acom \<Rightarrow> com" where
"strip (SKIP {P}) = SKIP" |
"strip (x ::= e {P}) = x ::= e" |
"strip (C\<^sub>1;;C\<^sub>2) = strip C\<^sub>1;; strip C\<^sub>2" |
"strip (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {P}) =
IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2" |
"strip ({I} WHILE b DO {P} C {Q}) = WHILE b DO strip C"
fun asize :: "com \<Rightarrow> nat" where
"asize SKIP = 1" |
"asize (x ::= e) = 1" |
"asize (C\<^sub>1;;C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2" |
"asize (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2 + 3" |
"asize (WHILE b DO C) = asize C + 3"
definition shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where
"shift f n = (\<lambda>p. f(p+n))"
fun annotate :: "(nat \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom" where
"annotate f SKIP = SKIP {f 0}" |
"annotate f (x ::= e) = x ::= e {f 0}" |
"annotate f (c\<^sub>1;;c\<^sub>2) = annotate f c\<^sub>1;; annotate (shift f (asize c\<^sub>1)) c\<^sub>2" |
"annotate f (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
IF b THEN {f 0} annotate (shift f 1) c\<^sub>1
ELSE {f(asize c\<^sub>1 + 1)} annotate (shift f (asize c\<^sub>1 + 2)) c\<^sub>2
{f(asize c\<^sub>1 + asize c\<^sub>2 + 2)}" |
"annotate f (WHILE b DO c) =
{f 0} WHILE b DO {f 1} annotate (shift f 2) c {f(asize c + 2)}"
fun annos :: "'a acom \<Rightarrow> 'a list" where
"annos (SKIP {P}) = [P]" |
"annos (x ::= e {P}) = [P]" |
"annos (C\<^sub>1;;C\<^sub>2) = annos C\<^sub>1 @ annos C\<^sub>2" |
"annos (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {Q}) =
P\<^sub>1 # annos C\<^sub>1 @ P\<^sub>2 # annos C\<^sub>2 @ [Q]" |
"annos ({I} WHILE b DO {P} C {Q}) = I # P # annos C @ [Q]"
definition anno :: "'a acom \<Rightarrow> nat \<Rightarrow> 'a" where
"anno C p = annos C ! p"
definition post :: "'a acom \<Rightarrow>'a" where
"post C = last(annos C)"
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
"map_acom f (SKIP {P}) = SKIP {f P}" |
"map_acom f (x ::= e {P}) = x ::= e {f P}" |
"map_acom f (C\<^sub>1;;C\<^sub>2) = map_acom f C\<^sub>1;; map_acom f C\<^sub>2" |
"map_acom f (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {Q}) =
IF b THEN {f P\<^sub>1} map_acom f C\<^sub>1 ELSE {f P\<^sub>2} map_acom f C\<^sub>2
{f Q}" |
"map_acom f ({I} WHILE b DO {P} C {Q}) =
{f I} WHILE b DO {f P} map_acom f C {f Q}"
lemma annos_ne: "annos C \<noteq> []"
by(induction C) auto
lemma strip_annotate[simp]: "strip(annotate f c) = c"
by(induction c arbitrary: f) auto
lemma length_annos_annotate[simp]: "length (annos (annotate f c)) = asize c"
by(induction c arbitrary: f) auto
lemma size_annos: "size(annos C) = asize(strip C)"
by(induction C)(auto)
lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)"
apply(induct C2 arbitrary: C1)
apply(case_tac C1, simp_all)+
done
lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
lemma anno_annotate[simp]: "p < asize c \<Longrightarrow> anno (annotate f c) p = f p"
apply(induction c arbitrary: f p)
apply (auto simp: anno_def nth_append nth_Cons numeral_eq_Suc shift_def
split: nat.split)
apply (metis add_Suc_right add_diff_inverse add.commute)
apply(rule_tac f=f in arg_cong)
apply arith
apply (metis less_Suc_eq)
done
lemma eq_acom_iff_strip_annos:
"C1 = C2 \<longleftrightarrow> strip C1 = strip C2 \<and> annos C1 = annos C2"
apply(induction C1 arbitrary: C2)
apply(case_tac C2, auto simp: size_annos_same2)+
done
lemma eq_acom_iff_strip_anno:
"C1=C2 \<longleftrightarrow> strip C1 = strip C2 \<and> (\<forall>p < size(annos C1). anno C1 p = anno C2 p)"
by(auto simp add: eq_acom_iff_strip_annos anno_def
list_eq_iff_nth_eq size_annos_same2)
lemma post_map_acom[simp]: "post(map_acom f C) = f(post C)"
by (induction C) (auto simp: post_def last_append annos_ne)
lemma strip_map_acom[simp]: "strip (map_acom f C) = strip C"
by (induction C) auto
lemma anno_map_acom: "p < size(annos C) \<Longrightarrow> anno (map_acom f C) p = f(anno C p)"
apply(induction C arbitrary: p)
apply(auto simp: anno_def nth_append nth_Cons' size_annos)
done
lemma strip_eq_SKIP:
"strip C = SKIP \<longleftrightarrow> (EX P. C = SKIP {P})"
by (cases C) simp_all
lemma strip_eq_Assign:
"strip C = x::=e \<longleftrightarrow> (EX P. C = x::=e {P})"
by (cases C) simp_all
lemma strip_eq_Seq:
"strip C = c1;;c2 \<longleftrightarrow> (EX C1 C2. C = C1;;C2 & strip C1 = c1 & strip C2 = c2)"
by (cases C) simp_all
lemma strip_eq_If:
"strip C = IF b THEN c1 ELSE c2 \<longleftrightarrow>
(EX P1 P2 C1 C2 Q. C = IF b THEN {P1} C1 ELSE {P2} C2 {Q} & strip C1 = c1 & strip C2 = c2)"
by (cases C) simp_all
lemma strip_eq_While:
"strip C = WHILE b DO c1 \<longleftrightarrow>
(EX I P C1 Q. C = {I} WHILE b DO {P} C1 {Q} & strip C1 = c1)"
by (cases C) simp_all
lemma [simp]: "shift (\<lambda>p. a) n = (\<lambda>p. a)"
by(simp add:shift_def)
lemma set_annos_anno[simp]: "set (annos (annotate (\<lambda>p. a) c)) = {a}"
by(induction c) simp_all
lemma post_in_annos: "post C \<in> set(annos C)"
by(auto simp: post_def annos_ne)
lemma post_anno_asize: "post C = anno C (size(annos C) - 1)"
by(simp add: post_def last_conv_nth[OF annos_ne] anno_def)
notation
sup (infixl "\<squnion>" 65) and
inf (infixl "\<sqinter>" 70) and
bot ("\<bottom>") and
top ("\<top>")
context
fixes f :: "vname \<Rightarrow> aexp \<Rightarrow> 'a \<Rightarrow> 'a::sup"
fixes g :: "bexp \<Rightarrow> 'a \<Rightarrow> 'a"
begin
fun Step :: "'a \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
"Step S (SKIP {Q}) = (SKIP {S})" |
"Step S (x ::= e {Q}) =
x ::= e {f x e S}" |
"Step S (C1;; C2) = Step S C1;; Step (post C1) C2" |
"Step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
IF b THEN {g b S} Step P1 C1 ELSE {g (Not b) S} Step P2 C2
{post C1 \<squnion> post C2}" |
"Step S ({I} WHILE b DO {P} C {Q}) =
{S \<squnion> post C} WHILE b DO {g b I} Step P C {g (Not b) I}"
end
lemma strip_Step[simp]: "strip(Step f g S C) = strip C"
by(induct C arbitrary: S) auto
subsection "Collecting Semantics of Commands"
subsubsection "Annotated commands as a complete lattice"
instantiation acom :: (order) order
begin
definition less_eq_acom :: "('a::order)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
"C1 \<le> C2 \<longleftrightarrow> strip C1 = strip C2 \<and> (\<forall>p < size(annos C1). anno C1 p \<le> anno C2 p)"
definition less_acom :: "'a acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
"less_acom x y = (x \<le> y \<and> \<not> y \<le> x)"
instance
proof (standard, goal_cases)
case 1 show ?case by(simp add: less_acom_def)
next
case 2 thus ?case by(auto simp: less_eq_acom_def)
next
case 3 thus ?case by(fastforce simp: less_eq_acom_def size_annos)
next
case 4 thus ?case
by(fastforce simp: le_antisym less_eq_acom_def size_annos
eq_acom_iff_strip_anno)
qed
end
lemma less_eq_acom_annos:
"C1 \<le> C2 \<longleftrightarrow> strip C1 = strip C2 \<and> list_all2 (\<le>) (annos C1) (annos C2)"
by(auto simp add: less_eq_acom_def anno_def list_all2_conv_all_nth size_annos_same2)
lemma SKIP_le[simp]: "SKIP {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<le> S')"
by (cases c) (auto simp:less_eq_acom_def anno_def)
lemma Assign_le[simp]: "x ::= e {S} \<le> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<le> S')"
by (cases c) (auto simp:less_eq_acom_def anno_def)
lemma Seq_le[simp]: "C1;;C2 \<le> C \<longleftrightarrow> (\<exists>C1' C2'. C = C1';;C2' \<and> C1 \<le> C1' \<and> C2 \<le> C2')"
apply (cases C)
apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
done
lemma If_le[simp]: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<le> C \<longleftrightarrow>
(\<exists>p1' p2' C1' C2' S'. C = IF b THEN {p1'} C1' ELSE {p2'} C2' {S'} \<and>
p1 \<le> p1' \<and> p2 \<le> p2' \<and> C1 \<le> C1' \<and> C2 \<le> C2' \<and> S \<le> S')"
apply (cases C)
apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
done
lemma While_le[simp]: "{I} WHILE b DO {p} C {P} \<le> W \<longleftrightarrow>
(\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> C \<le> C' \<and> p \<le> p' \<and> I \<le> I' \<and> P \<le> P')"
apply (cases W)
apply(auto simp: less_eq_acom_annos list_all2_append size_annos_same2)
done
lemma mono_post: "C \<le> C' \<Longrightarrow> post C \<le> post C'"
using annos_ne[of C']
by(auto simp: post_def less_eq_acom_def last_conv_nth[OF annos_ne] anno_def
dest: size_annos_same)
definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
"Inf_acom c M = annotate (\<lambda>p. INF C\<in>M. anno C p) c"
global_interpretation
Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
proof (standard, goal_cases)
case 1 thus ?case
by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_lower)
next
case 2 thus ?case
by(auto simp: Inf_acom_def less_eq_acom_def size_annos intro:INF_greatest)
next
case 3 thus ?case by(auto simp: Inf_acom_def)
qed
subsubsection "Collecting semantics"
definition "step = Step (\<lambda>x e S. {s(x := aval e s) |s. s : S}) (\<lambda>b S. {s:S. bval b s})"
definition CS :: "com \<Rightarrow> state set acom" where
"CS c = lfp c (step UNIV)"
lemma mono2_Step: fixes C1 C2 :: "'a::semilattice_sup acom"
assumes "!!x e S1 S2. S1 \<le> S2 \<Longrightarrow> f x e S1 \<le> f x e S2"
"!!b S1 S2. S1 \<le> S2 \<Longrightarrow> g b S1 \<le> g b S2"
shows "C1 \<le> C2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> Step f g S1 C1 \<le> Step f g S2 C2"
proof(induction S1 C1 arbitrary: C2 S2 rule: Step.induct)
case 1 thus ?case by(auto)
next
case 2 thus ?case by (auto simp: assms(1))
next
case 3 thus ?case by(auto simp: mono_post)
next
case 4 thus ?case
by(auto simp: subset_iff assms(2))
(metis mono_post le_supI1 le_supI2)+
next
case 5 thus ?case
by(auto simp: subset_iff assms(2))
(metis mono_post le_supI1 le_supI2)+
qed
lemma mono2_step: "C1 \<le> C2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 C1 \<le> step S2 C2"
unfolding step_def by(rule mono2_Step) auto
lemma mono_step: "mono (step S)"
by(blast intro: monoI mono2_step)
lemma strip_step: "strip(step S C) = strip C"
by (induction C arbitrary: S) (auto simp: step_def)
lemma lfp_cs_unfold: "lfp c (step S) = step S (lfp c (step S))"
apply(rule lfp_unfold[OF _ mono_step])
apply(simp add: strip_step)
done
lemma CS_unfold: "CS c = step UNIV (CS c)"
by (metis CS_def lfp_cs_unfold)
lemma strip_CS[simp]: "strip(CS c) = c"
by(simp add: CS_def index_lfp[simplified])
subsubsection "Relation to big-step semantics"
lemma asize_nz: "asize(c::com) \<noteq> 0"
by (metis length_0_conv length_annos_annotate annos_ne)
lemma post_Inf_acom:
"\<forall>C\<in>M. strip C = c \<Longrightarrow> post (Inf_acom c M) = \<Inter>(post ` M)"
apply(subgoal_tac "\<forall>C\<in>M. size(annos C) = asize c")
apply(simp add: post_anno_asize Inf_acom_def asize_nz neq0_conv[symmetric])
apply(simp add: size_annos)
done
lemma post_lfp: "post(lfp c f) = (\<Inter>{post C|C. strip C = c \<and> f C \<le> C})"
by(auto simp add: lfp_def post_Inf_acom)
lemma big_step_post_step:
"\<lbrakk> (c, s) \<Rightarrow> t; strip C = c; s \<in> S; step S C \<le> C \<rbrakk> \<Longrightarrow> t \<in> post C"
proof(induction arbitrary: C S rule: big_step_induct)
case Skip thus ?case by(auto simp: strip_eq_SKIP step_def post_def)
next
case Assign thus ?case
by(fastforce simp: strip_eq_Assign step_def post_def)
next
case Seq thus ?case
by(fastforce simp: strip_eq_Seq step_def post_def last_append annos_ne)
next
case IfTrue thus ?case apply(auto simp: strip_eq_If step_def post_def)
by (metis (no_types, lifting) mem_Collect_eq subset_eq)
next
case IfFalse thus ?case apply(auto simp: strip_eq_If step_def post_def)
by (metis (no_types, lifting) mem_Collect_eq subset_eq)
next
case (WhileTrue b s1 c' s2 s3)
from WhileTrue.prems(1) obtain I P C' Q where "C = {I} WHILE b DO {P} C' {Q}" "strip C' = c'"
by(auto simp: strip_eq_While)
from WhileTrue.prems(3) `C = _`
have "step P C' \<le> C'" "{s \<in> I. bval b s} \<le> P" "S \<le> I" "step (post C') C \<le> C"
by (auto simp: step_def post_def)
have "step {s \<in> I. bval b s} C' \<le> C'"
by (rule order_trans[OF mono2_step[OF order_refl `{s \<in> I. bval b s} \<le> P`] `step P C' \<le> C'`])
have "s1: {s:I. bval b s}" using `s1 \<in> S` `S \<subseteq> I` `bval b s1` by auto
note s2_in_post_C' = WhileTrue.IH(1)[OF `strip C' = c'` this `step {s \<in> I. bval b s} C' \<le> C'`]
from WhileTrue.IH(2)[OF WhileTrue.prems(1) s2_in_post_C' `step (post C') C \<le> C`]
show ?case .
next
case (WhileFalse b s1 c') thus ?case
by (force simp: strip_eq_While step_def post_def)
qed
lemma big_step_lfp: "\<lbrakk> (c,s) \<Rightarrow> t; s \<in> S \<rbrakk> \<Longrightarrow> t \<in> post(lfp c (step S))"
by(auto simp add: post_lfp intro: big_step_post_step)
lemma big_step_CS: "(c,s) \<Rightarrow> t \<Longrightarrow> t : post(CS c)"
by(simp add: CS_def big_step_lfp)
subsection "Orderings"
text \<open>
The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are
defined in @{theory Main}, more precisely in theories Orderings and Lattices.
If you view this theory with jedit, just click on the names to get there.
\<close>
class semilattice_sup_top = semilattice_sup + order_top
instance "fun" :: (type, semilattice_sup_top) semilattice_sup_top ..
instantiation option :: (order)order
begin
fun less_eq_option where
"Some x \<le> Some y = (x \<le> y)" |
"None \<le> y = True" |
"Some _ \<le> None = False"
definition less_option where "x < (y::'a option) = (x \<le> y \<and> \<not> y \<le> x)"
lemma le_None[simp]: "(x \<le> None) = (x = None)"
by (cases x) simp_all
lemma Some_le[simp]: "(Some x \<le> u) = (\<exists>y. u = Some y \<and> x \<le> y)"
by (cases u) auto
instance
proof (standard, goal_cases)
case 1 show ?case by(rule less_option_def)
next
case (2 x) show ?case by(cases x, simp_all)
next
case (3 x y z) thus ?case by(cases z, simp, cases y, simp, cases x, auto)
next
case (4 x y) thus ?case by(cases y, simp, cases x, auto)
qed
end
instantiation option :: (sup)sup
begin
fun sup_option where
"Some x \<squnion> Some y = Some(x \<squnion> y)" |
"None \<squnion> y = y" |
"x \<squnion> None = x"
lemma sup_None2[simp]: "x \<squnion> None = x"
by (cases x) simp_all
instance ..
end
instantiation option :: (semilattice_sup_top)semilattice_sup_top
begin
definition top_option where "\<top> = Some \<top>"
instance
proof (standard, goal_cases)
case (4 a) show ?case by(cases a, simp_all add: top_option_def)
next
case (1 x y) thus ?case by(cases x, simp, cases y, simp_all)
next
case (2 x y) thus ?case by(cases y, simp, cases x, simp_all)
next
case (3 x y z) thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
qed
end
lemma [simp]: "(Some x < Some y) = (x < y)"
by(auto simp: less_le)
instantiation option :: (order)order_bot
begin
definition bot_option :: "'a option" where
"\<bottom> = None"
instance
proof (standard, goal_cases)
case 1 thus ?case by(auto simp: bot_option_def)
qed
end
definition bot :: "com \<Rightarrow> 'a option acom" where
"bot c = annotate (\<lambda>p. None) c"
lemma bot_least: "strip C = c \<Longrightarrow> bot c \<le> C"
by(auto simp: bot_def less_eq_acom_def)
lemma strip_bot[simp]: "strip(bot c) = c"
by(simp add: bot_def)
subsubsection "Pre-fixpoint iteration"
definition pfp :: "(('a::order) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
"pfp f = while_option (\<lambda>x. \<not> f x \<le> x) f"
lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<le> x"
using while_option_stop[OF assms[simplified pfp_def]] by simp
lemma while_least:
fixes q :: "'a::order"
assumes "\<forall>x\<in>L.\<forall>y\<in>L. x \<le> y \<longrightarrow> f x \<le> f y" and "\<forall>x. x \<in> L \<longrightarrow> f x \<in> L"
and "\<forall>x \<in> L. b \<le> x" and "b \<in> L" and "f q \<le> q" and "q \<in> L"
and "while_option P f b = Some p"
shows "p \<le> q"
using while_option_rule[OF _ assms(7)[unfolded pfp_def],
where P = "%x. x \<in> L \<and> x \<le> q"]
by (metis assms(1-6) order_trans)
lemma pfp_bot_least:
assumes "\<forall>x\<in>{C. strip C = c}.\<forall>y\<in>{C. strip C = c}. x \<le> y \<longrightarrow> f x \<le> f y"
and "\<forall>C. C \<in> {C. strip C = c} \<longrightarrow> f C \<in> {C. strip C = c}"
and "f C' \<le> C'" "strip C' = c" "pfp f (bot c) = Some C"
shows "C \<le> C'"
by(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(5)[unfolded pfp_def]])
(simp_all add: assms(4) bot_least)
lemma pfp_inv:
"pfp f x = Some y \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P(f x)) \<Longrightarrow> P x \<Longrightarrow> P y"
unfolding pfp_def by (blast intro: while_option_rule)
lemma strip_pfp:
assumes "\<And>x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"
using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp
subsection "Abstract Interpretation"
definition \<gamma>_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
"\<gamma>_fun \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(F x)}"
fun \<gamma>_option :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a option \<Rightarrow> 'b set" where
"\<gamma>_option \<gamma> None = {}" |
"\<gamma>_option \<gamma> (Some a) = \<gamma> a"
text \<open>The interface for abstract values:\<close>
locale Val_semilattice =
fixes \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
assumes mono_gamma: "a \<le> b \<Longrightarrow> \<gamma> a \<le> \<gamma> b"
and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
fixes num' :: "val \<Rightarrow> 'av"
and and' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
and or' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
assumes gamma_num': "i \<in> \<gamma>(num' i)"
and gamma_and': "i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1 AND i2 \<in> \<gamma>(and' a1 a2)"
and gamma_or': "i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1 OR i2 \<in> \<gamma>(or' a1 a2)"
type_synonym 'av st = "(vname \<Rightarrow> 'av)"
text \<open>
The for-clause (here and elsewhere) only serves the purpose of fixing
the name of the type parameter @{typ 'av} which would otherwise be renamed to
@{typ 'a}.
\<close>
locale Abs_Int_fun = Val_semilattice where \<gamma>=\<gamma>
for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin
fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
"aval' (N i) S = num' i" |
"aval' (V x) S = S x" |
"aval' (Bit_And a1 a2) S = and' (aval' a1 S) (aval' a2 S)" |
"aval' (Bit_Or a1 a2) S = or' (aval' a1 S) (aval' a2 S)"
definition "asem x e S = (case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S)))"
definition "step' = Step asem (\<lambda>b S. S)"
lemma strip_step'[simp]: "strip(step' S C) = strip C"
by(simp add: step'_def)
definition AI :: "com \<Rightarrow> 'av st option acom option" where
"AI c = pfp (step' \<top>) (bot c)"
abbreviation \<gamma>\<^sub>s :: "'av st \<Rightarrow> state set"
where "\<gamma>\<^sub>s == \<gamma>_fun \<gamma>"
abbreviation \<gamma>\<^sub>o :: "'av st option \<Rightarrow> state set"
where "\<gamma>\<^sub>o == \<gamma>_option \<gamma>\<^sub>s"
abbreviation \<gamma>\<^sub>c :: "'av st option acom \<Rightarrow> state set acom"
where "\<gamma>\<^sub>c == map_acom \<gamma>\<^sub>o"
lemma gamma_s_Top[simp]: "\<gamma>\<^sub>s \<top> = UNIV"
by(simp add: top_fun_def \<gamma>_fun_def)
lemma gamma_o_Top[simp]: "\<gamma>\<^sub>o \<top> = UNIV"
by (simp add: top_option_def)
lemma mono_gamma_s: "f1 \<le> f2 \<Longrightarrow> \<gamma>\<^sub>s f1 \<subseteq> \<gamma>\<^sub>s f2"
by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
lemma mono_gamma_o:
"S1 \<le> S2 \<Longrightarrow> \<gamma>\<^sub>o S1 \<subseteq> \<gamma>\<^sub>o S2"
by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^sub>c C1 \<le> \<gamma>\<^sub>c C2"
by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])
text \<open>Correctness:\<close>
lemma aval'_correct: "s : \<gamma>\<^sub>s S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
by (induct a) (auto simp: gamma_num' gamma_and' gamma_or' \<gamma>_fun_def)
lemma in_gamma_update: "\<lbrakk> s : \<gamma>\<^sub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^sub>s(S(x := a))"
by(simp add: \<gamma>_fun_def)
lemma gamma_Step_subcomm:
assumes "!!x e S. f1 x e (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (f2 x e S)" "!!b S. g1 b (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (g2 b S)"
shows "Step f1 g1 (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (Step f2 g2 S C)"
by (induction C arbitrary: S) (auto simp: mono_gamma_o assms)
lemma step_step': "step (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' S C)"
unfolding step_def step'_def
by(rule gamma_Step_subcomm)
(auto simp: aval'_correct in_gamma_update asem_def split: option.splits)
lemma AI_correct: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c C"
proof(simp add: CS_def AI_def)
assume 1: "pfp (step' \<top>) (bot c) = Some C"
have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
have 2: "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c C" \<comment> \<open>transfer the pfp'\<close>
proof(rule order_trans)
show "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' \<top> C)" by(rule step_step')
show "... \<le> \<gamma>\<^sub>c C" by (metis mono_gamma_c[OF pfp'])
qed
have 3: "strip (\<gamma>\<^sub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
have "lfp c (step (\<gamma>\<^sub>o \<top>)) \<le> \<gamma>\<^sub>c C"
by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^sub>o \<top>)", OF 3 2])
thus "lfp c (step UNIV) \<le> \<gamma>\<^sub>c C" by simp
qed
end
subsubsection "Monotonicity"
locale Abs_Int_fun_mono = Abs_Int_fun +
assumes mono_and': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> and' a1 a2 \<le> and' b1 b2"
and mono_or': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> or' a1 a2 \<le> or' b1 b2"
begin
lemma mono_aval': "S \<le> S' \<Longrightarrow> aval' e S \<le> aval' e S'"
by(induction e)(auto simp: le_fun_def mono_and' mono_or')
lemma mono_update: "a \<le> a' \<Longrightarrow> S \<le> S' \<Longrightarrow> S(x := a) \<le> S'(x := a')"
by(simp add: le_fun_def)
lemma mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
unfolding step'_def
by(rule mono2_Step)
(auto simp: mono_update mono_aval' asem_def split: option.split)
lemma mono_step'_top: "C \<le> C' \<Longrightarrow> step' \<top> C \<le> step' \<top> C'"
by (metis mono_step' order_refl)
lemma AI_least_pfp: assumes "AI c = Some C" "step' \<top> C' \<le> C'" "strip C' = c"
shows "C \<le> C'"
by(rule pfp_bot_least[OF _ _ assms(2,3) assms(1)[unfolded AI_def]])
(simp_all add: mono_step'_top)
end
lemma finite_avars[simp]: "finite(vars(a::aexp))"
by(induction a) simp_all
lemma finite_bvars[simp]: "finite(vars(b::bexp))"
by(induction b) simp_all
lemma finite_lvars[simp]: "finite(lvars(c))"
by(induction c) simp_all
lemma finite_rvars[simp]: "finite(rvars(c))"
by(induction c) simp_all
lemma finite_cvars[simp]: "finite(vars(c::com))"
by(simp add: vars_com_def)
instantiation acom :: (type) vars
begin
definition "vars_acom = vars o strip"
instance ..
end
lemma finite_Cvars: "finite(vars(C::'a acom))"
by(simp add: vars_acom_def)
subsubsection "Termination"
lemma pfp_termination:
fixes x0 :: "'a::order" and m :: "'a \<Rightarrow> nat"
assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x < y \<Longrightarrow> m x > m y"
and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<le> f x0"
shows "\<exists>x. pfp f x0 = Some x"
proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<le> f x"])
show "wf {(y,x). ((I x \<and> x \<le> f x) \<and> \<not> f x \<le> x) \<and> y = f x}"
by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
next
show "I x0 \<and> x0 \<le> f x0" using `I x0` `x0 \<le> f x0` by blast
next
fix x assume "I x \<and> x \<le> f x" thus "I(f x) \<and> f x \<le> f(f x)"
by (blast intro: I mono)
qed
lemma le_iff_le_annos: "C1 \<le> C2 \<longleftrightarrow>
strip C1 = strip C2 \<and> (\<forall>i < size(annos C1). annos C1 ! i \<le> annos C2 ! i)"
by(simp add: less_eq_acom_def anno_def)
locale Measure1_fun =
fixes m :: "'av::top \<Rightarrow> nat"
fixes h :: "nat"
assumes h: "m x \<le> h"
begin
definition m_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>s") where
"m_s S X = (\<Sum> x \<in> X. m(S x))"
lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
by(simp add: m_s_def) (metis mult.commute of_nat_id sum_bounded_above[OF h])
fun m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where
"m_o (Some S) X = m_s S X" |
"m_o None X = h * card X + 1"
lemma m_o_h: "finite X \<Longrightarrow> m_o opt X \<le> (h*card X + 1)"
by(cases opt)(auto simp add: m_s_h le_SucI dest: m_s_h)
definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^sub>c") where
"m_c C = sum_list (map (\<lambda>a. m_o a (vars C)) (annos C))"
text \<open>Upper complexity bound:\<close>
lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
proof-
let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
have "m_c C = (\<Sum>i<?a. m_o (annos C ! i) ?X)"
by(simp add: m_c_def sum_list_sum_nth atLeast0LessThan)
also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
apply(rule sum_mono) using m_o_h[OF finite_Cvars] by simp
also have "\<dots> = ?a * (h * ?n + 1)" by simp
finally show ?thesis .
qed
end
abbreviation
eq_on :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool"
("(_ =/ _/ on _)" [50,0,50] 50) where
"f = g on X == \<forall> x \<in> X. f x = g x"
locale Measure_fun = Measure1_fun where m=m
for m :: "'av::semilattice_sup_top \<Rightarrow> nat" +
assumes m2: "x < y \<Longrightarrow> m x > m y"
begin
text \<open>
The predicates @{text "top_on_ty a X"} that follow describe that any abstract
state in @{text a} maps all variables in @{text X} to @{term \<top>}.
This is an important invariant for the termination proof where we argue that only
the finitely many variables in the program change. That the others do not change
follows because they remain @{term \<top>}.
\<close>
fun top_on_st :: "'av st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^sub>s") where
"top_on_st S X = (\<forall>x\<in>X. S x = \<top>)"
fun top_on_opt :: "'av st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^sub>o") where
"top_on_opt (Some S) X = top_on_st S X" |
"top_on_opt None X = True"
definition top_on_acom :: "'av st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^sub>c") where
"top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)"
lemma top_on_top: "top_on_opt \<top> X"
by(auto simp: top_option_def)
lemma top_on_bot: "top_on_acom (bot c) X"
by(auto simp add: top_on_acom_def bot_def)
lemma top_on_post: "top_on_acom C X \<Longrightarrow> top_on_opt (post C) X"
by(simp add: top_on_acom_def post_in_annos)
lemma top_on_acom_simps:
"top_on_acom (SKIP {Q}) X = top_on_opt Q X"
"top_on_acom (x ::= e {Q}) X = top_on_opt Q X"
"top_on_acom (C1;;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
"top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X =
(top_on_opt P1 X \<and> top_on_acom C1 X \<and> top_on_opt P2 X \<and> top_on_acom C2 X \<and> top_on_opt Q X)"
"top_on_acom ({I} WHILE b DO {P} C {Q}) X =
(top_on_opt I X \<and> top_on_acom C X \<and> top_on_opt P X \<and> top_on_opt Q X)"
by(auto simp add: top_on_acom_def)
lemma top_on_sup:
"top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<squnion> o2) X"
apply(induction o1 o2 rule: sup_option.induct)
apply(auto)
done
lemma top_on_Step: fixes C :: "'av st option acom"
assumes "!!x e S. \<lbrakk>top_on_opt S X; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt (f x e S) X"
"!!b S. top_on_opt S X \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt (g b S) X"
shows "\<lbrakk> vars C \<subseteq> -X; top_on_opt S X; top_on_acom C X \<rbrakk> \<Longrightarrow> top_on_acom (Step f g S C) X"
proof(induction C arbitrary: S)
qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)
lemma m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
by(auto simp: le_less m2)
lemma m_s2_rep: assumes "finite(X)" and "S1 = S2 on -X" and "\<forall>x. S1 x \<le> S2 x" and "S1 \<noteq> S2"
shows "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))"
proof-
from assms(3) have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S2 x)" by (simp add: m1)
from assms(2,3,4) have "EX x:X. S1 x < S2 x"
by(simp add: fun_eq_iff) (metis Compl_iff le_neq_trans)
hence 2: "\<exists>x\<in>X. m(S1 x) > m(S2 x)" by (metis m2)
from sum_strict_mono_ex1[OF `finite X` 1 2]
show "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))" .
qed
lemma m_s2: "finite(X) \<Longrightarrow> S1 = S2 on -X \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s S1 X > m_s S2 X"
apply(auto simp add: less_fun_def m_s_def)
apply(simp add: m_s2_rep le_fun_def)
done
lemma m_o2: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
o1 < o2 \<Longrightarrow> m_o o1 X > m_o o2 X"
proof(induction o1 o2 rule: less_eq_option.induct)
case 1 thus ?case by (auto simp: m_s2 less_option_def)
next
case 2 thus ?case by(auto simp: less_option_def le_imp_less_Suc m_s_h)
next
case 3 thus ?case by (auto simp: less_option_def)
qed
lemma m_o1: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
o1 \<le> o2 \<Longrightarrow> m_o o1 X \<ge> m_o o2 X"
by(auto simp: le_less m_o2)
lemma m_c2: "top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2) \<Longrightarrow>
C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
proof(auto simp add: le_iff_le_annos size_annos_same[of C1 C2] vars_acom_def less_acom_def)
let ?X = "vars(strip C2)"
assume top: "top_on_acom C1 (- vars(strip C2))" "top_on_acom C2 (- vars(strip C2))"
and strip_eq: "strip C1 = strip C2"
and 0: "\<forall>i < size(annos C2). annos C1 ! i \<le> annos C2 ! i"
hence 1: "\<forall>i < size(annos C2). m_o (annos C1 ! i) ?X \<ge> m_o (annos C2 ! i) ?X"
apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
by (metis (lifting, no_types) finite_cvars m_o1 size_annos_same2)
fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
have topo1: "top_on_opt (annos C1 ! i) (- ?X)"
using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
have topo2: "top_on_opt (annos C2 ! i) (- ?X)"
using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
from i have "m_o (annos C1 ! i) ?X > m_o (annos C2 ! i) ?X" (is "?P i")
by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
have "(\<Sum>i < size(annos C2). m_o (annos C2 ! i) ?X)
< (\<Sum>i < size(annos C2). m_o (annos C1 ! i) ?X)"
apply(rule sum_strict_mono_ex1) using 1 2 by (auto)
thus ?thesis
by(simp add: m_c_def vars_acom_def strip_eq sum_list_sum_nth atLeast0LessThan size_annos_same[OF strip_eq])
qed
end
locale Abs_Int_fun_measure =
Abs_Int_fun_mono where \<gamma>=\<gamma> + Measure_fun where m=m
for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
begin
lemma top_on_step': "top_on_acom C (-vars C) \<Longrightarrow> top_on_acom (step' \<top> C) (-vars C)"
unfolding step'_def
by(rule top_on_Step)
(auto simp add: top_option_def asem_def split: option.splits)
lemma AI_Some_measure: "\<exists>C. AI c = Some C"
unfolding AI_def
apply(rule pfp_termination[where I = "\<lambda>C. top_on_acom C (- vars C)" and m="m_c"])
apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
using top_on_step' apply(auto simp add: vars_acom_def)
done
end
type_synonym 'a st_rep = "(vname * 'a) list"
fun fun_rep :: "('a::top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
"fun_rep [] = (\<lambda>x. \<top>)" |
"fun_rep ((x,a)#ps) = (fun_rep ps) (x := a)"
lemma fun_rep_map_of[code]: \<comment> \<open>original def is too slow\<close>
"fun_rep ps = (%x. case map_of ps x of None \<Rightarrow> \<top> | Some a \<Rightarrow> a)"
by(induction ps rule: fun_rep.induct) auto
definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
"eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
hide_type st \<comment> \<open>hide previous def to avoid long names\<close>
declare [[typedef_overloaded]] \<comment> \<open>allow quotient types to depend on classes\<close>
quotient_type 'a st' = "('a::top) st_rep" / eq_st
morphisms rep_st St
by (metis eq_st_def equivpI reflpI sympI transpI)
lift_definition update :: "('a::top) st' \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st'"
is "\<lambda>ps x a. (x,a)#ps"
by(auto simp: eq_st_def)
lift_definition "fun" :: "('a::top) st' \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
by(simp add: eq_st_def)
definition show_st :: "vname set \<Rightarrow> ('a::top) st' \<Rightarrow> (vname * 'a)set" where
"show_st X S = (\<lambda>x. (x, fun S x)) ` X"
definition "show_acom C = map_acom (map_option (show_st (vars(strip C)))) C"
definition "show_acom_opt = map_option show_acom"
lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
by transfer auto
definition \<gamma>_st :: "(('a::top) \<Rightarrow> 'b set) \<Rightarrow> 'a st' \<Rightarrow> (vname \<Rightarrow> 'b) set" where
"\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(fun F x)}"
instantiation st' :: (order_top) order
begin
definition less_eq_st_rep :: "'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
"less_eq_st_rep ps1 ps2 =
((\<forall>x \<in> set(map fst ps1) \<union> set(map fst ps2). fun_rep ps1 x \<le> fun_rep ps2 x))"
lemma less_eq_st_rep_iff:
"less_eq_st_rep r1 r2 = (\<forall>x. fun_rep r1 x \<le> fun_rep r2 x)"
apply(auto simp: less_eq_st_rep_def fun_rep_map_of split: option.split)
apply (metis Un_iff map_of_eq_None_iff option.distinct(1))
apply (metis Un_iff map_of_eq_None_iff option.distinct(1))
done
corollary less_eq_st_rep_iff_fun:
"less_eq_st_rep r1 r2 = (fun_rep r1 \<le> fun_rep r2)"
by (metis less_eq_st_rep_iff le_fun_def)
lift_definition less_eq_st' :: "'a st' \<Rightarrow> 'a st' \<Rightarrow> bool" is less_eq_st_rep
by(auto simp add: eq_st_def less_eq_st_rep_iff)
definition less_st' where "F < (G::'a st') = (F \<le> G \<and> \<not> G \<le> F)"
instance
proof (standard, goal_cases)
case 1 show ?case by(rule less_st'_def)
next
case 2 show ?case by transfer (auto simp: less_eq_st_rep_def)
next
case 3 thus ?case by transfer (metis less_eq_st_rep_iff order_trans)
next
case 4 thus ?case
by transfer (metis less_eq_st_rep_iff eq_st_def fun_eq_iff antisym)
qed
end
lemma le_st_iff: "(F \<le> G) = (\<forall>x. fun F x \<le> fun G x)"
by transfer (rule less_eq_st_rep_iff)
fun map2_st_rep :: "('a::top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
"map2_st_rep f [] ps2 = map (%(x,y). (x, f \<top> y)) ps2" |
"map2_st_rep f ((x,y)#ps1) ps2 =
(let y2 = fun_rep ps2 x
in (x,f y y2) # map2_st_rep f ps1 ps2)"
lemma fun_rep_map2_rep[simp]: "f \<top> \<top> = \<top> \<Longrightarrow>
fun_rep (map2_st_rep f ps1 ps2) = (\<lambda>x. f (fun_rep ps1 x) (fun_rep ps2 x))"
apply(induction f ps1 ps2 rule: map2_st_rep.induct)
apply(simp add: fun_rep_map_of map_of_map fun_eq_iff split: option.split)
apply(fastforce simp: fun_rep_map_of fun_eq_iff split:option.splits)
done
instantiation st' :: (semilattice_sup_top) semilattice_sup_top
begin
lift_definition sup_st' :: "'a st' \<Rightarrow> 'a st' \<Rightarrow> 'a st'" is "map2_st_rep (\<squnion>)"
by (simp add: eq_st_def)
lift_definition top_st' :: "'a st'" is "[]" .
instance
proof (standard, goal_cases)
case 1 show ?case by transfer (simp add:less_eq_st_rep_iff)
next
case 2 show ?case by transfer (simp add:less_eq_st_rep_iff)
next
case 3 thus ?case by transfer (simp add:less_eq_st_rep_iff)
next
case 4 show ?case by transfer (simp add:less_eq_st_rep_iff fun_rep_map_of)
qed
end
lemma fun_top: "fun \<top> = (\<lambda>x. \<top>)"
by transfer simp
lemma mono_update[simp]:
"a1 \<le> a2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> update S1 x a1 \<le> update S2 x a2"
by transfer (auto simp add: less_eq_st_rep_def)
lemma mono_fun: "S1 \<le> S2 \<Longrightarrow> fun S1 x \<le> fun S2 x"
by transfer (simp add: less_eq_st_rep_iff)
locale Gamma_semilattice = Val_semilattice where \<gamma>=\<gamma>
for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin
abbreviation \<gamma>\<^sub>s :: "'av st' \<Rightarrow> state set"
where "\<gamma>\<^sub>s == \<gamma>_st \<gamma>"
abbreviation \<gamma>\<^sub>o :: "'av st' option \<Rightarrow> state set"
where "\<gamma>\<^sub>o == \<gamma>_option \<gamma>\<^sub>s"
abbreviation \<gamma>\<^sub>c :: "'av st' option acom \<Rightarrow> state set acom"
where "\<gamma>\<^sub>c == map_acom \<gamma>\<^sub>o"
lemma gamma_s_top[simp]: "\<gamma>\<^sub>s \<top> = UNIV"
by(auto simp: \<gamma>_st_def fun_top)
lemma gamma_o_Top[simp]: "\<gamma>\<^sub>o \<top> = UNIV"
by (simp add: top_option_def)
lemma mono_gamma_s: "f \<le> g \<Longrightarrow> \<gamma>\<^sub>s f \<subseteq> \<gamma>\<^sub>s g"
by(simp add:\<gamma>_st_def le_st_iff subset_iff) (metis mono_gamma subsetD)
lemma mono_gamma_o:
"S1 \<le> S2 \<Longrightarrow> \<gamma>\<^sub>o S1 \<subseteq> \<gamma>\<^sub>o S2"
by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^sub>c C1 \<le> \<gamma>\<^sub>c C2"
by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])
lemma in_gamma_option_iff:
"x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"
by (cases u) auto
end
text \<open>Abstract interpretation over type @{text st} instead of functions.\<close>
context Gamma_semilattice
begin
fun aval' :: "aexp \<Rightarrow> 'av st' \<Rightarrow> 'av" where
"aval' (N i) S = num' i" |
"aval' (V x) S = fun S x" |
"aval' (Bit_And a1 a2) S = and' (aval' a1 S) (aval' a2 S)" |
"aval' (Bit_Or a1 a2) S = or' (aval' a1 S) (aval' a2 S)"
lemma aval'_correct: "s : \<gamma>\<^sub>s S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
by (induction a) (auto simp: gamma_num' gamma_and' gamma_or' \<gamma>_st_def)
lemma gamma_Step_subcomm: fixes C1 C2 :: "'a::semilattice_sup acom"
assumes "!!x e S. f1 x e (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (f2 x e S)"
"!!b S. g1 b (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (g2 b S)"
shows "Step f1 g1 (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (Step f2 g2 S C)"
proof(induction C arbitrary: S)
qed (auto simp: assms intro!: mono_gamma_o sup_ge1 sup_ge2)
lemma in_gamma_update: "\<lbrakk> s : \<gamma>\<^sub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^sub>s(update S x a)"
by(simp add: \<gamma>_st_def)
end
locale Abs_Int = Gamma_semilattice where \<gamma>=\<gamma>
for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set"
begin
definition "step' = Step
(\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S)))
(\<lambda>b S. S)"
definition AI :: "com \<Rightarrow> 'av st' option acom option" where
"AI c = pfp (step' \<top>) (bot c)"
lemma strip_step'[simp]: "strip(step' S C) = strip C"
by(simp add: step'_def)
text \<open>Correctness:\<close>
lemma step_step': "step (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' S C)"
unfolding step_def step'_def
by(rule gamma_Step_subcomm)
(auto simp: intro!: aval'_correct in_gamma_update split: option.splits)
lemma AI_correct: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c C"
proof(simp add: CS_def AI_def)
assume 1: "pfp (step' \<top>) (bot c) = Some C"
have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
have 2: "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c C" \<comment> \<open>transfer the pfp'\<close>
proof(rule order_trans)
show "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' \<top> C)" by(rule step_step')
show "... \<le> \<gamma>\<^sub>c C" by (metis mono_gamma_c[OF pfp'])
qed
have 3: "strip (\<gamma>\<^sub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
have "lfp c (step (\<gamma>\<^sub>o \<top>)) \<le> \<gamma>\<^sub>c C"
by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^sub>o \<top>)", OF 3 2])
thus "lfp c (step UNIV) \<le> \<gamma>\<^sub>c C" by simp
qed
end
subsubsection "Monotonicity"
locale Abs_Int_mono = Abs_Int +
assumes mono_and': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> and' a1 a2 \<le> and' b1 b2"
and mono_or': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> or' a1 a2 \<le> or' b1 b2"
begin
lemma mono_aval': "S1 \<le> S2 \<Longrightarrow> aval' e S1 \<le> aval' e S2"
by(induction e) (auto simp: mono_and' mono_or' mono_fun)
theorem mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
unfolding step'_def
by(rule mono2_Step) (auto simp: mono_aval' split: option.split)
lemma mono_step'_top: "C \<le> C' \<Longrightarrow> step' \<top> C \<le> step' \<top> C'"
by (metis mono_step' order_refl)
lemma AI_least_pfp: assumes "AI c = Some C" "step' \<top> C' \<le> C'" "strip C' = c"
shows "C \<le> C'"
by(rule pfp_bot_least[OF _ _ assms(2,3) assms(1)[unfolded AI_def]])
(simp_all add: mono_step'_top)
end
subsubsection "Termination"
locale Measure1 =
fixes m :: "'av::order_top \<Rightarrow> nat"
fixes h :: "nat"
assumes h: "m x \<le> h"
begin
definition m_s :: "'av st' \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>s") where
"m_s S X = (\<Sum> x \<in> X. m(fun S x))"
lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
by(simp add: m_s_def) (metis mult.commute of_nat_id sum_bounded_above[OF h])
definition m_o :: "'av st' option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where
"m_o opt X = (case opt of None \<Rightarrow> h * card X + 1 | Some S \<Rightarrow> m_s S X)"
lemma m_o_h: "finite X \<Longrightarrow> m_o opt X \<le> (h*card X + 1)"
by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)
definition m_c :: "'av st' option acom \<Rightarrow> nat" ("m\<^sub>c") where
"m_c C = sum_list (map (\<lambda>a. m_o a (vars C)) (annos C))"
text \<open>Upper complexity bound:\<close>
lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
proof-
let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
have "m_c C = (\<Sum>i<?a. m_o (annos C ! i) ?X)"
by(simp add: m_c_def sum_list_sum_nth atLeast0LessThan)
also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
apply(rule sum_mono) using m_o_h[OF finite_Cvars] by simp
also have "\<dots> = ?a * (h * ?n + 1)" by simp
finally show ?thesis .
qed
end
fun top_on_st :: "'a::order_top st' \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^sub>s") where
"top_on_st S X = (\<forall>x\<in>X. fun S x = \<top>)"
fun top_on_opt :: "'a::order_top st' option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^sub>o") where
"top_on_opt (Some S) X = top_on_st S X" |
"top_on_opt None X = True"
definition top_on_acom :: "'a::order_top st' option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^sub>c") where
"top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)"
lemma top_on_top: "top_on_opt (\<top>::_ st' option) X"
by(auto simp: top_option_def fun_top)
lemma top_on_bot: "top_on_acom (bot c) X"
by(auto simp add: top_on_acom_def bot_def)
lemma top_on_post: "top_on_acom C X \<Longrightarrow> top_on_opt (post C) X"
by(simp add: top_on_acom_def post_in_annos)
lemma top_on_acom_simps:
"top_on_acom (SKIP {Q}) X = top_on_opt Q X"
"top_on_acom (x ::= e {Q}) X = top_on_opt Q X"
"top_on_acom (C1;;C2) X = (top_on_acom C1 X \<and> top_on_acom C2 X)"
"top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X =
(top_on_opt P1 X \<and> top_on_acom C1 X \<and> top_on_opt P2 X \<and> top_on_acom C2 X \<and> top_on_opt Q X)"
"top_on_acom ({I} WHILE b DO {P} C {Q}) X =
(top_on_opt I X \<and> top_on_acom C X \<and> top_on_opt P X \<and> top_on_opt Q X)"
by(auto simp add: top_on_acom_def)
lemma top_on_sup:
"top_on_opt o1 X \<Longrightarrow> top_on_opt o2 X \<Longrightarrow> top_on_opt (o1 \<squnion> o2 :: _ st' option) X"
apply(induction o1 o2 rule: sup_option.induct)
apply(auto)
by transfer simp
lemma top_on_Step: fixes C :: "('a::semilattice_sup_top)st' option acom"
assumes "!!x e S. \<lbrakk>top_on_opt S X; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt (f x e S) X"
"!!b S. top_on_opt S X \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt (g b S) X"
shows "\<lbrakk> vars C \<subseteq> -X; top_on_opt S X; top_on_acom C X \<rbrakk> \<Longrightarrow> top_on_acom (Step f g S C) X"
proof(induction C arbitrary: S)
qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)
locale Measure = Measure1 +
assumes m2: "x < y \<Longrightarrow> m x > m y"
begin
lemma m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
by(auto simp: le_less m2)
lemma m_s2_rep: assumes "finite(X)" and "S1 = S2 on -X" and "\<forall>x. S1 x \<le> S2 x" and "S1 \<noteq> S2"
shows "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))"
proof-
from assms(3) have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S2 x)" by (simp add: m1)
from assms(2,3,4) have "EX x:X. S1 x < S2 x"
by(simp add: fun_eq_iff) (metis Compl_iff le_neq_trans)
hence 2: "\<exists>x\<in>X. m(S1 x) > m(S2 x)" by (metis m2)
from sum_strict_mono_ex1[OF `finite X` 1 2]
show "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))" .
qed
lemma m_s2: "finite(X) \<Longrightarrow> fun S1 = fun S2 on -X
\<Longrightarrow> S1 < S2 \<Longrightarrow> m_s S1 X > m_s S2 X"
apply(auto simp add: less_st'_def m_s_def)
apply (transfer fixing: m)
apply(simp add: less_eq_st_rep_iff eq_st_def m_s2_rep)
done
lemma m_o2: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
o1 < o2 \<Longrightarrow> m_o o1 X > m_o o2 X"
proof(induction o1 o2 rule: less_eq_option.induct)
case 1 thus ?case by (auto simp: m_o_def m_s2 less_option_def)
next
case 2 thus ?case by(auto simp: m_o_def less_option_def le_imp_less_Suc m_s_h)
next
case 3 thus ?case by (auto simp: less_option_def)
qed
lemma m_o1: "finite X \<Longrightarrow> top_on_opt o1 (-X) \<Longrightarrow> top_on_opt o2 (-X) \<Longrightarrow>
o1 \<le> o2 \<Longrightarrow> m_o o1 X \<ge> m_o o2 X"
by(auto simp: le_less m_o2)
lemma m_c2: "top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2) \<Longrightarrow>
C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
proof(auto simp add: le_iff_le_annos size_annos_same[of C1 C2] vars_acom_def less_acom_def)
let ?X = "vars(strip C2)"
assume top: "top_on_acom C1 (- vars(strip C2))" "top_on_acom C2 (- vars(strip C2))"
and strip_eq: "strip C1 = strip C2"
and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
hence 1: "\<forall>i<size(annos C2). m_o (annos C1 ! i) ?X \<ge> m_o (annos C2 ! i) ?X"
apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
by (metis (no_types, hide_lams) finite_cvars m_o1 size_annos_same)
fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
have topo1: "top_on_opt (annos C1 ! i) (- ?X)"
using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
have topo2: "top_on_opt (annos C2 ! i) (- ?X)"
using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
from i have "m_o (annos C1 ! i) ?X > m_o (annos C2 ! i) ?X" (is "?P i")
by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
have "(\<Sum>i<size(annos C2). m_o (annos C2 ! i) ?X)
< (\<Sum>i<size(annos C2). m_o (annos C1 ! i) ?X)"
apply(rule sum_strict_mono_ex1) using 1 2 by (auto)
thus ?thesis
by(simp add: m_c_def vars_acom_def strip_eq sum_list_sum_nth atLeast0LessThan size_annos_same[OF strip_eq])
qed
end
locale Abs_Int_measure =
Abs_Int_mono where \<gamma>=\<gamma> + Measure where m=m
for \<gamma> :: "'av::semilattice_sup_top \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
begin
lemma top_on_step': "\<lbrakk> top_on_acom C (-vars C) \<rbrakk> \<Longrightarrow> top_on_acom (step' \<top> C) (-vars C)"
unfolding step'_def
by(rule top_on_Step)
(auto simp add: top_option_def fun_top split: option.splits)
lemma AI_Some_measure: "\<exists>C. AI c = Some C"
unfolding AI_def
apply(rule pfp_termination[where I = "\<lambda>C. top_on_acom C (- vars C)" and m="m_c"])
apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
using top_on_step' apply(auto simp add: vars_acom_def)
done
end
instantiation prod :: (order,order) order
begin
definition "less_eq_prod p1 p2 = (fst p1 \<le> fst p2 \<and> snd p1 \<le> snd p2)"
definition "less_prod p1 p2 = (p1 \<le> p2 \<and> \<not> p2 \<le> (p1::'a*'b))"
instance
proof (standard, goal_cases)
case 1 show ?case by(rule less_prod_def)
next
case 2 show ?case by(simp add: less_eq_prod_def)
next
case 3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
next
case 4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
qed
end
subsubsection "Extended Framework"
subclass (in bounded_lattice) semilattice_sup_top ..
locale Val_lattice_gamma = Gamma_semilattice where \<gamma> = \<gamma>
for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
assumes inter_gamma_subset_gamma_inf:
"\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
and gamma_bot[simp]: "\<gamma> \<bottom> = {}"
begin
lemma in_gamma_inf: "x \<in> \<gamma> a1 \<Longrightarrow> x \<in> \<gamma> a2 \<Longrightarrow> x \<in> \<gamma>(a1 \<sqinter> a2)"
by (metis IntI inter_gamma_subset_gamma_inf subsetD)
lemma gamma_inf: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
(metis inf_le1 inf_le2 le_inf_iff mono_gamma)
end
locale Val_inv = Val_lattice_gamma where \<gamma> = \<gamma>
for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
and inv_and' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
and inv_or' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
and inv_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
assumes test_num': "test_num' i a = (i \<in> \<gamma> a)"
and inv_and': "inv_and' a a1 a2 = (a\<^sub>1',a\<^sub>2') \<Longrightarrow>
i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1 AND i2 \<in> \<gamma> a \<Longrightarrow> i1 \<in> \<gamma> a\<^sub>1' \<and> i2 \<in> \<gamma> a\<^sub>2'"
and inv_or': "inv_or' a a1 a2 = (a\<^sub>1',a\<^sub>2') \<Longrightarrow>
i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1 OR i2 \<in> \<gamma> a \<Longrightarrow> i1 \<in> \<gamma> a\<^sub>1' \<and> i2 \<in> \<gamma> a\<^sub>2'"
and inv_less': "inv_less' (i1<i2) a1 a2 = (a\<^sub>1',a\<^sub>2') \<Longrightarrow>
i1 \<in> \<gamma> a1 \<Longrightarrow> i2 \<in> \<gamma> a2 \<Longrightarrow> i1 \<in> \<gamma> a\<^sub>1' \<and> i2 \<in> \<gamma> a\<^sub>2'"
locale Abs_Int_inv = Val_inv where \<gamma> = \<gamma>
for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set"
begin
lemma in_gamma_sup_UpI:
"s \<in> \<gamma>\<^sub>o S1 \<or> s \<in> \<gamma>\<^sub>o S2 \<Longrightarrow> s \<in> \<gamma>\<^sub>o(S1 \<squnion> S2)"
by (metis (hide_lams, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)
fun aval'' :: "aexp \<Rightarrow> 'av st' option \<Rightarrow> 'av" where
"aval'' e None = \<bottom>" |
"aval'' e (Some S) = aval' e S"
lemma aval''_correct: "s \<in> \<gamma>\<^sub>o S \<Longrightarrow> aval a s \<in> \<gamma>(aval'' a S)"
by(cases S)(auto simp add: aval'_correct split: option.splits)
subsubsection "Backward analysis"
fun inv_aval' :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st' option \<Rightarrow> 'av st' option" where
"inv_aval' (N n) a S = (if test_num' n a then S else None)" |
"inv_aval' (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
let a' = fun S x \<sqinter> a in
if a' = \<bottom> then None else Some(update S x a'))" |
"inv_aval' (Bit_And e1 e2) a S =
(let (a1,a2) = inv_and' a (aval'' e1 S) (aval'' e2 S)
in inv_aval' e1 a1 (inv_aval' e2 a2 S))" |
"inv_aval' (Bit_Or e1 e2) a S =
(let (a1,a2) = inv_or' a (aval'' e1 S) (aval'' e2 S)
in inv_aval' e1 a1 (inv_aval' e2 a2 S))"
text\<open>The test for \<^const>\<open>bot\<close> in the \<^const>\<open>V\<close>-case is important: \<^const>\<open>bot\<close> indicates that a variable has no possible values, i.e.\ that the current
program point is unreachable. But then the abstract state should collapse to
\<^const>\<open>None\<close>. Put differently, we maintain the invariant that in an abstract
state of the form \<^term>\<open>Some s\<close>, all variables are mapped to non-\<^const>\<open>bot\<close> values. Otherwise the (pointwise) sup of two abstract states, one of
which contains \<^const>\<open>bot\<close> values, may produce too large a result, thus
making the analysis less precise.\<close>
fun inv_bval' :: "bexp \<Rightarrow> bool \<Rightarrow> 'av st' option \<Rightarrow> 'av st' option" where
"inv_bval' (Bc v) res S = (if v=res then S else None)" |
"inv_bval' (Not b) res S = inv_bval' b (\<not> res) S" |
"inv_bval' (And b1 b2) res S =
(if res then inv_bval' b1 True (inv_bval' b2 True S)
else inv_bval' b1 False S \<squnion> inv_bval' b2 False S)" |
"inv_bval' (Less e1 e2) res S =
(let (a1,a2) = inv_less' res (aval'' e1 S) (aval'' e2 S)
in inv_aval' e1 a1 (inv_aval' e2 a2 S))"
lemma inv_aval'_correct: "s \<in> \<gamma>\<^sub>o S \<Longrightarrow> aval e s \<in> \<gamma> a \<Longrightarrow> s \<in> \<gamma>\<^sub>o (inv_aval' e a S)"
proof(induction e arbitrary: a S)
case N thus ?case by simp (metis test_num')
next
case (V x)
obtain S' where "S = Some S'" and "s \<in> \<gamma>\<^sub>s S'" using \<open>s \<in> \<gamma>\<^sub>o S\<close>
by(auto simp: in_gamma_option_iff)
moreover hence "s x \<in> \<gamma> (fun S' x)"
by(simp add: \<gamma>_st_def)
moreover have "s x \<in> \<gamma> a" using V(2) by simp
ultimately show ?case
by(simp add: Let_def \<gamma>_st_def)
(metis mono_gamma emptyE in_gamma_inf gamma_bot subset_empty)
next
case (Bit_And e1 e2) thus ?case
using inv_and'[OF _ aval''_correct aval''_correct]
by (auto split: prod.split)
next
case (Bit_Or e1 e2) thus ?case
thm inv_or'[OF _ aval''_correct aval''_correct]
using inv_or'[OF _ aval''_correct aval''_correct]
by (auto split: prod.split)
qed
lemma inv_bval'_correct: "s \<in> \<gamma>\<^sub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s \<in> \<gamma>\<^sub>o(inv_bval' b bv S)"
proof(induction b arbitrary: S bv)
case Bc thus ?case by simp
next
case (Not b) thus ?case by simp
next
case (And b1 b2) thus ?case
by simp (metis And(1) And(2) in_gamma_sup_UpI)
next
case (Less e1 e2) thus ?case
apply hypsubst_thin
apply (auto split: prod.split)
apply (metis (lifting) inv_aval'_correct aval''_correct inv_less')
done
qed
definition "step'' = Step
(\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S)))
(\<lambda>b S. inv_bval' b True S)"
definition AI' :: "com \<Rightarrow> 'av st' option acom option" where
"AI' c = pfp (step'' \<top>) (bot c)"
lemma strip_step''[simp]: "strip(step'' S c) = strip c"
by(simp add: step''_def)
lemma top_on_inv_aval': "\<lbrakk> top_on_opt S X; vars e \<subseteq> -X \<rbrakk> \<Longrightarrow> top_on_opt (inv_aval' e a S) X"
by(induction e arbitrary: a S) (auto simp: Let_def split: option.splits prod.split)
lemma top_on_inv_bval': "\<lbrakk>top_on_opt S X; vars b \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt (inv_bval' b r S) X"
by(induction b arbitrary: r S) (auto simp: top_on_inv_aval' top_on_sup split: prod.split)
lemma top_on_step': "top_on_acom C (- vars C) \<Longrightarrow> top_on_acom (step'' \<top> C) (- vars C)"
unfolding step''_def
by(rule top_on_Step)
(auto simp add: top_on_top top_on_inv_bval' split: option.split)
subsubsection "Correctness"
lemma step_step'': "step (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step'' S C)"
unfolding step_def step''_def
by(rule gamma_Step_subcomm)
(auto simp: intro!: aval'_correct inv_bval'_correct in_gamma_update split: option.splits)
lemma AI_correct': "AI' c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c C"
proof(simp add: CS_def AI'_def)
assume 1: "pfp (step'' \<top>) (bot c) = Some C"
have pfp': "step'' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
have 2: "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c C" \<comment> \<open>transfer the pfp'\<close>
proof(rule order_trans)
show "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step'' \<top> C)" by(rule step_step'')
show "... \<le> \<gamma>\<^sub>c C" by (metis mono_gamma_c[OF pfp'])
qed
have 3: "strip (\<gamma>\<^sub>c C) = c" by(simp add: strip_pfp[OF _ 1] step''_def)
have "lfp c (step (\<gamma>\<^sub>o \<top>)) \<le> \<gamma>\<^sub>c C"
by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^sub>o \<top>)", OF 3 2])
thus "lfp c (step UNIV) \<le> \<gamma>\<^sub>c C" by simp
qed
end
subsubsection "Monotonicity"
locale Abs_Int_inv_mono = Abs_Int_inv +
assumes mono_and': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> and' a1 a2 \<le> and' b1 b2"
and mono_inv_and': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> r \<le> r' \<Longrightarrow>
inv_and' r a1 a2 \<le> inv_and' r' b1 b2"
assumes mono_or': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> or' a1 a2 \<le> or' b1 b2"
and mono_inv_or': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> r \<le> r' \<Longrightarrow>
inv_or' r a1 a2 \<le> inv_or' r' b1 b2"
and mono_inv_less': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow>
inv_less' bv a1 a2 \<le> inv_less' bv b1 b2"
begin
lemma mono_aval':
"S1 \<le> S2 \<Longrightarrow> aval' e S1 \<le> aval' e S2"
by(induction e) (auto simp: mono_and' mono_or' mono_fun)
lemma mono_aval'':
"S1 \<le> S2 \<Longrightarrow> aval'' e S1 \<le> aval'' e S2"
apply(cases S1)
apply simp
apply(cases S2)
apply simp
by (simp add: mono_aval')
lemma mono_inv_aval': "r1 \<le> r2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> inv_aval' e r1 S1 \<le> inv_aval' e r2 S2"
apply(induction e arbitrary: r1 r2 S1 S2)
apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
apply (metis mono_gamma subsetD)
apply (metis le_bot inf_mono le_st_iff)
apply (metis inf_mono mono_update le_st_iff)
apply(metis mono_aval'' mono_inv_and'[simplified less_eq_prod_def] fst_conv snd_conv)
apply(metis mono_aval'' mono_inv_or'[simplified less_eq_prod_def] fst_conv snd_conv)
done
lemma mono_inv_bval': "S1 \<le> S2 \<Longrightarrow> inv_bval' b bv S1 \<le> inv_bval' b bv S2"
apply(induction b arbitrary: bv S1 S2)
apply(simp)
apply(simp)
apply simp
apply(metis order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2])
apply (simp split: prod.splits)
apply(metis mono_aval'' mono_inv_aval' mono_inv_less'[simplified less_eq_prod_def] fst_conv snd_conv)
done
theorem mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step'' S1 C1 \<le> step'' S2 C2"
unfolding step''_def
by(rule mono2_Step) (auto simp: mono_aval' mono_inv_bval' split: option.split)
lemma mono_step'_top: "C1 \<le> C2 \<Longrightarrow> step'' \<top> C1 \<le> step'' \<top> C2"
by (metis mono_step' order_refl)
end
instance word :: (semilattice_sup_top) semilattice_sup_top ..
end
theory Submission imports Defs begin
datatype parity = T | F | Either | None
fun \<gamma>_parity where
"\<gamma>_parity _ = undefined"
fun conj_parity where
"conj_parity _ = undefined"
fun disj_parity where
"disj_parity _ = undefined"
fun num_parity where
"num_parity _ = undefined"
instantiation parity :: "{order, semilattice_sup_top, bounded_lattice}"
begin
definition less_eq_parity :: "parity \<Rightarrow> parity \<Rightarrow> bool" where
"x \<le> (y::parity) = undefined"
definition less_parity :: "parity \<Rightarrow> parity \<Rightarrow> bool" where
"x < (y::parity) = undefined"
definition sup_parity :: "parity \<Rightarrow> parity \<Rightarrow> parity" where
"x \<squnion> (y::parity) = undefined"
definition inf_parity :: "parity \<Rightarrow> parity \<Rightarrow> parity" where
"x \<sqinter> (y::parity) = undefined"
definition top_parity :: "parity" where
"(\<top>::parity) = undefined"
definition bot_parity :: "parity" where
"(\<bottom>::parity) = undefined"
instance
sorry
end
type_synonym word_parity = "parity word"
fun \<gamma>_word_parity :: "word_parity \<Rightarrow> val set" where
"\<gamma>_word_parity _ = undefined"
definition and_parity :: "word_parity \<Rightarrow> word_parity \<Rightarrow> word_parity" where
"and_parity _ = undefined"
definition or_parity :: "word_parity \<Rightarrow> word_parity \<Rightarrow> word_parity" where
"or_parity _ = undefined"
definition num_word_parity :: "val \<Rightarrow> word_parity" where
"num_word_parity _ = undefined"
global_interpretation Val_semilattice
where \<gamma> = \<gamma>_word_parity and num' = num_word_parity and and' = and_parity and or' = or_parity
sorry
global_interpretation Abs_Int
where \<gamma> = \<gamma>_word_parity and num' = num_word_parity and and' = and_parity and or' = or_parity
defines step_parity = step' and AI_parity = AI
sorry
global_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_word_parity and num' = num_word_parity and and' = and_parity and or' = or_parity
sorry
global_interpretation Val_lattice_gamma
where \<gamma> = \<gamma>_word_parity and num' = num_word_parity and and' = and_parity and or' = or_parity
sorry
definition test_num_word_parity :: "val \<Rightarrow> word_parity \<Rightarrow> bool" where
"test_num_word_parity _ = undefined"
definition inv_and_word_parity ::
"word_parity \<Rightarrow> word_parity \<Rightarrow> word_parity \<Rightarrow> (word_parity \<times> word_parity)" where
"inv_and_word_parity _ = undefined"
definition inv_or_word_parity ::
"word_parity \<Rightarrow> word_parity \<Rightarrow> word_parity \<Rightarrow> (word_parity \<times> word_parity)" where
"inv_or_word_parity _ = undefined"
definition inv_less_word_parity ::
"bool \<Rightarrow> word_parity \<Rightarrow> word_parity \<Rightarrow> (word_parity \<times> word_parity)" where
"inv_less_word_parity _ = undefined"
global_interpretation Abs_Int_inv
where \<gamma> = \<gamma>_word_parity and num' = num_word_parity and and' = and_parity and or' = or_parity
and test_num' = test_num_word_parity and inv_and' = inv_and_word_parity
and inv_or' = inv_or_word_parity and inv_less' = inv_less_word_parity
defines step_parity' = step' and AI_parity' = AI'
sorry
end
theory Check imports Submission begin theorem Val_Semilattice: "Val_semilattice \<gamma>_word_parity num_word_parity and_parity or_parity" by (rule Submission.Val_semilattice_axioms) theorem Abs_Int: "Abs_Int num_word_parity and_parity or_parity \<gamma>_word_parity" by (rule Submission.Abs_Int_axioms) theorem Abs_Int_mono: "Abs_Int_mono num_word_parity and_parity or_parity \<gamma>_word_parity" by (rule Submission.Abs_Int_mono_axioms) theorem Val_lattice_gamma: "Val_lattice_gamma num_word_parity and_parity or_parity \<gamma>_word_parity" by (rule Submission.Val_lattice_gamma_axioms) theorem Abs_Int_inv: "Abs_Int_inv num_word_parity and_parity or_parity test_num_word_parity inv_and_word_parity inv_or_word_parity inv_less_word_parity \<gamma>_word_parity" by (rule Submission.Abs_Int_inv_axioms) end