--- 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<n. ss!p ~= T; p < n |] ==> \
-\ 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";
-*)
--- 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<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 => ('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<n. (bcv ss)!p ~= T) =
- (? ts: list n A. ss <=[r] ts & welltyping T wti ts)"
-
- wti_is_stable_topless ::
- 's ord => '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<n. ss!p ~= T) & p < n -->
- wti ss p = stable r step succs ss p"
-
- welltyping :: 's => ('s list => nat => bool) => 's list => bool
-"welltyping T wti ts == !p<size(ts). ts!p ~= T & wti ts p"
-
-end
--- a/src/HOL/BCV/Err.ML Fri Jun 01 11:04:19 2001 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,289 +0,0 @@
-(* Title: HOL/BCV/Err.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 2000 TUM
-*)
-
-Goalw [lesub_def] "e1 <=_(le r) e2 == le r e1 e2";
-by (Simp_tac 1);
-qed "unfold_lesub_err";
-
-Goalw [lesub_def,Err.le_def] "!x. x <=_r x ==> 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";
--- 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
--- 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];
--- 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
--- 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";
--- 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
--- 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<n |] ==> 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<n) \
-\ --> 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<size xs) --> 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<size xs) --> \
-\ (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<size ts |] ==> \
-\ 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<size ts; \
-\ ss <=[r] ts |] \
-\ ==> 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<n) --> \
-\ (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<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})))";
-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<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)";
-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";
--- 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<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])"
-
-end
--- 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<size xs; xs <=[r] ys; x <=_r y |] ==> 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<n --> \
-\ (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<size xs --> 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";
--- 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
--- 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";
-
--- 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
--- 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";
--- 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
--- 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 @@
-<HTML><HEAD><TITLE>HOL/BCV/README</TITLE></HEAD>
-<BODY>
-
-<H1>Verified Bytecode Verifiers</H1>
-
-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.
-
-<P>
-
-A paper describing the theory is found here:
-<A HREF = "http://www.in.tum.de/~nipkow/pubs/bcv2.html">
-Verified Bytecode Verifiers</A>.
-
-</BODY>
-</HTML>
--- 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";
--- 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";
--- 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