equal
deleted
inserted
replaced
|
1 |
|
2 (* $Id$ *) |
|
3 |
1 local |
4 local |
2 fun prover s = prove_goal Init.thy s |
5 fun prover s = prove_goal (the_context ()) s |
3 (K [force_tac (claset(), simpset() addsimps [Init_def]) 1]) |
6 (K [force_tac (claset(), simpset() addsimps [Init_def]) 1]) |
4 in |
7 in |
5 val const_simps = map (int_rewrite o prover) |
8 val const_simps = map (int_rewrite o prover) |
6 [ "|- (Init #True) = #True", |
9 [ "|- (Init #True) = #True", |
7 "|- (Init #False) = #False"] |
10 "|- (Init #False) = #False"] |
38 Goalw [Init_def,fw_act_def] "(sigma |= Init A) = A (st1 sigma, st2 sigma)"; |
41 Goalw [Init_def,fw_act_def] "(sigma |= Init A) = A (st1 sigma, st2 sigma)"; |
39 by (rtac refl 1); |
42 by (rtac refl 1); |
40 qed "Init_act"; |
43 qed "Init_act"; |
41 |
44 |
42 val Init_defs = [Init_stp, Init_act, int_use Init_temp]; |
45 val Init_defs = [Init_stp, Init_act, int_use Init_temp]; |
43 |
|