14 goalw Confluence.thy [confluence_def,strip_def] |
14 goalw Confluence.thy [confluence_def,strip_def] |
15 "!!u.[|confluence(Spar_red1)|]==> strip"; |
15 "!!u.[|confluence(Spar_red1)|]==> strip"; |
16 by (resolve_tac [impI RS allI RS allI] 1); |
16 by (resolve_tac [impI RS allI RS allI] 1); |
17 by (etac Spar_red.induct 1); |
17 by (etac Spar_red.induct 1); |
18 by (Fast_tac 1); |
18 by (Fast_tac 1); |
19 by (fast_tac (!claset addIs [Spar_red.trans]) 1); |
19 by (fast_tac (claset() addIs [Spar_red.trans]) 1); |
20 qed "strip_lemma_r"; |
20 qed "strip_lemma_r"; |
21 |
21 |
22 |
22 |
23 goalw Confluence.thy [confluence_def,strip_def] |
23 goalw Confluence.thy [confluence_def,strip_def] |
24 "!!u. strip==> confluence(Spar_red)"; |
24 "!!u. strip==> confluence(Spar_red)"; |
27 by (Fast_tac 1); |
27 by (Fast_tac 1); |
28 by (Clarify_tac 1); |
28 by (Clarify_tac 1); |
29 by (dres_inst_tac [("x1","z")] (spec RS mp) 1); |
29 by (dres_inst_tac [("x1","z")] (spec RS mp) 1); |
30 by (REPEAT(eresolve_tac [exE,conjE] 2)); |
30 by (REPEAT(eresolve_tac [exE,conjE] 2)); |
31 by (dres_inst_tac [("x1","ua")] (spec RS mp) 2); |
31 by (dres_inst_tac [("x1","ua")] (spec RS mp) 2); |
32 by (fast_tac (!claset addIs [Spar_red.trans]) 3); |
32 by (fast_tac (claset() addIs [Spar_red.trans]) 3); |
33 by (TRYALL assume_tac ); |
33 by (TRYALL assume_tac ); |
34 qed "strip_lemma_l"; |
34 qed "strip_lemma_l"; |
35 |
35 |
36 (* ------------------------------------------------------------------------- *) |
36 (* ------------------------------------------------------------------------- *) |
37 (* Confluence *) |
37 (* Confluence *) |
43 by (forward_tac [simulation] 1); |
43 by (forward_tac [simulation] 1); |
44 by (forw_inst_tac [("n","z")] simulation 1); |
44 by (forw_inst_tac [("n","z")] simulation 1); |
45 by (Clarify_tac 1); |
45 by (Clarify_tac 1); |
46 by (forw_inst_tac [("v","va")] paving 1); |
46 by (forw_inst_tac [("v","va")] paving 1); |
47 by (TRYALL assume_tac); |
47 by (TRYALL assume_tac); |
48 by (fast_tac (!claset addIs [completeness] addss (!simpset)) 1); |
48 by (fast_tac (claset() addIs [completeness] addss (simpset())) 1); |
49 qed "parallel_moves"; |
49 qed "parallel_moves"; |
50 |
50 |
51 bind_thm ("confluence_parallel_reduction", |
51 bind_thm ("confluence_parallel_reduction", |
52 parallel_moves RS strip_lemma_r RS strip_lemma_l); |
52 parallel_moves RS strip_lemma_r RS strip_lemma_l); |
53 |
53 |
54 goalw Confluence.thy [confluence_def] |
54 goalw Confluence.thy [confluence_def] |
55 "!!u.[|confluence(Spar_red)|]==> confluence(Sred)"; |
55 "!!u.[|confluence(Spar_red)|]==> confluence(Sred)"; |
56 by(blast_tac (!claset addIs [par_red_red, red_par_red]) 1); |
56 by(blast_tac (claset() addIs [par_red_red, red_par_red]) 1); |
57 val lemma1 = result(); |
57 val lemma1 = result(); |
58 |
58 |
59 bind_thm ("confluence_beta_reduction", |
59 bind_thm ("confluence_beta_reduction", |
60 confluence_parallel_reduction RS lemma1); |
60 confluence_parallel_reduction RS lemma1); |
61 |
61 |