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_Real"
"HOL-IMP.Complete_Lattice" begin
subsection "Arithmetic Expressions"
type_synonym vname = string
type_synonym val = "ereal option"
type_synonym state = "vname \<Rightarrow> val"
datatype aexp = N ereal | V vname | Plus aexp aexp
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where
"aval (N n) s = Some n" |
"aval (V x) s = s x" |
"aval (Plus a\<^sub>1 a\<^sub>2) s =
(
case (aval a\<^sub>1 s, aval a\<^sub>2 s) of
(None, _) \<Rightarrow> None
| (_, None) \<Rightarrow> None
| (Some PInfty, Some (MInfty)) \<Rightarrow> None
| (Some (MInfty), Some PInfty) \<Rightarrow> None
| (Some x, Some y) \<Rightarrow> Some (x + y)
)"
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"
subsection "Boolean Expressions"
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool option" where
"bval (Bc v) s = Some v" |
"bval (Not b) s = map_option (HOL.Not) (bval b s)" |
"bval (And b\<^sub>1 b\<^sub>2) s =
(case (bval b\<^sub>1 s, bval b\<^sub>2 s) of
(_, None) \<Rightarrow> None
| (None, _) \<Rightarrow> None
| (Some a, Some b) \<Rightarrow> Some (a \<and> b)
)
" |
"bval (Less a\<^sub>1 a\<^sub>2) s =
(
case (aval a\<^sub>1 s, aval a\<^sub>2 s) of
(_, None) \<Rightarrow> None
| (None, _) \<Rightarrow> None
| (Some a, Some b) \<Rightarrow> Some (a < b)
)
"
subsection \<open>Commands\<close>
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)
subsection "Big-Step Semantics of Commands"
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 = Some True; (c\<^sub>1,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
IfFalse: "\<lbrakk> bval b s = Some False; (c\<^sub>2,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t" |
WhileFalse: "bval b s = Some False \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s" |
WhileTrue:
"\<lbrakk> bval b s\<^sub>1 = Some True; (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"
code_pred big_step .
declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
subsection "Rule inversion"
inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
inductive_cases AssignE[elim!]: "(x ::= a,s) \<Rightarrow> t"
inductive_cases SeqE[elim!]: "(c1;;c2,s1) \<Rightarrow> s3"
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) \<Rightarrow> t"
inductive_cases WhileE[elim]: "(WHILE b DO c,s) \<Rightarrow> t"
subsection "Annotated Commands"
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> (\<exists>P. C = SKIP {P})"
by (cases C) simp_all
lemma strip_eq_Assign:
"strip C = x::=e \<longleftrightarrow> (\<exists>P. C = x::=e {P})"
by (cases C) simp_all
lemma strip_eq_Seq:
"strip C = c1;;c2 \<longleftrightarrow> (\<exists>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>
(\<exists>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>
(\<exists>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)
subsubsection "The generic Step function"
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
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 \<in> S}) (\<lambda>b S. {s:S. bval b s = Some True})"
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)
using subset_eq by blast
next
case IfFalse thus ?case apply(auto simp: strip_eq_If step_def post_def)
using subset_eq by blast
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 = Some True} \<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 = Some True} C' \<le> C'"
by (rule order_trans[OF mono2_step[OF order_refl `{s \<in> I. bval b s = Some True} \<le> P`] `step P C' \<le> C'`])
have "s1: {s:I. bval b s = Some True}" using `s1 \<in> S` `S \<subseteq> I` `bval b s1 = Some True` by auto
note s2_in_post_C' = WhileTrue.IH(1)[OF `strip C' = c'` this `step {s \<in> I. bval b s = Some True} 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 \<in> post(CS c)"
by(simp add: CS_def big_step_lfp)
hide_const (open) top bot dom
subsection "The Variables in an Expression"
class vars =
fixes vars :: "'a \<Rightarrow> vname set"
instantiation aexp :: vars
begin
fun vars_aexp :: "aexp \<Rightarrow> vname set" where
"vars (N n) = {}" |
"vars (V x) = {x}" |
"vars (Plus a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \<union> vars a\<^sub>2"
instance ..
end
instantiation bexp :: vars
begin
fun vars_bexp :: "bexp \<Rightarrow> vname set" where
"vars (Bc v) = {}" |
"vars (Not b) = vars b" |
"vars (And b\<^sub>1 b\<^sub>2) = vars b\<^sub>1 \<union> vars b\<^sub>2" |
"vars (Less a\<^sub>1 a\<^sub>2) = vars a\<^sub>1 \<union> vars a\<^sub>2"
instance ..
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"
lemma aval_eq_if_eq_on_vars[simp]:
"s\<^sub>1 = s\<^sub>2 on vars a \<Longrightarrow> aval a s\<^sub>1 = aval a s\<^sub>2"
apply(induction a)
apply simp_all
done
lemma bval_eq_if_eq_on_vars:
"s\<^sub>1 = s\<^sub>2 on vars b \<Longrightarrow> bval b s\<^sub>1 = bval b s\<^sub>2"
proof(induction b)
case (Less a1 a2)
hence "aval a1 s\<^sub>1 = aval a1 s\<^sub>2" and "aval a2 s\<^sub>1 = aval a2 s\<^sub>2" by simp_all
thus ?case by simp
qed simp_all
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)
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)
subsubsection "Orderings"
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
end
theory Submission imports Defs begin
context order
begin
abbreviation "lower S l \<equiv> \<forall>s\<in>S. l \<le> s"
abbreviation "greatest S l \<equiv> \<forall>l'. (lower S l' \<longrightarrow> l' \<le> l)"
end
class complete_lattice = order +
assumes "\<And>S::'a set. \<exists>l. (lower S l \<and> greatest S l)"
class finite_semilattice_sup_bot = semilattice_sup + order_bot + finite
begin
inductive set_sup :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> bool" ("\<Squnion> _/ _/ := _/" [59, 59, 59]) for b where
empty[intro]: "\<Squnion> b {} := b"
| insert[intro]: "\<Squnion> b A := y \<Longrightarrow> \<Squnion> b (insert x A) := (x \<squnion> y)"
theorem sup_pres_p:
assumes sup: "\<Squnion> b A := y"
assumes pres: "\<And> x y. P x \<Longrightarrow> P y \<Longrightarrow> P (x \<squnion> y)"
shows "\<forall>x \<in> A. P x \<Longrightarrow> P b \<Longrightarrow> P y"
sorry
txt \<open>Case proof:\<close>
theorem complete_lattice_prf: "class.complete_lattice (\<le>) (<)"
proof
oops
end
txt \<open>Case counterexample:\<close>
datatype cex_a = TODO txt \<open>Put in your type here\<close>
instantiation cex_a :: finite_semilattice_sup_bot
begin
definition less_eq_cex_a :: "cex_a \<Rightarrow> cex_a \<Rightarrow> bool" where
"less_eq_cex_a _ _ = True"
definition less_cex_a :: "cex_a \<Rightarrow> cex_a \<Rightarrow> bool" where
"less_cex_a _ _ = False"
definition bot_cex_a :: "cex_a" where
"bot_cex_a = TODO"
definition sup_cex_a :: "cex_a \<Rightarrow> cex_a \<Rightarrow> cex_a" where
"sup_cex_a _ _ = TODO"
instance sorry
lemma complete_lattice_cex: "\<not>class.complete_lattice (\<le>) (<)"
proof -
have "\<exists>S. \<nexists>l. (lower S l \<and> greatest S l)"
oops
end
txt \<open>Finally, add the name of the lemma you proved below:\<close>
lemmas prf_or_cex = complete_lattice_prf complete_lattice_cex
subsubsection "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"
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' :: "ereal \<Rightarrow> 'av"
and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
assumes gamma_num': "Some i \<in> \<gamma>(num' i)"
and gamma_plus': "Some i1 \<in> \<gamma> a1 \<Longrightarrow> Some i2 \<in> \<gamma> a2 \<Longrightarrow> Some (i1+i2) \<in> \<gamma>(plus' a1 a2)"
type_synonym 'av st = "(vname \<Rightarrow> 'av)"
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' (Plus a1 a2) S = plus' (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])
lemma aval'_correct: "s \<in> \<gamma>\<^sub>s S \<Longrightarrow> aval a s \<in> \<gamma>(aval' a S)"
sorry
lemma in_gamma_update: "\<lbrakk> s \<in> \<gamma>\<^sub>s S; i \<in> \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) \<in> \<gamma>\<^sub>s(S(x := a))"
by(simp add: \<gamma>_fun_def)
lemma gamma_Step_subcomm:
assumes "\<And>x e S. f1 x e (\<gamma>\<^sub>o S) \<subseteq> \<gamma>\<^sub>o (f2 x e S)" "\<And>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_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' 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_plus')
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
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 \<open>I x0\<close> \<open>x0 \<le> f x0\<close> 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))"
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
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
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 "\<exists>x\<in>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 \<open>finite X\<close> 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 \<open>i < size(annos C2)\<close> 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
subsection "Computable State"
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]:
"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
declare [[typedef_overloaded]]
quotient_type 'a st_c = "('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_c \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st_c"
is "\<lambda>ps x a. (x,a)#ps"
by(auto simp: eq_st_def)
lift_definition "fun" :: "('a::top) st_c \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
by(simp add: eq_st_def)
definition show_st :: "vname set \<Rightarrow> ('a::top) st_c \<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_c \<Rightarrow> (vname \<Rightarrow> 'b) set" where
"\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(fun F x)}"
instantiation st_c :: (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_c :: "'a st_c \<Rightarrow> 'a st_c \<Rightarrow> bool" is less_eq_st_rep
by(auto simp add: eq_st_def less_eq_st_rep_iff)
definition less_st_c where "F < (G::'a st_c) = (F \<le> G \<and> \<not> G \<le> F)"
instance
proof (standard, goal_cases)
case 1 show ?case by(rule less_st_c_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_c :: (semilattice_sup_top) semilattice_sup_top
begin
lift_definition sup_st_c:: "'a st_c \<Rightarrow> 'a st_c \<Rightarrow> 'a st_c" is "map2_st_rep (\<squnion>)"
by (simp add: eq_st_def)
lift_definition top_st_c :: "'a st_c" 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_c \<Rightarrow> state set"
where "\<gamma>\<^sub>s == \<gamma>_st \<gamma>"
abbreviation \<gamma>\<^sub>o :: "'av st_c option \<Rightarrow> state set"
where "\<gamma>\<^sub>o == \<gamma>_option \<gamma>\<^sub>s"
abbreviation \<gamma>\<^sub>c :: "'av st_c 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 \<in> \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x \<in> r u')"
by (cases u) auto
end
subsection "Computable Abstract Interpretation"
context Gamma_semilattice
begin
fun aval' :: "aexp \<Rightarrow> 'av st_c \<Rightarrow> 'av" where
"aval' (N i) S = num' i" |
"aval' (V x) S = fun S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
lemma aval'_correct: "s \<in> \<gamma>\<^sub>s S \<Longrightarrow> aval a s \<in> \<gamma>(aval' a S)"
sorry
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 \<in> \<gamma>\<^sub>s S; i \<in> \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) \<in> \<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_c 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 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_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
begin
lemma mono_aval': "S1 \<le> S2 \<Longrightarrow> aval' e S1 \<le> aval' e S2"
by(induction e) (auto simp: mono_plus' 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_c \<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_c 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_c option acom \<Rightarrow> nat" ("m\<^sub>c") where
"m_c C = sum_list (map (\<lambda>a. m_o a (vars C)) (annos C))"
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_c \<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_c 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_c 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_c 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_c 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_c 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 "\<exists>x\<in>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 \<open>finite X\<close> 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_c_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, lifting) 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 \<open>i < size(annos C2)\<close> 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
txt \<open>You can start the formalization of the AI like this:\<close>
datatype bound = NegInf ("\<infinity>\<^sup>-") | PosInf ("\<infinity>\<^sup>+") | NaN | Real
datatype bounds = S "bound set"
instantiation bounds :: order
begin
definition less_eq_bounds where
"x \<le> y = (case (x, y) of (S x, S y) \<Rightarrow> x \<subseteq> y)"
definition less_bounds where
"x < y = (case (x, y) of (S x, S y) \<Rightarrow> x \<subset> y)"
instance sorry
end
instantiation bounds :: semilattice_sup_top
begin
definition sup_bounds :: "bounds \<Rightarrow> bounds \<Rightarrow> bounds" where
"sup_bounds x y = undefined"
definition top_bounds :: "bounds" where
"top_bounds = undefined"
instance sorry
end
fun \<gamma>_bounds :: "bounds \<Rightarrow> val set" where
"\<gamma>_bounds _ = undefined"
definition num_bounds :: "ereal \<Rightarrow> bounds" where
"num_bounds _ = undefined"
fun plus_bounds :: "bounds \<Rightarrow> bounds \<Rightarrow> bounds" where
"plus_bounds _ = undefined"
global_interpretation Val_semilattice
where \<gamma> = \<gamma>_bounds and num' = num_bounds and plus' = plus_bounds
sorry
global_interpretation Abs_Int
where \<gamma> = \<gamma>_bounds and num' = num_bounds and plus' = plus_bounds
defines aval_bounds = aval' and step_bounds = step' and AI_bounds = AI
sorry
global_interpretation Abs_Int_mono
where \<gamma> = \<gamma>_bounds and num' = num_bounds and plus' = plus_bounds
sorry
fun m_bounds :: "bounds \<Rightarrow> nat" where
"m_bounds _ = undefined"
abbreviation h_bounds :: nat where
"h_bounds \<equiv> undefined"
global_interpretation Abs_Int_measure
where \<gamma> = \<gamma>_bounds and num' = num_bounds and plus' = plus_bounds
and m = m_bounds and h = h_bounds
sorry
end
theory Check imports Submission begin theorem sup_pres_p: assumes sup: "\<Squnion> b A := y" assumes pres: "\<And> x y. P x \<Longrightarrow> P y \<Longrightarrow> P (x \<squnion> y)" shows "\<forall>x \<in> A. P x \<Longrightarrow> P b \<Longrightarrow> P y" using assms by (rule Submission.sup_pres_p) theorem Val_Semilattice: "Val_semilattice \<gamma>_bounds num_bounds plus_bounds" by (rule Submission.Val_semilattice_axioms) theorem Abs_Int: "Abs_Int num_bounds plus_bounds \<gamma>_bounds" by (rule Submission.Abs_Int_axioms) theorem Abs_Int_mono: "Abs_Int_mono num_bounds plus_bounds \<gamma>_bounds" by (rule Submission.Abs_Int_mono_axioms) theorem Abs_Int_measure: "Abs_Int_measure num_bounds plus_bounds h_bounds \<gamma>_bounds m_bounds" by (rule Submission.Abs_Int_measure_axioms) end