36 val strenthen_pre = prove_goalw thy [Spec_def] |
36 val strenthen_pre = prove_goalw thy [Spec_def] |
37 "[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q" |
37 "[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q" |
38 (fn [prem1,prem2] =>[cut_facts_tac [prem2] 1, |
38 (fn [prem1,prem2] =>[cut_facts_tac [prem2] 1, |
39 fast_tac (!claset addIs [prem1]) 1]); |
39 fast_tac (!claset addIs [prem1]) 1]); |
40 |
40 |
41 val [iter_0,iter_Suc] = nat_recs Iter_def; |
|
42 |
|
43 val lemma = prove_goalw thy [Spec_def,While_def] |
41 val lemma = prove_goalw thy [Spec_def,While_def] |
44 "[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \ |
42 "[| Spec (%s.I s & b s) c I; !!s. [| I s; ~b s |] ==> q s |] \ |
45 \ ==> Spec inv (While b inv c) q" |
43 \ ==> Spec I (While b I c) q" |
46 (fn [prem1,prem2] => |
44 (fn [prem1,prem2] => |
47 [REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2, |
45 [REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2, |
48 etac thin_rl 1, res_inst_tac[("x","s")]spec 1, |
46 etac thin_rl 1, res_inst_tac[("x","s")]spec 1, |
49 res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1, |
47 res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1, |
50 simp_tac (!simpset addsimps [iter_0]) 1, |
48 Simp_tac 1, |
51 fast_tac (!claset addIs [prem2]) 1, |
49 fast_tac (!claset addIs [prem2]) 1, |
52 simp_tac (!simpset addsimps [iter_Suc,Seq_def]) 1, |
50 simp_tac (!simpset addsimps [Seq_def]) 1, |
53 cut_facts_tac [prem1] 1, fast_tac (!claset addIs [prem2]) 1]); |
51 cut_facts_tac [prem1] 1, fast_tac (!claset addIs [prem2]) 1]); |
54 |
52 |
55 val WhileRule = lemma RSN (2,strenthen_pre); |
53 val WhileRule = lemma RSN (2,strenthen_pre); |
56 |
54 |
57 |
55 |