equal
deleted
inserted
replaced
15 val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t"; |
15 val evalc_WHILE_case = evalc.mk_cases com.simps "<WHILE b DO c,s> -c-> t"; |
16 |
16 |
17 AddSEs evalc_elim_cases; |
17 AddSEs evalc_elim_cases; |
18 |
18 |
19 (* evaluation of com is deterministic *) |
19 (* evaluation of com is deterministic *) |
20 Goal "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"; |
20 Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"; |
21 by (etac evalc.induct 1); |
21 by (etac evalc.induct 1); |
22 by (thin_tac "<?c,s2> -c-> s1" 7); |
22 by (thin_tac "<?c,s2> -c-> s1" 7); |
23 (*blast_tac needs Unify.search_bound, trace_bound := 40*) |
23 (*blast_tac needs Unify.search_bound, trace_bound := 40*) |
24 by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case]))); |
24 by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case]))); |
25 qed_spec_mp "com_det"; |
25 qed_spec_mp "com_det"; |