--- a/src/HOL/MicroJava/BV/BVSpec.thy Sat Nov 18 19:48:34 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy Mon Nov 20 16:37:42 2000 +0100
@@ -9,11 +9,6 @@
theory BVSpec = Step:
-types
- method_type = "state_type option list"
- class_type = "sig => method_type"
- prog_type = "cname => class_type"
-
constdefs
wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] => bool"
"wt_instr i G rT phi max_pc pc ==
@@ -22,7 +17,7 @@
wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
"wt_start G C pTs mxl phi ==
- G \<turnstile> Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err)) <=' phi!0"
+ G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] => bool"
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Sat Nov 18 19:48:34 2000 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy Mon Nov 20 16:37:42 2000 +0100
@@ -274,7 +274,7 @@
from a_stk
obtain opTs stk' oX where
opTs: "approx_stk G hp opTs (rev apTs)" and
- oX: "approx_val G hp oX (Ok X)" and
+ oX: "approx_val G hp oX (OK X)" and
a_stk': "approx_stk G hp stk' ST" and
stk': "stk = opTs @ oX # stk'" and
l_o: "length opTs = length apTs"
@@ -377,7 +377,7 @@
proof -
from start LT0
have sup_loc:
- "G \<turnstile> (Ok (Class D'') # map Ok pTs @ replicate mxl' Err) <=l LT0"
+ "G \<turnstile> (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0"
(is "G \<turnstile> ?LT <=l LT0")
by (simp add: wt_start_def sup_state_def)
@@ -389,14 +389,14 @@
have "G \<turnstile> Class D \<preceq> Class D''"
by (auto dest: method_wf_mdecl)
with obj_ty loc
- have a: "approx_val G hp (Addr ref) (Ok (Class D''))"
+ have a: "approx_val G hp (Addr ref) (OK (Class D''))"
by (simp add: approx_val_def conf_def)
from w l
have "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> widen G"
by (auto simp add: zip_rev)
with wfprog l l_o opTs
- have "approx_loc G hp opTs (map Ok (rev pTs))"
+ have "approx_loc G hp opTs (map OK (rev pTs))"
by (auto intro: assConv_approx_stk_imp_approx_loc)
hence "approx_stk G hp opTs (rev pTs)"
by (simp add: approx_stk_def)
@@ -427,7 +427,7 @@
by (rule approx_loc_imp_approx_loc_sup)
moreover
from s s' mC' step l
- have "G \<turnstile> map Ok ST <=l map Ok (tl ST')"
+ have "G \<turnstile> map OK ST <=l map OK (tl ST')"
by (auto simp add: step_def sup_state_def map_eq_Cons)
with wfprog a_stk'
have "approx_stk G hp stk' (tl ST')"
--- a/src/HOL/MicroJava/BV/Convert.thy Sat Nov 18 19:48:34 2000 +0100
+++ b/src/HOL/MicroJava/BV/Convert.thy Mon Nov 20 16:37:42 2000 +0100
@@ -6,29 +6,23 @@
header "Lifted Type Relations"
-theory Convert = JVMExec:
+theory Convert = Err + JVMExec:
text "The supertype relation lifted to type err, type lists and state types."
-datatype 'a err = Err | Ok 'a
-
types
locvars_type = "ty err list"
opstack_type = "ty list"
state_type = "opstack_type \<times> locvars_type"
-
+ method_type = "state_type option list"
+ class_type = "sig => method_type"
+ prog_type = "cname => class_type"
consts
strict :: "('a => 'b err) => ('a err => 'b err)"
primrec
"strict f Err = Err"
- "strict f (Ok x) = f x"
-
-
-consts
- val :: "'a err => 'a"
-primrec
- "val (Ok s) = s"
+ "strict f (OK x) = f x"
constdefs
@@ -36,7 +30,7 @@
lift_top :: "('a => 'b => bool) => ('a err => 'b err => bool)"
"lift_top P a' a == case a of
Err => True
- | Ok t => (case a' of Err => False | Ok t' => P t' t)"
+ | OK t => (case a' of Err => False | OK t' => P t' t)"
(* lifts a relation to option with None as bottom element *)
lift_bottom :: "('a => 'b => bool) => ('a option => 'b option => bool)"
@@ -56,7 +50,7 @@
sup_state :: "['code prog,state_type,state_type] => bool"
("_ \<turnstile> _ <=s _" [71,71] 70)
"G \<turnstile> s <=s s' ==
- (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+ (G \<turnstile> map OK (fst s) <=l map OK (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
sup_state_opt :: "['code prog,state_type option,state_type option] => bool"
("_ \<turnstile> _ <=' _" [71,71] 70)
@@ -73,14 +67,7 @@
("_ |- _ <=' _" [71,71] 70)
-lemma not_Err_eq [iff]:
- "(x \<noteq> Err) = (\<exists>a. x = Ok a)"
- by (cases x) auto
-
-lemma not_Some_eq [iff]:
- "(\<forall>y. x \<noteq> Ok y) = (x = Err)"
- by (cases x) auto
-
+lemmas [iff] = not_Err_eq not_OK_eq
lemma lift_top_refl [simp]:
"[| !!x. P x x |] ==> lift_top P x x"
@@ -105,9 +92,9 @@
} note x_none = this
{ fix r t
- assume x: "x = Ok r" and z: "z = Ok t"
+ assume x: "x = OK r" and z: "z = OK t"
with a b
- obtain s where y: "y = Ok s"
+ obtain s where y: "y = OK s"
by (simp add: lift_top_def split: err.splits)
from a x y
@@ -130,16 +117,16 @@
"lift_top P Err any = (any = Err)"
by (simp add: lift_top_def split: err.splits)
-lemma lift_top_Ok_Ok [simp]:
- "lift_top P (Ok a) (Ok b) = P a b"
+lemma lift_top_OK_OK [simp]:
+ "lift_top P (OK a) (OK b) = P a b"
by (simp add: lift_top_def split: err.splits)
-lemma lift_top_any_Ok [simp]:
- "lift_top P any (Ok b) = (\<exists>a. any = Ok a \<and> P a b)"
+lemma lift_top_any_OK [simp]:
+ "lift_top P any (OK b) = (\<exists>a. any = OK a \<and> P a b)"
by (simp add: lift_top_def split: err.splits)
-lemma lift_top_Ok_any:
- "lift_top P (Ok a) any = (any = Err \<or> (\<exists>b. any = Ok b \<and> P a b))"
+lemma lift_top_OK_any:
+ "lift_top P (OK a) any = (any = Err \<or> (\<exists>b. any = OK b \<and> P a b))"
by (simp add: lift_top_def split: err.splits)
@@ -227,12 +214,12 @@
"(G \<turnstile> Err <=o any) = (any = Err)"
by (simp add: sup_ty_opt_def)
-theorem OkanyConvOk [simp]:
- "(G \<turnstile> (Ok ty') <=o (Ok ty)) = (G \<turnstile> ty' \<preceq> ty)"
+theorem OKanyConvOK [simp]:
+ "(G \<turnstile> (OK ty') <=o (OK ty)) = (G \<turnstile> ty' \<preceq> ty)"
by (simp add: sup_ty_opt_def)
-theorem sup_ty_opt_Ok:
- "G \<turnstile> a <=o (Ok b) ==> \<exists> x. a = Ok x"
+theorem sup_ty_opt_OK:
+ "G \<turnstile> a <=o (OK b) ==> \<exists> x. a = OK x"
by (clarsimp simp add: sup_ty_opt_def)
lemma widen_PrimT_conv1 [simp]:
@@ -240,8 +227,8 @@
by (auto elim: widen.elims)
theorem sup_PTS_eq:
- "(G \<turnstile> Ok (PrimT p) <=o X) = (X=Err \<or> X = Ok (PrimT p))"
- by (auto simp add: sup_ty_opt_def lift_top_Ok_any)
+ "(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))"
+ by (auto simp add: sup_ty_opt_def lift_top_OK_any)
--- a/src/HOL/MicroJava/BV/Correct.thy Sat Nov 18 19:48:34 2000 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy Mon Nov 20 16:37:42 2000 +0100
@@ -12,13 +12,13 @@
constdefs
approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
- "approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T"
+ "approx_val G h v any == case any of Err => True | OK T => G,h\<turnstile>v::\<preceq>T"
approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
"approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
- "approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
+ "approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)"
correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
"correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
@@ -96,12 +96,12 @@
by (simp add: approx_val_def)
lemma approx_val_Null:
- "approx_val G hp Null (Ok (RefT x))"
+ "approx_val G hp Null (OK (RefT x))"
by (auto intro: null simp add: approx_val_def)
lemma approx_val_imp_approx_val_assConvertible [rule_format]:
- "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T'
- --> approx_val G hp v (Ok T')"
+ "wf_prog wt G ==> approx_val G hp v (OK T) --> G\<turnstile> T\<preceq>T'
+ --> approx_val G hp v (OK T')"
by (cases T) (auto intro: conf_widen simp add: approx_val_def)
lemma approx_val_imp_approx_val_sup_heap [rule_format]:
@@ -143,7 +143,7 @@
lemma assConv_approx_stk_imp_approx_loc [rule_format]:
"wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G)
--> length tys_n = length ts --> approx_stk G hp s tys_n -->
- approx_loc G hp s (map Ok ts)"
+ approx_loc G hp s (map OK ts)"
apply (unfold approx_stk_def approx_loc_def list_all2_def)
apply (clarsimp simp add: all_set_conv_all_nth)
apply (rule approx_val_imp_approx_val_assConvertible)
@@ -212,7 +212,7 @@
by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
lemma approx_stk_imp_approx_stk_sup [rule_format]:
- "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map Ok st <=l (map Ok st'))
+ "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map OK st <=l (map OK st'))
--> approx_stk G hp lvars st'"
by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
@@ -222,12 +222,12 @@
lemma approx_stk_Cons [iff]:
"approx_stk G hp (x # stk) (S#ST) =
- (approx_val G hp x (Ok S) \<and> approx_stk G hp stk ST)"
+ (approx_val G hp x (OK S) \<and> approx_stk G hp stk ST)"
by (simp add: approx_stk_def approx_loc_def)
lemma approx_stk_Cons_lemma [iff]:
"approx_stk G hp stk (S#ST') =
- (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (Ok S) \<and> approx_stk G hp stk' ST')"
+ (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (OK S) \<and> approx_stk G hp stk' ST')"
by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
lemma approx_stk_append_lemma:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/DFA_Framework.thy Mon Nov 20 16:37:42 2000 +0100
@@ -0,0 +1,76 @@
+(* Title: HOL/BCV/DFA_Framework.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TUM
+
+The relationship between dataflow analysis and a welltyped-insruction predicate.
+*)
+
+header "Dataflow Analysis Framework"
+
+theory DFA_Framework = Listn:
+
+constdefs
+
+ stable :: "'s ord =>
+ (nat => 's => 's)
+ => (nat => nat list) => 's list => nat => bool"
+"stable r step succs ss p == !q:set(succs p). step p (ss!p) <=_r ss!q"
+
+ stables :: "'s ord => (nat => 's => 's)
+ => (nat => nat list) => 's list => bool"
+"stables r step succs ss == !p<size ss. stable r step succs ss p"
+
+ is_dfa :: "'s ord
+ => ('s list => 's list)
+ => (nat => 's => 's)
+ => (nat => nat list)
+ => nat => 's set => bool"
+"is_dfa r dfa step succs n A == !ss : list n A.
+ dfa ss : list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss &
+ (!ts: list n A. ss <=[r] ts & stables r step succs ts
+ --> dfa ss <=[r] ts)"
+
+ is_bcv :: "'s ord => 's => (nat => 's => 's) => (nat => nat list)
+ => nat => 's set => ('s list => 's list) => bool"
+"is_bcv r T step succs n A bcv == !ss : list n A.
+ (!p<n. (bcv ss)!p ~= T) =
+ (? ts: list n A. ss <=[r] ts & welltyping r T step succs ts)"
+
+ welltyping ::
+"'s ord => 's => (nat => 's => 's) => (nat => nat list) => 's list => bool"
+"welltyping r T step succs ts ==
+ !p<size(ts). ts!p ~= T & stable r step succs ts p"
+
+
+lemma is_dfaD:
+ "[| is_dfa r dfa step succs n A; ss : list n A |] ==>
+ dfa ss:list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss &
+ (!ts: list n A. stables r step succs ts & ss <=[r] ts
+ --> dfa ss <=[r] ts)"
+ by (simp add: is_dfa_def)
+
+
+lemma is_bcv_dfa:
+ "[| order r; top r T; is_dfa r dfa step succs n A |]
+ ==> is_bcv r T step succs n A dfa"
+apply (unfold is_bcv_def welltyping_def stables_def)
+apply clarify
+apply (drule is_dfaD)
+apply assumption
+apply clarify
+apply (rule iffI)
+ apply (rule bexI)
+ apply (rule conjI)
+ apply assumption
+ apply (simp add: stables_def)
+ apply assumption
+apply clarify
+apply (simp add: imp_conjR all_conj_distrib stables_def
+ cong: conj_cong)
+apply (drule_tac x = ts in bspec)
+ apply assumption
+apply (force dest: le_listD)
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/DFA_err.thy Mon Nov 20 16:37:42 2000 +0100
@@ -0,0 +1,121 @@
+(* Title: HOL/BCV/DFA_err.thy
+ ID: $Id$
+ Author: Gerwin Klein
+ Copyright 2000 TUM
+
+static and dynamic welltyping
+*)
+
+header "Static and Dynamic Welltyping"
+
+theory DFA_err = DFA_Framework:
+
+constdefs
+
+dynamic_wt :: "'s ord => (nat => 's err => 's err) => (nat => nat list) =>
+ 's err list => bool"
+"dynamic_wt r step succs ts == welltyping (Err.le r) Err step succs ts"
+
+static_wt :: "'s ord => (nat => 's => bool) =>
+ (nat => 's => 's) => (nat => nat list) => 's list => bool"
+"static_wt r app step succs ts ==
+ !p < size ts. app p (ts!p) & (!q:set(succs p). step p (ts!p) <=_r ts!q)"
+
+err_step :: "(nat => 's => bool) => (nat => 's => 's) =>
+ (nat => 's err => 's err)"
+"err_step app step p == lift (%t. if app p t then OK (step p t) else Err)"
+
+bounded :: "(nat => nat list) => nat => bool"
+"bounded succs n == !p<n. !q:set(succs p). q<n"
+
+non_empty :: "(nat => nat list) => bool"
+"non_empty succs == !p. succs p ~= []"
+
+
+lemma non_emptyD:
+ "non_empty succs ==> ? q. q:set(succs p)"
+proof (unfold non_empty_def)
+ assume "!p. succs p ~= []"
+ hence "succs p ~= []" ..
+ then obtain x xs where "succs p = x#xs"
+ by (auto simp add: neq_Nil_conv)
+ thus ?thesis
+ by auto
+qed
+
+text_raw {* \newpage *}
+lemma dynamic_imp_static:
+ "[| bounded succs (size ts); non_empty succs;
+ dynamic_wt r (err_step app step) succs ts |]
+ ==> static_wt r app step succs (map ok_val ts)"
+proof (unfold static_wt_def, intro strip, rule conjI)
+
+ assume b: "bounded succs (size ts)"
+ assume n: "non_empty succs"
+ assume wt: "dynamic_wt r (err_step app step) succs ts"
+
+ fix p
+ assume "p < length (map ok_val ts)"
+ hence lp: "p < length ts" by simp
+
+ from wt lp
+ have [intro?]: "!!p. p < length ts ==> ts ! p ~= Err"
+ by (unfold dynamic_wt_def welltyping_def) simp
+
+ show app: "app p (map ok_val ts ! p)"
+ proof -
+ from n
+ obtain q where q: "q:set(succs p)"
+ by (auto dest: non_emptyD)
+
+ from wt lp q
+ obtain s where
+ OKp: "ts ! p = OK s" and
+ less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
+ by (unfold dynamic_wt_def welltyping_def stable_def)
+ (auto iff: not_Err_eq)
+
+ from lp b q
+ have lq: "q < length ts"
+ by (unfold bounded_def) blast
+ hence "ts!q ~= Err" ..
+ then
+ obtain s' where OKq: "ts ! q = OK s'"
+ by (auto iff: not_Err_eq)
+
+ with OKp less
+ have "app p s"
+ by (simp add: err_step_def lift_def split: err.split_asm split_if_asm)
+
+ with lp OKp
+ show ?thesis
+ by simp
+ qed
+
+ show "!q:set(succs p). step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
+ proof (intro strip)
+ fix q
+ assume q: "q:set (succs p)"
+
+ from wt lp q
+ obtain s where
+ OKp: "ts ! p = OK s" and
+ less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
+ by (unfold dynamic_wt_def welltyping_def stable_def)
+ (auto iff: not_Err_eq)
+
+ from lp b q
+ have lq: "q < length ts"
+ by (unfold bounded_def) blast
+ hence "ts!q ~= Err" ..
+ then
+ obtain s' where OKq: "ts ! q = OK s'"
+ by (auto iff: not_Err_eq)
+
+ from lp lq OKp OKq app less
+ show "step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
+ by (simp add: err_step_def lift_def)
+ qed
+qed
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Err.thy Mon Nov 20 16:37:42 2000 +0100
@@ -0,0 +1,336 @@
+(* Title: HOL/BCV/Err.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TUM
+
+The error type
+*)
+
+header "The Error Type"
+
+theory Err = Semilat:
+
+datatype 'a err = Err | OK 'a
+
+types 'a ebinop = "'a => 'a => 'a err"
+ 'a esl = "'a set * 'a ord * 'a ebinop"
+
+
+consts
+ ok_val :: "'a err => 'a"
+primrec
+ "ok_val (OK x) = x"
+
+
+constdefs
+ lift :: "('a => 'b err) => ('a err => 'b err)"
+"lift f e == case e of Err => Err | OK x => f x"
+
+ lift2 :: "('a => 'b => 'c err) => 'a err => 'b err => 'c err"
+"lift2 f e1 e2 ==
+ case e1 of Err => Err
+ | OK x => (case e2 of Err => Err | OK y => f x y)"
+
+ le :: "'a ord => 'a err ord"
+"le r e1 e2 ==
+ case e2 of Err => True |
+ OK y => (case e1 of Err => False | OK x => x <=_r y)"
+
+ sup :: "('a => 'b => 'c) => ('a err => 'b err => 'c err)"
+"sup f == lift2(%x y. OK(x +_f y))"
+
+ err :: "'a set => 'a err set"
+"err A == insert Err {x . ? y:A. x = OK y}"
+
+ esl :: "'a sl => 'a esl"
+"esl == %(A,r,f). (A,r, %x y. OK(f x y))"
+
+ sl :: "'a esl => 'a err sl"
+"sl == %(A,r,f). (err A, le r, lift2 f)"
+
+syntax
+ err_semilat :: "'a esl => bool"
+translations
+"err_semilat L" == "semilat(Err.sl L)"
+
+
+lemma not_Err_eq:
+ "(x \<noteq> Err) = (\<exists>a. x = OK a)"
+ by (cases x) auto
+
+lemma not_OK_eq:
+ "(\<forall>y. x \<noteq> OK y) = (x = Err)"
+ by (cases x) auto
+
+
+lemma unfold_lesub_err:
+ "e1 <=_(le r) e2 == le r e1 e2"
+ by (simp add: lesub_def)
+
+lemma le_err_refl:
+ "!x. x <=_r x ==> e <=_(Err.le r) e"
+apply (unfold lesub_def Err.le_def)
+apply (simp split: err.split)
+done
+
+lemma le_err_trans [rule_format]:
+ "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e3 --> e1 <=_(le r) e3"
+apply (unfold unfold_lesub_err le_def)
+apply (simp split: err.split)
+apply (blast intro: order_trans)
+done
+
+lemma le_err_antisym [rule_format]:
+ "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e1 --> e1=e2"
+apply (unfold unfold_lesub_err le_def)
+apply (simp split: err.split)
+apply (blast intro: order_antisym)
+done
+
+lemma OK_le_err_OK:
+ "(OK x <=_(le r) OK y) = (x <=_r y)"
+ by (simp add: unfold_lesub_err le_def)
+
+lemma order_le_err [iff]:
+ "order(le r) = order r"
+apply (rule iffI)
+ apply (subst order_def)
+ apply (blast dest: order_antisym OK_le_err_OK [THEN iffD2]
+ intro: order_trans OK_le_err_OK [THEN iffD1])
+apply (subst order_def)
+apply (blast intro: le_err_refl le_err_trans le_err_antisym
+ dest: order_refl)
+done
+
+lemma le_Err [iff]: "e <=_(le r) Err"
+ by (simp add: unfold_lesub_err le_def)
+
+lemma Err_le_conv [iff]:
+ "Err <=_(le r) e = (e = Err)"
+ by (simp add: unfold_lesub_err le_def split: err.split)
+
+lemma le_OK_conv [iff]:
+ "e <=_(le r) OK x = (? y. e = OK y & y <=_r x)"
+ by (simp add: unfold_lesub_err le_def split: err.split)
+
+lemma OK_le_conv:
+ "OK x <=_(le r) e = (e = Err | (? y. e = OK y & x <=_r y))"
+ by (simp add: unfold_lesub_err le_def split: err.split)
+
+lemma top_Err [iff]: "top (le r) Err";
+ by (simp add: top_def)
+
+lemma OK_less_conv [rule_format, iff]:
+ "OK x <_(le r) e = (e=Err | (? y. e = OK y & x <_r y))"
+ by (simp add: lesssub_def lesub_def le_def split: err.split)
+
+lemma not_Err_less [rule_format, iff]:
+ "~(Err <_(le r) x)"
+ by (simp add: lesssub_def lesub_def le_def split: err.split)
+
+lemma semilat_errI:
+ "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
+apply (unfold semilat_Def closed_def plussub_def lesub_def lift2_def Err.le_def err_def)
+apply (simp split: err.split)
+apply blast
+done
+
+lemma err_semilat_eslI:
+ "!!L. semilat L ==> err_semilat(esl L)"
+apply (unfold sl_def esl_def)
+apply (simp (no_asm_simp) only: split_tupled_all)
+apply (simp add: semilat_errI)
+done
+
+lemma acc_err [simp, intro!]: "acc r ==> acc(le r)"
+apply (unfold acc_def lesub_def le_def lesssub_def)
+apply (simp add: wf_eq_minimal split: err.split)
+apply clarify
+apply (case_tac "Err : Q")
+ apply blast
+apply (erule_tac x = "{a . OK a : Q}" in allE)
+apply (case_tac "x")
+ apply fast
+apply blast
+done
+
+lemma Err_in_err [iff]: "Err : err A"
+ by (simp add: err_def)
+
+lemma Ok_in_err [iff]: "(OK x : err A) = (x:A)"
+ by (auto simp add: err_def)
+
+(** lift **)
+
+lemma lift_in_errI:
+ "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S"
+apply (unfold lift_def)
+apply (simp split: err.split)
+apply blast
+done
+
+(** lift2 **)
+
+lemma Err_lift2 [simp]:
+ "Err +_(lift2 f) x = Err"
+ by (simp add: lift2_def plussub_def)
+
+lemma lift2_Err [simp]:
+ "x +_(lift2 f) Err = Err"
+ by (simp add: lift2_def plussub_def split: err.split)
+
+lemma OK_lift2_OK [simp]:
+ "OK x +_(lift2 f) OK y = x +_f y"
+ by (simp add: lift2_def plussub_def split: err.split)
+
+(** sup **)
+
+lemma Err_sup_Err [simp]:
+ "Err +_(Err.sup f) x = Err"
+ by (simp add: plussub_def Err.sup_def Err.lift2_def)
+
+lemma Err_sup_Err2 [simp]:
+ "x +_(Err.sup f) Err = Err"
+ by (simp add: plussub_def Err.sup_def Err.lift2_def split: err.split)
+
+lemma Err_sup_OK [simp]:
+ "OK x +_(Err.sup f) OK y = OK(x +_f y)"
+ by (simp add: plussub_def Err.sup_def Err.lift2_def)
+
+lemma Err_sup_eq_OK_conv [iff]:
+ "(Err.sup f ex ey = OK z) = (? x y. ex = OK x & ey = OK y & f x y = z)"
+apply (unfold Err.sup_def lift2_def plussub_def)
+apply (rule iffI)
+ apply (simp split: err.split_asm)
+apply clarify
+apply simp
+done
+
+lemma Err_sup_eq_Err [iff]:
+ "(Err.sup f ex ey = Err) = (ex=Err | ey=Err)"
+apply (unfold Err.sup_def lift2_def plussub_def)
+apply (simp split: err.split)
+done
+
+(*** semilat (err A) (le r) f ***)
+
+lemma semilat_le_err_Err_plus [simp]:
+ "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err"
+ by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
+
+lemma semilat_le_err_plus_Err [simp]:
+ "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err"
+ by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
+
+lemma semilat_le_err_OK1:
+ "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |]
+ ==> x <=_r z";
+apply (rule OK_le_err_OK [THEN iffD1])
+apply (erule subst)
+apply simp
+done
+
+lemma semilat_le_err_OK2:
+ "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |]
+ ==> y <=_r z"
+apply (rule OK_le_err_OK [THEN iffD1])
+apply (erule subst)
+apply simp
+done
+
+lemma eq_order_le:
+ "[| x=y; order r |] ==> x <=_r y"
+apply (unfold order_def)
+apply blast
+done
+
+lemma OK_plus_OK_eq_Err_conv [simp]:
+ "[| x:A; y:A; semilat(err A, le r, fe) |] ==>
+ ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
+proof -
+ have plus_le_conv3: "!!A x y z f r.
+ [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |]
+ ==> x <=_r z \<and> y <=_r z"
+ by (rule plus_le_conv [THEN iffD1])
+ case antecedent
+ thus ?thesis
+ apply (rule_tac iffI)
+ apply clarify
+ apply (drule OK_le_err_OK [THEN iffD2])
+ apply (drule OK_le_err_OK [THEN iffD2])
+ apply (drule semilat_lub)
+ apply assumption
+ apply assumption
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ apply (case_tac "(OK x) +_fe (OK y)")
+ apply assumption
+ apply (rename_tac z)
+ apply (subgoal_tac "OK z: err A")
+ apply (drule eq_order_le)
+ apply blast
+ apply (blast dest: plus_le_conv3)
+ apply (erule subst)
+ apply (blast intro: closedD)
+ done
+qed
+
+(*** semilat (err(Union AS)) ***)
+
+(* FIXME? *)
+lemma all_bex_swap_lemma [iff]:
+ "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))"
+ by blast
+
+lemma closed_err_Union_lift2I:
+ "[| !A:AS. closed (err A) (lift2 f); AS ~= {};
+ !A:AS.!B:AS. A~=B --> (!a:A.!b:B. a +_f b = Err) |]
+ ==> closed (err(Union AS)) (lift2 f)"
+apply (unfold closed_def err_def)
+apply simp
+apply clarify
+apply simp
+apply fast
+done
+
+(* If AS = {} the thm collapses to
+ order r & closed {Err} f & Err +_f Err = Err
+ which may not hold *)
+lemma err_semilat_UnionI:
+ "[| !A:AS. err_semilat(A, r, f); AS ~= {};
+ !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |]
+ ==> err_semilat(Union AS, r, f)"
+apply (unfold semilat_def sl_def)
+apply (simp add: closed_err_Union_lift2I)
+apply (rule conjI)
+ apply blast
+apply (simp add: err_def)
+apply (rule conjI)
+ apply clarify
+ apply (rename_tac A a u B b)
+ apply (case_tac "A = B")
+ apply simp
+ apply simp
+apply (rule conjI)
+ apply clarify
+ apply (rename_tac A a u B b)
+ apply (case_tac "A = B")
+ apply simp
+ apply simp
+apply clarify
+apply (rename_tac A ya yb B yd z C c a b)
+apply (case_tac "A = B")
+ apply (case_tac "A = C")
+ apply simp
+ apply (rotate_tac -1)
+ apply simp
+apply (rotate_tac -1)
+apply (case_tac "B = C")
+ apply simp
+apply (rotate_tac -1)
+apply simp
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Kildall.thy Mon Nov 20 16:37:42 2000 +0100
@@ -0,0 +1,445 @@
+(* Title: HOL/BCV/Kildall.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TUM
+
+Kildall's algorithm
+*)
+
+header "Kildall's Algorithm"
+
+theory Kildall = DFA_Framework:
+
+constdefs
+ bounded :: "(nat => nat list) => nat => bool"
+"bounded succs n == !p<n. !q:set(succs p). q<n"
+
+ pres_type :: "(nat => 's => 's) => nat => 's set => bool"
+"pres_type step n A == !s:A. !p<n. step p s : A"
+
+ mono :: "'s ord => (nat => 's => 's) => nat => 's set => bool"
+"mono r step n A ==
+ !s p t. s : A & p < n & s <=_r t --> step p s <=_r step p t"
+
+consts
+ iter :: "('s sl * (nat => 's => 's) * (nat => nat list))
+ * 's list * nat set => 's list"
+ propa :: "'s binop => nat list => 's => 's list => nat set => 's list * nat set"
+
+primrec
+"propa f [] t ss w = (ss,w)"
+"propa f (q#qs) t ss w = (let u = t +_f ss!q;
+ w' = (if u = ss!q then w else insert q w)
+ in propa f qs t (ss[q := u]) w')"
+
+recdef iter
+ "same_fst (%((A,r,f),step,succs). semilat(A,r,f) & acc r)
+ (%((A,r,f),step,succs).
+ {(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset)"
+"iter(((A,r,f),step,succs),ss,w) =
+ (if semilat(A,r,f) & acc r & (!p:w. p < size ss) &
+ bounded succs (size ss) & set ss <= A & pres_type step (size ss) A
+ then if w={} then ss
+ else let p = SOME p. p : w
+ in iter(((A,r,f),step,succs),
+ propa f (succs p) (step p (ss!p)) ss (w-{p}))
+ else arbitrary)"
+
+constdefs
+ unstables ::
+ "'s binop => (nat => 's => 's) => (nat => nat list) => 's list => nat set"
+"unstables f step succs ss ==
+ {p. p < size ss & (? q:set(succs p). step p (ss!p) +_f ss!q ~= ss!q)}"
+
+ kildall :: "'s sl => (nat => 's => 's) => (nat => nat list)
+ => 's list => 's list"
+"kildall Arf step succs ss ==
+ iter((Arf,step,succs),ss,unstables (snd(snd Arf)) step succs ss)"
+
+consts merges :: "'s binop => 's => nat list => 's list => 's list"
+primrec
+"merges f s [] ss = ss"
+"merges f s (p#ps) ss = merges f s ps (ss[p := s +_f ss!p])"
+
+
+lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric];
+
+
+lemma pres_typeD:
+ "[| pres_type step n A; s:A; p<n |] ==> step p s : A"
+ by (unfold pres_type_def, blast)
+
+lemma boundedD:
+ "[| bounded succs n; p < n; q : set(succs p) |] ==> q < n"
+ by (unfold bounded_def, blast)
+
+lemma monoD:
+ "[| mono r step n A; p < n; s:A; s <=_r t |] ==> step p s <=_r step p t"
+ by (unfold mono_def, blast)
+
+(** merges **)
+
+lemma length_merges [rule_format, simp]:
+ "!ss. size(merges f t ps ss) = size ss"
+ by (induct_tac ps, auto)
+
+lemma merges_preserves_type [rule_format, simp]:
+ "[| semilat(A,r,f) |] ==>
+ !xs. xs : list n A --> x : A --> (!p : set ps. p<n)
+ --> merges f x ps xs : list n A"
+ apply (frule semilatDclosedI)
+ apply (unfold closed_def)
+ apply (induct_tac ps)
+ apply auto
+ done
+
+lemma merges_incr [rule_format]:
+ "[| semilat(A,r,f) |] ==>
+ !xs. xs : list n A --> x : A --> (!p:set ps. p<size xs) --> xs <=[r] merges f x ps xs"
+ apply (induct_tac ps)
+ apply simp
+ apply simp
+ apply clarify
+ apply (rule order_trans)
+ apply simp
+ apply (erule list_update_incr)
+ apply assumption
+ apply simp
+ apply simp
+ apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
+ done
+
+lemma merges_same_conv [rule_format]:
+ "[| semilat(A,r,f) |] ==>
+ (!xs. xs : list n A --> x:A --> (!p:set ps. p<size xs) -->
+ (merges f x ps xs = xs) = (!p:set ps. x <=_r xs!p))"
+ apply (induct_tac ps)
+ apply simp
+ apply clarsimp
+ apply (rename_tac p ps xs)
+ apply (rule iffI)
+ apply (rule context_conjI)
+ apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")
+ apply (force dest!: le_listD simp add: nth_list_update)
+ apply (erule subst, rule merges_incr)
+ apply assumption
+ apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
+ apply assumption
+ apply simp
+ apply clarify
+ apply (rotate_tac -2)
+ apply (erule allE)
+ apply (erule impE)
+ apply assumption
+ apply (erule impE)
+ apply assumption
+ apply (drule bspec)
+ apply assumption
+ apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
+ apply clarify
+ apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
+ done
+
+
+lemma list_update_le_listI [rule_format]:
+ "set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->
+ x <=_r ys!p --> semilat(A,r,f) --> x:A -->
+ xs[p := x +_f xs!p] <=[r] ys"
+ apply (unfold Listn.le_def lesub_def semilat_def)
+ apply (simp add: list_all2_conv_all_nth nth_list_update)
+ done
+
+lemma merges_pres_le_ub:
+ "[| semilat(A,r,f); t:A; set ts <= A; set ss <= A;
+ !p. p:set ps --> t <=_r ts!p;
+ !p. p:set ps --> p<size ts;
+ ss <=[r] ts |]
+ ==> merges f t ps ss <=[r] ts"
+proof -
+ { fix A r f t ts ps
+ have
+ "!!qs. [| semilat(A,r,f); set ts <= A; t:A;
+ !p. p:set ps --> t <=_r ts!p;
+ !p. p:set ps --> p<size ts |] ==>
+ set qs <= set ps -->
+ (!ss. set ss <= A --> ss <=[r] ts --> merges f t qs ss <=[r] ts)"
+ apply (induct_tac qs)
+ apply simp
+ apply (simp (no_asm_simp))
+ apply clarify
+ apply (rotate_tac -2)
+ apply simp
+ apply (erule allE, erule impE, erule_tac [2] mp)
+ apply (simp (no_asm_simp) add: closedD)
+ apply (simp add: list_update_le_listI)
+ done
+ } note this [dest]
+
+ case antecedent
+ thus ?thesis by blast
+qed
+
+
+lemma nth_merges [rule_format]:
+ "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A -->
+ (!p:set ps. p<n) -->
+ (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)"
+ apply (induct_tac "ps")
+ apply simp
+ apply (simp add: nth_list_update closedD listE_nth_in)
+ done
+
+
+(** propa **)
+
+lemma decomp_propa [rule_format]:
+ "!ss w. (!q:set qs. q < size ss) -->
+ propa f qs t ss w =
+ (merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)"
+ apply (induct_tac qs)
+ apply simp
+ apply (simp (no_asm))
+ apply clarify
+ apply (rule conjI)
+ apply (simp add: nth_list_update)
+ apply blast
+ apply (simp add: nth_list_update)
+ apply blast
+ done
+
+(** iter **)
+
+ML_setup {*
+let
+val thy = the_context ()
+val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter";
+in
+goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
+by (REPEAT(rtac wf_same_fstI 1));
+by (split_all_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [thm "lesssub_def"]) 1);
+by (REPEAT(rtac wf_same_fstI 1));
+by (rtac wf_lex_prod 1);
+ by (rtac wf_finite_psubset 2);
+by (Clarify_tac 1);
+by (dtac (thm "semilatDorderI" RS (thm "acc_le_listI")) 1);
+ by (assume_tac 1);
+by (rewrite_goals_tac [thm "acc_def",thm "lesssub_def"]);
+by (assume_tac 1);
+qed "iter_wf"
+end
+*}
+
+lemma inter_tc_lemma:
+ "[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==>
+ ss <[r] merges f t qs ss |
+ merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w"
+ apply (unfold lesssub_def)
+ apply (simp (no_asm_simp) add: merges_incr)
+ apply (rule impI)
+ apply (rule merges_same_conv [THEN iffD1, elim_format])
+ apply assumption+
+ defer
+ apply (rule sym, assumption)
+ apply (simp cong add: conj_cong add: le_iff_plus_unchanged [symmetric])
+ apply (blast intro!: psubsetI elim: equalityE)
+ apply simp
+ done
+
+ML_setup {*
+let
+val thy = the_context ()
+val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter";
+in
+goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc));
+by (asm_simp_tac (simpset() addsimps [same_fst_def,thm "pres_type_def"]) 1);
+by (clarify_tac (claset() delrules [disjCI]) 1);
+by (subgoal_tac "(@p. p:w) : w" 1);
+ by (fast_tac (claset() addIs [someI]) 2);
+by (subgoal_tac "ss : list (size ss) A" 1);
+ by (blast_tac (claset() addSIs [thm "listI"]) 2);
+by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
+ by (blast_tac (claset() addDs [thm "boundedD"]) 2);
+by (rotate_tac 1 1);
+by (asm_full_simp_tac (simpset() delsimps [thm "listE_length"]
+ addsimps [thm "decomp_propa",finite_psubset_def,thm "inter_tc_lemma",
+ bounded_nat_set_is_finite]) 1);
+qed "iter_tc"
+end
+*}
+
+
+lemma iter_induct:
+ "(!!A r f step succs ss w.
+ (!p. p = (@ p. p : w) & w ~= {} & semilat(A,r,f) & acc r &
+ (!p:w. p < length ss) & bounded succs (length ss) &
+ set ss <= A & pres_type step (length ss) A
+ --> P A r f step succs (merges f (step p (ss!p)) (succs p) ss)
+ ({q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))
+ ==> P A r f step succs ss w) ==> P A r f step succs ss w"
+proof -
+ case antecedent
+ show ?thesis
+ apply (rule_tac P = P in iter_tc [THEN iter_wf [THEN iter.induct]])
+ apply (rule antecedent)
+ apply clarify
+ apply simp
+ apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
+ apply (rotate_tac -1)
+ apply (simp add: decomp_propa)
+ apply (subgoal_tac "(@p. p:w) : w")
+ apply (blast dest: boundedD)
+ apply (fast intro: someI)
+ done
+qed
+
+lemma iter_unfold:
+ "[| semilat(A,r,f); acc r; set ss <= A; pres_type step (length ss) A;
+ bounded succs (size ss); !p:w. p<size ss |] ==>
+ iter(((A,r,f),step,succs),ss,w) =
+ (if w={} then ss
+ else let p = SOME p. p : w
+ in iter(((A,r,f),step,succs),merges f (step p (ss!p)) (succs p) ss,
+ {q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))"
+ apply (rule iter_tc [THEN iter_wf [THEN iter.simps [THEN trans]]])
+ apply simp
+ apply (rule impI)
+ apply (subst decomp_propa)
+ apply (subgoal_tac "(@p. p:w) : w")
+ apply (blast dest: boundedD)
+ apply (fast intro: someI)
+ apply simp
+ done
+
+lemma stable_pres_lemma:
+ "[| semilat (A,r,f); pres_type step n A; bounded succs n;
+ ss : list n A; p : w; ! q:w. q < n;
+ ! q. q < n --> q ~: w --> stable r step succs ss q; q < n;
+ q : set (succs p) --> step p (ss ! p) +_f ss ! q = ss ! q;
+ q ~: w | q = p |]
+ ==> stable r step succs (merges f (step p (ss!p)) (succs p) ss) q"
+ apply (unfold stable_def)
+ apply (subgoal_tac "step p (ss!p) : A")
+ defer
+ apply (blast intro: listE_nth_in pres_typeD)
+ apply simp
+ apply clarify
+ apply (subst nth_merges)
+ apply assumption
+ apply assumption
+ prefer 2
+ apply assumption
+ apply (blast dest: boundedD)
+ apply (blast dest: boundedD)
+ apply (subst nth_merges)
+ apply assumption
+ apply assumption
+ prefer 2
+ apply assumption
+ apply (blast dest: boundedD)
+ apply (blast dest: boundedD)
+ apply simp
+ apply (rule conjI)
+ apply clarify
+ apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in
+ intro: order_trans dest: boundedD)
+ apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in
+ intro: order_trans dest: boundedD)
+ done
+
+lemma merges_bounded_lemma [rule_format]:
+ "[| semilat (A,r,f); mono r step n A; bounded succs n;
+ step p (ss!p) : A; ss : list n A; ts : list n A; p < n;
+ ss <=[r] ts; ! p. p < n --> stable r step succs ts p |]
+ ==> merges f (step p (ss!p)) (succs p) ss <=[r] ts"
+ apply (unfold stable_def)
+ apply (blast intro!: listE_set monoD listE_nth_in le_listD less_lengthI
+ intro: merges_pres_le_ub order_trans
+ dest: pres_typeD boundedD)
+ done
+
+ML_setup {*
+Unify.trace_bound := 80;
+Unify.search_bound := 90;
+*}
+
+lemma iter_properties [rule_format]:
+ "semilat(A,r,f) & acc r & pres_type step n A & mono r step n A &
+ bounded succs n & (! p:w. p < n) & ss:list n A &
+ (!p<n. p~:w --> stable r step succs ss p)
+ --> iter(((A,r,f),step,succs),ss,w) : list n A &
+ stables r step succs (iter(((A,r,f),step,succs),ss,w)) &
+ ss <=[r] iter(((A,r,f),step,succs),ss,w) &
+ (! ts:list n A.
+ ss <=[r] ts & stables r step succs ts -->
+ iter(((A,r,f),step,succs),ss,w) <=[r] ts)"
+ apply (unfold stables_def)
+ apply (rule_tac A = A and r = r and f = f and step = step and ss = ss and w = w in iter_induct)
+ apply clarify
+ apply (frule listE_length)
+ apply hypsubst
+ apply (subst iter_unfold)
+ apply assumption
+ apply assumption
+ apply (simp (no_asm_simp))
+ apply assumption
+ apply assumption
+ apply assumption
+ apply (simp (no_asm_simp) del: listE_length)
+ apply (rule impI)
+ apply (erule allE)
+ apply (erule impE)
+ apply (simp (no_asm_simp) del: listE_length)
+ apply (subgoal_tac "(@p. p:w) : w")
+ prefer 2
+ apply (fast intro: someI)
+ apply (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A")
+ prefer 2
+ apply (blast intro: pres_typeD listE_nth_in)
+ apply (erule impE)
+ apply (simp (no_asm_simp) del: listE_length le_iff_plus_unchanged [symmetric])
+ apply (rule conjI)
+ apply (blast dest: boundedD)
+ apply (rule conjI)
+ apply (blast intro: merges_preserves_type dest: boundedD)
+ apply clarify
+ apply (blast intro!: stable_pres_lemma)
+ apply (simp (no_asm_simp) del: listE_length)
+ apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
+ prefer 2
+ apply (blast dest: boundedD)
+ apply (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A")
+ prefer 2
+ apply (blast intro: pres_typeD)
+ apply (rule conjI)
+ apply (blast intro!: merges_incr intro: le_list_trans)
+ apply clarify
+ apply (drule bspec, assumption, erule mp)
+ apply (simp del: listE_length)
+ apply (blast intro: merges_bounded_lemma)
+ done
+
+
+lemma is_dfa_kildall:
+ "[| semilat(A,r,f); acc r; pres_type step n A;
+ mono r step n A; bounded succs n|]
+ ==> is_dfa r (kildall (A,r,f) step succs) step succs n A"
+ apply (unfold is_dfa_def kildall_def)
+ apply clarify
+ apply simp
+ apply (rule iter_properties)
+ apply (simp add: unstables_def stable_def)
+ apply (blast intro!: le_iff_plus_unchanged [THEN iffD2] listE_nth_in
+ dest: boundedD pres_typeD)
+ done
+
+lemma is_bcv_kildall:
+ "[| semilat(A,r,f); acc r; top r T;
+ pres_type step n A; bounded succs n;
+ mono r step n A |]
+ ==> is_bcv r T step succs n A (kildall (A,r,f) step succs)"
+ apply (intro is_bcv_dfa is_dfa_kildall semilatDorderI)
+ apply assumption+
+ done
+
+end
--- a/src/HOL/MicroJava/BV/LBVComplete.thy Sat Nov 18 19:48:34 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVComplete.thy Mon Nov 20 16:37:42 2000 +0100
@@ -83,44 +83,41 @@
lemma wtl_inst_mono:
- "[| wtl_inst i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi;
+ "[| wtl_inst i G rT s1 cert mpc pc = OK s1'; fits ins cert phi;
pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
- \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mpc pc = Ok s2' \<and> (G \<turnstile> s2' <=' s1')"
+ \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
proof -
assume pc: "pc < length ins" "i = ins!pc"
- assume wtl: "wtl_inst i G rT s1 cert mpc pc = Ok s1'"
+ assume wtl: "wtl_inst i G rT s1 cert mpc pc = OK s1'"
assume fits: "fits ins cert phi"
assume G: "G \<turnstile> s2 <=' s1"
let "?step s" = "step i G s"
from wtl G
- have app: "app i G rT s2" by (auto simp add: wtl_inst_Ok app_mono)
+ have app: "app i G rT s2" by (auto simp add: wtl_inst_OK app_mono)
from wtl G
- have step: "succs i pc \<noteq> [] ==> G \<turnstile> ?step s2 <=' ?step s1"
- by - (drule step_mono, auto simp add: wtl_inst_Ok)
+ have step: "G \<turnstile> ?step s2 <=' ?step s1"
+ by (auto intro: step_mono simp add: wtl_inst_OK)
- {
+ { also
fix pc'
- assume 0: "pc' \<in> set (succs i pc)" "pc' \<noteq> pc+1"
- hence "succs i pc \<noteq> []" by auto
- hence "G \<turnstile> ?step s2 <=' ?step s1" by (rule step)
- also
- from wtl 0
+ assume "pc' \<in> set (succs i pc)" "pc' \<noteq> pc+1"
+ with wtl
have "G \<turnstile> ?step s1 <=' cert!pc'"
- by (auto simp add: wtl_inst_Ok)
+ by (auto simp add: wtl_inst_OK)
finally
have "G\<turnstile> ?step s2 <=' cert!pc'" .
} note cert = this
- have "\<exists>s2'. wtl_inst i G rT s2 cert mpc pc = Ok s2' \<and> G \<turnstile> s2' <=' s1'"
+ have "\<exists>s2'. wtl_inst i G rT s2 cert mpc pc = OK s2' \<and> G \<turnstile> s2' <=' s1'"
proof (cases "pc+1 \<in> set (succs i pc)")
case True
with wtl
- have s1': "s1' = ?step s1" by (simp add: wtl_inst_Ok)
+ have s1': "s1' = ?step s1" by (simp add: wtl_inst_OK)
- have "wtl_inst i G rT s2 cert mpc pc = Ok (?step s2) \<and> G \<turnstile> ?step s2 <=' s1'"
+ have "wtl_inst i G rT s2 cert mpc pc = OK (?step s2) \<and> G \<turnstile> ?step s2 <=' s1'"
(is "?wtl \<and> ?G")
proof
from True s1'
@@ -128,17 +125,17 @@
from True app wtl
show ?wtl
- by (clarsimp intro!: cert simp add: wtl_inst_Ok)
+ by (clarsimp intro!: cert simp add: wtl_inst_OK)
qed
thus ?thesis by blast
next
case False
with wtl
- have "s1' = cert ! Suc pc" by (simp add: wtl_inst_Ok)
+ have "s1' = cert ! Suc pc" by (simp add: wtl_inst_OK)
with False app wtl
- have "wtl_inst i G rT s2 cert mpc pc = Ok s1' \<and> G \<turnstile> s1' <=' s1'"
- by (clarsimp intro!: cert simp add: wtl_inst_Ok)
+ have "wtl_inst i G rT s2 cert mpc pc = OK s1' \<and> G \<turnstile> s1' <=' s1'"
+ by (clarsimp intro!: cert simp add: wtl_inst_OK)
thus ?thesis by blast
qed
@@ -148,11 +145,11 @@
lemma wtl_cert_mono:
- "[| wtl_cert i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi;
+ "[| wtl_cert i G rT s1 cert mpc pc = OK s1'; fits ins cert phi;
pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
- \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mpc pc = Ok s2' \<and> (G \<turnstile> s2' <=' s1')"
+ \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
proof -
- assume wtl: "wtl_cert i G rT s1 cert mpc pc = Ok s1'" and
+ assume wtl: "wtl_cert i G rT s1 cert mpc pc = OK s1'" and
fits: "fits ins cert phi" "pc < length ins"
"G \<turnstile> s2 <=' s1" "i = ins!pc"
@@ -170,11 +167,11 @@
by - (rule sup_state_opt_trans, auto simp add: wtl_cert_def split: if_splits)
from Some wtl
- have "wtl_inst i G rT (Some a) cert mpc pc = Ok s1'"
+ have "wtl_inst i G rT (Some a) cert mpc pc = OK s1'"
by (simp add: wtl_cert_def split: if_splits)
with G fits
- have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mpc pc = Ok s2' \<and>
+ have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mpc pc = OK s2' \<and>
(G \<turnstile> s2' <=' s1')"
by - (rule wtl_inst_mono, (simp add: wtl_cert_def)+)
@@ -209,23 +206,23 @@
from app pc cert pc'
show ?thesis
- by (auto simp add: wtl_inst_Ok)
+ by (auto simp add: wtl_inst_OK)
qed
lemma wt_less_wtl:
"[| wt_instr (ins!pc) G rT phi max_pc pc;
- wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s;
+ wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s;
fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==>
G \<turnstile> s <=' phi ! Suc pc"
proof -
assume wt: "wt_instr (ins!pc) G rT phi max_pc pc"
- assume wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
+ assume wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
assume fits: "fits ins cert phi"
assume pc: "Suc pc < length ins" "length ins = max_pc"
{ assume suc: "Suc pc \<in> set (succs (ins ! pc) pc)"
with wtl have "s = step (ins!pc) G (phi!pc)"
- by (simp add: wtl_inst_Ok)
+ by (simp add: wtl_inst_OK)
also from suc wt have "G \<turnstile> ... <=' phi!Suc pc"
by (simp add: wt_instr_def)
finally have ?thesis .
@@ -236,7 +233,7 @@
with wtl
have "s = cert!Suc pc"
- by (simp add: wtl_inst_Ok)
+ by (simp add: wtl_inst_OK)
with fits pc
have ?thesis
by - (cases "cert!Suc pc", simp, drule fitsD2, assumption+, simp)
@@ -281,11 +278,11 @@
lemma wt_less_wtl_cert:
"[| wt_instr (ins!pc) G rT phi max_pc pc;
- wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s;
+ wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = OK s;
fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==>
G \<turnstile> s <=' phi ! Suc pc"
proof -
- assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
+ assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
assume wti: "wt_instr (ins!pc) G rT phi max_pc pc"
"fits ins cert phi"
@@ -293,7 +290,7 @@
{ assume "cert!pc = None"
with wtl
- have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
+ have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
by (simp add: wtl_cert_def)
with wti
have ?thesis
@@ -306,7 +303,7 @@
have "cert!pc = phi!pc"
by - (rule fitsD2, simp+)
with c wtl
- have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
+ have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
by (simp add: wtl_cert_def)
with wti
have ?thesis
@@ -378,13 +375,13 @@
from c wti fits l True
obtain s'' where
- "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc = Ok s''"
+ "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc = OK s''"
"G \<turnstile> s'' <=' phi ! Suc pc"
by clarsimp (drule wt_less_wtl_cert, auto)
moreover
from calculation fits G l
obtain s' where
- c': "wtl_cert (all_ins!pc) G rT s cert (length all_ins) pc = Ok s'" and
+ c': "wtl_cert (all_ins!pc) G rT s cert (length all_ins) pc = OK s'" and
"G \<turnstile> s' <=' s''"
by - (drule wtl_cert_mono, auto)
ultimately
--- a/src/HOL/MicroJava/BV/LBVCorrect.thy Sat Nov 18 19:48:34 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVCorrect.thy Mon Nov 20 16:37:42 2000 +0100
@@ -14,7 +14,7 @@
fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] => bool"
"fits phi is G rT s0 cert ==
(\<forall>pc s1. pc < length is -->
- (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 -->
+ (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1 -->
(case cert!pc of None => phi!pc = s1
| Some t => phi!pc = Some t)))"
@@ -22,19 +22,19 @@
make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] => method_type"
"make_phi is G rT s0 cert ==
map (\<lambda>pc. case cert!pc of
- None => val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)
+ None => ok_val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)
| Some t => Some t) [0..length is(]"
lemma fitsD_None:
"[|fits phi is G rT s0 cert; pc < length is;
- wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1;
+ wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1;
cert ! pc = None|] ==> phi!pc = s1"
by (auto simp add: fits_def)
lemma fitsD_Some:
"[|fits phi is G rT s0 cert; pc < length is;
- wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1;
+ wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1;
cert ! pc = Some t|] ==> phi!pc = Some t"
by (auto simp add: fits_def)
@@ -46,7 +46,7 @@
lemma make_phi_None:
"[| pc < length is; cert!pc = None |] ==>
make_phi is G rT s0 cert ! pc =
- val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)"
+ ok_val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)"
by (simp add: make_phi_def)
lemma exists_phi:
@@ -61,14 +61,14 @@
qed
lemma fits_lemma1:
- "[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |]
+ "[| wtl_inst_list is G rT cert (length is) 0 s = OK s'; fits phi is G rT s cert |]
==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
proof (intro strip)
fix pc t
- assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'"
+ assume "wtl_inst_list is G rT cert (length is) 0 s = OK s'"
then
obtain s'' where
- "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s''"
+ "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s''"
by (blast dest: wtl_take)
moreover
assume "fits phi is G rT s cert"
@@ -81,8 +81,8 @@
lemma wtl_suc_pc:
"[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
- wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s';
- wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s'';
+ wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s';
+ wtl_cert (is!pc) G rT s' cert (length is) pc = OK s'';
fits phi is G rT s cert; Suc pc < length is |] ==>
G \<turnstile> s'' <=' phi ! Suc pc"
proof -
@@ -90,11 +90,11 @@
assume all: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
assume fits: "fits phi is G rT s cert"
- assume wtl: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
- wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" and
+ assume wtl: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'" and
+ wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''" and
pc: "Suc pc < length is"
- hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''"
+ hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = OK s''"
by (rule wtl_Suc)
from all
@@ -111,7 +111,7 @@
by (auto simp add: neq_Nil_conv simp del: length_drop)
with app wts pc
obtain x where
- "wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x"
+ "wtl_cert l G rT s'' cert (length is) (Suc pc) = OK x"
by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
@@ -144,8 +144,8 @@
then
obtain s' s'' where
- w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
- c: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
+ w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'" and
+ c: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''"
by - (drule wtl_all, auto)
from fits wtl pc
@@ -158,7 +158,7 @@
by - (drule fitsD_None)
from pc c cert_None cert_Some
- have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = Ok s''"
+ have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = OK s''"
by (auto simp add: wtl_cert_def split: if_splits option.splits)
{ fix pc'
@@ -166,14 +166,14 @@
with wti
have less: "pc' < length is"
- by (simp add: wtl_inst_Ok)
+ by (simp add: wtl_inst_OK)
have "G \<turnstile> step (is!pc) G (phi!pc) <=' phi ! pc'"
proof (cases "pc' = Suc pc")
case False
with wti pc'
have G: "G \<turnstile> step (is ! pc) G (phi ! pc) <=' cert ! pc'"
- by (simp add: wtl_inst_Ok)
+ by (simp add: wtl_inst_OK)
hence "cert!pc' = None ==> step (is ! pc) G (phi ! pc) = None"
by simp
@@ -197,7 +197,7 @@
case True
with pc' wti
have "step (is ! pc) G (phi ! pc) = s''"
- by (simp add: wtl_inst_Ok)
+ by (simp add: wtl_inst_OK)
also
from w c fits pc wtl
have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc"
@@ -213,7 +213,7 @@
with wti
show ?thesis
- by (auto simp add: wtl_inst_Ok wt_instr_def)
+ by (auto simp add: wtl_inst_OK wt_instr_def)
qed
@@ -228,7 +228,7 @@
assume pc: "0 < length is"
from wtl
- have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = Ok s"
+ have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = OK s"
by simp
with fits pc
@@ -244,7 +244,7 @@
by (simp add: neq_Nil_conv) (elim, rule that)
with wtl
obtain s' where
- "wtl_cert x G rT s cert (length is) 0 = Ok s'"
+ "wtl_cert x G rT s cert (length is) 0 = OK s'"
by simp (elim, rule that, simp)
hence
"!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
@@ -259,7 +259,7 @@
lemma wtl_method_correct:
"wtl_method G C pTs rT mxl ins cert ==> \<exists> phi. wt_method G C pTs rT mxl ins phi"
proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
- let "?s0" = "Some ([], Ok (Class C) # map Ok pTs @ replicate mxl Err)"
+ let "?s0" = "Some ([], OK (Class C) # map OK pTs @ replicate mxl Err)"
assume pc: "0 < length ins"
assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
--- a/src/HOL/MicroJava/BV/LBVSpec.thy Sat Nov 18 19:48:34 2000 +0100
+++ b/src/HOL/MicroJava/BV/LBVSpec.thy Mon Nov 20 16:37:42 2000 +0100
@@ -25,7 +25,7 @@
=> state_type option err"
"wtl_inst i G rT s cert max_pc pc ==
if app i G rT s \<and> check_cert i G s cert pc max_pc then
- if pc+1 mem (succs i pc) then Ok (step i G s) else Ok (cert!(pc+1))
+ if pc+1 mem (succs i pc) then OK (step i G s) else OK (cert!(pc+1))
else Err";
constdefs
@@ -42,7 +42,7 @@
wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count,
state_type option] => state_type option err"
primrec
- "wtl_inst_list [] G rT cert max_pc pc s = Ok s"
+ "wtl_inst_list [] G rT cert max_pc pc s = OK s"
"wtl_inst_list (i#is) G rT cert max_pc pc s =
(let s' = wtl_cert i G rT s cert max_pc pc in
strict (wtl_inst_list is G rT cert max_pc (pc+1)) s')";
@@ -55,7 +55,7 @@
in
0 < max_pc \<and>
wtl_inst_list ins G rT cert max_pc 0
- (Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err))) \<noteq> Err"
+ (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool"
"wtl_jvm_prog G cert ==
@@ -63,27 +63,27 @@
-lemma wtl_inst_Ok:
-"(wtl_inst i G rT s cert max_pc pc = Ok s') =
+lemma wtl_inst_OK:
+"(wtl_inst i G rT s cert max_pc pc = OK s') =
(app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc).
pc' < max_pc \<and> (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')) \<and>
(if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
by (auto simp add: wtl_inst_def check_cert_def set_mem_eq);
lemma strict_Some [simp]:
-"(strict f x = Ok y) = (\<exists> z. x = Ok z \<and> f z = Ok y)"
+"(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
by (cases x, auto)
lemma wtl_Cons:
"wtl_inst_list (i#is) G rT cert max_pc pc s \<noteq> Err =
- (\<exists>s'. wtl_cert i G rT s cert max_pc pc = Ok s' \<and>
+ (\<exists>s'. wtl_cert i G rT s cert max_pc pc = OK s' \<and>
wtl_inst_list is G rT cert max_pc (pc+1) s' \<noteq> Err)"
by (auto simp del: split_paired_Ex)
lemma wtl_append:
-"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = Ok s') =
- (\<exists>s''. wtl_inst_list a G rT cert mpc pc s = Ok s'' \<and>
- wtl_inst_list b G rT cert mpc (pc+length a) s'' = Ok s')"
+"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = OK s') =
+ (\<exists>s''. wtl_inst_list a G rT cert mpc pc s = OK s'' \<and>
+ wtl_inst_list b G rT cert mpc (pc+length a) s'' = OK s')"
(is "\<forall> s pc. ?C s pc a" is "?P a")
proof (induct ?P a)
@@ -101,24 +101,24 @@
case Err thus ?thesis by simp
next
fix s0
- assume Ok: "wtl_cert x G rT s cert mpc pc = Ok s0"
+ assume OK: "wtl_cert x G rT s cert mpc pc = OK s0"
with IH
have "?C s0 (Suc pc) xs" by blast
- with Ok
+ with OK
show ?thesis by simp
qed
qed
qed
lemma wtl_take:
- "wtl_inst_list is G rT cert mpc pc s = Ok s'' ==>
- \<exists>s'. wtl_inst_list (take pc' is) G rT cert mpc pc s = Ok s'"
+ "wtl_inst_list is G rT cert mpc pc s = OK s'' ==>
+ \<exists>s'. wtl_inst_list (take pc' is) G rT cert mpc pc s = OK s'"
proof -
- assume "wtl_inst_list is G rT cert mpc pc s = Ok s''"
+ assume "wtl_inst_list is G rT cert mpc pc s = OK s''"
- hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mpc pc s = Ok s''"
+ hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mpc pc s = OK s''"
by simp
thus ?thesis
@@ -144,13 +144,13 @@
qed
lemma wtl_Suc:
- "[| wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s';
- wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s'';
+ "[| wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s';
+ wtl_cert (is!pc) G rT s' cert (length is) pc = OK s'';
Suc pc < length is |] ==>
- wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''"
+ wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = OK s''"
proof -
- assume wtt: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'"
- assume wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
+ assume wtt: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'"
+ assume wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''"
assume pc: "Suc pc < length is"
hence "take (Suc pc) is = (take pc is)@[is!pc]"
@@ -164,8 +164,8 @@
lemma wtl_all:
"[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
pc < length is |] ==>
- \<exists>s' s''. wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s' \<and>
- wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
+ \<exists>s' s''. wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s' \<and>
+ wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''"
proof -
assume all: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Listn.thy Mon Nov 20 16:37:42 2000 +0100
@@ -0,0 +1,495 @@
+(* Title: HOL/BCV/Listn.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TUM
+
+Lists of a fixed length
+*)
+
+header "Fixed Length Lists"
+
+theory Listn = Err:
+
+constdefs
+
+ list :: "nat => 'a set => 'a list set"
+"list n A == {xs. length xs = n & set xs <= A}"
+
+ le :: "'a ord => ('a list)ord"
+"le r == list_all2 (%x y. x <=_r y)"
+
+syntax "@lesublist" :: "'a list => 'a ord => 'a list => bool"
+ ("(_ /<=[_] _)" [50, 0, 51] 50)
+syntax "@lesssublist" :: "'a list => 'a ord => 'a list => bool"
+ ("(_ /<[_] _)" [50, 0, 51] 50)
+translations
+ "x <=[r] y" == "x <=_(Listn.le r) y"
+ "x <[r] y" == "x <_(Listn.le r) y"
+
+constdefs
+ map2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
+"map2 f == (%xs ys. map (split f) (zip xs ys))"
+
+syntax "@plussublist" :: "'a list => ('a => 'b => 'c) => 'b list => 'c list"
+ ("(_ /+[_] _)" [65, 0, 66] 65)
+translations "x +[f] y" == "x +_(map2 f) y"
+
+consts coalesce :: "'a err list => 'a list err"
+primrec
+"coalesce [] = OK[]"
+"coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
+
+constdefs
+ sl :: "nat => 'a sl => 'a list sl"
+"sl n == %(A,r,f). (list n A, le r, map2 f)"
+
+ sup :: "('a => 'b => 'c err) => 'a list => 'b list => 'c list err"
+"sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
+
+ upto_esl :: "nat => 'a esl => 'a list esl"
+"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
+
+lemmas [simp] = set_update_subsetI
+
+lemma unfold_lesub_list:
+ "xs <=[r] ys == Listn.le r xs ys"
+ by (simp add: lesub_def)
+
+lemma Nil_le_conv [iff]:
+ "([] <=[r] ys) = (ys = [])"
+apply (unfold lesub_def Listn.le_def)
+apply simp
+done
+
+lemma Cons_notle_Nil [iff]:
+ "~ x#xs <=[r] []"
+apply (unfold lesub_def Listn.le_def)
+apply simp
+done
+
+
+lemma Cons_le_Cons [iff]:
+ "x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)"
+apply (unfold lesub_def Listn.le_def)
+apply simp
+done
+
+lemma Cons_less_Conss [simp]:
+ "order r ==>
+ x#xs <_(Listn.le r) y#ys =
+ (x <_r y & xs <=[r] ys | x = y & xs <_(Listn.le r) ys)"
+apply (unfold lesssub_def)
+apply blast
+done
+
+lemma list_update_le_cong:
+ "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";
+apply (unfold unfold_lesub_list)
+apply (unfold Listn.le_def)
+apply (simp add: list_all2_conv_all_nth nth_list_update)
+done
+
+
+lemma le_listD:
+ "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p"
+apply (unfold Listn.le_def lesub_def)
+apply (simp add: list_all2_conv_all_nth)
+done
+
+lemma le_list_refl:
+ "!x. x <=_r x ==> xs <=[r] xs"
+apply (unfold unfold_lesub_list)
+apply (simp add: Listn.le_def list_all2_conv_all_nth)
+done
+
+lemma le_list_trans:
+ "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs"
+apply (unfold unfold_lesub_list)
+apply (simp add: Listn.le_def list_all2_conv_all_nth)
+apply clarify
+apply simp
+apply (blast intro: order_trans)
+done
+
+lemma le_list_antisym:
+ "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys"
+apply (unfold unfold_lesub_list)
+apply (simp add: Listn.le_def list_all2_conv_all_nth)
+apply (rule nth_equalityI)
+ apply blast
+apply clarify
+apply simp
+apply (blast intro: order_antisym)
+done
+
+lemma order_listI [simp, intro!]:
+ "order r ==> order(Listn.le r)"
+apply (subst order_def)
+apply (blast intro: le_list_refl le_list_trans le_list_antisym
+ dest: order_refl)
+done
+
+
+lemma lesub_list_impl_same_size [simp]:
+ "xs <=[r] ys ==> size ys = size xs"
+apply (unfold Listn.le_def lesub_def)
+apply (simp add: list_all2_conv_all_nth)
+done
+
+lemma lesssub_list_impl_same_size:
+ "xs <_(Listn.le r) ys ==> size ys = size xs"
+apply (unfold lesssub_def)
+apply auto
+done
+
+lemma listI:
+ "[| length xs = n; set xs <= A |] ==> xs : list n A"
+apply (unfold list_def)
+apply blast
+done
+
+lemma listE_length [simp]:
+ "xs : list n A ==> length xs = n"
+apply (unfold list_def)
+apply blast
+done
+
+lemma less_lengthI:
+ "[| xs : list n A; p < n |] ==> p < length xs"
+ by simp
+
+lemma listE_set [simp]:
+ "xs : list n A ==> set xs <= A"
+apply (unfold list_def)
+apply blast
+done
+
+lemma list_0 [simp]:
+ "list 0 A = {[]}"
+apply (unfold list_def)
+apply auto
+done
+
+lemma in_list_Suc_iff:
+ "(xs : list (Suc n) A) = (? y:A. ? ys:list n A. xs = y#ys)"
+apply (unfold list_def)
+apply (case_tac "xs")
+apply auto
+done
+
+lemma Cons_in_list_Suc [iff]:
+ "(x#xs : list (Suc n) A) = (x:A & xs : list n A)";
+apply (simp add: in_list_Suc_iff)
+apply blast
+done
+
+lemma list_not_empty:
+ "? a. a:A ==> ? xs. xs : list n A";
+apply (induct "n")
+ apply simp
+apply (simp add: in_list_Suc_iff)
+apply blast
+done
+
+
+lemma nth_in [rule_format, simp]:
+ "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A"
+apply (induct "xs")
+ apply simp
+apply (simp add: nth_Cons split: nat.split)
+done
+
+lemma listE_nth_in:
+ "[| xs : list n A; i < n |] ==> (xs!i) : A"
+ by auto
+
+lemma listt_update_in_list [simp, intro!]:
+ "[| xs : list n A; x:A |] ==> xs[i := x] : list n A"
+apply (unfold list_def)
+apply simp
+done
+
+lemma plus_list_Nil [simp]:
+ "[] +[f] xs = []"
+apply (unfold plussub_def map2_def)
+apply simp
+done
+
+lemma plus_list_Cons [simp]:
+ "(x#xs) +[f] ys = (case ys of [] => [] | y#ys => (x +_f y)#(xs +[f] ys))"
+ by (simp add: plussub_def map2_def split: list.split)
+
+lemma length_plus_list [rule_format, simp]:
+ "!ys. length(xs +[f] ys) = min(length xs) (length ys)"
+apply (induct xs)
+ apply simp
+apply clarify
+apply (simp (no_asm_simp) split: list.split)
+done
+
+lemma nth_plus_list [rule_format, simp]:
+ "!xs ys i. length xs = n --> length ys = n --> i<n -->
+ (xs +[f] ys)!i = (xs!i) +_f (ys!i)"
+apply (induct n)
+ apply simp
+apply clarify
+apply (case_tac xs)
+ apply simp
+apply (force simp add: nth_Cons split: list.split nat.split)
+done
+
+
+lemma plus_list_ub1 [rule_format]:
+ "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |]
+ ==> xs <=[r] xs +[f] ys"
+apply (unfold unfold_lesub_list)
+apply (simp add: Listn.le_def list_all2_conv_all_nth)
+done
+
+lemma plus_list_ub2:
+ "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |]
+ ==> ys <=[r] xs +[f] ys"
+apply (unfold unfold_lesub_list)
+apply (simp add: Listn.le_def list_all2_conv_all_nth)
+done
+
+lemma plus_list_lub [rule_format]:
+ "semilat(A,r,f) ==> !xs ys zs. set xs <= A --> set ys <= A --> set zs <= A
+ --> size xs = n & size ys = n -->
+ xs <=[r] zs & ys <=[r] zs --> xs +[f] ys <=[r] zs"
+apply (unfold unfold_lesub_list)
+apply (simp add: Listn.le_def list_all2_conv_all_nth)
+done
+
+lemma list_update_incr [rule_format]:
+ "[| semilat(A,r,f); x:A |] ==> set xs <= A -->
+ (!i. i<size xs --> xs <=[r] xs[i := x +_f xs!i])"
+apply (unfold unfold_lesub_list)
+apply (simp add: Listn.le_def list_all2_conv_all_nth)
+apply (induct xs)
+ apply simp
+apply (simp add: in_list_Suc_iff)
+apply clarify
+apply (simp add: nth_Cons split: nat.split)
+done
+
+lemma acc_le_listI [intro!]:
+ "[| order r; acc r |] ==> acc(Listn.le r)"
+apply (unfold acc_def)
+apply (subgoal_tac
+ "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
+ apply (erule wf_subset)
+ apply (blast intro: lesssub_list_impl_same_size)
+apply (rule wf_UN)
+ prefer 2
+ apply clarify
+ apply (rename_tac m n)
+ apply (case_tac "m=n")
+ apply simp
+ apply (rule conjI)
+ apply (fast intro!: equals0I dest: not_sym)
+ apply (fast intro!: equals0I dest: not_sym)
+apply clarify
+apply (rename_tac n)
+apply (induct_tac n)
+ apply (simp add: lesssub_def cong: conj_cong)
+apply (rename_tac k)
+apply (simp add: wf_eq_minimal)
+apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
+apply clarify
+apply (rename_tac M m)
+apply (case_tac "? x xs. size xs = k & x#xs : M")
+ prefer 2
+ apply (erule thin_rl)
+ apply (erule thin_rl)
+ apply blast
+apply (erule_tac x = "{a. ? xs. size xs = k & a#xs:M}" in allE)
+apply (erule impE)
+ apply blast
+apply (thin_tac "? x xs. ?P x xs")
+apply clarify
+apply (rename_tac maxA xs)
+apply (erule_tac x = "{ys. size ys = size xs & maxA#ys : M}" in allE)
+apply (erule impE)
+ apply blast
+apply clarify
+apply (thin_tac "m : M")
+apply (thin_tac "maxA#xs : M")
+apply (rule bexI)
+ prefer 2
+ apply assumption
+apply clarify
+apply simp
+apply blast
+done
+
+lemma closed_listI:
+ "closed S f ==> closed (list n S) (map2 f)"
+apply (unfold closed_def)
+apply (induct n)
+ apply simp
+apply clarify
+apply (simp add: in_list_Suc_iff)
+apply clarify
+apply simp
+apply blast
+done
+
+
+lemma semilat_Listn_sl:
+ "!!L. semilat L ==> semilat (Listn.sl n L)"
+apply (unfold Listn.sl_def)
+apply (simp (no_asm_simp) only: split_tupled_all)
+apply (simp (no_asm) only: semilat_Def Product_Type.split)
+apply (rule conjI)
+ apply simp
+apply (rule conjI)
+ apply (simp only: semilatDclosedI closed_listI)
+apply (simp (no_asm) only: list_def)
+apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
+done
+
+
+lemma coalesce_in_err_list [rule_format]:
+ "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"
+apply (induct n)
+ apply simp
+apply clarify
+apply (simp add: in_list_Suc_iff)
+apply clarify
+apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split)
+apply force
+done
+
+lemma lem: "!!x xs. x +_(op #) xs = x#xs"
+ by (simp add: plussub_def)
+
+lemma coalesce_eq_OK1_D [rule_format]:
+ "semilat(err A, Err.le r, lift2 f) ==>
+ !xs. xs : list n A --> (!ys. ys : list n A -->
+ (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))"
+apply (induct n)
+ apply simp
+apply clarify
+apply (simp add: in_list_Suc_iff)
+apply clarify
+apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
+apply (force simp add: semilat_le_err_OK1)
+done
+
+lemma coalesce_eq_OK2_D [rule_format]:
+ "semilat(err A, Err.le r, lift2 f) ==>
+ !xs. xs : list n A --> (!ys. ys : list n A -->
+ (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))"
+apply (induct n)
+ apply simp
+apply clarify
+apply (simp add: in_list_Suc_iff)
+apply clarify
+apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
+apply (force simp add: semilat_le_err_OK2)
+done
+
+lemma lift2_le_ub:
+ "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z;
+ u:A; x <=_r u; y <=_r u |] ==> z <=_r u"
+apply (unfold semilat_Def plussub_def err_def)
+apply (simp add: lift2_def)
+apply clarify
+apply (rotate_tac -3)
+apply (erule thin_rl)
+apply (erule thin_rl)
+apply force
+done
+
+lemma coalesce_eq_OK_ub_D [rule_format]:
+ "semilat(err A, Err.le r, lift2 f) ==>
+ !xs. xs : list n A --> (!ys. ys : list n A -->
+ (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us
+ & us : list n A --> zs <=[r] us))"
+apply (induct n)
+ apply simp
+apply clarify
+apply (simp add: in_list_Suc_iff)
+apply clarify
+apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)
+apply clarify
+apply (rule conjI)
+ apply (blast intro: lift2_le_ub)
+apply blast
+done
+
+lemma lift2_eq_ErrD:
+ "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |]
+ ==> ~(? u:A. x <=_r u & y <=_r u)"
+ by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])
+
+
+lemma coalesce_eq_Err_D [rule_format]:
+ "[| semilat(err A, Err.le r, lift2 f) |]
+ ==> !xs. xs:list n A --> (!ys. ys:list n A -->
+ coalesce (xs +[f] ys) = Err -->
+ ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"
+apply (induct n)
+ apply simp
+apply clarify
+apply (simp add: in_list_Suc_iff)
+apply clarify
+apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
+ apply (blast dest: lift2_eq_ErrD)
+apply blast
+done
+
+lemma closed_err_lift2_conv:
+ "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)"
+apply (unfold closed_def)
+apply (simp add: err_def)
+done
+
+lemma closed_map2_list [rule_format]:
+ "closed (err A) (lift2 f) ==>
+ !xs. xs : list n A --> (!ys. ys : list n A -->
+ map2 f xs ys : list n (err A))"
+apply (unfold map2_def)
+apply (induct n)
+ apply simp
+apply clarify
+apply (simp add: in_list_Suc_iff)
+apply clarify
+apply (simp add: plussub_def closed_err_lift2_conv)
+apply blast
+done
+
+lemma closed_lift2_sup:
+ "closed (err A) (lift2 f) ==>
+ closed (err (list n A)) (lift2 (sup f))"
+ by (fastsimp simp add: closed_def plussub_def sup_def lift2_def
+ coalesce_in_err_list closed_map2_list
+ split: err.split)
+
+lemma err_semilat_sup:
+ "err_semilat (A,r,f) ==>
+ err_semilat (list n A, Listn.le r, sup f)"
+apply (unfold Err.sl_def)
+apply (simp only: Product_Type.split)
+apply (simp (no_asm) only: semilat_Def plussub_def)
+apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
+apply (rule conjI)
+ apply (drule semilatDorderI)
+ apply simp
+apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)
+apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
+apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D)
+done
+
+lemma err_semilat_upto_esl:
+ "!!L. err_semilat L ==> err_semilat(upto_esl m L)"
+apply (unfold Listn.upto_esl_def)
+apply (simp (no_asm_simp) only: split_tupled_all)
+apply simp
+apply (fastsimp intro!: err_semilat_UnionI err_semilat_sup
+ dest: lesub_list_impl_same_size
+ simp add: plussub_def Listn.sup_def)
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Opt.thy Mon Nov 20 16:37:42 2000 +0100
@@ -0,0 +1,359 @@
+(* Title: HOL/BCV/Opt.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TUM
+
+More about options
+*)
+
+header "More about Options"
+
+theory Opt = Err:
+
+constdefs
+ le :: "'a ord => 'a option ord"
+"le r o1 o2 == case o2 of None => o1=None |
+ Some y => (case o1 of None => True |
+ Some x => x <=_r y)"
+
+ opt :: "'a set => 'a option set"
+"opt A == insert None {x . ? y:A. x = Some y}"
+
+ sup :: "'a ebinop => 'a option ebinop"
+"sup f o1 o2 ==
+ case o1 of None => OK o2 | Some x => (case o2 of None => OK o1
+ | Some y => (case f x y of Err => Err | OK z => OK (Some z)))"
+
+ esl :: "'a esl => 'a option esl"
+"esl == %(A,r,f). (opt A, le r, sup f)"
+
+lemma unfold_le_opt:
+ "o1 <=_(le r) o2 =
+ (case o2 of None => o1=None |
+ Some y => (case o1 of None => True | Some x => x <=_r y))"
+apply (unfold lesub_def le_def)
+apply (rule refl)
+done
+
+lemma le_opt_refl:
+ "order r ==> o1 <=_(le r) o1"
+by (simp add: unfold_le_opt split: option.split)
+
+lemma le_opt_trans [rule_format]:
+ "order r ==>
+ o1 <=_(le r) o2 --> o2 <=_(le r) o3 --> 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 ==> o1 <=_(le r) o2 --> o2 <=_(le r) o1 --> 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 ==> order(le r)"
+apply (subst 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) = (? y. ox = Some y & 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 : opt A"
+by (simp add: opt_def)
+
+lemma Some_in_opt [iff]:
+ "(Some x : opt A) = (x:A)"
+apply (unfold opt_def)
+apply auto
+done
+
+
+lemma semilat_opt:
+ "!!L. err_semilat L ==> 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 : ?A"
+ assume y: "y : ?A"
+
+ {
+ fix a b
+ assume ab: "x = OK a" "y = OK b"
+
+ with x
+ have a: "!!c. a = Some c ==> c : A"
+ by (clarsimp simp add: opt_def)
+
+ from ab y
+ have b: "!!d. b = Some d ==> d : A"
+ by (clarsimp simp add: opt_def)
+
+ { fix c d assume "a = Some c" "b = Some d"
+ with ab x y
+ have "c:A & d:A"
+ by (simp add: err_def opt_def Bex_def)
+ with clo
+ have "f c d : 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 : A" by simp
+ } note f_closed = this
+
+ have "sup f a b : ?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 : ?A"
+ by (simp add: plussub_def lift2_def split: err.split)
+ qed
+
+ moreover
+
+ have "\<forall>x\<in>?A. \<forall>y\<in>?A. x <=_?r x +_?f y"
+ proof (intro strip)
+ fix x y
+ assume x: "x : ?A"
+ assume y: "y : ?A"
+
+ show "x <=_?r x +_?f y"
+ proof -
+ from ord
+ have order_r: "order r" by simp
+
+ { fix a b
+ assume ok: "x = OK a" "y = OK b"
+
+ { fix c d
+ assume some: "a = Some c" "b = Some d"
+
+ with x y ok
+ obtain "c:A" "d:A" by simp
+ then
+ obtain "OK c : err A" "OK d : err A" by simp
+ with ub1
+ have OK: "OK c <=_(Err.le r) (OK c) +_(lift2 f) (OK d)"
+ by blast
+
+ { fix e assume "f c d = OK e"
+ with OK
+ have "c <=_r e"
+ by (simp add: lesub_def Err.le_def plussub_def lift2_def)
+ }
+ with ok some
+ have ?thesis
+ by (simp add: plussub_def sup_def lesub_def le_def lift2_def Err.le_def
+ split: err.split)
+ } note this [intro!]
+
+ from ok
+ have ?thesis
+ by - (cases a, simp, cases b, simp add: order_r, blast)
+ }
+ thus ?thesis
+ by - (cases x, simp, cases y, simp+)
+ qed
+ qed
+
+ moreover
+
+ have "\<forall>x\<in>?A. \<forall>y\<in>?A. y <=_?r x +_?f y"
+ proof (intro strip)
+ fix x y
+ assume x: "x : ?A"
+ assume y: "y : ?A"
+
+ show "y <=_?r x +_?f y"
+ proof -
+ from ord
+ have order_r: "order r" by simp
+
+ { fix a b
+ assume ok: "x = OK a" "y = OK b"
+
+ { fix c d
+ assume some: "a = Some c" "b = Some d"
+
+ with x y ok
+ obtain "c:A" "d:A" by simp
+ then
+ obtain "OK c : err A" "OK d : err A" by simp
+ with ub2
+ have OK: "OK d <=_(Err.le r) (OK c) +_(lift2 f) (OK d)"
+ by blast
+
+ { fix e assume "f c d = OK e"
+ with OK
+ have "d <=_r e"
+ by (simp add: lesub_def Err.le_def plussub_def lift2_def)
+ }
+ with ok some
+ have ?thesis
+ by (simp add: plussub_def sup_def lesub_def le_def lift2_def Err.le_def
+ split: err.split)
+ } note this [intro!]
+
+ from ok
+ have ?thesis
+ by - (cases a, simp add: order_r, cases b, simp, blast)
+ }
+ thus ?thesis
+ by - (cases x, simp, cases y, simp+)
+ qed
+ qed
+
+ 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 : ?A" "y : ?A" "z : ?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:err A" "OK e:err A" "OK g:err A"
+ by simp
+ with lub
+ have "[| (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) |]
+ ==> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
+ by blast
+ hence "[| d <=_r g; e <=_r g |] ==> \<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:
+ "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
+apply (unfold top_def)
+apply (blast intro: order_antisym)
+done
+
+
+lemma acc_le_optI [intro!]:
+ "acc r ==> 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 "? a. Some a : Q")
+ apply (erule_tac x = "{a . Some a : Q}" in allE)
+ apply blast
+apply (case_tac "x")
+ apply blast
+apply blast
+done
+
+lemma option_map_in_optionI:
+ "[| ox : opt S; !x:S. ox = Some x --> f x : S |]
+ ==> option_map f ox : opt S";
+apply (unfold option_map_def)
+apply (simp split: option.split)
+apply blast
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Product.thy Mon Nov 20 16:37:42 2000 +0100
@@ -0,0 +1,144 @@
+(* Title: HOL/BCV/Product.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TUM
+
+Products as semilattices
+*)
+
+header "Products as Semilattices"
+
+theory Product = Err:
+
+constdefs
+ le :: "'a ord => 'b ord => ('a * 'b) ord"
+"le rA rB == %(a,b) (a',b'). a <=_rA a' & b <=_rB b'"
+
+ sup :: "'a ebinop => 'b ebinop => ('a * 'b)ebinop"
+"sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
+
+ esl :: "'a esl => 'b esl => ('a * 'b ) esl"
+"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
+
+syntax "@lesubprod" :: "'a*'b => 'a ord => 'b ord => 'b => bool"
+ ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
+translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
+
+lemma unfold_lesub_prod:
+ "p <=(rA,rB) q == le rA rB p q"
+ by (simp add: lesub_def)
+
+lemma le_prod_Pair_conv [iff]:
+ "((a1,b1) <=(rA,rB) (a2,b2)) = (a1 <=_rA a2 & b1 <=_rB b2)"
+ by (simp add: lesub_def le_def)
+
+lemma less_prod_Pair_conv:
+ "((a1,b1) <_(Product.le rA rB) (a2,b2)) =
+ (a1 <_rA a2 & b1 <=_rB b2 | a1 <=_rA a2 & b1 <_rB b2)"
+apply (unfold lesssub_def)
+apply simp
+apply blast
+done
+
+lemma order_le_prod [iff]:
+ "order(Product.le rA rB) = (order rA & order rB)"
+apply (unfold order_def)
+apply simp
+apply blast
+done
+
+
+lemma acc_le_prodI [intro!]:
+ "[| acc rA; acc rB |] ==> acc(Product.le rA rB)"
+apply (unfold acc_def)
+apply (rule wf_subset)
+ apply (erule wf_lex_prod)
+ apply assumption
+apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def)
+done
+
+
+lemma closed_lift2_sup:
+ "[| closed (err A) (lift2 f); closed (err B) (lift2 g) |] ==>
+ closed (err(A<*>B)) (lift2(sup f g))";
+apply (unfold closed_def plussub_def lift2_def err_def sup_def)
+apply (simp split: err.split)
+apply blast
+done
+
+lemma unfold_plussub_lift2:
+ "e1 +_(lift2 f) e2 == lift2 f e1 e2"
+ by (simp add: plussub_def)
+
+
+lemma plus_eq_Err_conv [simp]:
+ "[| x:A; y:A; semilat(err A, Err.le r, lift2 f) |]
+ ==> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
+proof -
+ have plus_le_conv2:
+ "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
+ OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z"
+ by (rule plus_le_conv [THEN iffD1])
+ case antecedent
+ thus ?thesis
+ apply (rule_tac iffI)
+ apply clarify
+ apply (drule OK_le_err_OK [THEN iffD2])
+ apply (drule OK_le_err_OK [THEN iffD2])
+ apply (drule semilat_lub)
+ apply assumption
+ apply assumption
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ apply (case_tac "x +_f y")
+ apply assumption
+ apply (rename_tac "z")
+ apply (subgoal_tac "OK z: err A")
+ apply (frule plus_le_conv2)
+ apply assumption
+ apply simp
+ apply blast
+ apply simp
+ apply (blast dest: semilatDorderI order_refl)
+ apply blast
+ apply (erule subst)
+ apply (unfold semilat_def err_def closed_def)
+ apply simp
+ done
+qed
+
+lemma err_semilat_Product_esl:
+ "!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)"
+apply (unfold esl_def Err.sl_def)
+apply (simp (no_asm_simp) only: split_tupled_all)
+apply simp
+apply (simp (no_asm) only: semilat_Def)
+apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
+apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def)
+apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2
+ simp add: lift2_def split: err.split)
+apply (blast dest: semilatDorderI)
+apply (blast dest: semilatDorderI)
+
+apply (rule OK_le_err_OK [THEN iffD1])
+apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat_lub)
+apply simp
+apply simp
+apply simp
+apply simp
+apply simp
+apply simp
+
+apply (rule OK_le_err_OK [THEN iffD1])
+apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat_lub)
+apply simp
+apply simp
+apply simp
+apply simp
+apply simp
+apply simp
+done
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/MicroJava/BV/Semilat.thy Mon Nov 20 16:37:42 2000 +0100
@@ -0,0 +1,235 @@
+(* Title: HOL/BCV/Semilat.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 2000 TUM
+
+Semilattices
+*)
+
+header "Semilattices"
+
+theory Semilat = Main:
+
+types 'a ord = "'a => 'a => bool"
+ 'a binop = "'a => 'a => 'a"
+ 'a sl = "'a set * 'a ord * 'a binop"
+
+consts
+ "@lesub" :: "'a => 'a ord => 'a => bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
+ "@lesssub" :: "'a => 'a ord => 'a => bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
+defs
+lesub_def: "x <=_r y == r x y"
+lesssub_def: "x <_r y == x <=_r y & x ~= y"
+
+consts
+ "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
+defs
+plussub_def: "x +_f y == f x y"
+
+
+constdefs
+ ord :: "('a*'a)set => 'a ord"
+"ord r == %x y. (x,y):r"
+
+ order :: "'a ord => bool"
+"order r == (!x. x <=_r x) &
+ (!x y. x <=_r y & y <=_r x --> x=y) &
+ (!x y z. x <=_r y & y <=_r z --> x <=_r z)"
+
+ acc :: "'a ord => bool"
+"acc r == wf{(y,x) . x <_r y}"
+
+ top :: "'a ord => 'a => bool"
+"top r T == !x. x <=_r T"
+
+ closed :: "'a set => 'a binop => bool"
+"closed A f == !x:A. !y:A. x +_f y : A"
+
+ semilat :: "'a sl => bool"
+"semilat == %(A,r,f). order r & closed A f &
+ (!x:A. !y:A. x <=_r x +_f y) &
+ (!x:A. !y:A. y <=_r x +_f y) &
+ (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
+
+ is_ub :: "('a*'a)set => 'a => 'a => 'a => bool"
+"is_ub r x y u == (x,u):r & (y,u):r"
+
+ is_lub :: "('a*'a)set => 'a => 'a => 'a => bool"
+"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
+
+ some_lub :: "('a*'a)set => 'a => 'a => 'a"
+"some_lub r x y == SOME z. is_lub r x y z"
+
+
+lemma order_refl [simp, intro]:
+ "order r ==> x <=_r x";
+ by (simp add: order_def)
+
+lemma order_antisym:
+ "[| order r; x <=_r y; y <=_r x |] ==> x = y"
+apply (unfold order_def)
+apply (simp (no_asm_simp))
+done
+
+lemma order_trans:
+ "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z"
+apply (unfold order_def)
+apply blast
+done
+
+lemma order_less_irrefl [intro, simp]:
+ "order r ==> ~ x <_r x"
+apply (unfold order_def lesssub_def)
+apply blast
+done
+
+lemma order_less_trans:
+ "[| order r; x <_r y; y <_r z |] ==> x <_r z"
+apply (unfold order_def lesssub_def)
+apply blast
+done
+
+lemma topD [simp, intro]:
+ "top r T ==> x <=_r T"
+ by (simp add: top_def)
+
+lemma top_le_conv [simp]:
+ "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
+ by (blast intro: order_antisym)
+
+lemma semilat_Def:
+"semilat(A,r,f) == order r & closed A f &
+ (!x:A. !y:A. x <=_r x +_f y) &
+ (!x:A. !y:A. y <=_r x +_f y) &
+ (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
+apply (unfold semilat_def Product_Type.split [THEN eq_reflection])
+apply (rule refl [THEN eq_reflection])
+done
+
+lemma semilatDorderI [simp, intro]:
+ "semilat(A,r,f) ==> order r"
+ by (simp add: semilat_Def)
+
+lemma semilatDclosedI [simp, intro]:
+ "semilat(A,r,f) ==> closed A f"
+apply (unfold semilat_Def)
+apply simp
+done
+
+lemma semilat_ub1 [simp]:
+ "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y"
+ by (unfold semilat_Def, simp)
+
+lemma semilat_ub2 [simp]:
+ "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y"
+ by (unfold semilat_Def, simp)
+
+lemma semilat_lub [simp]:
+ "[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z";
+ by (unfold semilat_Def, simp)
+
+
+lemma plus_le_conv [simp]:
+ "[| x:A; y:A; z:A; semilat(A,r,f) |]
+ ==> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
+apply (unfold semilat_Def)
+apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans)
+done
+
+lemma le_iff_plus_unchanged:
+ "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (x +_f y = y)"
+apply (rule iffI)
+ apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+)
+apply (erule subst)
+apply simp
+done
+
+lemma le_iff_plus_unchanged2:
+ "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (y +_f x = y)"
+apply (rule iffI)
+ apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+)
+apply (erule subst)
+apply simp
+done
+
+(*** closed ***)
+
+lemma closedD:
+ "[| closed A f; x:A; y:A |] ==> x +_f y : A"
+apply (unfold closed_def)
+apply blast
+done
+
+lemma closed_UNIV [simp]: "closed UNIV f"
+ by (simp add: closed_def)
+
+(*** lub ***)
+
+lemma is_lubD:
+ "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
+ by (simp add: is_lub_def)
+
+lemma is_ubI:
+ "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u"
+ by (simp add: is_ub_def)
+
+lemma is_ubD:
+ "is_ub r x y u ==> (x,u) : r & (y,u) : r"
+ by (simp add: is_ub_def)
+
+
+lemma is_lub_bigger1 [iff]:
+ "is_lub (r^* ) x y y = ((x,y):r^* )"
+apply (unfold is_lub_def is_ub_def)
+apply blast
+done
+
+
+lemma is_lub_bigger2 [iff]:
+ "is_lub (r^* ) x y x = ((y,x):r^* )"
+apply (unfold is_lub_def is_ub_def)
+apply blast
+done
+
+
+lemma extend_lub:
+ "[| univalent r; is_lub (r^* ) x y u; (x',x) : r |]
+ ==> EX v. is_lub (r^* ) x' y v"
+apply (unfold is_lub_def is_ub_def)
+apply (case_tac "(y,x) : r^*")
+ apply (case_tac "(y,x') : r^*")
+ apply blast
+ apply (blast intro: r_into_rtrancl elim: converse_rtranclE
+ dest: univalentD)
+apply (rule exI)
+apply (rule conjI)
+ apply (blast intro: rtrancl_into_rtrancl2 dest: univalentD)
+apply (blast intro: rtrancl_into_rtrancl rtrancl_into_rtrancl2
+ elim: converse_rtranclE dest: univalentD)
+done
+
+lemma univalent_has_lubs [rule_format]:
+ "[| univalent r; (x,u) : r^* |] ==> (!y. (y,u) : r^* -->
+ (EX z. is_lub (r^* ) x y z))"
+apply (erule converse_rtrancl_induct)
+ apply clarify
+ apply (erule converse_rtrancl_induct)
+ apply blast
+ apply (blast intro: rtrancl_into_rtrancl2)
+apply (blast intro: extend_lub)
+done
+
+lemma some_lub_conv:
+ "[| acyclic r; is_lub (r^* ) x y u |] ==> some_lub (r^* ) x y = u"
+apply (unfold some_lub_def is_lub_def)
+apply (rule someI2)
+ apply assumption
+apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl)
+done
+
+lemma is_lub_some_lub:
+ "[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |]
+ ==> is_lub (r^* ) x y (some_lub (r^* ) x y)";
+ by (fastsimp dest: univalent_has_lubs simp add: some_lub_conv)
+
+end
--- a/src/HOL/MicroJava/BV/Step.thy Sat Nov 18 19:48:34 2000 +0100
+++ b/src/HOL/MicroJava/BV/Step.thy Mon Nov 20 16:37:42 2000 +0100
@@ -15,8 +15,8 @@
step' :: "instr \<times> jvm_prog \<times> state_type => state_type"
recdef step' "{}"
-"step' (Load idx, G, (ST, LT)) = (val (LT ! idx) # ST, LT)"
-"step' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= Ok ts])"
+"step' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)"
+"step' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])"
"step' (Bipush i, G, (ST, LT)) = (PrimT Integer # ST, LT)"
"step' (Aconst_null, G, (ST, LT)) = (NT#ST,LT)"
"step' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)"
@@ -32,12 +32,11 @@
= (PrimT Integer#ST,LT)"
"step' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)"
"step' (Goto b, G, s) = s"
- (* Return has no successor instruction in the same method: *)
-(* "step' (Return, G, (T#ST,LT)) = None" *)
+ (* Return has no successor instruction in the same method *)
+"step' (Return, G, s) = s"
"step' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST
in (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))"
-(* "step' (i,G,s) = None" *)
constdefs
step :: "instr => jvm_prog => state_type option => state_type option"
@@ -113,7 +112,7 @@
"succs IAdd pc = [pc+1]"
"succs (Ifcmpeq b) pc = [pc+1, nat (int pc + b)]"
"succs (Goto b) pc = [nat (int pc + b)]"
-"succs Return pc = []"
+"succs Return pc = [pc]"
"succs (Invoke C mn fpTs) pc = [pc+1]"
--- a/src/HOL/MicroJava/BV/StepMono.thy Sat Nov 18 19:48:34 2000 +0100
+++ b/src/HOL/MicroJava/BV/StepMono.thy Mon Nov 20 16:37:42 2000 +0100
@@ -14,8 +14,8 @@
lemma sup_loc_some [rule_format]:
-"\<forall> y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = Ok t -->
- (\<exists>t. b!n = Ok t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
+"\<forall> y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = OK t -->
+ (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
proof (induct (open) ?P b)
show "?P []" by simp
@@ -25,12 +25,12 @@
fix z zs n
assume * :
"G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs"
- "n < Suc (length zs)" "(z # zs) ! n = Ok t"
+ "n < Suc (length zs)" "(z # zs) ! n = OK t"
- show "(\<exists>t. (a # list) ! n = Ok t) \<and> G \<turnstile>(a # list) ! n <=o Ok t"
+ show "(\<exists>t. (a # list) ! n = OK t) \<and> G \<turnstile>(a # list) ! n <=o OK t"
proof (cases n)
case 0
- with * show ?thesis by (simp add: sup_ty_opt_Ok)
+ with * show ?thesis by (simp add: sup_ty_opt_OK)
next
case Suc
with Cons *
@@ -42,7 +42,7 @@
lemma all_widen_is_sup_loc:
"\<forall>b. length a = length b -->
- (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map Ok a) <=l (map Ok b))"
+ (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map OK a) <=l (map OK b))"
(is "\<forall>b. length a = length b --> ?Q a b" is "?P a")
proof (induct "a")
show "?P []" by simp
@@ -273,14 +273,14 @@
by - (rule widen_trans, auto)
from G'
- have "G \<turnstile> map Ok apTs' <=l map Ok apTs"
+ have "G \<turnstile> map OK apTs' <=l map OK apTs"
by (simp add: sup_state_def)
also
from l w
- have "G \<turnstile> map Ok apTs <=l map Ok list"
+ have "G \<turnstile> map OK apTs <=l map OK list"
by (simp add: all_widen_is_sup_loc)
finally
- have "G \<turnstile> map Ok apTs' <=l map Ok list" .
+ have "G \<turnstile> map OK apTs' <=l map OK list" .
with l'
have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
@@ -302,12 +302,11 @@
lemmas [simp] = step_def
lemma step_mono_Some:
-"[| succs i pc \<noteq> []; app i G rT (Some s2); G \<turnstile> s1 <=s s2 |] ==>
+"[| app i G rT (Some s2); G \<turnstile> s1 <=s s2 |] ==>
G \<turnstile> the (step i G (Some s1)) <=s the (step i G (Some s2))"
proof (cases s1, cases s2)
fix a1 b1 a2 b2
assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
- assume succs: "succs i pc \<noteq> []"
assume app2: "app i G rT (Some s2)"
assume G: "G \<turnstile> s1 <=s s2"
@@ -330,11 +329,11 @@
with s app1
obtain y where
- y: "nat < length b1" "b1 ! nat = Ok y" by clarsimp
+ y: "nat < length b1" "b1 ! nat = OK y" by clarsimp
from Load s app2
obtain y' where
- y': "nat < length b2" "b2 ! nat = Ok y'" by clarsimp
+ y': "nat < length b2" "b2 ! nat = OK y'" by clarsimp
from G s
have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_def)
@@ -415,9 +414,10 @@
show ?thesis
by (clarsimp simp add: sup_state_def)
next
- case Return
- with succs have "False" by simp
- thus ?thesis by blast
+ case Return
+ with G step
+ show ?thesis
+ by simp
next
case Pop
with G s step app1 app2
@@ -464,7 +464,7 @@
qed
lemma step_mono:
- "[| succs i pc \<noteq> []; app i G rT s2; G \<turnstile> s1 <=' s2 |] ==>
+ "[| app i G rT s2; G \<turnstile> s1 <=' s2 |] ==>
G \<turnstile> step i G s1 <=' step i G s2"
by (cases s1, cases s2, auto dest: step_mono_Some)