28 Unify.trace_bound := 30; |
28 Unify.trace_bound := 30; |
29 Unify.search_bound := 60; |
29 Unify.search_bound := 60; |
30 |
30 |
31 (*Command execution is functional (deterministic) provided evaluation is*) |
31 (*Command execution is functional (deterministic) provided evaluation is*) |
32 goal thy "!!x. Function ev ==> Function(exec ev)"; |
32 goal thy "!!x. Function ev ==> Function(exec ev)"; |
33 by (simp_tac (!simpset addsimps [Function_def, Unique_def]) 1); |
33 by (simp_tac (simpset() addsimps [Function_def, Unique_def]) 1); |
34 by (REPEAT (rtac allI 1)); |
34 by (REPEAT (rtac allI 1)); |
35 by (rtac impI 1); |
35 by (rtac impI 1); |
36 by (etac exec.induct 1); |
36 by (etac exec.induct 1); |
37 by (Blast_tac 3); |
37 by (Blast_tac 3); |
38 by (Blast_tac 1); |
38 by (Blast_tac 1); |
39 by (rewrite_goals_tac [Function_def, Unique_def]); |
39 by (rewrite_goals_tac [Function_def, Unique_def]); |
40 by (thin_tac "(?c,s1) -[ev]-> s2" 5); |
40 by (thin_tac "(?c,s1) -[ev]-> s2" 5); |
41 (*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*) |
41 (*SLOW (23s) due to proof reconstruction; needs 60s if thin_tac is omitted*) |
42 by (REPEAT (blast_tac (!claset addEs [exec_WHILE_case]) 1)); |
42 by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1)); |
43 qed "Function_exec"; |
43 qed "Function_exec"; |
44 |
44 |
45 |
45 |
46 goalw thy [assign_def] "(s[v/x])x = v"; |
46 goalw thy [assign_def] "(s[v/x])x = v"; |
47 by (Simp_tac 1); |
47 by (Simp_tac 1); |
51 by (Asm_simp_tac 1); |
51 by (Asm_simp_tac 1); |
52 qed "assign_different"; |
52 qed "assign_different"; |
53 |
53 |
54 goalw thy [assign_def] "s[s x/x] = s"; |
54 goalw thy [assign_def] "s[s x/x] = s"; |
55 by (rtac ext 1); |
55 by (rtac ext 1); |
56 by (simp_tac (!simpset addsplits [expand_if]) 1); |
56 by (simp_tac (simpset() addsplits [expand_if]) 1); |
57 qed "assign_triv"; |
57 qed "assign_triv"; |
58 |
58 |
59 Addsimps [assign_same, assign_different, assign_triv]; |
59 Addsimps [assign_same, assign_different, assign_triv]; |