--- /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<n. ss!p ~= T; p < n |] ==> \
+\ wti ss p = stable r step succs ss p";
+by (Asm_simp_tac 1);
+qed "wti_is_stable_toplessD";
+
+Goalw [is_dfa_def]
+ "[| is_dfa r dfa step succs n A; ss : list n A |] ==> \
+\ dfa ss:list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss & \
+\ (!ts: list n A. stables r step succs ts & ss <=[r] ts \
+\ --> dfa ss <=[r] ts)";
+by (Asm_full_simp_tac 1);
+qed "is_dfaD";
+
+Goalw [is_bcv_def,welltyping_def,stables_def]
+ "[| order r; top r T; \
+\ wti_is_stable_topless r T step wti succs n A; \
+\ is_dfa r dfa step succs n A |] ==> is_bcv r T wti n A dfa";
+by(Clarify_tac 1);
+by (dtac is_dfaD 1);
+by (assume_tac 1);
+by(Clarify_tac 1);
+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";
+*)
--- /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<size ss. stable r step succs ss p"
+
+ is_dfa :: 's ord
+ => ('s list => 's list)
+ => (nat => 's => 's)
+ => (nat => nat list)
+ => nat => 's set => bool
+"is_dfa r dfa step succs n A == !ss : list n A.
+ dfa ss : list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss &
+ (!ts: list n A. ss <=[r] ts & stables r step succs ts
+ --> dfa ss <=[r] ts)"
+
+ is_bcv :: 's ord => 's => ('s list => nat => bool)
+ => nat => 's set => ('s list => 's list) => bool
+"is_bcv r T wti n A bcv == !ss : list n A.
+ (!p<n. (bcv ss)!p ~= T) =
+ (? ts: list n A. ss <=[r] ts & welltyping T wti ts)"
+
+ wti_is_stable_topless ::
+ 's ord => 's
+ => (nat => 's => 's)
+ => ('s list => nat => bool)
+ => (nat => nat list)
+ => nat => 's set => bool
+"wti_is_stable_topless r T step wti succs n A == !ss p.
+ ss : list n A & (!p<n. ss!p ~= T) & p < n -->
+ wti ss p = stable r step succs ss p"
+
+ welltyping :: 's => ('s list => nat => bool) => 's list => bool
+"welltyping T wti ts == !p<size(ts). ts!p ~= T & wti ts p"
+
+end
--- a/src/HOL/BCV/DFAandWTI.ML Fri Sep 01 18:01:05 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-(* Title: HOL/BCV/DFAandWTI.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1999 TUM
-*)
-
-Goalw [wti_is_fix_step_def]
- "[| wti_is_fix_step step wti succs n L; \
-\ sos : listsn n (option L); p < n |] ==> \
-\ 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";
--- 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<size(tos). wti p tos"
-
- is_dfa :: ('s os => 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
--- 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<n) --> \
-\ 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<n) \
-\ --> 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<n) --> \
-\ (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<n |] ==> \
-\ 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<n; \
-\ sos <= tos; sos : listsn n (option L); tos : listsn n (option L) |] \
-\ ==> 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<n. ? s. sos!p = Some s & step p s = None";
-by (subgoal_tac "n=size sos" 1);
-by (Blast_tac 1);
-by (Asm_simp_tac 1);
-qed "next_None";
-
-Goalw [is_next_def]
- "[| is_next next; succs_bounded succs n; sos : listsn n S |] ==> \
-\ next step succs sos = Some sos --> \
-\ (!p<n. !s. sos!p = Some s --> (? 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<n. ? s. sos!p = Some s & (? 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_Some2";
-
-Goal
- "[| is_next next; succs_bounded succs n; sos : listsn n S |] ==> \
-\ (next step succs sos = Some sos) = \
-\ (!p<n. !s. sos!p = Some s --> (? 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<n; step p s = Some(t) |] ==> 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<n. stable step succs p sos)";
-by (Asm_simp_tac 1);
-by (rtac iffI 1);
- by (Clarify_tac 1);
- by (etac allE 1 THEN mp_tac 1);
- by (etac allE 1 THEN mp_tac 1);
- by (Clarify_tac 1);
- bd(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 1);
-by (Clarify_tac 1);
-by (etac allE 1 THEN mp_tac 1);
-by (Asm_full_simp_tac 1);
-by (Clarify_tac 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addSIs [merges_same_conv RS iffD2]
- addIs [step_pres_typeD,succs_boundedD,listsn_optionE_in]) 1);
-qed "fixpoint_next_iff_stable";
-
-Goal
- "[| semilat L; is_next next; succs_bounded succs n; \
-\ step_pres_type step n L; step_mono_None step n L; step_mono step n L; \
-\ tos:listsn n (option L); next step succs tos = Some tos; \
-\ sos:listsn n (option L); sos <= tos |] \
-\ ==> ? sos'. next step succs sos = Some sos' & sos' <= tos";
-by (subgoal_tac
- "!p<n. !s. sos!p = Some s --> (? 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";
--- 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<n. !q:set(succs p). q<n"
-
- is_next :: "((nat => '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<size sos. ? s. sos!p = Some s & step p s = None)) &
- (next step succs sos = Some sos -->
- (!p<size sos. !s. sos!p = Some s --> (? t.
- step p s = Some(t) & merges t (succs p) sos = sos))) &
- (next step succs sos = Some sos' & sos' ~= sos -->
- (? p<size sos. ? s. sos!p = Some s & (? t.
- step p s = Some(t) & merges t (succs p) sos = sos')))"
-
- step_pres_type :: "(nat => 's => 's option) => nat => 's set => bool"
-"step_pres_type step n L == !s:L. !p<n. !t. step p s = Some(t) --> 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
--- /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";
--- /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
--- 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";
-*)
--- 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
--- /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];
--- /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
--- /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";
--- /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
--- /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<n |] ==> step p s : A";
+by (Blast_tac 1);
+qed "pres_typeD";
+
+Goalw [bounded_def]
+ "[| bounded succs n; p < n; q : set(succs p) |] ==> q < n";
+by (Blast_tac 1);
+qed "boundedD";
+
+Goalw [mono_def]
+ "[| mono r step n A; p < n; s:A; s <=_r t |] ==> step p s <=_r step p t";
+by (Blast_tac 1);
+qed "monoD";
+
+(** merges **)
+
+Goal "!ss. size(merges f t ps ss) = size ss";
+by (induct_tac "ps" 1);
+by (Auto_tac);
+qed_spec_mp "length_merges";
+Addsimps [length_merges];
+
+Goalw [closed_def]
+ "[| semilat(A,r,f) |] ==> \
+\ !xs. xs : list n A --> x : A --> (!p : set ps. p<n) \
+\ --> merges f x ps xs : list n A";
+by(ftac semilatDclosedI 1);
+by(rewtac closed_def);
+by (induct_tac "ps" 1);
+by (Auto_tac);
+qed_spec_mp "merges_preserves_type";
+Addsimps [merges_preserves_type];
+
+Goal
+ "[| semilat(A,r,f) |] ==> \
+\ !xs. xs : list n A --> x : A --> (!p:set ps. p<size xs) --> xs <=[r] merges f x ps xs";
+by (induct_tac "ps" 1);
+ by (Asm_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (rtac order_trans 1);
+ by(Asm_simp_tac 1);
+ by (etac list_update_incr 1);
+ 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<size xs) --> \
+\ (merges f x ps xs = xs) = (!p:set ps. x <=_r xs!p))";
+by (induct_tac "ps" 1);
+ by (Asm_simp_tac 1);
+by (Clarsimp_tac 1);
+by (rename_tac "p ps xs" 1);
+by (rtac iffI 1);
+ by (rtac context_conjI 1);
+ by (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs" 1);
+ by (EVERY[etac subst 2, rtac merges_incr 2]);
+ by(force_tac (claset() addSDs [le_listD],
+ simpset() addsimps [nth_list_update]) 1);
+ by (assume_tac 1);
+ by (blast_tac (claset() addSIs [listE_set]
+ addIs [closedD,listE_length RS nth_in]) 1);
+ 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<size ts |] ==> \
+\ set qs <= set ps --> \
+\ (!ss. set ss <= A --> ss <=[r] ts --> merges f t qs ss <=[r] ts)";
+by (induct_tac "qs" 1);
+ by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (Clarify_tac 1);
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac 1);
+by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
+ by (asm_simp_tac (simpset() addsimps [closedD]) 1);
+by (asm_full_simp_tac (simpset() addsimps [list_update_le_listI]) 1);
+val lemma = result();
+
+Goal
+ "[| semilat(A,r,f); t:A; set ts <= A; set ss <= A; \
+\ !p. p:set ps --> t <=_r ts!p; \
+\ !p. p:set ps --> p<size ts; \
+\ ss <=[r] ts |] \
+\ ==> merges f t ps ss <=[r] ts";
+by (blast_tac (claset() addDs [lemma]) 1);
+qed "merges_pres_le_ub";
+
+Goal "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A --> \
+\ (!p:set ps. p<n) --> \
+\ (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)";
+by(induct_tac "ps" 1);
+ by (Simp_tac 1);
+by(asm_simp_tac (simpset() addsimps [nth_list_update,closedD,listE_nth_in]) 1);
+qed_spec_mp "nth_merges";
+
+
+(** propa **)
+
+Goal "!ss w. (!q:set qs. q < size ss) --> \
+\ propa f qs t ss w = \
+\ (merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)";
+by (induct_tac "qs" 1);
+ by(Simp_tac 1);
+by (Simp_tac 1);
+by(Clarify_tac 1);
+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<size ss |] ==> \
+\ iter(((A,r,f),step,succs),ss,w) = \
+\ (if w={} then ss \
+\ else let p = SOME p. p : w \
+\ in iter(((A,r,f),step,succs),merges f (step p (ss!p)) (succs p) ss, \
+\ {q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))";
+by (rtac ((iter_tc RS (iter_wf RS (hd iter.simps))) RS trans) 1);
+by (Asm_simp_tac 1);
+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<n. p~:w --> stable r step succs ss p) \
+\ --> iter(((A,r,f),step,succs),ss,w) : list n A & \
+\ stables r step succs (iter(((A,r,f),step,succs),ss,w)) & \
+\ ss <=[r] iter(((A,r,f),step,succs),ss,w) & \
+\ (! ts:list n A. \
+\ ss <=[r] ts & stables r step succs ts --> \
+\ iter(((A,r,f),step,succs),ss,w) <=[r] ts)";
+by(res_inst_tac [("A","A"),("r","r"),("f","f"),("step","step"),("ss","ss"),("w","w")]iter_induct 1);
+by(Clarify_tac 1);
+by(ftac listE_length 1);
+by(hyp_subst_tac 1);
+by(stac iter_unfold 1);
+ 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";
--- /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<n. !q:set(succs p). q<n"
+
+ pres_type :: "(nat => 's => 's) => nat => 's set => bool"
+"pres_type step n A == !s:A. !p<n. step p s : A"
+
+ mono :: "'s ord => (nat => 's => 's) => nat => 's set => bool"
+"mono r step n A ==
+ !s p t. s : A & p < n & s <=_r t --> step p s <=_r step p t"
+
+consts
+ iter :: "('s sl * (nat => 's => 's) * (nat => nat list))
+ * 's list * nat set => 's list"
+ propa :: "'s binop => nat list => 's => 's list => nat set => 's list * nat set"
+
+primrec
+"propa f [] t ss w = (ss,w)"
+"propa f (q#qs) t ss w = (let u = t +_f ss!q;
+ w' = (if u = ss!q then w else insert q w)
+ in propa f qs t (ss[q := u]) w')"
+
+recdef iter
+ "same_fst (%((A,r,f),step,succs). semilat(A,r,f) & acc r)
+ (%((A,r,f),step,succs).
+ {(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset)"
+"iter(((A,r,f),step,succs),ss,w) =
+ (if semilat(A,r,f) & acc r & (!p:w. p < size ss) &
+ bounded succs (size ss) & set ss <= A & pres_type step (size ss) A
+ then if w={} then ss
+ else let p = SOME p. p : w
+ in iter(((A,r,f),step,succs),
+ propa f (succs p) (step p (ss!p)) ss (w-{p}))
+ else arbitrary)"
+
+constdefs
+ unstables ::
+ "'s binop => (nat => 's => 's) => (nat => nat list) => 's list => nat set"
+"unstables f step succs ss ==
+ {p. p < size ss & (? q:set(succs p). step p (ss!p) +_f ss!q ~= ss!q)}"
+
+ kildall :: "'s sl => (nat => 's => 's) => (nat => nat list)
+ => 's list => 's list"
+"kildall Arf step succs ss ==
+ iter((Arf,step,succs),ss,unstables (snd(snd Arf)) step succs ss)"
+
+consts merges :: "'s binop => 's => nat list => 's list => 's list"
+primrec
+"merges f s [] ss = ss"
+"merges f s (p#ps) ss = merges f s ps (ss[p := s +_f ss!p])"
+
+end
--- /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<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";
+by(rewtac Listn.le_def);
+by (asm_full_simp_tac (simpset() addsimps [list_all2_conv_all_nth,nth_list_update]) 1);
+qed "list_update_le_cong";
+
+
+Goalw [Listn.le_def,lesub_def]
+ "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p";
+by (asm_full_simp_tac (simpset() addsimps [list_all2_conv_all_nth]) 1);
+qed "le_listD";
+
+Goalw [unfold_lesub_list] "!x. x <=_r x ==> xs <=[r] xs";
+by (asm_simp_tac (simpset() addsimps [Listn.le_def,list_all2_conv_all_nth]) 1);
+qed "le_list_refl";
+
+Goalw [unfold_lesub_list]
+ "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs";
+by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [order_trans]) 1);
+qed "le_list_trans";
+
+Goalw [unfold_lesub_list]
+ "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys";
+by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1);
+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<n --> \
+\ (xs +[f] ys)!i = (xs!i) +_f (ys!i)";
+by (induct_tac "n" 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
+by (case_tac "xs" 1);
+ by (Asm_full_simp_tac 1);
+by (force_tac (claset(),simpset() addsimps [nth_Cons]
+ addsplits [list.split,nat.split]) 1);
+qed_spec_mp "nth_plus_list";
+Addsimps [nth_plus_list];
+
+Goalw [unfold_lesub_list]
+ "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |] \
+\ ==> xs <=[r] xs +[f] ys";
+by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1);
+qed_spec_mp "plus_list_ub1";
+
+Goalw [unfold_lesub_list]
+ "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |] \
+\ ==> ys <=[r] xs +[f] ys";
+by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1);
+qed_spec_mp "plus_list_ub2";
+
+Goalw [unfold_lesub_list]
+ "semilat(A,r,f) ==> !xs ys zs. set xs <= A --> set ys <= A --> set zs <= A \
+\ --> size xs = n & size ys = n --> \
+\ xs <=[r] zs & ys <=[r] zs --> xs +[f] ys <=[r] zs";
+by (asm_full_simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1);
+qed_spec_mp "plus_list_lub";
+
+Goalw [unfold_lesub_list]
+ "[| semilat(A,r,f); x:A |] ==> set xs <= A --> \
+\ (!i. i<size xs --> xs <=[r] xs[i := x +_f xs!i])";
+by (simp_tac(simpset()addsimps[Listn.le_def,list_all2_conv_all_nth])1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [in_list_Suc_iff]) 1);
+by (Clarify_tac 1);
+by (asm_simp_tac (simpset() addsimps [nth_Cons] addsplits [nat.split]) 1);
+qed_spec_mp "list_update_incr";
+
+Goalw [acc_def] "[| order r; acc r |] ==> acc(Listn.le r)";
+by(subgoal_tac
+ "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})" 1);
+ 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";
--- /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
--- 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<size(bs) --> 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";
--- 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
--- /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";
+
--- /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
--- 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<size xs; xs <= ys; x <= y |] ==> 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];
--- 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
--- 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];
--- 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<size xs --> 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
--- 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];
--- 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
--- /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";
--- /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
--- 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 @@
<HTML><HEAD><TITLE>HOL/BCV/README</TITLE></HEAD>
<BODY>
-<H1>Towards Verified Bytecode Verifiers</H1>
+<H1>Verified Bytecode Verifiers</H1>
-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.
<P>
A paper describing the theory is found here:
-<A HREF = "http://www4.in.tum.de/~nipkow/pubs/bcv.html">
-Towards Verified Bytecode Verifiers</A>.
+<A HREF = "http://www.in.tum.de/~nipkow/pubs/bcv2.html">
+Verified Bytecode Verifiers</A>.
</BODY>
</HTML>
--- 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";
--- 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<n--> (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<n --> 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";
--- 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
--- /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";
--- /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
--- 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<x}^+ = {(x,y::'a::order). y<x}";
-by (Auto_tac);
- by (etac trancl_induct 1);
- by (Blast_tac 1);
- by (blast_tac (claset() addIs [order_less_trans]) 1);
-by (blast_tac (claset() addIs [r_into_trancl]) 1);
-qed "trancl_order1_conv";
-Addsimps [trancl_order1_conv];
-
-Goalw [acyclic_def] "acyclic{(x,y::'a::order). y<x}";
-by (Simp_tac 1);
-qed "acyclic_order1";
-AddIffs [acyclic_order1];
-
-Goalw [acc_def] "acc(UNIV::typ set)";
-by (rtac finite_acyclic_wf 1);
- by (fast_tac (claset() addIs [finite_SigmaI RSN (2,finite_subset)]) 1);
-by (blast_tac (claset() addIs [acyclic_subset]) 1);
-qed "acc_UNIV_typ";
-AddIffs [acc_UNIV_typ];
--- a/src/HOL/BCV/Types.thy Fri Sep 01 18:01:05 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,13 +0,0 @@
-(* Title: HOL/BCV/Types.thy
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1999 TUM
-
-Types for the register machine
-*)
-
-Types = Types0 +
-
-instance typ :: order (le_typ_refl,le_typ_trans,le_typ_antisym,less_le_typ)
-
-end
--- a/src/HOL/BCV/Types0.ML Fri Sep 01 18:01:05 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* Title: HOL/BCV/Types0.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1999 TUM
-*)
-
-Goalw [le_typ] "(t::typ) <= t";
-by (Blast_tac 1);
-qed "le_typ_refl";
-
-Goalw [le_typ] "[| (t1::typ) <= t2; t2<=t3 |] ==> 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];
--- 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