author | wenzelm |
Fri, 21 Nov 1997 15:29:56 +0100 | |
changeset 4271 | 3a82492e70c5 |
parent 4089 | 96fba19bcbe2 |
child 5069 | 3ea049f7979d |
permissions | -rw-r--r-- |
3210 | 1 |
(* Title: HOL/Modelcheck/MCSyn.ML |
2 |
ID: $Id$ |
|
3 |
Author: Olaf Mueller, Jan Philipps, Robert Sandner |
|
4 |
Copyright 1997 TU Muenchen |
|
5 |
*) |
|
6 |
||
3581 | 7 |
fun mc_tac i state = |
3210 | 8 |
let val sign = #sign (rep_thm state) |
9 |
in |
|
10 |
case drop(i-1,prems_of state) of |
|
4271
3a82492e70c5
changed Pure/Sequence interface -- isatool fixseq;
wenzelm
parents:
4089
diff
changeset
|
11 |
[] => Seq.empty | |
3210 | 12 |
subgoal::_ => |
13 |
let val concl = Logic.strip_imp_concl subgoal; |
|
3818 | 14 |
val OraAss = invoke_oracle MCSyn.thy "mc" (sign,MCOracleExn concl); |
3210 | 15 |
in |
16 |
((cut_facts_tac [OraAss] i) THEN (atac i)) state |
|
17 |
end |
|
18 |
end; |
|
19 |
||
20 |
||
21 |
goalw thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))"; |
|
3457 | 22 |
by (rtac ext 1); |
3210 | 23 |
by (stac (surjective_pairing RS sym) 1); |
3457 | 24 |
by (rtac refl 1); |
3210 | 25 |
qed "pair_eta_expand"; |
26 |
||
27 |
local |
|
3581 | 28 |
val lhss = [read_cterm (sign_of thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; |
3210 | 29 |
val rew = mk_meta_eq pair_eta_expand; |
30 |
||
3581 | 31 |
fun proc _ _ (Abs _) = Some rew |
32 |
| proc _ _ _ = None; |
|
3210 | 33 |
in |
34 |
val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc; |
|
35 |
end; |
|
36 |
||
37 |
||
3581 | 38 |
val MC_ss = |
4089 | 39 |
simpset() addsimprocs [pair_eta_expand_proc] |
3581 | 40 |
addsimps [split_paired_Ex, Let_def]; |