equal
deleted
inserted
replaced
23 |
23 |
24 val [_, spec_mp] = [spec] RL [mp]; |
24 val [_, spec_mp] = [spec] RL [mp]; |
25 |
25 |
26 (*Strip lemma. The induction hyp is all but the last diamond of the strip.*) |
26 (*Strip lemma. The induction hyp is all but the last diamond of the strip.*) |
27 Goalw [diamond_def] |
27 Goalw [diamond_def] |
28 "!!r. [| diamond(r); (x,y):r^* |] ==> \ |
28 "[| diamond(r); (x,y):r^* |] ==> \ |
29 \ ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)"; |
29 \ ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)"; |
30 by (etac rtrancl_induct 1); |
30 by (etac rtrancl_induct 1); |
31 by (Blast_tac 1); |
31 by (Blast_tac 1); |
32 by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)] |
32 by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)] |
33 addSDs [spec_mp]) 1); |
33 addSDs [spec_mp]) 1); |
116 Goal "S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')"; |
116 Goal "S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')"; |
117 by (Blast_tac 1); |
117 by (Blast_tac 1); |
118 qed "S1_parcontractD"; |
118 qed "S1_parcontractD"; |
119 AddSDs [S1_parcontractD]; |
119 AddSDs [S1_parcontractD]; |
120 |
120 |
121 Goal |
121 Goal "S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')"; |
122 "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')"; |
|
123 by (Blast_tac 1); |
122 by (Blast_tac 1); |
124 qed "S2_parcontractD"; |
123 qed "S2_parcontractD"; |
125 AddSDs [S2_parcontractD]; |
124 AddSDs [S2_parcontractD]; |
126 |
125 |
127 (*The rules above are not essential but make proofs much faster*) |
126 (*The rules above are not essential but make proofs much faster*) |