author | wenzelm |
Mon, 02 Aug 1999 18:10:26 +0200 | |
changeset 7156 | 3e84e73a3b6a |
parent 5929 | 890f2f9b926d |
child 7355 | 4c43090659ca |
permissions | -rw-r--r-- |
2469 | 1 |
(* Title: FOL/cladata.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Setting up the classical reasoner |
|
7 |
*) |
|
8 |
||
9 |
||
10 |
section "Classical Reasoner"; |
|
11 |
||
2844 | 12 |
|
2469 | 13 |
(*** Applying ClassicalFun to create a classical prover ***) |
14 |
structure Classical_Data = |
|
15 |
struct |
|
16 |
val sizef = size_of_thm |
|
17 |
val mp = mp |
|
18 |
val not_elim = notE |
|
19 |
val classical = classical |
|
20 |
val hyp_subst_tacs=[hyp_subst_tac] |
|
21 |
end; |
|
22 |
||
23 |
structure Cla = ClassicalFun(Classical_Data); |
|
5929 | 24 |
structure BasicClassical: BASIC_CLASSICAL = Cla; |
25 |
open BasicClassical; |
|
2469 | 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 |
|
4095 | 47 |
claset_ref() := FOL_cs; |
2469 | 48 |
|
3610 | 49 |
|
2867 | 50 |
(*** Applying BlastFun to create Blast_tac ***) |
51 |
structure Blast_Data = |
|
52 |
struct |
|
53 |
type claset = Cla.claset |
|
54 |
val notE = notE |
|
55 |
val ccontr = ccontr |
|
56 |
val contr_tac = Cla.contr_tac |
|
57 |
val dup_intr = Cla.dup_intr |
|
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4305
diff
changeset
|
58 |
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac |
2867 | 59 |
val claset = Cla.claset |
4653 | 60 |
val rep_cs = Cla.rep_cs |
7156 | 61 |
val cla_modifiers = Cla.cla_modifiers; |
62 |
val cla_meth' = Cla.cla_meth' |
|
2867 | 63 |
end; |
64 |
||
65 |
structure Blast = BlastFun(Blast_Data); |
|
66 |
||
67 |
val Blast_tac = Blast.Blast_tac |
|
68 |
and blast_tac = Blast.blast_tac; |