|
8180
|
1 |
val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
|
|
|
2 |
|
|
8177
|
3 |
Goalw [body_def] "finite (dom body)";
|
|
13911
|
4 |
by (rtac (thm"finite_dom_map_of") 1);
|
|
8177
|
5 |
qed "finite_dom_body";
|
|
|
6 |
|
|
|
7 |
Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b";
|
|
13911
|
8 |
by (dtac (thm"map_of_SomeD") 1);
|
|
8177
|
9 |
by (Fast_tac 1);
|
|
|
10 |
qed "WT_bodiesD";
|
|
|
11 |
|
|
|
12 |
val WTs_elim_cases = map WTs.mk_cases
|
|
|
13 |
["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)",
|
|
|
14 |
"WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
|
|
|
15 |
"WT (BODY P)", "WT (X:=CALL P(a))"];
|
|
|
16 |
|
|
|
17 |
AddSEs WTs_elim_cases;
|