equal
deleted
inserted
replaced
16 addEs [evalc_WHILE_case]; |
16 addEs [evalc_WHILE_case]; |
17 |
17 |
18 (* evaluation of com is deterministic *) |
18 (* evaluation of com is deterministic *) |
19 goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"; |
19 goal Natural.thy "!!c s t. <c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)"; |
20 by (etac evalc.induct 1); |
20 by (etac evalc.induct 1); |
21 by (eres_inst_tac [("V", "<?c,s2> -c-> s1")] thin_rl 7); |
21 by (thin_tac "<?c,s2> -c-> s1" 7); |
22 by (ALLGOALS (deepen_tac evalc_cs 4)); |
22 by (ALLGOALS (deepen_tac evalc_cs 4)); |
23 qed_spec_mp "com_det"; |
23 qed_spec_mp "com_det"; |