equal
deleted
inserted
replaced
54 |
54 |
55 Goalw (reachable_def::exec_rws) |
55 Goalw (reachable_def::exec_rws) |
56 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"; |
56 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"; |
57 by (asm_full_simp_tac (simpset() delsimps bex_simps) 1); |
57 by (asm_full_simp_tac (simpset() delsimps bex_simps) 1); |
58 by (split_all_tac 1); |
58 by (split_all_tac 1); |
59 by (Safe_tac); |
59 by Safe_tac; |
60 by (rename_tac "ex1 ex2 n" 1); |
60 by (rename_tac "ex1 ex2 n" 1); |
61 by (res_inst_tac [("x","(%i. if i<n then ex1 i \ |
61 by (res_inst_tac [("x","(%i. if i<n then ex1 i \ |
62 \ else (if i=n then Some a else None), \ |
62 \ else (if i=n then Some a else None), \ |
63 \ %i. if i<Suc n then ex2 i else t)")] bexI 1); |
63 \ %i. if i<Suc n then ex2 i else t)")] bexI 1); |
64 by (res_inst_tac [("x","Suc n")] exI 1); |
64 by (res_inst_tac [("x","Suc n")] exI 1); |
77 val [p1,p2] = goalw IOA.thy [invariant_def] |
77 val [p1,p2] = goalw IOA.thy [invariant_def] |
78 "[| !!s. s:starts_of(A) ==> P(s); \ |
78 "[| !!s. s:starts_of(A) ==> P(s); \ |
79 \ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \ |
79 \ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \ |
80 \ ==> invariant A P"; |
80 \ ==> invariant A P"; |
81 by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); |
81 by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); |
82 by (Safe_tac); |
82 by Safe_tac; |
83 by (rename_tac "ex1 ex2 n" 1); |
83 by (rename_tac "ex1 ex2 n" 1); |
84 by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1); |
84 by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1); |
85 by (Asm_full_simp_tac 1); |
85 by (Asm_full_simp_tac 1); |
86 by (nat_ind_tac "n" 1); |
86 by (nat_ind_tac "n" 1); |
87 by (fast_tac (claset() addIs [p1,reachable_0]) 1); |
87 by (fast_tac (claset() addIs [p1,reachable_0]) 1); |