Our site saves small pieces of text information (cookies) on your device in order to deliver better content and for statistical purposes. You can disable the usage of cookies by changing the settings of your browser. By browsing our website without changing the browser settings you grant us permission to store that information on your device.

# Homework 11

This is the task corresponding to homework 11.

## Resources

### Definitions File

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

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

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

lemma post_lfp: "post(lfp c f) = (\<Inter>{post C|C. strip C = c \<and> f C \<le> C})"

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

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

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"

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

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

### Template File

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

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"

lemma gamma_o_Top[simp]: "\<gamma>\<^sub>o \<top> = UNIV"

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

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

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

end

instantiation acom :: (type) vars
begin

definition "vars_acom = vars o strip"

instance ..

end

lemma finite_Cvars: "finite(vars(C::'a acom))"

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

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

lemma top_on_post: "top_on_acom C X \<Longrightarrow> top_on_opt (post C) X"

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

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

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

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

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

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"

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"

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

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"

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

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

lemma top_on_post: "top_on_acom C X \<Longrightarrow> top_on_opt (post C) X"

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

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 (transfer fixing: m)
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```

### Check File

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

Terms and Conditions