diff -r 3a8d722fd3ff -r 16c4ea954511 IOA/meta_theory/IOA.ML --- a/IOA/meta_theory/IOA.ML Fri Nov 11 10:35:03 1994 +0100 +++ b/IOA/meta_theory/IOA.ML Mon Nov 21 17:50:34 1994 +0100 @@ -15,14 +15,14 @@ goal IOA.thy "asig_of() = x & starts_of() = y & trans_of() = z"; by (simp_tac (SS addsimps ioa_projections) 1); - val ioa_triple_proj = result(); + qed "ioa_triple_proj"; goalw IOA.thy [ioa_def,state_trans_def,actions_def, is_asig_def] "!!A. [| IOA(A); :trans_of(A) |] ==> a:actions(asig_of(A))"; by (REPEAT(etac conjE 1)); by (EVERY1[etac allE, etac impE, atac]); by (asm_full_simp_tac SS 1); -val trans_in_actions = result(); +qed "trans_in_actions"; goal IOA.thy "filter_oseq(p,filter_oseq(p,s)) = filter_oseq(p,s)"; @@ -31,7 +31,7 @@ by (Option.option.induct_tac "s(i)" 1); by (simp_tac SS 1); by (simp_tac (SS setloop (split_tac [expand_if])) 1); -val filter_oseq_idemp = result(); +qed "filter_oseq_idemp"; goalw IOA.thy [mk_behaviour_def,filter_oseq_def] "(mk_behaviour(A, s, n) = None) = \ @@ -42,13 +42,13 @@ by (Option.option.induct_tac "s(n)" 1); by (ALLGOALS (simp_tac (SS setloop (split_tac [expand_if])))); by (fast_tac HOL_cs 1); -val mk_behaviour_thm = result(); +qed "mk_behaviour_thm"; goalw IOA.thy [reachable_def] "!!A. s:starts_of(A) ==> reachable(A,s)"; by (res_inst_tac [("x","<(%i.None),(%i.s)>::('action,'a)execution")] bexI 1); by (simp_tac SS 1); by (asm_simp_tac (SS addsimps exec_rws) 1); -val reachable_0 = result(); +qed "reachable_0"; goalw IOA.thy (reachable_def::exec_rws) "!!A. [| reachable(A,s); : trans_of(A) |] ==> reachable(A,t)"; @@ -68,7 +68,7 @@ by(fast_tac HOL_cs 1); by(forward_tac [less_not_sym] 1); by(asm_simp_tac (SS addsimps [less_not_refl2]) 1); -val reachable_n = result(); +qed "reachable_n"; val [p1,p2] = goalw IOA.thy [invariant_def] "[| !!s. s:starts_of(A) ==> P(s); \ @@ -87,37 +87,37 @@ by (etac (p2 RS mp) 1); by (ALLGOALS(fast_tac(set_cs addDs [hd Option.option.inject RS iffD1, reachable_n]))); -val invariantI = result(); +qed "invariantI"; val [p1,p2] = goal IOA.thy "[| !!s. s : starts_of(A) ==> P(s); \ \ !!s t a. reachable(A, s) ==> P(s) --> :trans_of(A) --> P(t) \ \ |] ==> invariant(A, P)"; by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1); -val invariantI1 = result(); +qed "invariantI1"; val [p1,p2] = goalw IOA.thy [invariant_def] "[| invariant(A,P); reachable(A,s) |] ==> P(s)"; br(p2 RS (p1 RS spec RS mp))1; -val invariantE = result(); +qed "invariantE"; goal IOA.thy "actions(asig_comp(a,b)) = actions(a) Un actions(b)"; by(simp_tac (pair_ss addsimps ([actions_def,asig_comp_def]@asig_projections)) 1); by(fast_tac eq_cs 1); -val actions_asig_comp = result(); +qed "actions_asig_comp"; goal IOA.thy "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; by(simp_tac (SS addsimps (par_def::ioa_projections)) 1); -val starts_of_par = result(); +qed "starts_of_par"; (* Every state in an execution is reachable *) goalw IOA.thy [reachable_def] "!!A. ex:executions(A) ==> !n. reachable(A, snd(ex,n))"; by (fast_tac set_cs 1); -val states_of_exec_reachable = result(); +qed "states_of_exec_reachable"; goal IOA.thy @@ -136,15 +136,15 @@ by(simp_tac (SS addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq]@ ioa_projections) setloop (split_tac [expand_if])) 1); -val trans_of_par4 = result(); +qed "trans_of_par4"; goal IOA.thy "starts_of(restrict(ioa,acts)) = starts_of(ioa) & \ \ trans_of(restrict(ioa,acts)) = trans_of(ioa) & \ \ reachable(restrict(ioa,acts),s) = reachable(ioa,s)"; by(simp_tac (SS addsimps ([is_execution_fragment_def,executions_def, reachable_def,restrict_def]@ioa_projections)) 1); -val cancel_restrict = result(); +qed "cancel_restrict"; goal IOA.thy "asig_of(A || B) = asig_comp(asig_of(A),asig_of(B))"; by(simp_tac (SS addsimps (par_def::ioa_projections)) 1); -val asig_of_par = result(); +qed "asig_of_par";