2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
3 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
4 Copyright 1997 TU Muenchen |
4 Copyright 1997 TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 fun mc_eindhoven_tac i state = |
7 fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) => |
8 let val sign = #sign (rep_thm state) |
8 let |
9 in |
9 val thy = Thm.theory_of_thm state; |
10 case Library.drop(i-1,prems_of state) of |
10 val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal); |
11 [] => Seq.empty | |
11 in cut_facts_tac [assertion] i THEN atac i end) i state; |
12 subgoal::_ => |
|
13 let val concl = Logic.strip_imp_concl subgoal; |
|
14 val OraAss = invoke_oracle EindhovenSyn.thy "eindhoven_mc" (sign,EindhovenOracleExn concl); |
|
15 in |
|
16 ((cut_facts_tac [OraAss] i) THEN (atac i)) state |
|
17 end |
|
18 end; |
|
19 |
|
20 |
12 |
21 Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))"; |
13 Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))"; |
22 by (rtac ext 1); |
14 by (rtac ext 1); |
23 by (stac (surjective_pairing RS sym) 1); |
15 by (stac (surjective_pairing RS sym) 1); |
24 by (rtac refl 1); |
16 by (rtac refl 1); |
25 qed "pair_eta_expand"; |
17 qed "pair_eta_expand"; |
26 |
18 |
27 val pair_eta_expand_proc = |
19 val pair_eta_expand_proc = |
28 Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"] |
20 Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"] |
29 (fn _ => fn _ => fn t => case t of Abs _ => SOME (mk_meta_eq pair_eta_expand) | _ => NONE); |
21 (fn _ => fn _ => fn t => case t of Abs _ => SOME (mk_meta_eq pair_eta_expand) | _ => NONE); |
30 |
22 |
31 val Eindhoven_ss = |
23 val Eindhoven_ss = |
32 simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def]; |
24 simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def]; |
33 |
25 |