author | wenzelm |
Sat, 01 Apr 2000 20:09:52 +0200 | |
changeset 8647 | 656f1b61875a |
parent 8099 | 6a087be9f6d9 |
child 9158 | 084abf3d0eff |
permissions | -rw-r--r-- |
2469 | 1 |
(* Title: FOL/cladata.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
7156
diff
changeset
|
6 |
Setting up the classical reasoner. |
2469 | 7 |
*) |
8 |
||
9 |
section "Classical Reasoner"; |
|
10 |
||
2844 | 11 |
|
2469 | 12 |
(*** Applying ClassicalFun to create a classical prover ***) |
13 |
structure Classical_Data = |
|
14 |
struct |
|
15 |
val sizef = size_of_thm |
|
16 |
val mp = mp |
|
17 |
val not_elim = notE |
|
18 |
val classical = classical |
|
19 |
val hyp_subst_tacs=[hyp_subst_tac] |
|
20 |
end; |
|
21 |
||
22 |
structure Cla = ClassicalFun(Classical_Data); |
|
8099 | 23 |
structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical; |
24 |
structure Obtain = ObtainFun(val that_atts = [Simplifier.simp_add_local, Cla.haz_intro_local]); |
|
2469 | 25 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
7156
diff
changeset
|
26 |
|
2844 | 27 |
(*Better for fast_tac: needs no quantifier duplication!*) |
28 |
qed_goal "alt_ex1E" IFOL.thy |
|
3835 | 29 |
"[| EX! x. P(x); \ |
2844 | 30 |
\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \ |
31 |
\ |] ==> R" |
|
32 |
(fn major::prems => |
|
33 |
[ (rtac (major RS ex1E) 1), |
|
34 |
(REPEAT (ares_tac (allI::prems) 1)), |
|
35 |
(etac (dup_elim allE) 1), |
|
36 |
(IntPr.fast_tac 1)]); |
|
37 |
||
38 |
||
4305
03d7de40ee4f
The change from iffE to iffCE means fewer case splits in most cases. Very few
paulson
parents:
4095
diff
changeset
|
39 |
(*Propositional rules*) |
2469 | 40 |
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] |
4305
03d7de40ee4f
The change from iffE to iffCE means fewer case splits in most cases. Very few
paulson
parents:
4095
diff
changeset
|
41 |
addSEs [conjE,disjE,impCE,FalseE,iffCE]; |
2469 | 42 |
|
43 |
(*Quantifier rules*) |
|
2844 | 44 |
val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] |
45 |
addSEs [exE,alt_ex1E] addEs [allE]; |
|
2469 | 46 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
7156
diff
changeset
|
47 |
val clasetup = [fn thy => (claset_ref_of thy := FOL_cs; thy)]; |