equal
deleted
inserted
replaced
9 |
9 |
10 (* ------------------------------------------------------------------------- *) |
10 (* ------------------------------------------------------------------------- *) |
11 (* strip lemmas *) |
11 (* strip lemmas *) |
12 (* ------------------------------------------------------------------------- *) |
12 (* ------------------------------------------------------------------------- *) |
13 |
13 |
14 goalw Confluence.thy [confluence_def,strip_def] |
14 Goalw [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_def,strip_def] |
24 "!!u. strip==> confluence(Spar_red)"; |
24 "!!u. strip==> confluence(Spar_red)"; |
25 by (resolve_tac [impI RS allI RS allI] 1); |
25 by (resolve_tac [impI RS allI RS allI] 1); |
26 by (etac Spar_red.induct 1); |
26 by (etac Spar_red.induct 1); |
27 by (Fast_tac 1); |
27 by (Fast_tac 1); |
28 by (Clarify_tac 1); |
28 by (Clarify_tac 1); |
36 (* ------------------------------------------------------------------------- *) |
36 (* ------------------------------------------------------------------------- *) |
37 (* Confluence *) |
37 (* Confluence *) |
38 (* ------------------------------------------------------------------------- *) |
38 (* ------------------------------------------------------------------------- *) |
39 |
39 |
40 |
40 |
41 goalw Confluence.thy [confluence_def] "confluence(Spar_red1)"; |
41 Goalw [confluence_def] "confluence(Spar_red1)"; |
42 by (Clarify_tac 1); |
42 by (Clarify_tac 1); |
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); |
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_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", |