31 Addsimps [in_step_atom_Some]; |
31 Addsimps [in_step_atom_Some]; |
32 |
32 |
33 Goal "([False],[False]) : steps (atom a) w = (w = [])"; |
33 Goal "([False],[False]) : steps (atom a) w = (w = [])"; |
34 by (induct_tac "w" 1); |
34 by (induct_tac "w" 1); |
35 by (Simp_tac 1); |
35 by (Simp_tac 1); |
36 by (asm_simp_tac (simpset() addsimps [comp_def]) 1); |
36 by (asm_simp_tac (simpset() addsimps [rel_comp_def]) 1); |
37 qed "False_False_in_steps_atom"; |
37 qed "False_False_in_steps_atom"; |
38 |
38 |
39 Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])"; |
39 Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])"; |
40 by (induct_tac "w" 1); |
40 by (induct_tac "w" 1); |
41 by (asm_simp_tac (simpset() addsimps [start_atom,thm"rtrancl_empty"]) 1); |
41 by (asm_simp_tac (simpset() addsimps [start_atom,thm"rtrancl_empty"]) 1); |
42 by (asm_full_simp_tac (simpset() |
42 by (asm_full_simp_tac (simpset() |
43 addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1); |
43 addsimps [False_False_in_steps_atom,rel_comp_def,start_atom]) 1); |
44 qed "start_fin_in_steps_atom"; |
44 qed "start_fin_in_steps_atom"; |
45 |
45 |
46 Goal "accepts (atom a) w = (w = [a])"; |
46 Goal "accepts (atom a) w = (w = [a])"; |
47 by (simp_tac(simpset() addsimps |
47 by (simp_tac(simpset() addsimps |
48 [accepts_def,start_fin_in_steps_atom,fin_atom]) 1); |
48 [accepts_def,start_fin_in_steps_atom,fin_atom]) 1); |