author | paulson |
Fri, 29 Oct 2004 15:16:02 +0200 | |
changeset 15270 | 8b3f707a78a7 |
parent 14156 | 2072802ab0e3 |
child 17876 | b9c92f384109 |
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 |
||
9158 | 11 |
(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***) |
9846 | 12 |
structure Make_Elim = Make_Elim_Fun(val classical = classical); |
9158 | 13 |
|
14 |
(*we don't redeclare the original make_elim (Tactic.make_elim) for |
|
13034 | 15 |
compatibility with strange things done in many existing proofs *) |
9158 | 16 |
val cla_make_elim = Make_Elim.make_elim; |
2844 | 17 |
|
2469 | 18 |
(*** Applying ClassicalFun to create a classical prover ***) |
19 |
structure Classical_Data = |
|
20 |
struct |
|
9158 | 21 |
val make_elim = cla_make_elim |
2469 | 22 |
val mp = mp |
23 |
val not_elim = notE |
|
24 |
val classical = classical |
|
9158 | 25 |
val sizef = size_of_thm |
2469 | 26 |
val hyp_subst_tacs=[hyp_subst_tac] |
27 |
end; |
|
28 |
||
29 |
structure Cla = ClassicalFun(Classical_Data); |
|
8099 | 30 |
structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical; |
2469 | 31 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
7156
diff
changeset
|
32 |
|
2844 | 33 |
(*Better for fast_tac: needs no quantifier duplication!*) |
34 |
qed_goal "alt_ex1E" IFOL.thy |
|
3835 | 35 |
"[| EX! x. P(x); \ |
2844 | 36 |
\ !!x. [| P(x); ALL y y'. P(y) & P(y') --> y=y' |] ==> R \ |
37 |
\ |] ==> R" |
|
38 |
(fn major::prems => |
|
39 |
[ (rtac (major RS ex1E) 1), |
|
40 |
(REPEAT (ares_tac (allI::prems) 1)), |
|
41 |
(etac (dup_elim allE) 1), |
|
42 |
(IntPr.fast_tac 1)]); |
|
43 |
||
44 |
||
4305
03d7de40ee4f
The change from iffE to iffCE means fewer case splits in most cases. Very few
paulson
parents:
4095
diff
changeset
|
45 |
(*Propositional rules*) |
2469 | 46 |
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
|
47 |
addSEs [conjE,disjE,impCE,FalseE,iffCE]; |
2469 | 48 |
|
49 |
(*Quantifier rules*) |
|
2844 | 50 |
val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] |
51 |
addSEs [exE,alt_ex1E] addEs [allE]; |
|
2469 | 52 |
|
14156 | 53 |
val cla_setup = [fn thy => (claset_ref_of thy := FOL_cs; thy)]; |
54 |
||
55 |
val case_setup = |
|
56 |
[Method.add_methods |
|
57 |
[("case_tac", Method.goal_args Args.name case_tac, |
|
58 |
"case_tac emulation (dynamic instantiation!)")]]; |