# HG changeset patch # User nipkow # Date 967825792 -7200 # Node ID a39e5d43de559dc459335e89c0f83bb3fd180124 # Parent 978c635c77f6fa28d199b556a710eb6596237f3a Completely new version of BCV diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/DFA_Framework.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/DFA_Framework.ML Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,96 @@ +(* 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); +br iffI 1; + br bexI 1; + br conjI 1; + ba 1; + by (asm_full_simp_tac + (simpset() addsimps[wti_is_stable_toplessD,stables_def]) 1); + ba 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); + ba 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/DFA_Framework.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/DFA_Framework.thy Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,51 @@ +(* 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 \ -\ wti p sos = stable step succs p sos"; -by (Asm_simp_tac 1); -qed "wti_is_fix_stepD"; - -Goalw [is_dfa_def] - "[| is_dfa dfa step succs n L; sos : listsn n (option L) |] ==> \ -\ dfa sos = (? tos : listsn (size sos) (option L). \ -\ sos <= tos & (!p < size tos. stable step succs p tos))"; -by (Asm_simp_tac 1); -qed "is_dfaD"; - -Goalw [welltyping_def] - "[| wti_is_fix_step step wti succs n L; is_dfa dfa step succs n L; \ -\ sos : listsn n (option L) |] ==> \ -\ dfa sos = (? tos : listsn n (option L). sos <= tos & welltyping wti tos)"; -by (dtac is_dfaD 1); -by (assume_tac 1); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addDs [wti_is_fix_stepD]) 1); -qed "dfa_iff_welltyping"; - -Goal - "x:M ==> replicate n x : listsn n M"; -by (induct_tac "n" 1); -by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [in_listsn_Suc_iff,Bex_def]) 1); -qed "replicate_in_listsn"; -Addsimps [replicate_in_listsn]; - -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_fix_step step wti succs n L; is_dfa dfa step succs n L; \ -\ 0 < n; init : (option L) |] ==> \ -\ dfa (init # replicate (n-1) None) = \ -\ (? tos : listsn n (option L). 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_listsn_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_listsn_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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/DFAandWTI.thy --- a/src/HOL/BCV/DFAandWTI.thy Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,41 +0,0 @@ -(* Title: HOL/BCV/DFAandWTI.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM - -The relationship between dataflow analysis and a welltyped-insruction predicate. -*) - -DFAandWTI = SemiLattice + - -types 's os = 's option list - -constdefs - - stable :: (nat => 's::ord => 's option) => (nat => nat list) => nat => 's os => bool -"stable step succs p sos == - !s. sos!p = Some s --> (? t. step p s = Some(t) & - (!q:set(succs p). Some t <= sos!q))" - - wti_is_fix_step :: - "(nat => 's::ord => 's option) - => (nat => 's os => bool) - => (nat => nat list) - => nat => 's set => bool" -"wti_is_fix_step step wti succs n L == !sos p. - sos : listsn n (option L) & p < n --> - wti p sos = stable step succs p sos" - - welltyping :: (nat => 's os => bool) => 's os => bool -"welltyping wti tos == !p bool) - => (nat => 's::ord => 's option) - => (nat => nat list) - => nat => 's set => bool -"is_dfa dfa step succs n L == !sos : listsn n (option L). - dfa sos = - (? tos : listsn n (option L). - sos <= tos & (!p < n. stable step succs p tos))" - -end diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/DFAimpl.ML --- a/src/HOL/BCV/DFAimpl.ML Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,336 +0,0 @@ -(* Title: HOL/BCV/DFAimpl.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM -*) - -(** merges **) - -Goal "!sos. size(merges t ps sos) = size sos"; -by (induct_tac "ps" 1); -by (Auto_tac); -qed_spec_mp "length_merges"; -Addsimps [length_merges]; - -Goal - "!xs. xs : listsn n (option A) --> x : A --> (!p : set ps. p \ -\ semilat A --> merges x ps xs : listsn n (option A)"; -by (induct_tac "ps" 1); -by (Auto_tac); -qed_spec_mp "merges_preserves_type"; -Addsimps [merges_preserves_type]; -(*AddSIs [merges_preserves_type];*) - -Goal "semilat A ==> !xs. xs : listsn n (option A) --> x:A --> (!p:set ps. p xs <= merges x ps xs"; -by (induct_tac "ps" 1); - by (Simp_tac 1); -by (Simp_tac 1); -by (Clarify_tac 1); -by (rtac order_trans 1); - by (etac list_update_incr 1); - by (Blast_tac 2); - by (assume_tac 2); - by (etac (Some_in_option RS iffD2) 1); -by (blast_tac (claset() addSIs [listsnE_set] - addIs [semilat_plus,listsnE_length RS nth_in]) 1); -qed_spec_mp "merges_incr"; - -(* is redundant but useful *) -Goal "[| xs!i = Some x; xs : listsn n (option A); i < n |] ==> x:A"; -by (dtac listsnE_nth_in 1); -by (assume_tac 1); -by (Asm_full_simp_tac 1); -qed "listsn_optionE_in"; -(*Addsimps [listsn_optionE_in];*) - -Goal - "[| semilat L |] ==> \ -\ (!xs. xs : listsn n (option L) --> x:L --> (!p:set ps. p \ -\ (merges x ps xs = xs) = (!p:set ps. Some x <= 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 := Some x + xs!p] <= xs" 1); - by (EVERY[etac subst 2, rtac merges_incr 2]); - by (assume_tac 2); - by (Force_tac 2); - by (assume_tac 2); - by (assume_tac 2); - by (case_tac "xs!p" 1); - by (asm_full_simp_tac (simpset() addsimps [list_update_le_conv]) 1); - by (asm_full_simp_tac (simpset() addsimps - [list_update_le_conv,listsn_optionE_in]) 1); - by (Clarify_tac 1); - by (rotate_tac ~3 1); - by (asm_full_simp_tac (simpset() addsimps - [le_iff_plus_unchanged RS iffD1,listsn_optionE_in, - list_update_same_conv RS iffD2]) 1); -by (Clarify_tac 1); -by (asm_simp_tac (simpset() addsimps - [le_iff_plus_unchanged RS iffD1,listsn_optionE_in, - list_update_same_conv RS iffD2]) 1); -qed_spec_mp "merges_same_conv"; - - -Goalw [le_list,plus_option] - "xs <= ys --> xs : listsn n (option L) --> ys : listsn n (option L) --> \ -\ p < n --> ys!p = Some y --> x <= y --> x : L --> semilat L --> \ -\ xs[p := Some x + xs!p] <= ys"; -by (simp_tac (simpset() addsimps [nth_list_update] - addsplits [option.split]) 1); -by (Clarify_tac 1); -by (rotate_tac 3 1); -by (force_tac (claset() addEs [listsn_optionE_in] addIs [semilat_lub], - simpset()) 1); -qed_spec_mp "list_update_le_listI"; - -Goal - "[| semilat(L); t:L; tos : listsn n (option L); \ -\ !p. p:set ps --> Some t <= tos!p; \ -\ !p. p:set ps --> p \ -\ set qs <= set ps --> \ -\ (!sos. sos : listsn n (option L) & sos <= tos --> merges t qs sos <= tos)"; -by (induct_tac "qs" 1); - by (Asm_simp_tac 1); -by (force_tac (claset(),simpset() addsimps [list_update_le_listI]) 1); -val lemma = result(); - -Goal - "[| semilat(L); t:L; \ -\ !p. p:set ps --> Some t <= tos!p; \ -\ !p. p:set ps --> p merges t ps sos <= tos"; -by (blast_tac (claset() addDs [lemma]) 1); -qed "merges_pres_le_ub"; - - -(** next **) - -Goalw [is_next_def] - "[| is_next next; next step succs sos = None; succs_bounded succs n; \ -\ sos : listsn n S |] ==> \ -\ ? p \ -\ next step succs sos = Some sos --> \ -\ (!p (? t. \ -\ step p s = Some(t) & merges t (succs p) sos = sos))"; -by (subgoal_tac "n=size sos" 1); -by (Blast_tac 1); -by (Asm_simp_tac 1); -qed "next_Some1"; - -Goalw [is_next_def] - "[| is_next next; next step succs sos = Some sos'; sos' ~= sos; \ -\ succs_bounded succs n; sos : listsn n S |] ==> \ -\ ? p \ -\ (next step succs sos = Some sos) = \ -\ (!p (? t. \ -\ step p s = Some(t) & merges t (succs p) sos = sos))"; -by (rtac iffI 1); - by (asm_simp_tac (simpset() addsimps [next_Some1]) 1); -by (case_tac "next step succs sos" 1); - by (best_tac (claset() addSDs [next_None] addss simpset()) 1); -by (rename_tac "sos'" 1); -by (case_tac "sos' = sos" 1); - by (Blast_tac 1); -by (best_tac (claset() addSDs [next_Some2] addss simpset()) 1); -qed "next_Some1_eq"; - -Addsimps [next_Some1_eq]; - -Goalw [step_pres_type_def] - "[| step_pres_type step n L; s:L; p t:L"; -by (Blast_tac 1); -qed "step_pres_typeD"; - -Goalw [succs_bounded_def] - "[| succs_bounded succs n; p < n; q : set(succs p) |] ==> q < n"; -by (Blast_tac 1); -qed "succs_boundedD"; - -Goal - "[| is_next next; semilat A; \ -\ step_pres_type step n A; succs_bounded succs n;\ -\ sos : listsn n (option A) |] ==> \ -\ next step succs sos : option (listsn n (option A))"; -by (case_tac "next step succs sos" 1); - by (ALLGOALS Asm_simp_tac); -by (rename_tac "sos'" 1); -by (case_tac "sos' = sos" 1); - by (Asm_simp_tac 1); -by (blast_tac (claset() addIs [step_pres_typeD,succs_boundedD,listsn_optionE_in] addSIs [merges_preserves_type] addDs [next_Some2]) 1); -qed_spec_mp "next_preserves_type"; - -Goal - "[| is_next next; semilat A; \ -\ step_pres_type step n A; succs_bounded succs n; \ -\ next step succs xs = Some ys; xs : listsn n (option A) |] ==> xs <= ys"; -by (case_tac "ys = xs" 1); - by (Asm_full_simp_tac 1); -by (blast_tac (claset() addSIs [merges_incr] addIs [listsn_optionE_in] - addDs [step_pres_typeD,succs_boundedD,next_Some2]) 1); -qed_spec_mp "next_incr"; - -val lemma = (Unify.trace_bound, Unify.search_bound); -Unify.trace_bound := 50; -Unify.search_bound := 50; - -Goalw [is_next_def] - "is_next (%step succs sos. itnext (size sos) step succs sos)"; -by (Clarify_tac 1); -by (etac thin_rl 1); -by (res_inst_tac [("n","length sos")] nat_induct 1); - by (Asm_full_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq,Let_def] - addsplits [option.split])1); -by (Blast_tac 1); -qed "is_next_itnext"; - -Unify.trace_bound := !(fst lemma); -Unify.search_bound := !(snd lemma); - -(** fix step **) - -Goalw [step_mono_None_def] - "[| step_mono_None step n L; s : L; p < n; s <= t; step p s = None |] ==> \ -\ step p t = None"; -by (Blast_tac 1); -qed "step_mono_NoneD"; - -Goalw [step_mono_def] - "[| step_mono step n L; s : L; p < n; s <= t; step p s = Some(u) |] ==> \ -\ !v. step p t = Some(v) --> u <= v"; -by (Blast_tac 1); -qed "step_monoD"; - -Goalw [stable_def] -"[| is_next next; semilat L; sos : listsn n (option L); \ -\ step_pres_type step n L; succs_bounded succs n |] \ -\ ==> (next step succs sos = Some sos) = (!p ? sos'. next step succs sos = Some sos' & sos' <= tos"; -by (subgoal_tac - "!p (? u. \ -\ step p s = Some(u) & (!q:set(succs p). Some u<=tos!q))" 1); - by (case_tac "next step succs sos" 1); - by (dtac next_None 1); - by (assume_tac 1); - by (assume_tac 1); - by (assume_tac 1); - by (Force_tac 1); - by (rename_tac "sos'" 1); - by (case_tac "sos' = sos" 1); - by (Blast_tac 1); - by (dtac next_Some2 1); - by (EVERY1[atac, atac, atac, atac]); - by (Clarify_tac 1); - by (etac allE 1 THEN mp_tac 1); - by (etac allE 1 THEN mp_tac 1); - by (Clarify_tac 1); - by (EVERY1[rtac exI, rtac conjI, atac]); - by (rtac merges_pres_le_ub 1); - by (assume_tac 1); - by (blast_tac (claset() addIs [step_pres_typeD,listsn_optionE_in]) 1); - by (Asm_full_simp_tac 1); - by (blast_tac (claset() addIs [succs_boundedD,listsn_optionE_in]) 1); - by (REPEAT(atac 1)); -by (Clarify_tac 1); -by (case_tac "tos!p" 1); - by (force_tac (claset() addDs [le_listD],simpset()) 1); -by (rename_tac "t" 1); -by (subgoal_tac "s <= t" 1); - by (force_tac (claset() addDs [le_listD],simpset()) 2); -by (case_tac "step p s" 1); - by (dtac step_mono_NoneD 1); - by (assume_tac 4); - by (blast_tac (claset() addIs [listsn_optionE_in]) 1); - by (assume_tac 1); - by (assume_tac 1); - by (Force_tac 1); -by (dtac step_monoD 1); - by (assume_tac 4); - by (blast_tac (claset() addIs [listsn_optionE_in]) 1); - by (assume_tac 1); - by (assume_tac 1); -by (Asm_full_simp_tac 1); -by (etac allE 1 THEN mp_tac 1); -by (etac allE 1 THEN mp_tac 1); -by (Clarify_tac 1); -by (Asm_full_simp_tac 1); -by (forward_tac[merges_same_conv RS iffD1]1); - by (assume_tac 4); - by (assume_tac 1); - by (blast_tac (claset() addIs [step_pres_typeD,listsn_optionE_in]) 1); - by (blast_tac (claset() addIs [succs_boundedD,listsn_optionE_in]) 1); -by (blast_tac (claset() addIs [order_trans]) 1); -val lemma = result(); - -Goalw [is_dfa_def] - "[| semilat L; acc L; is_next next; \ -\ step_pres_type step n L; succs_bounded succs n; \ -\ step_mono_None step n L; step_mono step n L |] ==> \ -\ is_dfa (%sos. fix(next step succs, sos)) step succs n L"; -by (Clarify_tac 1); -by (stac fix_iff_has_fixpoint 1); - by (etac (acc_option RS acc_listsn) 1); - by (blast_tac (claset() addIs [lemma]) 1); - by (blast_tac (claset() addIs [next_preserves_type]) 1); - by (blast_tac (claset() addIs [next_incr]) 1); - by (assume_tac 1); -by (asm_simp_tac (simpset() delsimps [next_Some1_eq] addsimps [fixpoint_next_iff_stable]) 1); -qed "is_dfa_fix_next"; - -Goal - "[| semilat L; acc L; is_next next; \ -\ step_pres_type step n L; succs_bounded succs n; \ -\ step_mono_None step n L; step_mono step n L; \ -\ wti_is_fix_step step wti succs n L; \ -\ sos : listsn n (option L) |] ==> \ -\ fix(next step succs, sos) = \ -\ (? tos:listsn n (option L). sos<=tos & welltyping wti tos)"; -by (blast_tac (claset() addSDs [dfa_iff_welltyping] addSIs [is_dfa_fix_next]) 1); -qed "fix_next_iff_welltyping"; diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/DFAimpl.thy --- a/src/HOL/BCV/DFAimpl.thy Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,60 +0,0 @@ -(* Title: HOL/BCV/DFAimpl.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM - -Implementations of data-flow analysis. -*) - -DFAimpl = DFAandWTI + Fixpoint + - -consts merges :: "('s::plus) => nat list => 's os => 's os" -primrec -"merges a [] s = s" -"merges a (p#ps) s = merges a ps (s[p := Some(a) + s!p])" - -constdefs - succs_bounded :: "(nat => nat list) => nat => bool" -"succs_bounded succs n == !p 's => ('s::plus)option) => (nat => nat list) - => 's os => 's os option) - => bool" -"is_next next == !step succs sos sos'. - succs_bounded succs (size sos) --> - (next step succs sos = None --> - (? p - (!p (? t. - step p s = Some(t) & merges t (succs p) sos = sos))) & - (next step succs sos = Some sos' & sos' ~= sos --> - (? p 's => 's option) => nat => 's set => bool" -"step_pres_type step n L == !s:L. !p t:L" - - step_mono_None :: "(nat => 's::ord => 's option) => nat => 's set => bool" -"step_mono_None step n L == !s p t. - s : L & p < n & s <= t & step p s = None --> step p t = None" - - step_mono :: "(nat => 's::ord => 's option) => nat => 's set => bool" -"step_mono step n L == !s p t u. - s : L & p < n & s <= t & step p s = Some(u) - --> (!v. step p t = Some(v) --> u <= v)" - -consts -itnext :: nat => (nat => 's => 's option) => (nat => nat list) - => 's os => ('s::plus) os option -primrec -"itnext 0 step succs sos = Some sos" -"itnext (Suc p) step succs sos = - (case sos!p of - None => itnext p step succs sos - | Some s => (case step p s of None => None - | Some t => let sos' = merges t (succs p) sos - in if sos' = sos - then itnext p step succs sos - else Some sos'))" - -end diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Err.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Err.ML Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,290 @@ +(* 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"; +br 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); +by (Blast_tac 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)"; +br 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"; +br (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"; +br (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))"; +br iffI 1; + by (Clarify_tac 1); + bd (OK_le_err_OK RS iffD2) 1; + bd (OK_le_err_OK RS iffD2) 1; + bd semilat_lub 1; + ba 1; + ba 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); + ba 1; +by(rename_tac "z" 1); +by(subgoal_tac "OK z: err A" 1); +bd 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); +br conjI 1; + by(Blast_tac 1); +by(asm_full_simp_tac (simpset() addsimps [err_def]) 1); +br 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); +br 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Err.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Err.thy Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,47 @@ +(* 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Fixpoint.ML --- a/src/HOL/BCV/Fixpoint.ML Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,142 +0,0 @@ -(* Title: HOL/BCV/Fixpoint.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM -*) - -goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop (hd fix.tcs))); -by (asm_full_simp_tac (simpset() addsimps [wf_iff_no_infinite_down_chain] - addsplits [split_split]) 1); -by (Clarify_tac 1); -by (rtac ccontr 1); -by (Asm_full_simp_tac 1); -by (res_inst_tac[("x","0")] allE 1); -by (assume_tac 1); -by (Clarify_tac 1); -by (rename_tac "next s0" 1); -by (subgoal_tac "!i. fst(f i) = next" 1); -by (eres_inst_tac[("x","%i. snd(f i)")] allE 1); -by (Asm_full_simp_tac 1); -by (Clarify_tac 1); -by (eres_inst_tac[("x","i")] allE 1); -by (eres_inst_tac[("x","i")] allE 1); -by (Force_tac 1); -by (rtac allI 1); -by (induct_tac "i" 1); -by (Asm_simp_tac 1); -by (eres_inst_tac[("x","n")] allE 1); -by (Auto_tac); -val fix_tc = result(); - -Goalw [wf_iff_no_infinite_down_chain RS eq_reflection] - "[| wf{(t,s). s:A & next s = Some t & t ~= s}; \ -\ !a:A. next a : option A; s:A |] ==> \ -\ fix(next,s) = (case next s of None => False \ -\ | Some t => if t=s then True else fix(next,t))"; -by (stac (fix_tc RS (hd fix.simps)) 1); -by (Simp_tac 1); -by (Clarify_tac 1); -by (subgoal_tac "!i. f i : A" 1); - by (Blast_tac 1); -by (rtac allI 1); -by (induct_tac "i" 1); - by (Asm_simp_tac 1); -by (Auto_tac); -qed "fix_unfold"; - -(* Thm: next has fixpoint above s iff fix(next,s) *) - -Goal "[| x = Some y; x : option A |] ==> y : A"; -by (Blast_tac 1); -val lemma = result(); - -Goal -"[| acc L; \ -\ !t:L. !s:L. next t = Some t & s <= t --> (? u. next s = Some u & u <= t); \ -\ !a:L. next a : option L; !a:L. !b. next a = Some b --> a <= b |] \ -\ ==> s:L --> fix(next,s) = (? t:L. s <= t & next t = Some t)"; -by (subgoal_tac "wf{(y,x::'a::order). x : L & next x = Some y & y ~= x}" 1); - by (full_simp_tac (simpset() addsimps [acc_def]) 2); - by (etac wf_subset 2); - by (simp_tac (simpset() addsimps [order_less_le]) 2); - by (blast_tac (claset() addDs [lemma]) 2); -by (res_inst_tac [("a","s")] wf_induct 1); - by (assume_tac 1); -by (Clarify_tac 1); -by (Full_simp_tac 1); -by (stac fix_unfold 1); - by (assume_tac 1); - by (assume_tac 1); - by (assume_tac 1); -by (split_tac [option.split] 1); -by (rtac conjI 1); - by (thin_tac "!a:L. !b. next a = Some b --> a <= b" 1); - by (Force_tac 1); -by (Clarify_tac 1); -by (split_tac [split_if] 1); -by (rtac conjI 1); - by (Blast_tac 1); -by (Clarify_tac 1); -by (EVERY[etac allE 1, etac impE 1, etac impE 2, etac trans 3]); - by (Blast_tac 1); - by (etac lemma 1); - by (Blast_tac 1); -by (rtac iffI 1); - by (blast_tac (claset() addIs [order_trans]) 1); -by (Clarify_tac 1); -by (EVERY[rtac bexI 1, atac 2, rtac conjI 1, atac 2]); -by (thin_tac "!a:L. !b. next a = Some b --> a <= b" 1); -by (Force_tac 1); -qed_spec_mp "fix_iff_has_fixpoint"; - - -(* This lemma looks more pleasing to the eye, because of the monotonicity -assumption for next, instead of the strange assumption above. -However, function next as defined in DFAimpl is NOT monotone because -None is not required to be detected as early as possible. Thus the following -does not hold: sos <= tos & next sos = None ==> next tos = None - -Goal -"[| wf{(y,x::'a::order). x : L & next x = Some y & y ~= x}; \ -\ !t:L. !s:L. s <= t & next s = None --> next t = None; \ -\ !t:L. !s:L. !u. s <= t & next s = Some u --> \ -\ next t = None | (? v. next t = Some v & u <= v); \ -\ !a:L. next a : option L; !a:L. !b. next a = Some b --> a <= b |] \ -\ ==> s:L --> fix(next,s) = (? t:L. s <= t & next t = Some t)"; -by (res_inst_tac [("a","s")] wf_induct 1); - by (assume_tac 1); -by (Clarify_tac 1); -by (Full_simp_tac 1); -by (stac fix_unfold 1); - by (assume_tac 1); - by (assume_tac 1); - by (assume_tac 1); -by (split_tac [option.split] 1); -by (rtac conjI 1); - by (blast_tac (claset() addDs [sym RS trans]) 1); -by (Clarify_tac 1); -by (split_tac [split_if] 1); -by (rtac conjI 1); - by (Blast_tac 1); -by (Clarify_tac 1); -by (EVERY[etac allE 1, etac impE 1, etac impE 2, etac trans 3]); - by (Blast_tac 1); - by (etac lemma 1); - by (Blast_tac 1); -by (rtac iffI 1); - by (subgoal_tac "next a ~= None" 1); - by (Clarify_tac 1); - by (EVERY[etac ballE 1, etac ballE 1, etac allE 1, etac impE 1,etac disjE 2]); - by (rtac conjI 1); - by (assume_tac 1); - by (assume_tac 1); - by (blast_tac (claset() addDs [sym RS trans]) 1); - by (blast_tac (claset() addIs [order_trans]) 1); - by (blast_tac (claset() addIs [order_trans]) 1); - by (Blast_tac 1); - by (rtac notI 1); - by (Clarify_tac 1); - by (blast_tac (claset() addDs [sym RS trans,lemma]) 1); -by (blast_tac (claset() addDs [sym RS trans]) 1); -qed_spec_mp "fix_iff_has_fixpoint"; -*) diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Fixpoint.thy --- a/src/HOL/BCV/Fixpoint.thy Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* Title: HOL/BCV/Fixpoint.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM - -Searching for a fixpoint. -*) - -Fixpoint = SemiLattice + - -consts fix :: "('a => 'a option) * 'a => bool" -recdef fix - "{((nxt,t),(nxs,s)) . nxt=nxs & - ~(? f. f 0 = s & (!i. nxt (f i) = Some(f(i+1)) & f(i+1) ~= f i)) & - nxs s = Some t & t ~= s}" -"fix(next,s) = - (if (? f. f 0 = s & (!i. next (f i) = Some(f(i+1)) & f(i+1) ~= f i)) - then arbitrary - else case next s of None => False | - Some t => if t=s then True else fix(next,t))" - - -end diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/JType.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/JType.ML Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,166 @@ +(* 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)"; +bd 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); +bd 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); + ba 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); +be rtranclE 1; + by(Blast_tac 1); +bd (converseI RS 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] + "[| univalent 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 RS eq_reflection,JType.esl_def,Err.sl_def] + "[| univalent S; acyclic S |] ==> err_semilat (JType.esl S)"; +by(asm_full_simp_tac (simpset() addsimps [acyclic_impl_order_subtype,closed_err_types]) 1); + +br 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); + +br 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); +br conjI 1; + by(Blast_tac 1); +br conjI 1; + by(Blast_tac 1); +br conjI 1; + by(Blast_tac 1); +by(Clarify_tac 1); +br conjI 1; + by(Clarify_tac 1); +br 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/JType.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/JType.thy Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,68 @@ +(* 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/JVM.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/JVM.ML Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,261 @@ +(* 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); + +br conjI 1; +by(fast_tac (claset() addDs [refl RS nth_in] addSEs [wf_LoadD] addss + (simpset() delsimps [is_type_def]addsplits [err.split])) 1); + +br conjI 1; +by (fast_tac (claset() addDs [set_update_subset_insert RS subsetD] + addSEs [wf_StoreD] addss (simpset() addsplits [list.split])) 1); + +br conjI 1; +by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1); + +br conjI 1; +by (fast_tac (claset() addIs [wf_GetfieldD] + addss (simpset() addsplits [list.split,ty.split])) 1); + +br conjI 1; +by (fast_tac (claset() addss (simpset() addsplits [list.split])) 1); + +br conjI 1; +by (fast_tac (claset() addIs [wf_NewD] addss simpset()) 1); + +br 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); +br 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); + +br conjI 1; +by(Clarify_tac 1); +by(asm_full_simp_tac (simpset() addsplits [option.split,list.split,err.split]) 1); + +br conjI 1; +by(Clarify_tac 1); +by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); + +br conjI 1; +by(Clarify_tac 1); +by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); + +br conjI 1; +by(Clarify_tac 1); +by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); + +br conjI 1; +by(Clarify_tac 1); +by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); +by(Blast_tac 1); + +br conjI 1; +by(Clarify_tac 1); +by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); + +br conjI 1; +by(Clarify_tac 1); +by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); + +br conjI 1; +by(Clarify_tac 1); +by(asm_full_simp_tac (simpset() addsplits [option.split,list.split]) 1); + +br conjI 1; +by(Clarify_tac 1); +by(asm_full_simp_tac (simpset() addsplits [option.split,list.split,ty.split]) 1); + +br 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); +br 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); + +br conjI 1; +by (fast_tac (claset() addDs [le_listD] addSEs [wf_LoadD] + addss (simpset() addsplits [err.split])) 1); + +br conjI 1; +by (fast_tac (claset() addIs [list_update_le_cong,le_listD] addSEs [wf_StoreD] + addss (simpset() addsplits [list.split])) 1); + +br conjI 1; +by(Asm_simp_tac 1); + +br conjI 1; +by(Asm_simp_tac 1); + +br conjI 1; +by(fast_tac (claset() addss (simpset() addsplits [list.split])) 1); + +br conjI 1; +by (fast_tac (claset() addDs [rtrancl_trans] + addss (simpset() addsplits [list.split])) 1); + +br conjI 1; + by (Clarify_tac 1); + by(asm_full_simp_tac (simpset() addsplits [list.split]) 1); + br conjI 1; + by (Clarify_tac 1); + by (Clarify_tac 1); + br conjI 1; + by (Clarify_tac 1); + by (Clarify_tac 1); + br 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); + +br conjI 1; +by(asm_full_simp_tac (simpset() addsimps [reflD] addsplits [list.split]) 1); + +br 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); + +br 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] + "[| univalent 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] + "[| univalent 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)"; +br 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); + be exec_pres_type 1; + ba 1; + ba 1; + be exec_mono 1; + ba 1; +be wti_is_stable_topless 1; +qed "is_bcv_kiljvm"; diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/JVM.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/JVM.thy Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,165 @@ +(* 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Kildall.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Kildall.ML Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,351 @@ +(* 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); + ba 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); + ba 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); +br 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_fstI 1)); +by(split_all_tac 1); +by(asm_full_simp_tac (simpset() addsimps [lesssub_def]) 1); +by(REPEAT(rtac wf_same_fstI 1)); +br wf_lex_prod 1; + br wf_finite_psubset 2; (* FIXME *) +by(Clarify_tac 1); +bd (semilatDorderI RS acc_le_listI) 1; + ba 1; +by(rewrite_goals_tac [acc_def,lesssub_def]); +ba 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); +br impI 1; +bd (sym RS (rotate_prems 4 (merges_same_conv RS iffD1))) 1; + ba 1; + ba 1; + ba 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 [selectI]) 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); +brs 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 [selectI]) 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); +br impI 1; +by(stac decomp_propa 1); + by(subgoal_tac "(@p. p:w) : w" 1); + by (fast_tac (claset() addIs [selectI]) 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); + ba 1; + ba 1; + ba 2; + by (blast_tac (claset() addDs [boundedD]) 1); + by (blast_tac (claset() addDs [boundedD]) 1); +by(stac nth_merges 1); + ba 1; + ba 1; + ba 2; + by (blast_tac (claset() addDs [boundedD]) 1); + by (blast_tac (claset() addDs [boundedD]) 1); +by (Simp_tac 1); +br 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); + ba 1; + ba 1; + by (Asm_simp_tac 1); + ba 1; + ba 1; + ba 1; +by(asm_simp_tac (simpset() delsimps [listE_length]) 1); +br impI 1; +be allE 1; +be impE 1; + by(asm_simp_tac (simpset() delsimps [listE_length]) 1); +by(subgoal_tac "(@p. p:w) : w" 1); + by (fast_tac (claset() addIs [selectI]) 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); +be impE 1; + by(asm_simp_tac (simpset() delsimps [listE_length,le_iff_plus_unchanged RS sym]) 1); + br conjI 1; + by (blast_tac (claset() addDs [boundedD]) 1); + br 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); +br 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); +br 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Kildall.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Kildall.thy Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,62 @@ +(* 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Listn.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Listn.ML Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,424 @@ +(* 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); +br 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); +by (Blast_tac 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); + be wf_subset 1; + by(blast_tac (claset() addIs [lesssub_list_impl_same_size]) 1); +br 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); + br 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); +be 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); + ba 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]) 1); +br conjI 1; + by(Asm_simp_tac 1); +br 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); +br 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]) 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); +br conjI 1; + bd 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Listn.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Listn.thy Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,50 @@ +(* 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Machine.ML --- a/src/HOL/BCV/Machine.ML Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,117 +0,0 @@ -(* Title: HOL/BCV/Machine.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM -*) - -Addsimps [Let_def]; - -Addsimps [stype_def]; - - -(*** Machine specific ***) - -Goal "!p. p maxreg(bs!p) < maxregs(bs)"; -by (induct_tac "bs" 1); -by (auto_tac (claset(), simpset() addsimps [nth_Cons,less_max_iff_disj] - addsplits [nat.split])); -qed_spec_mp "maxreg_less_maxregs"; - -Goalw [le_typ] "(t <= Ctyp) = (t = Ctyp)"; -by (Simp_tac 1); -qed "le_Ctyp_conv"; - -Goalw [le_typ] "(t ~= Top) = (t = Atyp | t = Btyp | t = Ctyp)"; -by (induct_tac "t" 1); -by (ALLGOALS Simp_tac); -qed "le_Top_conv"; - -Goalw [step_pres_type_def,listsn_def,exec_def,stype_def] - "step_pres_type (%p. exec (bs!p)) (length bs) (stype bs)"; -by (force_tac (claset(), simpset() addsplits [instr.split_asm,split_if_asm]) 1); -qed "exec_pres_type"; - -Goalw [wti_is_fix_step_def,stable_def,wt_instr_def,exec_def,succs_def] - "wti_is_fix_step (%p. exec (bs!p)) (%u. wt_instr (bs ! u) u) \ -\ (%p. succs (bs ! p) p) (length bs) (stype bs)"; -by (force_tac (claset() addDs [maxreg_less_maxregs, - le_Top_conv RS iffD1,le_Ctyp_conv RS iffD1], - simpset() addsplits [option.split,instr.split]) 1); -qed "wt_instr_is_fix_exec"; - - -Goalw [step_mono_None_def,exec_def,succs_def,le_list] - "step_mono_None (%p. exec (bs!p)) (length bs) (stype bs)"; -by (Clarify_tac 1); -by (ftac maxreg_less_maxregs 1); -by (split_asm_tac [instr.split_asm] 1); - -by (ALLGOALS (asm_full_simp_tac (simpset() addsplits [split_if_asm]))); - -by (rotate_tac 1 1); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addIs [order_trans]) 1); - -by (rotate_tac 1 1); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addIs [order_trans]) 1); - -by (rotate_tac 1 1); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addIs [order_trans]) 1); - -by (rotate_tac 1 1); -by (Asm_full_simp_tac 1); -by (subgoal_tac "s!nat1 <= t!nat1" 1); -by (Blast_tac 2); -by (subgoal_tac "s!nat2 <= t!nat2" 1); -by (Blast_tac 2); -by (etac thin_rl 1); -by (asm_full_simp_tac (simpset() addsimps [le_typ])1); -by (case_tac "t!nat1" 1); -by (ALLGOALS Asm_full_simp_tac); -by (case_tac "t!nat2" 1); -by (ALLGOALS Asm_full_simp_tac); -by (case_tac "t!nat2" 1); -by (ALLGOALS Asm_full_simp_tac); -by (case_tac "s!nat1" 1); -by (ALLGOALS Asm_full_simp_tac); -by (case_tac "t!nat2" 1); -by (ALLGOALS Asm_full_simp_tac); - -qed "exec_mono_None"; - -Goalw [step_mono_def,exec_def,succs_def] - "step_mono (%p. exec (bs!p)) (length bs) (stype bs)"; -by (Clarify_tac 1); -by (ftac maxreg_less_maxregs 1); -by (split_asm_tac [instr.split_asm] 1); -by (ALLGOALS - (fast_tac (claset() addIs [list_update_le_cong,le_listD] - addss (simpset() addsplits [split_if_asm])))); - -qed_spec_mp "exec_mono_Some"; - -Goalw [stype_def] "semilat(stype bs)"; -by (Blast_tac 1); -qed "lat_stype"; - -Goalw [stype_def] "acc(stype bs)"; -by (Simp_tac 1); -qed "acc_stype"; - -Delsimps [stype_def]; - -Goal - "[| is_next next; \ -\ succs_bounded (%p. succs (bs!p) p) (size bs); \ -\ sos : listsn (size bs) (option(stype bs)) |] ==> \ -\ fix(next (%p. exec (bs!p)) (%p. succs (bs!p) p), sos) = \ -\ (? tos : listsn (size bs) (option(stype bs)). \ -\ sos <= tos & welltyping (%p. wt_instr (bs!p) p) tos)"; -by (simp_tac (simpset() delsimps [not_None_eq]) 1); -by (REPEAT(ares_tac [fix_next_iff_welltyping,exec_pres_type, - exec_mono_None,exec_mono_Some, - wt_instr_is_fix_exec,lat_stype,acc_stype] 1)); - -qed "fix_iff_welltyped"; diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Machine.thy --- a/src/HOL/BCV/Machine.thy Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,96 +0,0 @@ -(* Title: HOL/BCV/Machine.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM - -A register machine. -*) - -Machine = Types + DFAimpl + - -datatype ('a,'b,'c)instr = - Move nat nat - | Aload 'a nat | Bload 'b nat | Cload 'c nat - | Aop nat nat nat | Bop nat nat nat | Cop nat nat nat - | Comp nat nat nat - | Halt - -consts maxreg :: ('a,'b,'c)instr => nat - maxregs :: ('a,'b,'c)instr list => nat -primrec -"maxreg(Move m n) = max m n" -"maxreg(Aload x n) = n" -"maxreg(Bload x n) = n" -"maxreg(Cload x n) = n" -"maxreg(Aop i j k) = max i (max j k)" -"maxreg(Bop i j k) = max i (max j k)" -"maxreg(Cop i j k) = max i (max j k)" -"maxreg(Comp i j l) = max i j" -"maxreg Halt = 0" - -primrec -"maxregs [] = 0" -"maxregs (x#xs) = max (maxreg x+1) (maxregs xs)" - -constdefs - - wt_instr :: ('a,'b,'c)instr => nat => typ list option list => bool -"wt_instr b p T == - case T!p of - None => True - | Some ts => - case b of - Move i j => Some(ts[j:=ts!i]) <= T!(p+1) - | Aload x i => Some(ts[i:=Atyp]) <= T!(p+1) - | Bload x i => Some(ts[i:=Btyp]) <= T!(p+1) - | Cload x i => Some(ts[i:=Ctyp]) <= T!(p+1) - | Aop i j k => ts!i <= Atyp & ts!j <= Atyp & Some(ts[k:=Atyp]) <= T!(p+1) - | Bop i j k => ts!i <= Btyp & ts!j <= Btyp & Some(ts[k:=Btyp]) <= T!(p+1) - | Cop i j k => ts!i <= Ctyp & ts!j <= Ctyp & Some(ts[k:=Ctyp]) <= T!(p+1) - | Comp i j q => (ts!i <= ts!j & ts!j ~= Top | ts!j <= ts!i & ts!i ~= Top) & - T!p <= T!(p+1) & T!p <= T!q - | Halt => True" - - stype :: ('a,'b,'c)instr list => typ list set -"stype bs == listsn (maxregs bs) UNIV" - -constdefs - succs :: "('a,'b,'c)instr => nat => nat list" -"succs instr p == - case instr of - Move i j => [p+1] - | Aload x i => [p+1] - | Bload x i => [p+1] - | Cload x i => [p+1] - | Aop i j k => [p+1] - | Bop i j k => [p+1] - | Cop i j k => [p+1] - | Comp i j q => [p+1,q] - | Halt => []" - - exec :: "('a,'b,'c)instr => typ list => typ list option" -"exec instr ts == - case instr of - Move i j => Some(ts[j := ts!i]) - | Aload x i => Some(ts[i := Atyp]) - | Bload x i => Some(ts[i := Btyp]) - | Cload x i => Some(ts[i := Ctyp]) - | Aop i j k => if ts!i <= Atyp & ts!j <= Atyp - then Some(ts[k := Atyp]) - else None - | Bop i j k => if ts!i <= Btyp & ts!j <= Btyp - then Some(ts[k := Btyp]) - else None - | Cop i j k => if ts!i <= Ctyp & ts!j <= Ctyp - then Some(ts[k := Ctyp]) - else None - | Comp i j q => if ts!i <= ts!j & ts!j ~= Top | ts!j <= ts!i & ts!i ~= Top - then Some ts - else None - | Halt => Some ts" -(* - | Bop i j k => if ts!i <= Btyp & ts!j <= Btyp - then Some(ts[k := ts!i+ts!j]) - else None -*) -end diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Opt.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Opt.ML Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,105 @@ +(* 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))"; +br 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 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"; +br iffI 1; + by(Blast_tac 1); +br 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Opt.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Opt.thy Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,28 @@ +(* 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Orders.ML --- a/src/HOL/BCV/Orders.ML Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,177 +0,0 @@ -(* Title: HOL/BCV/Orders.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM -*) - -Delrules[le_maxI1, le_maxI2]; - -(** option **) -section "option"; - -Goalw [option_def] "None : option A"; -by (Simp_tac 1); -qed "None_in_option"; -AddIffs [None_in_option]; - -Goalw [option_def] "(Some x : option A) = (x:A)"; -by (Auto_tac); -qed "Some_in_option"; -AddIffs [Some_in_option]; - -Goalw [less_option,le_option] - "Some x < opt = (? y. opt = Some y & x < (y::'a::order))"; -by (simp_tac (simpset() addsimps [order_less_le] addsplits [option.split]) 1); -qed_spec_mp "Some_less_conv"; -AddIffs [Some_less_conv]; - -Goalw [less_option,le_option] "None < x = (? a. x = Some a)"; -by (asm_simp_tac (simpset() addsplits [option.split]) 1); -qed_spec_mp "None_less_iff"; -AddIffs [None_less_iff]; - - -Goalw [acc_def] "acc A ==> acc(option A)"; -by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 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 (Fast_tac 1); -by (Blast_tac 1); -qed "acc_option"; -Addsimps [acc_option]; -AddSIs [acc_option]; - - -(** list **) -section "list"; - -Goalw [le_list] "~ [] <= x#xs"; -by (Simp_tac 1); -qed "Nil_notle_Cons"; - -Goalw [le_list] "~ x#xs <= []"; -by (Simp_tac 1); -qed "Cons_notle_Nil"; - -AddIffs [Nil_notle_Cons,Cons_notle_Nil]; - -Goalw [le_list] "x#xs <= y#ys = (x <= y & xs <= ys)"; -by (rtac iffI 1); - by (Asm_full_simp_tac 1); - by (Clarify_tac 1); - by (rtac conjI 1); - by (eres_inst_tac [("x","0")] allE 1); - by (Asm_full_simp_tac 1); - by (Clarify_tac 1); - by (eres_inst_tac [("x","Suc i")] allE 1); - by (Asm_full_simp_tac 1); -by (Asm_full_simp_tac 1); -by (Clarify_tac 1); -by (case_tac "i" 1); -by (ALLGOALS Asm_simp_tac); -qed "Cons_le_Cons"; -AddIffs [Cons_le_Cons]; - -Goal "(x#xs <= ys) = (? z zs. ys = z#zs & x <= z & xs <= zs)"; -by (case_tac "ys" 1); -by (ALLGOALS Asm_simp_tac); -qed "Cons_le_iff"; - -Goal "(xs <= y#ys) = (? z zs. xs = z#zs & z <= y & zs <= ys)"; -by (case_tac "xs" 1); -by (ALLGOALS Asm_simp_tac); -qed "le_Cons_iff"; - -Goalw [less_list] - "x#xs < y#ys = (x < (y::'a::order) & xs <= ys | x = y & xs < ys)"; -by (simp_tac (simpset() addsimps [order_less_le]) 1); -by (Blast_tac 1); -qed "Cons_less_Cons"; -AddIffs [Cons_less_Cons]; - -Goalw [le_list] - "[| i xs[i:=x] <= ys[i:=y]"; -by (asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1); -qed "list_update_le_cong"; - -Goal "!i < length xs. (xs[i := x] <= xs) = ((x::'a::order) <= xs!i)"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (asm_simp_tac (simpset() addsplits [nat.split]) 1); -qed_spec_mp "list_update_le_conv"; - -Goalw [listsn_def] "xs : listsn n A ==> length xs = n"; -by (Blast_tac 1); -qed "listsnE_length"; -Addsimps [listsnE_length]; - -Goalw [listsn_def] "xs : listsn n A ==> set xs <= A"; -by (Blast_tac 1); -qed "listsnE_set"; -Addsimps [listsnE_set]; - -Goalw [listsn_def] "listsn 0 A = {[]}"; -by (Auto_tac); -qed "listsn_0"; -Addsimps [listsn_0]; - -Goalw [listsn_def] - "(xs : listsn (Suc n) A) = (? y:A. ? ys:listsn n A. xs = y#ys)"; -by (case_tac "xs" 1); -by (Auto_tac); -qed "in_listsn_Suc_iff"; - - -Goal "? a. a:A ==> ? xs. xs : listsn n A"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [in_listsn_Suc_iff]) 1); -by (Blast_tac 1); -qed "listsn_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 : listsn n A; i < n |] ==> (xs!i) : A"; -by (blast_tac (HOL_cs addIs [nth_in,listsnE_length,listsnE_set]) 1); -qed "listsnE_nth_in"; - -Goalw [listsn_def] - "[| xs : listsn n A; x:A; i < n |] ==> xs[i := x] : listsn n A"; -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addDs [set_update_subset_insert RS subsetD]) 1); -qed "list_update_in_listsn"; -Addsimps [list_update_in_listsn]; -AddSIs [list_update_in_listsn]; - - -Goalw [acc_def] "acc(A) ==> acc(listsn n A)"; -by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); -by (induct_tac "n" 1); - by (simp_tac (simpset() addcongs [conj_cong]) 1); -by (simp_tac (simpset() addsimps [in_listsn_Suc_iff]) 1); -by (Clarify_tac 1); -by (rename_tac "M m" 1); -by (case_tac "? x xs. x:A & xs:listsn n A & x#xs : M" 1); - by (etac thin_rl 2); - by (etac thin_rl 2); - by (Blast_tac 2); -by (eres_inst_tac [("x","{a. a:A & (? xs. xs:listsn n A & 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","{xs. xs:listsn n A & maxA#xs : M}")] allE 1); -by (Blast_tac 1); -qed "acc_listsn"; -Addsimps [acc_listsn]; -AddSIs [acc_listsn]; diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Orders.thy --- a/src/HOL/BCV/Orders.thy Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* Title: HOL/BCV/Orders.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM - -Orderings and some sets. -*) - -Orders = Orders0 + - -instance option :: (order)order (le_option_refl,le_option_trans, - le_option_antisym,less_le_option) -instance list :: (order)order (le_list_refl,le_list_trans, - le_list_antisym,less_le_list) -instance "*" :: (order,order)order - (le_prod_refl,le_prod_trans,le_prod_antisym,less_le_prod) - -constdefs - acc :: "'a::order set => bool" -"acc A == wf{(y,x) . x:A & y:A & x < y}" - - option :: 'a set => 'a option set -"option A == insert None {x . ? y:A. x = Some y}" - - listsn :: nat => 'a set => 'a list set -"listsn n A == {xs. length xs = n & set xs <= A}" - -end diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Orders0.ML --- a/src/HOL/BCV/Orders0.ML Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,129 +0,0 @@ -(* Title: HOL/BCV/Orders0.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM -*) - -(** option **) -section "option"; - -Goalw [le_option] "(o1::('a::order)option) <= o1"; -by (simp_tac (simpset() addsplits [option.split]) 1); -qed "le_option_refl"; - -Goalw [le_option] "(o1::('a::order)option) <= o2 --> o2<=o3 --> o1<=o3"; -by (simp_tac (simpset() addsplits [option.split]) 1); -by (blast_tac (claset() addIs [order_trans]) 1); -qed_spec_mp "le_option_trans"; - -Goalw [le_option] "(o1::('a::order)option) <= o2 --> o2<=o1 --> o1=o2"; -by (simp_tac (simpset() addsplits [option.split]) 1); -by (blast_tac (claset() addIs [order_antisym]) 1); -qed_spec_mp "le_option_antisym"; - -Goalw [less_option] "(o1::('a::ord)option) < o2 = (o1<=o2 & o1 ~= o2)"; -by (rtac refl 1); -qed "less_le_option"; - -Goalw [le_option] "Some x <= opt = (? y. opt = Some y & x <= y)"; -by (simp_tac (simpset() addsplits [option.split]) 1); -qed_spec_mp "Some_le_conv"; -AddIffs [Some_le_conv]; - -Goalw [le_option] "None <= opt"; -by (simp_tac (simpset() addsplits [option.split]) 1); -qed "None_le"; -AddIffs [None_le]; - - -(** list **) -section "list"; - -Goalw [le_list] "[| xs <= ys; p < size xs |] ==> xs!p <= ys!p"; -by (Blast_tac 1); -qed "le_listD"; - -Goalw [le_list] "([] <= ys) = (ys = [])"; -by (Simp_tac 1); -qed "Nil_le_conv"; -AddIffs [Nil_le_conv]; - -Goalw [le_list] "(xs::('a::order)list) <= xs"; -by (induct_tac "xs" 1); -by (Auto_tac); -qed "le_list_refl"; - -Goalw [le_list] - "!ys zs.(xs::('a::order)list) <= ys --> ys <= zs --> xs <= zs"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (rtac allI 1); -by (case_tac "ys" 1); - by (hyp_subst_tac 1); - by (Simp_tac 1); -by (rtac allI 1); -by (case_tac "zs" 1); - by (hyp_subst_tac 1); - by (Simp_tac 1); -by (hyp_subst_tac 1); -by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); -by (Clarify_tac 1); -by (rtac conjI 1); - by (REPEAT(EVERY1[etac allE, etac conjE, etac impE, rtac refl])); - by (blast_tac (claset() addIs [order_trans]) 1); -by (Clarify_tac 1); -by (EVERY[etac allE 1, etac allE 1, etac impE 1, etac impE 2]); - by (rtac conjI 1); - by (assume_tac 1); - by (Blast_tac 1); - by (rtac conjI 1); - by (assume_tac 1); - by (Blast_tac 1); -by (Asm_full_simp_tac 1); -qed_spec_mp "le_list_trans"; - -Goalw [le_list] - "!ys. (xs::('a::order)list) <= ys --> ys <= xs --> xs = ys"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (rtac allI 1); -by (case_tac "ys" 1); - by (hyp_subst_tac 1); - by (Simp_tac 1); -by (hyp_subst_tac 1); -by (simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); -by (Clarify_tac 1); -by (rtac conjI 1); - by (blast_tac (claset() addIs [order_antisym]) 1); -by (Asm_full_simp_tac 1); -qed_spec_mp "le_list_antisym"; - -Goalw [less_list] "(xs::('a::ord)list) < ys = (xs<=ys & xs ~= ys)"; -by (rtac refl 1); -qed "less_le_list"; - -(** product **) -section "product"; - -Goalw [le_prod] "(p1::('a::order * 'b::order)) <= p1"; -by (Simp_tac 1); -qed "le_prod_refl"; - -Goalw [le_prod] - "[| (p1::('a::order * 'b::order)) <= p2; p2<=p3 |] ==> p1<=p3"; -by (blast_tac (claset() addIs [order_trans]) 1); -qed "le_prod_trans"; - -Goalw [le_prod] - "[| (p1::('a::order * 'b::order)) <= p2; p2 <= p1 |] ==> p1 = p2"; -by (blast_tac (claset() addIs [order_antisym,trans,surjective_pairing,sym]) 1); -qed_spec_mp "le_prod_antisym"; - -Goalw [less_prod] "(p1::('a::order * 'b::order)) < p2 = (p1<=p2 & p1 ~= p2)"; -by (rtac refl 1); -qed "less_le_prod"; - -Goalw [le_prod] "((a,b) <= (c,d)) = (a <= c & b <= d)"; -by (Simp_tac 1); -qed "le_prod_iff"; -AddIffs [le_prod_iff]; diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Orders0.thy --- a/src/HOL/BCV/Orders0.thy Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -(* Title: HOL/BCV/Orders0.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM - -Orderings on various types. -*) - -Orders0 = Main + - -instance option :: (ord)ord -instance list :: (ord)ord -instance "*" :: (ord,ord)ord - -defs -le_option "o1 <= o2 == case o2 of None => o1=None | - Some y => (case o1 of None => True | Some x => x<=y)" -less_option "(o1::('a::ord)option) < o2 == o1 <= o2 & o1 ~= o2" - -le_list "xs <= ys == size xs = size ys & (!i. i xs!i <= ys!i)" -less_list "(xs::('a::ord)list) < ys == xs <= ys & xs ~= ys" - -le_prod "p1 <= p2 == fst p1 <= fst p2 & snd p1 <= snd p2" -less_prod "(p1::('a::ord * 'b::ord)) < p2 == p1 <= p2 & p1 ~= p2" - -end diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Plus.ML --- a/src/HOL/BCV/Plus.ML Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,48 +0,0 @@ -(* Title: HOL/BCV/Plus.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM -*) - -(** option **) - -Goalw [plus_option] "x+None = x"; -by (simp_tac (simpset() addsplits [option.split]) 1); -qed "plus_None"; -Addsimps [plus_None]; - -Goalw [plus_option] "None+x = x"; -by (simp_tac (simpset() addsplits [option.split]) 1); -qed "None_plus"; -Addsimps [None_plus]; - -Goalw [plus_option] "Some x + Some y = Some(x+y)"; -by (Simp_tac 1); -qed "Some_plus_Some"; -Addsimps [Some_plus_Some]; - -Goalw [plus_option] "? y. Some x + opt = Some y"; -by (simp_tac (simpset() addsplits [option.split]) 1); -qed "plus_option_Some_Some"; - -(** list **) - -Goal "list_plus xs [] = xs"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (asm_simp_tac (simpset() addsplits [list.split]) 1); -qed "list_plus_Nil2"; -Addsimps [list_plus_Nil2]; - -Goal "!ys. length(list_plus xs ys) = max(length xs) (length ys)"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (asm_simp_tac (simpset() addsplits [list.split]) 1); -qed_spec_mp "length_list_plus"; -Addsimps [length_list_plus]; - -Goalw [plus_list] - "length(ts+us) = max (length ts) (length us)"; -by (Simp_tac 1); -qed "length_plus_list"; -Addsimps [length_plus_list]; diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Plus.thy --- a/src/HOL/BCV/Plus.thy Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -(* Title: HOL/BCV/Plus.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM - -Supremum operation on various domains. -*) - -Plus = Orders + - -instance option :: (plus)plus -instance list :: (plus)plus -instance "*" :: (plus,plus)plus - -consts list_plus :: "('a::plus)list => 'a list => 'a list" -primrec -"list_plus [] ys = ys" -"list_plus (x#xs) ys = (case ys of [] => x#xs | z#zs => (x+z)#list_plus xs zs)" -defs -plus_option "o1 + o2 == case o1 of None => o2 - | Some x => (case o2 of None => o1 - | Some y => Some(x+y))" -plus_list "op + == list_plus" -plus_prod "op + == %(a,b) (c,d). (a+c,b+d)" - -end diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Product.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Product.ML Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,114 @@ +(* 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)"; +br wf_subset 1; + be wf_lex_prod 1; + ba 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))"; +br iffI 1; + by (Clarify_tac 1); + bd (OK_le_err_OK RS iffD2) 1; + bd (OK_le_err_OK RS iffD2) 1; + bd semilat_lub 1; + ba 1; + ba 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); + ba 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); + ba 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); + +br (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); + +br (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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Product.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Product.thy Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,25 @@ +(* 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 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/README.html --- a/src/HOL/BCV/README.html Fri Sep 01 18:01:05 2000 +0200 +++ b/src/HOL/BCV/README.html Fri Sep 01 18:29:52 2000 +0200 @@ -1,16 +1,17 @@ HOL/BCV/README -

Towards Verified Bytecode Verifiers

+

Verified Bytecode Verifiers

-This theory defines a very abstract and generic model of bytecode -verification, i.e. data-flow analysis for assembly languages with subtypes. +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: - -Towards Verified Bytecode Verifiers. + +Verified Bytecode Verifiers. diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/ROOT.ML --- a/src/HOL/BCV/ROOT.ML Fri Sep 01 18:01:05 2000 +0200 +++ b/src/HOL/BCV/ROOT.ML Fri Sep 01 18:29:52 2000 +0200 @@ -1,10 +1,12 @@ (* Title: HOL/BCV/ROOT.ML ID: $Id$ Author: Tobias Nipkow - Copyright 1999 TUM + Copyright 2000 TUM A simple model of dataflow (sub)type analysis of instruction sequences, aka `bytecode verification'. *) -time_use_thy "Machine"; +writeln"Root file for HOL/BCV"; + +use_thy"JVM"; diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/SemiLattice.ML --- a/src/HOL/BCV/SemiLattice.ML Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,155 +0,0 @@ -(* Title: HOL/BCV/SemiLattice.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM -*) - -Goalw [semilat_def] "[| x:A; y:A; semilat A |] ==> x <= x+y"; -by (Blast_tac 1); -qed "semilat_ub1"; - -Goalw [semilat_def] "[| x:A; y:A; semilat A |] ==> y <= x+y"; -by (Blast_tac 1); -qed "semilat_ub2"; - -Goalw [semilat_def] "[| x:A; y:A; z:A; x <= z; y <= z; semilat A |] ==> x+y <= z"; -by (Blast_tac 1); -qed "semilat_lub"; - -Goalw [semilat_def] "[| x:A; y:A; semilat A |] ==> x+y : A"; -by (Blast_tac 1); -qed "semilat_plus"; - -Addsimps [semilat_ub1,semilat_ub2,semilat_lub,semilat_plus]; - -Goal "[| x:A; y:A; semilat A |] ==> (x <= y) = (x+y = y)"; -by (rtac iffI 1); - by (REPEAT(ares_tac [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 |] ==> (x <= y) = (y = x+y)"; -by (rtac iffI 1); - by (REPEAT(ares_tac [order_antisym,semilat_lub,order_refl,semilat_ub2] 1)); -by (etac ssubst 1); -by (Asm_simp_tac 1); -qed "le_iff_plus_unchanged2"; - -Goal "[| x:A; y:A; z:A; semilat A; x <= y | x <= z |] ==> x <= y+z"; -by (blast_tac (claset() addIs [order_trans,semilat_ub1,semilat_ub2]) 1); -qed "plus_mono"; - -Goal "[| x:A; semilat A |] ==> x+x = x"; -by (REPEAT(ares_tac [order_refl RSN (4,le_iff_plus_unchanged RS iffD1)] 1)); -qed "semilat_idemp"; -Addsimps [semilat_idemp]; - -Goal "[| x:A; y:A; z:A; semilat A |] ==> (x+y)+z = x+(y+z)"; -by (blast_tac (HOL_cs addSIs [order_refl,order_antisym,semilat_lub,semilat_plus] - addIs [plus_mono]) 1); -qed "semilat_assoc"; - -Goal "[| x:A; y:A; semilat A |] ==> x+(x+y) = x+y"; -by (asm_simp_tac (simpset() addsimps [semilat_assoc RS sym]) 1); -qed "semilat_assoc_idemp"; -Addsimps [semilat_assoc_idemp]; - -Goal "[| x:A; y:A; z:A; semilat A |] ==> (x+y <= z) = (x <= z & y <= z)"; -by (blast_tac (claset() addIs [semilat_ub1,semilat_ub2,semilat_lub,order_trans]) 1); -qed "plus_le_conv"; -Addsimps [plus_le_conv]; - - -(** option **) - -Goal "semilat A ==> semilat (option A)"; -by (simp_tac (simpset() addsimps [semilat_def,le_option,plus_option] - addsplits [option.split]) 1); -by (blast_tac (claset() addIs [semilat_ub1,semilat_ub2,semilat_lub,semilat_plus]) 1); -qed "semilat_option"; -Addsimps [semilat_option]; -AddSIs [semilat_option]; - -(** list **) -Goalw [plus_list] "[] + [] = []"; -by (Simp_tac 1); -qed "plus_Nil_Nil"; -Addsimps [plus_Nil_Nil]; - -Goalw [plus_list] "(x#xs) + (y#ys) = (x+y)#(xs+ys)"; -by (Simp_tac 1); -qed "plus_Cons_Cons"; -Addsimps [plus_Cons_Cons]; - -Goal - "!xs ys i. length xs = n--> length ys = n--> i (xs+ys)!i = xs!i + 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 (case_tac "ys" 1); - by (Asm_full_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1); -qed_spec_mp "nth_plus"; -Addsimps [nth_plus]; - -Goalw [le_list] - "semilat A ==> !xs:listsn n A. !ys:listsn n A. xs <= xs+ys"; -by (asm_simp_tac (simpset() addsimps [le_max_iff_disj]) 1); -by (Clarify_tac 1); -by (blast_tac (HOL_cs addIs [nth_in,nth_plus,listsnE_length,listsnE_set,semilat_ub1]) 1); -qed_spec_mp "plus_list_ub1"; - -Goalw [le_list] - "semilat A ==> !xs:listsn n A. !ys:listsn n A. ys <= xs+ys"; -by (asm_simp_tac (simpset() addsimps [le_max_iff_disj]) 1); -by (Clarify_tac 1); -by (blast_tac (HOL_cs addIs [nth_in,nth_plus,listsnE_length,listsnE_set,semilat_ub2]) 1); -qed_spec_mp "plus_list_ub2"; - -Goalw [le_list] - "semilat A ==> !xs:listsn n A. !ys:listsn n A. !zs:listsn n A. \ -\ xs <= zs & ys <= zs --> xs+ys <= zs"; -by (asm_simp_tac (simpset() addsimps [le_max_iff_disj] addcongs [conj_cong]) 1); -by (Clarify_tac 1); -by (blast_tac (HOL_cs addIs [nth_in,nth_plus,listsnE_length,listsnE_set,semilat_lub]) 1); -qed_spec_mp "plus_list_lub"; - -Goalw [listsn_def] - "semilat A ==> !xs:listsn n A. !ys:listsn n A. xs+ys : listsn n A"; -by (induct_tac "n" 1); - by (Simp_tac 1); -by (Asm_full_simp_tac 1); -by (Clarify_tac 1); -by (case_tac "xs" 1); - by (Asm_full_simp_tac 1); -by (case_tac "ys" 1); - by (Asm_full_simp_tac 1); -by (Asm_full_simp_tac 1); -by (blast_tac (claset() addIs [semilat_plus]) 1); -qed_spec_mp "plus_list_closed"; - -Goal "semilat A ==> semilat (listsn n A)"; -by (simp_tac (HOL_basic_ss addsimps [semilat_def]) 1); -by (asm_simp_tac (HOL_ss addsimps [plus_list_ub1,plus_list_ub2,plus_list_lub,plus_list_closed]) 1); -qed "semilat_listsn"; -Addsimps [semilat_listsn]; -AddSIs [semilat_listsn]; - -Goalw [le_list] - "!i xs. xs : listsn n A --> x:A --> semilat A --> i xs <= xs[i := x + xs!i]"; -by (Simp_tac 1); -by (induct_tac "n" 1); - by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [in_listsn_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"; - -(* product *) - -Goalw [semilat_def,plus_prod] "[| semilat A; semilat B |] ==> semilat (A <*> B)"; -by (Asm_simp_tac 1); -qed "semilat_Times"; diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/SemiLattice.thy --- a/src/HOL/BCV/SemiLattice.thy Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,18 +0,0 @@ -(* Title: HOL/BCV/SemiLattice.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM - -Semilattices -*) - -SemiLattice = Plus + - -constdefs - semilat :: "('a::{order,plus} set) => bool" -"semilat A == (!x:A. !y:A. x <= x+y) & - (!x:A. !y:A. y <= x+y) & - (!x:A. !y:A. !z:A. x <= z & y <= z --> x+y <= z) & - (!x:A. !y:A. x+y : A)" - -end diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Semilat.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Semilat.ML Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,177 @@ +(* 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 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)"; +br (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)"; +ba 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"; +ba 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] + "[| univalent 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 [univalentD]) 1); +br exI 1; +br conjI 1; + by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]addDs [univalentD]) 1); +by(blast_tac (claset() addIs [rtrancl_into_rtrancl,rtrancl_into_rtrancl2] + addEs [converse_rtranclE] addDs [univalentD]) 1); +qed "extend_lub"; + +Goal "[| univalent 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 "univalent_has_lubs"; + +Goalw [some_lub_def,is_lub_def] + "[| acyclic r; is_lub (r^*) x y u |] ==> some_lub (r^*) x y = u"; +br selectI2 1; + ba 1; +by(blast_tac (claset() addIs [antisymD] + addSDs [acyclic_impl_antisym_rtrancl]) 1); +qed "some_lub_conv"; + +Goal + "[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |] ==> \ +\ is_lub (r^*) x y (some_lub (r^*) x y)"; +by(fast_tac + (claset() addDs [univalent_has_lubs] + addss (simpset() addsimps [some_lub_conv])) 1); +qed "is_lub_some_lub"; diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Semilat.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BCV/Semilat.thy Fri Sep 01 18:29:52 2000 +0200 @@ -0,0 +1,61 @@ +(* 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 diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Types.ML --- a/src/HOL/BCV/Types.ML Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,31 +0,0 @@ -(* Title: HOL/BCV/Types.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM -*) - -Goalw [semilat_def,le_typ,plus_typ] "semilat (UNIV::typ set)"; -by (Auto_tac); -qed "semilat_typ"; -AddIffs [semilat_typ]; - -Goal "{(x,y::'a::order). y t1<=t3"; -by (Blast_tac 1); -qed "le_typ_trans"; - -Goalw [le_typ] "[| (t1::typ) <= t2; t2<=t1 |] ==> t1=t2"; -by (Blast_tac 1); -qed "le_typ_antisym"; - -Goalw [less_typ] "(t1::typ) < t2 = (t1<=t2 & t1 ~= t2)"; -by (rtac refl 1); -qed "less_le_typ"; - -Goal "(UNIV::typ set) = {Atyp,Btyp,Ctyp,Top}"; -by (Auto_tac); -by (rename_tac "t" 1); -by (case_tac "t" 1); -by (Auto_tac); -qed "UNIV_typ_enum"; - -Goal "finite(UNIV::typ set)"; -by (simp_tac (simpset() addsimps [UNIV_typ_enum]) 1); -qed "finite_UNIV_typ"; -AddIffs [finite_UNIV_typ]; diff -r 978c635c77f6 -r a39e5d43de55 src/HOL/BCV/Types0.thy --- a/src/HOL/BCV/Types0.thy Fri Sep 01 18:01:05 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* Title: HOL/BCV/Types0.thy - ID: $Id$ - Author: Tobias Nipkow - Copyright 1999 TUM - -Types for the register machine -*) - -Types0 = SemiLattice + - -datatype typ = Atyp | Btyp | Ctyp | Top - -instance typ :: ord -instance typ :: plus - -defs -le_typ "t1 <= t2 == (t1=t2) | (t1=Atyp & t2=Btyp) | (t2=Top)" -less_typ "(t1::typ) < t2 == t1 <= t2 & t1 ~= t2" -plus_typ "t1 + t2 == if t1<=t2 then t2 else if t2 <= t1 then t1 else Top" - -end