# HG changeset patch # User nipkow # Date 991726871 -7200 # Node ID 45f837f8889d6453b25632854bb6429f8187d529 # Parent 29f8b00d7e1f0f5b3ebcdb67243fd1ac915eb379 This is now superseded by MicroJava/BV diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/DFA_Framework.ML --- a/src/HOL/BCV/DFA_Framework.ML Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,96 +0,0 @@ -(* Title: HOL/BCV/DFAandWTI.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM -*) - -Goalw [wti_is_stable_topless_def] - "[| wti_is_stable_topless r T step wti succs n A; \ -\ ss : list n A; !p \ -\ wti ss p = stable r step succs ss p"; -by (Asm_simp_tac 1); -qed "wti_is_stable_toplessD"; - -Goalw [is_dfa_def] - "[| 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 (Asm_full_simp_tac 1); -qed "is_dfaD"; - -Goalw [is_bcv_def,welltyping_def,stables_def] - "[| order r; top r T; \ -\ wti_is_stable_topless r T step wti succs n A; \ -\ is_dfa r dfa step succs n A |] ==> is_bcv r T wti n A dfa"; -by (Clarify_tac 1); -by (dtac is_dfaD 1); -by (assume_tac 1); -by (Clarify_tac 1); -by (rtac iffI 1); - by (rtac bexI 1); - by (rtac conjI 1); - by (assume_tac 1); - by (asm_full_simp_tac - (simpset() addsimps[wti_is_stable_toplessD,stables_def]) 1); - by (assume_tac 1); -by (Clarify_tac 1); -by (asm_full_simp_tac - (simpset() addsimps [imp_conjR,all_conj_distrib,wti_is_stable_toplessD, - stables_def] addcongs [conj_cong]) 1); -by (dres_inst_tac [("x","ts")] bspec 1); - by (assume_tac 1); -by (force_tac (claset()addDs [le_listD],simpset()) 1); -qed "is_bcv_dfa"; - -(* -Goal - "x:M ==> replicate n x : list n M"; -by (induct_tac "n" 1); -by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [in_list_Suc_iff,Bex_def]) 1); -qed "replicate_in_list"; -Addsimps [replicate_in_list]; - -Goal "!ys. replicate n x <= ys = (length ys = n & (!y:set ys. x <= y))"; -by (induct_tac "n" 1); - by (Force_tac 1); -by (asm_full_simp_tac (simpset() addsimps [Cons_le_iff,length_Suc_conv]) 1); -by (Force_tac 1); -qed_spec_mp "replicate_le_conv"; -AddIffs [replicate_le_conv]; - -Goal - "[| wti_is_stable_topless step wti succs n A; is_dfa dfa step succs n A; \ -\ 0 < n; init : (option A) |] ==> \ -\ dfa (init # replicate (n-1) None) = \ -\ (? tos : list n (option A). init <= tos!0 & welltyping wti tos)"; -by (subgoal_tac "? m. n = m+1" 1); - by (res_inst_tac [("x","n-1")] exI 2); - by (arith_tac 2); -by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -by (dtac dfa_iff_welltyping 1); - by (assume_tac 1); - by (etac trans 2); - by (asm_simp_tac (simpset() addsimps [in_list_Suc_iff,Bex_def]) 1); -by (asm_full_simp_tac (simpset() addsimps [Cons_le_iff]) 1); -by (rtac iffI 1); - by (Clarify_tac 1); - by (rtac bexI 1); - by (rtac conjI 1); - by (assume_tac 2); - by (assume_tac 2); - by (Asm_simp_tac 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff,Bex_def]) 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps []) 1); -by (rtac exI 1); -by (rtac conjI 1); - by (rtac conjI 2); - by (assume_tac 3); - by (Blast_tac 1); -by (Force_tac 1); -qed "dfa_iff_welltyping0"; -*) diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/DFA_Framework.thy --- a/src/HOL/BCV/DFA_Framework.thy Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,51 +0,0 @@ -(* Title: HOL/BCV/DFA_Framework.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM - -The relationship between dataflow analysis and a welltyped-insruction predicate. -*) - -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 ('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 => ('s list => nat => bool) - => nat => 's set => ('s list => 's list) => bool -"is_bcv r T wti n A bcv == !ss : list n A. - (!p 's - => (nat => 's => 's) - => ('s list => nat => bool) - => (nat => nat list) - => nat => 's set => bool -"wti_is_stable_topless r T step wti succs n A == !ss p. - ss : list n A & (!p - wti ss p = stable r step succs ss p" - - welltyping :: 's => ('s list => nat => bool) => 's list => bool -"welltyping T wti ts == !p e <=_(Err.le r) e"; -by (asm_simp_tac (simpset() addsplits [err.split]) 1); -qed "le_err_refl"; - -Goalw [unfold_lesub_err,le_def] "order r ==> \ -\ e1 <=_(le r) e2 --> e2 <=_(le r) e3 --> e1 <=_(le r) e3"; -by (simp_tac (simpset() addsplits [err.split]) 1); -by (blast_tac (claset() addIs [order_trans]) 1); -qed_spec_mp "le_err_trans"; - -Goalw [unfold_lesub_err,le_def] - "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e1 --> e1=e2"; -by (simp_tac (simpset() addsplits [err.split]) 1); -by (blast_tac (claset() addIs [order_antisym]) 1); -qed_spec_mp "le_err_antisym"; - - -Goalw [unfold_lesub_err,le_def] - "(OK x <=_(le r) OK y) = (x <=_r y)"; -by (Simp_tac 1); -qed "OK_le_err_OK"; - - -Goal "order(le r) = order r"; -by (rtac iffI 1); - by (stac order_def 1); - by (blast_tac (claset() addDs [order_antisym,OK_le_err_OK RS iffD2] - addIs [order_trans,OK_le_err_OK RS iffD1]) 1); -by (stac order_def 1); -by (blast_tac (claset() addIs [le_err_refl,le_err_trans,le_err_antisym] - addDs [order_refl]) 1); -qed "order_le_err"; -AddIffs [order_le_err]; - - -Goalw [unfold_lesub_err,le_def] - "e <=_(le r) Err"; -by (Simp_tac 1); -qed "le_Err"; -AddIffs [le_Err]; - -Goalw [unfold_lesub_err,le_def] - "Err <=_(le r) e = (e = Err)"; -by (simp_tac (simpset() addsplits [err.split]) 1); -qed "Err_le_conv"; -AddIffs [Err_le_conv]; - -Goalw [unfold_lesub_err,le_def] - "e <=_(le r) OK x = (? y. e = OK y & y <=_r x)"; -by (simp_tac (simpset() addsplits [err.split]) 1); -qed "le_OK_conv"; -AddIffs [le_OK_conv]; - -Goalw [unfold_lesub_err,le_def] - "OK x <=_(le r) e = (e = Err | (? y. e = OK y & x <=_r y))"; -by (simp_tac (simpset() addsplits [err.split]) 1); -qed "OK_le_conv"; - -Goalw [top_def] "top (le r) Err"; -by (Simp_tac 1); -qed "top_Err"; -AddIffs [top_Err]; - -Goalw [lesssub_def,lesub_def,le_def] - "OK x <_(le r) e = (e=Err | (? y. e = OK y & x <_r y))"; -by (simp_tac (simpset() addsplits [err.split]) 1); -qed_spec_mp "OK_less_conv"; -AddIffs [OK_less_conv]; - -Goalw [lesssub_def,lesub_def,le_def] "~(Err <_(le r) x)"; -by (simp_tac (simpset() addsplits [err.split]) 1); -qed_spec_mp "not_Err_less"; -AddIffs [not_Err_less]; - - -Goalw - [semilat_Def,closed_def,plussub_def,lesub_def,lift2_def,Err.le_def,err_def] - "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"; -by (asm_full_simp_tac (simpset() addsplits [err.split]) 1); -qed "semilat_errI"; - -Goalw [sl_def,esl_def] - "!!L. semilat L ==> err_semilat(esl L)"; -by (split_all_tac 1); -by (asm_full_simp_tac (simpset() addsimps [semilat_errI]) 1); -qed "err_semilat_eslI"; - -Goalw [acc_def,lesub_def,le_def,lesssub_def] - "acc r ==> acc(le r)"; -by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal] addsplits [err.split]) 1); -by (Clarify_tac 1); -by (case_tac "Err : Q" 1); - by (Blast_tac 1); -by (eres_inst_tac [("x","{a . OK a : Q}")] allE 1); -by (case_tac "x" 1); - by (Fast_tac 1); -by (Blast_tac 1); -qed "acc_err"; -Addsimps [acc_err]; -AddSIs [acc_err]; - -Goalw [err_def] "Err : err A"; -by (Simp_tac 1); -qed "Err_in_err"; -AddIffs [Err_in_err]; - -Goalw [err_def] "(OK x : err A) = (x:A)"; -by (Auto_tac); -qed "OK_in_err"; -AddIffs [OK_in_err]; - - -(** lift **) - -Goalw [lift_def] - "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S"; -by (asm_simp_tac (simpset() addsplits [err.split]) 1); -by (Blast_tac 1); -qed "lift_in_errI"; - -(** lift2 **) - -Goalw [lift2_def,plussub_def] "Err +_(lift2 f) x = Err"; -by (Simp_tac 1); -qed "Err_lift2"; - -Goalw [lift2_def,plussub_def] "x +_(lift2 f) Err = Err"; -by (simp_tac (simpset() addsplits [err.split]) 1); -qed "lift2_Err"; - -Goalw [lift2_def,plussub_def] "OK x +_(lift2 f) OK y = x +_f y"; -by (simp_tac (simpset() addsplits [err.split]) 1); -qed "OK_lift2_OK"; - -Addsimps [Err_lift2,lift2_Err,OK_lift2_OK]; - -(** sup **) - -Goalw [plussub_def,Err.sup_def,Err.lift2_def] "Err +_(Err.sup f) x = Err"; -by (Simp_tac 1); -qed "Err_sup_Err"; - -Goalw [plussub_def,Err.sup_def,Err.lift2_def] "x +_(Err.sup f) Err = Err"; -by (simp_tac (simpset() addsplits [err.split]) 1); -qed "Err_sup_Err2"; - -Goalw [plussub_def,Err.sup_def,Err.lift2_def] - "OK x +_(Err.sup f) OK y = OK(x +_f y)"; -by (Simp_tac 1); -qed "Err_sup_OK"; - -Addsimps [Err_sup_Err,Err_sup_Err2,Err_sup_OK]; - -Goalw [Err.sup_def,lift2_def,plussub_def] - "(Err.sup f ex ey = OK z) = (? x y. ex = OK x & ey = OK y & f x y = z)"; -by (rtac iffI 1); - by (Clarify_tac 2); - by (Asm_simp_tac 2); -by (asm_full_simp_tac (simpset() addsplits [err.split_asm]) 1); -qed "Err_sup_eq_OK_conv"; -AddIffs [Err_sup_eq_OK_conv]; - -Goalw [Err.sup_def,lift2_def,plussub_def] - "(Err.sup f ex ey = Err) = (ex=Err | ey=Err)"; -by (simp_tac (simpset() addsplits [err.split]) 1); -qed "Err_sup_eq_Err"; -AddIffs [Err_sup_eq_Err]; - - -(*** semilat (err A) (le r) f ***) - -Goal "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err"; -by (blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1); -qed "semilat_le_err_Err_plus"; - -Goal "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err"; -by (blast_tac (claset() addIs [le_iff_plus_unchanged RS iffD1,le_iff_plus_unchanged2 RS iffD1]) 1); -qed "semilat_le_err_plus_Err"; - -Addsimps [semilat_le_err_Err_plus,semilat_le_err_plus_Err]; - -Goal "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] \ -\ ==> x <=_r z"; -by (rtac (OK_le_err_OK RS iffD1) 1); -by (etac subst 1); -by (Asm_simp_tac 1); -qed "semilat_le_err_OK1"; - -Goal "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] \ -\ ==> y <=_r z"; -by (rtac (OK_le_err_OK RS iffD1) 1); -by (etac subst 1); -by (Asm_simp_tac 1); -qed "semilat_le_err_OK2"; - -Goalw [order_def] "[| x=y; order r |] ==> x <=_r y"; -by (Blast_tac 1); -qed "eq_order_le"; - -Goal - "[| x:A; y:A; semilat(err A, le r, fe) |] ==> \ -\ ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"; -by (rtac iffI 1); - by (Clarify_tac 1); - by (dtac (OK_le_err_OK RS iffD2) 1); - by (dtac (OK_le_err_OK RS iffD2) 1); - by (dtac semilat_lub 1); - by (assume_tac 1); - by (assume_tac 1); - by (Asm_simp_tac 1); - by (Asm_simp_tac 1); - by (Asm_simp_tac 1); - by (Asm_full_simp_tac 1); -by (case_tac "(OK x) +_fe (OK y)" 1); - by (assume_tac 1); -by (rename_tac "z" 1); -by (subgoal_tac "OK z: err A" 1); -by (dtac eq_order_le 1); - by (Blast_tac 1); - by (blast_tac (claset() addDs [rotate_prems 3 (plus_le_conv RS iffD1)]) 1); -by (etac subst 1); -by (blast_tac (claset() addIs [closedD]) 1); -qed "OK_plus_OK_eq_Err_conv"; -Addsimps [OK_plus_OK_eq_Err_conv]; - -(*** semilat (err(Union AS)) ***) - -(* FIXME? *) -Goal "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))"; -by (Blast_tac 1); -qed "all_bex_swap_lemma"; -AddIffs [all_bex_swap_lemma]; - -Goalw [closed_def,err_def] - "[| !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)"; -by (Asm_full_simp_tac 1); -by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -by (Fast_tac 1); -qed "closed_err_Union_lift2I"; - -(* If AS = {} the thm collapses to - order r & closed {Err} f & Err +_f Err = Err - which may not hold *) -Goalw [semilat_def,sl_def] - "[| !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)"; -by (asm_full_simp_tac (simpset() addsimps [closed_err_Union_lift2I]) 1); -by (rtac conjI 1); - by (Blast_tac 1); -by (asm_full_simp_tac (simpset() addsimps [err_def]) 1); -by (rtac conjI 1); - by (Clarify_tac 1); - by (rename_tac "A a u B b" 1); - by (case_tac "A = B" 1); - by (Asm_full_simp_tac 1); - by (Asm_full_simp_tac 1); -by (rtac conjI 1); - by (Clarify_tac 1); - by (rename_tac "A a u B b" 1); - by (case_tac "A = B" 1); - by (Asm_full_simp_tac 1); - by (Asm_full_simp_tac 1); -by (Clarify_tac 1); -by (rename_tac "A ya yb B yd z C c a b" 1); -by (case_tac "A = B" 1); - by (case_tac "A = C" 1); - by (Asm_full_simp_tac 1); - by (rotate_tac ~1 1); - by (Asm_full_simp_tac 1); -by (rotate_tac ~1 1); -by (case_tac "B = C" 1); - by (Asm_full_simp_tac 1); -by (rotate_tac ~1 1); -by (Asm_full_simp_tac 1); -qed "err_semilat_UnionI"; diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Err.thy --- a/src/HOL/BCV/Err.thy Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -(* Title: HOL/BCV/Err.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM - -The error type -*) - -Err = Semilat + - -datatype 'a err = Err | OK 'a - -types 'a ebinop = 'a => 'a => 'a err - 'a esl = "'a set * 'a ord * 'a ebinop" - -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)" - -end diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/JType.ML --- a/src/HOL/BCV/JType.ML Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,166 +0,0 @@ -(* Title: HOL/BCV/JType.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM -*) - -Goalw [lesub_def,subtype_def] "T [=_S T"; -by (Simp_tac 1); -qed "subtype_refl"; -AddIffs [subtype_refl]; - -Goalw [lesub_def,subtype_def,is_Class_def] - "(T [=_S Integer) = (T = Integer)"; -by (Simp_tac 1); -qed "subtype_Int_conv"; - -Goalw [lesub_def,subtype_def] "(Integer [=_S T) = (T = Integer)"; -by (Blast_tac 1); -qed "Int_subtype_conv"; - -Goalw [lesub_def,subtype_def,is_Class_def] - "(T [=_S Void) = (T = Void)"; -by (Simp_tac 1); -qed "subtype_Void_conv"; - -Goalw [lesub_def,subtype_def] "(Void [=_S T) = (T = Void)"; -by (Blast_tac 1); -qed "Void_subtype_conv"; - -AddIffs [subtype_Int_conv,Int_subtype_conv, - subtype_Void_conv,Void_subtype_conv]; - -Goalw [lesub_def,subtype_def,is_Class_def] - "T [=_S NullT = (T=NullT)"; -by (Simp_tac 1); -qed "subtype_NullT_conv"; - -Goalw [lesub_def,subtype_def,is_Class_def] - "NullT [=_S T = (T=NullT | (? C. T = Class C))"; -by (simp_tac (simpset() addsplits [ty.split]) 1); -qed "NullT_subtype_conv"; - -AddIffs [NullT_subtype_conv,subtype_NullT_conv]; - -Goalw [lesub_def,subtype_def,is_Class_def] - "T [=_S Class C = (T=NullT | (? D. T = Class D & (D,C) : S^*))"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "subtype_Class_conv"; - -Goalw [lesub_def,subtype_def,refl_def] - "Class D [=_S T = (? C. T = Class C & (D,C):S^*)"; -by (Blast_tac 1); -qed "Class_subtype_conv"; - -AddIffs [Class_subtype_conv,subtype_Class_conv]; - -Goalw [lesub_def,subtype_def,is_Class_def] - "[| A [=_S B; B [=_S C |] ==> A [=_S C"; -by (asm_full_simp_tac (simpset() addsplits [ty.split,ty.split_asm]) 1); -by (blast_tac (claset() addDs [transD] addIs [rtrancl_trans]) 1); -qed "subtype_transD"; - -Goalw [order_def,subtype_def,lesub_def,is_Class_def] - "acyclic S ==> order (subtype S)"; -by (dtac acyclic_impl_antisym_rtrancl 1); -by (auto_tac (claset() addIs [rtrancl_trans],simpset() addsimps [antisymD]) ); -qed "acyclic_impl_order_subtype"; - -Goalw [acc_def,lesssub_def] - "wf(S^-1) ==> acc(subtype S)"; -by (dres_inst_tac [("p","S^-1 - Id")] wf_subset 1); - by (Blast_tac 1); -by (dtac wf_trancl 1); -by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); -by (Clarify_tac 1); -by (rename_tac "M T" 1); -by (case_tac "EX C. Class C : M" 1); - by (case_tac "T" 2); - by (Blast_tac 2); - by (Blast_tac 2); - by (res_inst_tac [("x","T")] bexI 2); - by (Blast_tac 2); - by (assume_tac 2); - by (Blast_tac 2); -by (eres_inst_tac [("x","{C. Class C : M}")] allE 1); -by (Auto_tac); -by (rename_tac "D" 1); -by (res_inst_tac [("x","Class D")] bexI 1); - by (atac 2); -by (Clarify_tac 1); -by (cut_inst_tac [("r","S")] (standard(rtrancl_r_diff_Id RS sym)) 1); -by (Asm_full_simp_tac 1); -by (etac rtranclE 1); - by (Blast_tac 1); -by (dtac rtrancl_converseI 1); -by (subgoal_tac "(S-Id)^-1 = (S^-1 - Id)" 1); - by (Blast_tac 2); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addIs [rtrancl_into_trancl2]) 1); -qed "wf_converse_subcls1_impl_acc_subtype"; - -Addsimps [is_type_def]; - -Goalw [closed_def,plussub_def,lift2_def,err_def,JType.sup_def] - "[| single_valued S; acyclic S |] ==> \ -\ closed (err(types S)) (lift2 (JType.sup S))"; -by (simp_tac (simpset() addsplits [err.split,ty.split]) 1); -by (blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD] - addSIs [is_ubI]) 1); -qed "closed_err_types"; - -AddIffs [OK_le_conv]; - -Goalw [semilat_def, split_conv RS eq_reflection,JType.esl_def,Err.sl_def] - "[| single_valued S; acyclic S |] ==> err_semilat (JType.esl S)"; -by (asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1); - -by (rtac conjI 1); - by (Clarify_tac 1); - by (case_tac "x" 1); - by (Clarify_tac 1); - by (Simp_tac 1); - by (case_tac "y" 1); - by (Clarify_tac 1); - by (Simp_tac 1); - by (fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss - (simpset() addsimps [plussub_def,lift2_def,JType.sup_def] - addsplits [ty.split])) 1); - -by (rtac conjI 1); - by (Clarify_tac 1); - by (case_tac "x" 1); - by (Clarify_tac 1); - by (Simp_tac 1); - by (case_tac "y" 1); - by (Clarify_tac 1); - by (Simp_tac 1); - by (fast_tac (claset() addDs [is_lub_some_lub,is_lubD,is_ubD] addss - (simpset() addsimps [plussub_def,lift2_def,JType.sup_def] - addsplits [ty.split])) 1); - -by (Clarify_tac 1); -by (case_tac "x" 1); - by (Clarify_tac 1); -by (case_tac "y" 1); - by (Clarify_tac 1); -by (asm_simp_tac(simpset() addsimps [plussub_def,lift2_def,JType.sup_def] - addsplits [ty.split]) 1); -by (rtac conjI 1); - by (Blast_tac 1); -by (rtac conjI 1); - by (Blast_tac 1); -by (rtac conjI 1); - by (Blast_tac 1); -by (Clarify_tac 1); -by (rtac conjI 1); - by (Clarify_tac 1); -by (rtac conjI 1); - by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addSDs [is_lub_some_lub,is_lubD,is_ubD] - addSIs [is_ubI]) 1); -qed "err_semilat_JType_esl"; - -DelIffs [OK_le_conv]; diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/JType.thy --- a/src/HOL/BCV/JType.thy Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,68 +0,0 @@ -(* Title: HOL/BCV/JType.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM - -The type system of the JVM -*) - -JType = Err + - -types cname -arities cname :: term - -types subclass = "(cname*cname)set" - -datatype ty = Void | Integer | NullT | Class cname - -constdefs - is_Class :: ty => bool -"is_Class T == case T of Void => False | Integer => False | NullT => False - | Class C => True" - - is_ref :: ty => bool -"is_ref T == T=NullT | is_Class T" - - subtype :: subclass => ty ord -"subtype S T1 T2 == - (T1=T2) | T1=NullT & is_Class T2 | - (? C D. T1 = Class C & T2 = Class D & (C,D) : S^*)" - - sup :: "subclass => ty => ty => ty err" -"sup S T1 T2 == - case T1 of Void => (case T2 of Void => OK Void - | Integer => Err - | NullT => Err - | Class D => Err) - | Integer => (case T2 of Void => Err - | Integer => OK Integer - | NullT => Err - | Class D => Err) - | NullT => (case T2 of Void => Err - | Integer => Err - | NullT => OK NullT - | Class D => OK(Class D)) - | Class C => (case T2 of Void => Err - | Integer => Err - | NullT => OK(Class C) - | Class D => OK(Class(some_lub (S^*) C D)))" - - Object :: cname -"Object == arbitrary" - - is_type :: subclass => ty => bool -"is_type S T == case T of Void => True | Integer => True | NullT => True - | Class C => (C,Object):S^*" - -syntax - "types" :: subclass => ty set - "@subty" :: ty => subclass => ty => bool ("(_ /[='__ _)" [50, 1000, 51] 50) -translations - "types S" == "Collect(is_type S)" - "x [=_S y" == "x <=_(subtype S) y" - -constdefs - esl :: "subclass => ty esl" -"esl S == (types S, subtype S, sup S)" - -end diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/JVM.ML --- a/src/HOL/BCV/JVM.ML Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,262 +0,0 @@ -(* Title: HOL/BCV/JVM.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM -*) - -Addsimps [Let_def]; - -Addsimps [is_type_def]; - -Goalw [states_def,JVM.sl_def,Opt.sl_def,Err.sl_def, - stk_esl_def,reg_sl_def,Product.esl_def, - Listn.sl_def,upto_esl_def,JType.esl_def,Err.esl_def] - "states S maxs maxr == opt(err((Union {list n (types S) |n. n <= maxs}) <*>\ -\ list maxr (err(types S))))"; -by (Simp_tac 1); -qed "JVM_states_unfold"; - -Goalw [JVM.le_def,JVM.sl_def,Opt.sl_def,Err.sl_def, - stk_esl_def,reg_sl_def,Product.esl_def, - Listn.sl_def,upto_esl_def,JType.esl_def,Err.esl_def] - "JVM.le S m n == \ -\ Opt.le(Err.le(Product.le(Listn.le(subtype S))(Listn.le(Err.le(subtype S)))))"; -by (Simp_tac 1); -qed "JVM_le_unfold"; - -Goalw [wfis_def,wfi_def] - "[| wfis S md maxr bs; bs!p = Load n; p < size bs |] ==> n < maxr"; -by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth])); -qed "wf_LoadD"; - -Goalw [wfis_def,wfi_def] - "[| wfis S md maxr bs; bs!p = Store n; p < size bs |] ==> n < maxr"; -by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth])); -qed "wf_StoreD"; - -Goalw [wfis_def,wfi_def] - "[| wfis S md m bs; bs!p = New C; p < size bs |] ==> (C,Object):S^*"; -by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth])); -qed "wf_NewD"; - -Goalw [wfis_def,wfi_def,wf_mdict_def] - "[| wfis S md maxr bs; wf_mdict S md; bs!p = Invoke C m pT (Class R); \ -\ p < size bs |] ==> (R,Object):S^*"; -by (force_tac (claset(),simpset()addsimps [all_set_conv_all_nth]) 1); -qed "wf_InvokeD"; - -Goalw [wfis_def,wfi_def] - "[|wfis S md m bs; bs!p = Getfield (Class C) D; p < size bs|] ==> \ -\ (C,Object):S^*"; -by (auto_tac (claset(),simpset()addsimps [all_set_conv_all_nth])); -qed "wf_GetfieldD"; - -Goal "(? X. (? n. X = A n & P n) & Q X) = (? n. Q(A n) & P n)"; -by (Blast_tac 1); -qed "special_ex_swap_lemma"; -AddIffs [special_ex_swap_lemma]; - -Goalw [pres_type_def,list_def,step_def,JVM_states_unfold] - "[| wfis S md maxr bs; wf_mdict S md |] ==> \ -\ pres_type (step S maxs rT bs) (size bs) (states S maxs maxr)"; -by (clarify_tac (claset() addSEs [option_map_in_optionI,lift_in_errI]) 1); -by (asm_simp_tac (simpset()addsimps [exec_def] addsplits [instr.split]) 1); - -by (rtac conjI 1); -by (fast_tac (claset() addDs [refl RS nth_in] addSEs [wf_LoadD] addss - (simpset() delsimps [is_type_def]addsplits [err.split])) 1); - -by (rtac conjI 1); -by (fast_tac (claset() addDs [set_update_subset_insert RS subsetD] - addSEs [wf_StoreD] addss (simpset() addsplits [list.split])) 1); - -by (rtac conjI 1); -by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1); - -by (rtac conjI 1); -by (fast_tac (claset() addIs [wf_GetfieldD] - addss (simpset() addsplits [list.split,ty.split])) 1); - -by (rtac conjI 1); -by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1); - -by (rtac conjI 1); -by (fast_tac (claset() addIs [wf_NewD] addss simpset()) 1); - -by (rtac conjI 1); -by (DEPTH_SOLVE_1(rtac conjI 1 ORELSE - Clarify_tac 1 THEN asm_full_simp_tac (simpset() addsimps [wf_InvokeD] - addsplits [list.split,ty.split,option.split]) 1)); - -by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1); - -qed "exec_pres_type"; - -Goalw [wti_is_stable_topless_def,wti_def,stable_def,step_def, - option_map_def,lift_def,bounded_def,JVM_le_unfold] - "[| bounded (succs bs) (size bs) |] ==> \ -\ wti_is_stable_topless (JVM.le S maxs maxr) \ -\ (Some Err) \ -\ (step S maxs rT bs) \ -\ (wti S maxs rT bs) \ -\ (succs bs) (size bs) (states S maxs maxr)"; -by (simp_tac (simpset() addsplits [option.split]) 1); -by (simp_tac (simpset() addsplits [err.split]) 1); -by (Clarify_tac 1); -by (rtac conjI 1); - by (Blast_tac 1); -by (Clarify_tac 1); -by (EVERY1[etac allE, mp_tac]); -by (rewrite_goals_tac [exec_def,succs_def]); -by (split_tac [instr.split] 1); - -by (rtac conjI 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split,err.split]) 1); - -by (rtac conjI 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); - -by (rtac conjI 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); - -by (rtac conjI 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); - -by (rtac conjI 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); -by (Blast_tac 1); - -by (rtac conjI 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); - -by (rtac conjI 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); - -by (rtac conjI 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); - -by (rtac conjI 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split,ty.split]) 1); - -by (rtac conjI 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); -by (Blast_tac 1); - -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split,list.split] - addsimps [le_list_refl,le_err_refl] ) 1); -qed "wti_is_stable_topless"; - -Goalw [mono_def,step_def,option_map_def,lift_def, - JVM_states_unfold,JVM_le_unfold] - "[| wfis S md maxr bs; wf_mdict S md |] ==> \ -\ mono (JVM.le S maxs maxr) (step S maxs rT bs) (size bs) (states S maxs maxr)"; -by (Clarify_tac 1); -by (simp_tac (simpset() addsplits [option.split]) 1); -by (Clarify_tac 1); -by (Asm_simp_tac 1); -by (split_tac [err.split] 1); -by (rtac conjI 1); - by (Clarify_tac 1); -by (Clarify_tac 1); -by (simp_tac (simpset() addsimps [exec_def] delsplits [split_if]) 1); -by (split_tac [instr.split] 1); - -by (rtac conjI 1); -by (fast_tac (claset() addDs [le_listD] addSEs [wf_LoadD] - addss (simpset() addsplits [err.split])) 1); - -by (rtac conjI 1); -by (fast_tac (claset() addIs [list_update_le_cong,le_listD] addSEs [wf_StoreD] - addss (simpset() addsplits [list.split])) 1); - -by (rtac conjI 1); -by (Asm_simp_tac 1); - -by (rtac conjI 1); -by (Asm_simp_tac 1); - -by (rtac conjI 1); -by (force_tac (claset(), simpset() addsplits [list.split]) 1); - -by (rtac conjI 1); -by (fast_tac (claset() delrules [r_into_rtrancl] - addDs [rtrancl_trans] - addss (simpset() addsplits [list.split])) 1); - -by (rtac conjI 1); - by (Clarify_tac 1); - by (asm_full_simp_tac (simpset() addsplits [list.split]) 1); - by (rtac conjI 1); - by (Clarify_tac 1); - by (Clarify_tac 1); - by (rtac conjI 1); - by (Clarify_tac 1); - by (Clarify_tac 1); - by (rtac conjI 1); - by (Clarify_tac 1); - by (Clarify_tac 1); - by (Asm_full_simp_tac 1); - by (blast_tac (claset() addIs [rtrancl_trans,subtype_transD]) 1); - -by (rtac conjI 1); -by (asm_full_simp_tac (simpset() addsimps [reflD] addsplits [list.split]) 1); - -by (rtac conjI 1); -(* 39 *) - by (Clarify_tac 1); - by (asm_full_simp_tac (simpset() addsplits [list.split]) 1); - by (blast_tac (claset() addIs [rtrancl_trans,subtype_transD]) 1); - -by (rtac conjI 1); -by (fast_tac (claset() addss (simpset() addsplits [list.split,ty.split_asm] - addsimps [is_Class_def,is_ref_def])) 1); - -by (asm_simp_tac (simpset() addsplits [list.split]) 1); -by (blast_tac (claset() addIs [subtype_transD]) 1); - -qed "exec_mono"; - - -Goalw [JVM.sl_def,stk_esl_def,reg_sl_def] - "[| single_valued S; acyclic S |] ==> semilat(JVM.sl S maxs maxr)"; -by (REPEAT(ares_tac [semilat_opt,err_semilat_Product_esl,err_semilat_upto_esl, - err_semilat_eslI,semilat_Listn_sl,err_semilat_JType_esl] 1)); -qed "semilat_JVM_slI"; - -Goal "JVM.sl S maxs maxr == \ -\ (states S maxs maxr, JVM.le S maxs maxr, JVM.sup S maxs maxr)"; -by (simp_tac (simpset() addsimps [states_def,JVM.le_def,JVM.sup_def, - surjective_pairing RS sym]) 1); -qed "sl_triple_conv"; - -Goalw [kiljvm_def,sl_triple_conv] - "[| single_valued S; wf(S^-1); wfis S md maxr bs; wf_mdict S md; \ -\ bounded (succs bs) (size bs) |] ==> \ -\ is_bcv (JVM.le S maxs maxr) (Some Err) (wti S maxs rT bs) \ -\ (size bs) (states S maxs maxr) (kiljvm S maxs maxr rT bs)"; -by (rtac is_bcv_kildall 1); - by (simp_tac (simpset() addsimps [symmetric sl_triple_conv]) 1); - by (blast_tac (claset() addSIs [semilat_JVM_slI] addDs [wf_acyclic]) 1); - by (simp_tac (simpset() addsimps [JVM_le_unfold]) 1); - by (blast_tac (claset() - addSIs [acyclic_impl_order_subtype,wf_converse_subcls1_impl_acc_subtype] - addDs [wf_acyclic]) 1); - by (simp_tac (simpset() addsimps [JVM_le_unfold]) 1); - by (etac exec_pres_type 1); - by (assume_tac 1); - by (assume_tac 1); - by (etac exec_mono 1); - by (assume_tac 1); -by (etac wti_is_stable_topless 1); -qed "is_bcv_kiljvm"; diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/JVM.thy --- a/src/HOL/BCV/JVM.thy Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,165 +0,0 @@ -(* Title: HOL/BCV/JVM.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM - -A micro-JVM -*) - -JVM = Kildall + JType + Opt + Product + - -types mname -arities mname :: term - -datatype instr = - Load nat | Store nat | AConst_Null | IConst int - | IAdd | Getfield ty cname | Putfield ty cname - | New cname - | Invoke cname mname ty ty - | CmpEq nat - | Return - -types mdict = "cname => (mname * ty ~=> ty)" - -constdefs - wfi :: subclass => mdict => nat => instr => bool -"wfi S md maxr i == case i of - Load n => n < maxr - | Store n => n < maxr - | AConst_Null => True - | IConst j => True - | IAdd => True - | Getfield T C => is_type S T & is_type S (Class C) - | Putfield T C => is_type S T & is_type S (Class C) - | New C => is_type S (Class C) - | Invoke C m pT rT => md C (m,pT) = Some(rT) - | CmpEq n => True - | Return => True" - - wfis :: subclass => mdict => nat => instr list => bool -"wfis S md maxr ins == !i : set ins. wfi S md maxr i" - -types config = "ty list * ty err list" - state = config err option - -constdefs - stk_esl :: subclass => nat => ty list esl -"stk_esl S maxs == upto_esl maxs (JType.esl S)" - - reg_sl :: subclass => nat => ty err list sl -"reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))" - - sl :: subclass => nat => nat => state sl -"sl S maxs maxr == - Opt.sl(Err.sl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))" - - states :: subclass => nat => nat => state set -"states S maxs maxr == fst(sl S maxs maxr)" - - le :: subclass => nat => nat => state ord -"le S maxs maxr == fst(snd(sl S maxs maxr))" - - sup :: subclass => nat => nat => state binop -"sup S maxs maxr == snd(snd(sl S maxs maxr))" - -syntax "@lle" :: state => subclass => state => bool - ("(_ /<<='__ _)" [50, 1000, 51] 50) - -translations -"x <<=_S y" => "x <=_(le S arbitrary arbitrary) y" - -constdefs - - wf_mdict :: subclass => mdict => bool -"wf_mdict S md == - !C mpT rT. md C mpT = Some(rT) - --> is_type S rT & - (!C'. (C',C) : S^* - --> (EX rT'. md C' mpT = Some(rT') & rT' [=_S rT))" - - wti :: subclass => nat => ty => instr list => state list => nat => bool -"wti S maxs rT bs ss p == - case ss!p of - None => True - | Some e => - (case e of - Err => False - | OK (st,reg) => - (case bs!p of - Load n => size st < maxs & - (? T. reg!n = OK T & Some(OK(T#st,reg)) <<=_S ss!(p+1)) - | Store n => (? T Ts. st = T#Ts & Some(OK(Ts,reg[n := OK T])) <<=_S ss!(p+1)) - | AConst_Null => size st < maxs & Some(OK(NullT#st,reg)) <<=_S ss!(p+1) - | IConst i => size st < maxs & Some(OK(Integer#st,reg)) <<=_S ss!(p+1) - | IAdd => (? Ts. st = Integer#Integer#Ts & - Some(OK(Integer#Ts,reg)) <<=_S ss!(p+1)) - | Getfield fT C => (? T Ts. st = T#Ts & T [=_S Class(C) & - Some(OK(fT#Ts,reg)) <<=_S ss!(p+1)) - | Putfield fT C => (? vT oT Ts. st = vT#oT#Ts & vT [=_S fT & oT [=_S Class C & - Some(OK(Ts,reg)) <<=_S ss!(p+1)) - | New C => (size st < maxs & Some(OK((Class C)#st,reg)) <<=_S ss!(p+1)) - | Invoke C m pT rT => - (? aT oT Ts. st = aT#oT#Ts & oT [=_S Class C & aT [=_S pT & - Some(OK(rT#Ts,reg)) <<=_S ss!(p+1)) - | CmpEq q => (? T1 T2 Ts. st = T1#T2#Ts & (T1=T2 | is_ref T1 & is_ref T2) & - Some(OK(Ts,reg)) <<=_S ss!(p+1) & - Some(OK(Ts,reg)) <<=_S ss!q) - | Return => (? T Ts. st = T#Ts & T [=_S rT)))" - - succs :: "instr list => nat => nat list" -"succs bs p == - case bs!p of - Load n => [p+1] - | Store n => [p+1] - | AConst_Null => [p+1] - | IConst i => [p+1] - | IAdd => [p+1] - | Getfield x C => [p+1] - | Putfield x C => [p+1] - | New C => [p+1] - | Invoke C m pT rT => [p+1] - | CmpEq q => [p+1,q] - | Return => [p]" - - exec :: "subclass => nat => ty => instr => config => config err" -"exec S maxs rT instr == %(st,reg). - case instr of - Load n => if size st < maxs - then case reg!n of Err => Err | OK T => OK(T#st,reg) - else Err - | Store n => (case st of [] => Err | T#Ts => OK(Ts,reg[n := OK T])) - | AConst_Null => if size st < maxs then OK(NullT#st,reg) else Err - | IConst i => if size st < maxs then OK(Integer#st,reg) else Err - | IAdd => - (case st of [] => Err | T1#st1 => - (case st1 of [] => Err | T2#st2 => - if T1 = Integer & T2 = Integer then OK(st1,reg) else Err)) - | Getfield fT C => - (case st of [] => Err | oT#st' => - (if oT [=_S Class(C) then OK(fT#st',reg) else Err)) - | Putfield fT C => - (case st of [] => Err | vT#st1 => - (case st1 of [] => Err | oT#st2 => - if vT [=_S fT & oT [=_S Class C then OK(st2,reg) else Err)) - | New C => if size st < maxs then OK((Class C)#st,reg) else Err - | Invoke C m pT rT => - (case st of [] => Err | aT#st1 => - (case st1 of [] => Err | oT#st2 => - if oT [=_S Class C & aT [=_S pT then OK(rT#st2,reg) else Err)) - | CmpEq q => - (case st of [] => Err | T1#st1 => - (case st1 of [] => Err | T2#st2 => - if T1=T2 | is_ref T1 & is_ref T2 then OK(st2,reg) else Err)) - | Return => - (case st of [] => Err | T#Ts => - if T [=_S rT then OK(st,reg) else Err)" - - step :: "subclass => nat => ty => instr list => nat => state => state" -"step S maxs rT bs p == option_map (lift (exec S maxs rT (bs!p)))" - - kiljvm :: - "subclass => nat => nat => ty => instr list => state list => state list" -"kiljvm S maxs maxr rT bs == - kildall (sl S maxs maxr) (step S maxs rT bs) (succs bs)" - -end diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Kildall.ML --- a/src/HOL/BCV/Kildall.ML Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,351 +0,0 @@ -(* Title: HOL/BCV/Kildall.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM -*) - -Addsimps [Let_def]; -Addsimps [le_iff_plus_unchanged RS sym]; - -Goalw [pres_type_def] - "[| pres_type step n A; s:A; p step p s : A"; -by (Blast_tac 1); -qed "pres_typeD"; - -Goalw [bounded_def] - "[| bounded succs n; p < n; q : set(succs p) |] ==> q < n"; -by (Blast_tac 1); -qed "boundedD"; - -Goalw [mono_def] - "[| mono r step n A; p < n; s:A; s <=_r t |] ==> step p s <=_r step p t"; -by (Blast_tac 1); -qed "monoD"; - -(** merges **) - -Goal "!ss. size(merges f t ps ss) = size ss"; -by (induct_tac "ps" 1); -by (Auto_tac); -qed_spec_mp "length_merges"; -Addsimps [length_merges]; - -Goalw [closed_def] - "[| semilat(A,r,f) |] ==> \ -\ !xs. xs : list n A --> x : A --> (!p : set ps. p merges f x ps xs : list n A"; -by (ftac semilatDclosedI 1); -by (rewtac closed_def); -by (induct_tac "ps" 1); -by (Auto_tac); -qed_spec_mp "merges_preserves_type"; -Addsimps [merges_preserves_type]; - -Goal - "[| semilat(A,r,f) |] ==> \ -\ !xs. xs : list n A --> x : A --> (!p:set ps. p xs <=[r] merges f x ps xs"; -by (induct_tac "ps" 1); - by (Asm_simp_tac 1); -by (Asm_full_simp_tac 1); -by (Clarify_tac 1); -by (rtac order_trans 1); - by (Asm_simp_tac 1); - by (etac list_update_incr 1); - by (assume_tac 1); - by (Asm_simp_tac 1); - by (Asm_simp_tac 1); -by (blast_tac (claset() addSIs [listE_set] - addIs [closedD,listE_length RS nth_in]) 1); -qed_spec_mp "merges_incr"; - -Goal - "[| semilat(A,r,f) |] ==> \ -\ (!xs. xs : list n A --> x:A --> (!p:set ps. p \ -\ (merges f x ps xs = xs) = (!p:set ps. x <=_r xs!p))"; -by (induct_tac "ps" 1); - by (Asm_simp_tac 1); -by (Clarsimp_tac 1); -by (rename_tac "p ps xs" 1); -by (rtac iffI 1); - by (rtac context_conjI 1); - by (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs" 1); - by (EVERY[etac subst 2, rtac merges_incr 2]); - by (force_tac (claset() addSDs [le_listD], - simpset() addsimps [nth_list_update]) 1); - by (assume_tac 1); - by (blast_tac (claset() addSIs [listE_set] - addIs [closedD,listE_length RS nth_in]) 1); - by (assume_tac 1); - by (Asm_simp_tac 1); - by (Clarify_tac 1); - by (rotate_tac ~2 1); - by (asm_full_simp_tac (simpset() addsimps - [le_iff_plus_unchanged RS iffD1, - list_update_same_conv RS iffD2]) 1); -by (Clarify_tac 1); -by (asm_simp_tac (simpset() addsimps - [le_iff_plus_unchanged RS iffD1, - list_update_same_conv RS iffD2]) 1); -qed_spec_mp "merges_same_conv"; - - -Goalw [Listn.le_def,lesub_def,semilat_def] - "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"; -by (simp_tac (simpset() addsimps [list_all2_conv_all_nth,nth_list_update]) 1); -qed_spec_mp "list_update_le_listI"; - -Goalw [closed_def] - "[| semilat(A,r,f); set ts <= A; t:A; \ -\ !p. p:set ps --> t <=_r ts!p; \ -\ !p. p:set ps --> p \ -\ set qs <= set ps --> \ -\ (!ss. set ss <= A --> ss <=[r] ts --> merges f t qs ss <=[r] ts)"; -by (induct_tac "qs" 1); - by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Clarify_tac 1); -by (rotate_tac ~2 1); -by (Asm_full_simp_tac 1); -by (EVERY[etac allE 1, etac impE 1, etac mp 2]); - by (asm_simp_tac (simpset() addsimps [closedD]) 1); -by (asm_full_simp_tac (simpset() addsimps [list_update_le_listI]) 1); -val lemma = result(); - -Goal - "[| 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 merges f t ps ss <=[r] ts"; -by (blast_tac (claset() addDs [lemma]) 1); -qed "merges_pres_le_ub"; - -Goal "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A --> \ -\ (!p:set ps. p \ -\ (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)"; -by (induct_tac "ps" 1); - by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [nth_list_update,closedD,listE_nth_in]) 1); -qed_spec_mp "nth_merges"; - - -(** propa **) - -Goal "!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)"; -by (induct_tac "qs" 1); - by (Simp_tac 1); -by (Simp_tac 1); -by (Clarify_tac 1); -by (rtac conjI 1); - by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1); - by (Blast_tac 1); -by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1); -by (Blast_tac 1); -qed_spec_mp "decomp_propa"; - -(** iter **) - -val [iter_wf,iter_tc] = iter.tcs; - -goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf)); -by (REPEAT(rtac wf_same_fst 1)); -by (split_all_tac 1); -by (asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1); -by (REPEAT(rtac wf_same_fst 1)); -by (rtac wf_lex_prod 1); - by (rtac wf_finite_psubset 2); (* FIXME *) -by (Clarify_tac 1); -by (dtac (semilatDorderI RS acc_le_listI) 1); - by (assume_tac 1); -by (rewrite_goals_tac [acc_def,lesssub_def]); -by (assume_tac 1); -qed "iter_wf"; - -Goalw [lesssub_def] - "[| 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"; -by (asm_simp_tac (simpset() addsimps [merges_incr]) 1); -by (rtac impI 1); -by (dtac (sym RS (rotate_prems 4 (merges_same_conv RS iffD1))) 1); - by (assume_tac 1); - by (assume_tac 1); - by (assume_tac 1); - by (Asm_simp_tac 1); -by (asm_simp_tac (simpset() addcongs [conj_cong] - addsimps [le_iff_plus_unchanged RS sym]) 1); -by (blast_tac (claset() addSIs [psubsetI] addEs [equalityE]) 1); -qed "inter_tc_lemma"; - -goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc)); -by (asm_simp_tac (simpset() addsimps [same_fst_def,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 [listI]) 2); -by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1); - by (blast_tac (claset() addDs [boundedD]) 2); -by (rotate_tac 1 1); -by (asm_full_simp_tac (simpset() delsimps [listE_length] - addsimps [decomp_propa,finite_psubset_def,inter_tc_lemma, - bounded_nat_set_is_finite]) 1); -qed "iter_tc"; - -val prems = goal thy - "(!!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"; -by (res_inst_tac [("P","P")] (iter_tc RS (iter_wf RS iter.induct)) 1); -by (rename_tac "w" 1); -by (resolve_tac prems 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset()) 1); -by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1); - by (rotate_tac ~1 1); - by (asm_full_simp_tac (simpset() addsimps [decomp_propa]) 1); -by (subgoal_tac "(@p. p:w) : w" 1); - by (fast_tac (claset() addIs [someI]) 2); -by (blast_tac (claset() addDs [boundedD]) 1); -qed "iter_induct"; - -Goal - "[| semilat(A,r,f); acc r; set ss <= A; pres_type step (length ss) A; \ -\ bounded succs (size ss); !p:w. p \ -\ 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})))"; -by (rtac ((iter_tc RS (iter_wf RS (hd iter.simps))) RS trans) 1); -by (Asm_simp_tac 1); -by (rtac impI 1); -by (stac decomp_propa 1); - by (subgoal_tac "(@p. p:w) : w" 1); - by (fast_tac (claset() addIs [someI]) 2); - by (blast_tac (claset() addDs [boundedD]) 1); -by (Simp_tac 1); -qed "iter_unfold"; - -Goalw [stable_def] - "[| 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"; -by (subgoal_tac "step p (ss!p) : A" 1); - by (blast_tac (claset() addIs [listE_nth_in,pres_typeD]) 2); -by (Simp_tac 1); -by (Clarify_tac 1); -by (stac nth_merges 1); - by (assume_tac 1); - by (assume_tac 1); - by (assume_tac 2); - by (blast_tac (claset() addDs [boundedD]) 1); - by (blast_tac (claset() addDs [boundedD]) 1); -by (stac nth_merges 1); - by (assume_tac 1); - by (assume_tac 1); - by (assume_tac 2); - by (blast_tac (claset() addDs [boundedD]) 1); - by (blast_tac (claset() addDs [boundedD]) 1); -by (Simp_tac 1); -by (rtac conjI 1); - by (Clarify_tac 1); - by (asm_simp_tac (simpset() delsimps [listE_length]) 1); - by (blast_tac (claset() addSIs [semilat_ub1,semilat_ub2,listE_nth_in] addIs [order_trans]addDs [boundedD]) 1); -by (blast_tac (claset() addSIs [semilat_ub1,semilat_ub2,listE_nth_in] addIs [order_trans]addDs [boundedD]) 1); -qed "stable_pres_lemma"; - -Goalw [stable_def] - "[| 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"; -by (blast_tac (claset() - addSIs [listE_set,monoD,listE_nth_in,le_listD,less_lengthI] - addIs [merges_pres_le_ub,order_trans] - addDs [pres_typeD,boundedD]) 1); -qed_spec_mp "merges_bounded_lemma"; - -Unify.trace_bound := 80; -Unify.search_bound := 90; -Goalw [stables_def] - "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 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)"; -by (res_inst_tac [("A","A"),("r","r"),("f","f"),("step","step"),("ss","ss"),("w","w")]iter_induct 1); -by (Clarify_tac 1); -by (ftac listE_length 1); -by (hyp_subst_tac 1); -by (stac iter_unfold 1); - by (assume_tac 1); - by (assume_tac 1); - by (Asm_simp_tac 1); - by (assume_tac 1); - by (assume_tac 1); - by (assume_tac 1); -by (asm_simp_tac (simpset() delsimps [listE_length]) 1); -by (rtac impI 1); -by (etac allE 1); -by (etac impE 1); - by (asm_simp_tac (simpset() delsimps [listE_length]) 1); -by (subgoal_tac "(@p. p:w) : w" 1); - by (fast_tac (claset() addIs [someI]) 2); -by (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1); - by (blast_tac (claset() addIs [pres_typeD,listE_nth_in]) 2); -by (etac impE 1); - by (asm_simp_tac (simpset() delsimps [listE_length,le_iff_plus_unchanged RS sym]) 1); - by (rtac conjI 1); - by (blast_tac (claset() addDs [boundedD]) 1); - by (rtac conjI 1); - by (blast_tac (claset() addIs[merges_preserves_type]addDs[boundedD]) 1); - by (blast_tac (claset() addSIs [stable_pres_lemma]) 1); -by (asm_simp_tac (simpset() delsimps [listE_length]) 1); -by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1); - by (blast_tac (claset() addDs [boundedD]) 2); -by (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A" 1); - by (blast_tac (claset() addIs [pres_typeD]) 2); -by (rtac conjI 1); - by (blast_tac (claset() addSIs [merges_incr] addIs [le_list_trans]) 1); -by (Clarify_tac 1); -by (EVERY1[dtac bspec, atac, etac mp]); -by (asm_full_simp_tac (simpset() delsimps [listE_length]) 1); -by (blast_tac (claset() addIs [merges_bounded_lemma]) 1); -qed_spec_mp "iter_properties"; - - -Goalw [is_dfa_def,kildall_def] - "[| 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"; -by (Clarify_tac 1); -by (Simp_tac 1); -by (rtac iter_properties 1); -by (asm_simp_tac (simpset() addsimps [unstables_def,stable_def]) 1); -by (blast_tac (claset() addSIs [le_iff_plus_unchanged RS iffD2,listE_nth_in] - addDs [boundedD,pres_typeD]) 1); -qed "is_dfa_kildall"; - -Goal - "[| semilat(A,r,f); acc r; top r T; \ -\ pres_type step n A; bounded succs n; \ -\ mono r step n A; wti_is_stable_topless r T step wti succs n A |] \ -\ ==> is_bcv r T wti n A (kildall (A,r,f) step succs)"; -by (REPEAT(ares_tac [is_bcv_dfa,is_dfa_kildall,semilatDorderI] 1)); -qed "is_bcv_kildall"; diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Kildall.thy --- a/src/HOL/BCV/Kildall.thy Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,62 +0,0 @@ -(* Title: HOL/BCV/Kildall.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM - -Kildall's algorithm -*) - -Kildall = DFA_Framework + - -constdefs - bounded :: "(nat => nat list) => nat => bool" -"bounded succs n == !p 's => 's) => nat => 's set => bool" -"pres_type step n A == !s:A. !p (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])" - -end diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Listn.ML --- a/src/HOL/BCV/Listn.ML Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,423 +0,0 @@ -(* Title: HOL/BCV/Listn.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM -*) - -Addsimps [set_update_subsetI]; - -Goalw [lesub_def] "xs <=[r] ys == Listn.le r xs ys"; -by (Simp_tac 1); -qed "unfold_lesub_list"; - -Goalw [lesub_def,Listn.le_def] "([] <=[r] ys) = (ys = [])"; -by (Simp_tac 1); -qed "Nil_le_conv"; - -Goalw [lesub_def,Listn.le_def] "~ x#xs <=[r] []"; -by (Simp_tac 1); -qed "Cons_notle_Nil"; - -AddIffs [Nil_le_conv,Cons_notle_Nil]; - -Goalw [lesub_def,Listn.le_def] "x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)"; -by (Simp_tac 1); -qed "Cons_le_Cons"; -AddIffs [Cons_le_Cons]; - -Goalw [lesssub_def] "order r ==> \ -\ x#xs <_(Listn.le r) y#ys = \ -\ (x <_r y & xs <=[r] ys | x = y & xs <_(Listn.le r) ys)"; -by (Blast_tac 1); -qed "Cons_less_Cons"; -Addsimps [Cons_less_Cons]; - -Goalw [unfold_lesub_list] - "[| i xs[i:=x] <=[r] ys[i:=y]"; -by (rewtac Listn.le_def); -by (asm_full_simp_tac (simpset() addsimps [list_all2_conv_all_nth,nth_list_update]) 1); -qed "list_update_le_cong"; - - -Goalw [Listn.le_def,lesub_def] - "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p"; -by (asm_full_simp_tac (simpset() addsimps [list_all2_conv_all_nth]) 1); -qed "le_listD"; - -Goalw [unfold_lesub_list] "!x. x <=_r x ==> xs <=[r] xs"; -by (asm_simp_tac (simpset() addsimps [Listn.le_def,list_all2_conv_all_nth]) 1); -qed "le_list_refl"; - -Goalw [unfold_lesub_list] - "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs"; -by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1); -by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addIs [order_trans]) 1); -qed "le_list_trans"; - -Goalw [unfold_lesub_list] - "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys"; -by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1); -by (rtac nth_equalityI 1); - by (Blast_tac 1); -by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addIs [order_antisym]) 1); -qed "le_list_antisym"; - -Goal "order r ==> order(Listn.le r)"; -by (stac order_def 1); -by (blast_tac (claset() addIs [le_list_refl,le_list_trans,le_list_antisym] - addDs [order_refl]) 1); -qed "order_listI"; -Addsimps [order_listI]; -AddSIs [order_listI]; - - -Goalw [Listn.le_def,lesub_def] "xs <=[r] ys ==> size ys = size xs"; -by (asm_full_simp_tac(simpset()addsimps[list_all2_conv_all_nth])1); -qed "lesub_list_impl_same_size"; -Addsimps [lesub_list_impl_same_size]; - -Goalw [lesssub_def] "xs <_(Listn.le r) ys ==> size ys = size xs"; -by (Auto_tac); -qed "lesssub_list_impl_same_size"; - -Goalw [list_def] "[| length xs = n; set xs <= A |] ==> xs : list n A"; -by (Blast_tac 1); -qed "listI"; - -Goalw [list_def] "xs : list n A ==> length xs = n"; -by (Blast_tac 1); -qed "listE_length"; -Addsimps [listE_length]; - -Goal "[| xs : list n A; p < n |] ==> p < length xs"; -by (Asm_simp_tac 1); -qed "less_lengthI"; - -Goalw [list_def] "xs : list n A ==> set xs <= A"; -by (Blast_tac 1); -qed "listE_set"; -Addsimps [listE_set]; - -Goalw [list_def] "list 0 A = {[]}"; -by (Auto_tac); -qed "list_0"; -Addsimps [list_0]; - -Goalw [list_def] - "(xs : list (Suc n) A) = (? y:A. ? ys:list n A. xs = y#ys)"; -by (case_tac "xs" 1); -by (Auto_tac); -qed "in_list_Suc_iff"; - -Goal "(x#xs : list (Suc n) A) = (x:A & xs : list n A)"; -by (simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); -qed "Cons_in_list_Suc"; -AddIffs [Cons_in_list_Suc]; - -Goal "? a. a:A ==> ? xs. xs : list n A"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); -by (Blast_tac 1); -qed "list_not_empty"; - - -Goal "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); -qed_spec_mp "nth_in"; -Addsimps [nth_in]; - -Goal "[| xs : list n A; i < n |] ==> (xs!i) : A"; -by (blast_tac (HOL_cs addIs [nth_in,listE_length,listE_set]) 1); -qed "listE_nth_in"; - -Goalw [list_def] - "[| xs : list n A; x:A |] ==> xs[i := x] : list n A"; -by (Asm_full_simp_tac 1); -qed "list_update_in_list"; -Addsimps [list_update_in_list]; -AddSIs [list_update_in_list]; - -Goalw [plussub_def,map2_def] "[] +[f] xs = []"; -by (Simp_tac 1); -qed "plus_list_Nil"; -Addsimps [plus_list_Nil]; - -Goal - "(x#xs) +[f] ys = (case ys of [] => [] | y#ys => (x +_f y)#(xs +[f] ys))"; -by (simp_tac (simpset() addsimps [plussub_def,map2_def] addsplits [list.split]) 1); -qed "plus_list_Cons"; -Addsimps [plus_list_Cons]; - -Goal "!ys. length(xs +[f] ys) = min(length xs) (length ys)"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (asm_simp_tac (simpset() addsplits [list.split]) 1); -qed_spec_mp "length_plus_list"; -Addsimps [length_plus_list]; - -Goal - "!xs ys i. length xs = n --> length ys = n --> i \ -\ (xs +[f] ys)!i = (xs!i) +_f (ys!i)"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (case_tac "xs" 1); - by (Asm_full_simp_tac 1); -by (force_tac (claset(),simpset() addsimps [nth_Cons] - addsplits [list.split,nat.split]) 1); -qed_spec_mp "nth_plus_list"; -Addsimps [nth_plus_list]; - -Goalw [unfold_lesub_list] - "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |] \ -\ ==> xs <=[r] xs +[f] ys"; -by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1); -qed_spec_mp "plus_list_ub1"; - -Goalw [unfold_lesub_list] - "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |] \ -\ ==> ys <=[r] xs +[f] ys"; -by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1); -qed_spec_mp "plus_list_ub2"; - -Goalw [unfold_lesub_list] - "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"; -by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1); -qed_spec_mp "plus_list_lub"; - -Goalw [unfold_lesub_list] - "[| semilat(A,r,f); x:A |] ==> set xs <= A --> \ -\ (!i. i xs <=[r] xs[i := x +_f xs!i])"; -by (simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1); -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); -by (Clarify_tac 1); -by (asm_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); -qed_spec_mp "list_update_incr"; - -Goalw [acc_def] "[| order r; acc r |] ==> acc(Listn.le r)"; -by (subgoal_tac - "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})" 1); - by (etac wf_subset 1); - by (blast_tac (claset() addIs [lesssub_list_impl_same_size]) 1); -by (rtac wf_UN 1); - by (Clarify_tac 2); - by (rename_tac "m n" 2); - by (case_tac "m=n" 2); - by (Asm_full_simp_tac 2); - by (rtac conjI 2); - by (fast_tac (claset() addSIs [equals0I] addDs [not_sym]) 2); - by (fast_tac (claset() addSIs [equals0I] addDs [not_sym]) 2); -by (Clarify_tac 1); -by (rename_tac "n" 1); -by (induct_tac "n" 1); - by (simp_tac (simpset() addsimps [lesssub_def] addcongs [conj_cong]) 1); -by (rename_tac "k" 1); -by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); -by (simp_tac (simpset() addsimps [length_Suc_conv] addcongs [conj_cong]) 1); -by (Clarify_tac 1); -by (rename_tac "M m" 1); -by (case_tac "? x xs. size xs = k & x#xs : M" 1); - by (etac thin_rl 2); - by (etac thin_rl 2); - by (Blast_tac 2); -by (eres_inst_tac [("x","{a. ? xs. size xs = k & a#xs:M}")] allE 1); -by (etac impE 1); - by (Blast_tac 1); -by (thin_tac "? x xs. ?P x xs" 1); -by (Clarify_tac 1); -by (rename_tac "maxA xs" 1); -by (eres_inst_tac [("x","{ys. size ys = size xs & maxA#ys : M}")] allE 1); -by (etac impE 1); - by (Blast_tac 1); -by (Clarify_tac 1); -by (thin_tac "m : M" 1); -by (thin_tac "maxA#xs : M" 1); -by (rtac bexI 1); - by (assume_tac 2); -by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -by (Blast_tac 1); -qed "acc_le_listI"; -AddSIs [acc_le_listI]; - - -Goalw [closed_def] - "closed S f ==> closed (list n S) (map2 f)"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); -by (Clarify_tac 1); -by (Simp_tac 1); -by (Blast_tac 1); -qed "closed_listI"; - - -Goalw [Listn.sl_def] - "!!L. semilat L ==> semilat (Listn.sl n L)"; -by (split_all_tac 1); -by (simp_tac (HOL_basic_ss addsimps [semilat_Def, split_conv]) 1); -by (rtac conjI 1); - by (Asm_simp_tac 1); -by (rtac conjI 1); - by (asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_listI]) 1); -by (simp_tac (HOL_basic_ss addsimps [list_def]) 1); -by (asm_simp_tac (simpset() addsimps [plus_list_ub1,plus_list_ub2,plus_list_lub]) 1); -qed "semilat_Listn_sl"; - - -Goal "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); -by (Clarify_tac 1); -by (simp_tac (simpset() addsimps [plussub_def,Err.sup_def,lift2_def] addsplits [err.split]) 1); -by (Force_tac 1); -qed_spec_mp "coalesce_in_err_list"; - - -Goal "x +_(op #) xs = x#xs"; -by (simp_tac (simpset() addsimps [plussub_def]) 1); -val lemma = result(); - -Goal - "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))"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); -by (Clarify_tac 1); -by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); -by (force_tac (claset(), simpset() addsimps [semilat_le_err_OK1]) 1); -qed_spec_mp "coalesce_eq_OK1_D"; - -Goal - "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))"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); -by (Clarify_tac 1); -by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); -by (force_tac (claset(), simpset() addsimps [semilat_le_err_OK2]) 1); -qed_spec_mp "coalesce_eq_OK2_D"; - -Goalw [semilat_Def,plussub_def,err_def] - "[| 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"; -by (asm_full_simp_tac (simpset() addsimps [lift2_def]) 1); -by (Clarify_tac 1); -by (rotate_tac ~3 1); -by (etac thin_rl 1); -by (etac thin_rl 1); -by (Force_tac 1); -qed "lift2_le_ub"; - -Goal - "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))"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); -by (Clarify_tac 1); -by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); -by (Clarify_tac 1); -by (rtac conjI 1); - by (Blast_tac 2); -by (blast_tac (claset() addIs [lift2_le_ub]) 1); -qed_spec_mp "coalesce_eq_OK_ub_D"; - -Goal - "[| 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 (asm_simp_tac (simpset() addsimps [OK_plus_OK_eq_Err_conv RS iffD1]) 1); -qed "lift2_eq_ErrD"; - -Goal - "[| 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))"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); -by (Clarify_tac 1); -by (full_simp_tac (simpset() addsplits [err.split_asm] addsimps [lemma,Err.sup_def,lift2_def]) 1); - by (blast_tac (claset() addDs [lift2_eq_ErrD]) 1); -by (Blast_tac 1); -qed_spec_mp "coalesce_eq_Err_D"; - - -Goalw [closed_def] - "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)"; -by (simp_tac (simpset() addsimps [err_def]) 1); -qed "closed_err_lift2_conv"; - -Goalw [map2_def] - "closed (err A) (lift2 f) ==> \ -\ !xs. xs : list n A --> (!ys. ys : list n A --> \ -\ map2 f xs ys : list n (err A))"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1); -by (Clarify_tac 1); -by (full_simp_tac (simpset() addsimps [plussub_def,closed_err_lift2_conv]) 1); -by (Blast_tac 1); -qed_spec_mp "closed_map2_list"; - -Goal - "closed (err A) (lift2 f) ==> \ -\ closed (err (list n A)) (lift2 (sup f))"; -by (fast_tac (claset() addss (simpset() addsimps - [closed_def,plussub_def,sup_def,lift2_def, - coalesce_in_err_list,closed_map2_list] - addsplits [err.split])) 1); -qed "closed_lift2_sup"; - -Goalw [Err.sl_def] - "err_semilat (A,r,f) ==> \ -\ err_semilat (list n A, Listn.le r, sup f)"; -by (asm_full_simp_tac (HOL_basic_ss addsimps [split_conv]) 1); -by (simp_tac (HOL_basic_ss addsimps [semilat_Def,plussub_def]) 1); -by (asm_simp_tac(HOL_basic_ss addsimps [semilatDclosedI,closed_lift2_sup]) 1); -by (rtac conjI 1); - by (dtac semilatDorderI 1); - by (Asm_full_simp_tac 1); -by (simp_tac (HOL_basic_ss addsimps - [unfold_lesub_err,Err.le_def,err_def,sup_def,lift2_def]) 1); -by (asm_simp_tac (simpset() addsimps - [coalesce_eq_OK1_D,coalesce_eq_OK2_D] addsplits [err.split]) 1); -by (blast_tac (claset()addIs[coalesce_eq_OK_ub_D] addDs [coalesce_eq_Err_D]) 1); -qed "err_semilat_sup"; - -Goalw [Listn.upto_esl_def] - "!!L. err_semilat L ==> err_semilat(upto_esl m L)"; -by (split_all_tac 1); -by (Asm_full_simp_tac 1); -by (fast_tac (claset() - addSIs [err_semilat_UnionI,err_semilat_sup] - addDs [lesub_list_impl_same_size] addss (simpset() - addsimps [plussub_def,Listn.sup_def])) 1); -qed "err_semilat_upto_esl"; diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Listn.thy --- a/src/HOL/BCV/Listn.thy Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,50 +0,0 @@ -(* Title: HOL/BCV/Listn.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM - -Lists of a fixed length -*) - -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)" - -end diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Opt.ML --- a/src/HOL/BCV/Opt.ML Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,105 +0,0 @@ -(* Title: HOL/BCV/Opt.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM -*) - -Goalw [lesub_def,le_def] - "o1 <=_(le r) o2 = \ -\ (case o2 of None => o1=None | \ -\ Some y => (case o1 of None => True | Some x => x <=_r y))"; -by (rtac refl 1); -qed "unfold_le_opt"; - -Goal "order r ==> o1 <=_(le r) o1"; -by (asm_simp_tac (simpset() addsimps [unfold_le_opt] addsplits [option.split]) 1); -qed "le_opt_refl"; - -Goal "order r ==> \ -\ o1 <=_(le r) o2 --> o2 <=_(le r) o3 --> o1 <=_(le r) o3"; -by (simp_tac (simpset() addsimps [unfold_le_opt] addsplits [option.split]) 1); -by (blast_tac (claset() addIs [order_trans]) 1); -qed_spec_mp "le_opt_trans"; - -Goal "order r ==> o1 <=_(le r) o2 --> o2 <=_(le r) o1 --> o1=o2"; -by (simp_tac (simpset() addsimps [unfold_le_opt] addsplits [option.split]) 1); -by (blast_tac (claset() addIs [order_antisym]) 1); -qed_spec_mp "le_opt_antisym"; - -Goal "order r ==> order(le r)"; -by (stac order_def 1); -by (blast_tac (claset() addIs [le_opt_refl,le_opt_trans,le_opt_antisym]) 1); -qed "order_le_opt"; -AddSIs [order_le_opt]; -Addsimps [order_le_opt]; - -Goalw [lesub_def,le_def] "None <=_(le r) ox"; -by (simp_tac (simpset() addsplits [option.split]) 1); -qed "None_bot"; -AddIffs [None_bot]; - -Goalw [lesub_def,le_def] - "(Some x <=_(le r) ox) = (? y. ox = Some y & x <=_r y)"; -by (simp_tac (simpset() addsplits [option.split]) 1); -qed "Some_le"; -AddIffs [Some_le]; - -Goalw [lesub_def,le_def] "(ox <=_(le r) None) = (ox = None)"; -by (simp_tac (simpset() addsplits [option.split]) 1); -qed "le_None"; -AddIffs [le_None]; - - -Goalw [Opt.sl_def,semilat_def,closed_def, split_conv RS eq_reflection] - "!!L. semilat L ==> semilat (Opt.sl L)"; -by (split_all_tac 1); -by (asm_full_simp_tac (simpset() addsplits [option.split] - addsimps [lesub_def,Opt.le_def,plussub_def,Opt.sup_def,opt_def,Bex_def]) 1); -by (asm_full_simp_tac (simpset() addsimps [order_def,lesub_def]) 1); -qed "semilat_opt"; - - -Goalw [top_def] "top (le r) (Some T) = top r T"; -by (rtac iffI 1); - by (Blast_tac 1); -by (rtac allI 1); -by (case_tac "x" 1); -by (ALLGOALS Asm_simp_tac); -qed "top_le_opt_Some"; -AddIffs [top_le_opt_Some]; - -Goalw [top_def] "[| order r; top r T |] ==> (T <=_r x) = (x = T)"; -by (blast_tac (claset() addIs [order_antisym]) 1); -qed "Top_le_conv"; - - -Goalw [opt_def] "None : opt A"; -by (Simp_tac 1); -qed "None_in_opt"; -AddIffs [None_in_opt]; - -Goalw [opt_def] "(Some x : opt A) = (x:A)"; -by (Auto_tac); -qed "Some_in_opt"; -AddIffs [Some_in_opt]; - -Goalw [acc_def,lesub_def,le_def,lesssub_def] "acc r ==> acc(le r)"; -by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal] addsplits [option.split]) 1); -by (Clarify_tac 1); -by (case_tac "? a. Some a : Q" 1); - by (eres_inst_tac [("x","{a . Some a : Q}")] allE 1); - by (Blast_tac 1); -by (case_tac "x" 1); - by (Blast_tac 1); -by (Blast_tac 1); -qed "acc_le_optI"; -AddSIs [acc_le_optI]; - - -Goalw [option_map_def] - "[| ox : opt S; !x:S. ox = Some x --> f x : S |] \ -\ ==> option_map f ox : opt S"; -by (asm_simp_tac (simpset() addsplits [option.split]) 1); -by (Blast_tac 1); -qed "option_map_in_optionI"; - diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Opt.thy --- a/src/HOL/BCV/Opt.thy Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* Title: HOL/BCV/Opt.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM - -More about options -*) - -Opt = Semilat + - -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 binop => 'a option binop -"sup f o1 o2 == - case o1 of None => o2 | Some x => (case o2 of None => o1 - | Some y => Some(f x y))" - - sl :: "'a sl => 'a option sl" -"sl == %(A,r,f). (opt A, le r, sup f)" - -end diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Product.ML --- a/src/HOL/BCV/Product.ML Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,114 +0,0 @@ -(* Title: HOL/BCV/Product.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM -*) - -Goalw [lesub_def] "p <=(rA,rB) q == le rA rB p q"; -by (Simp_tac 1); -qed "unfold_lesub_prod"; - -Goalw [lesub_def,le_def] - "((a1,b1) <=(rA,rB) (a2,b2)) = (a1 <=_rA a2 & b1 <=_rB b2)"; -by (Simp_tac 1); -qed "le_prod_Pair_conv"; -AddIffs [le_prod_Pair_conv]; - -Goalw [lesssub_def] - "((a1,b1) <_(Product.le rA rB) (a2,b2)) = \ -\ (a1 <_rA a2 & b1 <=_rB b2 | a1 <=_rA a2 & b1 <_rB b2)"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "less_prod_Pair_conv"; - -Goalw [order_def] "order(Product.le rA rB) = (order rA & order rB)"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "order_le_prod"; -AddIffs [order_le_prod]; - - -Goalw [acc_def] "[| acc rA; acc rB |] ==> acc(Product.le rA rB)"; -by (rtac wf_subset 1); - by (etac wf_lex_prod 1); - by (assume_tac 1); -by (auto_tac (claset(), simpset() - addsimps [lesssub_def,less_prod_Pair_conv,lex_prod_def])); -qed "acc_le_prodI"; -AddSIs [acc_le_prodI]; - - -Goalw [closed_def,plussub_def,lift2_def,err_def,sup_def] - "[| closed (err A) (lift2 f); closed (err B) (lift2 g) |] ==> \ -\ closed (err(A<*>B)) (lift2(sup f g))"; -by (asm_full_simp_tac (simpset() addsplits [err.split]) 1); -by (Blast_tac 1); -qed "closed_lift2_sup"; - -Goalw [plussub_def] "e1 +_(lift2 f) e2 == lift2 f e1 e2"; -by (Simp_tac 1); -qed "unfold_plussub_lift2"; - -Goal - "[| x:A; y:A; semilat(err A, Err.le r, lift2 f) |] ==> \ -\ (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"; -by (rtac iffI 1); - by (Clarify_tac 1); - by (dtac (OK_le_err_OK RS iffD2) 1); - by (dtac (OK_le_err_OK RS iffD2) 1); - by (dtac semilat_lub 1); - by (assume_tac 1); - by (assume_tac 1); - by (Asm_simp_tac 1); - by (Asm_simp_tac 1); - by (Asm_simp_tac 1); - by (Asm_full_simp_tac 1); -by (case_tac "x +_f y" 1); - by (assume_tac 1); -by (rename_tac "z" 1); -by (subgoal_tac "OK z: err A" 1); - by (ftac (rotate_prems 2 (read_instantiate_sg(sign_of Err.thy)[("x","OK(x::'a)"),("y","OK(y::'a)")]plus_le_conv RS iffD1))1); - by (assume_tac 1); - by (Asm_simp_tac 1); - by (blast_tac (claset() addDs [semilatDorderI,order_refl]) 1); - by (Asm_simp_tac 1); - by (Asm_simp_tac 1); - by (Blast_tac 1); -by (etac subst 1); -by (rewrite_goals_tac [semilat_def,err_def,closed_def]); -by (Asm_full_simp_tac 1); -qed "plus_eq_Err_conv"; -Addsimps [plus_eq_Err_conv]; - -Goalw [esl_def,Err.sl_def] - "!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)"; -by (split_all_tac 1); -by (Asm_full_simp_tac 1); -by (simp_tac (HOL_basic_ss addsimps [semilat_Def]) 1); -by (asm_simp_tac(HOL_basic_ss addsimps[semilatDclosedI,closed_lift2_sup])1); -by (simp_tac (HOL_basic_ss addsimps - [unfold_lesub_err,Err.le_def,unfold_plussub_lift2,sup_def]) 1); -by (auto_tac (claset() addEs [semilat_le_err_OK1,semilat_le_err_OK2], - simpset() addsimps [lift2_def] addsplits [err.split])); -by (blast_tac (claset() addDs [semilatDorderI]) 1); -by (blast_tac (claset() addDs [semilatDorderI]) 1); - -by (rtac (OK_le_err_OK RS iffD1) 1); -by (etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); - -by (rtac (OK_le_err_OK RS iffD1) 1); -by (etac subst 1 THEN stac (OK_lift2_OK RS sym) 1 THEN rtac semilat_lub 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); - -qed "err_semilat_Product_esl"; diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Product.thy --- a/src/HOL/BCV/Product.thy Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ -(* Title: HOL/BCV/Product.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM - -Products as semilattices -*) - -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" - -end diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/README.html --- a/src/HOL/BCV/README.html Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,17 +0,0 @@ -HOL/BCV/README - - -

Verified Bytecode Verifiers

- -This theory defines an abstract and generic model of bytecode -verification, i.e. data-flow analysis for assembly languages with subtypes, -and applies it to an equally abstract model of the JVM. - -

- -A paper describing the theory is found here: - -Verified Bytecode Verifiers. - - - diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/ROOT.ML --- a/src/HOL/BCV/ROOT.ML Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,12 +0,0 @@ -(* Title: HOL/BCV/ROOT.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM - -A simple model of dataflow (sub)type analysis of instruction sequences, -aka `bytecode verification'. -*) - -writeln"Root file for HOL/BCV"; - -use_thy"JVM"; diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Semilat.ML --- a/src/HOL/BCV/Semilat.ML Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,177 +0,0 @@ -(* Title: HOL/BCV/Semilat.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM -*) - -Goalw [order_def] "order r ==> x <=_r x"; -by (Asm_simp_tac 1); -qed "order_refl"; -Addsimps [order_refl]; -AddIs [order_refl]; - -Goalw [order_def] "[| order r; x <=_r y; y <=_r x |] ==> x = y"; -by (Asm_simp_tac 1); -qed "order_antisym"; - -Goalw [order_def] "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z"; -by (Blast_tac 1); -qed "order_trans"; - -Goalw [order_def,lesssub_def] "order r ==> ~ x <_r x"; -by (Blast_tac 1); -qed "order_less_irrefl"; -AddIs [order_less_irrefl]; -Addsimps [order_less_irrefl]; - -Goalw [order_def,lesssub_def] "[| order r; x <_r y; y <_r z |] ==> x <_r z"; -by (Blast_tac 1); -qed "order_less_trans"; - -Goalw [top_def] "top r T ==> x <=_r T"; -by (Asm_simp_tac 1); -qed "topD"; -Addsimps [topD]; -AddIs [topD]; - -Goal "[| order r; top r T |] ==> (T <=_r x) = (x = T)"; -by (blast_tac (claset() addIs [order_antisym]) 1); -qed "top_le_conv"; -Addsimps [top_le_conv]; - -Goalw [semilat_def, split_conv RS eq_reflection] -"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)"; -by (rtac (refl RS eq_reflection) 1); -qed "semilat_Def"; - -Goalw [semilat_Def] "semilat(A,r,f) ==> order r"; -by (Asm_simp_tac 1); -qed "semilatDorderI"; -Addsimps [semilatDorderI]; -AddIs [semilatDorderI]; - -Goalw [semilat_Def] "semilat(A,r,f) ==> closed A f"; -by (Asm_simp_tac 1); -qed "semilatDclosedI"; -Addsimps [semilatDclosedI]; -AddIs [semilatDclosedI]; - -Goalw [semilat_Def] "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y"; -by (Asm_simp_tac 1); -qed "semilat_ub1"; - -Goalw [semilat_Def] "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y"; -by (Asm_simp_tac 1); -qed "semilat_ub2"; - -Goalw [semilat_Def] - "[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z"; -by (Asm_simp_tac 1); -qed "semilat_lub"; - -Addsimps [semilat_ub1,semilat_ub2,semilat_lub]; - -Goalw [semilat_Def] - "[| x:A; y:A; z:A; semilat(A,r,f) |] ==> \ -\ (x +_f y <=_r z) = (x <=_r z & y <=_r z)"; -by (blast_tac (claset() addIs [semilat_ub1,semilat_ub2,semilat_lub,order_trans]) 1); -qed "plus_le_conv"; -Addsimps [plus_le_conv]; - -Goal "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (x +_f y = y)"; -by (rtac iffI 1); - by (REPEAT(ares_tac [semilatDorderI,order_antisym,semilat_lub,order_refl,semilat_ub2] 1)); -by (etac subst 1); -by (Asm_simp_tac 1); -qed "le_iff_plus_unchanged"; - -Goal "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (y +_f x = y)"; -by (rtac iffI 1); - by (REPEAT(ares_tac [semilatDorderI,order_antisym,semilat_lub,order_refl,semilat_ub1] 1)); -by (etac subst 1); -by (Asm_simp_tac 1); -qed "le_iff_plus_unchanged2"; - -(*** closed ***) - -Goalw [closed_def] "[| closed A f; x:A; y:A |] ==> x +_f y : A"; -by (Blast_tac 1); -qed "closedD"; - -Goalw [closed_def] "closed UNIV f"; -by (Simp_tac 1); -qed "closed_UNIV"; -AddIffs [closed_UNIV]; - -(*** lub ***) - -Goalw [is_lub_def] - "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"; -by (assume_tac 1); -qed "is_lubD"; - -Goalw [is_ub_def] - "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u"; -by (Asm_simp_tac 1); -qed "is_ubI"; - -Goalw [is_ub_def] - "is_ub r x y u ==> (x,u) : r & (y,u) : r"; -by (assume_tac 1); -qed "is_ubD"; - - -Goalw [is_lub_def,is_ub_def] "is_lub (r^*) x y y = ((x,y):r^*)"; -by (Blast_tac 1); -qed "is_lub_bigger1"; -AddIffs [is_lub_bigger1]; - -Goalw [is_lub_def,is_ub_def] "is_lub (r^*) x y x = ((y,x):r^*)"; -by (Blast_tac 1); -qed "is_lub_bigger2"; -AddIffs [is_lub_bigger2]; - - -Goalw [is_lub_def,is_ub_def] - "[| single_valued r; is_lub (r^*) x y u; (x',x) : r |] ==> \ -\ EX v. is_lub (r^*) x' y v"; -by (case_tac "(y,x) : r^*" 1); - by (case_tac "(y,x') : r^*" 1); - by (Blast_tac 1); - by (blast_tac (claset() addIs [r_into_rtrancl] addEs [converse_rtranclE] - addDs [single_valuedD]) 1); -by (rtac exI 1); -by (rtac conjI 1); - by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [single_valuedD]) 1); -by (blast_tac (claset() addIs [rtrancl_into_rtrancl,rtrancl_into_rtrancl2] - addEs [converse_rtranclE] addDs [single_valuedD]) 1); -qed "extend_lub"; - -Goal "[| single_valued r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> \ -\ (EX z. is_lub (r^*) x y z))"; -by (etac converse_rtrancl_induct 1); - by (Clarify_tac 1); - by (etac converse_rtrancl_induct 1); - by (Blast_tac 1); - by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); -by (blast_tac (claset() addIs [extend_lub]) 1); -qed_spec_mp "single_valued_has_lubs"; - -Goalw [some_lub_def,is_lub_def] - "[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u"; -by (rtac someI2 1); - by (assume_tac 1); -by (blast_tac (claset() addIs [antisymD] - addSDs [acyclic_impl_antisym_rtrancl]) 1); -qed "some_lub_conv"; - -Goal - "[| single_valued r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> \ -\ is_lub (r^*) x y (some_lub (r^*) x y)"; -by (fast_tac - (claset() addDs [single_valued_has_lubs] - addss (simpset() addsimps [some_lub_conv])) 1); -qed "is_lub_some_lub"; diff -r 29f8b00d7e1f -r 45f837f8889d src/HOL/BCV/Semilat.thy --- a/src/HOL/BCV/Semilat.thy Fri Jun 01 11:04:19 2001 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,61 +0,0 @@ -(* Title: HOL/BCV/Semilat.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 2000 TUM - -Semilattices -*) - -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" - -end