src/HOL/IMPP/Com.ML
author nipkow
Mon, 29 Nov 2004 11:23:48 +0100
changeset 15339 a7b603bbc1e6
parent 13911 f5c3750292f5
child 17477 ceb42ea2f223
permissions -rw-r--r--
onsolete
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8180
879280b50571 added forgotten definition of make_imp_tac
oheimb
parents: 8177
diff changeset
     1
val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
879280b50571 added forgotten definition of make_imp_tac
oheimb
parents: 8177
diff changeset
     2
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     3
Goalw [body_def] "finite (dom body)";
13911
f5c3750292f5 added thm"..." due to new Map.thy
nipkow
parents: 10962
diff changeset
     4
by (rtac (thm"finite_dom_map_of") 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     5
qed "finite_dom_body";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     6
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     7
Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b";
13911
f5c3750292f5 added thm"..." due to new Map.thy
nipkow
parents: 10962
diff changeset
     8
by (dtac (thm"map_of_SomeD") 1);
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     9
by (Fast_tac 1);
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    10
qed "WT_bodiesD";
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    11
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    12
val WTs_elim_cases = map WTs.mk_cases
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    13
   ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", 
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    14
    "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    15
    "WT (BODY P)", "WT (X:=CALL P(a))"];
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    16
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    17
AddSEs WTs_elim_cases;