24 |
24 |
25 Goal |
25 Goal |
26 "([False],[False]) : steps (atom a) w = (w = [])"; |
26 "([False],[False]) : steps (atom a) w = (w = [])"; |
27 by (induct_tac "w" 1); |
27 by (induct_tac "w" 1); |
28 by (Simp_tac 1); |
28 by (Simp_tac 1); |
29 by (asm_simp_tac (simpset() addsimps [comp_def]) 1); |
29 by (asm_simp_tac (simpset() addsimps [rel_comp_def]) 1); |
30 qed "False_False_in_steps_atom"; |
30 qed "False_False_in_steps_atom"; |
31 |
31 |
32 Goal |
32 Goal |
33 "(start (atom a), [False]) : steps (atom a) w = (w = [a])"; |
33 "(start (atom a), [False]) : steps (atom a) w = (w = [a])"; |
34 by (induct_tac "w" 1); |
34 by (induct_tac "w" 1); |
35 by (asm_simp_tac (simpset() addsimps [start_atom]) 1); |
35 by (asm_simp_tac (simpset() addsimps [start_atom]) 1); |
36 by (asm_full_simp_tac (simpset() |
36 by (asm_full_simp_tac (simpset() |
37 addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1); |
37 addsimps [False_False_in_steps_atom,rel_comp_def,start_atom]) 1); |
38 qed "start_fin_in_steps_atom"; |
38 qed "start_fin_in_steps_atom"; |
39 |
39 |
40 Goal |
40 Goal |
41 "accepts (atom a) w = (w = [a])"; |
41 "accepts (atom a) w = (w = [a])"; |
42 by (simp_tac(simpset() addsimps |
42 by (simp_tac(simpset() addsimps |