(* Title: HOL/MicroJava/DFA/Opt.thy
Author: Tobias Nipkow
Copyright 2000 TUM
*)
section \<open>More about Options\<close>
theory Opt
imports Err
begin
definition le :: "'a ord \<Rightarrow> 'a option ord" where
"le r o1 o2 == case o2 of None \<Rightarrow> o1=None |
Some y \<Rightarrow> (case o1 of None \<Rightarrow> True
| Some x \<Rightarrow> x <=_r y)"
definition opt :: "'a set \<Rightarrow> 'a option set" where
"opt A == insert None {x. \<exists>y\<in>A. x = Some y}"
definition sup :: "'a ebinop \<Rightarrow> 'a option ebinop" where
"sup f o1 o2 ==
case o1 of None \<Rightarrow> OK o2 | Some x \<Rightarrow> (case o2 of None \<Rightarrow> OK o1
| Some y \<Rightarrow> (case f x y of Err \<Rightarrow> Err | OK z \<Rightarrow> OK (Some z)))"
definition esl :: "'a esl \<Rightarrow> 'a option esl" where
"esl == %(A,r,f). (opt A, le r, sup f)"
lemma unfold_le_opt:
"o1 <=_(le r) o2 =
(case o2 of None \<Rightarrow> o1=None |
Some y \<Rightarrow> (case o1 of None \<Rightarrow> True | Some x \<Rightarrow> x <=_r y))"
apply (unfold lesub_def le_def)
apply (rule refl)
done
lemma le_opt_refl:
"order r \<Longrightarrow> o1 <=_(le r) o1"
by (simp add: unfold_le_opt split: option.split)
lemma le_opt_trans [rule_format]:
"order r \<Longrightarrow>
o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o3 \<longrightarrow> o1 <=_(le r) o3"
apply (simp add: unfold_le_opt split: option.split)
apply (blast intro: order_trans)
done
lemma le_opt_antisym [rule_format]:
"order r \<Longrightarrow> o1 <=_(le r) o2 \<longrightarrow> o2 <=_(le r) o1 \<longrightarrow> o1=o2"
apply (simp add: unfold_le_opt split: option.split)
apply (blast intro: order_antisym)
done
lemma order_le_opt [intro!,simp]:
"order r \<Longrightarrow> order(le r)"
apply (subst Semilat.order_def)
apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
done
lemma None_bot [iff]:
"None <=_(le r) ox"
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done
lemma Some_le [iff]:
"(Some x <=_(le r) ox) = (\<exists>y. ox = Some y \<and> x <=_r y)"
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done
lemma le_None [iff]:
"(ox <=_(le r) None) = (ox = None)"
apply (unfold lesub_def le_def)
apply (simp split: option.split)
done
lemma OK_None_bot [iff]:
"OK None <=_(Err.le (le r)) x"
by (simp add: lesub_def Err.le_def le_def split: option.split err.split)
lemma sup_None1 [iff]:
"x +_(sup f) None = OK x"
by (simp add: plussub_def sup_def split: option.split)
lemma sup_None2 [iff]:
"None +_(sup f) x = OK x"
by (simp add: plussub_def sup_def split: option.split)
lemma None_in_opt [iff]:
"None \<in> opt A"
by (simp add: opt_def)
lemma Some_in_opt [iff]:
"(Some x \<in> opt A) = (x\<in>A)"
apply (unfold opt_def)
apply auto
done
lemma semilat_opt [intro, simp]:
"\<And>L. err_semilat L \<Longrightarrow> err_semilat (Opt.esl L)"
proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)
fix A r f
assume s: "semilat (err A, Err.le r, lift2 f)"
let ?A0 = "err A"
let ?r0 = "Err.le r"
let ?f0 = "lift2 f"
from s
obtain
ord: "order ?r0" and
clo: "closed ?A0 ?f0" and
ub1: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. x <=_?r0 x +_?f0 y" and
ub2: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. y <=_?r0 x +_?f0 y" and
lub: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. \<forall>z\<in>?A0. x <=_?r0 z \<and> y <=_?r0 z \<longrightarrow> x +_?f0 y <=_?r0 z"
by (unfold semilat_def) simp
let ?A = "err (opt A)"
let ?r = "Err.le (Opt.le r)"
let ?f = "lift2 (Opt.sup f)"
from ord
have "order ?r"
by simp
moreover
have "closed ?A ?f"
proof (unfold closed_def, intro strip)
fix x y
assume x: "x \<in> ?A"
assume y: "y \<in> ?A"
{ fix a b
assume ab: "x = OK a" "y = OK b"
with x
have a: "\<And>c. a = Some c \<Longrightarrow> c \<in> A"
by (clarsimp simp add: opt_def)
from ab y
have b: "\<And>d. b = Some d \<Longrightarrow> d \<in> A"
by (clarsimp simp add: opt_def)
{ fix c d assume "a = Some c" "b = Some d"
with ab x y
have "c \<in> A \<and> d \<in> A"
by (simp add: err_def opt_def Bex_def)
with clo
have "f c d \<in> err A"
by (simp add: closed_def plussub_def err_def lift2_def)
moreover
fix z assume "f c d = OK z"
ultimately
have "z \<in> A" by simp
} note f_closed = this
have "sup f a b \<in> ?A"
proof (cases a)
case None
thus ?thesis
by (simp add: sup_def opt_def) (cases b, simp, simp add: b Bex_def)
next
case Some
thus ?thesis
by (auto simp add: sup_def opt_def Bex_def a b f_closed split: err.split option.split)
qed
}
thus "x +_?f y \<in> ?A"
by (simp add: plussub_def lift2_def split: err.split)
qed
moreover
{ fix a b c
assume "a \<in> opt A" "b \<in> opt A" "a +_(sup f) b = OK c"
moreover
from ord have "order r" by simp
moreover
{ fix x y z
assume "x \<in> A" "y \<in> A"
hence "OK x \<in> err A \<and> OK y \<in> err A" by simp
with ub1 ub2
have "(OK x) <=_(Err.le r) (OK x) +_(lift2 f) (OK y) \<and>
(OK y) <=_(Err.le r) (OK x) +_(lift2 f) (OK y)"
by blast
moreover
assume "x +_f y = OK z"
ultimately
have "x <=_r z \<and> y <=_r z"
by (auto simp add: plussub_def lift2_def Err.le_def lesub_def)
}
ultimately
have "a <=_(le r) c \<and> b <=_(le r) c"
by (auto simp add: sup_def le_def lesub_def plussub_def
dest: order_refl split: option.splits err.splits)
}
hence "(\<forall>x\<in>?A. \<forall>y\<in>?A. x <=_?r x +_?f y) \<and> (\<forall>x\<in>?A. \<forall>y\<in>?A. y <=_?r x +_?f y)"
by (auto simp add: lesub_def plussub_def Err.le_def lift2_def split: err.split)
moreover
have "\<forall>x\<in>?A. \<forall>y\<in>?A. \<forall>z\<in>?A. x <=_?r z \<and> y <=_?r z \<longrightarrow> x +_?f y <=_?r z"
proof (intro strip, elim conjE)
fix x y z
assume xyz: "x \<in> ?A" "y \<in> ?A" "z \<in> ?A"
assume xz: "x <=_?r z"
assume yz: "y <=_?r z"
{ fix a b c
assume ok: "x = OK a" "y = OK b" "z = OK c"
{ fix d e g
assume some: "a = Some d" "b = Some e" "c = Some g"
with ok xyz
obtain "OK d \<in> err A" "OK e \<in> err A" "OK g \<in> err A"
by simp
with lub
have "\<lbrakk> (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) \<rbrakk>
\<Longrightarrow> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
by blast
hence "\<lbrakk> d <=_r g; e <=_r g \<rbrakk> \<Longrightarrow> \<exists>y. d +_f e = OK y \<and> y <=_r g"
by simp
with ok some xyz xz yz
have "x +_?f y <=_?r z"
by (auto simp add: sup_def le_def lesub_def lift2_def plussub_def Err.le_def)
} note this [intro!]
from ok xyz xz yz
have "x +_?f y <=_?r z"
by - (cases a, simp, cases b, simp, cases c, simp, blast)
}
with xyz xz yz
show "x +_?f y <=_?r z"
by - (cases x, simp, cases y, simp, cases z, simp+)
qed
ultimately
show "semilat (?A,?r,?f)"
by (unfold semilat_def) simp
qed
lemma top_le_opt_Some [iff]:
"top (le r) (Some T) = top r T"
apply (unfold top_def)
apply (rule iffI)
apply blast
apply (rule allI)
apply (case_tac "x")
apply simp+
done
lemma Top_le_conv:
"\<lbrakk> order r; top r T \<rbrakk> \<Longrightarrow> (T <=_r x) = (x = T)"
apply (unfold top_def)
apply (blast intro: order_antisym)
done
lemma acc_le_optI [intro!]:
"acc r \<Longrightarrow> acc(le r)"
apply (unfold acc_def lesub_def le_def lesssub_def)
apply (simp add: wf_eq_minimal split: option.split)
apply clarify
apply (case_tac "\<exists>a. Some a \<in> Q")
apply (erule_tac x = "{a. Some a \<in> Q}" in allE)
apply blast
apply (case_tac "x")
apply blast
apply blast
done
lemma option_map_in_optionI:
"\<lbrakk> ox \<in> opt S; \<forall>x\<in>S. ox = Some x \<longrightarrow> f x \<in> S \<rbrakk>
\<Longrightarrow> map_option f ox \<in> opt S"
apply (unfold map_option_case)
apply (simp split: option.split)
apply blast
done
end